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) => GenBind order card a b -> (a, b)

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

permCloseAny :: Alpha t => [AnyName] -> t -> ([AnyName], t)

strength :: Functor f => (a, f b) -> f (a, b)

permClose :: (Alpha a, Alpha t) => [Name a] -> t -> ([Name a], t)

permbind :: (Alpha p, Alpha t) => p -> t -> SetBind p t

Bind the pattern in the term "up to permutation" of bound variables. For example, the following 4 terms are all alpha-equivalent:

 permbind [a,b] (a,b)
 permbind [a,b] (b,a)
 permbind [b,a] (a,b)
 permbind [b,a] (b,a)

Note that none of these terms is equivalent to a term with a redundant pattern such as

 permbind [a,b,c] (a,b)

For binding constructors which do render these equivalent, see setbind and setbindAny.

setbind :: (Alpha a, Alpha t) => [Name a] -> t -> SetPlusBind [Name a] t

Bind the list of names in the term up to permutation and dropping of unused variables.

For example, the following 5 terms are all alpha-equivalent:

 setbind [a,b] (a,b)
 setbind [a,b] (b,a)
 setbind [b,a] (a,b)
 setbind [b,a] (b,a)
 setbind [a,b,c] (a,b)

There is also a variant, setbindAny, which ignores name sorts.

setbindAny :: Alpha t => [AnyName] -> t -> SetPlusBind [AnyName] t

Bind the list of (any-sorted) names in the term up to permutation and dropping of unused variables. See setbind.

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) => GenBind order card 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) => GenBind order card p1 t1 -> GenBind order card p2 t2 -> m (Maybe (p1, t1, p2, t2))

Unbind two terms with the same fresh names, provided the binders have the same binding variables (both number and sort). If the patterns have different 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) => GenBind order card p1 t1 -> GenBind order card p2 t2 -> GenBind order card 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) => GenBind order card 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) => GenBind order card p1 t1 -> GenBind order card 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) => GenBind order card p1 t1 -> GenBind order card p2 t2 -> GenBind order card 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.

unbind2Plus :: (MonadPlus m, Fresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => GenBind order card p1 t1 -> GenBind order card p2 t2 -> m (p1, t1, p2, t2)

unbind3Plus :: (MonadPlus m, Fresh m, Alpha p1, Alpha p2, Alpha p3, Alpha t1, Alpha t2, Alpha t3) => GenBind order card p1 t1 -> GenBind order card p2 t2 -> GenBind order card p3 t3 -> m (p1, t1, p2, t2, p3, t3)

lunbind2Plus :: (MonadPlus m, LFresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => GenBind order card p1 t1 -> GenBind order card p2 t2 -> ((p1, t1, p2, t2) -> m r) -> m r

lunbind3Plus :: (MonadPlus m, LFresh m, Alpha p1, Alpha p2, Alpha p3, Alpha t1, Alpha t2, Alpha t3) => GenBind order card p1 t1 -> GenBind order card p2 t2 -> GenBind order card p3 t3 -> ((p1, t1, p2, t2, p3, t3) -> m r) -> m r