Unbound.LocallyNameless.Ops

Generic operations defined in terms of the RepLib framework and the Alpha type class.

Documentation

bind :: (Alpha p, Alpha t) => p -> t -> Bind p t

A smart constructor for binders, also sometimes referred to as "close". Free variables in the term are taken to be references to matching binders in the pattern. (Free variables with no matching binders will remain free.)

unsafeUnbind :: (Alpha a, Alpha b) => Bind a b -> (a, b)

A destructor for binders that does not guarantee fresh names for the binders.

rebind :: (Alpha p1, Alpha p2) => p1 -> p2 -> Rebind p1 p2

Constructor for rebinding patterns.

unrebind :: (Alpha p1, Alpha p2) => Rebind p1 p2 -> (p1, p2)

Destructor for rebinding patterns. It does not need a monadic context for generating fresh names, since Rebind can only occur in the pattern of a Bind; hence a previous call to unbind (or something similar) must have already freshened the names at this point.

rec :: Alpha p => p -> Rec p

Constructor for recursive patterns.

unrec :: Alpha p => Rec p -> p

Destructor for recursive patterns.

trec :: Alpha p => p -> TRec p

Constructor for recursive abstractions.

untrec :: (Fresh m, Alpha p) => TRec p -> m p

Destructor for recursive abstractions which picks globally fresh names for the binders.

luntrec :: (LFresh m, Alpha p) => TRec p -> m p

Destructor for recursive abstractions which picks locally fresh names for binders (see LFresh).

aeq :: Alpha t => t -> t -> Bool

Determine the alpha-equivalence of two terms.

aeqBinders :: Alpha p => p -> p -> Bool

Determine (alpha-)equivalence of patterns. Do they bind the same variables in the same patterns and have alpha-equivalent annotations in matching positions?

acompare :: Alpha t => t -> t -> Ordering

An alpha-respecting total order on terms involving binders.

fvAny :: (Alpha t, Collection f) => t -> f AnyName

Calculate the free variables (of any sort) contained in a term.

fv :: (Rep a, Alpha t, Collection f) => t -> f (Name a)

Calculate the free variables of a particular sort contained in a term.

patfvAny :: (Alpha p, Collection f) => p -> f AnyName

Calculate the variables (of any sort) that occur freely in terms embedded within a pattern (but are not bound by the pattern).

patfv :: (Rep a, Alpha p, Collection f) => p -> f (Name a)

Calculate the variables of a particular sort that occur freely in terms embedded within a pattern (but are not bound by the pattern).

bindersAny :: (Alpha p, Collection f) => p -> f AnyName

Calculate the binding variables (of any sort) in a pattern.

binders :: (Rep a, Alpha p, Collection f) => p -> f (Name a)

Calculate the binding variables (of a particular sort) in a pattern.

swaps :: Alpha t => Perm AnyName -> t -> t

Apply a permutation to a term.

swapsBinders :: Alpha p => Perm AnyName -> p -> p

Apply a permutation to the binding variables in a pattern. Embedded terms are left alone by the permutation.

swapsEmbeds :: Alpha p => Perm AnyName -> p -> p

Apply a permutation to the embedded terms in a pattern. Binding names are left alone by the permutation.

lfreshen :: (Alpha p, LFresh m) => p -> (p -> Perm AnyName -> m b) -> m b

"Locally" freshen a pattern, replacing all binding names with new names that are not already "in scope". The second argument is a continuation, which takes the renamed term and a permutation that specifies how the pattern has been renamed. The resulting computation will be run with the in-scope set extended by the names just generated.

freshen :: (Alpha p, Fresh m) => p -> m (p, Perm AnyName)

Freshen a pattern by replacing all old binding Names with new fresh Names, returning a new pattern and a Perm Name specifying how Names were replaced.

unbind :: (Fresh m, Alpha p, Alpha t) => Bind p t -> m (p, t)

Unbind (also known as "open") is the simplest destructor for bindings. It ensures that the names in the binding are globally fresh, using a monad which is an instance of the Fresh type class.

unbind2 :: (Fresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => Bind p1 t1 -> Bind p2 t2 -> m (Maybe (p1, t1, p2, t2))

Unbind two terms with the same fresh names, provided the binders have the same number of binding variables. If the patterns have different numbers of binding variables, return Nothing. Otherwise, return the renamed patterns and the associated terms.

unbind3 :: (Fresh m, Alpha p1, Alpha p2, Alpha p3, Alpha t1, Alpha t2, Alpha t3) => Bind p1 t1 -> Bind p2 t2 -> Bind p3 t3 -> m (Maybe (p1, t1, p2, t2, p3, t3))

Unbind three terms with the same fresh names, provided the binders have the same number of binding variables. See the documentation for unbind2 for more details.

lunbind :: (LFresh m, Alpha p, Alpha t) => Bind p t -> ((p, t) -> m c) -> m c

lunbind opens a binding in an LFresh monad, ensuring that the names chosen for the binders are locally fresh. The components of the binding are passed to a continuation, and the resulting monadic action is run in a context extended to avoid choosing new names which are the same as the ones chosen for this binding.

For more information, see the documentation for the LFresh type class.

lunbind2 :: (LFresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => Bind p1 t1 -> Bind p2 t2 -> (Maybe (p1, t1, p2, t2) -> m r) -> m r

Unbind two terms with the same locally fresh names, provided the patterns have the same number of binding variables. See the documentation for unbind2 and lunbind for more details.

lunbind3 :: (LFresh m, Alpha p1, Alpha p2, Alpha p3, Alpha t1, Alpha t2, Alpha t3) => Bind p1 t1 -> Bind p2 t2 -> Bind p3 t3 -> (Maybe (p1, t1, p2, t2, p3, t3) -> m r) -> m r

Unbind three terms with the same locally fresh names, provided the binders have the same number of binding variables. See the documentation for unbind2 and lunbind for more details.