Data.Rewriting.HigherOrder

Higher-order rewriting

Documentation

class Bind r where

Representations supporting variable binding

Methods

var :: Var r a -> r a

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

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

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

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

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

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)

Generic lambda abstraction

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

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

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

One-to-one map

oEmpty :: OneToOne a b

Empty one-to-one map

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

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

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

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

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

Left lookup in a one-to-one map

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

Insert a one-to-one mapping

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

type AlphaEnv = OneToOne Name Name

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

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

Alpha-equivalence

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

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))

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))

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)

Annotate a node with its set of free variables

type Aliases = (Map Name Name, Name)

Environment for aliases

initAliases :: Set Name -> Aliases

Set up an initial alias environment from a set of reserved names

rename :: Name -> Aliases -> (Name, Aliases)

Rename to a fresh name

renameNaive :: Name -> Aliases -> (Name, Aliases)

Naive renaming. Use instead of rename to get naive substitution.

lookAlias :: Name -> Aliases -> Maybe Name

Lookup a name in an alias environment

substitute

Arguments

:: (VAR :<: f, LAM :<: f, VAR :<: PF (RHS f), LAM :<: PF (RHS 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.

Uses the "rapier" method described in "Secrets of the Glasgow Haskell Compiler inliner" (Peyton Jones and Marlow, JFP 2006) to rename variables where there's risk for capturing.

rewrite

Arguments

:: (VAR :<: f, LAM :<: f, VAR :<: PF (LHS f), LAM :<: PF (LHS f), VAR :<: PF (RHS f), LAM :<: PF (RHS f), Traversable f, EqF f, g ~ (f :&: Set Name))

=> (Term g -> Term g -> Term g)

Application operator

-> Rule (LHS f) (RHS f)

-> Term g

-> Maybe (Term g)

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

applyFirst

Arguments

:: (VAR :<: f, LAM :<: f, VAR :<: PF (LHS f), LAM :<: PF (LHS f), VAR :<: PF (RHS f), LAM :<: PF (RHS f), Traversable f, EqF f, g ~ (f :&: Set Name))

=> (Term g -> Term g -> Term g)

Application operator

-> [Rule (LHS f) (RHS f)]

-> Term g

-> Term g

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

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

Prepare a term for rewriting by annotating each node with its set of free variables

stripAnn :: Functor f => Term (f :&: a) -> Term f

Strip out the annotations from a term

rewriteWith :: (VAR :<: f, LAM :<: f, Functor f, Foldable f, g ~ (f :&: Set Name)) => (Term g -> Term g) -> Term f -> Term f

Apply a higher-order rewriter to a term

Typically used as rewriteWith (bottomUp (applyFirst ...)) :: (...) => Term f -> Term f, where f is not annotated