Unbound.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 Embed 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[a18ML], Sat (ctx[a18QA] (R a[a18ML])), Sat (ctx[a18QA] (String, Integer)), Sat (ctx[a18QA] Integer)) => Rep1 ctx[a18QA] (Name a[a18ML])

Rep a => Subst b (Name a)

Eq (Name a)

Ord (Name a)

Show (Name a)

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

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

Subst b AnyName

Monad m => MonadReader (Set AnyName) (LFreshMT m)

data Bind p t

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 p[a1f71], Rep t[a1f72], Sat (ctx[a1fbG] p[a1f71]), Sat (ctx[a1fbG] t[a1f72])) => Rep1 ctx[a1fbG] (Bind p[a1f71] t[a1f72])

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

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

(Rep p[a1f71], Rep t[a1f72]) => Rep (Bind p[a1f71] t[a1f72])

(Alpha p, Alpha t) => Alpha (Bind p t)

newtype Embed t

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 t

Instances

(Rep t[a1f6W], Sat (ctx[a1fby] t[a1f6W])) => Rep1 ctx[a1fby] (Embed t[a1f6W])

Subst c a => Subst c (Embed a)

Eq t => Eq (Embed t)

Show a => Show (Embed a)

Rep t[a1f6W] => Rep (Embed t[a1f6W])

Alpha t => Alpha (Embed t)

data Rebind p1 p2

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

Instances

(Rep p1[a1f6Z], Rep p2[a1f70], Sat (ctx[a1fbl] p1[a1f6Z]), Sat (ctx[a1fbl] p2[a1f70])) => Rep1 ctx[a1fbl] (Rebind p1[a1f6Z] p2[a1f70])

(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 p1[a1f6Z], Rep p2[a1f70]) => Rep (Rebind p1[a1f6Z] p2[a1f70])

(Alpha p, Alpha q) => Alpha (Rebind p q)

data Rec p

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 p[a1f6Y], Sat (ctx[a1fbd] p[a1f6Y])) => Rep1 ctx[a1fbd] (Rec p[a1f6Y])

(Alpha a, Subst c a) => Subst c (Rec a)

Show a => Show (Rec a)

Rep p[a1f6Y] => Rep (Rec p[a1f6Y])

Alpha p => Alpha (Rec p)

data TRec p

TRec is a standalone variant of Rec -- that is, if p is a pattern type then TRec p is a term type. It is isomorphic to Bind (Rec p) ().

Instances

Show a => Show (TRec a)

newtype Shift p

Shift the scope of an embedded term one level outwards.

Constructors

Shift p

Instances

(Rep p[a1f6V], Sat (ctx[a1fb5] p[a1f6V])) => Rep1 ctx[a1fb5] (Shift p[a1f6V])

Eq p => Eq (Shift p)

Show a => Show (Shift a)

Rep p[a1f6V] => Rep (Shift p[a1f6V])

Alpha a => Alpha (Shift a)

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.

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

Convenient synonym for string2Name.

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

translate :: Rep b => Name a -> Name b

Change the sort of a name

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' :: Collection f => AlphaCtx -> a -> f 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.

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

See aeq.

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.

acompare' :: AlphaCtx -> a -> a -> Ordering

See acompare.

isPat :: a -> Maybe [AnyName]

isPat x dynamically checks whether x can be used as a valid pattern. The default instance returns True if at all possible.

isTerm :: a -> Bool

isTerm x dynamically checks whether x can be used as a valid term. The default instance returns True if at all possible.

isEmbed :: a -> Bool

isEmbed is needed internally for the implementation of isPat. isEmbed is true for terms wrapped in Embed and zero or more occurrences of Shift. The default implementation simply returns False.

nthpatrec :: a -> NthCont

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

findpatrec :: a -> AnyName -> FindResult

Find the (first) index of the name in the pattern if one exists; otherwise, return the number of names encountered instead.

Instances

Alpha Bool

Alpha Char

Alpha Double

Alpha Float

Alpha Int

Alpha Integer

Alpha ()

Alpha AnyName

Alpha a => Alpha [a]

Rep a => Alpha (R a)

Alpha a => Alpha (Maybe a)

Rep a => Alpha (Name a)

Alpha a => Alpha (Shift a)

Alpha t => Alpha (Embed t)

Alpha p => Alpha (Rec p)

(Alpha a, Alpha b) => Alpha (Either a b)

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

(Alpha p, Alpha q) => Alpha (Rebind p q)

(Alpha p, Alpha t) => Alpha (Bind p t)

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

swapsEmbeds :: 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. Embedded terms are left alone by the permutation.

aeq :: Alpha t => t -> t -> Bool

Determine alpha-equivalence of terms.

aeqBinders :: Alpha p => p -> p -> Bool

Determine (alpha-)equivalence of patterns. Do they bind the same variables and have alpha-equal annotations?

acompare :: Alpha t => t -> t -> Ordering

An alpha-respecting total order on terms involving binders.

Variable calculations

class Foldable f => Collection f where

Collections are foldable types that support empty, singleton, union, and map operations. The result of a free variable calculation may be any collection. Instances are provided for lists and sets.

Methods

emptyC :: f a

singleton :: a -> f a

union :: Ord a => f a -> f a -> f a

cmap :: (Ord a, Ord b) => (a -> b) -> f a -> f b

Instances

Collection []

Lists are containers under concatenation. Lists preserve ordering and multiplicity of elements.

Collection Set

Sets are containers under union, which preserve only occurrence, not multiplicity or ordering.

Collection Multiset

Multisets are containers which preserve multiplicity but not ordering.

newtype Multiset a

A simple representation of multisets.

Constructors

Multiset (Map a Int)

Instances

Foldable Multiset

Collection Multiset

Multisets are containers which preserve multiplicity but not ordering.

fv :: (Rep a, Alpha t, Collection f) => t -> f (Name a)

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

fvAny :: (Alpha t, Collection f) => t -> f AnyName

Calculate the free variables (of any sort) contained in a term.

patfv :: (Rep a, Alpha p, Collection f) => p -> f (Name a)

Calculate the variables of a particular sort that occur freely in pattern annotations (but are not bound by the pattern).

patfvAny :: (Alpha p, Collection f) => p -> f AnyName

Calculate the variables (of any sort) that occur freely within pattern annotations (but are not bound by the pattern).

binders :: (Rep a, Alpha p, Collection f) => p -> f (Name a)

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

bindersAny :: (Alpha p, Collection f) => p -> f AnyName

Calculate the binding variables (of any sort) in a pattern.

Binding operations

bind :: (Alpha c, Alpha b) => 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

Fresh m => Fresh (ListT m)

Fresh m => Fresh (MaybeT m)

Fresh m => Fresh (IdentityT m)

Monad m => Fresh (FreshMT m)

Fresh m => Fresh (ContT r m)

(Error e, Fresh m) => Fresh (ErrorT e m)

Fresh m => Fresh (ReaderT r m)

Fresh m => Fresh (StateT s m)

Fresh m => Fresh (StateT s m)

(Monoid w, Fresh m) => Fresh (WriterT w m)

(Monoid w, Fresh m) => Fresh (WriterT w m)

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

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

unbind :: (Fresh m, Alpha p, Alpha t) => Bind p t -> m (p, t)

Unbind (also known as "open") is the destructor for bindings. It ensures that the names in the binding are fresh.

unbind2 :: (Fresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => Bind p1 t1 -> Bind p2 t2 -> m (Maybe (p1, t1, p2, t2))

Unbind two terms with the same fresh names, provided the binders have the same number of binding variables.

unbind3 :: (Fresh m, Alpha p1, Alpha p2, Alpha p3, Alpha t1, Alpha t2, Alpha t3) => Bind p1 t1 -> Bind p2 t2 -> Bind p3 t3 -> m (Maybe (p1, t1, p2, t2, p3, t3))

Unbind three terms with the same fresh names, provided the binders have the same number of binding variables.

type FreshM = FreshMT Identity

A convenient monad which is an instance of Fresh. It keeps track of a global index used for generating fresh names, which is incremented every time fresh is called.

runFreshM :: FreshM a -> a

Run a FreshM computation in an empty context.

data FreshMT m a

The FreshM monad transformer. Keeps track of the lowest index still globally unused, and increments the index every time it is asked for a fresh name.

Instances

MonadTrans FreshMT

MonadError e m => MonadError e (FreshMT m)

MonadReader r m => MonadReader r (FreshMT m)

Monad m => MonadState Integer (FreshMT m)

MonadState s m => MonadState s (FreshMT m)

Monad m => Monad (FreshMT m)

Functor m => Functor (FreshMT m)

MonadPlus m => MonadPlus (FreshMT m)

(Monad m, Functor m) => Applicative (FreshMT m)

MonadIO m => MonadIO (FreshMT m)

MonadCont m => MonadCont (FreshMT m)

Monad m => Fresh (FreshMT m)

runFreshMT :: Monad m => FreshMT m a -> m a

Run a FreshMT computation starting in an empty context.

The LFresh class

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.

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 m => LFresh (ListT m)

LFresh (Reader Integer)

A simple reader monad instance for LFresh.

LFresh m => LFresh (MaybeT m)

LFresh m => LFresh (IdentityT m)

Monad m => LFresh (LFreshMT m)

LFresh m => LFresh (ContT r m)

(Error e, LFresh m) => LFresh (ErrorT e m)

LFresh m => LFresh (ReaderT r m)

LFresh m => LFresh (StateT s m)

LFresh m => LFresh (StateT s m)

(Monoid w, LFresh m) => LFresh (WriterT w m)

(Monoid w, LFresh m) => LFresh (WriterT w m)

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

"Locally" freshen a pattern replacing all binding names with new names that have not already been used. The second argument is a continuation, which takes the renamed term and a permutation that specifies how the pattern has been renamed.

lunbind :: (LFresh m, Alpha p, Alpha t) => Bind p t -> ((p, t) -> m c) -> m c

Destruct a binding in an LFresh monad.

lunbind2 :: (LFresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => Bind p1 t1 -> Bind p2 t2 -> (Maybe (p1, t1, p2, t2) -> m r) -> m r

Unbind two terms with the same fresh names, provided the binders have the same number of binding variables.

lunbind3 :: (LFresh m, Alpha p1, Alpha p2, Alpha p3, Alpha t1, Alpha t2, Alpha t3) => Bind p1 t1 -> Bind p2 t2 -> Bind p3 t3 -> (Maybe (p1, t1, p2, t2, p3, t3) -> m r) -> m r

Unbind three terms with the same fresh names, provided the binders have the same number of binding variables.

type LFreshM = LFreshMT Identity

A convenient monad which is an instance of LFresh. It keeps track of a set of names to avoid, and when asked for a fresh one will choose the first unused numerical name.

runLFreshM :: LFreshM a -> a

Run a LFreshM computation in an empty context.

getAvoids :: Monad m => LFreshMT m (Set AnyName)

Get the set of names currently being avoided.

data LFreshMT m a

The LFresh monad transformer. Keeps track of a set of names to avoid, and when asked for a fresh one will choose the first unused numerical name.

Instances

MonadTrans LFreshMT

MonadError e m => MonadError e (LFreshMT m)

MonadReader r m => MonadReader r (LFreshMT m)

MonadState s m => MonadState s (LFreshMT m)

Monad m => Monad (LFreshMT m)

Functor m => Functor (LFreshMT m)

MonadPlus m => MonadPlus (LFreshMT m)

Applicative m => Applicative (LFreshMT m)

MonadIO m => MonadIO (LFreshMT m)

MonadCont m => MonadCont (LFreshMT m)

Monad m => LFresh (LFreshMT m)

Monad m => MonadReader (Set AnyName) (LFreshMT m)

runLFreshMT :: LFreshMT m a -> m a

Run an LFreshMT computation in an empty context.

Rebinding operations

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

Constructor for binding in patterns.

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

Destructor for Rebind. It does not need a monadic context for generating fresh names, since Rebind can only occur in the pattern of a Bind; hence a previous call to open must have already freshened the names at this point.

Rec operations

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

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

trec :: Alpha p => p -> TRec p

untrec :: (Fresh m, Alpha p) => TRec p -> m p

luntrec :: (LFresh m, Alpha p) => TRec p -> m p

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 (SubstName a b)

If the argument is a variable, return its name wrapped in the SubstName constructor. Return Nothing for non-variable arguments. The default implementation always returns Nothing.

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

(Alpha a, Subst c a) => Subst c (Rec a)

Subst c a => Subst c (Embed 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)

data SubstName a b where

See isvar.

Constructors

SubstName :: a ~ b => Name a -> SubstName a b

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[a18ML]. Rep a[a18ML] => R (Name a[a18ML])

rBind :: forall p[a1f71] t[a1f72]. (Rep p[a1f71], Rep t[a1f72]) => R (Bind p[a1f71] t[a1f72])

rRebind :: forall p1[a1f6Z] p2[a1f70]. (Rep p1[a1f6Z], Rep p2[a1f70]) => R (Rebind p1[a1f6Z] p2[a1f70])

rEmbed :: forall t[a1f6W]. Rep t[a1f6W] => R (Embed t[a1f6W])

rRec :: forall p[a1f6Y]. Rep p[a1f6Y] => R (Rec p[a1f6Y])

rShift :: forall p[a1f6V]. Rep p[a1f6V] => R (Shift p[a1f6V])