- bind :: (Alpha c, Alpha b) => b -> c -> Bind b c
- unsafeUnbind :: (Alpha a, Alpha b) => Bind a b -> (a, b)
- rebind :: (Alpha a, Alpha b) => a -> b -> Rebind a b
- unrebind :: (Alpha a, Alpha b) => Rebind a b -> (a, b)
- rec :: Alpha a => a -> Rec a
- unrec :: Alpha a => Rec a -> a
- 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 a => Perm AnyName -> a -> a
- swapsBinders :: Alpha a => Perm AnyName -> a -> a
- swapsEmbeds :: Alpha a => Perm AnyName -> a -> a
- 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 c, Alpha b) => b -> c -> Bind b cSource

A smart constructor for binders, also sometimes known as "close".

unsafeUnbind :: (Alpha a, Alpha b) => Bind a b -> (a, b)Source

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

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

Determine (alpha-)equivalence of patterns. Do they bind the same variables and have alpha-equal annotations?

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 within pattern annotations (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 pattern annotations (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 a => Perm AnyName -> a -> aSource

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

swapsEmbeds :: Alpha a => Perm AnyName -> a -> aSource

Apply a permutation to the annotations 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 have not already been used. The second argument is a continuation, which takes the renamed term and a permutation that specifies how the pattern has been renamed.

unbind :: (Fresh m, Alpha p, Alpha t) => Bind p t -> m (p, t)Source

Unbind (also known as "open") is the destructor for bindings. It ensures that the names in the binding are fresh.

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.

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.

lunbind :: (LFresh m, Alpha p, Alpha t) => Bind p t -> ((p, t) -> m c) -> m cSource

Destruct a binding in an `LFresh`

monad.