Fixed EId, more work on other expressions needed

src/TypeChecker/TypeChecker.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE LambdaCase, OverloadedStrings #-}
+{-# LANGUAGE LambdaCase, OverloadedStrings, OverloadedRecordDot #-}
 
 module TypeChecker.TypeChecker (typecheck) where
 
@@ -18,6 +18,8 @@ import qualified Data.Map as M
 import Data.Set (Set)
 import qualified Data.Set as S
 
+import Data.Bool (bool)
+
 import qualified Grammar.Abs as Old
 import Grammar.ErrM (Err)
 
@@ -25,7 +27,7 @@ import TypeChecker.TypeCheckerIr
 
 data Ctx = Ctx
     { env :: [Map Ident Type]
-    , sig :: Map Ident Bind
+    , sigs :: Map Ident Type
     , typs :: Set Ident
     }
     deriving Show
@@ -35,7 +37,7 @@ type Check = ReaderT Ctx (ExceptT Error Identity)
 initEnv :: Ctx
 initEnv =
     Ctx { env = mempty
-        , sig = mempty
+        , sigs = mempty
         , typs = mempty
         }
 
@@ -54,7 +56,14 @@ inferBind (Bind _ _ e) = void $ inferExp e
 inferExp :: Old.Exp -> Check Type
 inferExp = \case
 
-    Old.EId i -> undefined
+    Old.EId i -> do
+        ctx <- R.ask
+        case lookupEnv i ctx of
+          Just t -> return t
+          Nothing -> case lookupSigs i ctx of
+                       Just t -> return t
+                       Nothing -> throwError UnboundVar
+        
 
     Old.EAnn e t -> do
         infT <- inferExp e
@@ -68,8 +77,12 @@ inferExp = \case
     Old.EAdd e1 e2 -> do
         t1 <- inferExp e1
         t2 <- inferExp e2
+        let int = TMono (UIdent "Int")
         case (t1, t2) of
-            (TMono (UIdent "Int"), TMono (UIdent "Int")) -> return t1
+            (TMono (UIdent "Int"), TMono (UIdent "Int")) -> return int
+            (_, TMono (UIdent "Int")) -> return int
+            (TMono (UIdent "Int"), _) -> return int
+            (TPoly (LIdent x), TPoly (LIdent y)) -> bool (throwError TypeMismatch) (return int) (x==y)
             _ -> throwError NotNumber
         return t1
 
@@ -95,27 +108,39 @@ inferExp = \case
 
 -- Aux
 
+-- Double check this function. It's bad and maybe wrong
 subtype :: Type -> Type -> Bool
 subtype (TMono t1) (TMono t2) = t1 == t2
 subtype (TMono t1) (TPoly t2) = True
 subtype (TPoly t2) (TMono t1) = False
 subtype (TArrow t1 t2) (TArrow t3 t4) = t1 `subtype` t3 && t2 `subtype` t4
+subtype _ _                   = False
 
 lookupEnv :: Ident -> Ctx -> Maybe Type
 lookupEnv i c = case env c of
     [] -> Nothing
     x : xs -> case M.lookup i x of
-            Nothing -> lookupEnv i (Ctx { env = xs })
+            Nothing -> lookupEnv i (Ctx { env = xs
+                                        , sigs = c.sigs
+                                        , typs = c.typs
+                                        })
             Just x -> Just x
 
-lookupSig :: Ident -> Ctx -> Maybe Bind
-lookupSig i = M.lookup i . sig
+lookupSigs :: Ident -> Ctx -> Maybe Type
+lookupSigs i = M.lookup i . sigs
 
 insertEnv :: Ident -> Type -> Ctx -> Ctx
 insertEnv i t c =
     case env c of
-        [] -> Ctx{env = [M.insert i t mempty]}
-        (x : xs) -> Ctx{env = M.insert i t x : xs}
+        [] -> Ctx { env = [M.insert i t mempty]
+                  , sigs = c.sigs
+                  , typs = c.typs
+                  }
+
+        (x : xs) -> Ctx { env = M.insert i t x : xs
+                        , sigs = c.sigs
+                        , typs = c.typs
+                        }
 
 data Error
     = TypeMismatch
@@ -145,17 +170,19 @@ data Error
 --             ]
 --     Default mess -> mess
 
-
 -- Tests
 
 number :: Old.Exp
 number = Old.EConst (CInt 3)
 
-lambda :: Old.Exp
-lambda = Old.EAbs (Old.Ident "x") (Old.EAdd (Old.EConst (Old.CInt 3)) (Old.EConst (Old.CInt 3)))
+aToInt :: Old.Exp
+aToInt = Old.EAbs (Old.Ident "x") (Old.EAdd (Old.EConst (Old.CInt 3)) (Old.EConst (Old.CInt 3)))
+
+intToInt :: Old.Exp
+intToInt = Old.EAbs (Old.Ident "x") (Old.EAdd (Old.EId $ Ident "x") (Old.EConst (Old.CInt 3)))
 
 apply :: Old.Exp
-apply = Old.EApp lambda (Old.EConst (Old.CInt 3))
+apply = Old.EApp aToInt (Old.EConst (Old.CInt 3))
 
 {-# WARNING todo "TODO IN CODE" #-}
 todo :: a