From 363097525b1958b8b1c345fbec73872d5c2936e2 Mon Sep 17 00:00:00 2001 From: Anders Date: Mon, 16 Mar 2015 17:09:28 +0100 Subject: [PATCH] Start working on cubical type theory --- Eval.hs | 45 +++++++++------- Exp.cf | 11 ++-- Main.hs | 3 +- Resolver.hs | 141 ++++++++++++++++++++++++++++-------------------- TT.hs | 44 +++++++-------- TypeChecker.hs | 94 ++++++++++++++++---------------- examples/nat.tt | 36 +++++++++---- 7 files changed, 213 insertions(+), 161 deletions(-) diff --git a/Eval.hs b/Eval.hs index 682d50c..9146f57 100644 --- a/Eval.hs +++ b/Eval.hs @@ -9,23 +9,30 @@ 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 + Just (_,t) -> eval r t Nothing -> look x r1 +lookType :: String -> Env -> Val +lookType x (Pair rho ((y,_),VN (VVar _ a))) | x == y = a + | otherwise = lookType x rho +lookType x r@(PDef es r1) = case lookupIdent x es of + Just (a,_) -> eval r a + Nothing -> lookType 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) + Pi t@(Lam _ a _) -> VPi (eval e a) (eval e t) + Lam x a t -> Ter (Lam x a t) e + Sigma t@(Lam _ a _) -> VSigma (eval e a) (eval e t) 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 + Where t decls -> eval (PDef decls e) t Con name ts -> VCon name (map (eval e) ts) - Split l brcs -> Ter (Split l brcs) e + Split l t brcs -> Ter (Split l t brcs) e Sum pr lbls -> Ter (Sum pr lbls) e Undef l -> error $ "eval: undefined at " ++ show l @@ -33,12 +40,12 @@ 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 +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 u@(Ter (Split _ _ _) _) (VN v) = VN (VSplit u v) app (VN r) s = VN (VApp r s) fstVal, sndVal :: Val -> Val @@ -53,23 +60,23 @@ sndVal (VN u) = VN (VSnd u) 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 + (Ter (Lam x a u) e,Ter (Lam x' a' u') e') -> + let v = mkVar k (eval e a) 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 + (Ter (Lam x a u) e,u') -> + let v = mkVar k (eval e a) in conv (k+1) (eval (Pair e (x,v)) u) (app u' v) - (u',Ter (Lam x u) e) -> - let v = mkVar k + (u',Ter (Lam x a u) e) -> + let v = mkVar k (eval e a) 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 (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 + let w = mkVar k u in conv k u u' && conv (k+1) (app v w) (app v' w) (VSigma u v,VSigma u' v') -> - let w = mkVar k + let w = mkVar k u 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' @@ -84,7 +91,7 @@ convNeutral k u v = case (u,v) of (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' + (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 index 9658ba1..928b5ab 100644 --- a/Exp.cf +++ b/Exp.cf @@ -12,18 +12,17 @@ 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] ; +DeclDef. Decl ::= AIdent [Tele] ":" Exp "=" ExpWhere ; +DeclData. Decl ::= "data" AIdent [Tele] "=" [Label] ; +DeclSplit. Decl ::= AIdent [Tele] ":" Exp "=" "split" "{" [Branch] "}" ; +-- DeclMutual. Decl ::= "mutual" "{" [Decl] "}" ; 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] "}" ; +Lam. Exp ::= "\\" [PTele] "->" Exp ; Fun. Exp1 ::= Exp2 "->" Exp1 ; Pi. Exp1 ::= [PTele] "->" Exp1 ; Sigma. Exp1 ::= [PTele] "*" Exp1 ; diff --git a/Main.hs b/Main.hs index 6c2d413..4b05ded 100644 --- a/Main.hs +++ b/Main.hs @@ -89,6 +89,7 @@ initLoop flags f = do putStrLn $ "Resolver failed: " ++ err runInputT (settings []) (loop flags f [] TC.verboseEnv) Right (adefs,names) -> do + -- putStrLn $ "adefs = " ++ show adefs (merr,tenv) <- TC.runDeclss TC.verboseEnv adefs case merr of Just err -> putStrLn $ "Type checking failed: " ++ err @@ -99,7 +100,7 @@ initLoop flags f = do -- The main loop loop :: [Flag] -> FilePath -> [(Binder,SymKind)] -> TC.TEnv -> Interpreter () -loop flags f names tenv@(TC.TEnv _ rho _ _) = do +loop flags f names tenv@(TC.TEnv _ rho _) = do input <- getInputLine prompt case input of Nothing -> outputStrLn help >> loop flags f names tenv diff --git a/Resolver.hs b/Resolver.hs index b0e587e..6af143e 100644 --- a/Resolver.hs +++ b/Resolver.hs @@ -14,6 +14,7 @@ import Control.Monad.Error (throwError) import Control.Monad (when) import Data.Functor.Identity import Data.List (nub) +import Prelude hiding (pi) type Ter = TT.Ter @@ -52,12 +53,13 @@ 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 :: [PTele] -> Resolver [(AIdent,Exp)] flattenPTele [] = return [] -flattenPTele (PTele exp typ : xs) = do - ids <- appsToIdents exp - pt <- flattenPTele xs +flattenPTele (PTele exp typ : xs) = case appsToIdents exp of + Just ids -> do + pt <- flattenPTele xs return $ map (,typ) ids ++ pt + Nothing -> throwError "malformed ptele" ------------------------------------------------------------------------------- -- | Resolver and environment @@ -125,17 +127,19 @@ resolveVar (AIdent (l,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 +lam :: (AIdent,Exp) -> Resolver Ter -> Resolver Ter +lam (a,t) e = do + x <- resolveAIdent a + t' <- resolveExp t + TT.Lam x t' <$> local (insertVar x) e -lams :: [AIdent] -> Resolver Ter -> Resolver Ter +lams :: [(AIdent,Exp)] -> 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 +bind :: (Ter -> Ter) -> (AIdent,Exp) -> Resolver Ter -> Resolver Ter +bind f (x,t) e = f <$> lam (x,t) e -binds :: (Ter -> Ter -> Ter) -> [(AIdent,Exp)] -> Resolver Ter -> Resolver Ter +binds :: (Ter -> Ter) -> [(AIdent,Exp)] -> Resolver Ter -> Resolver Ter binds f = flip $ foldr $ bind f resolveExp :: Exp -> Resolver Ter @@ -143,21 +147,19 @@ 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 (Sigma ptele b) = do + tele <- flattenPTele ptele + binds TT.Sigma tele (resolveExp b) +resolveExp (Pi ptele b) = do + tele <- flattenPTele ptele + binds TT.Pi tele (resolveExp b) resolveExp (Fun a b) = bind TT.Pi (AIdent ((0,0),"_"), a) (resolveExp b) -resolveExp (Lam x xs t) = lams (x:xs) (resolveExp t) +resolveExp (Lam ptele t) = do + tele <- flattenPTele ptele + lams tele (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) @@ -184,48 +186,73 @@ 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 +piToFam :: Exp -> Resolver Ter +piToFam (Fun a b) = lam (AIdent ((0,0),"_"),a) $ resolveExp b +piToFam (Pi ptele b) = do + (x,a):tele <- flattenPTele ptele + lam (x,a) (binds TT.Pi tele (resolveExp b)) + +-- Resolve Data or Def or Split declaration +resolveDecl :: Decl -> Resolver ((TT.Binder,(Ter,Ter)),[(TT.Binder,SymKind)]) +resolveDecl (DeclDef n tele t body) = do + f <- resolveAIdent n + let tele' = flattenTele tele + d <- lams tele' (resolveWhere body) + a <- binds TT.Pi tele' (resolveExp t) + return ((f,(a,d)),[(f,Variable)]) +resolveDecl (DeclData n tele sums) = do + f <- resolveAIdent n + let tele' = flattenTele tele + d <- lams tele' $ local (insertVar f) $ + TT.Sum <$> resolveAIdent n <*> mapM resolveLabel sums + a <- binds TT.Pi tele' (return TT.U) + cs <- mapM resolveAIdent [ lbl | Label lbl _ <- sums ] + return ((f,(a,d)),(f,Variable):map (,Constructor) cs) +resolveDecl (DeclSplit n tele t brs) = do + f <- resolveAIdent n + let tele' = flattenTele tele + vars <- mapM resolveAIdent $ map fst tele' + fam <- local (insertVars vars) $ piToFam t + brs' <- local (insertVars (f:vars)) (mapM resolveBranch brs) + a <- binds TT.Pi tele' (resolveExp t) + loc <- getLoc (case brs of Branch (AIdent (l,_)) _ _:_ -> l ; _ -> (0,0)) + body <- lams tele' (return $ TT.Split loc fam brs') + return $ ((f,(a,body)),[(f,Variable)]) -- 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 +-- 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] +resolveDecls (d:ds) = do + (rtd,names) <- resolveDecl d -- (TT.Binder,(Ter,Ter)) (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 + 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) = diff --git a/TT.hs b/TT.hs index 4566f12..be00846 100644 --- a/TT.hs +++ b/TT.hs @@ -29,36 +29,36 @@ type Tele = [(Binder,Ter)] type LblSum = [(Binder,Tele)] -- Mutual recursive definitions: (x1 : A1) .. (xn : An) and x1 = e1 .. xn = en -type Decls = [(Binder,Ter,Ter)] +type Decls = [(Binder,(Ter,Ter))] declBinders :: Decls -> [Binder] -declBinders decls = [ x | (x,_,_) <- decls ] +declBinders decls = [ x | (x,_) <- decls ] declTers :: Decls -> [Ter] -declTers decls = [ d | (_,_,d) <- decls ] +declTers decls = [ d | (_,(_,d)) <- decls ] declTele :: Decls -> Tele -declTele decls = [ (x,t) | (x,t,_) <- decls ] +declTele decls = [ (x,t) | (x,(t,_)) <- decls ] declDefs :: Decls -> [(Binder,Ter)] -declDefs decls = [ (x,d) | (x,_,d) <- decls ] +declDefs decls = [ (x,d) | (x,(_,d)) <- decls ] -- Terms data Ter = App Ter Ter - | Pi Ter Ter - | Lam Binder Ter + | Pi Ter + | Lam Binder Ter Ter | Where Ter Decls | Var String | U -- Sigma types: - | Sigma Ter Ter + | Sigma Ter | SPair Ter Ter | Fst Ter | Snd Ter -- constructor c Ms | Con Label [Ter] -- branches c1 xs1 -> M1,..., cn xsn -> Mn - | Split Loc [Branch] + | Split Loc Ter [Branch] -- labelled sum c1 A1s,..., cn Ans (assumes terms are constructors) | Sum Binder LblSum -- undefined @@ -76,8 +76,8 @@ 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 ] +-- mkLams :: [String] -> Ter -> Ter +-- mkLams bs t = foldr Lam t [ noLoc b | b <- bs ] mkWheres :: [Decls] -> Ter -> Ter mkWheres [] e = e @@ -97,22 +97,22 @@ data Val = VU deriving Eq -- neutral values -data Neutral = VVar String +data Neutral = VVar String Val | VFst Neutral | VSnd Neutral | VSplit Val Neutral | VApp Neutral Val deriving Eq -mkVar :: Int -> Val -mkVar k = VN (VVar ('X' : show k)) +mkVar :: Int -> Val -> Val +mkVar k t = VN (VVar ('X' : show k) t) -------------------------------------------------------------------------------- -- | Environments data Env = Empty | Pair Env (Binder,Val) - | PDef [(Binder,Ter)] Env + | PDef Decls Env deriving Eq pairs :: Env -> [(Binder,Val)] -> Env @@ -159,16 +159,16 @@ 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 + Pi e0 -> text "Pi" <+> showTer e0 + Lam (x,_) t 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] + Sigma e0 -> text "Sigma" <+> showTer e0 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 + Split l _ _ -> text "split" <+> showLoc l Sum (n,l) _ -> text "sum" <+> text n Undef _ -> text "undefined" @@ -186,7 +186,7 @@ showTer1 t = case t of showDecls :: Decls -> Doc showDecls defs = hsep $ punctuate (char ',') - [ text x <+> equals <+> showTer d | ((x,_),_,d) <- defs ] + [ text x <+> equals <+> showTer d | ((x,_),(_,d)) <- defs ] instance Show Val where show = render . showVal @@ -197,7 +197,7 @@ showVal v = case v of 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] + VPi a b -> text "Pi" <+> showVals [a,b] VSPair u v -> parens (showVal1 u <> comma <> showVal1 v) VSigma u v -> text "Sigma" <+> showVals [u,v] VN n -> showNeutral n @@ -216,7 +216,7 @@ 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 + VVar x t -> text x VFst u -> showNeutral u <> text ".1" VSnd u -> showNeutral u <> text ".2" showNeutral1 n = case n of diff --git a/TypeChecker.hs b/TypeChecker.hs index 2ff658e..46fde7f 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -18,45 +18,31 @@ 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 +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 +addTypeVal (x,a) (TEnv k rho v) = + TEnv (k+1) (Pair rho (x,mkVar k a)) 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 +addType (x,a) tenv@(TEnv _ rho _) = return $ addTypeVal (x,eval rho a) tenv -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 +addBranch :: [(Binder,Val)] -> (Tele,Env) -> TEnv -> TEnv +addBranch nvs (tele,env) (TEnv k rho v) = + TEnv (k + length nvs) (pairs rho nvs) 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 +addDecls :: Decls -> TEnv -> TEnv +addDecls d (TEnv k rho v) = TEnv k (PDef d rho) v addTele :: Tele -> TEnv -> Typing TEnv addTele xas lenv = foldM (flip addType) lenv xas @@ -73,7 +59,7 @@ runTyping env t = runErrorT $ runReaderT t env runDecls :: TEnv -> Decls -> IO (Either String TEnv) runDecls tenv d = runTyping tenv $ do checkDecls d - addDecls d tenv + return $ addDecls d tenv runDeclss :: TEnv -> [Decls] -> IO (Maybe String,TEnv) runDeclss tenv [] = return (Nothing, tenv) @@ -101,11 +87,11 @@ localM f r = do a <- f e local (const a) r -getFresh :: Typing Val -getFresh = do +getFresh :: Val -> Typing Val +getFresh a = do k <- index <$> ask e <- asks env - return $ mkVar k + return $ mkVar k a checkDecls :: Decls -> Typing () checkDecls d = do @@ -121,28 +107,38 @@ checkTele ((x,a):xas) = do check VU a localM (addType (x,a)) $ checkTele xas +checkFam :: Ter -> Typing () +checkFam (Lam x a b) = do + check VU a + localM (addType (x,a)) $ check VU b +checkFam _ = throwError "checkFam" + -- 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,Pi f) -> checkFam f + (VU,Sigma f) -> checkFam f (VU,Sum _ bs) -> sequence_ [checkTele as | (_,as) <- bs] - (VPi (Ter (Sum _ cas) nu) f,Split _ ces) -> do + (VPi (Ter (Sum _ cas) nu) f,Split _ f' ces) -> do + checkFam f' + k <- asks index + rho <- asks env + unless (conv k f (eval rho f')) $ throwError "check: split annotations" 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 + (VPi a f,Lam x a' t) -> do + check VU a' + k <- asks index + rho <- asks env + unless (conv k a (eval rho a')) $ throwError "check: lam types don't match" + var <- getFresh a local (addTypeVal (x,a)) $ check (app f var) t (VSigma a f, SPair t1 t2) -> do check a t1 @@ -151,7 +147,7 @@ check a t = case (a,t) of check (app f v) t2 (_,Where e d) -> do checkDecls d - localM (addDecls d) $ check a e + local (addDecls d) $ check a e (_,Undef _) -> return () _ -> do v <- infer t @@ -163,19 +159,25 @@ 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 + let us = mkVars k xas nu + local (addBranch (zip xs us) (xas,nu)) $ check (app f (VCon c us)) e + +mkVars k [] _ = [] +mkVars k ((x,a):xas) nu = + let w = mkVar k (eval nu a) + in w : mkVars (k+1) xas (Pair nu (x,w)) + +-- inferNeutral :: Val -> Val +-- inferNeutral (VN (VVar _ a)) = a +-- inferNeutral _ = error "not done yet" -- 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!" + rho <- env <$> ask + return $ lookType n rho App t u -> do c <- infer t case c of @@ -200,7 +202,7 @@ infer e = case e of _ -> throwError $ show c ++ " is not a sigma-type" Where t d -> do checkDecls d - localM (addDecls d) $ infer t + local (addDecls d) $ infer t _ -> throwError ("infer " ++ show e) checks :: (Tele,Env) -> [Ter] -> Typing () diff --git a/examples/nat.tt b/examples/nat.tt index 2130d7f..47c9f44 100644 --- a/examples/nat.tt +++ b/examples/nat.tt @@ -1,20 +1,36 @@ module nat where -nat : U data nat = zero | suc (n : nat) -one : nat -one = suc zero +zero' : nat = zero +one : nat = suc zero +two : nat = suc one -two : nat -two = suc one -pred : nat -> nat -pred = split +pred : nat -> nat = split zero -> zero suc n -> n -add : nat -> nat -> nat -add m = split +add (m : nat) : nat -> nat = split zero -> m - suc n -> suc (add m n) \ No newline at end of file + suc n -> suc (add m n) + +add' : nat -> nat -> nat = split + zero -> \(x : nat) -> x + suc n -> \(x : nat) -> suc (add' n x) + +id (A : U) (a : A) : A = a + + +data list (A : U) = nil | cons (a : A) (as : list A) + +l : list nat = cons one (cons two nil) + +append (A : U) : list A -> list A -> list A = split + nil -> id (list A) + cons x xs -> \(ys : list A) -> cons x (append A xs ys) + +reverse (A : U) : list A -> list A = split + nil -> nil + cons x xs -> append A (reverse A xs) (cons x nil) + \ No newline at end of file -- 2.34.1