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
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
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'
(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')
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 ;
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
-- 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
import Control.Monad (when)
import Data.Functor.Identity
import Data.List (nub)
+import Prelude hiding (pi)
type Ter = TT.Ter
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
_ -> 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
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)
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) =
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
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
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
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"
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
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
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
-- 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
+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
+addTypeVal (x,a) (TEnv k rho v) =\r
+ TEnv (k+1) (Pair rho (x,mkVar k a)) 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
+addType (x,a) tenv@(TEnv _ rho _) = return $ addTypeVal (x,eval rho a) tenv\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
+addBranch :: [(Binder,Val)] -> (Tele,Env) -> TEnv -> TEnv\r
+addBranch nvs (tele,env) (TEnv k rho v) =\r
+ TEnv (k + length nvs) (pairs rho nvs) 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
+addDecls :: Decls -> TEnv -> TEnv\r
+addDecls d (TEnv k rho v) = TEnv k (PDef d rho) v\r
\r
addTele :: Tele -> TEnv -> Typing TEnv\r
addTele xas lenv = foldM (flip addType) lenv xas\r
runDecls :: TEnv -> Decls -> IO (Either String TEnv)\r
runDecls tenv d = runTyping tenv $ do\r
checkDecls d\r
- addDecls d tenv\r
+ return $ addDecls d tenv\r
\r
runDeclss :: TEnv -> [Decls] -> IO (Maybe String,TEnv)\r
runDeclss tenv [] = return (Nothing, tenv)\r
a <- f e\r
local (const a) r\r
\r
-getFresh :: Typing Val\r
-getFresh = do\r
+getFresh :: Val -> Typing Val\r
+getFresh a = do\r
k <- index <$> ask\r
e <- asks env\r
- return $ mkVar k\r
+ return $ mkVar k a\r
\r
checkDecls :: Decls -> Typing ()\r
checkDecls d = do\r
check VU a\r
localM (addType (x,a)) $ checkTele xas\r
\r
+checkFam :: Ter -> Typing ()\r
+checkFam (Lam x a b) = do\r
+ check VU a\r
+ localM (addType (x,a)) $ check VU b\r
+checkFam _ = throwError "checkFam"\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,Pi f) -> checkFam f\r
+ (VU,Sigma f) -> checkFam f\r
(VU,Sum _ bs) -> sequence_ [checkTele as | (_,as) <- bs]\r
- (VPi (Ter (Sum _ cas) nu) f,Split _ ces) -> do\r
+ (VPi (Ter (Sum _ cas) nu) f,Split _ f' ces) -> do\r
+ checkFam f'\r
+ k <- asks index\r
+ rho <- asks env\r
+ unless (conv k f (eval rho f')) $ throwError "check: split annotations"\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
+ (VPi a f,Lam x a' t) -> do\r
+ check VU a'\r
+ k <- asks index\r
+ rho <- asks env\r
+ unless (conv k a (eval rho a')) $ throwError "check: lam types don't match"\r
+ var <- getFresh a\r
local (addTypeVal (x,a)) $ check (app f var) t\r
(VSigma a f, SPair t1 t2) -> do\r
check a t1\r
check (app f v) t2\r
(_,Where e d) -> do\r
checkDecls d\r
- localM (addDecls d) $ check a e\r
+ local (addDecls d) $ check a e\r
(_,Undef _) -> return ()\r
_ -> do\r
v <- infer t\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
+ let us = mkVars k xas nu\r
+ local (addBranch (zip xs us) (xas,nu)) $ check (app f (VCon c us)) e\r
+\r
+mkVars k [] _ = []\r
+mkVars k ((x,a):xas) nu =\r
+ let w = mkVar k (eval nu a)\r
+ in w : mkVars (k+1) xas (Pair nu (x,w))\r
+\r
+-- inferNeutral :: Val -> Val\r
+-- inferNeutral (VN (VVar _ a)) = a\r
+-- inferNeutral _ = error "not done yet"\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
+ rho <- env <$> ask\r
+ return $ lookType n rho\r
App t u -> do\r
c <- infer t\r
case c of\r
_ -> throwError $ show c ++ " is not a sigma-type"\r
Where t d -> do\r
checkDecls d\r
- localM (addDecls d) $ infer t\r
+ local (addDecls d) $ infer t\r
_ -> throwError ("infer " ++ show e)\r
\r
checks :: (Tele,Env) -> [Ter] -> Typing ()\r
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
projects / cubicaltt.git / commitdiff