From: Anders Date: Thu, 26 Feb 2015 13:35:29 +0000 (+0100) Subject: Initial commit X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=a7fb332b67b31ab9e2cc2f2b36a550bbf3259e37;p=cubicaltt.git Initial commit --- 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)