diff --git a/Grammar.cf b/Grammar.cf index 410d11d..4446eaf 100644 --- a/Grammar.cf +++ b/Grammar.cf @@ -1,4 +1,7 @@ +Program. Program ::= [Def] ; +DExp. Def ::= Ident ":" Type + Ident [Ident] "=" Exp ; Program. Program ::= [Bind]; diff --git a/Makefile b/Makefile index 6e8a54d..ad830b5 100644 --- a/Makefile +++ b/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 $< diff --git a/language b/language new file mode 120000 index 0000000..29e6f1c --- /dev/null +++ b/language @@ -0,0 +1 @@ +/home/sebastian/.cabal/store/ghc-9.4.4/language-0.1.0.0-e-language-b98a5580bec9e5cee0ea5d675b3788bf6eec0b9eb955374c9ba250c1d3b935fc/bin/language \ No newline at end of file diff --git a/language.cabal b/language.cabal index 52b2577..f95d1dd 100644 --- a/language.cabal +++ b/language.cabal @@ -17,7 +17,7 @@ extra-source-files: common warnings - ghc-options: -Wall + ghc-options: -W executable language import: warnings diff --git a/src/Abs.hs b/src/Abs.hs new file mode 100644 index 0000000..35e2904 --- /dev/null +++ b/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 diff --git a/src/Interpreter.hs b/src/Interpreter.hs index 378c95b..b7d83a5 100644 --- a/src/Interpreter.hs +++ b/src/Interpreter.hs @@ -1,14 +1,10 @@ {-# LANGUAGE LambdaCase #-} + module Interpreter where -import Control.Applicative (Applicative) -import Control.Monad.Except (Except, MonadError (throwError), - liftEither) -import Data.Either.Combinators (maybeToRight) -import Data.Map (Map) -import qualified Data.Map as Map +import Control.Monad.Except (Except, MonadError (throwError)) + import Grammar.Abs -import Grammar.Print (printTree) interpret :: Program -> Except String Integer interpret (Program e) = diff --git a/src/NewAbs.hs b/src/NewAbs.hs new file mode 100644 index 0000000..9a0296d --- /dev/null +++ b/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] diff --git a/src/Rename/Renamer.hs b/src/Rename/Renamer.hs new file mode 100644 index 0000000..a6cf12d --- /dev/null +++ b/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 diff --git a/src/TypeChecker.hs b/src/TypeChecker.hs index e69de29..8e233bb 100644 --- a/src/TypeChecker.hs +++ b/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] diff --git a/test_program b/test_program new file mode 100644 index 0000000..77bf0ad --- /dev/null +++ b/test_program @@ -0,0 +1,2 @@ +main : Int +main = (\x : Int. x + x + 3) ((\x : Int. x) 2)