From: Anders <mortberg@chalmers.se>
Date: Mon, 16 Mar 2015 16:09:28 +0000 (+0100)
Subject: Start working on cubical type theory
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=363097525b1958b8b1c345fbec73872d5c2936e2;p=cubicaltt.git

Start working on cubical type theory
---

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