From ff4c5f15f354aa8da7bb5868d913dbbef23832a3 Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Sun, 18 Dec 2022 16:36:09 +0000 Subject: Add dependent products. --- src/Obs/Abstract.idr | 25 ++++++++++++++++++------- 1 file changed, 18 insertions(+), 7 deletions(-) (limited to 'src/Obs/Abstract.idr') 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) -- cgit v1.2.3