Improve parsing.

1 files changed, 62 insertions, 59 deletions

diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr
index 9215dda..b8fca7b 100644
--- a/src/Obs/Abstract.idr
+++ b/src/Obs/Abstract.idr
@@ -18,74 +18,77 @@ Context n = List (String, Fin n)
 bind : Context n -> String -> Context (S n)
 bind ctx str = (str, 0) :: map (mapSnd FS) ctx
 
-export
 abstractSyntax : Context n -> Syntax -> Logging ann (Term n)
+abstractSyntaxBounds : Context n -> WithBounds Syntax -> Logging ann (WithBounds (Term n))
+
 abstractSyntax ctx (Var var) = do
-  let Just i = lookup var.val ctx
+  let Just i = lookup var ctx
     | Nothing => inScope "unbound variable" $ fatal var
   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 (Sort s) = pure (Sort s)
+abstractSyntax ctx (Pi var a b) = do
+  a <- abstractSyntaxBounds ctx a
+  b <- abstractSyntaxBounds (bind ctx var.val) b
+  pure (Pi var a b)
+abstractSyntax ctx (Lambda var t) = do
+  t <- abstractSyntaxBounds (bind ctx var.val) t
+  pure (Lambda var t)
 abstractSyntax ctx (App t u) = do
-  t <- abstractSyntax ctx t
-  u <- abstractSyntax ctx u
+  t <- abstractSyntaxBounds ctx t
+  u <- abstractSyntaxBounds ctx u
   pure (App t u)
-abstractSyntax ctx (Sigma bounds var a b) = do
-  a <- abstractSyntax ctx a
-  b <- abstractSyntax (bind ctx var.val) b
-  pure (Sigma bounds var.val a b)
-abstractSyntax ctx (Pair b t u) = do
-  t <- abstractSyntax ctx t
-  u <- abstractSyntax ctx u
-  pure (Pair b t u)
-abstractSyntax ctx (Fst b t) = do
-  t <- abstractSyntax ctx t
-  pure (Fst b t)
-abstractSyntax ctx (Snd b t) = do
-  t <- abstractSyntax ctx t
-  pure (Snd b t)
-abstractSyntax ctx (Top b) = pure (Top b)
-abstractSyntax ctx (Point b) = pure (Point b)
-abstractSyntax ctx (Bottom b) = pure (Bottom b)
-abstractSyntax ctx (Absurd bounds a t) = do
-  a <- abstractSyntax ctx a
-  t <- abstractSyntax ctx t
-  pure (Absurd bounds a t)
-abstractSyntax ctx (Equal bounds t u) = do
-  t <- abstractSyntax ctx t
-  u <- abstractSyntax ctx u
-  pure (Equal bounds t u)
-abstractSyntax ctx (Refl bounds t) = do
-  t <- abstractSyntax ctx t
-  pure (Refl bounds t)
-abstractSyntax ctx (Transp bounds t b u t' e) = do
-  t <- abstractSyntax ctx t
-  b <- abstractSyntax ctx b
-  u <- abstractSyntax ctx u
-  t' <- abstractSyntax ctx t'
-  e <- abstractSyntax ctx e
-  pure (Transp bounds t b u t' e)
-abstractSyntax ctx (Cast bounds b e t) = do
-  b <- abstractSyntax ctx b
-  e <- abstractSyntax ctx e
-  t <- abstractSyntax ctx t
-  pure (Cast bounds b e t)
-abstractSyntax ctx (CastId bounds t) = do
-  t <- abstractSyntax ctx t
-  pure (CastId bounds t)
+abstractSyntax ctx (Sigma var a b) = do
+  a <- abstractSyntaxBounds ctx a
+  b <- abstractSyntaxBounds (bind ctx var.val) b
+  pure (Sigma var a b)
+abstractSyntax ctx (Pair t u) = do
+  t <- abstractSyntaxBounds ctx t
+  u <- abstractSyntaxBounds ctx u
+  pure (Pair t u)
+abstractSyntax ctx (Fst t) = do
+  t <- abstractSyntaxBounds ctx t
+  pure (Fst t)
+abstractSyntax ctx (Snd t) = do
+  t <- abstractSyntaxBounds ctx t
+  pure (Snd t)
+abstractSyntax ctx Top = pure Top
+abstractSyntax ctx Point = pure Point
+abstractSyntax ctx Bottom = pure Bottom
+abstractSyntax ctx (Absurd a t) = do
+  a <- abstractSyntaxBounds ctx a
+  t <- abstractSyntaxBounds ctx t
+  pure (Absurd a t)
+abstractSyntax ctx (Equal t u) = do
+  t <- abstractSyntaxBounds ctx t
+  u <- abstractSyntaxBounds ctx u
+  pure (Equal t u)
+abstractSyntax ctx (Refl t) = do
+  t <- abstractSyntaxBounds ctx t
+  pure (Refl t)
+abstractSyntax ctx (Transp t b u t' e) = do
+  t <- abstractSyntaxBounds ctx t
+  b <- abstractSyntaxBounds ctx b
+  u <- abstractSyntaxBounds ctx u
+  t' <- abstractSyntaxBounds ctx t'
+  e <- abstractSyntaxBounds ctx e
+  pure (Transp t b u t' e)
+abstractSyntax ctx (Cast b e t) = do
+  b <- abstractSyntaxBounds ctx b
+  e <- abstractSyntaxBounds ctx e
+  t <- abstractSyntaxBounds ctx t
+  pure (Cast b e t)
+abstractSyntax ctx (CastId t) = do
+  t <- abstractSyntaxBounds ctx t
+  pure (CastId t)
+
+abstractSyntaxBounds ctx (MkBounded v irrel bnds) =
+  pure $ MkBounded !(abstractSyntax ctx v) irrel bnds
 
 abstractDefinition : Context n -> Definition -> Logging ann (Definition n)
 abstractDefinition ctx def = pure $ MkDefinition
   { name = def.name
-  , bounds = def.bounds
-  , ty = !(abstractSyntax ctx def.ty)
-  , tm = !(abstractSyntax ctx def.tm)
+  , ty = !(abstractSyntaxBounds ctx def.ty)
+  , tm = !(abstractSyntaxBounds ctx def.tm)
   }
 
 export
@@ -93,7 +96,7 @@ abstractBlock : (defs : List Definition) -> Logging ann (Block (length defs))
 abstractBlock defs =
   let asContext : Block n -> Context n
       asContext []            = []
-      asContext (defs :< def) = bind (asContext defs) def.name
+      asContext (defs :< def) = bind (asContext defs) def.name.val
   in let helper : Block n -> (defs : List Definition) -> Logging ann (Block (length defs + n))
          helper blk []            = pure blk
          helper blk (def :: defs) = do