Generics.RepLib.Bind.LocallyNameless

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:

• Alpha -- the class of types and patterns that include binders,
• Subst -- for subtitution functions.

Name generation is controlled via monads which implement the Fresh and LFresh classes.

Basic types

data Name a

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

Instances

(Rep a[aKgL], Sat (ctx[aKnq] (R a[aKgL])), Sat (ctx[aKnq] (String, Integer)), Sat (ctx[aKnq] Integer)) => Rep1 ctx[aKnq] (Name a[aKgL])

Rep a => Subst b (Name a)

Eq (Name a)

Ord (Name a)

Show (Name a)

Rep a[aKgL] => Rep (Name a[aKgL])

Rep a => Alpha (Name a)

data AnyName

A name with a hidden (existentially quantified) sort.

Constructors

forall a . Rep a => AnyName (Name a)

Instances

Eq AnyName

Ord AnyName

Show AnyName

Rep AnyName

Alpha AnyName

Rep1 ctx[aKum] AnyName

Subst b AnyName

LFresh (Reader (Set AnyName))

A monad instance for LFresh which renames to the lowest number not currently being used

data Bind a b

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.

Instances

(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 Eq instance for Bind compares bindings for alpha-equality.

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

newtype Annot a

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.

Constructors

Annot a

Instances

(Rep a[aKgF], Sat (ctx[aKni] a[aKgF])) => Rep1 ctx[aKni] (Annot a[aKgF])

Subst c a => Subst c (Annot a)

Eq a => Eq (Annot a)

Read a => Read (Annot a)

Show a => Show (Annot a)

Rep a[aKgF] => Rep (Annot a[aKgF])

Alpha a => Alpha (Annot a)

data Rebind a b

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

Instances

(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

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

Create a Name from an Integer.

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

Create a Name from a String.

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

Create a Name from a String and an Integer index.

name2Integer :: Name a -> Integer

Get the integer index of a Name.

name2String :: Name a -> String

Get the string part of a Name.

anyName2Integer :: AnyName -> Integer

Get the integer index of an AnyName.

anyName2String :: AnyName -> String

Get the string part of an AnyName.

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

The Alpha class

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

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

Methods

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

See swaps.

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

See fv.

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

See lfreshen.

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

See freshen.

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

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

Replace free names by bound names.

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

Replace bound names by free names.

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

nthpatrec b n looks up the nth name in the pattern b (zero-indexed), returning the number of names encountered if not found.

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

Find the (first) index of the name in the pattern if it exists; if not found (Bool = False), return the number of names encountered instead.

Instances

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)

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

Apply a permutation to a term.

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

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

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

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)

Compare two data structures and produce a permutation of their Names that will make them alpha-equivalent to each other (Names 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)

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.

matchBinders :: Alpha a => a -> a -> Maybe (Perm AnyName)

Compare two patterns for equality and produce a permutation of their binding Names to make them alpha-equivalent to each other (Names that appear in annotations must match exactly). Return Nothing if no such renaming is possible.

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

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

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

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

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

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

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

Determine alpha-equivalence.

aeqBinders :: Alpha a => a -> a -> Bool

Determine (alpha-)equivalence of patterns

Binding operations

bind :: (Alpha b, Alpha c) => b -> c -> Bind b c

A smart constructor for binders, also sometimes known as "close".

unsafeUnBind :: (Alpha a, Alpha b) => Bind a b -> (a, b)

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

The Fresh class

class Monad m => Fresh m where

Type class for monads which can generate new globally unique Names based on a given Name.

Methods

fresh :: Name a -> m (Name a)

Instances

(Monad m, HasNext m) => Fresh m

A monad m supports the fresh operation if it can generate a new unique names.

freshen :: (Fresh m, Alpha a) => a -> m (a, Perm AnyName)

Freshen a term by replacing all old binding Names with new fresh Names, returning a new term and a Perm Name specifying how Names were replaced.

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

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

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

The LFresh class

class HasNext m where

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

Methods

nextInteger :: m Integer

Get a new, globally fresh Integer.

resetNext :: Integer -> m ()

Reset the internal state, i.e. forget about Integers that have already been generated.

class Monad m => LFresh m where

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.

Methods

lfresh :: Rep a => Name a -> m (Name a)

Pick a new name that is fresh for the current (implicit) scope.

avoid :: [AnyName] -> m a -> m a

Avoid the given names when freshening in the subcomputation.

Instances

LFresh (Reader Integer)

Simple reader monad instance for LFresh.

LFresh (Reader (Set AnyName))

A monad instance for LFresh which renames to the lowest number not currently being used

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

"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 c

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 e

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 f

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

Rebinding operations

rebind :: (Alpha a, Alpha b) => a -> b -> Rebind a b

Constructor for binding in patterns.

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

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

Substitution

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

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.

Methods

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

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

subst nm sub tm substitutes sub for nm in tm.

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

Perform several simultaneous substitutions.

Instances

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

Advanced

data AlphaCtx

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.

matchR1 :: R1 AlphaD a -> AlphaCtx -> a -> a -> Maybe (Perm AnyName)

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.

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