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

Safe HaskellNone

HERMIT.Dictionary.Local.Case

Contents

Synopsis

Rewrites on Case Expressions

externals :: [External]Source

Externals relating to Case expressions.

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

(case s of alt1 -> e1; alt2 -> e2) v ==> case s of alt1 -> e1 v; alt2 -> e2 v

caseFloatArgRSource

Arguments

:: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, BoundVars c, HasGlobalRdrEnv c) 
=> Maybe (CoreExpr, Maybe (Rewrite c HermitM CoreExpr))

Maybe the function to float past, and maybe a proof of its strictness.

-> Rewrite c HermitM CoreExpr 

f (case s of alt1 -> e1; alt2 -> e2) ==> case s of alt1 -> f e1; alt2 -> f e2 Only safe if f is strict.

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

case (case s1 of alt11 -> e11; alt12 -> e12) of alt21 -> e21; alt22 -> e22 ==> case s1 of alt11 -> case e11 of alt21 -> e21; alt22 -> e22 alt12 -> case e12 of alt21 -> e21; alt22 -> e22

caseFloatCastR :: MonadCatch m => Rewrite c m CoreExprSource

cast (case s of p -> e) co ==> case s of p -> cast e co

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

let v = case s of alt1 -> e1 in e ==> case s of alt1 -> let v = e1 in e

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

caseFloatR = caseFloatAppR <+ caseFloatCaseR <+ caseFloatLetR <+ caseFloatCastR Note: does NOT include caseFloatArg

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

Float in a Case whatever the context.

caseFloatInAppR :: Monad m => Rewrite c m CoreExprSource

Unimplemented!

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

Case of Known Constructor. Eliminate a case if the scrutinee is a data constructor or a literal.

caseReduceDataconR :: forall c. (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, ReadBindings c) => Rewrite c HermitM CoreExprSource

Case of Known Constructor. Eliminate a case if the scrutinee is a data constructor.

caseReduceLiteralR :: MonadCatch m => Rewrite c m CoreExprSource

Case of Known Constructor. Eliminate a case if the scrutinee is a literal. NB: LitAlt cases don't do evaluation

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

Inline the case scrutinee (if it is an identifier), and then perform case reduction.

caseSplitR :: Name -> Rewrite c HermitM CoreExprSource

Case split a free identifier in an expression:

E.g. Assume expression e which mentions i :: [a]

e ==> case i of i [] -> e (a:as) -> e

caseSplitInlineR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, ReadBindings c) => Name -> Rewrite c HermitM CoreSource

Like caseSplit, but additionally inlines the constructor applications for each occurance of the named variable.

 caseSplitInline nm = caseSplit nm >>> anybuR (inlineName nm)

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

Inline the case wildcard binder as the case scrutinee everywhere in the case alternatives.

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

Inline the case wildcard binder as the case-alternative pattern everywhere in the case alternatives.

caseMergeAltsR :: MonadCatch m => Rewrite c m CoreExprSource

Merge all case alternatives into a single default case. The RHS of each alternative must be the same. case s of {pat1 -> e ; pat2 -> e ; ... ; patn -> e} ==> case s of {_ -> e}

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

A cleverer version of mergeCaseAlts that first attempts to abstract out any occurrences of the alternative pattern using the wildcard binder.

caseElimR :: Rewrite c HermitM CoreExprSource

case s of w; C vs -> e ==> e if w and vs are not free in e

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

Eliminate a case, inlining any occurrences of the case binder as the scrutinee.

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

Eliminate a case, merging the case alternatives into a single default alternative and inlining the case binder as the scrutinee (if possible).

caseIntroSeqR :: Name -> Rewrite c HermitM CoreExprSource

Force evaluation of an identifier by introducing a case. This is equivalent to adding (seq v) in the source code.

e -> case v of v _ -> e

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

Eliminate a case that corresponds to a pointless seq.