ho-rewriting-0.1: Generic rewrite rules with safe treatment of variables and binders

Safe HaskellNone
LanguageHaskell2010

Data.Rewriting.Rules

Contents

Description

Rewrite rules

Synopsis

Tagless rewrite rules

data Rule lhs rhs where Source

Rewrite rules

Constructors

Rule :: lhs a -> rhs a -> Rule lhs rhs 

Instances

Quantifiable (Rule lhs rhs)

Base case: no meta-variables

type RuleType (Rule lhs rhs) = Rule lhs rhs 

(===>) :: lhs a -> rhs a -> Rule lhs rhs infix 1 Source

Construct a rule from an LHS and an RHS

class WildCard r where Source

Representations supporting wildcards

Minimal complete definition

Nothing

Methods

__ :: r a Source

Instances

data MetaExp r a where Source

Meta-variable applied to a number of Var expressions

Constructors

MVar :: MetaRep r a -> MetaExp r a 
MApp :: MetaExp r (a -> b) -> MetaArg r a -> MetaExp r b 

class MetaVar r where Source

Representations supporting meta-variables

Associated Types

type MetaRep r :: * -> * Source

type MetaArg r :: * -> * Source

Methods

metaExp :: MetaExp r a -> r a Source

Instances

MetaVar (RHS f) 
MetaVar (LHS f) 

mvar :: MetaVar r => MetaRep r a -> r a Source

Construct a meta-variable

($$) :: 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)

type Name = Integer Source

Variable identifier

newtype MetaId a Source

Typed meta-variable identifiers

Constructors

MetaId Name 

Instances

Enum (MetaId a) 
Eq (MetaId a) 
Integral (MetaId a) 
Num (MetaId a) 
Ord (MetaId a) 
Real (MetaId a) 
Show (MetaId a) 

class Quantifiable rule where Source

Rules that may take a number of meta-variables as arguments. Those meta-variables are implicitly forall-quantified.

Associated Types

type RuleType rule Source

Rule type after quantification

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)

Recursive case: one more meta-variable

Quantifiable (Rule lhs rhs)

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

data WILD a Source

Functor representing wildcards

Constructors

WildCard 

data META r a Source

Functor representing meta variables applied to a number of Var expressions

Constructors

forall b . Meta (MetaExp r b) 

Instances

newtype LHS f a Source

Left hand side of a rule

Constructors

LHS 

Fields

unLHS :: Term (WILD :+: (META (LHS f) :+: f))
 

Instances

Rep (LHS f) 
MetaVar (LHS f) 
WildCard (LHS f) 
((:<:) VAR (PF (LHS f)), (:<:) LAM (PF (LHS f)), Functor f, Foldable f) => Bind (LHS f) 
type PF (LHS f) = (:+:) * WILD ((:+:) * (META (LHS f)) f) 
type Var (LHS f) = VAR 
type MetaRep (LHS f) = MetaId 
type MetaArg (LHS f) = Var (LHS f) 

newtype RHS f a Source

Right hand side of a rule

Constructors

RHS 

Fields

unRHS :: Term (META (RHS f) :+: f)
 

Instances

Rep (RHS f) 
MetaVar (RHS f) 
((:<:) VAR (PF (RHS f)), (:<:) LAM (PF (RHS f)), Functor f, Foldable f) => Bind (RHS f) 
type PF (RHS f) = (:+:) * (META (RHS f)) f 
type Var (RHS f) = VAR 
type MetaRep (RHS f) = MetaId 
type MetaArg (RHS f) = RHS f 

type family Var r :: * -> * Source

Representation of object variables

Instances

type Var (RHS f) = VAR 
type Var (LHS f) = VAR 

Generalize over representations

class Rep r where Source

Associated Types

type PF r :: * -> * Source

Methods

toRep :: Term (PF r) -> r a Source

fromRep :: r a -> Term (PF r) Source

Instances

Rep (RHS f) 
Rep (LHS f) 

Misc.

tRule :: Patch (Rule (LHS f) (RHS f)) (Rule (LHS f) (RHS f)) Source

data A Source

Constructors

A 

Instances

Eq A 

data B Source

Constructors

B 

Instances

Eq B 

data C Source

Constructors

C 

Instances

Eq C 

type Subst f = [(Name, Term f)] Source

Substitution