Add dependent products.

1 files changed, 18 insertions, 7 deletions

diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr
index 1b72965..0915152 100644
--- a/src/Obs/Abstract.idr
+++ b/src/Obs/Abstract.idr
@@ -33,18 +33,29 @@ printErr (Right x) = pure x
 
 export
 abstractSyntax : Context n -> Syntax -> Error (Term n)
-abstractSyntax ctx (Var b str) = do
-  let Just i = lookup str ctx
-    | Nothing => report b "unbound variable: \{str}"
-  pure (Var b i)
-abstractSyntax ctx (Sort b s) = pure (Sort b s)
+abstractSyntax ctx (Var var) = do
+  let Just i = lookup var.val ctx
+    | Nothing => report var.bounds "unbound variable: \{var.val}"
+  pure (Var var i)
+abstractSyntax ctx (Sort bounds s) = pure (Sort bounds s)
+abstractSyntax ctx (Pi bounds var a b) = do
+  a <- abstractSyntax ctx a
+  b <- abstractSyntax (bind ctx var.val) b
+  pure (Pi bounds var.val a b)
+abstractSyntax ctx (Lambda bounds var t) = do
+  t <- abstractSyntax (bind ctx var.val) t
+  pure (Lambda bounds var.val t)
+abstractSyntax ctx (App t u) = do
+  t <- abstractSyntax ctx t
+  u <- abstractSyntax ctx u
+  pure (App t u)
 abstractSyntax ctx (Top b) = pure (Top b)
 abstractSyntax ctx (Point b) = pure (Point b)
 abstractSyntax ctx (Bottom b) = pure (Bottom b)
-abstractSyntax ctx (Absurd b a t) = do
+abstractSyntax ctx (Absurd bounds a t) = do
   a <- abstractSyntax ctx a
   t <- abstractSyntax ctx t
-  pure (Absurd b a t)
+  pure (Absurd bounds a t)
 
 export
 abstractDefinition : Context n -> Definition -> Error (Definition n)