Add type checking.HEADmaster

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

1 files changed, 21 insertions, 10 deletions

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