Safe Haskell  None 

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 :: Ord n => [(BindMode, Bind n)] > [Type n] > Exp a n > Maybe (Exp a n) > Exp a n > RewriteRule a n
 checkRewriteRule :: (Ord n, Show n, Pretty n) => Config n > Env n > Env 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
RewriteRule  

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)Source
Construction
:: Ord n  
=> [(BindMode, Bind n)]  Variables bound by the rule. 
> [Type n]  Extra constraints on the rule. 
> Exp a n  Lefthand side of the rule. 
> Maybe (Exp a n)  Extra part of left, can be out of context. 
> Exp a n  Righthand 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.
:: (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 lefthand side of rule can't have any binders (lambdas, lets etc).
All binders must appear in the lefthand 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.
ErrorTypeCheck  Error typechecking one of the expressions 
ErrorBadConstraint  Error typechecking one of the expressions 
 
ErrorTypeConflict  Types don't match... 
 
ErrorNotFirstOrder  No binders allowed in lefthand side (right is fine, eg 
ErrorVarUnmentioned  All variables must be mentioned in lefthand side, otherwise they won't get bound. 
ErrorAnonymousBinder  I don't want to deal with anonymous variables. 
