From eb49ef28b93431d9694a17b1ad44d9ea966bcb05 Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Sat, 7 Jan 2023 22:01:05 +0000 Subject: Add postulates. --- src/Obs/Abstract.idr | 20 ++++++++++++++++---- 1 file changed, 16 insertions(+), 4 deletions(-) (limited to 'src/Obs/Abstract.idr') 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 -- cgit v1.2.3