Browse Source

switch to reader model for type checking, got a lot of stuff done

master
depsterr 7 months ago
parent
commit
12b7a3c540
  1. 2
      TODO
  2. 2
      sexprml.cabal
  3. 37
      src/Parser/Parser.y
  4. 14
      src/Parser/SanityCheck.hs
  5. 26
      src/Parser/Types.hs
  6. 32
      src/Simple/AST.hs
  7. 28
      src/Simple/Convert.hs
  8. 237
      src/Simple/TC.hs
  9. 2
      src/Types.hs

2
TODO

@ -1,5 +1,5 @@
short term:
figure out how to represent types
non-empty list type
long term:
floats?

2
sexprml.cabal

@ -29,6 +29,7 @@ library
, Misc
, Simple.AST
, Simple.Convert
, Simple.TC
build-tool-depends: alex:alex >= 3.0, happy:happy >= 1.19.5
build-depends: base ^>=4.14.1.0
, array
@ -36,6 +37,7 @@ library
, transformers
, microlens
, microlens-th
, mtl
hs-source-dirs: src
default-language: Haskell2010

37
src/Parser/Parser.y

@ -96,9 +96,9 @@ toplevelsr :: { [TL] }
| toplevelsr toplvl { $2 : $1 }
toplvl :: { TL }
: '[' tysign ']' '(' def ident expr ')' {% i $6 >>= \x -> pure $ ExDef $5 $2 [(x, [], $7)] }
| '[' tysign ']' '(' def '(' ident patterns1 ')' expr ')' {% i $7 >>= \x -> pure $ ExDef $5 $2 [(x, $8, $10)] }
| '[' tysign ']' '(' def '(' defs ')' ')' { ExDef $5 $2 $7 }
: '[' tysign ']' '(' def ident expr ')' {% i $6 >>= \x -> pure $ ExDef $5 $2 x [([], $7)] }
| '[' tysign ']' '(' def '(' ident patterns1 ')' expr ')' {% i $7 >>= \x -> pure $ ExDef $5 $2 x [($8, $10)] }
| '[' tysign ']' '(' def '(' defs ')' ')' {% parseGeneralExDef $5 $2 $7 }
| '(' data ident typcons ')' {% i $3 >>= \x -> pure $ DtDef $2 x [] $4 }
| '(' data '(' ident idents ')' typcons ')' {% i $4 >>= \x -> pure $ DtDef $2 x $5 $7 }
| '(' record ident typcons ')' {% i $3 >>= \x -> pure $ RcDef $2 x [] $4 }
@ -155,7 +155,7 @@ expr :: { Expr }
| expr1 { EExp $1 }
expr1 :: { Expr1 }
: '(' instance idexprs ')' { Inst $2 $3 }
: '(' instance ident idexprs ')' {% i $3 >>= \x -> pure $ Inst $2 x $4 }
| '(' let idexprs in expr ')' { ELet $2 $3 $5 }
| '(' case expr cases ')' { ECase $2 $3 $4 }
| '(' expr args ')' { Apply (pos $2) $2 $3 }
@ -197,6 +197,15 @@ term :: { Term }
| '(' npl args ')' {% getTNpl $2 $3 }
| '(' lambda idents expr ')' { TLambda $2 $3 $4 }
| '(' lambdacase cases ')' { TLambdaCase $2 $3 }
| '(' lambda typedidents expr ')' { TyLambda $2 $3 $4 }
| '(' lambdacase tysign2 cases ')' { TyLambdaCase $2 $3 $4 }
typedidents :: { [(TYSG1, Identifier)] }
: typedidentsr { reverse $1 }
typedidentsr :: { [(TYSG1, Identifier)] }
: {-empty-} { [] }
| typedidentsr '[' tysign2 ']' ident {% i $5 >>= pure . (:$1) . ($3,) }
cases :: { [(Pattern, Expr)] }
: casesr { reverse $1 }
@ -254,4 +263,24 @@ expected = errorHere . ("Expected " <>)
expected1 :: String -> Alex a
expected1 = expected . ("one or more " <>)
-- I'm sorry
parseGeneralExDef :: PN -> TYSG -> [(Identifier, [Pattern], Expr)] -> Alex TL
parseGeneralExDef p tysg ipes = ExDef p tysg <$> goI <*> pure goPE
where
goPE :: [([Pattern], Expr)]
goPE = (\(_,ps,e) -> (ps,e)) <$> ipes
fst3 :: (a,b,c) -> a
fst3 (a,_,_) = a
i1 :: Alex Identifier
i1 = pure (fst3 (head ipes))
goI :: Alex Identifier
goI = foldr (\(i1,_,_) ai2 -> ai2
>>= \i2 -> if i1 == i2
then pure i1
else alexError' (fromPN p) ("Identifier '" <> unId i1 <> "' and '" <> unId i2 <> "' used in same definition")) i1 ipes
}

14
src/Parser/SanityCheck.hs

@ -38,8 +38,8 @@ sanityCheck fp tx tl = verifyTL <~> tl
-- | Verify that a top level decleration has valid type signatures, this does not do any form of
-- type checking.
verifyTL :: TL -> Either String TL
verifyTL (ExDef p t ipes) = ExDef p <$> verifyTYSG t <*>
(\(i,ps,e) -> (i,,) <$> verifyPattern <~> ps <*> verifyExpr e) <~> ipes
verifyTL (ExDef p t i pes) = ExDef p <$> verifyTYSG t <*> pure i <*>
(\(ps,e) -> (,) <$> verifyPattern <~> ps <*> verifyExpr e) <~> pes
verifyTL (DtDef p i is tis) = DtDef p i is <$>
(\(t,i') -> (,i') <$> verifyTYSG1 t) <~> tis
verifyTL (RcDef p i is tis) = RcDef p i is <$>
@ -75,8 +75,8 @@ sanityCheck fp tx tl = verifyTL <~> tl
-- | Verify an expr1.. you get the drill
verifyExpr1 :: Expr1 -> Either String Expr1
verifyExpr1 (Apply p e as) = Apply p <$> verifyExpr e <*> verifyArg <~> as
verifyExpr1 (ECase p e pes) = ECase p <$> verifyExpr e <*> (\(pt,ex) -> (pt,) <$> verifyExpr ex) <~> pes
verifyExpr1 (ELet p ies e) = ELet p <$> (\(i,ex) -> (i,) <$> verifyExpr ex) <~> ies <*> verifyExpr e
verifyExpr1 (Inst p ies) = Inst p <$> (\(i,e) -> (i,) <$> verifyExpr e) <~> ies
verifyExpr1 (Term t) = Term <$> verifyTerm t
verifyExpr1 (Apply p e as) = Apply p <$> verifyExpr e <*> verifyArg <~> as
verifyExpr1 (ECase p e pes) = ECase p <$> verifyExpr e <*> (\(pt,ex) -> (pt,) <$> verifyExpr ex) <~> pes
verifyExpr1 (ELet p ies e) = ELet p <$> (\(i,ex) -> (i,) <$> verifyExpr ex) <~> ies <*> verifyExpr e
verifyExpr1 (Inst p i ies) = Inst p i <$> (\(i,e) -> (i,) <$> verifyExpr e) <~> ies
verifyExpr1 (Term t) = Term <$> verifyTerm t

26
src/Parser/Types.hs

@ -43,13 +43,13 @@ instance Positioned TYSG1 where
-- | Top level parse tree
data TL
= ExDef PN TYSG [(Identifier, [Pattern], Expr)] -- ^ Definition with args
= ExDef PN TYSG Identifier [([Pattern], Expr)] -- ^ Definition with args
| DtDef PN Identifier [Identifier] [(TYSG1, Identifier)] -- ^ Data definition
| RcDef PN Identifier [Identifier] [(TYSG1, Identifier)] -- ^ Record definition
deriving Show
instance Positioned TL where
pos (ExDef p _ _) = p
pos (ExDef p _ _ _) = p
pos (DtDef p _ _ _) = p
pos (RcDef p _ _ _) = p
@ -82,18 +82,22 @@ instance Positioned Literal where
-- | A term, the core / lowest level of value
data Term
= TLit Literal
| TLambda PN [Identifier] Expr
| TLambdaCase PN [(Pattern, Expr)]
| TLambda PN [Identifier] Expr
| TLambdaCase PN [(Pattern, Expr)]
| TyLambda PN [(TYSG1, Identifier)] Expr
| TyLambdaCase PN TYSG1 [(Pattern, Expr)]
| TVar PN Identifier
| TNpl PN Int [Arg]
deriving Show
instance Positioned Term where
pos (TVar p _) = p
pos (TNpl p _ _) = p
pos (TLit l) = pos l
pos (TLambda p _ _) = p
pos (TLambdaCase p _) = p
pos (TVar p _) = p
pos (TNpl p _ _) = p
pos (TLit l) = pos l
pos (TLambda p _ _) = p
pos (TLambdaCase p _) = p
pos (TyLambda p _ _) = p
pos (TyLambdaCase p _ _) = p
-- | Implicit and explicit arguments
data Arg
@ -129,7 +133,7 @@ data Expr1
= Apply PN Expr [Arg]
| ECase PN Expr [(Pattern, Expr)]
| ELet PN [(Identifier, Expr)] Expr
| Inst PN [(Identifier, Expr)] -- ^ Instance
| Inst PN Identifier [(Identifier, Expr)] -- ^ Instance
| Term Term
deriving Show
@ -137,5 +141,5 @@ instance Positioned Expr1 where
pos (Apply p _ _) = p
pos (ECase p _ _) = p
pos (ELet p _ _) = p
pos (Inst p _) = p
pos (Inst p _ _) = p
pos (Term t) = pos t

32
src/Simple/AST.hs

@ -16,23 +16,31 @@ data Type
| UsrType PN Identifier
deriving Show
instance Eq Type where
FuncType _ t11 t12 == FuncType _ t21 t22 = t11 == t21 && t12 == t22
ChrType _ == ChrType _ = True
StrType _ == StrType _ = True
IntType _ == IntType _ = True
UsrType _ i1 == UsrType _ i2 = i1 == i2
_ == _ = False
instance Positioned Type where
pos (FuncType p _ _) = p
pos (ChrType p) = p
pos (StrType p) = p
pos (IntType p) = p
pos (UsrType p _ ) = p
pos (UsrType p _) = p
data TopLevel
= Def PN Type [(Identifier, [Pattern], Expr)] -- ^ Variable and function definition
= Def PN Type Identifier [([Pattern], Expr)] -- ^ Variable and function definition
| Dat PN Identifier [(Type, Identifier)] -- ^ Data definition
| Rec PN Identifier [(Type, Identifier)] -- ^ Record definition
deriving Show
instance Positioned TopLevel where
pos (Def p _ _) = p
pos (Dat p _ _) = p
pos (Rec p _ _) = p
pos (Def p _ _ _) = p
pos (Dat p _ _) = p
pos (Rec p _ _) = p
data Pattern
= Wild PN
@ -60,16 +68,16 @@ instance Positioned Literal where
data Term
= TLit Literal
| TLambda PN [Identifier] Expr
| TLambdaCase PN [(Pattern, Expr)]
| TLambda PN [(Type, Identifier)] Expr
| TLambdaCase PN Type [(Pattern, Expr)]
| TVar PN Identifier
deriving Show
instance Positioned Term where
pos (TLambdaCase p _) = p
pos (TLambda p _ _) = p
pos (TLit l) = pos l
pos (TVar p _) = p
pos (TLambdaCase p _ _) = p
pos (TLambda p _ _) = p
pos (TLit l) = pos l
pos (TVar p _) = p
data Expr
= ExpExpr Type Expr1
@ -84,6 +92,7 @@ data Expr1
= Apply PN Expr [Expr]
| Case PN Expr [(Pattern, Expr)]
| Let PN [(Identifier, Expr)] Expr
| Inst PN Identifier [(Identifier, Expr)]
| Term Term
deriving Show
@ -91,4 +100,5 @@ instance Positioned Expr1 where
pos (Apply p _ _) = p
pos (Case p _ _) = p
pos (Let p _ _) = p
pos (Inst p _ _) = p
pos (Term t) = pos t

28
src/Simple/Convert.hs

@ -23,7 +23,7 @@ convert fp tx = traverse convertTL
lerror p = Left . errorMessage p fp tx
convertTL :: P.TL -> Either String S.TopLevel
convertTL (P.ExDef p t ipes) = S.Def p <$> convertTYSG t <*> convertIPE <~> ipes
convertTL (P.ExDef p t i pes) = S.Def p <$> convertTYSG t <*> pure i <*> convertPE2 <~> pes
convertTL (P.DtDef p i (_:_) _) = lerror p ("Type arguments in definition of type '" <> unId i <> "'")
convertTL (P.DtDef p i [] tis) = S.Dat p i <$> convertTI <~> tis
convertTL (P.RcDef p i (_:_) _) = lerror p ("Type arguments in definition of record '" <> unId i <> "'")
@ -56,21 +56,23 @@ convert fp tx = traverse convertTL
convertLiteral (P.LString p s) = S.LStr p s
convertTerm :: P.Term -> Either String S.Term
convertTerm (P.TLit l) = pure (S.TLit (convertLiteral l))
convertTerm (P.TLambda p is e) = S.TLambda p is <$> convertExpr e
convertTerm (P.TLambdaCase p pes) = S.TLambdaCase p <$> convertPE <~> pes
convertTerm (P.TVar p i) = pure (S.TVar p i)
convertTerm (P.TNpl p _ _) = lerror p "Npl"
convertTerm (P.TLit l) = pure (S.TLit (convertLiteral l))
convertTerm (P.TLambda p _ _) = lerror p "Ambigously typed lambda"
convertTerm (P.TLambdaCase p _) = lerror p "Ambigously typed lambda"
convertTerm (P.TyLambda p tis e) = S.TLambda p <$> convertTI <~> tis <*> convertExpr e
convertTerm (P.TyLambdaCase p t pes) = S.TLambdaCase p <$> convertTYSG1 t <*> convertPE <~> pes
convertTerm (P.TVar p i) = pure (S.TVar p i)
convertTerm (P.TNpl p _ _) = lerror p "Npl"
convertExpr :: P.Expr -> Either String S.Expr
convertExpr (P.TExp t e) = S.ExpExpr <$> convertTYSG t <*> convertExpr1 e
convertExpr (P.EExp e) = S.ImpExpr <$> convertExpr1 e
convertExpr1 :: P.Expr1 -> Either String S.Expr1
convertExpr1 (P.Apply p e as) = S.Apply p <$> convertExpr e <*> convertArg <~> as
convertExpr1 (P.ECase p e pes) = S.Case p <$> convertExpr e <*> convertPE <~> pes
convertExpr1 (P.ELet p ies e) = S.Let p <$> convertIE <~> ies <*> convertExpr e
convertExpr1 (P.Inst p _) = lerror p "Instance"
convertExpr1 (P.Apply p e as) = S.Apply p <$> convertExpr e <*> convertArg <~> as
convertExpr1 (P.ECase p e pes) = S.Case p <$> convertExpr e <*> convertPE <~> pes
convertExpr1 (P.ELet p ies e) = S.Let p <$> convertIE <~> ies <*> convertExpr e
convertExpr1 (P.Inst p i ies) = S.Inst p i <$> convertIE <~> ies
convertExpr1 (P.Term t) = S.Term <$> convertTerm t
convertIE :: (Identifier, P.Expr) -> Either String (Identifier, S.Expr)
@ -79,6 +81,9 @@ convert fp tx = traverse convertTL
convertPE :: (P.Pattern, P.Expr) -> Either String (S.Pattern, S.Expr)
convertPE (p,e) = (convertPattern p,) <$> convertExpr e
convertPE2 :: ([P.Pattern], P.Expr) -> Either String ([S.Pattern], S.Expr)
convertPE2 (ps,e) = (convertPattern <$> ps,) <$> convertExpr e
convertArg :: P.Arg -> Either String S.Expr
convertArg (P.Imp a) = lerror (pos a) "Implicit argument"
convertArg (P.Exp (P.Wild p)) = lerror p "Wildcard argument"
@ -86,6 +91,3 @@ convert fp tx = traverse convertTL
convertTI :: (P.TYSG1, Identifier) -> Either String (S.Type, Identifier)
convertTI (t,i) = (,i) <$> convertTYSG1 t
convertIPE :: (Identifier, [P.Pattern], P.Expr) -> Either String (Identifier, [S.Pattern], S.Expr)
convertIPE (i,ps,e) = (i, convertPattern <$> ps,) <$> convertExpr e

237
src/Simple/TC.hs

@ -4,65 +4,200 @@ Description: Simple type checker.
A type checker for a simple subset of the language.
-}
{-# LANGUAGE GeneralizedNewtypeDeriving, LambdaCase #-}
{-# LANGUAGE GeneralizedNewtypeDeriving, LambdaCase, TupleSections, TemplateHaskell #-}
module Simple.TC where
import Simple.AST
import Types
import Control.Monad.Except
import Control.Monad.Reader
import Control.Monad.Reader hiding (guard)
import Control.Monad.Except hiding (guard)
import Data.Map (Map)
import Data.Set (Set)
import qualified Data.Map as M
import qualified Data.Set as S
import Lens.Micro
import Lens.Micro.TH
data TypeError
= Urk
| TypeMisMatch PN Got Expected
| TypeMismatch PN Type Type -- ^ expected, got
| ArityMismatch PN
| UnboundVar PN Identifier
| NoCase PN
| UnknownPattern PN
type Env a = Map Identifier a
data CheckEnv = CheckEnv { _defs :: Env Type
, _types :: Set Identifier
} deriving Show
makeLenses ''CheckEnv
newtype Check a = Check { getCheck :: ReaderT CheckEnv (ExceptT TypeError IO) a }
deriving (Functor, Applicative, Monad, MonadError TypeError, MonadReader CheckEnv)
askEnv :: Check (Env Type)
askEnv = (^. defs) <$> ask
localEnv :: (Env Type -> Env Type) -> Check a -> Check a
localEnv f = local (\env -> env & defs %~ f)
askTypeEnv :: Check (Set Identifier)
askTypeEnv = (^. types) <$> ask
localTypeEnv :: (Set Identifier -> Set Identifier) -> Check a -> Check a
localTypeEnv f = local (\env -> env & types %~ f)
guard :: Type -> TypeError -> Bool -> Check Type
guard t _ True = pure t
guard _ e False = throwError e
withBindings :: [(Type, Identifier)] -> Check a -> Check a
withBindings = localEnv . (flip insertBindings)
insertBindings :: Env a -> [(a, Identifier)] -> Env a
insertBindings = foldr (uncurry (flip M.insert))
iesTotis :: [(Identifier, Expr)] -> Check [(Type, Identifier)]
iesTotis ies = askEnv >>= \env -> traverse (\(i,e) -> (,i) <$> inferExpr e) ies
-- ^ Create function to third arg
tsToFunc :: PN -> [Type] -> Type -> Type
tsToFunc _ [] b = b
tsToFunc p (t:ts) b = FuncType p t (tsToFunc p ts b)
-- ^ Constructors of.. maybe I don't need this lol
consOf :: Type -> Check [(Type, Identifier)]
consOf t = pure . filter (constructs t . fst) . map flip2 . M.toList =<< askEnv
where
flip2 :: (a,b) -> (b,a)
flip2 (a,b) = (b,a)
-- ^ checks if second arg constructs first arg
constructs :: Type -> Type -> Bool
constructs t1 t2 | t1 == t2 = True
constructs t1 (FuncType _ t2 t3) = constructs t1 t3
constructs _ _ = False
checkExpr :: Type -> Expr -> Check Type
checkExpr t expr = inferExpr expr >>=
\t2 -> guard t (TypeMismatch (pos expr) t t2) (t == t2)
inferExpr :: Expr -> Check Type
inferExpr = \case
ExpExpr t e -> checkExpr1 t e >> pure t
ImpExpr e -> inferExpr1 e
checkExpr1 :: Type -> Expr1 -> Check Type
checkExpr1 t expr = inferExpr1 expr >>=
\t2 -> guard t (TypeMismatch (pos expr) t t2) (t == t2)
inferFunc :: PN -> Expr -> [Expr] -> Check Type
inferFunc p _ [] = throwError (ArityMismatch p)
inferFunc p e es = inferExpr e >>= \t -> go p t es
where
go :: PN -> Type -> [Expr] -> Check Type
go _ t [] = pure t
go p t (e:es) =
case t of
FuncType _ t1 t2 -> checkExpr t1 e >> go p t2 es
_ -> throwError (ArityMismatch p)
inferExpr1 :: Expr1 -> Check Type
inferExpr1 = \case
Apply p e es -> inferFunc p e es
Case p e pes -> inferExpr e >>= \t -> inferCase p t pes
Let _ ies e -> iesTotis ies >>= \tis -> withBindings tis (inferExpr e)
Inst p i ies -> undefined -- TODO
Term t -> inferTerm t
checkTerm :: Type -> Term -> Check Type
checkTerm t term = inferTerm term >>=
\t2 -> guard t (TypeMismatch (pos term) t t2) (t == t2)
inferTerm :: Term -> Check Type
inferTerm = \case
TLit l -> inferLiteral l
TLambda p tis e -> tsToFunc p (fst <$> tis) <$> withBindings tis (inferExpr e)
TLambdaCase p t pes -> inferCase p t pes
TVar p i -> askEnv >>= \env -> case M.lookup i env of
Just t -> pure t
Nothing -> throwError (UnboundVar p i)
checkLiteral :: Type -> Literal -> Check Type
checkLiteral t lit = inferLiteral lit >>=
\t2 -> guard t (TypeMismatch (pos lit) t t2) (t == t2)
inferLiteral :: Literal -> Check Type
inferLiteral = \case
LInt p _ -> pure (IntType p)
LChr p _ -> pure (ChrType p)
LStr p _ -> pure (StrType p)
-- no totality checking :/
inferCase :: PN -> Type -> [(Pattern, Expr)] -> Check Type
inferCase p _ [] = throwError (NoCase p)
inferCase p t ((pt,e):[]) = checkPattern t pt >> inferExpr e
inferCase p t ((pt,e):pes) = checkPattern t pt >> inferCase p t pes
>>= \t -> patternBindings t pt >>= \bs -> withBindings bs (checkExpr t e)
patternBindings :: Type -> Pattern -> Check [(Type, Identifier)]
patternBindings target = \case
Wild _ -> pure []
PLit _ -> pure []
PVar _ i -> askEnv >>= \env -> case M.lookup i env of
Just _ -> pure []
Nothing -> pure [(target, i)]
PApp p _ [] -> throwError (UnknownPattern p)
PApp p i ps -> askEnv >>= \env -> case M.lookup i env of
Just t -> go p t ps
Nothing -> throwError (UnknownPattern p)
where
go :: PN -> Type -> [Pattern] -> Check [(Type, Identifier)]
go _ _ [] = pure []
go p t (pt:ps) =
case t of
FuncType _ t1 t2 -> case pt of
PVar _ i -> ((t1, i):) <$> go p t2 ps
PApp p i ps -> askEnv >>= \env -> case M.lookup i env of
Just t -> go p t ps
Nothing -> throwError (UnknownPattern p)
_ -> go p t2 ps
_ -> throwError (ArityMismatch p)
checkPattern :: Type -> Pattern -> Check Type
checkPattern t pt = inferPattern t pt >>=
\t2 -> guard t (TypeMismatch (pos pt) t t2) (t == t2)
inferPattern :: Type -> Pattern -> Check Type
inferPattern target = \case
Wild p -> pure target
PVar p i -> askEnv >>= \env -> case M.lookup i env of
Just t -> pure t
Nothing -> pure target -- variable
PLit l -> inferLiteral l
PApp p _ [] -> throwError (UnknownPattern p)
PApp p i ps -> askEnv >>= \env -> case M.lookup i env of
Just t -> go p t ps
Nothing -> throwError (UnknownPattern p)
where
go :: PN -> Type -> [Pattern] -> Check Type
go _ t [] = pure t
go p t (pt:ps) =
case t of
FuncType _ t1 t2 -> checkPattern t1 pt >> go p t2 ps
_ -> throwError (ArityMismatch p)
-- This goes on the users given declerations, if they've been wrong it'll error out later
withTlBinding :: Check a -> TopLevel -> Check a
withTlBinding = undefined
checkTopLevel :: Type -> TopLevel -> Check Type
checkTopLevel t tl = inferTopLevel tl >>=
\t2 -> guard t (TypeMismatch (pos tl) t t2) (t == t2)
data Env = Map Identifier TypeSignature
newtype Check a = Check { getCheck :: ReaderT (Except TypeError) Env a }
deriving (Functor, Applicative, Monad, MonadReader Env, MonadError TypeError)
guard :: TypeError -> Bool -> Check ()
guard e True = pure ()
guard e False = throwError e
checkExpr :: Type -> Env -> Expr -> Check ()
checkExpr type = guard TypeMismatch . (==type) =<< inferExp
inferExpr :: Env -> Expr -> Check Type
inferExpr env = \case
ExpExpr t e -> checkExpr1 t env e >> pure t
ImpExpr e -> inferExpr1 env e
checkExpr1 :: Type -> Env -> Expr -> Check ()
checkExpr1 type = guard TypeMisMatch . (==type) =<< inferExpr1
inferExpr1 :: Env -> Expr1 -> Check Type
inferExpr1 env = \case
Apply p e es -> -- infer first and check rest
Case p e p es -> throwError Urk
Let p ie e -> -- insert stuff <$> inferExpr1 e env'
Term t -> inferTerm env t
checkTerm :: Type -> Env -> Term -> Check ()
checkTerm type = guard TypeMisMatch . (==type) =<< inferTerm
inferTerm :: Env -> Term -> Check Type
inferTerm env = \case
TLit l -> inferLiteral env l
TLambda p is e ->
TLambdaCase p ie ->
TVar p i -> case M.lookup i env of
Just t -> pure t
Nothing -> throwError (UnboundVar p i)
checkLiteral :: Type -> Env -> Term -> Check ()
checkLiteral type = guard TypeMisMatch . (==type) =<< inferLiteral
inferLiteral :: Env -> Term -> Check Type
inferLiteral env = \case
LInt _ _ -> pure IntType
LChr _ _ -> pure ChrType
LStr _ _ -> pure StrType
inferTopLevel :: TopLevel -> Check Type
inferTopLevel = undefined

2
src/Types.hs

@ -11,7 +11,7 @@ import Lens.Micro.TH
-- | Represents text in an identifier
newtype Identifier = Id { unId :: String }
deriving Show
deriving (Show, Eq, Ord)
-- | An abslute offset in a file
type Offset = Int

Loading…
Cancel
Save