Add typecheck for let

app/Interpreter.hs

@@ -1,6 +1,6 @@
 module Main where
 
-import Control.Monad.Foil (emptyScope)
+import Control.Monad.Foil (emptyNameMap, emptyScope)
 import HM.Eval
 import HM.Parser.Par
 import HM.Syntax (toExpClosed)
@@ -22,9 +22,10 @@ main = do
 
 run :: String -> Result
 run input =
+
   case toExpClosed <$> pExp tokens of
     Left err -> Failure 1 ("Parsing error: " ++ err)
-    Right e -> case inferType e of
+    Right e -> case inferType emptyNameMap e of
       Left err -> Failure 2 ("Typechecking error: " ++ err)
       Right _type -> case eval emptyScope e of
         Left err -> Failure 3 ("Evaluation error: " ++ err)

app/Repl.hs

@@ -1,6 +1,6 @@
 module Main where
 
-import           Control.Monad.Foil (emptyScope)
+import           Control.Monad.Foil (emptyScope, emptyNameMap)
 import           HM.Eval
 import           HM.Parser.Par
 import           HM.Syntax          (toExpClosed)
@@ -15,7 +15,7 @@ repl :: String -> String
 repl input =
   case toExpClosed <$> pExp tokens of
     Left err -> "Parsing error: " ++ err
-    Right e -> case inferType e of
+    Right e -> case inferType emptyNameMap e of
       Left err -> "Typechecking error: " ++ err
       Right _type -> case eval emptyScope e of
         Left err     -> "Evaluation error: " ++ err

src/HM/Typecheck.hs

@@ -2,6 +2,7 @@
 
 module HM.Typecheck where
 
+import Control.Monad.Foil (NameMap, addNameBinder, emptyNameMap, lookupName)
 import qualified Control.Monad.Foil as Foil
 import qualified Control.Monad.Free.Foil as FreeFoil
 import HM.Parser.Abs (Type (..))
@@ -15,15 +16,17 @@ import HM.Syntax
 -- >>> typecheckClosed "2 - (1 + 1)" TNat
 -- >>> typecheckClosed "2 - (1 + true)" TNat
 -- >>> typecheckClosed "2 - (1 + 1)" TBool
+-- >>> typecheckClosed "let x = 1 in let y = 2 in x + (let x = 3 in x + y)" TNat
 -- Right TNat
 -- Left "expected type\n  TNat\nbut got type\n  Bool\nwhen typechecking expession\n  true\n"
 -- Left "expected type\n  TBool\nbut got type\n  Nat\nwhen typechecking expession\n  2 - (1 + 1)\n"
+-- Right TNat
 typecheckClosed :: Exp Foil.VoidS -> Type -> Either String Type
-typecheckClosed = typecheck
+typecheckClosed = typecheck emptyNameMap
 
-typecheck :: Exp n -> Type -> Either String Type
-typecheck e expectedType = do
-  typeOfE <- inferType e
+typecheck :: NameMap n Type -> Exp n -> Type -> Either String Type
+typecheck _scope e expectedType = do
+  typeOfE <- inferType _scope e
   if typeOfE == expectedType
     then return typeOfE
     else
@@ -37,25 +40,29 @@ typecheck e expectedType = do
             "  " ++ show e
           ]
 
-inferType :: Exp n -> Either String Type
-inferType ETrue = return TBool
-inferType EFalse = return TBool
-inferType (ENat _) = return TNat
-inferType (EIf eCond eThen eElse) = do
-  _ <- typecheck eCond TBool
-  typeOfThen <- inferType eThen
-  _ <- typecheck eElse typeOfThen
+inferType :: NameMap n Type -> Exp n -> Either String Type
+inferType _scope ETrue = return TBool
+inferType _scope EFalse = return TBool
+inferType _scope (ENat _) = return TNat
+inferType _scope (EIf eCond eThen eElse) = do
+  _ <- typecheck _scope eCond TBool
+  typeOfThen <- inferType _scope eThen
+  _ <- typecheck _scope eElse typeOfThen
   return typeOfThen
-inferType (EAdd l r) = do
-  _ <- typecheck l TNat
-  _ <- typecheck r TNat
+inferType _scope (EAdd l r) = do
+  _ <- typecheck _scope l TNat
+  _ <- typecheck _scope r TNat
   return TNat
-inferType (ESub l r) = do
-  _ <- typecheck l TNat
-  _ <- typecheck r TNat
+inferType _scope (ESub l r) = do
+  _ <- typecheck _scope l TNat
+  _ <- typecheck _scope r TNat
   return TNat
-inferType (EIsZero e) = do
-  _ <- typecheck e TNat
+inferType _scope (EIsZero e) = do
+  _ <- typecheck _scope e TNat
   return TBool
-inferType (FreeFoil.Var _) = error "Type inference for 'Var' is not implemented"
-inferType (FreeFoil.Node _) = error "Type inference for 'Node' is not implemented"
+inferType _scope (ELet pat e se) = do
+  patt <- inferType _scope pat
+  let newScope = addNameBinder e patt _scope
+  inferType newScope se
+inferType _scope (FreeFoil.Var n) = Right $ lookupName n _scope
+inferType _scope (FreeFoil.Node _) = error "Type inference for 'Node' is not implemented"