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

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

Stability | experimental |

Portability | GHC only |

Safe Haskell | None |

Language | Haskell2010 |

Special type combinators for specifying binding structure.

## Synopsis

- data GenBind order card p t = B p t
- type Bind p t = GenBind StrictOrder StrictCard p t
- type SetBind p t = GenBind RelaxedOrder StrictCard p t
- type SetPlusBind p t = GenBind RelaxedOrder RelaxedCard p t
- data Rebind p1 p2 = R p1 p2
- data Rec p = Rec p
- newtype TRec p = TRec (Bind (Rec p) ())
- newtype Embed t = Embed t
- newtype Shift p = Shift p
- module Unbound.LocallyNameless.Name
- rGenBind :: forall order card p t. (Rep order, Rep card, Rep p, Rep t) => R (GenBind order card p t)
- rRebind :: forall p1 p2. (Rep p1, Rep p2) => R (Rebind p1 p2)
- rEmbed :: forall t. Rep t => R (Embed t)
- rRec :: forall p. Rep p => R (Rec p)
- rShift :: forall p. Rep p => R (Shift p)

# Documentation

data GenBind order card p t Source #

Generic binding combinator for a pattern `p`

within a term `t`

.
Flexible over the order and cardinality of the variables bound
in the pattern

B p t |

## Instances

(Rep order, Rep card, Rep p, Rep t, Sat (ctx p), Sat (ctx t)) => Rep1 ctx (GenBind order card p t) Source # | |

Defined in Unbound.LocallyNameless.Types | |

(Rep order, Rep card, Alpha p, Alpha t, Subst b p, Subst b t) => Subst b (GenBind order card p t) Source # | |

Defined in Unbound.LocallyNameless.Subst isvar :: GenBind order card p t -> Maybe (SubstName (GenBind order card p t) b) Source # isCoerceVar :: GenBind order card p t -> Maybe (SubstCoerce (GenBind order card p t) b) Source # subst :: Name b -> b -> GenBind order card p t -> GenBind order card p t Source # substs :: [(Name b, b)] -> GenBind order card p t -> GenBind order card p t Source # substPat :: AlphaCtx -> b -> GenBind order card p t -> GenBind order card p t Source # substPats :: Proxy b -> AlphaCtx -> [Dyn] -> GenBind order card p t -> GenBind order card p t Source # | |

(Alpha a, Alpha b, Read a, Read b) => Read (Bind a b) # | |

(Show a, Show b) => Show (GenBind order card a b) Source # | |

(Rep order, Rep card, Rep p, Rep t) => Rep (GenBind order card p t) Source # | |

Defined in Unbound.LocallyNameless.Types | |

(Binary p, Binary t) => Binary (GenBind order card p t) Source # | |

(Rep order, Rep card, Alpha p, Alpha t) => Alpha (GenBind order card p t) Source # | |

Defined in Unbound.LocallyNameless.Alpha swaps' :: AlphaCtx -> Perm AnyName -> GenBind order card p t -> GenBind order card p t Source # fv' :: Collection f => AlphaCtx -> GenBind order card p t -> f AnyName Source # lfreshen' :: LFresh m => AlphaCtx -> GenBind order card p t -> (GenBind order card p t -> Perm AnyName -> m b) -> m b Source # freshen' :: Fresh m => AlphaCtx -> GenBind order card p t -> m (GenBind order card p t, Perm AnyName) Source # aeq' :: AlphaCtx -> GenBind order card p t -> GenBind order card p t -> Bool Source # acompare' :: AlphaCtx -> GenBind order card p t -> GenBind order card p t -> Ordering Source # close :: Alpha b => AlphaCtx -> b -> GenBind order card p t -> GenBind order card p t Source # open :: Alpha b => AlphaCtx -> b -> GenBind order card p t -> GenBind order card p t Source # isPat :: GenBind order card p t -> Maybe [AnyName] Source # isTerm :: GenBind order card p t -> Bool Source # isEmbed :: GenBind order card p t -> Bool Source # nthpatrec :: GenBind order card p t -> NthCont Source # findpatrec :: GenBind order card p t -> AnyName -> FindResult Source # |

type SetBind p t = GenBind RelaxedOrder StrictCard p t Source #

A variant of `Bind`

where alpha-equivalence allows multiple
variables bound in the same pattern to be reordered

type SetPlusBind p t = GenBind RelaxedOrder RelaxedCard p t Source #

A variant of `Bind`

where alpha-equivalence allows multiple
variables bound in the same pattern to be reordered, and
allows the binding of unused variables
For example, { a b c } . a b `aeq`

{ b a } . a b

`Rebind`

allows for *nested* bindings. If `p1`

and `p2`

are
pattern types, then `Rebind p1 p2`

is also a pattern type,
similar to the pattern type `(p1,p2)`

except that `p1`

*scopes over* `p2`

. That is, names within terms embedded in `p2`

may refer to binders in `p1`

.

R p1 p2 |

## Instances

If `p`

is a pattern type, then `Rec p`

is also a pattern type,
which is *recursive* in the sense that `p`

may bind names in terms
embedded within itself. Useful for encoding e.g. lectrec and
Agda's dot notation.

Rec p |

## Instances

`TRec`

is a standalone variant of `Rec`

: the only difference is
that whereas

is a pattern type, `Rec`

p`TRec p`

is a *term type*. It is isomorphic to

.`Bind`

(`Rec`

p) ()

Note that `TRec`

corresponds to Pottier's *abstraction* construct
from alpha-Caml. In this context,

corresponds to
alpha-Caml's `Embed`

t`inner t`

, and

corresponds to
alpha-Caml's `Shift`

(`Embed`

t)`outer t`

.

`Embed`

allows for terms to be *embedded* within patterns. Such
embedded terms do not bind names along with the rest of the
pattern. For examples, see the tutorial or examples directories.

If `t`

is a *term type*, then `Embed t`

is a *pattern type*.

`Embed`

is not abstract since it involves no binding, and hence
it is safe to manipulate directly. To create and destruct
`Embed`

terms, you may use the `Embed`

constructor directly.
(You may also use the functions `embed`

and `unembed`

, which
additionally can construct or destruct any number of enclosing
`Shift`

s at the same time.)

Embed t |

## Instances

Shift the scope of an embedded term one level outwards.

Shift p |

## Instances

module Unbound.LocallyNameless.Name

# Pay no attention to the man behind the curtain

These type representation objects are exported so they can be referenced by auto-generated code. Please pretend they do not exist.

rGenBind :: forall order card p t. (Rep order, Rep card, Rep p, Rep t) => R (GenBind order card p t) Source #