Portability | GHC only (-XKitchenSink) |
---|---|

Maintainer | Brent Yorgey <byorgey@cis.upenn.edu> |

Generic operations defined in terms of the RepLib framework and the
`Alpha`

type class.

- bind :: (Alpha p, Alpha t) => p -> t -> Bind p t
- unsafeUnbind :: (Alpha a, Alpha b) => GenBind order card a b -> (a, b)
- 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
- setbind :: (Alpha a, Alpha t) => [Name a] -> t -> SetPlusBind [Name a] t
- setbindAny :: Alpha t => [AnyName] -> t -> SetPlusBind [AnyName] t
- rebind :: (Alpha p1, Alpha p2) => p1 -> p2 -> Rebind p1 p2
- unrebind :: (Alpha p1, Alpha p2) => Rebind p1 p2 -> (p1, p2)
- rec :: Alpha p => p -> Rec p
- unrec :: Alpha p => Rec p -> p
- trec :: Alpha p => p -> TRec p
- untrec :: (Fresh m, Alpha p) => TRec p -> m p
- luntrec :: (LFresh m, Alpha p) => TRec p -> m p
- aeq :: Alpha t => t -> t -> Bool
- aeqBinders :: Alpha p => p -> p -> Bool
- acompare :: Alpha t => t -> t -> Ordering
- fvAny :: (Alpha t, Collection f) => t -> f AnyName
- fv :: (Rep a, Alpha t, Collection f) => t -> f (Name a)
- patfvAny :: (Alpha p, Collection f) => p -> f AnyName
- patfv :: (Rep a, Alpha p, Collection f) => p -> f (Name a)
- bindersAny :: (Alpha p, Collection f) => p -> f AnyName
- binders :: (Rep a, Alpha p, Collection f) => p -> f (Name a)
- swaps :: Alpha t => Perm AnyName -> t -> t
- swapsBinders :: Alpha p => Perm AnyName -> p -> p
- swapsEmbeds :: Alpha p => Perm AnyName -> p -> p
- lfreshen :: (Alpha p, LFresh m) => p -> (p -> Perm AnyName -> m b) -> m b
- freshen :: (Alpha p, Fresh m) => p -> m (p, Perm AnyName)
- unbind :: (Fresh m, Alpha p, Alpha t) => GenBind order card p t -> m (p, t)
- 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))
- 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))
- lunbind :: (LFresh m, Alpha p, Alpha t) => GenBind order card p t -> ((p, t) -> m c) -> m c
- 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
- 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

# 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

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`

.

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`

).

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.

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.

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