Add postulates.

1 files changed, 16 insertions, 4 deletions

diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr
index 25c4210..16b0c92 100644
--- a/src/Obs/Abstract.idr
+++ b/src/Obs/Abstract.idr
@@ -132,6 +132,12 @@ abstractSyntaxBounds ctx val@(MkBounded v irrel bnds) = do
   term <- inBounds $ (MkBounded (abstractSyntax ctx v) irrel bnds)
   pure $ map (const term) val
 
+abstractParameter : Context n -> Parameter -> Logging ann (Parameter n)
+abstractParameter ctx param = pure $ MkParameter
+  { name = param.name
+  , ty = !(abstractSyntaxBounds ctx param.ty)
+  }
+
 abstractDefinition : Context n -> Definition -> Logging ann (Definition n)
 abstractDefinition ctx def = pure $ MkDefinition
   { name = def.name
@@ -140,14 +146,20 @@ abstractDefinition ctx def = pure $ MkDefinition
   }
 
 export
-abstractBlock : (defs : List Definition) -> Logging ann (Block (length defs))
+abstractBlock : (defs : List (Either Parameter Definition)) -> Logging ann (Block (length defs))
 abstractBlock defs =
   let asContext : Block n -> Context n
       asContext []            = []
-      asContext (defs :< def) = bind (asContext defs) def.name.val
-  in let helper : Block n -> (defs : List Definition) -> Logging ann (Block (length defs + n))
+      asContext (blk :< def) = bind (asContext blk) def.name.val
+      asContext (blk ::< param) = bind (asContext blk) param.name.val
+  in let helper : Block n ->
+           (defs : List (Either Parameter Definition)) ->
+           Logging ann (Block (length defs + n))
          helper blk []            = pure blk
-         helper blk (def :: defs) = do
+         helper blk (Left param :: defs) = do
+           param <- abstractParameter (asContext blk) param
+           (rewrite plusSuccRightSucc (length defs) n in helper (blk ::< param) defs)
+         helper blk (Right def :: defs) = do
            def <- abstractDefinition (asContext blk) def
            (rewrite plusSuccRightSucc (length defs) n in helper (blk :< def) defs)
   in rewrite sym $ plusZeroRightNeutral (length defs) in helper [] defs