| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
HERMIT.Dictionary.WorkerWrapper.FixResult
- externals :: [External]
- wwResultFacBR :: Maybe WWAssumption -> CoreExpr -> CoreExpr -> BiRewriteH CoreExpr
- wwResultSplitR :: Maybe WWAssumption -> CoreExpr -> CoreExpr -> RewriteH CoreDef
- wwResultSplitStaticArg :: Int -> [Int] -> Maybe WWAssumption -> CoreString -> CoreString -> RewriteH CoreDef
- wwResultGenerateFusionT :: Maybe WWAssumption -> TransformH LCore ()
- wwResultFusionBR :: BiRewriteH CoreExpr
- wwResultAssA :: Maybe (RewriteH CoreExpr) -> CoreExpr -> CoreExpr -> BiRewriteH CoreExpr
- wwResultAssB :: Maybe (RewriteH CoreExpr) -> CoreExpr -> CoreExpr -> CoreExpr -> BiRewriteH CoreExpr
- wwResultAssC :: Maybe (RewriteH CoreExpr) -> CoreExpr -> CoreExpr -> CoreExpr -> BiRewriteH CoreExpr
The Worker/Wrapper Transformation (Result Variant)
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.
wwResultFacBR :: Maybe WWAssumption -> CoreExpr -> CoreExpr -> BiRewriteH CoreExpr Source
For any f :: (X -> A) -> (X -> A), and given abs :: B -> A and rep :: A -> B as arguments, then
fix A f <==> \ x1 -> abs (fix (X->B) (\ h x2 -> rep (f (\ x3 -> abs (h x3)) x2)) x1)
wwResultSplitR :: Maybe WWAssumption -> CoreExpr -> CoreExpr -> RewriteH CoreDef Source
\ abs rep -> (prog = expr ==> prog = let f = \ prog -> expr in let work = \ x1 -> rep (f (\ x2 -> abs (work x2)) x1) in \ x0 -> abs (work x0))
wwResultSplitStaticArg :: 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 abs and rep.
This is useful if, for example, the expression, and abs and rep, all have a forall type.
wwResultGenerateFusionT :: Maybe WWAssumption -> TransformH LCore () Source
Save the recursive definition of work in the stash, so that we can later verify uses of wwResultFusionBR.
Must be applied to a definition of the form: work = \ x1 -> rep (f (\ x2 -> abs (work x2)) x1)
Note that this is performed automatically as part of wwResultSplitR.
wwResultFusionBR :: BiRewriteH CoreExpr Source
Given abs :: B -> A, rep :: A -> B and work :: X -> B as arguments, then
rep (abs (work x)) <==> work x
Arguments
| :: Maybe (RewriteH CoreExpr) | WW Assumption A |
| -> CoreExpr | abs |
| -> CoreExpr | rep |
| -> BiRewriteH CoreExpr |
abs (rep a) <==> a
Arguments
| :: Maybe (RewriteH CoreExpr) | WW Assumption B |
| -> CoreExpr | abs |
| -> CoreExpr | rep |
| -> CoreExpr | f |
| -> BiRewriteH CoreExpr |
abs (rep (f h x)) <==> f h x