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

Stability | experimental |

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

A generic implementation of standard functions dealing with names and binding structure (alpha equivalence, free variable calculation, capture-avoiding substitution, name permutation, ...) using a nominal representation.

DISCLAIMER: this module almost certainly contains bugs and may be slower than Unbound.LocallyNameless. The documentation is also sparse and likely out of date. At this point we recommend it only for the curious or intrepid. We are actively working on bringing it up to speed as a viable alternative to Unbound.LocallyNameless.

- data Name a
- data AnyName = forall a . Rep a => AnyName (Name a)
- data Bind a b
- newtype Embed a = Embed a
- data Rebind a b
- data Rec a
- data Shift a
- integer2Name :: Rep a => Integer -> Name a
- string2Name :: Rep a => String -> Name a
- name2Integer :: Name a -> Integer
- name2String :: Name a -> String
- makeName :: Rep a => String -> Integer -> Name a
- 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
- translate :: Rep b => Name a -> Name b
- class Rep1 AlphaD a => Alpha a where
- aeq' :: AlphaCtx -> a -> a -> Bool
- swapall' :: AlphaCtx -> Perm AnyName -> a -> a
- swaps' :: AlphaCtx -> Perm AnyName -> a -> a
- fv' :: AlphaCtx -> a -> Set AnyName
- binders' :: AlphaCtx -> a -> [AnyName]
- match' :: AlphaCtx -> a -> a -> Maybe (Perm AnyName)
- freshen' :: Fresh m => AlphaCtx -> a -> m (a, Perm AnyName)
- lfreshen' :: LFresh m => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b

- swaps :: Alpha a => Perm AnyName -> a -> a
- match :: Alpha a => a -> a -> Maybe (Perm AnyName)
- binders :: (Rep b, Alpha b) => b -> [AnyName]
- patfv :: (Rep a, Alpha b) => b -> Set (Name a)
- fv :: (Rep b, Alpha a) => a -> Set (Name b)
- aeq :: Alpha a => a -> a -> Bool
- bind :: (Alpha b, Alpha c) => b -> c -> Bind b c
- unsafeUnbind :: Bind a b -> (a, b)
- class (Monad m, HasNext m) => Fresh m where
- freshen :: (Fresh m, Alpha a) => a -> m (a, Perm AnyName)
- unbind :: (Alpha b, Fresh m, 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 Monad m => 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 -> m (a, b)
- lunbind2 :: (LFresh m, Alpha b, Alpha c, Alpha d) => Bind b c -> Bind b d -> m (Maybe (b, c, d))
- lunbind3 :: (LFresh m, Alpha b, Alpha c, Alpha d, Alpha e) => Bind b c -> Bind b d -> Bind b e -> m (Maybe (b, c, d, e))
- rebind :: (Alpha a, Alpha b) => a -> b -> Rebind a b
- reopen :: (Alpha a, Alpha b) => Rebind a b -> (a, b)
- rec :: Alpha a => a -> Rec a
- unrec :: Alpha a => Rec a -> a
- class Rep1 (SubstD b) a => Subst b a where
- data AlphaCtx
- matchR1 :: R1 AlphaD a -> AlphaCtx -> a -> a -> Maybe (Perm AnyName)
- rName :: forall a[a1Ev]. Rep a[a1Ev] => R (Name a[a1Ev])
- rBind :: forall a[a5FT] b[a5FU]. (Rep a[a5FT], Rep b[a5FU]) => R (Bind a[a5FT] b[a5FU])
- rRebind :: forall a[a5FP] b[a5FQ]. (Rep a[a5FP], Rep b[a5FQ]) => R (Rebind a[a5FP] b[a5FQ])
- rEmbed :: forall a[a5FS]. Rep a[a5FS] => R (Embed a[a5FS])
- rRec :: forall a[a5FO]. Rep a[a5FO] => R (Rec a[a5FO])
- rShift :: forall a[a5FR]. Rep a[a5FR] => R (Shift a[a5FR])

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

Type of a binding. Morally, the type a should be in the
class `Pattern`

and the type b should be in the class `Alpha`

.
The Pattern class contains the constructor and a safe
destructor for these types.
We can Bind an a object in a b object if we
can create fresh a objects, and Names can be
swapped in b objects. Often a is Name
but that need not be the case.

(Rep a[a5FT], Rep b[a5FU], Sat (ctx[a5QY] a[a5FT]), Sat (ctx[a5QY] b[a5FU])) => Rep1 ctx[a5QY] (Bind a[a5FT] b[a5FU]) | |

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

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

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

(Rep a[a5FT], Rep b[a5FU]) => Rep (Bind a[a5FT] b[a5FU]) | |

(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

Embed a |

Rebinding is for telescopes --- i.e. to support patterns that also bind variables that appear later

(Rep a[a5FP], Rep b[a5FQ], Sat (ctx[a5Qq] a[a5FP]), Sat (ctx[a5Qq] (Bind [AnyName] b[a5FQ]))) => Rep1 ctx[a5Qq] (Rebind a[a5FP] b[a5FQ]) | |

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

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

(Rep a[a5FP], Rep b[a5FQ]) => Rep (Rebind a[a5FP] b[a5FQ]) | |

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

`Rec`

supports recursive patterns --- that is, patterns where
any variables anywhere in the pattern are bound in the pattern
itself. Useful for lectrec (and Agda's dot notation).

Shift the scope of an embedded term one level outwards.

## Utilities

name2Integer :: Name a -> IntegerSource

Get the integer index of a `Name`

.

name2String :: Name a -> StringSource

Get the string part of a `Name`

.

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

Create a `Name`

from a `String`

and an `Integer`

index.

# The `Alpha`

class

class Rep1 AlphaD a => Alpha a whereSource

The Alpha class is for all terms that may contain binders
The `Rep1`

class constraint means that we can only
make instances of this class for types that have
generic representations. (Derive these using TH and
RepLib.)

aeq' :: AlphaCtx -> a -> a -> BoolSource

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

swap everything, including bound and free variables, parts in annots, etc.

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

The method swaps' applys a compound permutation

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

calculate the free variables (aka support)

binders' :: AlphaCtx -> a -> [AnyName]Source

list the binding variables in a pattern, in order

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

Match' compares two data structures and produces a permutation of their free variables that will make them alpha-equivalent to eachother.

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

An object of type a can be freshened if a new copy of a can be produced where all old Names in a are replaced with new fresh Names, and the permutation reports which names were swapped by others.

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

See `lfreshen`

Alpha Bool | |

Alpha Char | |

Alpha Double | |

Alpha Float | |

Alpha Int | |

Alpha Integer | |

Alpha () | |

Alpha AnyName | |

Alpha Exp | |

Alpha a => Alpha [a] | |

Rep a => Alpha (R a) | |

Alpha a => Alpha (Maybe a) | |

Rep a => Alpha (Name a) | |

(Eq a, Alpha a) => Alpha (Embed 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) |

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

The method swaps applys a permutation to all free variables in the term.

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

Match compares two data structures and produces a permutation of their Names that will make them alpha-equivalent to eachother. (Names that appear in annotations must match exactly.) Also note that two terms are alpha-equivalent when the empty permutation is returned.

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

Set of variables that occur freely in annotations (not binding)

# Binding operations

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

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

# The `Fresh`

class

unbind :: (Alpha b, Fresh m, Alpha c) => Bind b c -> m (b, c)Source

Unbind is the destructor of a binding. It ensures that the names in the binding b are fresh.

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

Destruct two bindings simultanously, if they match, using the same list of fresh names

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

class Monad m => HasNext m whereSource

A monad m supports the nextInteger operation if it can generate new fresh integers

class Monad m => LFresh m whereSource

Locally fresh monad This is the class of monads that support freshness in an (implicit) local scope. Names drawn are fresh for this particular 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 an object

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

Destruct a binding in the LFresh monad.

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

lunbind3 :: (LFresh 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

# Rebinding operations

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

destructor for binding patterns, the external names should have already been freshen'ed. We swap the internal names so that they use the external names

# Rec operations

# Substitution

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

Subst b Double | |

Subst b Float | |

Subst b Integer | |

Subst b Char | |

Subst b () | |

Subst b Bool | |

Subst b Int | |

Subst c AnyName | |

Subst Exp Exp | |

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

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

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

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

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

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

(Subst c a, Alpha a, Subst c b, 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) |

# Advanced

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