| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Data.Rewriting.Rules
Description
Rewrite rules
- data Rule lhs rhs where
- (===>) :: lhs a -> rhs a -> Rule lhs rhs
- class WildCard r where
- __ :: r a
- data MetaExp r a where
- class MetaVar r where
- meta :: MetaVar r => MetaRep r a -> r a
- ($$) :: MetaExp r (a -> b) -> MetaArg r a -> MetaExp r b
- ($-) :: MetaVar r => MetaExp r (a -> b) -> MetaArg r a -> r b
- (-$) :: MetaRep r (a -> b) -> MetaArg r a -> MetaExp r b
- (-$-) :: MetaVar r => MetaRep r (a -> b) -> MetaArg r a -> r b
- type Name = Integer
- newtype MetaId a = MetaId Name
- class Quantifiable rule where
- quantify :: (Quantifiable rule, RuleType rule ~ Rule lhs rhs) => rule -> Rule lhs rhs
- data WILD a = WildCard
- data META r a = forall b . Meta (MetaExp r b)
- newtype LHS f a = LHS {}
- newtype RHS f a = RHS {}
- type family Var r :: * -> *
- class Rep r where
- tRule :: Patch (Rule (LHS f) (RHS f)) (Rule (LHS f) (RHS f))
- data A = A
- data B = B
- data C = C
- tA :: Patch A A
- tB :: Patch B B
- tC :: Patch C C
- type Subst f = [(Name, Term f)]
Tagless rewrite rules
Representations supporting wildcards
Minimal complete definition
Nothing
Meta-variable applied to a number of Var expressions
Representations supporting meta-variables
($$) :: MetaExp r (a -> b) -> MetaArg r a -> MetaExp r b infixl 2 Source
Meta-variable application (used for all but the first and last variable)
($-) :: MetaVar r => MetaExp r (a -> b) -> MetaArg r a -> r b infixl 2 Source
Meta-variable application (used for the last variable)
(-$) :: MetaRep r (a -> b) -> MetaArg r a -> MetaExp r b infixl 2 Source
Meta-variable application (used for the first variable)
(-$-) :: MetaVar r => MetaRep r (a -> b) -> MetaArg r a -> r b infixl 2 Source
Meta-variable application (used when there is only variable)
Typed meta-variable identifiers
class Quantifiable rule where Source
Rules that may take a number of meta-variables as arguments. Those meta-variables are implicitly forall-quantified.
Methods
quantify' :: Name -> rule -> RuleType rule Source
Quantify a rule starting from the provided variable identifier
Instances
| (Quantifiable rule, (~) * m (MetaId a)) => Quantifiable (m -> rule) Source | Recursive case: one more meta-variable |
| Quantifiable (Rule lhs rhs) Source | Base case: no meta-variables |
quantify :: (Quantifiable rule, RuleType rule ~ Rule lhs rhs) => rule -> Rule lhs rhs Source
Forall-quantify the meta-variable arguments of a rule
Representation of rules
Functor representing wildcards
Constructors
| WildCard |
Functor representing meta variables applied to a number of Var expressions
Left hand side of a rule
Instances
| Rep (LHS f) Source | |
| MetaVar (LHS f) Source | |
| WildCard (LHS f) Source | |
| ((:<:) VAR (PF (LHS f)), (:<:) LAM (PF (LHS f)), Functor f, Foldable f) => Bind (LHS f) Source | |
| type PF (LHS f) = (:+:) * WILD ((:+:) * (META (LHS f)) f) Source | |
| type Var (LHS f) = VAR Source | |
| type MetaRep (LHS f) = MetaId Source | |
| type MetaArg (LHS f) = Var (LHS f) Source |
Right hand side of a rule