hermit-1.0.0.0: Haskell Equational Reasoning Model-to-Implementation Tunnel

Safe HaskellNone
LanguageHaskell2010

HERMIT.Dictionary.WorkerWrapper.Fix

Contents

Synopsis

The Worker/Wrapper Transformation

Note that many of these operations require fix to be in scope.

externals :: [External] Source

Externals for manipulating fixed points, and for the worker/wrapper transformation.

wwFacBR :: Maybe WWAssumption -> CoreExpr -> CoreExpr -> BiRewriteH CoreExpr Source

For any f :: A -> A, and given wrap :: B -> A and unwrap :: A -> B as arguments, then fix A f <==> wrap (fix B (\ b -> unwrap (f (wrap b))))

wwSplitR :: Maybe WWAssumption -> CoreExpr -> CoreExpr -> RewriteH CoreDef Source

\ wrap unwrap -> (prog = expr ==> prog = let f = \ prog -> expr in let work = unwrap (f (wrap work)) in wrap work)

wwSplitStaticArg :: Int -> [Int] -> Maybe WWAssumption -> CoreString -> CoreString -> RewriteH CoreDef Source

As wwSplit but performs the static-argument transformation for n static arguments first, and optionally provides some of those arguments (specified by index) to all calls of wrap and unwrap. This is useful if, for example, the expression, and wrap and unwrap, all have a forall type.

wwGenerateFusionT :: Maybe WWAssumption -> TransformH LCore () Source

Save the recursive definition of work in the stash, so that we can later verify uses of wwFusionBR. Must be applied to a definition of the form: work = unwrap (f (wrap work)) Note that this is performed automatically as part of wwSplitR.

wwFusionBR :: BiRewriteH CoreExpr Source

Given wrap :: B -> A, unwrap :: A -> B and work :: B as arguments, then unwrap (wrap work) <==> work

wwAssA Source

Arguments

:: Maybe (RewriteH CoreExpr)

WW Assumption A

-> CoreExpr

wrap

-> CoreExpr

unwrap

-> BiRewriteH CoreExpr 

wrap (unwrap a) <==> a

wwAssB Source

Arguments

:: Maybe (RewriteH CoreExpr)

WW Assumption B

-> CoreExpr

wrap

-> CoreExpr

unwrap

-> CoreExpr

f

-> BiRewriteH CoreExpr 

wrap (unwrap (f a)) <==> f a

wwAssC Source

Arguments

:: Maybe (RewriteH CoreExpr)

WW Assumption C

-> CoreExpr

wrap

-> CoreExpr

unwrap

-> CoreExpr

f

-> BiRewriteH CoreExpr 

fix A ( a -> wrap (unwrap (f a))) <==> fix A f