Add type checking.HEADmaster

Currently, there is Set in Set. Next step is to add universe levels.

10 files changed, 646 insertions, 100 deletions

diff --git a/obs.ipkg b/obs.ipkg
index f85a6ef..b6cb577 100644
--- a/obs.ipkg
+++ b/obs.ipkg
@@ -6,12 +6,13 @@ depends = contrib
 
 options = "--total"
 
-executable = "cc-eval"
+executable = "cc-check"
 main = Main
 
 modules
   = CC.Name
   , CC.Term
+  , CC.Term.Elaborate
   , CC.Term.Eval
   , CC.Term.Parse
   , CC.Term.Pretty
diff --git a/src/CC/Name.idr b/src/CC/Name.idr
index 4c25f5c..d1df253 100644
--- a/src/CC/Name.idr
+++ b/src/CC/Name.idr
@@ -2,6 +2,10 @@ module CC.Name
 
 import public Control.Relation
 
+import Data.List
+import Data.Singleton
+import Data.Stream
+
 import Decidable.Equality
 
 import Text.Bounded
@@ -65,3 +69,24 @@ decEquiv m n = decEq m.val n.val
 export
 bounds : (name : Name) -> Maybe Bounds
 bounds name = if name.isIrrelevant then Nothing else Just name.bounds
+
+||| Returns a new name not in the set.
+export
+fresh : Foldable f => f Name -> Name
+fresh xs =
+  irrelevantBounds $
+  select (unfoldr (\n => ("_\{show n}", S n)) 0) $
+  sort $
+  foldMap (singleton . val) xs
+  where
+  select : Ord a => Stream a -> List a -> a
+  select (x :: xs) [] = x
+  select (x :: xs) (y :: ys) =
+    case compare x y of
+      LT => x
+      EQ => select xs ys
+      GT => select (x :: xs) ys
+
+export
+fresh' : Foldable f => Singleton {a = f Name} xs -> Name
+fresh' (Val xs) = fresh xs
diff --git a/src/CC/Term.idr b/src/CC/Term.idr
index 1806904..233afda 100644
--- a/src/CC/Term.idr
+++ b/src/CC/Term.idr
@@ -3,6 +3,12 @@ module CC.Term
 import CC.Name
 import CC.Thinning
 
+import Control.Function
+
+import Data.Nat
+import Data.Singleton
+import Data.SnocList.Elem
+
 -- Definition ------------------------------------------------------------------
 
 public export
@@ -17,28 +23,41 @@ data IsVar : Nat -> Name -> Context -> Type where
 public export
 data Term : Context -> Type where
   Var : (k : Nat) -> (0 n : Name) -> (0 prf : IsVar k n ctx) -> Term ctx
+
+  Let :
+    (n : Name) ->
+    (ty : Maybe (Term ctx)) ->
+    (val : Term ctx) ->
+    (t : Term (ctx :< n)) ->
+    Term ctx
+
+  Set : Term ctx
+
+  Pi : (n : Maybe Name) -> Term ctx -> Term (ctx ++ maybe [<] ([<] :<) n) -> Term ctx
   Abs : (n : Name) -> Term (ctx :< n) -> Term ctx
   App : Term ctx -> Term ctx -> Term ctx
-  Let : (n : Name) -> Term ctx -> Term (ctx :< n) -> Term ctx
 
 public export
 data Value : Context -> Type
 public export
 data Neutral : Context -> Type
-public export
-data Closure : Context -> Type
 
 public export
 data Env : (local, global : Context) -> Type where
   Lin  : Env [<] global
   (:<) : Env local global -> (p : (Name, Lazy (Value global))) -> Env (local :< fst p) global
 
-data Closure : Context -> Type where
-  Close : (n : Name) -> Env local global -> Term (local :< n) -> Closure global
-
 data Value where
   Ntrl : Neutral ctx -> Value ctx
-  VAbs : Closure ctx -> Value ctx
+  VSet : Value ctx
+  VPi :
+    (n : Name) ->
+    Lazy (Value ctx) ->
+    Env local ctx ->
+    Term (local :< n) ->
+    Value ctx
+  VFunc : Env local ctx -> Term local -> Term local -> Value ctx
+  VAbs : Env local ctx -> (n : Name) -> Term (local :< n) -> Value ctx
 
 data Neutral where
   VVar : (k : Nat) -> (0 n : Name) -> (0 prf : IsVar k n ctx) -> Neutral ctx
@@ -48,7 +67,6 @@ data Neutral where
 %name Term t, u
 %name Value v
 %name Neutral n
-%name Closure close
 %name Env env
 
 -- Operations ------------------------------------------------------------------
@@ -58,6 +76,31 @@ index : Env local global -> (k : Nat) -> (0 prf : IsVar k n local) -> Value glob
 index (env :< (n, v)) 0 (Here eq) = v
 index (env :< _) (S k) (There prf) = index env k prf
 
+export
+fromElem : {n : Name} -> (prf : Elem n ctx) -> IsVar (elemToNat prf) n ctx
+fromElem Here = Here (reflexive {rel = (~~)})
+fromElem (There i) = There (fromElem i)
+
+export
+tabulate :
+  {local : Context} ->
+  (f : Nat -> Nat) ->
+  (0 prf : {k, n : _} -> IsVar k n local -> IsVar (f k) n global) ->
+  Env local global
+tabulate {local = [<]} f prf = [<]
+tabulate {local = _ :< n} f prf =
+  tabulate (f . S) (prf . There) :<
+  (n, Ntrl $ VVar (f 0) n (prf $ fromElem Here))
+
+export
+(++) : Env local1 global -> Env local2 global -> Env (local1 ++ local2) global
+env ++ [<] = env
+env ++ env' :< p = (env ++ env') :< p
+
+recomputeLocal : Env local global -> Singleton local
+recomputeLocal [<] = Val [<]
+recomputeLocal (env :< (n, _)) = Val (:< n) <*> recomputeLocal env
+
 -- Weakening -------------------------------------------------------------------
 
 wknVar' :
@@ -95,26 +138,64 @@ wknIsVar prf thin = wknIsVar' prf (view thin)
 export
 wknTerm : Term src -> src `Thins` tgt -> Term tgt
 wknTerm (Var k n prf) thin = Var (wknVar thin prf) n (wknIsVar prf thin)
+wknTerm (Let n Nothing val t) thin = Let n Nothing (wknTerm val thin) (wknTerm t (keep thin))
+wknTerm (Let n (Just ty) val t) thin =
+  Let n (Just $ wknTerm ty thin) (wknTerm val thin) (wknTerm t (keep thin))
+wknTerm Set thin = Set
+wknTerm (Pi Nothing dom cod) thin = Pi Nothing (wknTerm dom thin) (wknTerm cod thin)
+wknTerm (Pi (Just n) dom cod) thin = Pi (Just n) (wknTerm dom thin) (wknTerm cod (keep thin))
 wknTerm (Abs n t) thin = Abs n (wknTerm t (keep thin))
 wknTerm (App t u) thin = App (wknTerm t thin) (wknTerm u thin)
-wknTerm (Let n t u) thin = Let n (wknTerm t thin) (wknTerm u (keep thin))
 
 export
 wknNtrl : Neutral src -> src `Thins` tgt -> Neutral tgt
 export
 wknVal : Value src -> src `Thins` tgt -> Value tgt
 export
-wknClose : Closure src -> src `Thins` tgt -> Closure tgt
-export
 wknEnv : Env local src -> src `Thins` tgt -> Env local tgt
 
 wknNtrl (VVar k n prf) thin = VVar (wknVar thin prf) n (wknIsVar prf thin)
 wknNtrl (VApp n v) thin = VApp (wknNtrl n thin) (wknVal v thin)
 
 wknVal (Ntrl n) thin = Ntrl (wknNtrl n thin)
-wknVal (VAbs close) thin = VAbs (wknClose close thin)
-
-wknClose (Close n env t) thin = Close n (wknEnv env thin) t
+wknVal VSet thin = VSet
+wknVal (VPi n dom env cod) thin = VPi n (wknVal dom thin) (wknEnv env thin) cod
+wknVal (VFunc env dom cod) thin = VFunc (wknEnv env thin) dom cod
+wknVal (VAbs env n t) thin = VAbs (wknEnv env thin) n t
 
 wknEnv [<] thin = [<]
 wknEnv (env :< (n, v)) thin = wknEnv env thin :< (n, wknVal v thin)
+
+-- Renaming --------------------------------------------------------------------
+
+renVar : {src, tgt : Context} -> length src = length tgt -> IsVar k n src -> (m ** IsVar k m tgt)
+renVar prf (Here eq) {tgt = _ :< m} = (m ** fromElem Here)
+renVar prf (There prf') {tgt = _ :< m} =
+  let rec = renVar (injective prf) prf' in (rec.fst ** There rec.snd)
+
+export
+renTerm : length src = length tgt -> Term src -> Term tgt
+renTerm prf (Var k n prf') = let 0 var = renVar prf prf' in Var k var.fst var.snd
+renTerm prf (Let n Nothing val t) =
+  Let n Nothing (renTerm prf val) (renTerm (cong S prf) t)
+renTerm prf (Let n (Just ty) val t) =
+  Let n (Just $ renTerm prf ty) (renTerm prf val) (renTerm (cong S prf) t)
+renTerm prf Set = Set
+renTerm prf (Pi Nothing t u) = Pi Nothing (renTerm prf t) (renTerm prf u)
+renTerm prf (Pi (Just n) t u) = Pi (Just n) (renTerm prf t) (renTerm (cong S prf) u)
+renTerm prf (Abs n t) = Abs n (renTerm (cong S prf) t)
+renTerm prf (App t u) = App (renTerm prf t) (renTerm prf u)
+
+-- Lifting ---------------------------------------------------------------------
+
+inrVar : IsVar k n ctx -> IsVar k n (global ++ ctx)
+inrVar (Here eq) = Here eq
+inrVar (There prf) = There (inrVar prf)
+
+liftEnv :
+  {global : Context} ->
+  (ctx : Context) ->
+  Env local global ->
+  Env (local ++ ctx) (global ++ ctx)
+liftEnv [<] env = env
+liftEnv ctx env = wknEnv env (id ++ empty) ++ tabulate id inrVar
diff --git a/src/CC/Term/Elaborate.idr b/src/CC/Term/Elaborate.idr
new file mode 100644
index 0000000..458ec38
--- /dev/null
+++ b/src/CC/Term/Elaborate.idr
@@ -0,0 +1,221 @@
+module CC.Term.Elaborate
+
+import CC.Name
+import CC.Term
+import CC.Term.Eval
+import CC.Term.Raw
+import CC.Thinning
+
+import Data.DPair
+import Data.List1
+import Data.Singleton
+import Data.SnocList
+import Data.SnocList.Elem
+
+import Text.Bounded
+
+%prefix_record_projections off
+
+-- Elaboration Errors ----------------------------------------------------------
+
+export
+data ElabError : Type -> Type where
+  Ok : ty -> ElabError ty
+  Error : List1 (Either Name (String, Maybe Bounds)) -> ElabError ty
+
+Functor ElabError where
+  map f (Ok x) = Ok (f x)
+  map f (Error xs) = Error xs
+
+Applicative ElabError where
+  pure = Ok
+
+  Ok f <*> Ok v = Ok (f v)
+  Ok f <*> Error ys = Error ys
+  Error xs <*> Ok v = Error xs
+  Error xs <*> Error ys = Error (xs ++ ys)
+
+Monad ElabError where
+  join (Ok (Ok x)) = Ok x
+  join (Ok (Error xs)) = Error xs
+  join (Error xs) = Error xs
+
+export
+runElabError : ElabError ty -> Either (List1 (Either Name (String, Maybe Bounds))) ty
+runElabError (Ok x) = Right x
+runElabError (Error xs) = Left xs
+
+fromNameError : NameError ty -> ElabError ty
+fromNameError v =
+  case runNameError v of
+    Left errs => Error (map Left errs)
+    Right v => Ok v
+
+-- Elaboration Context ---------------------------------------------------------
+
+record ElabCtx (local, global : Context) where
+  constructor MkCtx
+  env : Env local global
+  types : (k : Nat) -> forall n. (0 prf : IsVar k n local) -> Lazy (Value global)
+  pos : Maybe Bounds
+
+%name ElabCtx ctx
+
+wknCtx :
+  {global : Context} ->
+  ElabCtx local global ->
+  (n : Name) ->
+  ElabCtx local (global :< n)
+wknCtx ctx n = { env $= flip wknEnv (drop id), types := types } ctx
+  where
+  types : (k : Nat) -> forall m. (0 _ : IsVar k m local) -> Lazy (Value (global :< n))
+  types k prf = wknVal (ctx.types k prf) (drop id)
+
+define :
+  ElabCtx local global ->
+  (n : Name) ->
+  (val : Lazy (Value global)) ->
+  (ty : Lazy (Value global)) ->
+  ElabCtx (local :< n) global
+define ctx n val ty = { env $= (:< (n, val)), types := types } ctx
+  where
+  types : (k : Nat) -> forall m. (0 _ : IsVar k m (local :< n)) -> Lazy (Value global)
+  types 0 (Here eq) = ty
+  types (S k) (There prf) = ctx.types k prf
+
+bind :
+  {global : Context} ->
+  ElabCtx local global ->
+  (n : Name) ->
+  (ty : Lazy (Value global)) ->
+  ElabCtx (local :< n) (global :< n)
+bind ctx n ty = define (wknCtx ctx n) n (Ntrl $ VVar 0 _ $ fromElem Here) (wknVal ty (drop id))
+
+updatePos : ElabCtx local global -> (irrel : Bool) -> Bounds -> ElabCtx local global
+updatePos ctx irrel bounds = { pos := if irrel then Nothing else Just bounds } ctx
+
+-- Checking and Inference ------------------------------------------------------
+
+record PiType (ctx : Context) where
+  constructor MkPi
+  {0 local : Context}
+  name : Name
+  dom : Lazy (Value ctx)
+  env : Env local ctx
+  cod : Term (local :< name)
+
+check :
+  {local, global : Context} ->
+  ElabCtx local global ->
+  RawTerm ->
+  Lazy (Value global) ->
+  ElabError (Term local)
+checkType :
+  {local, global : Context} ->
+  ElabCtx local global ->
+  RawTerm ->
+  ElabError (Term local)
+infer :
+  {local, global : Context} ->
+  ElabCtx local global ->
+  RawTerm ->
+  ElabError (Term local, Lazy (Value global))
+inferPi :
+  {local, global : Context} ->
+  ElabCtx local global ->
+  RawTerm ->
+  ElabError (Term local, PiType global)
+inferType :
+  {local, global : Context} ->
+  ElabCtx local global ->
+  RawTerm ->
+  ElabError (Term local)
+
+check ctx (Bounded (MkBounded t irrel bounds)) ty = check (updatePos ctx irrel bounds) t ty
+
+check ctx (Let n Nothing val t) ty = do
+  (val, ty') <- infer ctx val
+  t <- check (define ctx n (eval ctx.env val) ty') t ty
+  pure $ Let {n, ty = Nothing, val, t}
+check ctx (Let n (Just ty') val t) ty = do
+  ty' <- checkType ctx ty'
+  let vty : Lazy (Value global) = eval ctx.env ty'
+  val <- check ctx val vty
+  t <- check (define ctx n (eval ctx.env val) vty) t ty
+  pure $ Let {n, ty = Just ty', val, t}
+
+check ctx Set VSet = pure $ Set
+
+check ctx (Abs Nothing t) (VFunc env dom cod) = do
+  t <- check ctx t (eval env cod)
+  pure $ Abs (fresh local) (wknTerm t (drop id))
+check ctx (Abs (Just n) t) (VFunc env dom cod) = do
+  t <- check (bind ctx n (eval env dom)) t (eval (wknEnv env (drop id)) cod)
+  pure $ Abs n t
+check ctx (Abs Nothing t) (VPi m dom env cod) = do
+  t <- check (wknCtx ctx m) t (eval (liftEnv [<m] env) cod)
+  pure $ Abs m (wknTerm t (drop id))
+check ctx (Abs (Just n) t) (VPi m dom env cod) = do
+  t <- check (bind ctx n dom) t (eval (liftEnv [<n] env) $ renTerm Refl cod)
+  pure $ Abs n t
+
+check ctx t ty = do
+  (t, ty') <- infer ctx t
+  let True = convert ty ty'
+    | False => Error $ singleton $ Right ("conversion failed", ctx.pos)
+  pure t
+
+checkType ctx t = check ctx t VSet
+
+infer ctx (Bounded (MkBounded t irrel bounds)) = infer (updatePos ctx irrel bounds) t
+infer ctx (Var n) = do
+  Element k prf <- fromNameError $ lookup local n
+  pure (Var k n prf, ctx.types k prf)
+infer ctx (Let n Nothing val t) = do
+  (val, ty') <- infer ctx val
+  (t, ty) <- infer (define ctx n (eval ctx.env val) ty') t
+  pure $ (Let {n, ty = Nothing, val, t}, ty)
+infer ctx (Let n (Just ty) val t) = do
+  ty' <- checkType ctx ty
+  let vty : Lazy (Value global) = eval ctx.env ty'
+  val <- check ctx val vty
+  (t, ty) <- infer (define ctx n (eval ctx.env val) vty) t
+  pure $ (Let {n, ty = Just ty', val, t}, ty)
+infer ctx Set = pure (Set, delay VSet)
+infer ctx (Pi (Nothing `Of` dom) cod) = do
+  (dom, cod) <- [| MkPair (inferType ctx dom) (inferType ctx cod) |]
+  pure $ (Pi Nothing dom cod, delay VSet)
+infer ctx (Pi (Just n `Of` dom) cod) = do
+  dom <- inferType ctx dom
+  let vdom : Lazy (Value global) = eval ctx.env dom
+  cod <- inferType (bind ctx n vdom) cod
+  pure $ (Pi (Just n) dom cod, delay VSet)
+infer ctx (App t u) = do
+  (t, ty) <- inferPi ctx t
+  u <- check ctx u ty.dom
+  let vu : Lazy (Value global) = eval ctx.env u
+  pure $ (App t u, delay $ eval (ty.env :< (ty.name, vu)) ty.cod)
+infer ctx t = Error $ singleton $ Right ("cannot infer type", ctx.pos)
+
+inferPi ctx t = do
+  (t, ty) <- infer ctx t
+  case force ty of
+    VPi n dom env cod =>
+      pure $ (t, MkPi n dom env cod)
+    VFunc env dom cod =>
+      let local' = recomputeLocal env in
+      pure $ (t, MkPi (fresh' local') (eval env dom) env (wknTerm cod (drop $ id' local')))
+    ty => Error $ singleton $ Right ("expected pi type", ctx.pos)
+
+inferType ctx t = do
+  (t, ty) <- infer ctx t
+  case force ty of
+    VSet => pure t
+    ty => Error $ singleton $ Right ("expected set type", ctx.pos)
+
+export
+inferTerm : RawTerm -> ElabError (Term [<], Lazy (Value [<]))
+inferTerm = infer (MkCtx [<] types Nothing)
+  where
+  types : (k : Nat) -> forall n. (0 _ : IsVar k n [<]) -> Lazy (Value [<])
+  types k prf impossible
diff --git a/src/CC/Term/Eval.idr b/src/CC/Term/Eval.idr
index 311bc34..7029893 100644
--- a/src/CC/Term/Eval.idr
+++ b/src/CC/Term/Eval.idr
@@ -4,22 +4,28 @@ import CC.Name
 import CC.Term
 import CC.Thinning
 
+import Data.SnocList.Elem
+
 -- Evaluation ------------------------------------------------------------------
 
 export
-app : Closure ctx -> Lazy (Value ctx) -> Value ctx
+app : (n : Name) -> Env local global -> Term (local :< n) -> Lazy (Value global) -> Value global
 export
 eval : Env local global -> Term local -> Value global
 
-app (Close n env t) v = assert_total $ eval (env :< (n, v)) t
+app n env t v = eval (env :< (n, v)) t
 
 eval env (Var k n prf) = index env k prf
-eval env (Abs n t) = VAbs (Close n env t)
+eval env (Let n ty val t) = eval (env :< (n, eval env val)) t
+eval env Set = VSet
+eval env (Pi Nothing t u) = VFunc env t u
+eval env (Pi (Just n) t u) = VPi n (eval env t) env u
+eval env (Abs n t) = VAbs env n t
 eval env (App t u) =
   case eval env t of
     Ntrl n => Ntrl $ VApp n (eval env u)
-    VAbs close => app close (eval env u)
-eval env (Let n t u) = eval (env :< (n, eval env t)) u
+    VAbs env' n t => assert_total $ app n env' t (eval env u)
+    _ => assert_total $ idris_crash "eval invariant broken"
 
 -- Quoting ---------------------------------------------------------------------
 
@@ -28,11 +34,17 @@ quote : {ctx : _} -> Value ctx -> Term ctx
 quoteNtrl : {ctx : _} -> Neutral ctx -> Term ctx
 
 quote (Ntrl n) = quoteNtrl n
-quote (VAbs close@(Close n _ _)) =
-  Abs n $
-  assert_total $
-  quote $
-  app (wknClose close (drop id)) (Ntrl $ VVar 0 n $ Here $ reflexive {rel = (~~)})
+quote VSet = Set
+quote (VPi n t env u) =
+  Pi (Just n)
+    (quote t)
+    (assert_total $ quote $ eval (liftEnv [<n] env) u)
+quote (VFunc env t u) =
+  Pi Nothing
+    (assert_total $ quote $ eval env t)
+    (assert_total $ quote $ eval env u)
+quote (VAbs env n t) =
+  Abs n $ assert_total $ quote $ app n (wknEnv env (drop id)) t (Ntrl $ VVar 0 _ $ fromElem Here)
 
 quoteNtrl (VVar k n prf) = Var k n prf
 quoteNtrl (VApp n v) = App (quoteNtrl n) (quote v)
@@ -40,3 +52,49 @@ quoteNtrl (VApp n v) = App (quoteNtrl n) (quote v)
 export
 normalise : {global : _} -> Env local global -> Term local -> Term global
 normalise env t = quote $ eval env t
+
+-- Conversion ------------------------------------------------------------------
+
+export
+convert : {ctx : Context} -> Value ctx -> Value ctx -> Bool
+convertNtrl : {ctx : Context} -> Neutral ctx -> Neutral ctx -> Bool
+
+convert VSet VSet = True
+
+convert (VFunc env t u) (VFunc env' t' u') =
+  assert_total $
+  convert (eval env t) (eval env' t') &&
+  convert (eval env u) (eval env' u')
+convert (VFunc env t u) (VPi m t' env' u') =
+  assert_total $
+  convert (eval env t) t' &&
+  convert (eval (wknEnv env (drop id)) u) (eval (liftEnv [<m] env') u')
+convert (VPi n t env u) (VFunc env' t' u') =
+  assert_total $
+  convert t (eval env' t') &&
+  convert (eval (liftEnv [<n] env) u) (eval (wknEnv env' (drop id)) u')
+convert (VPi n t env u) (VPi m t' env' u') =
+  convert t t' &&
+  (assert_total $ convert (eval (liftEnv [<n] env) u) (eval (liftEnv [<n] env') $ renTerm Refl u'))
+
+convert (VAbs env n t) (VAbs env' m u) =
+  assert_total $
+  convert (eval (liftEnv [<n] env) t) (eval (liftEnv [<n] env') $ renTerm Refl u)
+convert (VAbs env n t) (Ntrl m) =
+  assert_total $
+  convert
+    (eval (liftEnv [<n] env) t)
+    (Ntrl (VApp (wknNtrl m (drop id)) (Ntrl $ VVar 0 _ $ fromElem Here)))
+convert (Ntrl n)  (VAbs env m t) =
+  assert_total $
+  convert
+    (Ntrl (VApp (wknNtrl n (drop id)) (Ntrl $ VVar 0 _ $ fromElem Here)))
+    (eval (liftEnv [<m] env) t)
+
+convert (Ntrl n) (Ntrl m) = convertNtrl n m
+
+convert _ _ = False
+
+convertNtrl (VVar k _ _) (VVar j _ _) = k == j
+convertNtrl (VApp n v) (VApp m u) = convertNtrl n m && convert v u
+convertNtrl _ _ = False
diff --git a/src/CC/Term/Parse.idr b/src/CC/Term/Parse.idr
index 3615956..5c8956a 100644
--- a/src/CC/Term/Parse.idr
+++ b/src/CC/Term/Parse.idr
@@ -4,40 +4,65 @@ import CC.Name
 import CC.Term
 import CC.Term.Raw
 
+import Data.Bool
 import Data.List
 
 import Text.Lexer
 import Text.Parser
 
+%hide Text.Parser.match
+
+-- Utilities -------------------------------------------------------------------
+
+expandBindList : Functor f => (f (Maybe Name), RawTerm) -> f RawBinding
+expandBindList (xs, t) = map (`Of` t) xs
+
 -- Tokens ----------------------------------------------------------------------
 
 data CCTokenKind
   = TIgnore
+  -- Variables
   | TIdent
-  -- Keywords
+  -- Let Syntax
   | TLet
-  -- Symbols
+  | TDef
+  | TSemi
+  -- Universes
+  | TSet
+  -- Abstraction
+  | TThinArrow
   | TLambda
-  | TPOpen
-  | TPClose
   | TComma
   | TFatArrow
-  | TDef
-  | TSemi
+  -- Symbols
+  | TUnderscore
+  | TColon
+  | TPOpen
+  | TPClose
 
 %name CCTokenKind k
 
 Eq CCTokenKind where
   TIgnore == TIgnore = True
+
   TIdent == TIdent = True
+
   TLet == TLet = True
+  TDef == TDef = True
+  TSemi == TSemi = True
+
+  TSet == TSet = True
+
+  TThinArrow == TThinArrow = True
   TLambda == TLambda = True
-  TPOpen == TPOpen = True
-  TPClose == TPClose = True
   TComma == TComma = True
   TFatArrow == TFatArrow = True
-  TDef == TDef = True
-  TSemi == TSemi = True
+
+  TUnderscore == TUnderscore = True
+  TColon == TColon = True
+  TPOpen == TPOpen = True
+  TPClose == TPClose = True
+
   _ == _ = False
 
 TokenKind CCTokenKind where
@@ -45,15 +70,45 @@ TokenKind CCTokenKind where
   TokType _ = ()
 
   tokValue TIgnore s = ()
+
   tokValue TIdent s = s
+
   tokValue TLet s = ()
+  tokValue TDef s = ()
+  tokValue TSemi s = ()
+
+  tokValue TSet s = ()
+
+  tokValue TThinArrow s = ()
   tokValue TLambda s = ()
-  tokValue TPOpen s = ()
-  tokValue TPClose s = ()
   tokValue TComma s = ()
   tokValue TFatArrow s = ()
-  tokValue TDef s = ()
-  tokValue TSemi s = ()
+
+  tokValue TUnderscore s = ()
+  tokValue TColon s = ()
+  tokValue TPOpen s = ()
+  tokValue TPClose s = ()
+
+Interpolation CCTokenKind where
+  interpolate TIgnore = "whitespace"
+
+  interpolate TIdent = "identifier"
+
+  interpolate TLet = #""let""#
+  interpolate TDef = #""=""#
+  interpolate TSemi = #"";""#
+
+  interpolate TSet = #""Set""#
+
+  interpolate TThinArrow = #""->""#
+  interpolate TLambda = #""\""#
+  interpolate TComma = #"",""#
+  interpolate TFatArrow = #""=>""#
+
+  interpolate TUnderscore = #""_""#
+  interpolate TColon = #"":""#
+  interpolate TPOpen = #""(""#
+  interpolate TPClose = #"")""#
 
 export
 CCToken : Type
@@ -68,47 +123,92 @@ identifier : Lexer
 identifier = alpha <+> many alphaNum
 
 keywords : List (String, CCTokenKind)
-keywords = [("let", TLet)]
+keywords = [("let", TLet), ("Set", TSet)]
 
 tokenMap : TokenMap CCToken
 tokenMap =
+  -- Ignored
   toTokenMap (map (, TIgnore) ignored) ++
+  -- Identifiers
   [(identifier, \s =>
     case lookup s keywords of
       Just kind => Tok kind s
       Nothing => Tok TIdent s)
   ] ++ toTokenMap [
+    -- Abstraction
+    (exact "->", TThinArrow),
     (exact "\\", TLambda),
     (exact "\x03BB", TLambda),
-    (exact "(", TPOpen),
-    (exact ")", TPClose),
     (exact ",", TComma),
     (exact "=>", TFatArrow),
+    -- Symbols
+    (exact "_", TUnderscore),
+    (exact ":", TColon),
+    (exact "(", TPOpen),
+    (exact ")", TPClose),
+    -- Let syntax (has to be after fat arrow)
     (exact "=", TDef),
     (exact ";", TSemi)
   ]
 
 -- Parser ----------------------------------------------------------------------
 
+match : (kind : CCTokenKind) -> Grammar state CCToken True (TokType kind)
+match k = terminal "expected \{k}" $
+  \t => if t.kind == k then Just $ tokValue k t.text else Nothing
+
 %tcinline
 parens : {b : Bool} -> Grammar state CCToken b ty -> Grammar state CCToken True ty
-parens p = match TPOpen >> commit >> p >>= (\t => match TPClose *> commit *> pure t)
+parens p = match TPOpen >> p >>= (\t => match TPClose *> pure t)
 
 parseIdent : Grammar state CCToken True Name
 parseIdent = MkName <$> (bounds $ match TIdent)
 
+parseBinder : Grammar state CCToken True (Maybe Name)
+parseBinder = either Just (const Nothing) <$> (parseIdent <||> match TUnderscore)
+
+%tcinline
+withBounds : Grammar state CCToken True RawTerm -> Grammar state CCToken True RawTerm
+withBounds p = Bounded <$> bounds p
+
+parseBindList : Grammar state CCToken True (List1 (Maybe Name))
+parseBindList = sepBy1 (match TComma) parseBinder
+
+parseAnnot : (commit : Bool) -> Grammar state CCToken True RawTerm
+parseMaybeAnnot : (commit : Bool) -> Grammar state CCToken False (Maybe RawTerm)
+parseAnnotArgs : (commit : Bool) -> Grammar state CCToken True (List1 (Maybe Name), RawTerm)
+parseOptArrow : (commit : Bool) -> Grammar state CCToken False (Maybe RawTerm)
+
 parseTerm : Grammar state CCToken True RawTerm
+parsePi : Grammar state CCToken True RawTerm
 parseLambda : Grammar state CCToken True RawTerm
 parseLet : Grammar state CCToken True RawTerm
+parseChain : Grammar state CCToken True RawTerm
 parseSpine : Grammar state CCToken True RawTerm
 parseAtom : Grammar state CCToken True RawTerm
 
-parseTerm = parseLambda <|> parseLet <|> parseSpine
+parseAnnot False = match TColon >> parseTerm
+parseAnnot True = match TColon >> commit >> parseTerm
+
+parseMaybeAnnot b = Just <$> parseAnnot b <|> pure Nothing
+
+parseAnnotArgs b = [| MkPair parseBindList (parseAnnot b) |]
+
+parseOptArrow False = Just <$> (match TThinArrow >> parseTerm) <|> pure Nothing
+parseOptArrow True = Just <$> (match TThinArrow >> commit >> parseTerm) <|> pure Nothing
+
+parseTerm = withBounds (parsePi <|> parseLambda <|> parseLet <|> parseChain)
+
+parsePi = do
+  dom <- parens (parseAnnotArgs False)
+  match TThinArrow
+  cod <- parseTerm
+  pure $ foldr1By Pi (flip Pi cod) $ expandBindList dom
 
 parseLambda = do
   match TLambda
   commit
-  names <- sepBy1 (match TComma >> commit) parseIdent
+  names <- parseBindList
   commit
   match TFatArrow
   commit
@@ -120,19 +220,28 @@ parseLet = do
   commit
   n <- parseIdent
   commit
+  ty <- parseMaybeAnnot True
   match TDef
   commit
   t <- parseTerm
   match TSemi
   commit
   u <- parseTerm
-  pure $ Let n t u
+  pure $ Let n ty t u
+
+parseChain = do
+  spine <- parseSpine
+  maybeCod <- parseOptArrow True
+  pure $ case maybeCod of
+    Just cod => Pi (Nothing `Of` spine) cod
+    Nothing => spine
 
 parseSpine = foldl1 App <$> some parseAtom
 
 parseAtom =
-  (Var <$> parseIdent <* commit) <|>
-  (parens parseTerm)
+  withBounds (Var <$> parseIdent <* commit) <|>
+  withBounds (Set <$ match TSet <* commit) <|>
+  parens parseTerm
 
 parseSrc : Grammar state CCToken True RawTerm
 parseSrc = parseTerm <* eof
diff --git a/src/CC/Term/Pretty.idr b/src/CC/Term/Pretty.idr
index 04e3109..2b56e16 100644
--- a/src/CC/Term/Pretty.idr
+++ b/src/CC/Term/Pretty.idr
@@ -7,36 +7,46 @@ import Text.PrettyPrint.Prettyprinter
 
 --------------------------------------------------------------------------------
 
-startPrec, leftAppPrec, appPrec : Prec
+startPrec, leftArrowPrec, leftAppPrec, appPrec : Prec
 startPrec = Open
-leftAppPrec = Backtick
+leftArrowPrec = Backtick
+leftAppPrec = Open
 appPrec = App
 
 prettyVar : (ctx : Context) -> (k : Nat) -> (0 _ : IsVar k n ctx) -> Doc ann
 prettyVar (_ :< n) 0 (Here eq) = pretty n
 prettyVar (ctx :< _) (S k) (There prf) = prettyVar ctx k prf
 
-prettyTerm : {ctx : Context} -> Prec -> Term ctx -> Doc ann
-prettyTerm d (Var k _ prf) = prettyVar ctx k prf
-prettyTerm d (Abs n t) =
-  let (names, body) = mapFst (pretty n ::) $ getNames t in
-  parenthesise (d > startPrec) $ group $
-    backslash <+> concatWith (\x, y => x <+> comma <+> line <+> y) names <++>
-    pretty "=>" <+> softline <+> body
-  where
-  getNames : {ctx : Context} -> Term ctx -> (List (Doc ann), Doc ann)
-  getNames (Abs n t) = mapFst (pretty n ::) (getNames t)
-  getNames t = ([], prettyTerm startPrec t)
-prettyTerm d (App t u) =
-  parenthesise (d >= appPrec) $ group $
-  prettyTerm leftAppPrec t <++> prettyTerm appPrec u
-prettyTerm d (Let n t u) =
-  parenthesise (d > startPrec) $ group $ align $
-    pretty "let" <++>
-    (group $ align $ hang 2 $ pretty n <++> pretty "=" <+> line <+> prettyTerm startPrec t) <+>
-    pretty ";" <+> line <+>
-    prettyTerm startPrec u
-
 export
 {ctx : Context} -> Pretty (Term ctx) where
-  prettyPrec = prettyTerm
+  prettyPrec d (Var k n prf) = prettyVar ctx k prf
+  prettyPrec d (Let n Nothing val t) =
+    parenthesise (d > startPrec) $ group $ align $
+      pretty "let" <++>
+      (group $ align $ hang 2 $ pretty n <++> equals <+> line <+> pretty val) <+>
+      pretty ";" <+> line <+> pretty t
+  prettyPrec d (Let n (Just ty) val t) =
+    parenthesise (d > startPrec) $ group $ align $
+      pretty "let" <++>
+      (group $ align $ hang 2 $
+        pretty n <++> colon <++> pretty ty <++> equals <+> line <+> pretty val) <+>
+      pretty ";" <+> line <+> pretty t
+  prettyPrec d Set = pretty "Set"
+  prettyPrec d (Pi Nothing dom cod) =
+    parenthesise (d > startPrec) $ group $
+      prettyPrec leftArrowPrec dom <++> pretty "->" <++> pretty cod
+  prettyPrec d (Pi (Just n) dom cod) =
+    parenthesise (d > startPrec) $ group $
+      parens (pretty n <++> colon <++> pretty dom) <++> pretty "->" <+> softline <+> pretty cod
+  prettyPrec d (Abs n t) =
+    let (names, body) = mapFst (pretty n ::) $ getNames t in
+    parenthesise (d > startPrec) $ group $
+      backslash <+> concatWith (\x, y => x <+> comma <+> line <+> y) names <++>
+      pretty "=>" <+> softline <+> body
+    where
+    getNames : {ctx : Context} -> Term ctx -> (List (Doc ann), Doc ann)
+    getNames (Abs n t) = mapFst (pretty n ::) (getNames t)
+    getNames t = ([], pretty t)
+  prettyPrec d (App t u) =
+    parenthesise (d >= appPrec) $ group $
+    prettyPrec leftAppPrec t <++> prettyPrec appPrec u
diff --git a/src/CC/Term/Raw.idr b/src/CC/Term/Raw.idr
index 833daf5..10e74bb 100644
--- a/src/CC/Term/Raw.idr
+++ b/src/CC/Term/Raw.idr
@@ -6,15 +6,33 @@ import CC.Term
 import Data.DPair
 import Data.List1
 
+import Text.Bounded
+
 -- Definition ------------------------------------------------------------------
 
 public export
-data RawTerm : Type where
+data RawTerm : Type
+
+public export
+record RawBinding where
+  constructor Of
+  name : Maybe Name
+  bound : RawTerm
+
+data RawTerm where
+  Bounded : WithBounds RawTerm -> RawTerm
+
   Var : (n : Name) -> RawTerm
-  Abs : (n : Name) -> RawTerm -> RawTerm
+
+  Let : Name -> Maybe RawTerm -> RawTerm -> RawTerm -> RawTerm
+
+  Set : RawTerm
+
+  Pi : RawBinding -> RawTerm -> RawTerm
+  Abs : (n : Maybe Name) -> RawTerm -> RawTerm
   App : RawTerm -> RawTerm -> RawTerm
-  Let : (n : Name) -> RawTerm -> RawTerm -> RawTerm
 
+%name RawBinding bind
 %name RawTerm t, u
 
 -- Error Type ------------------------------------------------------------------
@@ -52,10 +70,3 @@ lookup (ctx :< m) n =
   case decEquiv n m of
     Yes eq => Ok (Element 0 (Here eq))
     No _ => map (\p => Element (S p.fst) (There p.snd)) (lookup ctx n)
-
-export
-translate : (ctx : Context) -> RawTerm -> NameError (Term ctx)
-translate ctx (Var n) = (\p => Var p.fst n p.snd) <$> lookup ctx n
-translate ctx (Abs n t) = pure (Abs n) <*> translate (ctx :< n) t
-translate ctx (App t u) = [| App (translate ctx t) (translate ctx u) |]
-translate ctx (Let n t u) = pure (Let n) <*> translate ctx t <*> translate (ctx :< n) u
diff --git a/src/CC/Thinning.idr b/src/CC/Thinning.idr
index 284a230..d1e7745 100644
--- a/src/CC/Thinning.idr
+++ b/src/CC/Thinning.idr
@@ -1,10 +1,12 @@
 module CC.Thinning
 
+import Data.Singleton
+
 -- Definition ------------------------------------------------------------------
 
 export
 data Thins : (src, tgt : SnocList a) -> Type where
-  IsEmpty : [<] `Thins` [<]
+  IsDone : [<] `Thins` [<]
   IsDrop : src `Thins` tgt -> src `Thins` tgt :< x
   IsKeep : src `Thins` tgt -> src :< x `Thins` tgt :< x
 
@@ -13,8 +15,8 @@ data Thins : (src, tgt : SnocList a) -> Type where
 -- Operations ------------------------------------------------------------------
 
 export
-empty : [<] `Thins` [<]
-empty = IsEmpty
+done : [<] `Thins` [<]
+done = IsDone
 
 export
 drop : src `Thins` tgt -> src `Thins` tgt :< x
@@ -25,15 +27,30 @@ keep : src `Thins` tgt -> src :< x `Thins` tgt :< x
 keep thin = IsKeep thin
 
 export
+empty : {ctx : SnocList a} -> [<] `Thins` ctx
+empty {ctx = [<]} = done
+empty {ctx = _ :< _} = drop empty
+
+export
 id : {ctx : SnocList a} -> ctx `Thins` ctx
-id {ctx = [<]} = empty
+id {ctx = [<]} = done
 id {ctx = _ :< _} = keep id
 
+export
+id' : Singleton ctx -> ctx `Thins` ctx
+id' (Val ctx) = id
+
+export
+(++) : src1 `Thins` tgt1 -> src2 `Thins` tgt2 -> src1 ++ src2 `Thins` tgt1 ++ tgt2
+thin ++ IsDone = thin
+thin ++ IsDrop thin' = IsDrop (thin ++ thin')
+thin ++ IsKeep thin' = IsKeep (thin ++ thin')
+
 -- Views -----------------------------------------------------------------------
 
 public export
 data View : src `Thins` tgt -> Type where
-  Empty : View CC.Thinning.empty
+  Done : View CC.Thinning.done
   Drop : (thin : src `Thins` tgt) -> View (drop thin)
   Keep : (thin : src `Thins` tgt) -> View (keep thin)
 
@@ -41,6 +58,6 @@ data View : src `Thins` tgt -> Type where
 
 public export
 view : (thin : src `Thins` tgt) -> View thin
-view IsEmpty = Empty
+view IsDone = Done
 view (IsDrop thin) = Drop thin
 view (IsKeep thin) = Keep thin
diff --git a/src/Main.idr b/src/Main.idr
index 2f05ccf..6f3fafe 100644
--- a/src/Main.idr
+++ b/src/Main.idr
@@ -2,6 +2,7 @@ module Main
 
 import CC.Name
 import CC.Term
+import CC.Term.Elaborate
 import CC.Term.Eval
 import CC.Term.Parse
 import CC.Term.Pretty
@@ -56,24 +57,36 @@ parseStdin = do
 
 helpMsg : String
 helpMsg = unlines [
-  "usage: cc-eval [--help|nf]",
+  "usage: cc-check [--help|nf|type]",
   "  --help : display this message",
-  "  nf     : read expression from stdin, print its normal form"
+  "  nf     : read & typecheck expression from stdin, print its normal form and type",
+  "  type   : read & typecheck expression from stdin, print its type"
   ]
 
+
+
 mainWith : IO (List String) -> IO RawTerm -> IO ()
 mainWith getOpt getTerm = do
-  [_, "nf"] <- getOpt
-    | [_, "--help"] => putStrLn helpMsg
-    | _ => putErrLn helpMsg >> exitFailure
-  rawTerm <- getTerm
-  let Right term = runNameError $ translate [<] rawTerm
-    | Left errs => for_ errs putErr >> exitFailure
-  let nf : Term [<] = normalise [<] term
-  putDoc (pretty nf)
+  opts <- getOpt
+  case opts of
+    [_, "--help"] => putStrLn helpMsg
+    [_, "nf"] => do
+      rawTerm <- getTerm
+      let Right (t, ty) = runElabError $ inferTerm rawTerm
+        | Left errs => for_ errs putErr >> exitFailure
+      let nf : Term [<] = normalise [<] t
+      let ty = quote ty
+      putDoc (group $ pretty nf <++> colon <+> line <+> pretty ty)
+    [_, "type"] => do
+      rawTerm <- getTerm
+      let Right (t, ty) = runElabError $ inferTerm rawTerm
+        | Left errs => for_ errs putErr >> exitFailure
+      putDoc (group $ pretty $ quote ty)
+    _ => putErrLn helpMsg >> exitFailure
   where
-  putErr : Name -> IO ()
-  putErr n = putBoundErrLn (bounds n) "undefined name: \{n}"
+  putErr : Either Name (String, Maybe Bounds) -> IO ()
+  putErr (Left n) = putBoundErrLn (bounds n) "undefined name: \{n}"
+  putErr (Right (s, bounds)) = putBoundErrLn bounds s
 
 partial
 main : IO ()