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) => Bind a b -> (a, b)
- 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) => Bind p t -> m (p, t)
- unbind2 :: (Fresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => Bind p1 t1 -> Bind p2 t2 -> m (Maybe (p1, t1, p2, t2))
- 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))
- lunbind :: (LFresh m, Alpha p, Alpha t) => Bind p t -> ((p, t) -> m c) -> m c
- 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
- 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

# 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) => Bind a b -> (a, b)Source

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

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) => Bind 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) => Bind p1 t1 -> Bind 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) => Bind p1 t1 -> Bind p2 t2 -> Bind 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) => Bind 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) => Bind p1 t1 -> Bind p2 t2 -> (Maybe (p1, t1, p2, t2) -> m r) -> m rSource