Merge branch 'typechecking' into codegen-martin-3

Grammar.cf

@@ -1,4 +1,7 @@
+Program. Program ::= [Def] ;
 
+DExp.  Def ::= Ident ":" Type
+               Ident [Ident] "=" Exp ;
 
 Program. Program ::= [Bind];
 

Makefile

@@ -1,7 +1,7 @@
 .PHONY : sdist clean
 
 language : src/Grammar/Test
-	cabal install --installdir=.
+	cabal install --installdir=. --overwrite-policy=always
 
 src/Grammar/Test.hs src/Grammar/Lex.x src/Grammar/Par.y : Grammar.cf
 	bnfc -o src -d $<

language

@@ -0,0 +1 @@
+/home/sebastian/.cabal/store/ghc-9.4.4/language-0.1.0.0-e-language-b98a5580bec9e5cee0ea5d675b3788bf6eec0b9eb955374c9ba250c1d3b935fc/bin/language

language.cabal

@@ -17,7 +17,7 @@ extra-source-files:
 
 
 common warnings
-    ghc-options: -Wall
+    ghc-options: -W
 
 executable language
     import:           warnings

src/Abs.hs

@@ -0,0 +1,20 @@
+{-# LANGUAGE TypeFamilies, StandaloneDeriving #-}
+
+module Abs where
+
+data Exp eps
+    = EInt (XInt eps) Integer
+    | EId (XId eps) String
+    | EAdd (XAdd eps) (Exp eps) (Exp eps)
+    | EApp (XApp eps) (Exp eps) (Exp eps)
+    | EAbs (XAbs eps) String (Exp eps)
+    | EExp (XExp eps)
+
+newtype Ident = Ident String
+
+type family XInt eps
+type family XId  eps
+type family XAdd eps
+type family XApp eps
+type family XAbs eps
+type family XExp eps

src/Interpreter.hs

@@ -1,14 +1,10 @@
 {-# LANGUAGE LambdaCase #-}
+
 module Interpreter where
 
-import           Control.Applicative     (Applicative)
+import           Control.Monad.Except    (Except, MonadError (throwError))
-import           Control.Monad.Except    (Except, MonadError (throwError),
+
-                                          liftEither)
-import           Data.Either.Combinators (maybeToRight)
-import           Data.Map                (Map)
-import qualified Data.Map                as Map
 import           Grammar.Abs
-import           Grammar.Print           (printTree)
 
 interpret :: Program -> Except String Integer
 interpret (Program e) =

src/NewAbs.hs

@@ -0,0 +1,29 @@
+{-# LANGUAGE GADTs, LambdaCase #-}
+
+module NewAbs where
+
+import Grammar.Abs ( Ident(..), Type )
+
+data CExp where
+    CId  :: Type -> Ident -> CExp
+    CInt :: Type -> Int -> CExp
+    CAdd :: Type -> CExp -> CExp -> CExp
+    CAbs :: Type -> Ident -> Type -> CExp -> CExp
+    CApp :: Type -> CExp -> CExp -> CExp 
+
+instance Show CExp where
+    show :: CExp -> String
+    show = \case
+        CId _ (Ident a) -> show a
+        CInt _ i -> show i
+        CAdd _ e1 e2 -> show e1 <> " + " <> show e2
+        CAbs t1 i t2 e -> appendType t1 $ show "\\" <> show i <> " : " <> show t2 <> ". " <> show e
+        CApp _ e1 e2 -> show e1 <> " " <> show e2
+
+appendType :: Type -> String -> String
+appendType t s = s <> " : " <> show t
+
+data CDef = CDef Ident Type Ident [Ident] CExp
+    deriving Show
+
+newtype CProgram = CProgram [CDef]

src/Rename/Renamer.hs

@@ -0,0 +1,96 @@
+{-# LANGUAGE OverloadedRecordDot, LambdaCase, TypeFamilies, PatternSynonyms #-}
+
+module Rename.Renamer where
+
+import Abs
+
+import qualified Grammar.Abs as A
+import           Grammar.ErrM         (Err)
+import           Control.Monad.Except (throwError)
+import           Grammar.Print        (printTree)
+import           Control.Monad.State
+import qualified Data.Map as M
+import           Data.Map (Map)
+import qualified Data.Set as S
+import           Data.Set (Set)
+
+------------------ DATA TYPES ------------------
+
+type Rn a = StateT Env Err a
+
+data Env = Env { uniques :: Map String Unique
+               , nextUnique :: Unique
+               , sig :: Set String
+               }
+
+newtype Unique = Unique Int
+    deriving Enum
+
+data Name = Nu Unique | Ni String
+
+initEnv :: Env
+initEnv = Env
+        { uniques    = mempty
+        , nextUnique = Unique 0
+        , sig        = mempty
+        }
+
+findBind :: String -> Rn Name
+findBind x = lookupUnique x >>= \case
+    Just u  -> pure $ Nu u
+    Nothing -> gets (S.member x . sig) >>= \case
+      False -> throwError ("Unbound variable " ++ printTree x)
+      True  -> pure $ Ni x
+
+newUnique :: String -> Rn Unique
+newUnique x = do
+  u <- gets nextUnique
+  modify $ \env -> env { nextUnique = succ u
+                       , uniques = M.insert x u env.uniques }
+  return u
+
+lookupUnique :: String -> Rn (Maybe Unique)
+lookupUnique x = gets (M.lookup x . uniques)
+
+renameDef :: Def -> Rn Def
+renameDef = \case
+  DExp x t _ xs e -> do
+    newSig x
+    xs' <- mapM newUnique xs
+    e'  <- renameExp e
+    let e'' = foldr ($) e' . zipWith R.EAbs xs' $ fromTree t
+    pure . R.DBind $ R.Bind x t e''
+
+renameExp :: A.Exp -> Rn ExpRE
+renameExp e =
+    case e of
+   A.EInt i -> pure (EIntR i)
+   A.EId (A.Ident str) -> flip EIdR str <$> findBind str
+   A.EAdd e1 e2 -> EAppR <$> renameExp e1 <*> renameExp e2
+   A.EApp e1 e2 -> EAppR <$> renameExp e1 <*> renameExp e2
+   A.EAbs (A.Ident x) e -> do
+       x' <- newUnique x
+       e' <- renameExp e
+       pure $ EAbsR x' x e'
+
+data R
+type ExpRE = Exp R
+
+type instance XInt R = ()
+type instance XId  R = Name
+type instance XAdd R = ()
+type instance XApp R = ()
+type instance XAbs R = Unique
+type instance XExp R = ()
+
+pattern EIntR :: Integer -> ExpRE
+pattern EIntR i = EInt () i
+
+pattern EIdR :: Name -> String -> ExpRE
+pattern EIdR n s = EId n s
+
+pattern EAppR :: ExpRE -> ExpRE -> ExpRE
+pattern EAppR e1 e2 = EApp () e1 e2
+
+pattern EAbsR :: Unique -> String -> ExpRE -> ExpRE
+pattern EAbsR u n e = EAbs u n e

src/TypeChecker.hs

@@ -0,0 +1,129 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE OverloadedRecordDot #-}
+
+module TypeChecker (typecheck) where
+
+import Grammar.Abs
+import Grammar.ErrM ( Err )
+import NewAbs
+import Data.Map (Map)
+import Data.Map qualified as Map
+import Control.Monad.Reader
+import Control.Monad.Except
+import Data.List (isPrefixOf)
+import Control.Applicative ((<|>))
+
+type Check a = ReaderT Context Err a
+
+data Context = Ctx { sig :: Map Ident Type
+                   , env :: [Map Ident Type]
+                   }
+
+initEnv :: Context
+initEnv = Ctx { sig = mempty
+              , env = mempty
+              }
+
+run :: Check a -> Either String a
+run = flip runReaderT initEnv
+
+typecheck :: Program -> Err Program
+typecheck prg = case run $ checkProg prg of
+                  Left err -> fail err
+                  Right _ -> pure prg
+
+
+checkProg :: Program -> Check CProgram
+checkProg (Program ds) = undefined
+    
+checkDef :: Def -> Check CDef
+checkDef (DExp i1 TInt i2 args e) = undefined
+checkDef (DExp i1 (TPol i) i2 args e) = undefined
+checkDef (DExp i1 (TFun xs) i2 args e) = do
+        when (i1 /= i2) (fail $ "Mismatched names: " <> show i1 <> " != " <> show i2)
+        case compare (length xs - 1) (length args) of
+          LT -> fail $ "Too many arguments, got " <> show (length args) <> " expected " <> show (length xs)
+          _ -> do
+              let vars = Map.fromList $ zip args xs
+              e' <- local (\r -> r { env =  [vars] }) (checkExp e)
+              return $ CDef i1 (TFun xs) i2 args e'
+
+checkExp :: Exp -> Check CExp
+checkExp = \case
+
+    EInt i -> pure $ CInt TInt (fromIntegral i)
+
+    EAdd e1 e2 -> do
+        e1' <- checkExp e1
+        e2' <- checkExp e2
+        let t1 = getType e1'
+        let t2 = getType e2'
+        when (t1 /= t2) (fail $ "Different types occured, got " <> show t1 <> " and " <> show t2)
+        return $ CAdd t1 e1' e2'
+
+    EId i -> do
+        asks (lookupEnv i) >>= \case
+            Right t -> return $ CId t i
+            Left _ -> asks (lookupSig i) >>= \case
+                Right t -> return $ CId t i
+                Left x -> fail x
+
+    EAbs i t e -> do
+        e' <- local (\r -> r { env = Map.singleton i t : r.env }) (checkExp e)
+        return $ CAbs (TFun [t, getType e']) i t e'
+
+    EApp e1 e2 -> do
+        e1' <- checkExp e1
+        e2' <- checkExp e2
+        let retT = applyType (getType e1') (getType e2')
+        case retT of
+          Left x -> fail x
+          Right t -> return $ CApp t e1' e2'
+
+lookupSig :: Ident -> Context -> Err Type
+lookupSig i (Ctx s _) = case Map.lookup i s of
+                  Nothing -> throwError $ "Undefined function: " <> show i
+                  Just x -> pure x
+
+lookupEnv :: Ident -> Context -> Err Type
+lookupEnv i (Ctx _ []) = throwError $ "Unbound variable: " <> show i
+lookupEnv i (Ctx s (e:es)) = case Map.lookup i e of
+                  Nothing -> lookupEnv i (Ctx s es)
+                  Just x -> pure x
+
+
+applyType :: Type -> Type -> Err Type
+applyType (TFun (x:xs)) t = case t of
+    (TFun ys) -> if ys `isPrefixOf` (x:xs)
+                         then return . TFun $ drop (length ys) (x:xs)
+                         else fail $ "Mismatched types, expected " <> show x <> " got " <> show TInt
+applyType t1 t2 = fail $ "Can not apply " <> show t1 <> " to " <> show t2
+
+class ExtractType a where
+    getType :: a -> Type
+
+instance ExtractType CExp where
+    getType = \case
+        CId t _ -> t
+        CInt t _ -> t
+        CAdd t _ _ -> t
+        CAbs t _ _ _ -> t
+        CApp t _ _ -> t
+
+-- | λx : Int. x + 3 + 5
+customLambda1 :: Exp
+customLambda1 = EAbs (Ident "x") TInt (EAdd (EId (Ident "x")) (EAdd (EInt 3) (EInt 5)))
+
+customLambda2 :: Exp
+customLambda2 = EAbs (Ident "x") (TFun [TInt, TInt]) (EId (Ident "f"))
+
+-- | main : Int 
+--   main = λx : Int. x + 3 + 5
+customPrg1 :: Program
+customPrg1 = Program [DExp (Ident "main") TInt (Ident "main") [] customLambda1]
+
+-- | main : Int -> Int
+--   main = λx : Int. x + 3 + 5
+customPrg2 :: Program
+customPrg2 = Program [DExp (Ident "main") (TFun [TInt, TInt]) (Ident "main") [] customLambda2]

test_program

@@ -0,0 +1,2 @@
+main : Int
+main = (\x : Int. x + x + 3) ((\x : Int. x) 2)