Portability | non-portable (-XKitchenSink) |
---|---|

Stability | experimental |

Maintainer | Stephanie Weirich <sweirich@cis.upenn.edu> |

A generic implementation of name binding functions using a locally
nameless representation. Datatypes with binding can be defined
using the `Name`

and `Bind`

types. Expressive patterns for binding
come from the `Annot`

and `Rebind`

types.

Important classes are:

Name generation is controlled via monads which implement the
`Fresh`

and `LFresh`

classes.

- data Name a
- data AnyName = forall a . Rep a => AnyName (Name a)
- data Bind a b
- newtype Annot a = Annot a
- data Rebind a b
- integer2Name :: Rep a => Integer -> Name a
- string2Name :: Rep a => String -> Name a
- makeName :: Rep a => String -> Integer -> Name a
- name2Integer :: Name a -> Integer
- name2String :: Name a -> String
- anyName2Integer :: AnyName -> Integer
- anyName2String :: AnyName -> String
- name1 :: Rep a => Name a
- name2 :: Rep a => Name a
- name3 :: Rep a => Name a
- name4 :: Rep a => Name a
- name5 :: Rep a => Name a
- name6 :: Rep a => Name a
- name7 :: Rep a => Name a
- name8 :: Rep a => Name a
- name9 :: Rep a => Name a
- name10 :: Rep a => Name a
- class (Show a, Rep1 AlphaD a) => Alpha a where
- swaps' :: AlphaCtx -> Perm AnyName -> a -> a
- fv' :: AlphaCtx -> a -> Set AnyName
- lfreshen' :: LFresh m => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b
- freshen' :: Fresh m => AlphaCtx -> a -> m (a, Perm AnyName)
- match' :: AlphaCtx -> a -> a -> Maybe (Perm AnyName)
- close :: Alpha b => AlphaCtx -> b -> a -> a
- open :: Alpha b => AlphaCtx -> b -> a -> a
- nthpatrec :: a -> Integer -> (Integer, Maybe AnyName)
- findpatrec :: a -> AnyName -> (Integer, Bool)

- swaps :: Alpha a => Perm AnyName -> a -> a
- swapsAnnots :: Alpha a => Perm AnyName -> a -> a
- swapsBinders :: Alpha a => Perm AnyName -> a -> a
- match :: Alpha a => a -> a -> Maybe (Perm AnyName)
- matchAnnots :: Alpha a => a -> a -> Maybe (Perm AnyName)
- matchBinders :: Alpha a => a -> a -> Maybe (Perm AnyName)
- fv :: (Rep b, Alpha a) => a -> Set (Name b)
- patfv :: (Rep a, Alpha b) => b -> Set (Name a)
- binders :: (Rep a, Alpha b) => b -> Set (Name a)
- aeq :: Alpha a => a -> a -> Bool
- aeqBinders :: Alpha a => a -> a -> Bool
- bind :: (Alpha b, Alpha c) => b -> c -> Bind b c
- unsafeUnBind :: (Alpha a, Alpha b) => Bind a b -> (a, b)
- class Monad m => Fresh m where
- freshen :: (Fresh m, Alpha a) => a -> m (a, Perm AnyName)
- unbind :: (Fresh m, Alpha b, Alpha c) => Bind b c -> m (b, c)
- unbind2 :: (Fresh m, Alpha b, Alpha c, Alpha d) => Bind b c -> Bind b d -> m (Maybe (b, c, d))
- unbind3 :: (Fresh m, Alpha b, Alpha c, Alpha d, Alpha e) => Bind b c -> Bind b d -> Bind b e -> m (Maybe (b, c, d, e))
- class HasNext m where
- nextInteger :: m Integer
- resetNext :: Integer -> m ()

- class Monad m => LFresh m where
- lfreshen :: (Alpha a, LFresh m) => a -> (a -> Perm AnyName -> m b) -> m b
- lunbind :: (LFresh m, Alpha a, Alpha b) => Bind a b -> ((a, b) -> m c) -> m c
- lunbind2 :: (LFresh m, Alpha b, Alpha c, Alpha d) => Bind b c -> Bind b d -> (Maybe (b, c, d) -> m e) -> m e
- lunbind3 :: (LFresh m, Alpha b, Alpha c, Alpha d, Alpha e) => Bind b c -> Bind b d -> Bind b e -> (Maybe (b, c, d, e) -> m f) -> m f
- rebind :: (Alpha a, Alpha b) => a -> b -> Rebind a b
- reopen :: (Alpha a, Alpha b) => Rebind a b -> (a, b)
- class Rep1 (SubstD b) a => Subst b a where
- abs_swaps :: t -> t1 -> t2 -> t2
- abs_fv :: t -> t1 -> Set a
- abs_freshen :: Monad m => t -> t1 -> m (t1, Perm a)
- abs_match :: Eq a => t -> a -> a -> Maybe (Perm a1)
- abs_nthpatrec :: t -> t1 -> (t1, Maybe a)
- abs_findpatrec :: Num a => t -> t1 -> (a, Bool)
- abs_close :: t -> t1 -> t2 -> t2
- abs_open :: t -> t1 -> t2 -> t2
- data AlphaCtx
- matchR1 :: R1 AlphaD a -> AlphaCtx -> a -> a -> Maybe (Perm AnyName)
- rName :: forall a[aKgL]. Rep a[aKgL] => R (Name a[aKgL])
- rBind :: forall a[aKgI] b[aKgJ]. (Rep a[aKgI], Rep b[aKgJ]) => R (Bind a[aKgI] b[aKgJ])
- rRebind :: forall a[aKgD] b[aKgE]. (Rep a[aKgD], Rep b[aKgE]) => R (Rebind a[aKgD] b[aKgE])
- rAnnot :: forall a[aKgF]. Rep a[aKgF] => R (Annot a[aKgF])

# Basic types

`Name`

s are things that get bound. This type is intentionally
abstract; to create a `Name`

you can use `string2Name`

or
`integer2Name`

. The type parameter is a tag, or *sort*, which tells
us what sorts of things this name may stand for. The sort must
be an instance of the `Rep`

type class.

A name with a hidden (existentially quantified) sort.

The type of a binding. We can `Bind`

an `a`

object in a `b`

object if we can create "fresh" `a`

objects, and `a`

objects
can occur unbound in `b`

objects. Often `a`

is `Name`

but that
need not be the case.

Like `Name`

, `Bind`

is also abstract. You can create bindings
using `bind`

and take them apart with `unbind`

and friends.

(Rep a[aKgI], Rep b[aKgJ], Sat (ctx[aKnS] a[aKgI]), Sat (ctx[aKnS] b[aKgJ])) => Rep1 ctx[aKnS] (Bind a[aKgI] b[aKgJ]) | |

(Subst c b, Subst c a, Alpha a, Alpha b) => Subst c (Bind a b) | |

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

(Show a, Show b) => Show (Bind a b) | |

(Rep a[aKgI], Rep b[aKgJ]) => Rep (Bind a[aKgI] b[aKgJ]) | |

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

An annotation is a "hole" in a pattern where variables can be used, but not bound. For example, patterns may include type annotations, and those annotations can reference variables without binding them. Annotations do nothing special when they appear elsewhere in terms.

Annot a |

`Rebind`

supports "telescopes" --- that is, patterns where
bound variables appear in multiple subterms.

(Rep a[aKgD], Rep b[aKgE], Sat (ctx[aKn5] a[aKgD]), Sat (ctx[aKn5] b[aKgE])) => Rep1 ctx[aKn5] (Rebind a[aKgD] b[aKgE]) | |

(Subst c b, Subst c a, Alpha a, Alpha b) => Subst c (Rebind a b) | |

(Alpha a, Alpha b, Eq b) => Eq (Rebind a b) | Compare for alpha-equality. |

(Show a, Show b) => Show (Rebind a b) | |

(Rep a[aKgD], Rep b[aKgE]) => Rep (Rebind a[aKgD] b[aKgE]) | |

(Alpha a, Alpha b) => Alpha (Rebind a b) |

## Utilities

makeName :: Rep a => String -> Integer -> Name aSource

Create a `Name`

from a `String`

and an `Integer`

index.

name2Integer :: Name a -> IntegerSource

Get the integer index of a `Name`

.

name2String :: Name a -> StringSource

Get the string part of a `Name`

.

anyName2Integer :: AnyName -> IntegerSource

Get the integer index of an `AnyName`

.

anyName2String :: AnyName -> StringSource

Get the string part of an `AnyName`

.

# The `Alpha`

class

class (Show a, Rep1 AlphaD a) => Alpha a whereSource

The `Alpha`

type class is for types which may contain names. The
`Rep1`

constraint means that we can only make instances of this
class for types that have generic representations (which can be
automatically derived by RepLib.)

Note that the methods of `Alpha`

should never be called directly!
Instead, use other methods provided by this module which are
defined in terms of `Alpha`

methods. (The only reason they are
exported is to make them available to automatically-generated
code.)

Most of the time, the default definitions of these methods will suffice, so you can make an instance for your data type by simply declaring

instance Alpha MyType

swaps' :: AlphaCtx -> Perm AnyName -> a -> aSource

See `swaps`

.

fv' :: AlphaCtx -> a -> Set AnyNameSource

See `fv`

.

lfreshen' :: LFresh m => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m bSource

See `lfreshen`

.

freshen' :: Fresh m => AlphaCtx -> a -> m (a, Perm AnyName)Source

See `freshen`

.

match' :: AlphaCtx -> a -> a -> Maybe (Perm AnyName)Source

close :: Alpha b => AlphaCtx -> b -> a -> aSource

Replace free names by bound names.

open :: Alpha b => AlphaCtx -> b -> a -> aSource

Replace bound names by free names.

nthpatrec :: a -> Integer -> (Integer, Maybe AnyName)Source

looks up the `nthpatrec`

b n`n`

th name in the pattern `b`

(zero-indexed), returning the number of names encountered if not
found.

findpatrec :: a -> AnyName -> (Integer, Bool)Source

Alpha Bool | |

Alpha Char | |

Alpha Double | |

Alpha Float | |

Alpha Int | |

Alpha Integer | |

Alpha () | |

Alpha AnyName | |

Alpha Exp | |

Alpha a => Alpha [a] | |

Alpha a => Alpha (Maybe a) | |

Rep a => Alpha (R a) | |

Alpha a => Alpha (Annot a) | |

Rep a => Alpha (Name a) | |

(Alpha a, Alpha b) => Alpha (Either a b) | |

(Alpha a, Alpha b) => Alpha (a, b) | |

(Alpha a, Alpha b) => Alpha (Rebind a b) | |

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

(Alpha a, Alpha b, Alpha c) => Alpha (a, b, c) | |

(Alpha a, Alpha b, Alpha c, Alpha d) => Alpha (a, b, c, d) | |

(Alpha a, Alpha b, Alpha c, Alpha d, Alpha e) => Alpha (a, b, c, d, e) |

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

Apply a permutation to the annotations in a pattern. Binding names are left alone by the permutation.

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

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

match :: Alpha a => a -> a -> Maybe (Perm AnyName)Source

Compare two data structures and produce a permutation of their
`Name`

s that will make them alpha-equivalent to each other (`Name`

s
that appear in annotations must match exactly). Return `Nothing`

if no such renaming is possible. Note that two terms are
alpha-equivalent if the empty permutation is returned.

matchAnnots :: Alpha a => a -> a -> Maybe (Perm AnyName)Source

Compare two patterns, ignoring the names of binders, and produce
a permutation of their annotations to make them alpha-equivalent
to eachother. Return `Nothing`

if no such renaming is possible.

fv :: (Rep b, Alpha a) => a -> Set (Name b)Source

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

patfv :: (Rep a, Alpha b) => b -> Set (Name a)Source

List variables of a particular sort that occur freely in annotations (not bindings).

binders :: (Rep a, Alpha b) => b -> Set (Name a)Source

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

aeqBinders :: Alpha a => a -> a -> BoolSource

Determine (alpha-)equivalence of patterns

# Binding operations

bind :: (Alpha b, Alpha c) => 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.

# The `Fresh`

class

unbind :: (Fresh m, Alpha b, Alpha c) => Bind b c -> m (b, c)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 b, Alpha c, Alpha d) => Bind b c -> Bind b d -> m (Maybe (b, c, d))Source

Unbind two terms with the same fresh names, provided the binders match.

unbind3 :: (Fresh m, Alpha b, Alpha c, Alpha d, Alpha e) => Bind b c -> Bind b d -> Bind b e -> m (Maybe (b, c, d, e))Source

# The `LFresh`

class

Type class for contexts which can generate new globally fresh integers.

class Monad m => LFresh m whereSource

This is the class of monads that support freshness in an (implicit) local scope. Generated names are fresh for the current local scope, but not globally fresh. This class has a basic instance based on the reader monad.

lfreshen :: (Alpha a, LFresh m) => a -> (a -> Perm AnyName -> m b) -> m bSource

"Locally" freshen a term. TODO: explain this type signature a bit better.

lunbind :: (LFresh m, Alpha a, Alpha b) => Bind a b -> ((a, b) -> m c) -> m cSource

Destruct a binding in an `LFresh`

monad.

lunbind2 :: (LFresh m, Alpha b, Alpha c, Alpha d) => Bind b c -> Bind b d -> (Maybe (b, c, d) -> m e) -> m eSource

Unbind two terms with the same fresh names, provided the binders match.

lunbind3 :: (LFresh m, Alpha b, Alpha c, Alpha d, Alpha e) => Bind b c -> Bind b d -> Bind b e -> (Maybe (b, c, d, e) -> m f) -> m fSource

Unbind three terms with the same fresh names, provided the binders match.

# Rebinding operations

reopen :: (Alpha a, Alpha b) => Rebind a b -> (a, b)Source

destructor for binding patterns, the names should have already been freshened.

# Substitution

class Rep1 (SubstD b) a => Subst b a whereSource

The `Subst`

class governs capture-avoiding substitution. To
derive this class, you only need to indicate where the variables
are in the data type, by overriding the method `isvar`

.

isvar :: a -> Maybe (Name b, b -> a)Source

If the argument is a variable, return its name and a function
to generate a substituted term. Return `Nothing`

for
non-variable arguments.

subst :: Name b -> b -> a -> aSource

substitutes `subst`

nm sub tm`sub`

for `nm`

in `tm`

.

substs :: [Name b] -> [b] -> a -> aSource

Perform several simultaneous substitutions.

Subst b AnyName | |

Subst b Double | |

Subst b Float | |

Subst b Integer | |

Subst b Char | |

Subst b () | |

Subst b Bool | |

Subst b Int | |

Subst Exp Exp | |

Subst c a => Subst c (Annot a) | |

Subst c a => Subst c (Maybe a) | |

Subst c a => Subst c [a] | |

Rep a => Subst b (Name a) | |

Rep a => Subst b (R a) | |

(Subst c b, Subst c a, Alpha a, Alpha b) => Subst c (Rebind a b) | |

(Subst c b, Subst c a, Alpha a, Alpha b) => Subst c (Bind a b) | |

(Subst c a, Subst c b) => Subst c (Either a b) | |

(Subst c a, Subst c b) => Subst c (a, b) | |

(Subst c a, Subst c b, Subst c d) => Subst c (a, b, d) | |

(Subst c a, Subst c b, Subst c d, Subst c e) => Subst c (a, b, d, e) | |

(Subst c a, Subst c b, Subst c d, Subst c e, Subst c f) => Subst c (a, b, d, e, f) |

# For abstract types

abs_freshen :: Monad m => t -> t1 -> m (t1, Perm a)Source

abs_nthpatrec :: t -> t1 -> (t1, Maybe a)Source

abs_findpatrec :: Num a => t -> t1 -> (a, Bool)Source

# Advanced

Match returns a permutation ordering. Either the terms are known to be LT or GT, or there is some permutation that can make them equal to eachother data POrdering = PLT | PEq (Perm AnyName) | PGT

Many of the operations in the `Alpha`

class take an `AlphaCtx`

:
stored information about the iteration as it progresses. This type
is abstract, as classes that override these operations should just pass
the context on.

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