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

Safe HaskellNone

HERMIT.Dictionary.Local.Let

Contents

Synopsis

Rewrites on Let Expressions

externals :: [External]Source

Externals relating to Let expressions.

Let Elimination

letNonRecSubstR :: MonadCatch m => Rewrite c m CoreExprSource

Let (NonRec v e) body ==> body[e/v]

letNonRecSubstSafeR :: forall c m. (AddBindings c, ExtendPath c Crumb, ReadBindings c, MonadCatch m) => Rewrite c m CoreExprSource

Currently we always substitute types and coercions, and use a heuristic to decide whether to substitute expressions. This may need revisiting.

letSubstR :: (AddBindings c, ExtendPath c Crumb, MonadCatch m) => Rewrite c m CoreExprSource

(let x = e1 in e2) ==> (e2[e1/x]), (x must not be free in e1)

letSubstSafeR :: (AddBindings c, ExtendPath c Crumb, ReadBindings c, MonadCatch m) => Rewrite c m CoreExprSource

As letNonRecSubstSafeR, but attempting to convert a singleton recursive binding to a non-recursive binding first.

letNonRecElimR :: MonadCatch m => Rewrite c m CoreExprSource

Remove an unused non-recursive let binding. let v = E1 in E2 ==> E2, if v is not free in E2

letRecElimR :: MonadCatch m => Rewrite c m CoreExprSource

Remove all unused recursive let bindings in the current group.

Let Introduction

letIntroR :: String -> Rewrite c HermitM CoreExprSource

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

Let Floating

letFloatAppR :: (ExtendPath c Crumb, AddBindings c, BoundVars c) => Rewrite c HermitM CoreExprSource

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

letFloatArgR :: (ExtendPath c Crumb, AddBindings c, BoundVars c) => Rewrite c HermitM CoreExprSource

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

letFloatLetR :: (ExtendPath c Crumb, AddBindings c, BoundVars c) => Rewrite c HermitM CoreExprSource

let v = (let bds in e1) in e2 ==> let bds in let v = e1 in e2

letFloatLamR :: (ExtendPath c Crumb, AddBindings c, BoundVars c) => Rewrite c HermitM CoreExprSource

( v -> let binds in e2) ==> let binds in ( v1 -> e2) Fails if v occurs in the RHS of binds. If v is shadowed in binds, then v will be alpha-renamed.

letFloatCaseR :: (ExtendPath c Crumb, AddBindings c, BoundVars c) => Rewrite c HermitM 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.

letFloatCastR :: MonadCatch m => Rewrite c m CoreExprSource

cast (let bnds in e) co ==> let bnds in cast e co

letFloatExprR :: (ExtendPath c Crumb, AddBindings c, BoundVars c) => Rewrite c HermitM CoreExprSource

Float a Let through an expression, whatever the context.

Let Unfloating

letUnfloatR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m CoreExprSource

Unfloat a Let if possible.

letUnfloatAppR :: MonadCatch m => Rewrite c m CoreExprSource

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

letUnfloatCaseR :: MonadCatch m => Rewrite c m CoreExprSource

let v = ev in case s of p -> e ==> case (let v = ev in s) of p -> let v = ev in e, if v does not shadow a pattern binder in p

letUnfloatLamR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m CoreExprSource

let v = ev in x -> e ==> x -> let v = ev in e if v does not shadow x

Miscallaneous

reorderNonRecLetsR :: MonadCatch m => [Name] -> Rewrite c m CoreExprSource

Re-order a sequence of nested non-recursive let bindings. The argument list should contain the let-bound variables, in the desired order.

letTupleR :: String -> Rewrite c HermitM CoreExprSource

Combine nested non-recursive lets into case of a tuple. E.g. let {v1 = e1 ; v2 = e2 ; v3 = e3} in body ==> case (e1,e2,e3) of {(v1,v2,v3) -> body}

letToCaseR :: (ExtendPath c Crumb, AddBindings c, ReadBindings c) => Rewrite c HermitM CoreExprSource

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