| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
DDC.Core.Transform.Rewrite.Rule
Contents
Description
Constructing and checking whether rewrite rules are valid
- data BindMode
- isBMSpec :: BindMode -> Bool
- isBMValue :: BindMode -> Bool
- data RewriteRule a n = RewriteRule {
- ruleBinds :: [(BindMode, Bind n)]
- ruleConstraints :: [Type n]
- ruleLeft :: Exp a n
- ruleLeftHole :: Maybe (Exp a n)
- ruleRight :: Exp a n
- ruleWeakEff :: Maybe (Effect n)
- ruleWeakClo :: [Exp a n]
- ruleFreeVars :: [Bound n]
- type NamedRewriteRule a n = (String, RewriteRule a n)
- mkRewriteRule :: [(BindMode, Bind n)] -> [Type n] -> Exp a n -> Maybe (Exp a n) -> Exp a n -> RewriteRule a n
- checkRewriteRule :: (Show a, Ord n, Show n, Pretty n) => Config n -> EnvX n -> RewriteRule a n -> Either (Error a n) (RewriteRule (AnTEC a n) n)
- data Error a n
- = ErrorTypeCheck { }
- | ErrorBadConstraint {
- errorConstraint :: Type n
- | ErrorTypeConflict {
- errorTypeLhs :: (Type n, Effect n, Closure n)
- errorTypeRhs :: (Type n, Effect n, Closure n)
- | ErrorNotFirstOrder { }
- | ErrorVarUnmentioned
- | ErrorAnonymousBinder {
- errorBinder :: Bind n
- data Side
Binding modes
Binding level for the binders in a rewrite rule.
data RewriteRule a n Source #
A rewrite rule. For example:
RULE [r1 r2 r3 : %] (x : Int r1)
. addInt [:r1 r2 r3:] x (0 [r2] ()
= copyInt [:r1 r3:] x
Constructors
| RewriteRule | |
Fields
| |
Instances
| Reannotate RewriteRule Source # | Allow the expressions and anything else with annotations to be reannotated |
| (Eq a, Eq n) => Eq (RewriteRule a n) Source # | |
| (Show a, Show n) => Show (RewriteRule a n) Source # | |
| (Pretty n, Eq n) => Pretty (RewriteRule a n) Source # | |
type NamedRewriteRule a n = (String, RewriteRule a n) Source #
Construction
Arguments
| :: [(BindMode, Bind n)] | Variables bound by the rule. |
| -> [Type n] | Extra constraints on the rule. |
| -> Exp a n | Left-hand side of the rule. |
| -> Maybe (Exp a n) | Extra part of left, can be out of context. |
| -> Exp a n | Right-hand side (replacement) |
| -> RewriteRule a n |
Construct a rewrite rule, but do not check if it's valid.
You then need to apply checkRewriteRule to check it.
Arguments
| :: (Show a, Ord n, Show n, Pretty n) | |
| => Config n | Type checker config. |
| -> EnvX n | Type checker environment. |
| -> RewriteRule a n | Rule to check |
| -> Either (Error a n) (RewriteRule (AnTEC a n) n) |
Take a rule, make sure it's valid and fill in type, closure and effect information.
The left-hand side of rule can't have any binders (lambdas, lets etc).
All binders must appear in the left-hand side, otherwise they would match with no value.
Both sides must have the same types, but the right can have fewer effects and smaller closure.
We don't handle anonymous binders on either the left or right.
What can go wrong when checking a rewrite rule.
Constructors
| ErrorTypeCheck | Error typechecking one of the expressions |
| ErrorBadConstraint | Error typechecking one of the expressions |
Fields
| |
| ErrorTypeConflict | Types don't match... |
Fields
| |
| ErrorNotFirstOrder | No binders allowed in left-hand side (right is fine, eg |
| ErrorVarUnmentioned | All variables must be mentioned in left-hand side, otherwise they won't get bound. |
| ErrorAnonymousBinder | I don't want to deal with anonymous variables. |
Fields
| |