Unbound.LocallyNameless.Ops

Documentation

bind :: (Alpha c, Alpha b) => b -> c -> Bind b c

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

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

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

rebind :: (Alpha a, Alpha b) => a -> b -> Rebind a b

Constructor for binding in patterns.

unrebind :: (Alpha a, Alpha b) => Rebind a b -> (a, b)

Destructor for Rebind. 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 open must have already freshened the names at this point.

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

Determine alpha-equivalence of terms.

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

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

acompare :: Alpha t => t -> t -> Ordering

An alpha-respecting total order on terms involving binders.

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

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

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

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

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

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)

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 AnyName

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

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

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

swaps :: Alpha a => Perm AnyName -> a -> a

Apply a permutation to a term.

swapsBinders :: Alpha a => Perm AnyName -> a -> a

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

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

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 b

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

freshen :: (Alpha p, Fresh m) => p -> m (p, Perm AnyName)

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) => Bind p t -> m (p, t)

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

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

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 c

Destruct a binding in an LFresh monad.

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

Unbind two terms with the same fresh names, provided the binders have the same number of binding variables.

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

Unbind three terms with the same fresh names, provided the binders have the same number of binding variables.