Safe Haskell | None |
---|---|
Language | Haskell2010 |
HERMIT.Dictionary.Local.Case
Contents
- externals :: [External]
- caseFloatAppR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, ReadBindings c, MonadCatch m, MonadUnique m) => Rewrite c m CoreExpr
- caseFloatArgR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, BoundVars c, HasDynFlags m, HasHermitMEnv m, HasHscEnv m, MonadCatch m, MonadIO m, MonadThings m, MonadUnique m) => Maybe CoreExpr -> Maybe (Rewrite c m CoreExpr) -> Rewrite c m CoreExpr
- caseFloatArgLemmaR :: (AddBindings c, BoundVars c, ExtendPath c Crumb, ReadPath c Crumb, HasHermitMEnv m, HasHscEnv m, HasDynFlags m, HasLemmas m, MonadCatch m, MonadIO m, MonadThings m, MonadUnique m) => LemmaName -> Rewrite c m CoreExpr
- caseFloatCaseR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, ReadBindings c, MonadCatch m, MonadUnique m) => Rewrite c m CoreExpr
- caseFloatCastR :: MonadCatch m => Rewrite c m CoreExpr
- caseFloatLetR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, ReadBindings c, MonadCatch m, MonadUnique m) => Rewrite c m CoreExpr
- caseFloatR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, ReadBindings c, MonadCatch m, MonadUnique m) => Rewrite c m CoreExpr
- caseFloatInR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m CoreExpr
- caseFloatInAppR :: Monad m => Rewrite c m CoreExpr
- caseFloatInArgsR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m CoreExpr
- caseReduceR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, ReadBindings c, MonadCatch m, MonadUnique m) => Bool -> Rewrite c m CoreExpr
- caseReduceDataconR :: forall c m. (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, ReadBindings c, MonadCatch m, MonadUnique m) => Bool -> Rewrite c m CoreExpr
- caseReduceLiteralR :: MonadCatch m => Bool -> Rewrite c m CoreExpr
- caseReduceUnfoldR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, ReadBindings c, HasEmptyContext c, MonadCatch m, MonadUnique m) => Bool -> Rewrite c m CoreExpr
- caseSplitR :: (MonadCatch m, MonadUnique m) => (Id -> Bool) -> Rewrite c m CoreExpr
- caseSplitInlineR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, ReadBindings c, HasEmptyContext c, MonadCatch m, MonadUnique m) => (Id -> Bool) -> Rewrite c m CoreExpr
- caseInlineScrutineeR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, ReadBindings c, HasEmptyContext c, MonadCatch m, MonadUnique m) => Rewrite c m CoreExpr
- caseInlineAlternativeR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, ReadBindings c, HasEmptyContext c, MonadCatch m, MonadUnique m) => Rewrite c m CoreExpr
- caseMergeAltsR :: MonadCatch m => Rewrite c m CoreExpr
- caseMergeAltsWithBinderR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, ReadBindings c, HasEmptyContext c, MonadCatch m, MonadUnique m) => Rewrite c m CoreExpr
- caseElimR :: MonadCatch m => Rewrite c m CoreExpr
- caseElimInlineScrutineeR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, ReadBindings c, HasEmptyContext c, MonadCatch m, MonadUnique m) => Rewrite c m CoreExpr
- caseElimMergeAltsR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, ReadBindings c, HasEmptyContext c, MonadCatch m, MonadUnique m) => Rewrite c m CoreExpr
- caseIntroSeqR :: (MonadCatch m, MonadUnique m) => (Id -> Bool) -> Rewrite c m CoreExpr
- caseElimSeqR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, ReadBindings c, HasEmptyContext c, MonadCatch m, MonadUnique m) => Rewrite c m CoreExpr
Rewrites on 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
Arguments
:: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, BoundVars c, HasDynFlags m, HasHermitMEnv m, HasHscEnv 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, BoundVars c, ExtendPath c Crumb, ReadPath c Crumb, HasHermitMEnv m, HasHscEnv m, HasDynFlags m, HasLemmas m, MonadCatch m, MonadIO m, MonadThings m, MonadUnique m) => 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!
caseFloatInArgsR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m CoreExpr Source
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 :: (MonadCatch m, MonadUnique m) => (Id -> Bool) -> Rewrite c m CoreExpr Source
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, HasEmptyContext c, MonadCatch m, MonadUnique m) => (Id -> Bool) -> 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
.