Minor rewrite of tc. Some bugs still left

Grammar.cf

@@ -3,7 +3,7 @@ Program. Program ::= [Bind] ;
 
 Bind. Bind ::= Ident [Ident] "=" Exp ;
 
-EAnn.   Exp5 ::= Exp5 ":" Type ;
+EAnn.   Exp5 ::= "(" Exp ":" Type ")" ;
 EId.    Exp4 ::= Ident ;
 EConst. Exp4 ::= Const ;
 EApp.   Exp3 ::= Exp3 Exp4 ;
@@ -16,8 +16,9 @@ CStr. Const ::= String ;
 
 TMono. Type ::= "Mono" Ident ;
 TPoly. Type ::= "Poly" Ident ;
-TArrow. Type ::= Type "->" Type1 ;
+TArrow. Type ::= Type1 "->" Type ;
 
+-- This doesn't seem to work so we'll have to live with ugly keywords for now
 -- token Upper (upper (letter | digit | '_')*) ;
 -- token Lower (lower (letter | digit | '_')*) ;
 

src/Main.hs

@@ -7,6 +7,7 @@ import           System.Environment (getArgs)
 import           System.Exit        (exitFailure, exitSuccess)
 import           TypeChecker.TypeChecker (typecheck)
 import           Renamer.Renamer (rename)
+import           Grammar.Print (prt)
 
 main :: IO ()
 main = getArgs >>= \case
@@ -19,10 +20,14 @@ main = getArgs >>= \case
        putStrLn err
        exitFailure
       Right prg -> case rename prg of
-        Right prg -> do
-            putStrLn "RENAME SUCCESSFUL"
-            putStrLn $ printTree prg
         Left err -> do
           putStrLn "FAILED RENAMING"
           putStrLn . show $ err
           exitFailure
+        Right prg -> case typecheck prg of
+            Left err -> do
+                putStrLn "TYPECHECK ERROR"
+                putStrLn . show $ err
+                exitFailure
+            Right prg -> do
+                putStrLn . printTree $ prg

src/Renamer/RenamerIr.hs

@@ -1,6 +1,12 @@
 {-# LANGUAGE LambdaCase #-}
 
-module Renamer.RenamerIr (module Grammar.Abs, RExp (..), RBind (..), RProgram (..)) where
+module Renamer.RenamerIr ( RExp (..)
+                         , RBind (..)
+                         , RProgram (..)
+                         , Const (..)
+                         , Ident (..)
+                         , Type (..)
+                         ) where
 
 import Grammar.Abs (
     Bind (..),
@@ -43,6 +49,7 @@ instance Print RBind where
 
 instance Print RExp where
     prt i = \case
+        RAnn e t -> prPrec i 2 (concatD [prt 0 e, doc (showString ":"), prt 1 t])
         RBound n _ -> prPrec i 3 (concatD [prt 0 ("var" ++ show n)])
         RFree id -> prPrec i 3 (concatD [prt 0 id])
         RConst n -> prPrec i 3 (concatD [prt 0 n])

src/TypeChecker/TypeChecker.hs

@@ -1,6 +1,6 @@
 {-# LANGUAGE LambdaCase, OverloadedStrings, OverloadedRecordDot #-}
 
-module TypeChecker.TypeChecker (typecheck) where
+module TypeChecker.TypeChecker where
 
 import Control.Monad (when, void)
 import Control.Monad.Except (ExceptT, throwError, runExceptT)
@@ -13,15 +13,11 @@ import qualified Control.Monad.State as St
 import Data.Functor.Identity (Identity, runIdentity)
 import Data.Map (Map)
 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)
 
 import TypeChecker.TypeCheckerIr
 
-data Ctx = Ctx { env :: Map Ident Type
+data Ctx = Ctx { vars :: Map Integer Type
                , sigs :: Map Ident Type
                }
     deriving Show
@@ -34,120 +30,164 @@ programmer.
 
 -}
 
-type Check = StateT (Map Ident Type) (ReaderT Ctx (ExceptT Error Identity))
+type Infer = StateT Ctx (ExceptT Error Identity)
 
 initEnv :: Ctx
-initEnv =
+initEnv = Ctx mempty mempty
-    Ctx { env = mempty
-        , sigs = mempty
-        }
 
-run :: Check Type -> Either Error Type
+run :: Infer a -> Either Error a
-run = runIdentity . runExceptT . flip R.runReaderT initEnv . flip St.evalStateT mempty
+run = runIdentity . runExceptT . flip St.evalStateT initEnv
 
-typecheck :: Old.Program -> Either Error ()
+typecheck :: RProgram -> Either Error TProgram
-typecheck = todo
+typecheck = run . inferPrg 
 
-inferPrg :: Old.Program -> Check ()
+inferPrg :: RProgram -> Infer TProgram
-inferPrg (Program [x]) = void $ inferBind x
+inferPrg (RProgram xs) = do
+    xs' <- mapM inferBind xs
+    return $ TProgram xs'
 
-inferBind :: Old.Bind -> Check ()
+inferBind :: RBind -> Infer TBind
-inferBind (Bind _ _ e) = void $ inferExp e
+inferBind (RBind name e) = do
+    t <- inferExp e
+    e' <- toTExpr e
+    return $ TBind name t e'
 
-inferExp :: Old.Exp -> Check Type
+toTExpr :: RExp -> Infer TExp
+toTExpr = \case
+
+    re@(RAnn e t) -> do
+        t <- inferExp re
+        e' <- toTExpr e
+        return $ TAnn e' t
+
+    re@(RBound num name) -> do
+        t <- inferExp re
+        return $ TBound num name t
+
+    re@(RFree name) -> do
+        t <- inferExp re
+        return $ TFree name t
+
+    re@(RConst con)-> do
+        t <- inferExp re
+        return $ TConst con t
+
+    re@(RApp e1 e2) -> do
+        t <- inferExp re
+        e1' <- toTExpr e1
+        e2' <- toTExpr e2
+        return $ TApp e1' e2' t
+
+    re@(RAdd e1 e2)-> do
+        t <- inferExp re
+        e1' <- toTExpr e1
+        e2' <- toTExpr e2
+        return $ TAdd e1' e2' t
+
+    re@(RAbs num name e) -> do
+        t <- inferExp re
+        e' <- toTExpr e
+        return $ TAbs num name e' t
+
+
+inferExp :: RExp -> Infer Type
 inferExp = \case
 
-    -- TODO: Fix bound variable lookup
+    RAnn expr typ -> do
-    Old.EId i -> do
+        exprT <- inferExp expr
-        st <- St.get 
+        when (not (exprT == typ || isPoly exprT)) (throwError AnnotatedMismatch)
-        case lookupBound i st of
+        return typ
+
+    -- Name is only here for proper error messages
+    RBound num name ->
+        M.lookup num <$> St.gets vars >>= \case
+            Nothing -> throwError UnboundVar
             Just t -> return t
-          Nothing -> do
+
-            ctx <- R.ask
+    RFree name -> do
-            case lookupEnv i ctx of
+        M.lookup name <$> St.gets sigs >>= \case
+            Nothing -> throwError UnboundVar
             Just t -> return t
-              Nothing -> case lookupSigs i ctx of
+
+    RConst (CInt _) -> return $ TMono "Int"
+    RConst (CStr _) -> return $ TMono "Str"
+
+    -- Currently does not accept using a polymorphic type as the function.
+    RApp expr1 expr2 -> do
+        typ1 <- inferExp expr1
+        typ2 <- inferExp expr2
+        fit typ2 typ1
+
+    RAdd expr1 expr2 -> do
+        typ1 <- inferExp expr1
+        typ2 <- inferExp expr2
+        when (not $ (isInt typ1 || isPoly typ1) && (isInt typ2 || isPoly typ2)) (throwError TypeMismatch)
+        specifyType expr1 (TMono "Int")
+        specifyType expr2 (TMono "Int")
+        return (TMono "Int")
+
+    RAbs num name expr -> do
+        insertVars num (TPoly "a")
+        typ <- inferExp expr
+        newTyp <- lookupVars num
+        return $ TArrow newTyp typ
+
+-- Aux
+isInt :: Type -> Bool
+isInt (TMono "Int") = True
+isInt _             = False
+
+isArrow :: Type -> Bool
+isArrow (TArrow _ _) = True
+isArrow _            = False
+
+isPoly :: Type -> Bool
+isPoly (TPoly _) = True
+isPoly _         = False
+
+fit :: Type -> Type -> Infer Type
+fit (TArrow t1 (TArrow t2 t3)) t4
+  | t1 == t4 = return $ TArrow t2 t3
+  | otherwise = fit (TArrow (TArrow t1 t2) t3) t4
+fit (TArrow t1 t2) t3
+  | t1 == t3 = return t2
+  | otherwise = throwError TypeMismatch
+fit _ _ = throwError TypeMismatch
+
+-- a -> (b -> (c -> d))
+-- a -> b
+
+-- | Specify the type of a bound variable
+-- Because in lambdas we have to assume a general type and update it
+specifyType :: RExp -> Type -> Infer ()
+specifyType (RBound num name) typ = do
+    insertVars num typ
+    return ()
+specifyType _ _ = return ()
+
+lookupVars :: Integer -> Infer Type
+lookupVars i = do
+    st <- St.gets vars
+    case M.lookup i st of
       Just t -> return t
       Nothing -> throwError UnboundVar
 
-    Old.EAnn e t -> do
+lookupSigs :: Ident -> Infer Type
-        infT <- inferExp e
+lookupSigs i = do
-        when (t /= infT) (throwError AnnotatedMismatch)
+    st <- St.gets sigs
-        return infT
+    case M.lookup i st of
+      Just t -> return t
+      Nothing -> throwError UnboundVar
 
-    Old.EConst c -> case c of
-        (Old.CInt i) -> return (TMono "Int")
-        (Old.CStr s) -> return (TMono "String")
 
-    Old.EAdd e1 e2 -> do
+insertVars :: Integer -> Type -> Infer ()
-        let int = TMono "Int"
+insertVars i t = do
-        updateBound e1 int
+    st <- St.get
-        updateBound e2 int
+    St.put ( Ctx { vars = M.insert i t st.vars, sigs = st.sigs } )
-        inf1 <- inferExp e1
-        inf2 <- inferExp e2
-        when (not $ isInt inf1 && isInt inf2) (throwError TypeMismatch)
-        return int
 
-    -- Incomplete and probably wrong
+{-# WARNING todo "TODO IN CODE" #-}
-    Old.EApp e1 e2 -> do
+todo :: a
-        inferExp e1 >>= \case
+todo = error "TODO in code"
-            TArrow mono@(TMono i) t2 -> do
-                t <- inferExp e2
-                when (t /= mono) (throwError TypeMismatch)
-                return t2
-
-            TArrow poly@(TPoly f) t2 -> do
-                t <- inferExp e2 
-                when (not $ t `subtype` t) (throwError TypeMismatch)
-                return t2
-
-    -- This is not entirely correct. The assumed type can change.
-    Old.EAbs i e -> do
-        let assume = (TPoly "a")
-        St.modify (M.insert i assume)
-        infT <- R.local (insertEnv i assume) (inferExp e)
-        St.gets (M.lookup i) >>= \case
-            Nothing -> todo
-            Just x -> return (TArrow x infT)
-
-    Old.ELet i e1 e2 -> todo
-
--- 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 = M.lookup i . env
-
-lookupSigs :: Ident -> Ctx -> Maybe Type
-lookupSigs i = M.lookup i . sigs
-
-insertEnv :: Ident -> Type -> Ctx -> Ctx
-insertEnv i t c = Ctx { env = M.insert i t c.env
-                      , sigs = c.sigs
-                      }
-
-updateBound :: Old.Exp -> Type -> Check ()
-updateBound (Old.EId i) t = St.modify (M.insert i t)
-updateBound _ _           = return ()
-
-isBound :: Old.Exp -> Check Bool
-isBound (Old.EId i) = (M.member i) <$> St.get
-isBound _           = return False
-
-lookupBound :: Ident -> Map Ident Type -> Maybe Type
-lookupBound = M.lookup
-
-isInt :: Type -> Bool
-isInt (TMono "Int") = True
-isInt (TPoly _)     = True
-isInt _             = False
 
 data Error
     = TypeMismatch
@@ -161,18 +201,17 @@ data Error
 
 -- Tests
 
-number :: Old.Exp
+lambda = RAbs 0 "x" (RAdd (RBound 0 "x") (RBound 0 "x"))
-number = Old.EConst (CInt 3)
+lambda2 = RAbs 0 "x" (RAnn (RBound 0 "x") (TArrow (TMono "Int") (TMono "String")))
 
-aToInt :: Old.Exp
+pp :: Type -> String
-aToInt = Old.EAbs (Old.Ident "x") (Old.EAdd (Old.EConst (Old.CInt 3)) (Old.EConst (Old.CInt 3)))
+pp (TMono (Ident x)) = x
+pp (TPoly (Ident x)) = x
+pp (TArrow t1 t2) = pp t1 <> " -> " <> pp t2
 
-intToInt :: Old.Exp
+int,str :: Type
-intToInt = Old.EAbs (Old.Ident "x") (Old.EAdd (Old.EId $ Ident "x") (Old.EConst (Old.CInt 3)))
+int = TMono "Int"
+str = TMono "Str"
 
-addLambda :: Old.Exp
+arrow :: Type -> Type -> Type
-addLambda = Old.EAbs (Old.Ident "x") (Old.EAdd (Old.EId $ Ident "x") (Old.EId $ Ident "x"))
+arrow = TArrow
-
-{-# WARNING todo "TODO IN CODE" #-}
-todo :: a
-todo = error "TODO in code"

src/TypeChecker/TypeCheckerIr.hs

@@ -1,12 +1,25 @@
 {-# LANGUAGE LambdaCase #-}
 
-module TypeChecker.TypeCheckerIr where
+module TypeChecker.TypeCheckerIr ( TProgram(..)
+                                 , TBind(..)
+                                 , TExp(..)
+                                 , RProgram(..)
+                                 , RBind(..)
+                                 , RExp(..)
+                                 , Type(..)
+                                 , Const(..)
+                                 , Ident(..)
+                                 )
+                                     where
 
 import Renamer.RenamerIr
+import Grammar.Print
 
 data TProgram = TProgram [TBind]
+    deriving (Eq, Show, Read, Ord)
 
 data TBind = TBind Ident Type TExp
+    deriving (Eq, Show, Read, Ord)
 
 data TExp
     = TAnn TExp Type
@@ -17,3 +30,69 @@ data TExp
     | TAdd TExp TExp Type
     | TAbs Integer Ident TExp Type
     deriving (Eq, Ord, Show, Read)
+
+instance Print TProgram where
+    prt i = \case
+        TProgram defs -> prPrec i 0 (concatD [prt 0 defs])
+
+instance Print TBind where
+    prt i = \case
+        TBind x t e ->
+            prPrec i 0 $
+                concatD
+                    [ prt 0 x
+                    , doc (showString ":")
+                    , prt 0 t
+                    , doc (showString "=")
+                    , prt 0 e
+                    ]
+
+instance Print TExp where
+    prt i = \case
+        TAnn e t -> prPrec i 2 $ concatD
+            [ prt 0 e
+            , doc (showString ":")
+            , prt 1 t
+            ]
+        TBound _ u t -> prPrec i 3 $ concatD
+              [ doc (showString "(")
+              , prt 0 u
+              , doc (showString ":")
+              , prt 0 t
+              , doc (showString ")")
+              ]
+        TFree u t -> prPrec i 3 $ concatD
+              [ doc (showString "(")
+              , prt 0 u
+              , doc (showString ":")
+              , prt 0 t
+              , doc (showString ")")
+              ]
+        TConst c _ -> prPrec i 3 (concatD [prt 0 c])
+        TApp e e1 t -> prPrec i 2 $ concatD
+              [ doc (showString "(")
+              , prt 2 e
+              , prt 3 e1
+              , doc (showString ")")
+              , doc (showString ":")
+              , prt 0 t
+              ]
+        TAdd e e1 t -> prPrec i 1 $ concatD
+              [ doc (showString "(")
+              , prt 1 e
+              , doc (showString "+")
+              , prt 2 e1
+              , doc (showString ")")
+              , doc (showString ":")
+              , prt 0 t
+              ]
+        TAbs _ u e t -> prPrec i 0 $ concatD
+              [ doc (showString "(")
+              , doc (showString "\\")
+              , prt 0 u
+              , doc (showString ".")
+              , prt 0 e
+              , doc (showString ")")
+              , doc (showString ":")
+              , prt 0 t, doc (showString ".")
+              ]

test_program

@@ -1,4 +1 @@
-letters = let x = 1
+testType f x = f x
-           in let y = 2
-               in let z = 3
-                   in x + y + z