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

Stability | experimental |

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

Generic implementation of name binding functions, based on the library RepLib. This version uses a nominal representation of binding structure.

DISCLAIMER: this module probably contains bugs and is noticeably slower than Generics.RepLib.Bind.LocallyNameless. At this point we recommend it only for the curious or intrepid.

Datatypes with binding defined using the `Name`

and `Bind`

types.
Important classes are
`Alpha`

-- the class of types that include binders.
These classes are generic, and default implementations exist for all
representable types. This file also defines a third generic class,
`Subst`

-- for subtitution functions.

- data 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
- 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
- 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
- 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)
- class Rep1 (SubstD b) a => Subst b a where
- data AlphaCtx
- matchR1 :: R1 AlphaD a -> AlphaCtx -> a -> a -> Maybe (Perm AnyName)
- rName :: forall a[aqf1]. Rep a[aqf1] => R (Name a[aqf1])
- rBind :: forall a[aqeZ] b[aqf0]. (Rep a[aqeZ], Rep b[aqf0]) => R (Bind a[aqeZ] b[aqf0])
- rRebind :: forall a[aqeV] b[aqeW]. (Rep a[aqeV], Rep b[aqeW]) => R (Rebind a[aqeV] b[aqeW])
- rAnnot :: forall a[aqeX]. Rep a[aqeX] => R (Annot a[aqeX])

# Basic types

Names are things that get bound. The usual protocol is for names to get created by some automatic process, that preserves alpha renaming under operations over Binding instances.

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[aqeZ], Rep b[aqf0], Sat (ctx[aqpv] a[aqeZ]), Sat (ctx[aqpv] b[aqf0])) => Rep1 ctx[aqpv] (Bind a[aqeZ] b[aqf0]) | |

(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[aqeZ], Rep b[aqf0]) => Rep (Bind a[aqeZ] b[aqf0]) | |

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

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

(Rep a[aqeV], Rep b[aqeW], Sat (ctx[aqoX] a[aqeV]), Sat (ctx[aqoX] (Bind [AnyName] b[aqeW]))) => Rep1 ctx[aqoX] (Rebind a[aqeV] b[aqeW]) | |

(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[aqeV], Rep b[aqeW]) => Rep (Rebind a[aqeV] b[aqeW]) | |

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

## Utilities

integer2Name :: Rep a => Integer -> Name aSource

string2Name :: Rep a => String -> Name aSource

name2Integer :: Name a -> IntegerSource

name2String :: Name a -> StringSource

Get the string part of a `Name`

.

# 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

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

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

Alpha a => Alpha (Maybe a) | |

Rep a => Alpha (R a) | |

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

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

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

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

# 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 (Annot 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) |