1 files changed, 27 insertions, 7 deletions
diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr
index 6b95910..4a7ee0c 100644
--- a/src/Obs/Syntax.idr
+++ b/src/Obs/Syntax.idr
@@ -11,9 +11,13 @@ import Text.PrettyPrint.Prettyprinter
 
 public export
 data Syntax : Type where
-  Var    : Bounds -> String -> Syntax
+  Var    : WithBounds String -> Syntax
   -- Sorts
   Sort   : Bounds -> Sort -> Syntax
+  -- Dependent Products
+  Pi     : Bounds -> WithBounds String -> Syntax -> Syntax -> Syntax
+  Lambda : Bounds -> WithBounds String -> Syntax -> Syntax
+  App    : Syntax -> Syntax -> Syntax
   -- True
   Top    : Bounds -> Syntax
   Point  : Bounds -> Syntax
@@ -33,14 +37,30 @@ record Definition where
 
 export
 Pretty Syntax where
-  prettyPrec d (Var x str) = pretty str
-  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.val <++> colon <+> softline <+> prettyPrec Open a) <++>
+    pretty "->" <+> softline <+>
+    prettyPrec Open b
+  prettyPrec d (Lambda _ var t) =
+    parenthesise (d > Open) $
+    group $
+    backslash <+> pretty var.val <++>
+    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 >= App) $
+    group $
     fillSep [pretty "absurd", prettyPrec App a, prettyPrec App t]
 
 export