DDC.Core.Transform.Rewrite.Rule

Constructing and checking whether rewrite rules are valid

Binding modes

data BindMode

Binding level for the binders in a rewrite rule.

Constructors

BMSpec

Level-1 binder (specs)

BMValue Int

number of usages

Instances

Eq BindMode

Show BindMode

isBMSpec :: BindMode -> Bool

Check if a BindMode is a BMSpec.

isBMValue :: BindMode -> Bool

Check if a BindMode is a BMValue.

data RewriteRule a n

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

ruleBinds :: [(BindMode, Bind n)]

Variables bound by the rule.

ruleConstraints :: [Type n]

Extra constraints on the rule. These must all be satisfied for the rule to fire.

ruleLeft :: Exp a n

Left-hand side of the rule. We match on this part.

ruleLeftHole :: Maybe (Exp a n)

Extra part of left-hand side, but allow this bit to be out-of-context.

ruleRight :: Exp a n

Right-hand side of the rule. We replace the matched expression with this part.

ruleWeakEff :: Maybe (Effect n)

Effects that are caused by the left but not the right. When applying the rule we add an effect weakning to ensure the rewritten expression has the same effects.

ruleWeakClo :: [Exp a n]

Closure that the left has that is not present in the right. When applying the rule we add a closure weakening to ensure the rewritten expression has the same closure.

ruleFreeVars :: [Bound n]

References to environment. Used to check whether the rule is shadowed.

Instances

Reannotate RewriteRule

Allow the expressions and anything else with annotations to be reannotated

(Eq a, Eq n) => Eq (RewriteRule a n)

(Show a, Show n) => Show (RewriteRule a n)

(Pretty n, Eq n) => Pretty (RewriteRule a n)

type NamedRewriteRule a n = (String, RewriteRule a n)

Construction

mkRewriteRule

Arguments

:: Ord n

=> [(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.

checkRewriteRule

Arguments

:: (Show a, Ord n, Show n, Pretty n)

=> Config n

Type checker config.

-> Env n

Kind environment.

-> Env n

Type 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.

data Error a n

What can go wrong when checking a rewrite rule.

Constructors

ErrorTypeCheck

Error typechecking one of the expressions

Fields

errorSide :: Side

What side of the rule the error was on.

errorExp :: Exp a n

errorCheckError :: Error a n

ErrorBadConstraint

Error typechecking one of the expressions

Fields

errorConstraint :: Type n

ErrorTypeConflict

Types don't match...

Fields

errorTypeLhs :: (Type n, Effect n, Closure n)

errorTypeRhs :: (Type n, Effect n, Closure n)

ErrorNotFirstOrder

No binders allowed in left-hand side (right is fine, eg lets)

Fields

errorExp :: Exp a n

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

errorBinder :: Bind n

Instances

(Pretty a, Show a, Pretty n, Show n, Eq n) => Pretty (Error a n)

data Side

What side of a rewrite rule we're talking about.

Constructors

Lhs

Rhs

Instances

Pretty Side