diff options
Diffstat (limited to 'src/Obs/Abstract.idr')
| -rw-r--r-- | src/Obs/Abstract.idr | 20 |
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 |