ddc-core-simpl-0.4.3.1: Disciplined Disciple Compiler code transformations.

DDC.Core.Transform.Rewrite.Rule

Contents

Description

Constructing and checking whether rewrite rules are valid

Synopsis

# Binding modes

data BindMode Source #

Binding level for the binders in a rewrite rule.

Constructors

 BMSpec Level-1 binder (specs) BMValue Int number of usages

Instances

 Source # Methods Source # MethodsshowList :: [BindMode] -> ShowS #

Check if a BindMode is a BMSpec.

Check if a BindMode is a BMValue.

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 FieldsruleBinds :: [(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 nLeft-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 nRight-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

 Source # Allow the expressions and anything else with annotations to be reannotated Methodsreannotate :: (a -> b) -> RewriteRule a n -> RewriteRule b n #reannotateM :: Monad m => (a -> m b) -> RewriteRule a n -> m (RewriteRule b n) # (Eq a, Eq n) => Eq (RewriteRule a n) Source # Methods(==) :: RewriteRule a n -> RewriteRule a n -> Bool #(/=) :: RewriteRule a n -> RewriteRule a n -> Bool # (Show a, Show n) => Show (RewriteRule a n) Source # MethodsshowsPrec :: Int -> RewriteRule a n -> ShowS #show :: RewriteRule a n -> String #showList :: [RewriteRule a n] -> ShowS # (Pretty n, Eq n) => Pretty (RewriteRule a n) Source # Associated Typesdata PrettyMode (RewriteRule a n) :: * # Methodsppr :: RewriteRule a n -> Doc #pprPrec :: Int -> RewriteRule a n -> Doc #pprModePrec :: PrettyMode (RewriteRule a n) -> Int -> RewriteRule a n -> Doc #

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

data Error a n Source #

What can go wrong when checking a rewrite rule.

Constructors

 ErrorTypeCheck Error typechecking one of the expressions FieldserrorSide :: SideWhat side of the rule the error was on.errorExp :: Exp a n errorCheckError :: Error a n ErrorBadConstraint Error typechecking one of the expressions FieldserrorConstraint :: Type n ErrorTypeConflict Types don't match... FieldserrorTypeLhs :: (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) FieldserrorExp :: 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. FieldserrorBinder :: Bind n

Instances

 (Pretty a, Pretty n, Show n, Eq n) => Pretty (Error a n) Source # Associated Typesdata PrettyMode (Error a n) :: * # Methodsppr :: Error a n -> Doc #pprPrec :: Int -> Error a n -> Doc #pprModePrec :: PrettyMode (Error a n) -> Int -> Error a n -> Doc #

data Side Source #

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

Constructors

 Lhs Rhs

Instances

 Source # Associated Typesdata PrettyMode Side :: * # Methodsppr :: Side -> Doc #pprPrec :: Int -> Side -> Doc #pprModePrec :: PrettyMode Side -> Int -> Side -> Doc #