unbound-0.4.3: Generic support for programming with names and binders

PortabilityGHC only (-XKitchenSink)
MaintainerBrent Yorgey <byorgey@cis.upenn.edu>
Safe HaskellNone

Unbound.LocallyNameless.Ops

Description

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

Synopsis

Documentation

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

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

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

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

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

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

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

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] tSource

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] tSource

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 p2Source

Constructor for rebinding patterns.

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

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 pSource

Constructor for recursive patterns.

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

Destructor for recursive patterns.

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

Constructor for recursive abstractions.

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

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

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

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

aeq :: Alpha t => t -> t -> BoolSource

Determine the alpha-equivalence of two terms.

aeqBinders :: Alpha p => p -> p -> BoolSource

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

An alpha-respecting total order on terms involving binders.

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

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

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

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

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

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

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 AnyNameSource

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

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

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

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

Apply a permutation to a term.

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

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

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

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 bSource

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

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

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

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

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 cSource

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 rSource

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 rSource

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

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

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 rSource

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 rSource