Add dependent products.

1 files changed, 35 insertions, 12 deletions

diff --git a/src/Obs/Term.idr b/src/Obs/Term.idr
index 05b9a7f..366a4b7 100644
--- a/src/Obs/Term.idr
+++ b/src/Obs/Term.idr
@@ -12,9 +12,13 @@ import Text.PrettyPrint.Prettyprinter
 
 public export
 data Term : Nat -> Type where
-  Var    : Bounds -> Fin n -> Term n
+  Var    : WithBounds String -> Fin n -> Term n
   -- Sorts
   Sort   : Bounds -> Sort -> Term n
+  -- Dependent Product
+  Pi     : Bounds -> String -> Term n -> Term (S n) -> Term n
+  Lambda : Bounds -> String -> Term (S n) -> Term n
+  App    : Term n -> Term n -> Term n
   -- True
   Top    : Bounds -> Term n
   Point  : Bounds -> Term n
@@ -39,23 +43,42 @@ data Block : Nat -> Type where
 
 export
 fullBounds : Term n -> WithBounds (Term n)
-fullBounds tm@(Var x i)      = MkBounded tm False x
-fullBounds tm@(Sort x s)     = MkBounded tm False x
-fullBounds tm@(Top x)        = MkBounded tm False x
-fullBounds tm@(Point x)      = MkBounded tm False x
-fullBounds tm@(Bottom x)     = MkBounded tm False x
+fullBounds tm@(Var var i) = map (\_ => tm) var
+fullBounds tm@(Sort x s) = MkBounded tm False x
+fullBounds tm@(Pi x var a b) = mergeBounds (mergeBounds (fullBounds a) (fullBounds b)) (MkBounded tm False x)
+fullBounds tm@(Lambda x var t) = mergeBounds (fullBounds t) (MkBounded tm False x)
+fullBounds tm@(App t u) = map (\_ => tm) (mergeBounds (fullBounds t) (fullBounds u))
+fullBounds tm@(Top x) = MkBounded tm False x
+fullBounds tm@(Point x) = MkBounded tm False x
+fullBounds tm@(Bottom x) = MkBounded tm False x
 fullBounds tm@(Absurd x a t) = mergeBounds (mergeBounds (fullBounds a) (fullBounds t)) (MkBounded tm False x)
 
 -- Pretty Print ----------------------------------------------------------------
 
 export
 Pretty (Term n) where
-  prettyPrec d (Var x i) = pretty "$\{show i}"
-  prettyPrec d (Sort x s) = prettyPrec d s
-  prettyPrec d (Top x) = pretty "()"
-  prettyPrec d (Point x) = pretty "*"
-  prettyPrec d (Bottom x) = pretty "Void"
-  prettyPrec d (Absurd x a t) =
+  prettyPrec d (Var var _) = pretty var.val
+  prettyPrec d (Sort _ s) = prettyPrec d s
+  prettyPrec d (Pi _ var a b) =
+    parenthesise (d > Open) $
+    group $
+    parens (pretty var <++> colon <+> softline <+> prettyPrec Open a) <++>
+    pretty "->" <+> softline <+>
+    prettyPrec Open b
+  prettyPrec d (Lambda _ var t) =
+    parenthesise (d > Open) $
+    group $
+    backslash <+> pretty var <++>
+    pretty "=>" <+> softline <+>
+    prettyPrec Open t
+  prettyPrec d (App t u) =
+    parenthesise (d >= App) $
+    group $
+    fillSep [prettyPrec Open t, prettyPrec App u]
+  prettyPrec d (Top _) = pretty "()"
+  prettyPrec d (Point _) = pretty "*"
+  prettyPrec d (Bottom _) = pretty "Void"
+  prettyPrec d (Absurd _ a t) =
     parenthesise (d > Open) $
     group $
     fillSep [pretty "absurd", prettyPrec App a, prettyPrec App t]