--- /dev/null
+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')
--- /dev/null
+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
--- /dev/null
+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] <file.tt>\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" ++
+ " <statement> infer type and evaluate statement\n" ++
+ " :q quit\n" ++
+ " :l <filename> loads filename (and resets environment before)\n" ++
+ " :cd <path> change directory to path\n" ++
+ " :r reload\n" ++
+ " :h display this message\n"
--- /dev/null
+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
--- /dev/null
+{-# 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)
--- /dev/null
+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)
--- /dev/null
+module TypeChecker where\r
+\r
+import Data.Either\r
+import Data.Function\r
+import Data.List\r
+import Data.Maybe\r
+import Data.Monoid hiding (Sum)\r
+import Control.Monad\r
+import Control.Monad.Trans\r
+import Control.Monad.Trans.Error hiding (throwError)\r
+import Control.Monad.Trans.Reader\r
+import Control.Monad.Error (throwError)\r
+import Control.Applicative\r
+\r
+import TT\r
+import Eval\r
+\r
+-- Type checking monad\r
+type Typing a = ReaderT TEnv (ErrorT String IO) a\r
+\r
+-- Context gives type values to identifiers\r
+type Ctxt = [(Binder,Val)]\r
+\r
+-- Environment for type checker\r
+data TEnv = TEnv { index :: Int -- for de Bruijn levels\r
+ , env :: Env\r
+ , ctxt :: Ctxt\r
+ , verbose :: Bool -- Should it be verbose and print\r
+ -- what it typechecks?\r
+ }\r
+ deriving (Eq,Show)\r
+\r
+verboseEnv, silentEnv :: TEnv\r
+verboseEnv = TEnv 0 Empty [] True\r
+silentEnv = TEnv 0 Empty [] False\r
+\r
+addTypeVal :: (Binder,Val) -> TEnv -> TEnv\r
+addTypeVal p@(x,_) (TEnv k rho gam v) =\r
+ TEnv (k+1) (Pair rho (x,mkVar k)) (p:gam) v\r
+\r
+addType :: (Binder,Ter) -> TEnv -> Typing TEnv\r
+addType (x,a) tenv@(TEnv _ rho _ _) = return $ addTypeVal (x,eval rho a) tenv\r
+\r
+addC :: Ctxt -> (Tele,Env) -> [(Binder,Val)] -> Typing Ctxt\r
+addC gam _ [] = return gam\r
+addC gam ((y,a):as,nu) ((x,u):xus) = \r
+ addC ((x,eval nu a):gam) (as,Pair nu (y,u)) xus\r
+\r
+addBranch :: [(Binder,Val)] -> (Tele,Env) -> TEnv -> Typing TEnv\r
+addBranch nvs (tele,env) (TEnv k rho gam v) = do\r
+ e <- addC gam (tele,env) nvs\r
+ return $ TEnv (k + length nvs) (pairs rho nvs) e v\r
+\r
+addDecls :: Decls -> TEnv -> Typing TEnv\r
+addDecls d (TEnv k rho gam v) = do\r
+ let rho1 = PDef [ (x,y) | (x,_,y) <- d ] rho\r
+ es' = evals rho1 (declDefs d)\r
+ gam' <- addC gam (declTele d,rho) es'\r
+ return $ TEnv k rho1 gam' v\r
+\r
+addTele :: Tele -> TEnv -> Typing TEnv\r
+addTele xas lenv = foldM (flip addType) lenv xas\r
+\r
+trace :: String -> Typing ()\r
+trace s = do\r
+ b <- verbose <$> ask\r
+ when b $ liftIO (putStrLn s)\r
+\r
+runTyping :: TEnv -> Typing a -> IO (Either String a)\r
+runTyping env t = runErrorT $ runReaderT t env\r
+\r
+-- Used in the interaction loop\r
+runDecls :: TEnv -> Decls -> IO (Either String TEnv)\r
+runDecls tenv d = runTyping tenv $ do\r
+ checkDecls d\r
+ addDecls d tenv\r
+\r
+runDeclss :: TEnv -> [Decls] -> IO (Maybe String,TEnv)\r
+runDeclss tenv [] = return (Nothing, tenv)\r
+runDeclss tenv (d:ds) = do\r
+ x <- runDecls tenv d\r
+ case x of\r
+ Right tenv' -> runDeclss tenv' ds\r
+ Left s -> return (Just s, tenv)\r
+\r
+runInfer :: TEnv -> Ter -> IO (Either String Val)\r
+runInfer lenv e = runTyping lenv (infer e)\r
+\r
+-- Extract the type of a label as a closure\r
+getLblType :: String -> Val -> Typing (Tele, Env)\r
+getLblType c (Ter (Sum _ cas) r) = case lookupIdent c cas of\r
+ Just as -> return (as,r)\r
+ Nothing -> throwError ("getLblType: " ++ show c)\r
+getLblType c u = throwError ("expected a data type for the constructor "\r
+ ++ c ++ " but got " ++ show u)\r
+\r
+-- Useful monadic versions of functions:\r
+localM :: (TEnv -> Typing TEnv) -> Typing a -> Typing a\r
+localM f r = do\r
+ e <- ask\r
+ a <- f e\r
+ local (const a) r\r
+\r
+getFresh :: Typing Val\r
+getFresh = do\r
+ k <- index <$> ask\r
+ e <- asks env\r
+ return $ mkVar k\r
+\r
+checkDecls :: Decls -> Typing ()\r
+checkDecls d = do\r
+ let (idents, tele, ters) = (declBinders d, declTele d, declTers d)\r
+ trace ("Checking: " ++ unwords (map fst idents))\r
+ checkTele tele\r
+ rho <- asks env\r
+ localM (addTele tele) $ checks (tele,rho) ters\r
+\r
+checkTele :: Tele -> Typing ()\r
+checkTele [] = return ()\r
+checkTele ((x,a):xas) = do\r
+ check VU a\r
+ localM (addType (x,a)) $ checkTele xas\r
+\r
+-- Check that t has type a\r
+check :: Val -> Ter -> Typing ()\r
+check a t = case (a,t) of\r
+ (_,Con c es) -> do\r
+ (bs,nu) <- getLblType c a\r
+ checks (bs,nu) es\r
+ (VU,Pi a (Lam x b)) -> do\r
+ check VU a\r
+ localM (addType (x,a)) $ check VU b\r
+ (VU,Sigma a (Lam x b)) -> do\r
+ check VU a\r
+ localM (addType (x,a)) $ check VU b\r
+ (VU,Sum _ bs) -> sequence_ [checkTele as | (_,as) <- bs]\r
+ (VPi (Ter (Sum _ cas) nu) f,Split _ ces) -> do\r
+ let cas' = sortBy (compare `on` fst . fst) cas\r
+ ces' = sortBy (compare `on` fst) ces\r
+ if map (fst . fst) cas' == map fst ces'\r
+ then sequence_ [ checkBranch (as,nu) f brc\r
+ | (brc, (_,as)) <- zip ces' cas' ]\r
+ else throwError "case branches does not match the data type"\r
+ (VPi a f,Lam x t) -> do\r
+ var <- getFresh\r
+ local (addTypeVal (x,a)) $ check (app f var) t\r
+ (VSigma a f, SPair t1 t2) -> do\r
+ check a t1\r
+ e <- asks env\r
+ let v = eval e t1\r
+ check (app f v) t2\r
+ (_,Where e d) -> do\r
+ checkDecls d\r
+ localM (addDecls d) $ check a e\r
+ (_,Undef _) -> return ()\r
+ _ -> do\r
+ v <- infer t\r
+ k <- index <$> ask\r
+ unless (conv k v a) $\r
+ throwError $ "check conv: " ++ show v ++ " /= " ++ show a\r
+\r
+checkBranch :: (Tele,Env) -> Val -> Branch -> Typing ()\r
+checkBranch (xas,nu) f (c,(xs,e)) = do\r
+ k <- asks index\r
+ env <- asks env\r
+ let l = length xas\r
+ us = map mkVar [k..k+l-1]\r
+ localM (addBranch (zip xs us) (xas,nu)) $ check (app f (VCon c us)) e\r
+\r
+-- infer the type of e\r
+infer :: Ter -> Typing Val\r
+infer e = case e of\r
+ U -> return VU -- U : U\r
+ Var n -> do\r
+ gam <- ctxt <$> ask\r
+ case lookupIdent n gam of\r
+ Just v -> return v\r
+ Nothing -> throwError $ show n ++ " is not declared!"\r
+ App t u -> do\r
+ c <- infer t\r
+ case c of\r
+ VPi a f -> do\r
+ check a u\r
+ rho <- asks env\r
+ let v = eval rho u\r
+ return $ app f v\r
+ _ -> throwError $ show c ++ " is not a product"\r
+ Fst t -> do\r
+ c <- infer t\r
+ case c of\r
+ VSigma a f -> return a\r
+ _ -> throwError $ show c ++ " is not a sigma-type"\r
+ Snd t -> do\r
+ c <- infer t\r
+ case c of\r
+ VSigma a f -> do\r
+ e <- asks env\r
+ let v = eval e t\r
+ return $ app f (fstVal v)\r
+ _ -> throwError $ show c ++ " is not a sigma-type"\r
+ Where t d -> do\r
+ checkDecls d\r
+ localM (addDecls d) $ infer t\r
+ _ -> throwError ("infer " ++ show e)\r
+\r
+checks :: (Tele,Env) -> [Ter] -> Typing ()\r
+checks _ [] = return ()\r
+checks ((x,a):xas,nu) (e:es) = do\r
+ let v = eval nu a\r
+ check v e\r
+ rho <- asks env\r
+ let v' = eval rho e\r
+ checks (xas,Pair nu (x,v')) es\r
+checks _ _ = throwError "checks"\r
+\r
+-- Not used since we have U : U\r
+--\r
+-- (=?=) :: Typing Ter -> Ter -> Typing ()\r
+-- m =?= s2 = do\r
+-- s1 <- m\r
+-- unless (s1 == s2) $ throwError (show s1 ++ " =/= " ++ show s2)\r
+--\r
+-- checkTs :: [(String,Ter)] -> Typing ()\r
+-- checkTs [] = return ()\r
+-- checkTs ((x,a):xas) = do\r
+-- checkType a\r
+-- local (addType (x,a)) (checkTs xas)\r
+--\r
+-- checkType :: Ter -> Typing ()\r
+-- checkType t = case t of\r
+-- U -> return ()\r
+-- Pi a (Lam x b) -> do\r
+-- checkType a\r
+-- local (addType (x,a)) (checkType b)\r
+-- _ -> infer t =?= U\r
--- /dev/null
+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
--- /dev/null
+;; 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)
projects / cubicaltt.git / commitdiff