Generics.RepLib.Bind.Nominal

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.

Basic types

data Name a

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.

Instances

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

Rep a => Subst b (Name a)

Eq (Name a)

Ord (Name a)

Show (Name a)

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

Rep a => Alpha (Name a)

data Bind a b

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.

Instances

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

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[aqeX], Sat (ctx[aqpa] a[aqeX])) => Rep1 ctx[aqpa] (Annot a[aqeX])

Subst c a => Subst c (Annot a)

Eq a => Eq (Annot a)

Read a => Read (Annot a)

Show a => Show (Annot a)

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

(Eq a, Alpha a) => Alpha (Annot a)

data Rebind a b

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

Instances

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

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

name2Integer :: Name a -> Integer

name2String :: Name a -> String

Get the string part of a Name.

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

The Alpha class

class Rep1 AlphaD a => Alpha a where

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

Methods

aeq' :: AlphaCtx -> a -> a -> Bool

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

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

The method swaps' applys a compound permutation.

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

calculate the free variables (aka support)

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

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

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)

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 b

See lfreshen

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)

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

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

binders :: (Rep b, Alpha b) => b -> [AnyName]

List the binding variables in a pattern

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

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

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

calculate the free variables of the term

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

Binding operations

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

Smart constructor for binders

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

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

The Fresh class

class (Monad m, HasNext m) => Fresh m where

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

Methods

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

Instances

HasNext m => Fresh m

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

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

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

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

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

The LFresh class

class Monad m => HasNext m where

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

Methods

nextInteger :: m Integer

resetNext :: Integer -> m ()

class Monad m => LFresh m where

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.

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 these names when freshening in the subcomputation.

Instances

LFresh (Reader Integer)

Reader monad instance for local freshness class.

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

Locally freshen an object

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

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

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

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

Methods

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

lsubst :: LFresh m => Name b -> b -> a -> m a

lsubsts :: LFresh m => [Name b] -> [b] -> a -> m a

Instances

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)

Advanced

data AlphaCtx

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.

Instances

Eq AlphaCtx

Read AlphaCtx

Show AlphaCtx

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

Pay no attention to the man behind the curtain

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