From bdc72de514f63440a634d011faedfbeef770ed1f Mon Sep 17 00:00:00 2001 From: Marcin Chrzanowski Date: Sun, 13 May 2018 19:51:07 +0200 Subject: Initial commit --- .gitignore | 4 ++ Abs.hs | 27 ++++++++ Eval.hs | 144 ++++++++++++++++++++++++++++++++++++++++++ Makefile | 15 +++++ README.md | 0 Schmim.hs | 59 +++++++++++++++++ Typecheck.hs | 202 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ schmim.bnfc | 51 +++++++++++++++ 8 files changed, 502 insertions(+) create mode 100644 .gitignore create mode 100644 Abs.hs create mode 100644 Eval.hs create mode 100644 Makefile create mode 100644 README.md create mode 100644 Schmim.hs create mode 100644 Typecheck.hs create mode 100644 schmim.bnfc diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..a6c8d5c --- /dev/null +++ b/.gitignore @@ -0,0 +1,4 @@ +*.o +*.hi +interpreter +Parser/* diff --git a/Abs.hs b/Abs.hs new file mode 100644 index 0000000..cfdd854 --- /dev/null +++ b/Abs.hs @@ -0,0 +1,27 @@ +module Abs where + +import Parser.AbsSchmim +import Data.Map.Lazy + +type Env = Map Ident Val + +data Val + = VNum Integer + | VAbs Ident Type Env Exp + | VTr + | VFl + | VVrnt Ident Val Type + | VTpl [Val] + | VNil Type + | VCons Val Val + deriving (Eq, Ord, Read) + +instance Show Val where + show (VNum n) = show n + show (VAbs x t _ _) = "#(lambda " ++ (show x) ++ " : " ++ (show t) ++ ")" + show (VTr) = "true" + show (VFl) = "false" + show (VVrnt l v _) = "<" ++ (show l) ++ " " ++ (show v) ++ ">" + show (VTpl vs) = "{" ++ (show vs) ++ "}" + show (VNil t) = "nil" + show (VCons v1 v2) = "(cons " ++ (show v1) ++ " " ++ (show v2) ++ ")" diff --git a/Eval.hs b/Eval.hs new file mode 100644 index 0000000..c4f6cf7 --- /dev/null +++ b/Eval.hs @@ -0,0 +1,144 @@ +module Eval where + +import Abs +import Prelude hiding (lookup) +import Parser.AbsSchmim +import Control.Monad.Reader +import Data.Map.Lazy +import Typecheck + +type Interpreter a = ReaderT Env (Either String) a + +eval :: Exp -> Interpreter Val +eval (EAdd e1 e2) = do + (VNum v1) <- eval e1 + (VNum v2) <- eval e2 + return (VNum $ v1 + v2) +eval (EMul e1 e2) = do + (VNum v1) <- eval e1 + (VNum v2) <- eval e2 + return (VNum $ v1 * v2) +eval (ESub e1 e2) = do + (VNum v1) <- eval e1 + (VNum v2) <- eval e2 + return (VNum $ v1 - v2) +eval (EDiv e1 e2) = do + (VNum v1) <- eval e1 + (VNum v2) <- eval e2 + if v2 == 0 + then lift $ Left "division by 0" + else return (VNum $ v1 `div` v2) +eval (EVar x) = do + (Just v) <- asks $ lookup x + return v +eval (ENum n) = return (VNum n) +eval (EAbs x t e) = do + env <- ask + return $ VAbs x t env e +eval (EApp e1 []) = do + eval e1 +eval (EApp e1 [e2]) = do + (VAbs x t env e) <- eval e1 + v <- eval e2 + local (\_ -> insert x v env) $ eval e +eval (EApp e1 (e2:es)) = do + eval (EApp (EApp e1 [e2]) es) +eval ETr = return VTr +eval EFl = return VFl +eval (EEq e1 e2) = do + (VNum v1) <- eval e1 + (VNum v2) <- eval e2 + return $ if v1 == v2 then VTr else VFl +eval (ELeq e1 e2) = do + (VNum v1) <- eval e1 + (VNum v2) <- eval e2 + return $ if v1 <= v2 then VTr else VFl +eval (EGeq e1 e2) = do + (VNum v1) <- eval e1 + (VNum v2) <- eval e2 + return $ if v1 >= v2 then VTr else VFl +eval (ELess e1 e2) = do + (VNum v1) <- eval e1 + (VNum v2) <- eval e2 + return $ if v1 < v2 then VTr else VFl +eval (EGrt e1 e2) = do + (VNum v1) <- eval e1 + (VNum v2) <- eval e2 + return $ if v1 > v2 then VTr else VFl +eval (EAnd e1 e2) = do + v1 <- eval e1 + v2 <- eval e2 + return $ case (v1, v2) of + (VTr, VTr) -> VTr + _ -> VFl +eval (EOr e1 e2) = do + v1 <- eval e1 + v2 <- eval e2 + return $ case (v1, v2) of + (VFl, VFl) -> VFl + _ -> VTr +eval (EIfte e1 e2 e3) = do + v1 <- eval e1 + let e = case v1 of + VTr -> e2 + VFl -> e3 + eval e +eval (EVrnt l e t) = do + v <- eval e + return $ VVrnt l v t +eval (ETpl es) = do + vs <- forM es eval + return $ VTpl vs +eval (EProj e i) = do + (VTpl vs) <- eval e + return $ vs !! (fromIntegral (i - 1)) +eval (EMtch e ms) = do + (VVrnt l v t) <- eval e + let (Matching _ x e') = lookupLabel l ms + local (insert x v) $ eval e' + where + lookupLabel l (m@(Matching l' x e):ms) + | l == l' = m + | otherwise = lookupLabel l ms +eval (ENil t) = return $ VNil t +eval (ECons e1 e2) = do + v1 <- eval e1 + v2 <- eval e2 + return (VCons v1 v2) +eval (EHead e) = do + v <- eval e + case v of + (VNil _) -> lift $ Left "head of empty list" + (VCons v _) -> return v +eval (ETail e) = do + v <- eval e + case v of + (VNil _) -> lift $ Left "tail of empty list" + (VCons _ v) -> return v +eval (EIsnil e) = do + v <- eval e + return $ case v of + (VNil _) -> VTr + _ -> VFl +eval (EFix (EAbs x t e)) = do + env <- ask + let env' = insert x (forcedEval (EFix (EAbs x t e)) env') env + local (\_ -> env') $ eval e + where + forcedEval e env = case runReaderT (eval e) env of + Right v -> v +eval (ELet x ps e1 e2) = do + eval (EApp (EAbs x t e2) [e1']) + where + (e1', t) = Prelude.foldr (\(Param x t') (e, t) -> ((EAbs x t' e), TFun t' t)) (e1, placeholderType) ps +eval (ELetrec x _ ps e1 e2) = do + eval (EApp (EAbs x t e2) [(EFix (EAbs x t e1'))]) + where + (e1', t) = Prelude.foldr (\(Param x t') (e, t) -> ((EAbs x t' e), TFun t' t)) (e1, placeholderType) ps + +placeholderType = TInt + +interp :: Exp -> Either String Val +interp e = case runReaderT (typeof e) empty of + (Just t) -> runReaderT (eval e) empty + Nothing -> Left "badly typed expression" diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..b32ae73 --- /dev/null +++ b/Makefile @@ -0,0 +1,15 @@ +all: bnfc parser interpreter + # ghc -dynamic --make Parser/TestSchmim.hs -o Parser/TestSchmim + +bnfc: + bnfc -haskell -p Parser schmim.bnfc + +parser: bnfc + happy -gca Parser/ParSchmim.y + alex -g Parser/LexSchmim.x + +interpreter: parser bnfc + ghc -dynamic Schmim.hs -o interpreter + +clean: + -rm -f Parser/*.log Parser/*.aux Parser/*.hi Parser/*.o Parser/*.dvi *.o *.hi interpreter diff --git a/README.md b/README.md new file mode 100644 index 0000000..e69de29 diff --git a/Schmim.hs b/Schmim.hs new file mode 100644 index 0000000..3c0bc79 --- /dev/null +++ b/Schmim.hs @@ -0,0 +1,59 @@ +module Main where + +import System.IO ( stdin, hGetContents ) +import System.Environment ( getArgs, getProgName ) +import System.Exit ( exitFailure, exitSuccess ) + +import Parser.LexSchmim +import Parser.ParSchmim +import Parser.SkelSchmim +import Parser.PrintSchmim +import Parser.AbsSchmim + +import Eval + +import Parser.ErrM + +type ParseFun a = [Token] -> Err a + +myLLexer = myLexer + +type Verbosity = Int + +putStrV :: Verbosity -> String -> IO () +putStrV v s = if v > 1 then putStrLn s else return () + +runFile :: Verbosity -> ParseFun Exp -> FilePath -> IO () +runFile v p f = readFile f >>= run v p + +run :: Verbosity -> ParseFun Exp -> String -> IO () +run v p s = let ts = myLLexer s in case p ts of + Bad s -> do putStrLn "\nParse Failed...\n" + exitFailure + Ok tree -> do let res = interp tree + case res of + (Left err) -> do putStrLn $ "Error: " ++ err + exitFailure + (Right v) -> print v + + exitSuccess + +usage :: IO () +usage = do + putStrLn $ unlines + [ "usage: Call with one of the following argument combinations:" + , " --help Display this help message." + , " (no arguments) Parse stdin verbosely." + , " (files) Parse content of files verbosely." + , " -s (files) Silent mode. Parse content of files silently." + ] + exitFailure + +main :: IO () +main = do + args <- getArgs + case args of + ["--help"] -> usage + [] -> hGetContents stdin >>= run 2 pExp + "-s":fs -> mapM_ (runFile 0 pExp) fs + fs -> mapM_ (runFile 2 pExp) fs diff --git a/Typecheck.hs b/Typecheck.hs new file mode 100644 index 0000000..6c62909 --- /dev/null +++ b/Typecheck.hs @@ -0,0 +1,202 @@ +module Typecheck where + +import Prelude hiding (lookup) +import Parser.AbsSchmim +import Data.Map.Lazy +import Control.Monad.Reader + +type Context = Map Ident Type +type Typechecker a = ReaderT Context Maybe a + +assert :: MonadPlus m => Bool -> m () +assert True = return () +assert False = mzero + +typeof :: Exp -> Typechecker Type +typeof ETr = return TBool +typeof EFl = return TBool +typeof (ENum _) = return TInt +typeof (EVar x) = do + mt <- asks $ lookup x + case mt of + (Just t) -> return t + Nothing -> lift Nothing +typeof (EAdd e1 e2) = do + t1 <- typeof e1 + t2 <- typeof e2 + assert (t1 == TInt) + assert (t2 == TInt) + return TInt +typeof (ESub e1 e2) = do + t1 <- typeof e1 + t2 <- typeof e2 + assert (t1 == TInt) + assert (t2 == TInt) + return TInt +typeof (EMul e1 e2) = do + t1 <- typeof e1 + t2 <- typeof e2 + assert (t1 == TInt) + assert (t2 == TInt) + return TInt +typeof (EDiv e1 e2) = do + t1 <- typeof e1 + t2 <- typeof e2 + assert (t1 == TInt) + assert (t2 == TInt) + return TInt +typeof (EAnd e1 e2) = do + t1 <- typeof e1 + t2 <- typeof e2 + assert (t1 == TBool) + assert (t2 == TBool) + return TBool +typeof (EOr e1 e2) = do + t1 <- typeof e1 + t2 <- typeof e2 + assert (t1 == TBool) + assert (t2 == TBool) + return TBool +typeof (ENot e) = do + t <- typeof e + assert (t == TBool) + return TBool +typeof (EEq e1 e2) = do + t1 <- typeof e1 + t2 <- typeof e2 + assert (t1 == TInt) + assert (t2 == TInt) + return TBool +typeof (ELeq e1 e2) = do + t1 <- typeof e1 + t2 <- typeof e2 + assert (t1 == TInt) + assert (t2 == TInt) + return TBool +typeof (EGeq e1 e2) = do + t1 <- typeof e1 + t2 <- typeof e2 + assert (t1 == TInt) + assert (t2 == TInt) + return TBool +typeof (ELess e1 e2) = do + t1 <- typeof e1 + t2 <- typeof e2 + assert (t1 == TInt) + assert (t2 == TInt) + return TBool +typeof (EGrt e1 e2) = do + t1 <- typeof e1 + t2 <- typeof e2 + assert (t1 == TInt) + assert (t2 == TInt) + return TBool +typeof (EIfte e1 e2 e3) = do + t1 <- typeof e1 + t2 <- typeof e2 + t3 <- typeof e3 + assert (t1 == TBool) + assert (t2 == t3) + return t2 +typeof (EAbs x t e) = do + t' <- local (insert x t) $ typeof e + return $ TFun t t' +typeof (EApp e []) = typeof e +typeof (EApp e1 [e2]) = do + t1 <- typeof e1 + t2 <- typeof e2 + case t1 of + (TFun t t') + | t == t2 -> return t' + _ -> lift Nothing +typeof (EApp e1 es) = do + t1 <- typeof e1 + ts <- forM es typeof + applyTypes t1 ts + where + applyTypes t [] = return t + applyTypes (TFun t t') (t1:ts) = do + assert $ t == t1 + applyTypes t' ts +typeof (EVrnt l e t@(TVrnt ls)) = do + t1 <- typeof e + (Labeled l' t2) <- lift $ lookupLabel l ls + assert $ t1 == t2 + return t + where + lookupLabel l [] = Nothing + lookupLabel l (lbl@(Labeled l1 t):ls) + | l == l1 = Just lbl + | otherwise = lookupLabel l ls +typeof (EVrnt l e _) = lift Nothing +typeof (ETpl es) = do + ts <- forM es typeof + return $ TTpl ts +typeof (EProj e n) = do + t <- typeof e + case t of + (TTpl ts) + | length ts >= fromIntegral n -> return $ ts !! (fromIntegral (n - 1)) + _ -> lift Nothing +typeof (EMtch e ms) = do + t <- typeof e + case t of + (TVrnt ls) -> do + assert $ (length ms == length ls) + ts <- forM (zip ms ls) getMatchingType + assert $ allSame ts + return $ head ts + _ -> lift Nothing + where + getMatchingType (Matching l1 x e, Labeled l2 t) = do + assert $ l1 == l2 + local (insert x t) $ typeof e + allSame [] = True + allSame [_] = True + allSame (x:y:zs) + | x == y = allSame (y:zs) + | otherwise = False +typeof (ENil t) = do + case t of + (TList _) -> return t + _ -> lift Nothing +typeof (ECons e1 e2) = do + t1 <- typeof e1 + t2 <- typeof e2 + case t2 of + (TList t) -> do + assert $ t == t1 + return t2 + _ -> lift Nothing +typeof (EHead e) = do + t <- typeof e + case t of + (TList t') -> return t' + _ -> lift Nothing +typeof (ETail e) = do + t <- typeof e + case t of + (TList _) -> return t + _ -> lift Nothing +typeof (EIsnil e) = do + t <- typeof e + case t of + (TList _) -> return TBool + _ -> lift Nothing +typeof (ELet f ps e1 e2) = do + t1 <- local (insertAll ps) $ typeof e1 + local (insert f (prependParamTypes t1 ps)) $ typeof e2 + where + insertAll [] env = env + insertAll ((Param x t):ps) env = insertAll ps $ insert x t env + prependParamTypes t ps = Prelude.foldr (\(Param _ t2) t1 -> TFun t2 t1) t ps +typeof (EFix f) = do + t <- typeof f + case t of + (TFun t1 t2) + | t1 == t2 -> return t1 + _ -> lift Nothing +typeof (ELetrec f t ps e1 e2) = do + typeof (EApp (EAbs f t e2) [(EFix (EAbs f t e1'))]) + where + e1' = Prelude.foldr (\(Param x t') e -> (EAbs x t' e)) e1 ps diff --git a/schmim.bnfc b/schmim.bnfc new file mode 100644 index 0000000..6fe294a --- /dev/null +++ b/schmim.bnfc @@ -0,0 +1,51 @@ +ENum. Exp ::= Integer; +EVar. Exp ::= Ident; +EAbs. Exp ::= "(" "lambda" Ident ":" Type Exp ")"; +EApp. Exp ::= "("Exp [Exp]")"; +ETr. Exp ::= "true"; +EFl. Exp ::= "false"; +EAdd. Exp ::= "(" "+" Exp Exp")"; +ESub. Exp ::= "(" "-" Exp Exp")"; +EMul. Exp ::= "(" "*" Exp Exp")"; +EDiv. Exp ::= "(" "/" Exp Exp")"; +EEq. Exp ::= "(" "=" Exp Exp")"; +ELeq. Exp ::= "(" "<=" Exp Exp")"; +EGeq. Exp ::= "(" ">=" Exp Exp")"; +ELess. Exp ::= "(" "<" Exp Exp")"; +EGrt. Exp ::= "(" ">" Exp Exp")"; +EAnd. Exp ::= "(" "and" Exp Exp")"; +EOr. Exp ::= "(" "or" Exp Exp")"; +ENot. Exp ::= "(" "not" Exp")"; +EIfte. Exp ::= "(" "if" Exp Exp Exp")"; +ELet. Exp ::= "(" "let" "("Ident [Param]")" Exp Exp")"; +ELetrec. Exp ::= "(" "letrec" "("Ident ":" Type [Param]")" Exp Exp")"; +EVrnt. Exp ::= "<" Ident Exp ">" ":" Type; +EMtch. Exp ::= "(" "match" Exp [Matching]")"; +ETpl. Exp ::= "{" [Exp] "}"; +EProj. Exp ::= Exp "." Integer; +ENil. Exp ::= "nil" ":" Type; +EIsnil. Exp ::= "(" "isnil" Exp")"; +ECons. Exp ::= "(" "cons" Exp Exp")"; +EHead. Exp ::= "(" "head" Exp")"; +ETail. Exp ::= "(" "tail" Exp")"; +EFix. Exp ::= "(" "fix" Exp")"; +separator Exp ""; + +Param. Param ::= Ident ":" Type; +separator Param ""; +Matching. Matching ::= "(<" Ident Ident ">" Exp ")"; +separator Matching ""; + +_. Type ::= "(" Type ")"; +TBool. Type ::= "Bool"; +TInt. Type ::= "Int"; +TFun. Type ::= Type "->" Type; +TVrnt. Type ::= "<" [Labeled] ">"; +TTpl. Type ::= "{" [Type] "}"; +TList. Type ::= "[" Type "]"; +separator Type ""; + +Labeled. Labeled ::= Ident ":" Type; +separator Labeled ""; + +comment ";"; -- cgit v1.2.3