hermit- Haskell Equational Reasoning Model-to-Implementation Tunnel

Safe HaskellNone




Rewrites on Case Expressions

externals :: [External]Source

Externals relating to Case expressions.

letFloatCase :: RewriteH CoreExprSource

case (let v = e1 in e2) of alts ==> let v = e1 in case e2 of alts

caseFloatApp :: RewriteH CoreExprSource

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

caseFloatArg :: RewriteH CoreExprSource

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

caseFloatCase :: RewriteH 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

caseFloatLet :: RewriteH CoreExprSource

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

caseFloat :: RewriteH CoreExprSource

Float a Case whatever the context.

caseReduce :: RewriteH CoreExprSource

Case-of-known-constructor rewrite.

caseSplit :: Name -> RewriteH CoreExprSource

Case split a free variable in an expression:

Assume expression e which mentions x :: [a]

e ==> case x of x [] -> e (a:b) -> e

caseSplitInline :: Name -> RewriteH CoreSource

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

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