unbound-0.5.0: Generic support for programming with names and binders

LicenseBSD-like (see LICENSE)
MaintainerBrent Yorgey <byorgey@cis.upenn.edu>
Stabilityexperimental
PortabilityGHC only (-XKitchenSink)
Safe HaskellNone
LanguageHaskell2010

Unbound.LocallyNameless

Contents

Description

A generic implementation of standard functions dealing with names and binding structure (alpha equivalence, free variable calculation, capture-avoiding substitution, name permutation, ...) using a locally nameless representation.

Normal users of this library should only need to import this module. In particular, this module is careful to export only an abstract interface with various safety guarantees. Power users who wish to have access to the internals of the library (at the risk of shooting oneself in the foot) can directly import the various implementation modules such as Unbound.LocallyNameless.Name and so on.

Ten-second tutorial: use the type combinators Bind, Embed, Rebind, Rec, TRec, and Shift to specify the binding structure of your data types. Then use Template Haskell to derive generic representations for your types:

$(derive [''Your, ''Types, ''Here])

Finally, declare Alpha and Subst instances for your types. Then you can go to town using all the generically-derived operations like aeq, fv, subst, and so on.

For more information, see the more in-depth literate Haskell tutorial in the tutorial directory (which can be obtained as part of the library source package: cabal unpack unbound) and the examples in the example directory.

See also: Stephanie Weirich, Brent A. Yorgey, and Tim Sheard. Binders Unbound. ICFP'11, September 2011, Tokyo, Japan. http://www.cis.upenn.edu/~byorgey/papers/binders-unbound.pdf.

Synopsis

Names

data Name a Source #

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 a representable type, i.e. an instance of the Rep type class from the RepLib generic programming framework.

To hide the sort of a name, use AnyName.

Instances

(Rep a0, Sat (ctx0 (R a0)), Sat (ctx0 (String, Integer)), Sat (ctx0 Integer)) => Rep1 ctx0 (Name a0) Source # 

Methods

rep1 :: R1 ctx0 (Name a0) #

Rep a => Subst b (Name a) Source # 

Methods

isvar :: Name a -> Maybe (SubstName (Name a) b) Source #

isCoerceVar :: Name a -> Maybe (SubstCoerce (Name a) b) Source #

subst :: Name b -> b -> Name a -> Name a Source #

substs :: [(Name b, b)] -> Name a -> Name a Source #

substPat :: AlphaCtx -> b -> Name a -> Name a Source #

substPats :: Proxy * b -> AlphaCtx -> [Dyn] -> Name a -> Name a Source #

Eq (Name a) Source # 

Methods

(==) :: Name a -> Name a -> Bool #

(/=) :: Name a -> Name a -> Bool #

Ord (Name a) Source # 

Methods

compare :: Name a -> Name a -> Ordering #

(<) :: Name a -> Name a -> Bool #

(<=) :: Name a -> Name a -> Bool #

(>) :: Name a -> Name a -> Bool #

(>=) :: Name a -> Name a -> Bool #

max :: Name a -> Name a -> Name a #

min :: Name a -> Name a -> Name a #

Show (Name a) Source # 

Methods

showsPrec :: Int -> Name a -> ShowS #

show :: Name a -> String #

showList :: [Name a] -> ShowS #

Rep a0 => Rep (Name a0) Source # 

Methods

rep :: R (Name a0) #

Rep a => Alpha (Name a) Source # 

Methods

swaps' :: AlphaCtx -> Perm AnyName -> Name a -> Name a Source #

fv' :: Collection f => AlphaCtx -> Name a -> f AnyName Source #

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

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

aeq' :: AlphaCtx -> Name a -> Name a -> Bool Source #

acompare' :: AlphaCtx -> Name a -> Name a -> Ordering Source #

close :: Alpha b => AlphaCtx -> b -> Name a -> Name a Source #

open :: Alpha b => AlphaCtx -> b -> Name a -> Name a Source #

isPat :: Name a -> Maybe [AnyName] Source #

isTerm :: Name a -> Bool Source #

isEmbed :: Name a -> Bool Source #

nthpatrec :: Name a -> NthCont Source #

findpatrec :: Name a -> AnyName -> FindResult Source #

data AnyName Source #

A name with a hidden (existentially quantified) sort. To hide the sort of a name, use the AnyName constructor directly; to extract a name with a hidden sort, use toSortedName.

Constructors

Rep a => AnyName (Name a) 

Instances

Eq AnyName Source # 

Methods

(==) :: AnyName -> AnyName -> Bool #

(/=) :: AnyName -> AnyName -> Bool #

Ord AnyName Source # 
Show AnyName Source # 
Rep AnyName Source # 

Methods

rep :: R AnyName #

Alpha AnyName Source # 
Rep1 ctx0 AnyName Source # 

Methods

rep1 :: R1 ctx0 AnyName #

Subst b AnyName Source # 

Constructing and destructing free names

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

Create a free Name from an Integer.

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

Create a free Name from a String.

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

Convenient synonym for string2Name.

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

Create a free Name from a String and an Integer index.

name2Integer :: Name a -> Integer Source #

Get the integer index of a Name.

name2String :: Name a -> String Source #

Get the string part of a Name.

anyName2Integer :: AnyName -> Integer Source #

Get the integer index of an AnyName.

anyName2String :: AnyName -> String Source #

Get the string part of an AnyName.

Dealing with name sorts

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

Change the sort of a name.

toSortedName :: Rep a => AnyName -> Maybe (Name a) Source #

Cast a name with an existentially hidden sort to an explicitly sorted name.

Type combinators for specifying binding structure

Bind, Embed, Rebind, Rec, TRec, and Shift are special types provided by Unbound for use in specifying the binding structure of your data types.

An important distinction to keep in mind is the difference between term types and pattern types.

  • Term types are normal types whose values represent data in your program. Any Names occurring in term types are either free variables, or references to binders.
  • Pattern types are types which may be used on the left hand side of a Bind. They bind names, that is, any Names occurring in pattern types are binding sites to which other names may refer.

Name may be used as both a term type (where it represents a free variable/reference) and a pattern type (where it represents a binding site).

Any first-order algebraic data type (i.e. one containing no functions) which contains only term types may be used as a term type, and likewise for algebraic data types containing only pattern types. For example,

(Name, [Name])

may be used as either a term type or a pattern type. On the other hand,

(Bind Name Name, Name)

may only be used as a term type, since Bind Name Name is a term type and not a pattern type.

We adopt the convention that the type variable t stands for term types, and the type variable p stands for pattern types. It would be nicer if we could actually use Haskell's type system to enforce the distinction, but for various technical reasons (involving the RepLib generic programming framework which is used in the implementation), we cannot. Or at least, we are not sufficiently clever to see how.

Bind

type Bind p t = GenBind StrictOrder StrictCard p t Source #

The most fundamental combinator for expressing binding structure is Bind. The term type Bind p t represents a pattern p paired with a term t, where names in p are bound within t.

Like Name, Bind is also abstract. You can create bindings using bind and take them apart with unbind and friends.

Bind constructors

bind :: (Alpha p, Alpha t) => p -> t -> Bind p t Source #

A smart constructor for binders, also sometimes referred to as "close". Free variables in the term are taken to be references to matching binders in the pattern. (Free variables with no matching binders will remain free.)

permbind :: (Alpha p, Alpha t) => p -> t -> SetBind p t Source #

Bind the pattern in the term "up to permutation" of bound variables. For example, the following 4 terms are all alpha-equivalent:

permbind [a,b] (a,b)
permbind [a,b] (b,a)
permbind [b,a] (a,b)
permbind [b,a] (b,a)

Note that none of these terms is equivalent to a term with a redundant pattern such as

permbind [a,b,c] (a,b)

For binding constructors which do render these equivalent, see setbind and setbindAny.

setbind :: (Alpha a, Alpha t) => [Name a] -> t -> SetPlusBind [Name a] t Source #

Bind the list of names in the term up to permutation and dropping of unused variables.

For example, the following 5 terms are all alpha-equivalent:

setbind [a,b] (a,b)
setbind [a,b] (b,a)
setbind [b,a] (a,b)
setbind [b,a] (b,a)
setbind [a,b,c] (a,b)

There is also a variant, setbindAny, which ignores name sorts.

setbindAny :: Alpha t => [AnyName] -> t -> SetPlusBind [AnyName] t Source #

Bind the list of (any-sorted) names in the term up to permutation and dropping of unused variables. See setbind.

Bind destructors

Directly pattern-matching on Bind values is not allowed, but there are quite a few different ways to safely "open" a binding. (If you want direct, unsafe access to the components of a binding --- e.g. to write a function to compute the size of terms that ignores all names --- you can directly import Unbound.LocallyNameless.Ops and use the unsafeUnbind function.)

unbind :: (Fresh m, Alpha p, Alpha t) => GenBind order card p t -> m (p, t) Source #

Unbind (also known as "open") is the simplest destructor for bindings. It ensures that the names in the binding are globally fresh, using a monad which is an instance of the Fresh type class.

lunbind :: (LFresh m, Alpha p, Alpha t) => GenBind order card p t -> ((p, t) -> m c) -> m c Source #

lunbind opens a binding in an LFresh monad, ensuring that the names chosen for the binders are locally fresh. The components of the binding are passed to a continuation, and the resulting monadic action is run in a context extended to avoid choosing new names which are the same as the ones chosen for this binding.

For more information, see the documentation for the LFresh type class.

Simultaneous unbinding

Sometimes one may wish to open several bindings using same names for their binding variables --- for example, when checking equality of terms involving binders, so that the free variables in the bodies will match appropriately during recursive calls. Opening two bindings simultaneously is accomplished with unbind2 (which picks globally fresh names) and lunbind2 (which picks locally fresh names, see the LFresh documentation for more information). unbind3 and lunbind3 open three bindings simultaneously. In principle, of course, unbindN and lunbindN can be easily implemented for any N; please let the maintainers know if for some reason you would like an N > 3.

unbind2 :: (Fresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => GenBind order card p1 t1 -> GenBind order card p2 t2 -> m (Maybe (p1, t1, p2, t2)) Source #

Unbind two terms with the same fresh names, provided the binders have the same binding variables (both number and sort). If the patterns have different binding variables, return Nothing. Otherwise, return the renamed patterns and the associated terms.

unbind3 :: (Fresh m, Alpha p1, Alpha p2, Alpha p3, Alpha t1, Alpha t2, Alpha t3) => GenBind order card p1 t1 -> GenBind order card p2 t2 -> GenBind order card p3 t3 -> m (Maybe (p1, t1, p2, t2, p3, t3)) Source #

Unbind three terms with the same fresh names, provided the binders have the same number of binding variables. See the documentation for unbind2 for more details.

lunbind2 :: (LFresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => GenBind order card p1 t1 -> GenBind order card p2 t2 -> (Maybe (p1, t1, p2, t2) -> m r) -> m r Source #

Unbind two terms with the same locally fresh names, provided the patterns have the same number of binding variables. See the documentation for unbind2 and lunbind for more details.

lunbind3 :: (LFresh m, Alpha p1, Alpha p2, Alpha p3, Alpha t1, Alpha t2, Alpha t3) => GenBind order card p1 t1 -> GenBind order card p2 t2 -> GenBind order card p3 t3 -> (Maybe (p1, t1, p2, t2, p3, t3) -> m r) -> m r Source #

Unbind three terms with the same locally fresh names, provided the binders have the same number of binding variables. See the documentation for unbind2 and lunbind for more details.

unbind2Plus :: (MonadPlus m, Fresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => GenBind order card p1 t1 -> GenBind order card p2 t2 -> m (p1, t1, p2, t2) Source #

Unbind two binders with the same names, fail if the number of required names and their sorts does not match. See unbind2

unbind3Plus :: (MonadPlus m, Fresh m, Alpha p1, Alpha p2, Alpha p3, Alpha t1, Alpha t2, Alpha t3) => GenBind order card p1 t1 -> GenBind order card p2 t2 -> GenBind order card p3 t3 -> m (p1, t1, p2, t2, p3, t3) Source #

Unbind three binders with the same names, fail if the number of required names and their sorts does not match. See unbind3

lunbind2Plus :: (MonadPlus m, LFresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => GenBind order card p1 t1 -> GenBind order card p2 t2 -> ((p1, t1, p2, t2) -> m r) -> m r Source #

lunbind3Plus :: (MonadPlus m, LFresh m, Alpha p1, Alpha p2, Alpha p3, Alpha t1, Alpha t2, Alpha t3) => GenBind order card p1 t1 -> GenBind order card p2 t2 -> GenBind order card p3 t3 -> ((p1, t1, p2, t2, p3, t3) -> m r) -> m r Source #

Embed

newtype Embed t Source #

Embed allows for terms to be embedded within patterns. Such embedded terms do not bind names along with the rest of the pattern. For examples, see the tutorial or examples directories.

If t is a term type, then Embed t is a pattern type.

Embed is not abstract since it involves no binding, and hence it is safe to manipulate directly. To create and destruct Embed terms, you may use the Embed constructor directly. (You may also use the functions embed and unembed, which additionally can construct or destruct any number of enclosing Shifts at the same time.)

Constructors

Embed t 

Instances

(Rep t0, Sat (ctx0 t0)) => Rep1 ctx0 (Embed t0) Source # 

Methods

rep1 :: R1 ctx0 (Embed t0) #

(Alpha t, Subst b t) => Subst b (Embed t) Source # 

Methods

isvar :: Embed t -> Maybe (SubstName (Embed t) b) Source #

isCoerceVar :: Embed t -> Maybe (SubstCoerce (Embed t) b) Source #

subst :: Name b -> b -> Embed t -> Embed t Source #

substs :: [(Name b, b)] -> Embed t -> Embed t Source #

substPat :: AlphaCtx -> b -> Embed t -> Embed t Source #

substPats :: Proxy * b -> AlphaCtx -> [Dyn] -> Embed t -> Embed t Source #

Eq t => Eq (Embed t) Source # 

Methods

(==) :: Embed t -> Embed t -> Bool #

(/=) :: Embed t -> Embed t -> Bool #

Show a => Show (Embed a) Source # 

Methods

showsPrec :: Int -> Embed a -> ShowS #

show :: Embed a -> String #

showList :: [Embed a] -> ShowS #

Rep t0 => Rep (Embed t0) Source # 

Methods

rep :: R (Embed t0) #

Binary p => Binary (Embed p) Source # 

Methods

put :: Embed p -> Put #

get :: Get (Embed p) #

putList :: [Embed p] -> Put #

IsEmbed (Embed t) Source # 

Associated Types

type Embedded (Embed t) :: * Source #

Alpha t => Alpha (Embed t) Source # 
type Embedded (Embed t) Source # 
type Embedded (Embed t) = t

embed :: IsEmbed e => Embedded e -> e Source #

Construct an embedded term, which is an instance of Embed with any number of enclosing Shifts. That is, embed can have any of the types

  • t -> Embed t
  • t -> Shift (Embed t)
  • t -> Shift (Shift (Embed t))

and so on.

unembed :: IsEmbed e => e -> Embedded e Source #

Destruct an embedded term. unembed can have any of the types

  • Embed t -> t
  • Shift (Embed t) -> t

and so on.

Rebind

data Rebind p1 p2 Source #

Rebind allows for nested bindings. If p1 and p2 are pattern types, then Rebind p1 p2 is also a pattern type, similar to the pattern type (p1,p2) except that p1 scopes over p2. That is, names within terms embedded in p2 may refer to binders in p1.

Instances

(Rep p10, Rep p20, Sat (ctx0 p10), Sat (ctx0 p20)) => Rep1 ctx0 (Rebind p10 p20) Source # 

Methods

rep1 :: R1 ctx0 (Rebind p10 p20) #

(Alpha p, Alpha q, Subst b p, Subst b q) => Subst b (Rebind p q) Source # 

Methods

isvar :: Rebind p q -> Maybe (SubstName (Rebind p q) b) Source #

isCoerceVar :: Rebind p q -> Maybe (SubstCoerce (Rebind p q) b) Source #

subst :: Name b -> b -> Rebind p q -> Rebind p q Source #

substs :: [(Name b, b)] -> Rebind p q -> Rebind p q Source #

substPat :: AlphaCtx -> b -> Rebind p q -> Rebind p q Source #

substPats :: Proxy * b -> AlphaCtx -> [Dyn] -> Rebind p q -> Rebind p q Source #

(Show a, Show b) => Show (Rebind a b) Source # 

Methods

showsPrec :: Int -> Rebind a b -> ShowS #

show :: Rebind a b -> String #

showList :: [Rebind a b] -> ShowS #

(Rep p10, Rep p20) => Rep (Rebind p10 p20) Source # 

Methods

rep :: R (Rebind p10 p20) #

(Binary p1, Binary p2) => Binary (Rebind p1 p2) Source # 

Methods

put :: Rebind p1 p2 -> Put #

get :: Get (Rebind p1 p2) #

putList :: [Rebind p1 p2] -> Put #

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

Methods

swaps' :: AlphaCtx -> Perm AnyName -> Rebind p q -> Rebind p q Source #

fv' :: Collection f => AlphaCtx -> Rebind p q -> f AnyName Source #

lfreshen' :: LFresh m => AlphaCtx -> Rebind p q -> (Rebind p q -> Perm AnyName -> m b) -> m b Source #

freshen' :: Fresh m => AlphaCtx -> Rebind p q -> m (Rebind p q, Perm AnyName) Source #

aeq' :: AlphaCtx -> Rebind p q -> Rebind p q -> Bool Source #

acompare' :: AlphaCtx -> Rebind p q -> Rebind p q -> Ordering Source #

close :: Alpha b => AlphaCtx -> b -> Rebind p q -> Rebind p q Source #

open :: Alpha b => AlphaCtx -> b -> Rebind p q -> Rebind p q Source #

isPat :: Rebind p q -> Maybe [AnyName] Source #

isTerm :: Rebind p q -> Bool Source #

isEmbed :: Rebind p q -> Bool Source #

nthpatrec :: Rebind p q -> NthCont Source #

findpatrec :: Rebind p q -> AnyName -> FindResult Source #

rebind :: (Alpha p1, Alpha p2) => p1 -> p2 -> Rebind p1 p2 Source #

Constructor for rebinding patterns.

unrebind :: (Alpha p1, Alpha p2) => Rebind p1 p2 -> (p1, p2) Source #

Destructor for rebinding patterns. 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 unbind (or something similar) must have already freshened the names at this point.

Rec

data Rec p Source #

If p is a pattern type, then Rec p is also a pattern type, which is recursive in the sense that p may bind names in terms embedded within itself. Useful for encoding e.g. lectrec and Agda's dot notation.

Instances

(Rep p0, Sat (ctx0 p0)) => Rep1 ctx0 (Rec p0) Source # 

Methods

rep1 :: R1 ctx0 (Rec p0) #

(Alpha p, Subst b p) => Subst b (Rec p) Source # 

Methods

isvar :: Rec p -> Maybe (SubstName (Rec p) b) Source #

isCoerceVar :: Rec p -> Maybe (SubstCoerce (Rec p) b) Source #

subst :: Name b -> b -> Rec p -> Rec p Source #

substs :: [(Name b, b)] -> Rec p -> Rec p Source #

substPat :: AlphaCtx -> b -> Rec p -> Rec p Source #

substPats :: Proxy * b -> AlphaCtx -> [Dyn] -> Rec p -> Rec p Source #

Show a => Show (Rec a) Source # 

Methods

showsPrec :: Int -> Rec a -> ShowS #

show :: Rec a -> String #

showList :: [Rec a] -> ShowS #

Rep p0 => Rep (Rec p0) Source # 

Methods

rep :: R (Rec p0) #

Alpha p => Alpha (Rec p) Source # 

Methods

swaps' :: AlphaCtx -> Perm AnyName -> Rec p -> Rec p Source #

fv' :: Collection f => AlphaCtx -> Rec p -> f AnyName Source #

lfreshen' :: LFresh m => AlphaCtx -> Rec p -> (Rec p -> Perm AnyName -> m b) -> m b Source #

freshen' :: Fresh m => AlphaCtx -> Rec p -> m (Rec p, Perm AnyName) Source #

aeq' :: AlphaCtx -> Rec p -> Rec p -> Bool Source #

acompare' :: AlphaCtx -> Rec p -> Rec p -> Ordering Source #

close :: Alpha b => AlphaCtx -> b -> Rec p -> Rec p Source #

open :: Alpha b => AlphaCtx -> b -> Rec p -> Rec p Source #

isPat :: Rec p -> Maybe [AnyName] Source #

isTerm :: Rec p -> Bool Source #

isEmbed :: Rec p -> Bool Source #

nthpatrec :: Rec p -> NthCont Source #

findpatrec :: Rec p -> AnyName -> FindResult Source #

rec :: Alpha p => p -> Rec p Source #

Constructor for recursive patterns.

unrec :: Alpha p => Rec p -> p Source #

Destructor for recursive patterns.

TRec

data TRec p Source #

TRec is a standalone variant of Rec: the only difference is that whereas Rec p is a pattern type, TRec p is a term type. It is isomorphic to Bind (Rec p) ().

Note that TRec corresponds to Pottier's abstraction construct from alpha-Caml. In this context, Embed t corresponds to alpha-Caml's inner t, and Shift (Embed t) corresponds to alpha-Caml's outer t.

Instances

Show a => Show (TRec a) Source # 

Methods

showsPrec :: Int -> TRec a -> ShowS #

show :: TRec a -> String #

showList :: [TRec a] -> ShowS #

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

Constructor for recursive abstractions.

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

Destructor for recursive abstractions which picks globally fresh names for the binders.

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

Destructor for recursive abstractions which picks locally fresh names for binders (see LFresh).

Shift

newtype Shift p Source #

Shift the scope of an embedded term one level outwards.

Constructors

Shift p 

Instances

(Rep p0, Sat (ctx0 p0)) => Rep1 ctx0 (Shift p0) Source # 

Methods

rep1 :: R1 ctx0 (Shift p0) #

(Alpha a, Subst b a) => Subst b (Shift a) Source # 

Methods

isvar :: Shift a -> Maybe (SubstName (Shift a) b) Source #

isCoerceVar :: Shift a -> Maybe (SubstCoerce (Shift a) b) Source #

subst :: Name b -> b -> Shift a -> Shift a Source #

substs :: [(Name b, b)] -> Shift a -> Shift a Source #

substPat :: AlphaCtx -> b -> Shift a -> Shift a Source #

substPats :: Proxy * b -> AlphaCtx -> [Dyn] -> Shift a -> Shift a Source #

Eq p => Eq (Shift p) Source # 

Methods

(==) :: Shift p -> Shift p -> Bool #

(/=) :: Shift p -> Shift p -> Bool #

Show a => Show (Shift a) Source # 

Methods

showsPrec :: Int -> Shift a -> ShowS #

show :: Shift a -> String #

showList :: [Shift a] -> ShowS #

Rep p0 => Rep (Shift p0) Source # 

Methods

rep :: R (Shift p0) #

IsEmbed e => IsEmbed (Shift e) Source # 

Associated Types

type Embedded (Shift e) :: * Source #

Alpha a => Alpha (Shift a) Source # 
type Embedded (Shift e) Source # 
type Embedded (Shift e) = Embedded e

Generically derived operations

This section lists a number of operations which are derived generically for any types whose binding structure is specified via the type combinators described in the previous section.

Alpha-equivalence

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

Determine the alpha-equivalence of two terms.

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

Determine (alpha-)equivalence of patterns. Do they bind the same variables in the same patterns and have alpha-equivalent annotations in matching positions?

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

An alpha-respecting total order on terms involving binders.

Variable calculations

Functions for computing the free variables or binding variables of a term or pattern. Note that all these functions may return an arbitrary collection, which includes lists, sets, and multisets.

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

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

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

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

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

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

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

Calculate the variables (of any sort) that occur freely in terms embedded within a pattern (but are not bound by the pattern).

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

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

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

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

Collections

class Foldable f => Collection f where Source #

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, sets, and multisets.

Minimal complete definition

emptyC, singleton, union, cmap

Methods

emptyC :: f a Source #

An empty collection. Must be the identity for union.

singleton :: a -> f a Source #

Create a singleton collection.

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

An associative combining operation. The Ord constraint is in order to accommodate sets.

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

Collections must be functorial. The normal Functor class won't do because of the Ord constraint on sets.

Instances

Collection [] Source #

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

Methods

emptyC :: [a] Source #

singleton :: a -> [a] Source #

union :: Ord a => [a] -> [a] -> [a] Source #

cmap :: (Ord a, Ord b) => (a -> b) -> [a] -> [b] Source #

Collection Set Source #

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

Methods

emptyC :: Set a Source #

singleton :: a -> Set a Source #

union :: Ord a => Set a -> Set a -> Set a Source #

cmap :: (Ord a, Ord b) => (a -> b) -> Set a -> Set b Source #

Collection Multiset Source #

Multisets are containers which preserve multiplicity but not ordering.

Methods

emptyC :: Multiset a Source #

singleton :: a -> Multiset a Source #

union :: Ord a => Multiset a -> Multiset a -> Multiset a Source #

cmap :: (Ord a, Ord b) => (a -> b) -> Multiset a -> Multiset b Source #

newtype Multiset a Source #

A simple representation of multisets.

Constructors

Multiset (Map a Int) 

Instances

Foldable Multiset Source # 

Methods

fold :: Monoid m => Multiset m -> m #

foldMap :: Monoid m => (a -> m) -> Multiset a -> m #

foldr :: (a -> b -> b) -> b -> Multiset a -> b #

foldr' :: (a -> b -> b) -> b -> Multiset a -> b #

foldl :: (b -> a -> b) -> b -> Multiset a -> b #

foldl' :: (b -> a -> b) -> b -> Multiset a -> b #

foldr1 :: (a -> a -> a) -> Multiset a -> a #

foldl1 :: (a -> a -> a) -> Multiset a -> a #

toList :: Multiset a -> [a] #

null :: Multiset a -> Bool #

length :: Multiset a -> Int #

elem :: Eq a => a -> Multiset a -> Bool #

maximum :: Ord a => Multiset a -> a #

minimum :: Ord a => Multiset a -> a #

sum :: Num a => Multiset a -> a #

product :: Num a => Multiset a -> a #

Collection Multiset Source #

Multisets are containers which preserve multiplicity but not ordering.

Methods

emptyC :: Multiset a Source #

singleton :: a -> Multiset a Source #

union :: Ord a => Multiset a -> Multiset a -> Multiset a Source #

cmap :: (Ord a, Ord b) => (a -> b) -> Multiset a -> Multiset b Source #

Substitution

Capture-avoiding substitution.

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

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

This is the only method which normally needs to be implemented explicitly. 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.

isCoerceVar :: a -> Maybe (SubstCoerce a b) Source #

This is an alternative version to isvar, useable in the case that the substituted argument doesn't have *exactly* the same type as the term it should be substituted into. The default implementation always returns Nothing.

subst :: Name b -> b -> a -> a Source #

subst nm sub tm substitutes sub for nm in tm. It has a default generic implementation in terms of isvar.

substs :: [(Name b, b)] -> a -> a Source #

Perform several simultaneous substitutions. This method also has a default generic implementation in terms of isvar.

substPat :: AlphaCtx -> b -> a -> a Source #

substPats :: Proxy b -> AlphaCtx -> [Dyn] -> a -> a Source #

Instances

Subst b AnyName Source # 
Subst b Double Source # 
Subst b Float Source # 
Subst b Integer Source # 
Subst b Char Source # 
Subst b () Source # 

Methods

isvar :: () -> Maybe (SubstName () b) Source #

isCoerceVar :: () -> Maybe (SubstCoerce () b) Source #

subst :: Name b -> b -> () -> () Source #

substs :: [(Name b, b)] -> () -> () Source #

substPat :: AlphaCtx -> b -> () -> () Source #

substPats :: Proxy * b -> AlphaCtx -> [Dyn] -> () -> () Source #

Subst b Bool Source # 
Subst b Int Source # 

Methods

isvar :: Int -> Maybe (SubstName Int b) Source #

isCoerceVar :: Int -> Maybe (SubstCoerce Int b) Source #

subst :: Name b -> b -> Int -> Int Source #

substs :: [(Name b, b)] -> Int -> Int Source #

substPat :: AlphaCtx -> b -> Int -> Int Source #

substPats :: Proxy * b -> AlphaCtx -> [Dyn] -> Int -> Int Source #

Subst c a => Subst c (Maybe a) Source # 

Methods

isvar :: Maybe a -> Maybe (SubstName (Maybe a) c) Source #

isCoerceVar :: Maybe a -> Maybe (SubstCoerce (Maybe a) c) Source #

subst :: Name c -> c -> Maybe a -> Maybe a Source #

substs :: [(Name c, c)] -> Maybe a -> Maybe a Source #

substPat :: AlphaCtx -> c -> Maybe a -> Maybe a Source #

substPats :: Proxy * c -> AlphaCtx -> [Dyn] -> Maybe a -> Maybe a Source #

Subst c a => Subst c [a] Source # 

Methods

isvar :: [a] -> Maybe (SubstName [a] c) Source #

isCoerceVar :: [a] -> Maybe (SubstCoerce [a] c) Source #

subst :: Name c -> c -> [a] -> [a] Source #

substs :: [(Name c, c)] -> [a] -> [a] Source #

substPat :: AlphaCtx -> c -> [a] -> [a] Source #

substPats :: Proxy * c -> AlphaCtx -> [Dyn] -> [a] -> [a] Source #

Rep a => Subst b (Name a) Source # 

Methods

isvar :: Name a -> Maybe (SubstName (Name a) b) Source #

isCoerceVar :: Name a -> Maybe (SubstCoerce (Name a) b) Source #

subst :: Name b -> b -> Name a -> Name a Source #

substs :: [(Name b, b)] -> Name a -> Name a Source #

substPat :: AlphaCtx -> b -> Name a -> Name a Source #

substPats :: Proxy * b -> AlphaCtx -> [Dyn] -> Name a -> Name a Source #

Rep a => Subst b (R a) Source # 

Methods

isvar :: R a -> Maybe (SubstName (R a) b) Source #

isCoerceVar :: R a -> Maybe (SubstCoerce (R a) b) Source #

subst :: Name b -> b -> R a -> R a Source #

substs :: [(Name b, b)] -> R a -> R a Source #

substPat :: AlphaCtx -> b -> R a -> R a Source #

substPats :: Proxy * b -> AlphaCtx -> [Dyn] -> R a -> R a Source #

(Alpha a, Subst b a) => Subst b (Shift a) Source # 

Methods

isvar :: Shift a -> Maybe (SubstName (Shift a) b) Source #

isCoerceVar :: Shift a -> Maybe (SubstCoerce (Shift a) b) Source #

subst :: Name b -> b -> Shift a -> Shift a Source #

substs :: [(Name b, b)] -> Shift a -> Shift a Source #

substPat :: AlphaCtx -> b -> Shift a -> Shift a Source #

substPats :: Proxy * b -> AlphaCtx -> [Dyn] -> Shift a -> Shift a Source #

(Alpha t, Subst b t) => Subst b (Embed t) Source # 

Methods

isvar :: Embed t -> Maybe (SubstName (Embed t) b) Source #

isCoerceVar :: Embed t -> Maybe (SubstCoerce (Embed t) b) Source #

subst :: Name b -> b -> Embed t -> Embed t Source #

substs :: [(Name b, b)] -> Embed t -> Embed t Source #

substPat :: AlphaCtx -> b -> Embed t -> Embed t Source #

substPats :: Proxy * b -> AlphaCtx -> [Dyn] -> Embed t -> Embed t Source #

(Alpha p, Subst b p) => Subst b (Rec p) Source # 

Methods

isvar :: Rec p -> Maybe (SubstName (Rec p) b) Source #

isCoerceVar :: Rec p -> Maybe (SubstCoerce (Rec p) b) Source #

subst :: Name b -> b -> Rec p -> Rec p Source #

substs :: [(Name b, b)] -> Rec p -> Rec p Source #

substPat :: AlphaCtx -> b -> Rec p -> Rec p Source #

substPats :: Proxy * b -> AlphaCtx -> [Dyn] -> Rec p -> Rec p Source #

(Subst c a, Subst c b) => Subst c (Either a b) Source # 

Methods

isvar :: Either a b -> Maybe (SubstName (Either a b) c) Source #

isCoerceVar :: Either a b -> Maybe (SubstCoerce (Either a b) c) Source #

subst :: Name c -> c -> Either a b -> Either a b Source #

substs :: [(Name c, c)] -> Either a b -> Either a b Source #

substPat :: AlphaCtx -> c -> Either a b -> Either a b Source #

substPats :: Proxy * c -> AlphaCtx -> [Dyn] -> Either a b -> Either a b Source #

(Subst c a, Subst c b) => Subst c (a, b) Source # 

Methods

isvar :: (a, b) -> Maybe (SubstName (a, b) c) Source #

isCoerceVar :: (a, b) -> Maybe (SubstCoerce (a, b) c) Source #

subst :: Name c -> c -> (a, b) -> (a, b) Source #

substs :: [(Name c, c)] -> (a, b) -> (a, b) Source #

substPat :: AlphaCtx -> c -> (a, b) -> (a, b) Source #

substPats :: Proxy * c -> AlphaCtx -> [Dyn] -> (a, b) -> (a, b) Source #

(Alpha p, Alpha q, Subst b p, Subst b q) => Subst b (Rebind p q) Source # 

Methods

isvar :: Rebind p q -> Maybe (SubstName (Rebind p q) b) Source #

isCoerceVar :: Rebind p q -> Maybe (SubstCoerce (Rebind p q) b) Source #

subst :: Name b -> b -> Rebind p q -> Rebind p q Source #

substs :: [(Name b, b)] -> Rebind p q -> Rebind p q Source #

substPat :: AlphaCtx -> b -> Rebind p q -> Rebind p q Source #

substPats :: Proxy * b -> AlphaCtx -> [Dyn] -> Rebind p q -> Rebind p q Source #

(Subst c a, Subst c b, Subst c d) => Subst c (a, b, d) Source # 

Methods

isvar :: (a, b, d) -> Maybe (SubstName (a, b, d) c) Source #

isCoerceVar :: (a, b, d) -> Maybe (SubstCoerce (a, b, d) c) Source #

subst :: Name c -> c -> (a, b, d) -> (a, b, d) Source #

substs :: [(Name c, c)] -> (a, b, d) -> (a, b, d) Source #

substPat :: AlphaCtx -> c -> (a, b, d) -> (a, b, d) Source #

substPats :: Proxy * c -> AlphaCtx -> [Dyn] -> (a, b, d) -> (a, b, d) Source #

(Subst c a, Subst c b, Subst c d, Subst c e) => Subst c (a, b, d, e) Source # 

Methods

isvar :: (a, b, d, e) -> Maybe (SubstName (a, b, d, e) c) Source #

isCoerceVar :: (a, b, d, e) -> Maybe (SubstCoerce (a, b, d, e) c) Source #

subst :: Name c -> c -> (a, b, d, e) -> (a, b, d, e) Source #

substs :: [(Name c, c)] -> (a, b, d, e) -> (a, b, d, e) Source #

substPat :: AlphaCtx -> c -> (a, b, d, e) -> (a, b, d, e) Source #

substPats :: Proxy * c -> AlphaCtx -> [Dyn] -> (a, b, d, e) -> (a, b, d, e) Source #

(Rep order, Rep card, Alpha p, Alpha t, Subst b p, Subst b t) => Subst b (GenBind order card p t) Source # 

Methods

isvar :: GenBind order card p t -> Maybe (SubstName (GenBind order card p t) b) Source #

isCoerceVar :: GenBind order card p t -> Maybe (SubstCoerce (GenBind order card p t) b) Source #

subst :: Name b -> b -> GenBind order card p t -> GenBind order card p t Source #

substs :: [(Name b, b)] -> GenBind order card p t -> GenBind order card p t Source #

substPat :: AlphaCtx -> b -> GenBind order card p t -> GenBind order card p t Source #

substPats :: Proxy * b -> AlphaCtx -> [Dyn] -> GenBind order card p t -> GenBind order card p t Source #

(Subst c a, Subst c b, Subst c d, Subst c e, Subst c f) => Subst c (a, b, d, e, f) Source # 

Methods

isvar :: (a, b, d, e, f) -> Maybe (SubstName (a, b, d, e, f) c) Source #

isCoerceVar :: (a, b, d, e, f) -> Maybe (SubstCoerce (a, b, d, e, f) c) Source #

subst :: Name c -> c -> (a, b, d, e, f) -> (a, b, d, e, f) Source #

substs :: [(Name c, c)] -> (a, b, d, e, f) -> (a, b, d, e, f) Source #

substPat :: AlphaCtx -> c -> (a, b, d, e, f) -> (a, b, d, e, f) Source #

substPats :: Proxy * c -> AlphaCtx -> [Dyn] -> (a, b, d, e, f) -> (a, b, d, e, f) Source #

data SubstName a b where Source #

See isvar.

Constructors

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

substBind :: Subst a b => Bind (Name a) b -> a -> b Source #

Immediately substitute for a (single) bound variable in a binder, without first naming that variable.

Permutations

data Perm a Source #

A permutation is a bijective function from names to names which is the identity on all but a finite set of names. They form the basis for nominal approaches to binding, but can also be useful in general.

Instances

Ord a => Eq (Perm a) Source # 

Methods

(==) :: Perm a -> Perm a -> Bool #

(/=) :: Perm a -> Perm a -> Bool #

Show a => Show (Perm a) Source # 

Methods

showsPrec :: Int -> Perm a -> ShowS #

show :: Perm a -> String #

showList :: [Perm a] -> ShowS #

Ord a => Monoid (Perm a) Source #

Permutations form a monoid under composition.

Methods

mempty :: Perm a #

mappend :: Perm a -> Perm a -> Perm a #

mconcat :: [Perm a] -> Perm a #

Working with permutations

single :: Ord a => a -> a -> Perm a Source #

Create a permutation which swaps two elements.

compose :: Ord a => Perm a -> Perm a -> Perm a Source #

Compose two permutations. The right-hand permutation will be applied first.

apply :: Ord a => Perm a -> a -> a Source #

Apply a permutation to an element of the domain.

support :: Ord a => Perm a -> [a] Source #

The support of a permutation is the set of elements which are not fixed.

isid :: Ord a => Perm a -> Bool Source #

Is this the identity permutation?

join :: Ord a => Perm a -> Perm a -> Maybe (Perm a) Source #

Join two permutations by taking the union of their relation graphs. Fail if they are inconsistent, i.e. map the same element to two different elements.

empty :: Perm a Source #

The empty (identity) permutation.

restrict :: Ord a => Perm a -> [a] -> Perm a Source #

Restrict a permutation to a certain domain.

mkPerm :: Ord a => [a] -> [a] -> Maybe (Perm a) Source #

mkPerm l1 l2 creates a permutation that sends l1 to l2. Fail if there is no such permutation, either because the lists have different lengths or because they are inconsistent (which can only happen if l1 or l2 have repeated elements).

Permuting terms

swaps :: Alpha t => Perm AnyName -> t -> t Source #

Apply a permutation to a term.

swapsEmbeds :: Alpha p => Perm AnyName -> p -> p Source #

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

swapsBinders :: Alpha p => Perm AnyName -> p -> p Source #

Apply a permutation to the binding variables in a pattern. Embedded terms are left alone by the permutation.

Freshness

When opening a term-level binding (Bind or TRec), fresh names must be generated for the binders of its pattern. Fresh names can be generated according to one of two strategies: names can be globally fresh (not conflicting with any other generated names, ever; see Fresh) or locally fresh (not conflicting only with a specific set of "currently in-scope" names; see LFresh). Generating globally fresh names is simpler and suffices for many applications. Generating locally fresh names tends to be useful when the names are for human consumption, e.g. when implementing a pretty-printer.

Global freshness

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

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.

The Fresh class

class Monad m => Fresh m where Source #

The Fresh type class governs monads which can generate new globally unique Names based on a given Name.

Minimal complete definition

fresh

Methods

fresh :: Rep a => Name a -> m (Name a) Source #

Generate a new globally unique name based on the given one.

Instances

Fresh m => Fresh (ListT m) Source # 

Methods

fresh :: Rep a => Name a -> ListT m (Name a) Source #

Fresh m => Fresh (MaybeT m) Source # 

Methods

fresh :: Rep a => Name a -> MaybeT m (Name a) Source #

Monad m => Fresh (FreshMT m) Source # 

Methods

fresh :: Rep a => Name a -> FreshMT m (Name a) Source #

Fresh m => Fresh (ExceptT e m) Source # 

Methods

fresh :: Rep a => Name a -> ExceptT e m (Name a) Source #

Fresh m => Fresh (StateT s m) Source # 

Methods

fresh :: Rep a => Name a -> StateT s m (Name a) Source #

Fresh m => Fresh (StateT s m) Source # 

Methods

fresh :: Rep a => Name a -> StateT s m (Name a) Source #

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

Methods

fresh :: Rep a => Name a -> WriterT w m (Name a) Source #

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

Methods

fresh :: Rep a => Name a -> WriterT w m (Name a) Source #

Fresh m => Fresh (IdentityT * m) Source # 

Methods

fresh :: Rep a => Name a -> IdentityT * m (Name a) Source #

Fresh m => Fresh (ContT * r m) Source # 

Methods

fresh :: Rep a => Name a -> ContT * r m (Name a) Source #

Fresh m => Fresh (ReaderT * r m) Source # 

Methods

fresh :: Rep a => Name a -> ReaderT * r m (Name a) Source #

The FreshM monad

The FreshM monad provides a concrete implementation of the Fresh type class. The FreshMT monad transformer variant can be freely combined with other standard monads and monad transformers from the transformers library.

type FreshM = FreshMT Identity Source #

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 Source #

Run a FreshM computation (with the global index starting at zero).

data FreshMT m a Source #

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 Source # 

Methods

lift :: Monad m => m a -> FreshMT m a #

MonadError e m => MonadError e (FreshMT m) Source # 

Methods

throwError :: e -> FreshMT m a #

catchError :: FreshMT m a -> (e -> FreshMT m a) -> FreshMT m a #

MonadReader r m => MonadReader r (FreshMT m) Source # 

Methods

ask :: FreshMT m r #

local :: (r -> r) -> FreshMT m a -> FreshMT m a #

reader :: (r -> a) -> FreshMT m a #

MonadState s m => MonadState s (FreshMT m) Source # 

Methods

get :: FreshMT m s #

put :: s -> FreshMT m () #

state :: (s -> (a, s)) -> FreshMT m a #

MonadWriter w m => MonadWriter w (FreshMT m) Source # 

Methods

writer :: (a, w) -> FreshMT m a #

tell :: w -> FreshMT m () #

listen :: FreshMT m a -> FreshMT m (a, w) #

pass :: FreshMT m (a, w -> w) -> FreshMT m a #

Monad m => Monad (FreshMT m) Source # 

Methods

(>>=) :: FreshMT m a -> (a -> FreshMT m b) -> FreshMT m b #

(>>) :: FreshMT m a -> FreshMT m b -> FreshMT m b #

return :: a -> FreshMT m a #

fail :: String -> FreshMT m a #

Functor m => Functor (FreshMT m) Source # 

Methods

fmap :: (a -> b) -> FreshMT m a -> FreshMT m b #

(<$) :: a -> FreshMT m b -> FreshMT m a #

MonadFix m => MonadFix (FreshMT m) Source # 

Methods

mfix :: (a -> FreshMT m a) -> FreshMT m a #

Monad m => Applicative (FreshMT m) Source # 

Methods

pure :: a -> FreshMT m a #

(<*>) :: FreshMT m (a -> b) -> FreshMT m a -> FreshMT m b #

(*>) :: FreshMT m a -> FreshMT m b -> FreshMT m b #

(<*) :: FreshMT m a -> FreshMT m b -> FreshMT m a #

MonadIO m => MonadIO (FreshMT m) Source # 

Methods

liftIO :: IO a -> FreshMT m a #

MonadPlus m => Alternative (FreshMT m) Source # 

Methods

empty :: FreshMT m a #

(<|>) :: FreshMT m a -> FreshMT m a -> FreshMT m a #

some :: FreshMT m a -> FreshMT m [a] #

many :: FreshMT m a -> FreshMT m [a] #

MonadPlus m => MonadPlus (FreshMT m) Source # 

Methods

mzero :: FreshMT m a #

mplus :: FreshMT m a -> FreshMT m a -> FreshMT m a #

MonadCont m => MonadCont (FreshMT m) Source # 

Methods

callCC :: ((a -> FreshMT m b) -> FreshMT m a) -> FreshMT m a #

Monad m => Fresh (FreshMT m) Source # 

Methods

fresh :: Rep a => Name a -> FreshMT m (Name a) Source #

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

Run a FreshMT computation (with the global index starting at zero).

Local freshness

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

"Locally" freshen a pattern, replacing all binding names with new names that are not already "in scope". The second argument is a continuation, which takes the renamed term and a permutation that specifies how the pattern has been renamed. The resulting computation will be run with the in-scope set extended by the names just generated.

The LFresh class

class Monad m => LFresh m where Source #

This is the class of monads that support freshness in an (implicit) local scope. Generated names are fresh for the current local scope, not necessarily globally fresh.

Minimal complete definition

lfresh, avoid, getAvoids

Methods

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

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

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

Avoid the given names when freshening in the subcomputation, that is, add the given names to the in-scope set.

getAvoids :: m (Set AnyName) Source #

Get the set of names currently being avoided.

Instances

LFresh m => LFresh (ListT m) Source # 

Methods

lfresh :: Rep a => Name a -> ListT m (Name a) Source #

avoid :: [AnyName] -> ListT m a -> ListT m a Source #

getAvoids :: ListT m (Set AnyName) Source #

LFresh m => LFresh (MaybeT m) Source # 

Methods

lfresh :: Rep a => Name a -> MaybeT m (Name a) Source #

avoid :: [AnyName] -> MaybeT m a -> MaybeT m a Source #

getAvoids :: MaybeT m (Set AnyName) Source #

Monad m => LFresh (LFreshMT m) Source # 

Methods

lfresh :: Rep a => Name a -> LFreshMT m (Name a) Source #

avoid :: [AnyName] -> LFreshMT m a -> LFreshMT m a Source #

getAvoids :: LFreshMT m (Set AnyName) Source #

LFresh m => LFresh (ExceptT e m) Source # 

Methods

lfresh :: Rep a => Name a -> ExceptT e m (Name a) Source #

avoid :: [AnyName] -> ExceptT e m a -> ExceptT e m a Source #

getAvoids :: ExceptT e m (Set AnyName) Source #

LFresh m => LFresh (StateT s m) Source # 

Methods

lfresh :: Rep a => Name a -> StateT s m (Name a) Source #

avoid :: [AnyName] -> StateT s m a -> StateT s m a Source #

getAvoids :: StateT s m (Set AnyName) Source #

LFresh m => LFresh (StateT s m) Source # 

Methods

lfresh :: Rep a => Name a -> StateT s m (Name a) Source #

avoid :: [AnyName] -> StateT s m a -> StateT s m a Source #

getAvoids :: StateT s m (Set AnyName) Source #

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

Methods

lfresh :: Rep a => Name a -> WriterT w m (Name a) Source #

avoid :: [AnyName] -> WriterT w m a -> WriterT w m a Source #

getAvoids :: WriterT w m (Set AnyName) Source #

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

Methods

lfresh :: Rep a => Name a -> WriterT w m (Name a) Source #

avoid :: [AnyName] -> WriterT w m a -> WriterT w m a Source #

getAvoids :: WriterT w m (Set AnyName) Source #

LFresh m => LFresh (IdentityT * m) Source # 
LFresh m => LFresh (ContT * r m) Source # 

Methods

lfresh :: Rep a => Name a -> ContT * r m (Name a) Source #

avoid :: [AnyName] -> ContT * r m a -> ContT * r m a Source #

getAvoids :: ContT * r m (Set AnyName) Source #

LFresh m => LFresh (ReaderT * r m) Source # 

Methods

lfresh :: Rep a => Name a -> ReaderT * r m (Name a) Source #

avoid :: [AnyName] -> ReaderT * r m a -> ReaderT * r m a Source #

getAvoids :: ReaderT * r m (Set AnyName) Source #

The LFreshM monad

The LFreshM monad provides a concrete implementation of the LFresh type class. The LFreshMT monad transformer variant can be freely combined with other standard monads and monad transformers from the transformers library.

type LFreshM = LFreshMT Identity Source #

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 Source #

Run a LFreshM computation in an empty context.

data LFreshMT m a Source #

The LFresh monad transformer. Keeps track of a set of names to avoid, and when asked for a fresh one will choose the first numeric prefix of the given name which is currently unused.

Instances

MonadTrans LFreshMT Source # 

Methods

lift :: Monad m => m a -> LFreshMT m a #

MonadError e m => MonadError e (LFreshMT m) Source # 

Methods

throwError :: e -> LFreshMT m a #

catchError :: LFreshMT m a -> (e -> LFreshMT m a) -> LFreshMT m a #

MonadReader r m => MonadReader r (LFreshMT m) Source # 

Methods

ask :: LFreshMT m r #

local :: (r -> r) -> LFreshMT m a -> LFreshMT m a #

reader :: (r -> a) -> LFreshMT m a #

MonadState s m => MonadState s (LFreshMT m) Source # 

Methods

get :: LFreshMT m s #

put :: s -> LFreshMT m () #

state :: (s -> (a, s)) -> LFreshMT m a #

MonadWriter w m => MonadWriter w (LFreshMT m) Source # 

Methods

writer :: (a, w) -> LFreshMT m a #

tell :: w -> LFreshMT m () #

listen :: LFreshMT m a -> LFreshMT m (a, w) #

pass :: LFreshMT m (a, w -> w) -> LFreshMT m a #

Monad m => Monad (LFreshMT m) Source # 

Methods

(>>=) :: LFreshMT m a -> (a -> LFreshMT m b) -> LFreshMT m b #

(>>) :: LFreshMT m a -> LFreshMT m b -> LFreshMT m b #

return :: a -> LFreshMT m a #

fail :: String -> LFreshMT m a #

Functor m => Functor (LFreshMT m) Source # 

Methods

fmap :: (a -> b) -> LFreshMT m a -> LFreshMT m b #

(<$) :: a -> LFreshMT m b -> LFreshMT m a #

MonadFix m => MonadFix (LFreshMT m) Source # 

Methods

mfix :: (a -> LFreshMT m a) -> LFreshMT m a #

Applicative m => Applicative (LFreshMT m) Source # 

Methods

pure :: a -> LFreshMT m a #

(<*>) :: LFreshMT m (a -> b) -> LFreshMT m a -> LFreshMT m b #

(*>) :: LFreshMT m a -> LFreshMT m b -> LFreshMT m b #

(<*) :: LFreshMT m a -> LFreshMT m b -> LFreshMT m a #

MonadIO m => MonadIO (LFreshMT m) Source # 

Methods

liftIO :: IO a -> LFreshMT m a #

Alternative m => Alternative (LFreshMT m) Source # 

Methods

empty :: LFreshMT m a #

(<|>) :: LFreshMT m a -> LFreshMT m a -> LFreshMT m a #

some :: LFreshMT m a -> LFreshMT m [a] #

many :: LFreshMT m a -> LFreshMT m [a] #

MonadPlus m => MonadPlus (LFreshMT m) Source # 

Methods

mzero :: LFreshMT m a #

mplus :: LFreshMT m a -> LFreshMT m a -> LFreshMT m a #

MonadCont m => MonadCont (LFreshMT m) Source # 

Methods

callCC :: ((a -> LFreshMT m b) -> LFreshMT m a) -> LFreshMT m a #

Monad m => LFresh (LFreshMT m) Source # 

Methods

lfresh :: Rep a => Name a -> LFreshMT m (Name a) Source #

avoid :: [AnyName] -> LFreshMT m a -> LFreshMT m a Source #

getAvoids :: LFreshMT m (Set AnyName) Source #

runLFreshMT :: LFreshMT m a -> m a Source #

Run an LFreshMT computation in an empty context.

The Alpha class

class Rep1 AlphaD a => Alpha a where Source #

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 almost never be called directly. Instead, use other methods provided by this module which are defined in terms of Alpha methods.

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

Occasionally, however, it may be useful to override the default implementations of one or more Alpha methods for a particular type. For example, consider a type like

data Term = ...
          | Annotation Stuff Term

where the Annotation constructor of Term associates some sort of annotation with a term --- say, information obtained from a parser about where in an input file the term came from. This information is needed to produce good error messages, but should not be taken into consideration when, say, comparing two Terms for alpha-equivalence. In order to make aeq ignore annotations, you can override the implementation of aeq' like so:

instance Alpha Term where
  aeq' c (Annotation _ t1) t2 = aeq' c t1 t2
  aeq' c t1 (Annotation _ t2) = aeq' c t1 t2
  aeq' c t1 t2 = aeqR1 rep1 t1 t2

Note how the call to aeqR1 handles all the other cases generically.

If you use Abstract types (i.e. those with representations derived via derive_abstract) then you must provide a definition of aeq' and acompare'. In these cases, Unbound has no information about the structure of the type and cannot do anything sensible.

Methods

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

See swaps.

fv' :: Collection f => AlphaCtx -> a -> f AnyName Source #

See fv.

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

See lfreshen.

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

See freshen.

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

See aeq.

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

See acompare.

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

Replace free names by bound names.

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

Replace bound names by free names.

isPat :: a -> Maybe [AnyName] Source #

isPat x dynamically checks whether x can be used as a valid pattern. The default instance returns Just if at all possible. If successful, returns a list of names bound by the pattern.

isTerm :: a -> Bool Source #

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 Source #

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 Source #

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 Source #

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

Instances

Alpha Bool Source # 
Alpha Char Source # 
Alpha Double Source # 
Alpha Float Source # 
Alpha Int Source # 
Alpha Integer Source # 
Alpha () Source # 

Methods

swaps' :: AlphaCtx -> Perm AnyName -> () -> () Source #

fv' :: Collection f => AlphaCtx -> () -> f AnyName Source #

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

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

aeq' :: AlphaCtx -> () -> () -> Bool Source #

acompare' :: AlphaCtx -> () -> () -> Ordering Source #

close :: Alpha b => AlphaCtx -> b -> () -> () Source #

open :: Alpha b => AlphaCtx -> b -> () -> () Source #

isPat :: () -> Maybe [AnyName] Source #

isTerm :: () -> Bool Source #

isEmbed :: () -> Bool Source #

nthpatrec :: () -> NthCont Source #

findpatrec :: () -> AnyName -> FindResult Source #

Alpha AnyName Source # 
Alpha a => Alpha [a] Source # 

Methods

swaps' :: AlphaCtx -> Perm AnyName -> [a] -> [a] Source #

fv' :: Collection f => AlphaCtx -> [a] -> f AnyName Source #

lfreshen' :: LFresh m => AlphaCtx -> [a] -> ([a] -> Perm AnyName -> m b) -> m b Source #

freshen' :: Fresh m => AlphaCtx -> [a] -> m ([a], Perm AnyName) Source #

aeq' :: AlphaCtx -> [a] -> [a] -> Bool Source #

acompare' :: AlphaCtx -> [a] -> [a] -> Ordering Source #

close :: Alpha b => AlphaCtx -> b -> [a] -> [a] Source #

open :: Alpha b => AlphaCtx -> b -> [a] -> [a] Source #

isPat :: [a] -> Maybe [AnyName] Source #

isTerm :: [a] -> Bool Source #

isEmbed :: [a] -> Bool Source #

nthpatrec :: [a] -> NthCont Source #

findpatrec :: [a] -> AnyName -> FindResult Source #

Alpha a => Alpha (Maybe a) Source # 
Rep a => Alpha (R a) Source # 

Methods

swaps' :: AlphaCtx -> Perm AnyName -> R a -> R a Source #

fv' :: Collection f => AlphaCtx -> R a -> f AnyName Source #

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

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

aeq' :: AlphaCtx -> R a -> R a -> Bool Source #

acompare' :: AlphaCtx -> R a -> R a -> Ordering Source #

close :: Alpha b => AlphaCtx -> b -> R a -> R a Source #

open :: Alpha b => AlphaCtx -> b -> R a -> R a Source #

isPat :: R a -> Maybe [AnyName] Source #

isTerm :: R a -> Bool Source #

isEmbed :: R a -> Bool Source #

nthpatrec :: R a -> NthCont Source #

findpatrec :: R a -> AnyName -> FindResult Source #

Rep a => Alpha (Name a) Source # 

Methods

swaps' :: AlphaCtx -> Perm AnyName -> Name a -> Name a Source #

fv' :: Collection f => AlphaCtx -> Name a -> f AnyName Source #

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

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

aeq' :: AlphaCtx -> Name a -> Name a -> Bool Source #

acompare' :: AlphaCtx -> Name a -> Name a -> Ordering Source #

close :: Alpha b => AlphaCtx -> b -> Name a -> Name a Source #

open :: Alpha b => AlphaCtx -> b -> Name a -> Name a Source #

isPat :: Name a -> Maybe [AnyName] Source #

isTerm :: Name a -> Bool Source #

isEmbed :: Name a -> Bool Source #

nthpatrec :: Name a -> NthCont Source #

findpatrec :: Name a -> AnyName -> FindResult Source #

Alpha a => Alpha (Shift a) Source # 
Alpha t => Alpha (Embed t) Source # 
Alpha p => Alpha (Rec p) Source # 

Methods

swaps' :: AlphaCtx -> Perm AnyName -> Rec p -> Rec p Source #

fv' :: Collection f => AlphaCtx -> Rec p -> f AnyName Source #

lfreshen' :: LFresh m => AlphaCtx -> Rec p -> (Rec p -> Perm AnyName -> m b) -> m b Source #

freshen' :: Fresh m => AlphaCtx -> Rec p -> m (Rec p, Perm AnyName) Source #

aeq' :: AlphaCtx -> Rec p -> Rec p -> Bool Source #

acompare' :: AlphaCtx -> Rec p -> Rec p -> Ordering Source #

close :: Alpha b => AlphaCtx -> b -> Rec p -> Rec p Source #

open :: Alpha b => AlphaCtx -> b -> Rec p -> Rec p Source #

isPat :: Rec p -> Maybe [AnyName] Source #

isTerm :: Rec p -> Bool Source #

isEmbed :: Rec p -> Bool Source #

nthpatrec :: Rec p -> NthCont Source #

findpatrec :: Rec p -> AnyName -> FindResult Source #

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

Methods

swaps' :: AlphaCtx -> Perm AnyName -> Either a b -> Either a b Source #

fv' :: Collection f => AlphaCtx -> Either a b -> f AnyName Source #

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

freshen' :: Fresh m => AlphaCtx -> Either a b -> m (Either a b, Perm AnyName) Source #

aeq' :: AlphaCtx -> Either a b -> Either a b -> Bool Source #

acompare' :: AlphaCtx -> Either a b -> Either a b -> Ordering Source #

close :: Alpha b => AlphaCtx -> b -> Either a b -> Either a b Source #

open :: Alpha b => AlphaCtx -> b -> Either a b -> Either a b Source #

isPat :: Either a b -> Maybe [AnyName] Source #

isTerm :: Either a b -> Bool Source #

isEmbed :: Either a b -> Bool Source #

nthpatrec :: Either a b -> NthCont Source #

findpatrec :: Either a b -> AnyName -> FindResult Source #

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

Methods

swaps' :: AlphaCtx -> Perm AnyName -> (a, b) -> (a, b) Source #

fv' :: Collection f => AlphaCtx -> (a, b) -> f AnyName Source #

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

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

aeq' :: AlphaCtx -> (a, b) -> (a, b) -> Bool Source #

acompare' :: AlphaCtx -> (a, b) -> (a, b) -> Ordering Source #

close :: Alpha b => AlphaCtx -> b -> (a, b) -> (a, b) Source #

open :: Alpha b => AlphaCtx -> b -> (a, b) -> (a, b) Source #

isPat :: (a, b) -> Maybe [AnyName] Source #

isTerm :: (a, b) -> Bool Source #

isEmbed :: (a, b) -> Bool Source #

nthpatrec :: (a, b) -> NthCont Source #

findpatrec :: (a, b) -> AnyName -> FindResult Source #

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

Methods

swaps' :: AlphaCtx -> Perm AnyName -> Rebind p q -> Rebind p q Source #

fv' :: Collection f => AlphaCtx -> Rebind p q -> f AnyName Source #

lfreshen' :: LFresh m => AlphaCtx -> Rebind p q -> (Rebind p q -> Perm AnyName -> m b) -> m b Source #

freshen' :: Fresh m => AlphaCtx -> Rebind p q -> m (Rebind p q, Perm AnyName) Source #

aeq' :: AlphaCtx -> Rebind p q -> Rebind p q -> Bool Source #

acompare' :: AlphaCtx -> Rebind p q -> Rebind p q -> Ordering Source #

close :: Alpha b => AlphaCtx -> b -> Rebind p q -> Rebind p q Source #

open :: Alpha b => AlphaCtx -> b -> Rebind p q -> Rebind p q Source #

isPat :: Rebind p q -> Maybe [AnyName] Source #

isTerm :: Rebind p q -> Bool Source #

isEmbed :: Rebind p q -> Bool Source #

nthpatrec :: Rebind p q -> NthCont Source #

findpatrec :: Rebind p q -> AnyName -> FindResult Source #

(Alpha a, Alpha b, Alpha c) => Alpha (a, b, c) Source # 

Methods

swaps' :: AlphaCtx -> Perm AnyName -> (a, b, c) -> (a, b, c) Source #

fv' :: Collection f => AlphaCtx -> (a, b, c) -> f AnyName Source #

lfreshen' :: LFresh m => AlphaCtx -> (a, b, c) -> ((a, b, c) -> Perm AnyName -> m b) -> m b Source #

freshen' :: Fresh m => AlphaCtx -> (a, b, c) -> m ((a, b, c), Perm AnyName) Source #

aeq' :: AlphaCtx -> (a, b, c) -> (a, b, c) -> Bool Source #

acompare' :: AlphaCtx -> (a, b, c) -> (a, b, c) -> Ordering Source #

close :: Alpha b => AlphaCtx -> b -> (a, b, c) -> (a, b, c) Source #

open :: Alpha b => AlphaCtx -> b -> (a, b, c) -> (a, b, c) Source #

isPat :: (a, b, c) -> Maybe [AnyName] Source #

isTerm :: (a, b, c) -> Bool Source #

isEmbed :: (a, b, c) -> Bool Source #

nthpatrec :: (a, b, c) -> NthCont Source #

findpatrec :: (a, b, c) -> AnyName -> FindResult Source #

(Alpha a, Alpha b, Alpha c, Alpha d) => Alpha (a, b, c, d) Source # 

Methods

swaps' :: AlphaCtx -> Perm AnyName -> (a, b, c, d) -> (a, b, c, d) Source #

fv' :: Collection f => AlphaCtx -> (a, b, c, d) -> f AnyName Source #

lfreshen' :: LFresh m => AlphaCtx -> (a, b, c, d) -> ((a, b, c, d) -> Perm AnyName -> m b) -> m b Source #

freshen' :: Fresh m => AlphaCtx -> (a, b, c, d) -> m ((a, b, c, d), Perm AnyName) Source #

aeq' :: AlphaCtx -> (a, b, c, d) -> (a, b, c, d) -> Bool Source #

acompare' :: AlphaCtx -> (a, b, c, d) -> (a, b, c, d) -> Ordering Source #

close :: Alpha b => AlphaCtx -> b -> (a, b, c, d) -> (a, b, c, d) Source #

open :: Alpha b => AlphaCtx -> b -> (a, b, c, d) -> (a, b, c, d) Source #

isPat :: (a, b, c, d) -> Maybe [AnyName] Source #

isTerm :: (a, b, c, d) -> Bool Source #

isEmbed :: (a, b, c, d) -> Bool Source #

nthpatrec :: (a, b, c, d) -> NthCont Source #

findpatrec :: (a, b, c, d) -> AnyName -> FindResult Source #

(Rep order, Rep card, Alpha p, Alpha t) => Alpha (GenBind order card p t) Source # 

Methods

swaps' :: AlphaCtx -> Perm AnyName -> GenBind order card p t -> GenBind order card p t Source #

fv' :: Collection f => AlphaCtx -> GenBind order card p t -> f AnyName Source #

lfreshen' :: LFresh m => AlphaCtx -> GenBind order card p t -> (GenBind order card p t -> Perm AnyName -> m b) -> m b Source #

freshen' :: Fresh m => AlphaCtx -> GenBind order card p t -> m (GenBind order card p t, Perm AnyName) Source #

aeq' :: AlphaCtx -> GenBind order card p t -> GenBind order card p t -> Bool Source #

acompare' :: AlphaCtx -> GenBind order card p t -> GenBind order card p t -> Ordering Source #

close :: Alpha b => AlphaCtx -> b -> GenBind order card p t -> GenBind order card p t Source #

open :: Alpha b => AlphaCtx -> b -> GenBind order card p t -> GenBind order card p t Source #

isPat :: GenBind order card p t -> Maybe [AnyName] Source #

isTerm :: GenBind order card p t -> Bool Source #

isEmbed :: GenBind order card p t -> Bool Source #

nthpatrec :: GenBind order card p t -> NthCont Source #

findpatrec :: GenBind order card p t -> AnyName -> FindResult Source #

(Alpha a, Alpha b, Alpha c, Alpha d, Alpha e) => Alpha (a, b, c, d, e) Source # 

Methods

swaps' :: AlphaCtx -> Perm AnyName -> (a, b, c, d, e) -> (a, b, c, d, e) Source #

fv' :: Collection f => AlphaCtx -> (a, b, c, d, e) -> f AnyName Source #

lfreshen' :: LFresh m => AlphaCtx -> (a, b, c, d, e) -> ((a, b, c, d, e) -> Perm AnyName -> m b) -> m b Source #

freshen' :: Fresh m => AlphaCtx -> (a, b, c, d, e) -> m ((a, b, c, d, e), Perm AnyName) Source #

aeq' :: AlphaCtx -> (a, b, c, d, e) -> (a, b, c, d, e) -> Bool Source #

acompare' :: AlphaCtx -> (a, b, c, d, e) -> (a, b, c, d, e) -> Ordering Source #

close :: Alpha b => AlphaCtx -> b -> (a, b, c, d, e) -> (a, b, c, d, e) Source #

open :: Alpha b => AlphaCtx -> b -> (a, b, c, d, e) -> (a, b, c, d, e) Source #

isPat :: (a, b, c, d, e) -> Maybe [AnyName] Source #

isTerm :: (a, b, c, d, e) -> Bool Source #

isEmbed :: (a, b, c, d, e) -> Bool Source #

nthpatrec :: (a, b, c, d, e) -> NthCont Source #

findpatrec :: (a, b, c, d, e) -> AnyName -> FindResult Source #

Re-exported RepLib API for convenience

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. Rep a => R (Name a) Source #

rGenBind :: forall order card p t. (Rep order, Rep card, Rep p, Rep t) => R (GenBind order card p t) Source #

rRebind :: forall p1 p2. (Rep p1, Rep p2) => R (Rebind p1 p2) Source #

rEmbed :: forall t. Rep t => R (Embed t) Source #

rRec :: forall p. Rep p => R (Rec p) Source #

rShift :: forall p. Rep p => R (Shift p) Source #