From a7fb332b67b31ab9e2cc2f2b36a550bbf3259e37 Mon Sep 17 00:00:00 2001 From: Anders Date: Thu, 26 Feb 2015 14:35:29 +0100 Subject: [PATCH] Initial commit --- Eval.hs | 90 ++++++++++++++++++ Exp.cf | 56 ++++++++++++ Main.hs | 169 ++++++++++++++++++++++++++++++++++ Makefile | 13 +++ Resolver.hs | 239 ++++++++++++++++++++++++++++++++++++++++++++++++ TT.hs | 224 +++++++++++++++++++++++++++++++++++++++++++++ TypeChecker.hs | 235 +++++++++++++++++++++++++++++++++++++++++++++++ examples/nat.tt | 20 ++++ minitt.el | 64 +++++++++++++ 9 files changed, 1110 insertions(+) create mode 100644 Eval.hs create mode 100644 Exp.cf create mode 100644 Main.hs create mode 100644 Makefile create mode 100644 Resolver.hs create mode 100644 TT.hs create mode 100644 TypeChecker.hs create mode 100644 examples/nat.tt create mode 100644 minitt.el diff --git a/Eval.hs b/Eval.hs new file mode 100644 index 0000000..682d50c --- /dev/null +++ b/Eval.hs @@ -0,0 +1,90 @@ +module Eval where + +import Data.List +import Data.Maybe (fromMaybe) + +import TT + +look :: String -> Env -> Val +look x (Pair rho ((y,_),u)) | x == y = u + | otherwise = look x rho +look x r@(PDef es r1) = case lookupIdent x es of + Just t -> eval r t + Nothing -> look x r1 + +eval :: Env -> Ter -> Val +eval e v = case v of + U -> VU + App r s -> app (eval e r) (eval e s) + Var i -> look i e + Pi a b -> VPi (eval e a) (eval e b) + Lam x t -> Ter (Lam x t) e + Sigma a b -> VSigma (eval e a) (eval e b) + SPair a b -> VSPair (eval e a) (eval e b) + Fst a -> fstVal (eval e a) + Snd a -> sndVal (eval e a) + Where t decls -> eval (PDef (declDefs decls) e) t + Con name ts -> VCon name (map (eval e) ts) + Split l brcs -> Ter (Split l brcs) e + Sum pr lbls -> Ter (Sum pr lbls) e + Undef l -> error $ "eval: undefined at " ++ show l + +evals :: Env -> [(Binder,Ter)] -> [(Binder,Val)] +evals env bts = [ (b,eval env t) | (b,t) <- bts ] + +app :: Val -> Val -> Val +app (Ter (Lam x t) e) u = eval (Pair e (x,u)) t +app (Ter (Split _ nvs) e) (VCon name us) = case lookup name nvs of + Just (xs,t) -> eval (pairs e (zip xs us)) t + Nothing -> error $ "app: Split with insufficient arguments; " ++ + " missing case for " ++ name +app u@(Ter (Split _ _) _) (VN v) = VN (VSplit u v) +app (VN r) s = VN (VApp r s) + +fstVal, sndVal :: Val -> Val +fstVal (VSPair a b) = a +fstVal (VN u) = VN (VFst u) +sndVal (VSPair a b) = b +sndVal (VN u) = VN (VSnd u) + +------------------------------------------------------------------------------- +-- | Conversion + +conv :: Int -> Val -> Val -> Bool +conv k u v | u == v = True + | otherwise = case (u,v) of + (Ter (Lam x u) e,Ter (Lam x' u') e') -> + let v = mkVar k + in conv (k+1) (eval (Pair e (x,v)) u) (eval (Pair e' (x',v)) u') + (Ter (Lam x u) e,u') -> + let v = mkVar k + in conv (k+1) (eval (Pair e (x,v)) u) (app u' v) + (u',Ter (Lam x u) e) -> + let v = mkVar k + in conv (k+1) (app u' v) (eval (Pair e (x,v)) u) + (Ter (Split p _) e,Ter (Split p' _) e') -> (p == p') && convEnv k e e' + (Ter (Sum p _) e,Ter (Sum p' _) e') -> (p == p') && convEnv k e e' + (Ter (Undef p) e,Ter (Undef p') e') -> (p == p') && convEnv k e e' + (VPi u v,VPi u' v') -> + let w = mkVar k + in conv k u u' && conv (k+1) (app v w) (app v' w) + (VSigma u v,VSigma u' v') -> + let w = mkVar k + in conv k u u' && conv (k+1) (app v w) (app v' w) + (VCon c us,VCon c' us') -> (c == c') && and (zipWith (conv k) us us') + (VSPair u v,VSPair u' v') -> conv k u u' && conv k v v' + (VSPair u v,w) -> conv k u (fstVal w) && conv k v (sndVal w) + (w,VSPair u v) -> conv k (fstVal w) u && conv k (sndVal w) v + (VN u,VN v) -> convNeutral k u v + _ -> False + +convNeutral :: Int -> Neutral -> Neutral -> Bool +convNeutral k u v = case (u,v) of + (VFst u,VFst u') -> convNeutral k u u' + (VSnd u,VSnd u') -> convNeutral k u u' + (VApp u v,VApp u' v') -> convNeutral k u u' && conv k v v' + (VSplit u v,VSplit u' v') -> conv k u u' && convNeutral k v v' + (VVar x, VVar x') -> x == x' + +convEnv :: Int -> Env -> Env -> Bool +convEnv k e e' = and $ zipWith (conv k) (valOfEnv e) (valOfEnv e') diff --git a/Exp.cf b/Exp.cf new file mode 100644 index 0000000..9658ba1 --- /dev/null +++ b/Exp.cf @@ -0,0 +1,56 @@ +entrypoints Module, Exp ; + +comment "--" ; +comment "{-" "-}" ; + +layout "where", "let", "mutual", "split" ; +layout stop "in" ; +-- Do not use layout toplevel as it makes pExp fail! + +Module. Module ::= "module" AIdent "where" "{" [Imp] [Decl] "}" ; + +Import. Imp ::= "import" AIdent ; +separator Imp ";" ; + +DeclDef. Decl ::= AIdent [AIdent] "=" ExpWhere ; +DeclType. Decl ::= AIdent ":" Exp ; +DeclMutual. Decl ::= "mutual" "{" [Decl] "}" ; +DeclData. Decl ::= "data" AIdent [AIdent] "=" [Label] ; +separator Decl ";" ; + +Where. ExpWhere ::= Exp "where" "{" [Decl] "}" ; +NoWhere. ExpWhere ::= Exp ; + +Let. Exp ::= "let" "{" [Decl] "}" "in" Exp ; +Lam. Exp ::= "\\" AIdent [AIdent] "->" Exp ; +Split. Exp ::= "split" "{" [Branch] "}" ; +Fun. Exp1 ::= Exp2 "->" Exp1 ; +Pi. Exp1 ::= [PTele] "->" Exp1 ; +Sigma. Exp1 ::= [PTele] "*" Exp1 ; +App. Exp2 ::= Exp2 Exp3 ; +Var. Exp3 ::= AIdent ; +U. Exp3 ::= "U" ; +Fst. Exp3 ::= Exp3 ".1" ; +Snd. Exp3 ::= Exp3 ".2" ; +Pair. Exp3 ::= "(" Exp "," Exp ")" ; +coercions Exp 3 ; + +-- Branches +Branch. Branch ::= AIdent [AIdent] "->" ExpWhere ; +separator Branch ";" ; + +-- Labelled sum alternatives +Label. Label ::= AIdent [Tele] ; +separator Label "|" ; + +-- Telescopes +Tele. Tele ::= "(" AIdent [AIdent] ":" Exp ")" ; +terminator Tele "" ; + +-- Nonempty telescopes with Exp:s, this is hack to avoid ambiguities +-- in the grammar when parsing Pi +PTele. PTele ::= "(" Exp ":" Exp ")" ; +terminator nonempty PTele "" ; + +position token AIdent ((letter|'\''|'_')(letter|digit|'\''|'_')*) ; +terminator AIdent "" ; \ No newline at end of file diff --git a/Main.hs b/Main.hs new file mode 100644 index 0000000..6c2d413 --- /dev/null +++ b/Main.hs @@ -0,0 +1,169 @@ +module Main where + +import Control.Monad.Trans.Reader +import Control.Monad.Error +import Data.List +import System.Directory +import System.FilePath +import System.Environment +import System.Console.GetOpt +import System.Console.Haskeline + +import Exp.Lex +import Exp.Par +import Exp.Print +import Exp.Abs hiding (NoArg) +import Exp.Layout +import Exp.ErrM + +import TT +import Resolver +import qualified TypeChecker as TC +import qualified Eval as E + +type Interpreter a = InputT IO a + +-- Flag handling +data Flag = Debug | Help | Version + deriving (Eq,Show) + +options :: [OptDescr Flag] +options = [ Option "d" ["debug"] (NoArg Debug) "run in debugging mode" + , Option "" ["help"] (NoArg Help) "print help" + , Option "" ["version"] (NoArg Version) "print version number" ] + +-- Version number, welcome message, usage and prompt strings +version, welcome, usage, prompt :: String +version = "1.0" +welcome = "minitt, version: " ++ version ++ " (:h for help)\n" +usage = "Usage: minitt [options] \nOptions:" +prompt = "> " + +lexer :: String -> [Token] +lexer = resolveLayout True . myLexer + +showTree :: (Show a, Print a) => a -> IO () +showTree tree = do + putStrLn $ "\n[Abstract Syntax]\n\n" ++ show tree + putStrLn $ "\n[Linearized tree]\n\n" ++ printTree tree + +-- Used for auto completion +searchFunc :: [String] -> String -> [Completion] +searchFunc ns str = map simpleCompletion $ filter (str `isPrefixOf`) ns + +settings :: [String] -> Settings IO +settings ns = Settings + { historyFile = Nothing + , complete = completeWord Nothing " \t" $ return . searchFunc ns + , autoAddHistory = True } + +main :: IO () +main = do + args <- getArgs + case getOpt Permute options args of + (flags,files,[]) + | Help `elem` flags -> putStrLn $ usageInfo usage options + | Version `elem` flags -> putStrLn version + | otherwise -> case files of + [] -> do + putStrLn welcome + runInputT (settings []) (loop flags [] [] TC.verboseEnv) + [f] -> do + putStrLn welcome + putStrLn $ "Loading " ++ show f + initLoop flags f + _ -> putStrLn $ "Input error: zero or one file expected\n\n" ++ + usageInfo usage options + (_,_,errs) -> putStrLn $ "Input error: " ++ concat errs ++ "\n" ++ + usageInfo usage options + +-- Initialize the main loop +initLoop :: [Flag] -> FilePath -> IO () +initLoop flags f = do + -- Parse and type check files + (_,_,mods) <- imports True ([],[],[]) f + -- Translate to TT + let res = runResolver $ resolveModules mods + case res of + Left err -> do + putStrLn $ "Resolver failed: " ++ err + runInputT (settings []) (loop flags f [] TC.verboseEnv) + Right (adefs,names) -> do + (merr,tenv) <- TC.runDeclss TC.verboseEnv adefs + case merr of + Just err -> putStrLn $ "Type checking failed: " ++ err + Nothing -> return () + putStrLn "File loaded." + -- Compute names for auto completion + runInputT (settings [n | ((n,_),_) <- names]) (loop flags f names tenv) + +-- The main loop +loop :: [Flag] -> FilePath -> [(Binder,SymKind)] -> TC.TEnv -> Interpreter () +loop flags f names tenv@(TC.TEnv _ rho _ _) = do + input <- getInputLine prompt + case input of + Nothing -> outputStrLn help >> loop flags f names tenv + Just ":q" -> return () + Just ":r" -> lift $ initLoop flags f + Just (':':'l':' ':str) + | ' ' `elem` str -> do outputStrLn "Only one file allowed after :l" + loop flags f names tenv + | otherwise -> lift $ initLoop flags str + Just (':':'c':'d':' ':str) -> do lift (setCurrentDirectory str) + loop flags f names tenv + Just ":h" -> outputStrLn help >> loop flags f names tenv + Just str -> case pExp (lexer str) of + Bad err -> outputStrLn ("Parse error: " ++ err) >> loop flags f names tenv + Ok exp -> + case runResolver $ local (insertBinders names) $ resolveExp exp of + Left err -> do outputStrLn ("Resolver failed: " ++ err) + loop flags f names tenv + Right body -> do + x <- liftIO $ TC.runInfer tenv body + case x of + Left err -> do outputStrLn ("Could not type-check: " ++ err) + loop flags f names tenv + Right _ -> do + let e = E.eval rho body + outputStrLn ("EVAL: " ++ show e) + loop flags f names tenv + +-- (not ok,loaded,already loaded defs) -> to load -> +-- (new not ok, new loaded, new defs) +-- the bool determines if it should be verbose or not +imports :: Bool -> ([String],[String],[Module]) -> String -> + IO ([String],[String],[Module]) +imports v st@(notok,loaded,mods) f + | f `elem` notok = putStrLn ("Looping imports in " ++ f) >> return ([],[],[]) + | f `elem` loaded = return st + | otherwise = do + b <- doesFileExist f + let prefix = dropFileName f + if not b + then putStrLn (f ++ " does not exist") >> return ([],[],[]) + else do + s <- readFile f + let ts = lexer s + case pModule ts of + Bad s -> do + putStrLn $ "Parse failed in " ++ show f ++ "\n" ++ show s + return ([],[],[]) + Ok mod@(Module id imp decls) -> + let name = unAIdent id + imp_tt = [prefix ++ unAIdent i ++ ".tt" | Import i <- imp] + in do + when (name /= dropExtension (takeFileName f)) $ + error $ "Module name mismatch " ++ show (f,name) + (notok1,loaded1,mods1) <- + foldM (imports v) (f:notok,loaded,mods) imp_tt + when v $ putStrLn $ "Parsed " ++ show f ++ " successfully!" + return (notok,f:loaded1,mods1 ++ [mod]) + +help :: String +help = "\nAvailable commands:\n" ++ + " infer type and evaluate statement\n" ++ + " :q quit\n" ++ + " :l loads filename (and resets environment before)\n" ++ + " :cd change directory to path\n" ++ + " :r reload\n" ++ + " :h display this message\n" diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..c4afb96 --- /dev/null +++ b/Makefile @@ -0,0 +1,13 @@ +OPT=2 + +all: + ghc --make -O$(OPT) -o minitt Main.hs +bnfc: + bnfc --haskell -d Exp.cf + happy -gca Exp/Par.y + alex -g Exp/Lex.x + ghc --make -O$(OPT) Exp/Test.hs -o Exp/Test +clean: + rm -f *.log *.aux *.hi *.o minitt + cd Exp && rm -f ParExp.y LexExp.x LexhExp.hs \ + ParExp.hs PrintExp.hs AbsExp.hs *.o *.hi diff --git a/Resolver.hs b/Resolver.hs new file mode 100644 index 0000000..b0e587e --- /dev/null +++ b/Resolver.hs @@ -0,0 +1,239 @@ +{-# LANGUAGE TupleSections, ParallelListComp #-} + +-- | Convert the concrete syntax into the syntax of cubical TT. +module Resolver where + +import Exp.Abs +import qualified TT + +import Control.Applicative +import Control.Monad.Trans +import Control.Monad.Trans.Reader +import Control.Monad.Trans.Error hiding (throwError) +import Control.Monad.Error (throwError) +import Control.Monad (when) +import Data.Functor.Identity +import Data.List (nub) + +type Ter = TT.Ter + +-- | Useful auxiliary functions + +-- Applicative cons +(<:>) :: Applicative f => f a -> f [a] -> f [a] +a <:> b = (:) <$> a <*> b + +-- Un-something functions +unAIdent :: AIdent -> String +unAIdent (AIdent (_,x)) = x + +unVar :: Exp -> Maybe AIdent +unVar (Var x) = Just x +unVar _ = Nothing + +unWhere :: ExpWhere -> Exp +unWhere (Where e ds) = Let ds e +unWhere (NoWhere e) = e + +-- Tail recursive form to transform a sequence of applications +-- App (App (App u v) ...) w into (u, [v, …, w]) +-- (cleaner than the previous version of unApps) +unApps :: Exp -> [Exp] -> (Exp, [Exp]) +unApps (App u v) ws = unApps u (v : ws) +unApps u ws = (u, ws) + +-- Turns an expression of the form App (... (App id1 id2) ... idn) +-- into a list of idents +appsToIdents :: Exp -> Maybe [AIdent] +appsToIdents = mapM unVar . uncurry (:) . flip unApps [] + +-- Flatten a tele +flattenTele :: [Tele] -> [(AIdent,Exp)] +flattenTele tele = [ (i,typ) | Tele id ids typ <- tele, i <- id:ids ] + +-- Flatten a PTele +flattenPTele :: [PTele] -> Maybe [(AIdent,Exp)] +flattenPTele [] = return [] +flattenPTele (PTele exp typ : xs) = do + ids <- appsToIdents exp + pt <- flattenPTele xs + return $ map (,typ) ids ++ pt + +------------------------------------------------------------------------------- +-- | Resolver and environment + +data SymKind = Variable | Constructor + deriving (Eq,Show) + +-- local environment for constructors +data Env = Env { envModule :: String, + variables :: [(TT.Binder,SymKind)] } + deriving (Eq,Show) + +type Resolver a = ReaderT Env (ErrorT String Identity) a + +emptyEnv :: Env +emptyEnv = Env "" [] + +runResolver :: Resolver a -> Either String a +runResolver x = runIdentity $ runErrorT $ runReaderT x emptyEnv + +updateModule :: String -> Env -> Env +updateModule mod e = e{envModule = mod} + +insertBinder :: (TT.Binder,SymKind) -> Env -> Env +insertBinder (x@(n,_),var) e + | n == "_" || n == "undefined" = e + | otherwise = e{variables = (x,var) : variables e} + +insertBinders :: [(TT.Binder,SymKind)] -> Env -> Env +insertBinders = flip $ foldr insertBinder + +insertVar :: TT.Binder -> Env -> Env +insertVar x = insertBinder (x,Variable) + +insertVars :: [TT.Binder] -> Env -> Env +insertVars = flip $ foldr insertVar + +insertCon :: TT.Binder -> Env -> Env +insertCon x = insertBinder (x,Constructor) + +insertCons :: [TT.Binder] -> Env -> Env +insertCons = flip $ foldr insertCon + +getModule :: Resolver String +getModule = envModule <$> ask + +getVariables :: Resolver [(TT.Binder,SymKind)] +getVariables = variables <$> ask + +getLoc :: (Int,Int) -> Resolver TT.Loc +getLoc l = TT.Loc <$> getModule <*> pure l + +resolveAIdent :: AIdent -> Resolver TT.Binder +resolveAIdent (AIdent (l,x)) = (x,) <$> getLoc l + +resolveVar :: AIdent -> Resolver Ter +resolveVar (AIdent (l,x)) + | (x == "_") || (x == "undefined") = TT.Undef <$> getLoc l + | otherwise = do + modName <- getModule + vars <- getVariables + case TT.lookupIdent x vars of + Just Variable -> return $ TT.Var x + Just Constructor -> return $ TT.Con x [] + _ -> throwError $ "Cannot resolve variable " ++ x ++ " at position " ++ + show l ++ " in module " ++ modName + +lam :: AIdent -> Resolver Ter -> Resolver Ter +lam a e = do x <- resolveAIdent a + TT.Lam x <$> local (insertVar x) e + +lams :: [AIdent] -> Resolver Ter -> Resolver Ter +lams = flip $ foldr lam + +bind :: (Ter -> Ter -> Ter) -> (AIdent,Exp) -> Resolver Ter -> Resolver Ter +bind f (x,t) e = f <$> resolveExp t <*> lam x e + +binds :: (Ter -> Ter -> Ter) -> [(AIdent,Exp)] -> Resolver Ter -> Resolver Ter +binds f = flip $ foldr $ bind f + +resolveExp :: Exp -> Resolver Ter +resolveExp U = return TT.U +resolveExp (Var x) = resolveVar x +resolveExp (App t s) = TT.mkApps <$> resolveExp x <*> mapM resolveExp xs + where (x,xs) = unApps t [s] +resolveExp (Sigma t b) = case flattenPTele t of + Just tele -> binds TT.Sigma tele (resolveExp b) + Nothing -> throwError "Telescope malformed in Sigma" +resolveExp (Pi t b) = case flattenPTele t of + Just tele -> binds TT.Pi tele (resolveExp b) + Nothing -> throwError "Telescope malformed in Pigma" +resolveExp (Fun a b) = bind TT.Pi (AIdent ((0,0),"_"), a) (resolveExp b) +resolveExp (Lam x xs t) = lams (x:xs) (resolveExp t) +resolveExp (Fst t) = TT.Fst <$> resolveExp t +resolveExp (Snd t) = TT.Snd <$> resolveExp t +resolveExp (Pair t0 t1) = TT.SPair <$> resolveExp t0 <*> resolveExp t1 +resolveExp (Split brs) = do + brs' <- mapM resolveBranch brs + loc <- getLoc (case brs of Branch (AIdent (l,_)) _ _:_ -> l ; _ -> (0,0)) + return $ TT.Split loc brs' +resolveExp (Let decls e) = do + (rdecls,names) <- resolveDecls decls + TT.mkWheres rdecls <$> local (insertBinders names) (resolveExp e) + +resolveWhere :: ExpWhere -> Resolver Ter +resolveWhere = resolveExp . unWhere + +resolveBranch :: Branch -> Resolver (TT.Label,([TT.Binder],Ter)) +resolveBranch (Branch lbl args e) = do + binders <- mapM resolveAIdent args + re <- local (insertVars binders) $ resolveWhere e + return (unAIdent lbl, (binders, re)) + +resolveTele :: [(AIdent,Exp)] -> Resolver TT.Tele +resolveTele [] = return [] +resolveTele ((i,d):t) = do + x <- resolveAIdent i + ((x,) <$> resolveExp d) <:> local (insertVar x) (resolveTele t) + +resolveLabel :: Label -> Resolver (TT.Binder,TT.Tele) +resolveLabel (Label n vdecl) = (,) <$> resolveAIdent n <*> resolveTele (flattenTele vdecl) + +declsLabels :: [Decl] -> Resolver [TT.Binder] +declsLabels decls = mapM resolveAIdent [ lbl | Label lbl _ <- sums ] + where sums = concat [ sum | DeclData _ _ sum <- decls ] + +-- Resolve Data or Def declaration +resolveDDecl :: Decl -> Resolver (String,Ter) +resolveDDecl (DeclDef (AIdent (_,n)) args body) = + (n,) <$> lams args (resolveWhere body) +resolveDDecl (DeclData x@(AIdent (l,n)) args sum) = + (n,) <$> lams args (TT.Sum <$> resolveAIdent x <*> mapM resolveLabel sum) +resolveDDecl d = throwError $ "Definition expected " ++ show d + +-- Resolve mutual declarations (possibly one) +resolveMutuals :: [Decl] -> Resolver (TT.Decls,[(TT.Binder,SymKind)]) +resolveMutuals decls = do + binders <- mapM resolveAIdent idents + cs <- declsLabels decls + let cns = map fst cs ++ names + when (nub cns /= cns) $ + throwError $ "Duplicated constructor or ident: " ++ show cns + rddecls <- + mapM (local (insertVars binders . insertCons cs) . resolveDDecl) ddecls + when (names /= map fst rddecls) $ + throwError $ "Mismatching names in " ++ show decls + rtdecls <- resolveTele tdecls + return ([ (x,t,d) | (x,t) <- rtdecls | (_,d) <- rddecls ], + map (,Constructor) cs ++ map (,Variable) binders) + where + idents = [ x | DeclType x _ <- decls ] + names = [ unAIdent x | x <- idents ] + tdecls = [ (x,t) | DeclType x t <- decls ] + ddecls = [ t | t <- decls, not $ isTDecl t ] + isTDecl d = case d of DeclType{} -> True; _ -> False + +-- Resolve declarations +resolveDecls :: [Decl] -> Resolver ([TT.Decls],[(TT.Binder,SymKind)]) +resolveDecls [] = return ([],[]) +resolveDecls (td@DeclType{}:d:ds) = do + (rtd,names) <- resolveMutuals [td,d] + (rds,names') <- local (insertBinders names) $ resolveDecls ds + return (rtd : rds, names' ++ names) +resolveDecls (DeclMutual defs : ds) = do + (rdefs,names) <- resolveMutuals defs + (rds, names') <- local (insertBinders names) $ resolveDecls ds + return (rdefs : rds, names' ++ names) +resolveDecls (decl:_) = throwError $ "Invalid declaration: " ++ show decl + +resolveModule :: Module -> Resolver ([TT.Decls],[(TT.Binder,SymKind)]) +resolveModule (Module n imports decls) = + local (updateModule $ unAIdent n) $ resolveDecls decls + +resolveModules :: [Module] -> Resolver ([TT.Decls],[(TT.Binder,SymKind)]) +resolveModules [] = return ([],[]) +resolveModules (mod:mods) = do + (rmod, names) <- resolveModule mod + (rmods,names') <- local (insertBinders names) $ resolveModules mods + return (rmod ++ rmods, names' ++ names) diff --git a/TT.hs b/TT.hs new file mode 100644 index 0000000..4566f12 --- /dev/null +++ b/TT.hs @@ -0,0 +1,224 @@ +module TT where + +import Control.Applicative +import Data.List +import Data.Maybe +import Text.PrettyPrint as PP + +-------------------------------------------------------------------------------- +-- | Terms + +data Loc = Loc { locFile :: String + , locPos :: (Int,Int) } + deriving Eq + +type Binder = (String,Loc) +type Ident = String +type Label = String + +noLoc :: String -> Binder +noLoc x = (x, Loc "" (0,0)) + +-- Branch of the form: c x1 .. xn -> e +type Branch = (Label,([Binder],Ter)) + +-- Telescope (x1 : A1) .. (xn : An) +type Tele = [(Binder,Ter)] + +-- Labelled sum: c (x1 : A1) .. (xn : An) +type LblSum = [(Binder,Tele)] + +-- Mutual recursive definitions: (x1 : A1) .. (xn : An) and x1 = e1 .. xn = en +type Decls = [(Binder,Ter,Ter)] + +declBinders :: Decls -> [Binder] +declBinders decls = [ x | (x,_,_) <- decls ] + +declTers :: Decls -> [Ter] +declTers decls = [ d | (_,_,d) <- decls ] + +declTele :: Decls -> Tele +declTele decls = [ (x,t) | (x,t,_) <- decls ] + +declDefs :: Decls -> [(Binder,Ter)] +declDefs decls = [ (x,d) | (x,_,d) <- decls ] + +-- Terms +data Ter = App Ter Ter + | Pi Ter Ter + | Lam Binder Ter + | Where Ter Decls + | Var String + | U + -- Sigma types: + | Sigma Ter Ter + | SPair Ter Ter + | Fst Ter + | Snd Ter + -- constructor c Ms + | Con Label [Ter] + -- branches c1 xs1 -> M1,..., cn xsn -> Mn + | Split Loc [Branch] + -- labelled sum c1 A1s,..., cn Ans (assumes terms are constructors) + | Sum Binder LblSum + -- undefined + | Undef Loc + deriving Eq + +-- For an expression t, returns (u,ts) where u is no application and t = u ts +unApps :: Ter -> (Ter,[Ter]) +unApps = aux [] + where aux :: [Ter] -> Ter -> (Ter,[Ter]) + aux acc (App r s) = aux (s:acc) r + aux acc t = (t,acc) + +mkApps :: Ter -> [Ter] -> Ter +mkApps (Con l us) vs = Con l (us ++ vs) +mkApps t ts = foldl App t ts + +mkLams :: [String] -> Ter -> Ter +mkLams bs t = foldr Lam t [ noLoc b | b <- bs ] + +mkWheres :: [Decls] -> Ter -> Ter +mkWheres [] e = e +mkWheres (d:ds) e = Where (mkWheres ds e) d + +-------------------------------------------------------------------------------- +-- | Values + +data Val = VU + | Ter Ter Env + | VPi Val Val + | VId Val Val Val + | VSigma Val Val + | VSPair Val Val + | VCon String [Val] + | VN Neutral + deriving Eq + +-- neutral values +data Neutral = VVar String + | VFst Neutral + | VSnd Neutral + | VSplit Val Neutral + | VApp Neutral Val + deriving Eq + +mkVar :: Int -> Val +mkVar k = VN (VVar ('X' : show k)) + +-------------------------------------------------------------------------------- +-- | Environments + +data Env = Empty + | Pair Env (Binder,Val) + | PDef [(Binder,Ter)] Env + deriving Eq + +pairs :: Env -> [(Binder,Val)] -> Env +pairs = foldl Pair + +lookupIdent :: Ident -> [(Binder,a)] -> Maybe a +lookupIdent x defs = listToMaybe [ t | ((y,l),t) <- defs, x == y ] + +mapEnv :: (Val -> Val) -> Env -> Env +mapEnv _ Empty = Empty +mapEnv f (Pair e (x,v)) = Pair (mapEnv f e) (x,f v) +mapEnv f (PDef ts e) = PDef ts (mapEnv f e) + +valOfEnv :: Env -> [Val] +valOfEnv Empty = [] +valOfEnv (Pair env (_,v)) = v : valOfEnv env +valOfEnv (PDef _ env) = valOfEnv env + +-------------------------------------------------------------------------------- +-- | Pretty printing + +instance Show Env where + show = render . showEnv + +showEnv :: Env -> Doc +showEnv e = case e of + Empty -> PP.empty + PDef _ env -> showEnv env + Pair env (x,u) -> parens (showEnv1 env <> showVal u) + where + showEnv1 (Pair env (x,u)) = showEnv1 env <> showVal u <> text ", " + showEnv1 e = showEnv e + +instance Show Loc where + show = render . showLoc + +showLoc :: Loc -> Doc +showLoc (Loc name (i,j)) = hcat [text name,text "_L",int i,text "_C",int j] + +instance Show Ter where + show = render . showTer + +showTer :: Ter -> Doc +showTer v = case v of + U -> char 'U' + App e0 e1 -> showTer e0 <+> showTer1 e1 + Pi e0 e1 -> text "Pi" <+> showTers [e0,e1] + Lam (x,_) e -> char '\\' <> text x <+> text "->" <+> showTer e + Fst e -> showTer e <> text ".1" + Snd e -> showTer e <> text ".2" + Sigma e0 e1 -> text "Sigma" <+> showTers [e0,e1] + SPair e0 e1 -> parens (showTer1 e0 <> comma <> showTer1 e1) + Where e d -> showTer e <+> text "where" <+> showDecls d + Var x -> text x + Con c es -> text c <+> showTers es + Split l _ -> text "split" <+> showLoc l + Sum (n,l) _ -> text "sum" <+> text n + Undef _ -> text "undefined" + +showTers :: [Ter] -> Doc +showTers = hsep . map showTer1 + +showTer1 :: Ter -> Doc +showTer1 t = case t of + U -> char 'U' + Con c [] -> text c + Var x -> text x + Split{} -> showTer t + Sum{} -> showTer t + _ -> parens (showTer t) + +showDecls :: Decls -> Doc +showDecls defs = hsep $ punctuate (char ',') + [ text x <+> equals <+> showTer d | ((x,_),_,d) <- defs ] + +instance Show Val where + show = render . showVal + +showVal, showVal1 :: Val -> Doc +showVal v = case v of + VU -> char 'U' + Ter t env -> showTer t <+> showEnv env + VId a u v -> text "Id" <+> showVals [a,u,v] + VCon c us -> text c <+> showVals us + VPi a f -> text "Pi" <+> showVals [a,f] + VSPair u v -> parens (showVal1 u <> comma <> showVal1 v) + VSigma u v -> text "Sigma" <+> showVals [u,v] + VN n -> showNeutral n +showVal1 v = case v of + VU -> char 'U' + VCon c [] -> text c + _ -> parens (showVal v) + +showVals :: [Val] -> Doc +showVals = hsep . map showVal1 + +instance Show Neutral where + show = render . showNeutral + +showNeutral, showNeutral1 :: Neutral -> Doc +showNeutral n = case n of + VApp u v -> showNeutral u <+> showVal1 v + VSplit u v -> showVal u <+> showNeutral1 v + VVar x -> text x + VFst u -> showNeutral u <> text ".1" + VSnd u -> showNeutral u <> text ".2" +showNeutral1 n = case n of + VVar{} -> showNeutral n + _ -> parens (showNeutral n) diff --git a/TypeChecker.hs b/TypeChecker.hs new file mode 100644 index 0000000..2ff658e --- /dev/null +++ b/TypeChecker.hs @@ -0,0 +1,235 @@ +module TypeChecker where + +import Data.Either +import Data.Function +import Data.List +import Data.Maybe +import Data.Monoid hiding (Sum) +import Control.Monad +import Control.Monad.Trans +import Control.Monad.Trans.Error hiding (throwError) +import Control.Monad.Trans.Reader +import Control.Monad.Error (throwError) +import Control.Applicative + +import TT +import Eval + +-- Type checking monad +type Typing a = ReaderT TEnv (ErrorT String IO) a + +-- Context gives type values to identifiers +type Ctxt = [(Binder,Val)] + +-- Environment for type checker +data TEnv = TEnv { index :: Int -- for de Bruijn levels + , env :: Env + , ctxt :: Ctxt + , verbose :: Bool -- Should it be verbose and print + -- what it typechecks? + } + deriving (Eq,Show) + +verboseEnv, silentEnv :: TEnv +verboseEnv = TEnv 0 Empty [] True +silentEnv = TEnv 0 Empty [] False + +addTypeVal :: (Binder,Val) -> TEnv -> TEnv +addTypeVal p@(x,_) (TEnv k rho gam v) = + TEnv (k+1) (Pair rho (x,mkVar k)) (p:gam) v + +addType :: (Binder,Ter) -> TEnv -> Typing TEnv +addType (x,a) tenv@(TEnv _ rho _ _) = return $ addTypeVal (x,eval rho a) tenv + +addC :: Ctxt -> (Tele,Env) -> [(Binder,Val)] -> Typing Ctxt +addC gam _ [] = return gam +addC gam ((y,a):as,nu) ((x,u):xus) = + addC ((x,eval nu a):gam) (as,Pair nu (y,u)) xus + +addBranch :: [(Binder,Val)] -> (Tele,Env) -> TEnv -> Typing TEnv +addBranch nvs (tele,env) (TEnv k rho gam v) = do + e <- addC gam (tele,env) nvs + return $ TEnv (k + length nvs) (pairs rho nvs) e v + +addDecls :: Decls -> TEnv -> Typing TEnv +addDecls d (TEnv k rho gam v) = do + let rho1 = PDef [ (x,y) | (x,_,y) <- d ] rho + es' = evals rho1 (declDefs d) + gam' <- addC gam (declTele d,rho) es' + return $ TEnv k rho1 gam' v + +addTele :: Tele -> TEnv -> Typing TEnv +addTele xas lenv = foldM (flip addType) lenv xas + +trace :: String -> Typing () +trace s = do + b <- verbose <$> ask + when b $ liftIO (putStrLn s) + +runTyping :: TEnv -> Typing a -> IO (Either String a) +runTyping env t = runErrorT $ runReaderT t env + +-- Used in the interaction loop +runDecls :: TEnv -> Decls -> IO (Either String TEnv) +runDecls tenv d = runTyping tenv $ do + checkDecls d + addDecls d tenv + +runDeclss :: TEnv -> [Decls] -> IO (Maybe String,TEnv) +runDeclss tenv [] = return (Nothing, tenv) +runDeclss tenv (d:ds) = do + x <- runDecls tenv d + case x of + Right tenv' -> runDeclss tenv' ds + Left s -> return (Just s, tenv) + +runInfer :: TEnv -> Ter -> IO (Either String Val) +runInfer lenv e = runTyping lenv (infer e) + +-- Extract the type of a label as a closure +getLblType :: String -> Val -> Typing (Tele, Env) +getLblType c (Ter (Sum _ cas) r) = case lookupIdent c cas of + Just as -> return (as,r) + Nothing -> throwError ("getLblType: " ++ show c) +getLblType c u = throwError ("expected a data type for the constructor " + ++ c ++ " but got " ++ show u) + +-- Useful monadic versions of functions: +localM :: (TEnv -> Typing TEnv) -> Typing a -> Typing a +localM f r = do + e <- ask + a <- f e + local (const a) r + +getFresh :: Typing Val +getFresh = do + k <- index <$> ask + e <- asks env + return $ mkVar k + +checkDecls :: Decls -> Typing () +checkDecls d = do + let (idents, tele, ters) = (declBinders d, declTele d, declTers d) + trace ("Checking: " ++ unwords (map fst idents)) + checkTele tele + rho <- asks env + localM (addTele tele) $ checks (tele,rho) ters + +checkTele :: Tele -> Typing () +checkTele [] = return () +checkTele ((x,a):xas) = do + check VU a + localM (addType (x,a)) $ checkTele xas + +-- Check that t has type a +check :: Val -> Ter -> Typing () +check a t = case (a,t) of + (_,Con c es) -> do + (bs,nu) <- getLblType c a + checks (bs,nu) es + (VU,Pi a (Lam x b)) -> do + check VU a + localM (addType (x,a)) $ check VU b + (VU,Sigma a (Lam x b)) -> do + check VU a + localM (addType (x,a)) $ check VU b + (VU,Sum _ bs) -> sequence_ [checkTele as | (_,as) <- bs] + (VPi (Ter (Sum _ cas) nu) f,Split _ ces) -> do + let cas' = sortBy (compare `on` fst . fst) cas + ces' = sortBy (compare `on` fst) ces + if map (fst . fst) cas' == map fst ces' + then sequence_ [ checkBranch (as,nu) f brc + | (brc, (_,as)) <- zip ces' cas' ] + else throwError "case branches does not match the data type" + (VPi a f,Lam x t) -> do + var <- getFresh + local (addTypeVal (x,a)) $ check (app f var) t + (VSigma a f, SPair t1 t2) -> do + check a t1 + e <- asks env + let v = eval e t1 + check (app f v) t2 + (_,Where e d) -> do + checkDecls d + localM (addDecls d) $ check a e + (_,Undef _) -> return () + _ -> do + v <- infer t + k <- index <$> ask + unless (conv k v a) $ + throwError $ "check conv: " ++ show v ++ " /= " ++ show a + +checkBranch :: (Tele,Env) -> Val -> Branch -> Typing () +checkBranch (xas,nu) f (c,(xs,e)) = do + k <- asks index + env <- asks env + let l = length xas + us = map mkVar [k..k+l-1] + localM (addBranch (zip xs us) (xas,nu)) $ check (app f (VCon c us)) e + +-- infer the type of e +infer :: Ter -> Typing Val +infer e = case e of + U -> return VU -- U : U + Var n -> do + gam <- ctxt <$> ask + case lookupIdent n gam of + Just v -> return v + Nothing -> throwError $ show n ++ " is not declared!" + App t u -> do + c <- infer t + case c of + VPi a f -> do + check a u + rho <- asks env + let v = eval rho u + return $ app f v + _ -> throwError $ show c ++ " is not a product" + Fst t -> do + c <- infer t + case c of + VSigma a f -> return a + _ -> throwError $ show c ++ " is not a sigma-type" + Snd t -> do + c <- infer t + case c of + VSigma a f -> do + e <- asks env + let v = eval e t + return $ app f (fstVal v) + _ -> throwError $ show c ++ " is not a sigma-type" + Where t d -> do + checkDecls d + localM (addDecls d) $ infer t + _ -> throwError ("infer " ++ show e) + +checks :: (Tele,Env) -> [Ter] -> Typing () +checks _ [] = return () +checks ((x,a):xas,nu) (e:es) = do + let v = eval nu a + check v e + rho <- asks env + let v' = eval rho e + checks (xas,Pair nu (x,v')) es +checks _ _ = throwError "checks" + +-- Not used since we have U : U +-- +-- (=?=) :: Typing Ter -> Ter -> Typing () +-- m =?= s2 = do +-- s1 <- m +-- unless (s1 == s2) $ throwError (show s1 ++ " =/= " ++ show s2) +-- +-- checkTs :: [(String,Ter)] -> Typing () +-- checkTs [] = return () +-- checkTs ((x,a):xas) = do +-- checkType a +-- local (addType (x,a)) (checkTs xas) +-- +-- checkType :: Ter -> Typing () +-- checkType t = case t of +-- U -> return () +-- Pi a (Lam x b) -> do +-- checkType a +-- local (addType (x,a)) (checkType b) +-- _ -> infer t =?= U diff --git a/examples/nat.tt b/examples/nat.tt new file mode 100644 index 0000000..2130d7f --- /dev/null +++ b/examples/nat.tt @@ -0,0 +1,20 @@ +module nat where + +nat : U +data nat = zero | suc (n : nat) + +one : nat +one = suc zero + +two : nat +two = suc one + +pred : nat -> nat +pred = split + zero -> zero + suc n -> n + +add : nat -> nat -> nat +add m = split + zero -> m + suc n -> suc (add m n) \ No newline at end of file diff --git a/minitt.el b/minitt.el new file mode 100644 index 0000000..42dee62 --- /dev/null +++ b/minitt.el @@ -0,0 +1,64 @@ +;; define several class of keywords +(setq minitt-keywords '("data" "import" "mutual" "let" "in" "split" + "module" "where" "U") ) +(setq minitt-special '("undefined" "primitive")) + +;; create regex strings +(setq minitt-keywords-regexp (regexp-opt minitt-keywords 'words)) +(setq minitt-operators-regexp (regexp-opt '(":" "->" "=" "\\" "|" "\\" "*" "_") t)) +(setq minitt-special-regexp (regexp-opt minitt-special 'words)) +(setq minitt-def-regexp "^[[:word:]]+") + +;; clear memory +(setq minitt-keywords nil) +(setq minitt-special nil) + +;; create the list for font-lock. +;; each class of keyword is given a particular face +(setq minitt-font-lock-keywords + `( + (,minitt-keywords-regexp . font-lock-type-face) + (,minitt-operators-regexp . font-lock-variable-name-face) + (,minitt-special-regexp . font-lock-warning-face) + (,minitt-def-regexp . font-lock-function-name-face) +)) + +;; command to comment/uncomment text +(defun minitt-comment-dwim (arg) + "Comment or uncomment current line or region in a smart way. For detail, see `comment-dwim'." + (interactive "*P") + (require 'newcomment) + (let ((comment-start "--") (comment-end "")) + (comment-dwim arg))) + + +;; syntax table for comments, same as for haskell-mode +(defvar minitt-syntax-table + (let ((st (make-syntax-table))) + (modify-syntax-entry ?\{ "(}1nb" st) + (modify-syntax-entry ?\} "){4nb" st) + (modify-syntax-entry ?- "_ 123" st) + (modify-syntax-entry ?\n ">" st) + st)) + +;; define the mode +(define-derived-mode minitt-mode fundamental-mode + "minitt mode" + "Major mode for editing minitt files…" + + :syntax-table minitt-syntax-table + + ;; code for syntax highlighting + (setq font-lock-defaults '(minitt-font-lock-keywords)) + (setq mode-name "minitt") + + ;; modify the keymap + (define-key minitt-mode-map [remap comment-dwim] 'minitt-comment-dwim) + + ;; clear memory + (setq minitt-keywords-regexp nil) + (setq minitt-operators-regexp nil) + (setq minitt-special-regexp nil) +) + +(provide 'minitt-mode) -- 2.34.1