Copyright | (c) 2014 Aleksey Kliger |
---|---|

License | BSD3 (See LICENSE) |

Maintainer | Aleksey Kliger |

Stability | experimental |

Safe Haskell | None |

Language | Haskell2010 |

Operations on terms and patterns that contain names.

## Synopsis

- aeq :: Alpha a => a -> a -> Bool
- acompare :: Alpha a => a -> a -> Ordering
- fvAny :: (Alpha a, Contravariant f, Applicative f) => (AnyName -> f AnyName) -> a -> f a
- fv :: forall a f b. (Alpha a, Typeable b, Contravariant f, Applicative f) => (Name b -> f (Name b)) -> a -> f a
- freshen :: (Alpha p, Fresh m) => p -> m (p, Perm AnyName)
- lfreshen :: (Alpha p, LFresh m) => p -> (p -> Perm AnyName -> m b) -> m b
- swaps :: Alpha t => Perm AnyName -> t -> t
- data Bind p t
- bind :: (Alpha p, Alpha t) => p -> t -> Bind p t
- unbind :: (Alpha p, Alpha t, Fresh m) => Bind p t -> m (p, t)
- lunbind :: (LFresh m, Alpha p, Alpha t) => Bind p t -> ((p, t) -> m c) -> m c
- unbind2 :: (Fresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => Bind p1 t1 -> Bind p2 t2 -> m (Maybe (p1, t1, p2, t2))
- lunbind2 :: (LFresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => Bind p1 t1 -> Bind p2 t2 -> (Maybe (p1, t1, p2, t2) -> m c) -> m c
- unbind2Plus :: (MonadPlus m, Fresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => Bind p1 t1 -> Bind p2 t2 -> m (p1, t1, p2, t2)
- data Rebind p1 p2
- rebind :: (Alpha p1, Alpha p2) => p1 -> p2 -> Rebind p1 p2
- unrebind :: (Alpha p1, Alpha p2) => Rebind p1 p2 -> (p1, p2)
- newtype Embed t = Embed t
- class IsEmbed e where
- embed :: IsEmbed e => Embedded e -> e
- unembed :: IsEmbed e => e -> Embedded e
- data Rec p
- rec :: Alpha p => p -> Rec p
- unrec :: Alpha p => Rec p -> p
- newtype TRec p = TRec (Bind (Rec p) ())
- trec :: Alpha p => p -> TRec p
- untrec :: (Alpha p, Fresh m) => TRec p -> m p
- luntrec :: (Alpha p, LFresh m) => TRec p -> m p
- data Ignore t
- ignore :: t -> Ignore t
- unignore :: Ignore t -> t

# Equivalence, free variables, freshness

aeq :: Alpha a => a -> a -> Bool Source #

returns `aeq`

t1 t2`True`

iff `t1`

and `t2`

are alpha-equivalent terms.

acompare :: Alpha a => a -> a -> Ordering Source #

An alpha-respecting total order on terms involving binders.

fvAny :: (Alpha a, Contravariant f, Applicative f) => (AnyName -> f AnyName) -> a -> f a Source #

returns a fold over any names in a term `fvAny`

`a`

.

fvAny :: Alpha a => Fold a AnyName

fv :: forall a f b. (Alpha a, Typeable b, Contravariant f, Applicative f) => (Name b -> f (Name b)) -> a -> f a Source #

returns the free `fv`

`b`

variables of term `a`

.

fv :: (Alpha a, Typeable b) => Fold a (Name b)

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.

swaps :: Alpha t => Perm AnyName -> t -> t Source #

Apply the given permutation of variable names to the given term.

# Binding, unbinding

A term of type

is a term that binds the free
variable occurrences of the variables in pattern `Bind`

p t`p`

in the term
`t`

. In the overall term, those variables are now bound. See also
`bind`

and
`unbind`

and
`lunbind`

## Instances

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

closes over the variables of pattern `bind`

p t`p`

in the term `t`

lunbind :: (LFresh m, Alpha p, Alpha t) => Bind 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.

unbind2 :: (Fresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => Bind p1 t1 -> Bind p2 t2 -> m (Maybe (p1, t1, p2, t2)) Source #

Simultaneously unbind two patterns in two terms, returning `Nothing`

if
the two patterns don't bind the same number of variables.

lunbind2 :: (LFresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => Bind p1 t1 -> Bind p2 t2 -> (Maybe (p1, t1, p2, t2) -> m c) -> m c Source #

unbind2Plus :: (MonadPlus m, Fresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => Bind p1 t1 -> Bind p2 t2 -> m (p1, t1, p2, t2) Source #

Simultaneously unbind two patterns in two terms, returning `mzero`

if
the patterns don't bind the same number of variables.

# Rebinding, embedding

is a pattern that binds the names of `Rebind`

p1 p2`p1`

and `p2`

, and additionally
brings the names of `p1`

into scope over `p2`

.

This may be used, for example, to faithfully represent Scheme's `let*`

binding form, defined by:

(let* () body) ≙ body (let* ([v1, e1] binds ...) body) ≙ (let ([v1, e1]) (let* (binds ...) body))

using the following AST:

type Var = Name Expr data Lets = EmptyLs | ConsLs (Rebind (Var, Embed Expr) Lets) data Expr = ... | LetStar (Bind Lets Expr) | ...

## Instances

`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

unembed :: IsEmbed e => e -> Embedded e Source #

extracts the term embedded in the pattern `unembed`

p`p`

.

# Recursive bindings

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.

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

.

## Instances

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

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

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

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

).

# Opaque terms

Ignores a term `t`

for the purpose of alpha-equality and substitution