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

Safe HaskellNone
LanguageHaskell2010

HERMIT.Dictionary.Rules

Contents

Synopsis

GHC Rewrite Rules and Specialisation

externals :: [External] Source

Externals dealing with GHC rewrite rules.

Rules

foldRuleR :: (AddBindings c, ExtendPath c Crumb, HasCoreRules c, HasEmptyContext c, LemmaContext 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, LemmaContext 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, LemmaContext 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, LemmaContext 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.

ruleToClauseT :: (BoundVars c, HasHermitMEnv m, MonadThings m, MonadCatch m) => Transform c m CoreRule Clause Source

Transform GHC's CoreRule into an Clause.

ruleNameToClauseT :: (BoundVars c, HasCoreRules c, HasDynFlags m, HasHermitMEnv m, LiftCoreM m, MonadCatch m, MonadIO m, MonadThings m) => RuleName -> Transform c m a Clause Source

Build an Clause 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.