Safe Haskell | None |
---|---|
Language | Haskell2010 |
- externals :: [External]
- newtype RuleName = RuleName String
- newtype RuleNameListBox = RuleNameListBox [RuleName]
- foldRuleR :: (AddBindings c, ExtendPath c Crumb, HasCoreRules c, HasEmptyContext c, ReadBindings c, ReadPath c Crumb, HasDynFlags m, HasHermitMEnv m, HasLemmas m, LiftCoreM m, MonadCatch m, MonadIO m, MonadThings m, MonadUnique m) => Used -> RuleName -> Rewrite c m CoreExpr
- foldRulesR :: (AddBindings c, ExtendPath c Crumb, HasCoreRules c, HasEmptyContext c, ReadBindings c, ReadPath c Crumb, HasDynFlags m, HasHermitMEnv m, HasLemmas m, LiftCoreM m, MonadCatch m, MonadIO m, MonadThings m, MonadUnique m) => Used -> [RuleName] -> Rewrite c m CoreExpr
- unfoldRuleR :: (AddBindings c, ExtendPath c Crumb, HasCoreRules c, HasEmptyContext c, ReadBindings c, ReadPath c Crumb, HasDynFlags m, HasHermitMEnv m, HasLemmas m, LiftCoreM m, MonadCatch m, MonadIO m, MonadThings m, MonadUnique m) => Used -> RuleName -> Rewrite c m CoreExpr
- unfoldRulesR :: (AddBindings c, ExtendPath c Crumb, HasCoreRules c, HasEmptyContext c, ReadBindings c, ReadPath c Crumb, HasDynFlags m, HasHermitMEnv m, HasLemmas m, LiftCoreM m, MonadCatch m, MonadIO m, MonadThings m, MonadUnique m) => Used -> [RuleName] -> Rewrite c m CoreExpr
- compileRulesT :: (BoundVars c, HasCoreRules c, HasHermitMEnv m, LiftCoreM m, MonadCatch m, MonadIO m, MonadThings m) => [RuleName] -> Transform c m a CompiledFold
- ruleToQuantifiedT :: (BoundVars c, HasHermitMEnv m, MonadThings m, MonadCatch m) => Transform c m CoreRule Quantified
- ruleNameToQuantifiedT :: (BoundVars c, HasCoreRules c, HasDynFlags m, HasHermitMEnv m, LiftCoreM m, MonadCatch m, MonadIO m, MonadThings m) => RuleName -> Transform c m a Quantified
- getHermitRuleT :: (HasCoreRules c, HasHermitMEnv m, LiftCoreM m, MonadIO m) => RuleName -> Transform c m a CoreRule
- getHermitRulesT :: (HasCoreRules c, HasHermitMEnv m, LiftCoreM m, MonadIO m) => Transform c m a [(RuleName, CoreRule)]
- specConstrR :: RewriteH ModGuts
- specialiseR :: RewriteH ModGuts
GHC Rewrite Rules and Specialisation
Rules
foldRuleR :: (AddBindings c, ExtendPath c Crumb, HasCoreRules c, HasEmptyContext c, ReadBindings c, ReadPath c Crumb, HasDynFlags m, HasHermitMEnv m, HasLemmas m, LiftCoreM m, MonadCatch m, MonadIO m, MonadThings m, MonadUnique m) => Used -> RuleName -> Rewrite c m CoreExpr Source
Lookup a rule by name, attempt to apply it left-to-right. If successful, record it as an unproven lemma.
foldRulesR :: (AddBindings c, ExtendPath c Crumb, HasCoreRules c, HasEmptyContext c, ReadBindings c, ReadPath c Crumb, HasDynFlags m, HasHermitMEnv m, HasLemmas m, LiftCoreM m, MonadCatch m, MonadIO m, MonadThings m, MonadUnique m) => Used -> [RuleName] -> Rewrite c m CoreExpr Source
Lookup a set of rules by name, attempt to apply them left-to-right. Record an unproven lemma for the one that succeeds.
unfoldRuleR :: (AddBindings c, ExtendPath c Crumb, HasCoreRules c, HasEmptyContext c, ReadBindings c, ReadPath c Crumb, HasDynFlags m, HasHermitMEnv m, HasLemmas m, LiftCoreM m, MonadCatch m, MonadIO m, MonadThings m, MonadUnique m) => Used -> RuleName -> Rewrite c m CoreExpr Source
Lookup a rule by name, attempt to apply it left-to-right. If successful, record it as an unproven lemma.
unfoldRulesR :: (AddBindings c, ExtendPath c Crumb, HasCoreRules c, HasEmptyContext c, ReadBindings c, ReadPath c Crumb, HasDynFlags m, HasHermitMEnv m, HasLemmas m, LiftCoreM m, MonadCatch m, MonadIO m, MonadThings m, MonadUnique m) => Used -> [RuleName] -> Rewrite c m CoreExpr Source
Lookup a set of rules by name, attempt to apply them left-to-right. Record an unproven lemma for the one that succeeds.
compileRulesT :: (BoundVars c, HasCoreRules c, HasHermitMEnv m, LiftCoreM m, MonadCatch m, MonadIO m, MonadThings m) => [RuleName] -> Transform c m a CompiledFold Source
Can be used with runFoldR. Note: currently doesn't create a lemma for the rule used.
ruleToQuantifiedT :: (BoundVars c, HasHermitMEnv m, MonadThings m, MonadCatch m) => Transform c m CoreRule Quantified Source
Transform GHC's CoreRule into an Quantified.
ruleNameToQuantifiedT :: (BoundVars c, HasCoreRules c, HasDynFlags m, HasHermitMEnv m, LiftCoreM m, MonadCatch m, MonadIO m, MonadThings m) => RuleName -> Transform c m a Quantified Source
Build an Quantified from a named GHC rewrite rule.
getHermitRuleT :: (HasCoreRules c, HasHermitMEnv m, LiftCoreM m, MonadIO m) => RuleName -> Transform c m a CoreRule Source
Get a GHC CoreRule by name.
getHermitRulesT :: (HasCoreRules c, HasHermitMEnv m, LiftCoreM m, MonadIO m) => Transform c m a [(RuleName, CoreRule)] Source
Return all in-scope CoreRules (including specialization RULES on binders), with their names.
Specialisation
specConstrR :: RewriteH ModGuts Source
Run GHC's specConstr pass, and apply any rules generated.
specialiseR :: RewriteH ModGuts Source
Run GHC's specialisation pass, and apply any rules generated.