Safe Haskell | None |
---|

- 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
- wwResultGenerateFusionR :: Maybe WWAssumption -> RewriteH Core
- 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 for manipulating fixed points, and for the worker/wrapper transformation.

wwResultFacBR :: Maybe WWAssumption -> CoreExpr -> CoreExpr -> BiRewriteH CoreExprSource

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 CoreDefSource

\ 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 CoreDefSource

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.

wwResultGenerateFusionR :: Maybe WWAssumption -> RewriteH CoreSource

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 CoreExprSource

Given `abs :: B -> A`

, `rep :: A -> B`

and `work :: X -> B`

as arguments, then
`rep (abs (work x))`

<==> `work x`

`abs (rep a)`

<==> `a`

:: Maybe (RewriteH CoreExpr) | WW Assumption B |

-> CoreExpr | abs |

-> CoreExpr | rep |

-> CoreExpr | f |

-> BiRewriteH CoreExpr |

`abs (rep (f h x))`

<==> `f h x`