Safe Haskell	None
Language	Haskell2010

Data.Rewriting.HigherOrder

Description

Higher-order rewriting

Synopsis

Documentation

class Bind r where Source

Representations supporting variable binding

Methods

var :: Var r a -> r a Source

lam :: (Var r a -> r b) -> r (a -> b) Source

Instances

((:<:) VAR (PF (RHS f)), (:<:) LAM (PF (RHS f)), Functor f, Foldable f) => Bind (RHS f)
((:<:) VAR (PF (LHS f)), (:<:) LAM (PF (LHS f)), Functor f, Foldable f) => Bind (LHS f)

newtype VAR a Source

Functor representing object variables

Constructors

Var Name

Instances

Functor VAR
Foldable VAR
Traversable VAR
Render VAR
EqF VAR
ShowF VAR
ShowConstr VAR
Enum (VAR a)
Eq (VAR a)
Integral (VAR a)
Num (VAR a)
Ord (VAR a)
Real (VAR a)
Show (VAR a)

data LAM a Source

Functor representing lambda abstraction

Constructors

Lam Name a

Instances

Functor LAM
Foldable LAM
Traversable LAM
Render LAM
EqF LAM
ShowF LAM
ShowConstr LAM
Eq a => Eq (LAM a)
Show a => Show (LAM a)

data APP a Source

Functor representing application

Constructors

App a a

Instances

Functor APP
Foldable APP
Traversable APP
Render APP
EqF APP
ShowF APP
ShowConstr APP
Eq a => Eq (APP a)
Show a => Show (APP a)

fresh :: (LAM :<: f, Functor f, Foldable f) => Term f -> Name Source

mkLam :: (Rep r, VAR :<: PF r, LAM :<: PF r, Functor (PF r), Foldable (PF r)) => (VAR a -> Var r a) -> (Var r a -> r b) -> r (a -> b) Source

Generic lambda abstraction

app :: APP :<: f => Term (f :&: Set Name) -> Term (f :&: Set Name) -> Term (f :&: Set Name) Source

Application operator, to use as argument to functions like applyFirst, bottomUp, etc.

type OneToOne a b = (Map a b, Map b a) Source

One-to-one map

oEmpty :: OneToOne a b Source

Empty one-to-one map

oMember :: (Ord a, Ord b) => (a, b) -> OneToOne a b -> Bool Source

Test if a mapping is in a one-to-one map

oMemberEither :: (Ord a, Ord b) => (a, b) -> OneToOne a b -> Bool Source

Test if either side of a mapping is in a one-to-one map

oLookupL :: Ord a => a -> OneToOne a b -> Maybe b Source

Left lookup in a one-to-one map

oInsert :: (Ord a, Ord b) => (a, b) -> OneToOne a b -> OneToOne a b Source

Insert a one-to-one mapping

getAnn :: Term (f :&: a) -> a Source

type AlphaEnv = OneToOne Name Name Source

Environment keeping track of alpha-renaming

matchM :: forall f a. (VAR :<: f, LAM :<: f, VAR :<: PF (LHS f), LAM :<: PF (LHS f), Functor f, Foldable f, EqF f) => LHS f a -> Term (f :&: Set Name) -> ReaderT AlphaEnv (WriterT (Subst (f :&: Set Name)) Maybe) () Source

Higher-order matching. Results in a list of candidate mappings.

alphaEq :: (VAR :<: f, LAM :<: f, Functor f, Foldable f, EqF f) => Term f -> Term f -> Bool Source

Alpha-equivalence

solveTermAlpha :: (VAR :<: f, LAM :<: f, Functor f, Foldable f, EqF f) => [Term (f :&: a)] -> Maybe (Term (f :&: a)) Source

Check if all terms are alpha-equivalent, and if so, return one of them

solveSubstAlpha :: (VAR :<: f, LAM :<: f, Functor f, Foldable f, EqF f) => Subst (f :&: a) -> Maybe (Subst (f :&: a)) Source

Turn a list of candidate mappings into a substitution. Succeeds iff. all mappings for the same variable are alpha-equivalent.

match :: (VAR :<: f, LAM :<: f, VAR :<: PF (LHS f), LAM :<: PF (LHS f), Functor f, Foldable f, EqF f) => LHS f a -> Term (f :&: Set Name) -> Maybe (Subst (f :&: Set Name)) Source

Higher-order matching. Succeeds if the pattern matches and all occurrences of a given meta-variable are matched against equal terms.

annFreeVars :: (VAR :<: f, LAM :<: f, Functor f, Foldable f) => f (Term (f :&: Set Name)) -> Term (f :&: Set Name) Source

Annotate a node with its set of free variables

substitute Source

Arguments

:: (VAR :<: f, LAM :<: f, Traversable f, g ~ (f :&: Set Name))
=> (Term g -> Term g -> Term g)	Application operator
-> Subst g
-> RHS f a
-> Maybe (Term g)

Capture-avoiding substitution. Succeeds iff. each meta-variable in RHS has a mapping in the substitution.

rewrite Source

Arguments

:: (VAR :<: f, LAM :<: f, VAR :<: PF (LHS f), LAM :<: PF (LHS f), Traversable f, EqF f, g ~ (f :&: Set Name))
=> (Term g -> Term g -> Term g)	Application operator
-> Rule (LHS f) (RHS f)
-> Term (f :&: Set Name)
-> Maybe (Term (f :&: Set Name))

Apply a rule. Succeeds iff. both matching and substitution succeeds.

applyFirst Source

Arguments

:: (VAR :<: f, LAM :<: f, VAR :<: PF (LHS f), LAM :<: PF (LHS f), Traversable f, EqF f, g ~ (f :&: Set Name))
=> (Term g -> Term g -> Term g)	Application operator
-> [Rule (LHS f) (RHS f)]
-> Term (f :&: Set Name)
-> Term (f :&: Set Name)

Apply the first succeeding rule from a list of rules. If no rule succeeds the term is returned unchanged.

bottomUp Source

Arguments

:: (VAR :<: f, LAM :<: f, VAR :<: PF (LHS f), LAM :<: PF (LHS f), Traversable f, EqF f, g ~ (f :&: Set Name))
=> (Term g -> Term g -> Term g)	Application operator
-> [Rule (LHS f) (RHS f)]
-> Term f
-> Term (f :&: Set Name)

Apply a list of rules bottom-up across a term