Unbound.Nominal

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.

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[a1Ev], Sat (ctx[a5QL] (R a[a1Ev])), Sat (ctx[a5QL] (String, Integer))) => Rep1 ctx[a5QL] (Name a[a1Ev])

Rep a => Subst b (Name a)

Eq (Name a)

Ord (Name a)

Show (Name a)

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

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[a2w3] AnyName

Subst c AnyName

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

newtype Embed 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

Embed a

Instances

(Rep a[a5FS], Sat (ctx[a5QD] a[a5FS])) => Rep1 ctx[a5QD] (Embed a[a5FS])

Subst c a => Subst c (Embed a)

Eq a => Eq (Embed a)

Read a => Read (Embed a)

Show a => Show (Embed a)

Rep a[a5FS] => Rep (Embed a[a5FS])

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

data Rebind a b

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

Instances

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

data Rec a

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

Instances

(Rep a[a5FO], Sat (ctx[a5Qi] a[a5FO])) => Rep1 ctx[a5Qi] (Rec a[a5FO])

Show a => Show (Rec a)

Rep a[a5FO] => Rep (Rec a[a5FO])

data Shift a

Shift the scope of an embedded term one level outwards.

Instances

(Rep a[a5FR], Sat (ctx[a5Qa] a[a5FR])) => Rep1 ctx[a5Qa] (Shift a[a5FR])

Eq a => Eq (Shift a)

Rep a[a5FR] => Rep (Shift a[a5FR])

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.

name2Integer :: Name a -> Integer

Get the integer index of a Name.

name2String :: Name a -> String

Get the string part of a Name.

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

Create a Name from a String and an Integer index.

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

Change the sort of a name

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

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

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]

list the binding variables in a pattern, in order

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]

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

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

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

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.

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)

A pattern 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

Rec operations

rec :: Alpha a => a -> Rec a

unrec :: Alpha a => Rec a -> a

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

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

These type representation objects are exported so they can be referenced by auto-generated code. Please pretend they do not exist.

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