License | BSD-like (see LICENSE) |
---|---|

Maintainer | Stephanie Weirich <sweirich@cis.upenn.edu> |

Portability | GHC only (-XKitchenSink) |

Safe Haskell | None |

Language | Haskell2010 |

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

type class.

## Synopsis

- bind :: (Alpha p, Alpha t) => p -> t -> Bind p t
- permClose :: (Alpha a, Alpha t) => [Name a] -> t -> ([Name a], t)
- permCloseAny :: Alpha t => [AnyName] -> t -> ([AnyName], t)
- strength :: Functor f => (a, f b) -> f (a, b)
- 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
- 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
- patUnbind :: (Alpha p, Alpha t) => p -> Bind p t -> t
- unsafeUnbind :: (Alpha a, Alpha b) => GenBind order card a b -> (a, b)

# Documentation

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

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

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

Given a list of names and a term, close the term with those names where the indices of the bound variables occur in sequential order and return the equivalent ordering of the names, dropping those that do not occur in the term at all For example: permClose b,c = ([b,c], (0,1)) -- standard close permClose b,c = ([c,b], (0,1)) -- vars reordered permClose a,b,c = ([c,b], (0,1)) -- var dropped permClose a,b,c = ([c,b], (0,1,0)) -- additional occurrence ok

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

Variant of permClose for dynamically typed names

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

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

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

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

Constructor for rebinding patterns.

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

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

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

Destructor for recursive abstractions which picks *locally* fresh
names for binders (see `LFresh`

).

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

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

An alpha-respecting total order on terms involving binders.

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

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 AnyName Source #

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 AnyName Source #

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 -> p Source #

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

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

"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 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 c Source #

`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 Source #

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

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 #

Unbind two binders with the same names, fail if the number of required
names and their sorts does not match. See `unbind2`

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 #

Unbind three binders with the same names, fail if the number of required
names and their sorts does not match. See `unbind3`

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

See `lunbind2`

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

See `lunbind3`

patUnbind :: (Alpha p, Alpha t) => p -> Bind p t -> t Source #

A destructor for binders that does *not* guarantee fresh names
for the binders. Instead it uses the names in the provided pattern.

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. Instead, it uses the original names from
when the binder was constructed.