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

Safe HaskellNone
LanguageHaskell2010

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, MonadCatch m, MonadUnique m) => Rewrite c m CoreExpr Source

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

caseFloatArgR Source

Arguments

:: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, BoundVars c, HasDynFlags m, HasHermitMEnv m, LiftCoreM m, MonadCatch m, MonadIO m, MonadThings m, MonadUnique m) 
=> Maybe CoreExpr 
-> Maybe (Rewrite c m CoreExpr)

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

-> Rewrite c m CoreExpr 

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

caseFloatArgLemmaR :: (AddBindings c, ExtendPath c Crumb, HasCoreRules c, LemmaContext c, ReadBindings c, ReadPath c Crumb, HasHermitMEnv m, LiftCoreM m, HasDynFlags m, HasLemmas m, MonadCatch m, MonadIO m, MonadThings m, MonadUnique m) => Used -> LemmaName -> Rewrite c m CoreExpr Source

f (case s of alt1 -> e1; alt2 -> e2) ==> case s of alt1 -> f e1; alt2 -> f e2 Only safe if f is strict, so introduces a lemma to prove.

caseFloatCaseR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, ReadBindings c, MonadCatch m, MonadUnique m) => Rewrite c m CoreExpr Source

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 CoreExpr Source

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, MonadCatch m, MonadUnique m) => Rewrite c m CoreExpr Source

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, MonadCatch m, MonadUnique m) => Rewrite c m CoreExpr Source

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

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

Float in a Case whatever the context.

caseFloatInAppR :: Monad m => Rewrite c m CoreExpr Source

Unimplemented!

caseReduceR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, ReadBindings c, MonadCatch m, MonadUnique m) => Bool -> Rewrite c m CoreExpr Source

Case of Known Constructor. Eliminate a case if the scrutinee is a data constructor or a literal. If first argument is True, perform substitution in RHS, if False, build let expressions.

caseReduceDataconR :: forall c m. (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, ReadBindings c, MonadCatch m, MonadUnique m) => Bool -> Rewrite c m CoreExpr Source

Case of Known Constructor. Eliminate a case if the scrutinee is a data constructor. If first argument is True, perform substitution in RHS, if False, build let expressions.

caseReduceLiteralR :: MonadCatch m => Bool -> Rewrite c m CoreExpr Source

Case of Known Constructor. Eliminate a case if the scrutinee is a literal. If first argument is True, perform substitution in RHS, if False, build let expressions. NB: LitAlt cases don't do evaluation

caseReduceUnfoldR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, ReadBindings c, HasEmptyContext c, MonadCatch m, MonadUnique m) => Bool -> Rewrite c m CoreExpr Source

Unfold the case scrutinee and then perform case reduction. If first argument is True, perform substitution in RHS, if False, build let expressions.

caseSplitR :: forall c m. (AddBindings c, BoundVars c, ExtendPath c Crumb, HasEmptyContext c, ReadPath c Crumb, MonadCatch m, MonadUnique m) => CoreExpr -> Rewrite c m CoreExpr Source

Case split on an arbitrary scrutinee s. All free variables in s should be in scope.

E.g. If s has type [a], then case-split s:

e ==> case s of w [] -> e[w/s] (a:as) -> e[w/s]

Note that occurrences of s in e are replaced with the case binder.

caseSplitInlineR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, ReadBindings c, HasEmptyContext c, MonadCatch m, MonadUnique m) => CoreExpr -> Rewrite c m CoreExpr Source

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

caseSplitInline idPred = caseSplit idPred >>> caseInlineAlternativeR

caseInlineScrutineeR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, ReadBindings c, HasEmptyContext c, MonadCatch m, MonadUnique m) => Rewrite c m CoreExpr Source

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

caseInlineAlternativeR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, ReadBindings c, HasEmptyContext c, MonadCatch m, MonadUnique m) => Rewrite c m CoreExpr Source

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

caseMergeAltsR :: MonadCatch m => Rewrite c m CoreExpr Source

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}

caseMergeAltsWithBinderR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, ReadBindings c, HasEmptyContext c, MonadCatch m, MonadUnique m) => Rewrite c m CoreExpr Source

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

caseElimR :: MonadCatch m => Rewrite c m CoreExpr Source

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, HasEmptyContext c, MonadCatch m, MonadUnique m) => Rewrite c m CoreExpr Source

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

caseElimMergeAltsR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, ReadBindings c, HasEmptyContext c, MonadCatch m, MonadUnique m) => Rewrite c m CoreExpr Source

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

caseIntroSeqR :: (MonadCatch m, MonadUnique m) => (Id -> Bool) -> Rewrite c m CoreExpr Source

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, HasEmptyContext c, MonadCatch m, MonadUnique m) => Rewrite c m CoreExpr Source

Eliminate a case that corresponds to a pointless seq.