Add type checking.HEADmaster

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

5 files changed, 476 insertions, 67 deletions

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