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

Safe HaskellNone

Language.HERMIT.Primitive.Local.Let

Contents

Synopsis

Rewrites on Let Expressions

letExternals :: [External]Source

Externals relating to Let expressions.

letIntro :: Name -> RewriteH CoreExprSource

e => (let v = e in v), name of v is provided

letElim :: RewriteH CoreExprSource

Remove an unused let binding. (let v = E1 in E2) => E2, if v is not free in E2

letFloatApp :: RewriteH CoreExprSource

(let v = ev in e) x ==> let v = ev in e x

letFloatArg :: RewriteH CoreExprSource

f (let v = ev in e) ==> let v = ev in f e

letFloatLet :: RewriteH CoreExprSource

let v = (let w = ew in ev) in e ==> let w = ew in let v = ev in e

letFloatLam :: RewriteH CoreExprSource

( v1 -> let v2 = e1 in e2) ==> let v2 = e1 in ( v1 -> e2) Fails if v1 occurs in e1. If v1 = v2 then v1 will be alpha-renamed.

letFloatCase :: RewriteH CoreExprSource

case (let bnds in e) of wild alts ==> let bnds in (case e of wild alts) Fails if any variables bound in bnds occurs in alts.

letFloatExpr :: RewriteH CoreExprSource

Float a Let through an expression, whatever the context.

letFloatLetTop :: RewriteH CoreProgSource

NonRec v (Let (NonRec w ew) ev) ProgCons p ==> NonRec w ew ProgCons NonRec v ev ProgCons p

letToCase :: RewriteH CoreExprSource

let v = ev in e ==> case ev of v -> e