Portability | GHC only (-XKitchenSink) |
---|---|
Stability | experimental |
Maintainer | Brent Yorgey <byorgey@cis.upenn.edu> |
Safe Haskell | None |
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.
- data Name a
- data AnyName = forall a . Rep a => AnyName (Name a)
- integer2Name :: Rep a => Integer -> Name a
- string2Name :: Rep a => String -> Name a
- s2n :: Rep a => String -> Name a
- makeName :: Rep a => String -> Integer -> Name a
- name2Integer :: Name a -> Integer
- name2String :: Name a -> String
- anyName2Integer :: AnyName -> Integer
- anyName2String :: AnyName -> String
- translate :: Rep b => Name a -> Name b
- toSortedName :: Rep a => AnyName -> Maybe (Name a)
- type Bind p t = GenBind StrictOrder StrictCard p t
- bind :: (Alpha p, Alpha t) => p -> t -> Bind p t
- permbind :: (Alpha p, Alpha t) => p -> t -> SetBind p t
- setbind :: (Alpha a, Alpha t) => [Name a] -> t -> SetPlusBind [Name a] t
- setbindAny :: Alpha t => [AnyName] -> t -> SetPlusBind [AnyName] t
- unbind :: (Fresh m, Alpha p, Alpha t) => GenBind order card p t -> m (p, t)
- lunbind :: (LFresh m, Alpha p, Alpha t) => GenBind order card p t -> ((p, t) -> m c) -> m c
- 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))
- 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))
- 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
- 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
- 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)
- 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)
- 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
- 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
- newtype Embed t = Embed t
- embed :: IsEmbed e => Embedded e -> e
- unembed :: IsEmbed e => e -> Embedded e
- data Rebind p1 p2
- rebind :: (Alpha p1, Alpha p2) => p1 -> p2 -> Rebind p1 p2
- unrebind :: (Alpha p1, Alpha p2) => Rebind p1 p2 -> (p1, p2)
- data Rec p
- rec :: Alpha p => p -> Rec p
- unrec :: Alpha p => Rec p -> p
- data TRec p
- trec :: Alpha p => p -> TRec p
- untrec :: (Fresh m, Alpha p) => TRec p -> m p
- luntrec :: (LFresh m, Alpha p) => TRec p -> m p
- newtype Shift p = Shift p
- aeq :: Alpha t => t -> t -> Bool
- aeqBinders :: Alpha p => p -> p -> Bool
- acompare :: Alpha t => t -> t -> Ordering
- fv :: (Rep a, Alpha t, Collection f) => t -> f (Name a)
- fvAny :: (Alpha t, Collection f) => t -> f AnyName
- patfv :: (Rep a, Alpha p, Collection f) => p -> f (Name a)
- patfvAny :: (Alpha p, Collection f) => p -> f AnyName
- binders :: (Rep a, Alpha p, Collection f) => p -> f (Name a)
- bindersAny :: (Alpha p, Collection f) => p -> f AnyName
- class Foldable f => Collection f where
- newtype Multiset a = Multiset (Map a Int)
- class Rep1 (SubstD b) a => Subst b a where
- isvar :: a -> Maybe (SubstName a b)
- isCoerceVar :: a -> Maybe (SubstCoerce a b)
- subst :: Name b -> b -> a -> a
- substs :: [(Name b, b)] -> a -> a
- data SubstName a b where
- data Perm a
- single :: Ord a => a -> a -> Perm a
- compose :: Ord a => Perm a -> Perm a -> Perm a
- apply :: Ord a => Perm a -> a -> a
- support :: Ord a => Perm a -> [a]
- isid :: Ord a => Perm a -> Bool
- join :: Ord a => Perm a -> Perm a -> Maybe (Perm a)
- empty :: Perm a
- restrict :: Ord a => Perm a -> [a] -> Perm a
- mkPerm :: Ord a => [a] -> [a] -> Maybe (Perm a)
- swaps :: Alpha t => Perm AnyName -> t -> t
- swapsEmbeds :: Alpha p => Perm AnyName -> p -> p
- swapsBinders :: Alpha p => Perm AnyName -> p -> p
- freshen :: (Alpha p, Fresh m) => p -> m (p, Perm AnyName)
- class Monad m => Fresh m where
- type FreshM = FreshMT Identity
- runFreshM :: FreshM a -> a
- data FreshMT m a
- runFreshMT :: Monad m => FreshMT m a -> m a
- lfreshen :: (Alpha p, LFresh m) => p -> (p -> Perm AnyName -> m b) -> m b
- class Monad m => LFresh m where
- type LFreshM = LFreshMT Identity
- runLFreshM :: LFreshM a -> a
- data LFreshMT m a
- runLFreshMT :: LFreshMT m a -> m a
- class (Show a, Rep1 AlphaD a) => Alpha a where
- swaps' :: AlphaCtx -> Perm AnyName -> a -> a
- fv' :: Collection f => AlphaCtx -> a -> f AnyName
- lfreshen' :: LFresh m => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b
- freshen' :: Fresh m => AlphaCtx -> a -> m (a, Perm AnyName)
- aeq' :: AlphaCtx -> a -> a -> Bool
- acompare' :: AlphaCtx -> a -> a -> Ordering
- close :: Alpha b => AlphaCtx -> b -> a -> a
- open :: Alpha b => AlphaCtx -> b -> a -> a
- isPat :: a -> Maybe [AnyName]
- isTerm :: a -> Bool
- isEmbed :: a -> Bool
- nthpatrec :: a -> NthCont
- findpatrec :: a -> AnyName -> FindResult
- rName :: forall a. Rep a => R (Name a)
- rGenBind :: forall order card p t. (Rep order, Rep card, Rep p, Rep t) => R (GenBind order card p t)
- rRebind :: forall p1 p2. (Rep p1, Rep p2) => R (Rebind p1 p2)
- rEmbed :: forall t. Rep t => R (Embed t)
- rRec :: forall p. Rep p => R (Rec p)
- rShift :: forall p. Rep p => R (Shift p)
Names
Name
s 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
.
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
.
Constructing and destructing free names
s2n :: Rep a => String -> Name aSource
Convenient synonym for string2Name
.
makeName :: Rep a => String -> Integer -> Name aSource
Create a free Name
from a String
and an Integer
index.
name2Integer :: Name a -> IntegerSource
Get the integer index of a Name
.
name2String :: Name a -> StringSource
Get the string part of a Name
.
anyName2Integer :: AnyName -> IntegerSource
Get the integer index of an AnyName
.
anyName2String :: AnyName -> StringSource
Get the string part of an AnyName
.
Dealing with name sorts
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
Name
s 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, anyName
s 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
Bind constructors
bind :: (Alpha p, Alpha t) => p -> t -> Bind p tSource
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 tSource
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] tSource
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] tSource
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 cSource
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 rSource
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 rSource
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
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
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 rSource
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 rSource
Embed
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
Shift
s at the same time.)
Embed t |
unembed :: IsEmbed e => e -> Embedded eSource
Destruct an embedded term. unembed
can have any of the types
Embed t -> t
Shift (Embed t) -> t
and so on.
Rebind
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
.
(Rep p10, Rep p20, Sat (ctx0 p10), Sat (ctx0 p20)) => Rep1 ctx0 (Rebind p10 p20) | |
(Subst c b, Subst c a, Alpha a, Alpha b) => Subst c (Rebind a b) | |
(Alpha p1, Alpha p2, Eq p2) => Eq (Rebind p1 p2) | Compare for alpha-equality. |
(Show a, Show b) => Show (Rebind a b) | |
(Rep p10, Rep p20) => Rep (Rebind p10 p20) | |
(Alpha p, Alpha q) => Alpha (Rebind p q) |
Rec
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.
TRec
TRec
is a standalone variant of Rec
: the only difference is
that whereas
is a pattern type, Rec
pTRec 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,
corresponds to
alpha-Caml's Embed
tinner t
, and
corresponds to
alpha-Caml's Shift
(Embed
t)outer t
.
untrec :: (Fresh m, Alpha p) => TRec p -> m pSource
Destructor for recursive abstractions which picks globally fresh names for the binders.
luntrec :: (LFresh m, Alpha p) => TRec p -> m pSource
Destructor for recursive abstractions which picks locally fresh
names for binders (see LFresh
).
Shift
Shift the scope of an embedded term one level outwards.
Shift p |
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
aeqBinders :: Alpha p => p -> p -> BoolSource
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 -> OrderingSource
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 AnyNameSource
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 AnyNameSource
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 AnyNameSource
Calculate the binding variables (of any sort) in a pattern.
Collections
class Foldable f => Collection f whereSource
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.
An empty collection. Must be the identity for union
.
Create a singleton collection.
union :: Ord a => f a -> f a -> f aSource
An associative combining operation. The Ord
constraint is in
order to accommodate sets.
cmap :: (Ord a, Ord b) => (a -> b) -> f a -> f bSource
Collections must be functorial. The normal Functor
class
won't do because of the Ord
constraint on sets.
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. |
A simple representation of multisets.
Foldable Multiset | |
Collection Multiset | Multisets are containers which preserve multiplicity but not ordering. |
Substitution
Capture-avoiding substitution.
class Rep1 (SubstD b) a => Subst b a whereSource
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
.
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 -> aSource
substitutes subst
nm sub tmsub
for nm
in tm
. It has
a default generic implementation in terms of isvar
.
substs :: [(Name b, b)] -> a -> aSource
Perform several simultaneous substitutions. This method also
has a default generic implementation in terms of isvar
.
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 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) | |
(Rep order, Rep card, Subst c b, Subst c a, Alpha a, Alpha b) => Subst c (GenBind order card a b) | |
(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) |
Permutations
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.
Working with permutations
compose :: Ord a => Perm a -> Perm a -> Perm aSource
Compose two permutations. The right-hand permutation will be applied first.
support :: Ord a => Perm a -> [a]Source
The support of a permutation is the set of elements which are not fixed.
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.
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
swapsEmbeds :: Alpha p => Perm AnyName -> p -> pSource
Apply a permutation to the embedded terms in a pattern. Binding names are left alone by the permutation.
swapsBinders :: Alpha p => Perm AnyName -> p -> pSource
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
The Fresh
class
class Monad m => Fresh m whereSource
The Fresh
type class governs monads which can generate new
globally unique Name
s based on a given Name
.
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) |
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.
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.
MonadTrans FreshMT | |
MonadError e m => MonadError e (FreshMT m) | |
MonadReader r m => MonadReader r (FreshMT m) | |
MonadState s m => MonadState s (FreshMT m) | |
MonadWriter w m => MonadWriter w (FreshMT m) | |
Monad m => Monad (FreshMT m) | |
Functor m => Functor (FreshMT m) | |
MonadFix m => MonadFix (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 aSource
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 bSource
"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 whereSource
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.
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 aSource
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.
LFresh m => LFresh (ListT m) | |
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) |
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 IdentitySource
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 -> aSource
Run a LFreshM computation in an empty context.
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.
MonadTrans LFreshMT | |
MonadError e m => MonadError e (LFreshMT m) | |
MonadReader r m => MonadReader r (LFreshMT m) | |
MonadState s m => MonadState s (LFreshMT m) | |
MonadWriter w m => MonadWriter w (LFreshMT m) | |
Monad m => Monad (LFreshMT m) | |
Functor m => Functor (LFreshMT m) | |
MonadFix m => MonadFix (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) |
runLFreshMT :: LFreshMT m a -> m aSource
Run an LFreshMT
computation in an empty context.
The Alpha
class
class (Show a, Rep1 AlphaD a) => Alpha a whereSource
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 Term
s
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.
swaps' :: AlphaCtx -> Perm AnyName -> a -> aSource
See swaps
.
fv' :: Collection f => AlphaCtx -> a -> f AnyNameSource
See fv
.
lfreshen' :: LFresh m => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m bSource
See lfreshen
.
freshen' :: Fresh m => AlphaCtx -> a -> m (a, Perm AnyName)Source
See freshen
.
aeq' :: AlphaCtx -> a -> a -> BoolSource
See aeq
.
acompare' :: AlphaCtx -> a -> a -> OrderingSource
See acompare
.
close :: Alpha b => AlphaCtx -> b -> a -> aSource
Replace free names by bound names.
open :: Alpha b => AlphaCtx -> b -> a -> aSource
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 x
dynamically checks whether x
can be used as a
valid term. The default instance returns True
if at all
possible.
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 -> NthContSource
looks up the nthpatrec
p nn
th name in the pattern p
(zero-indexed), returning the number of names encountered if not
found.
findpatrec :: a -> AnyName -> FindResultSource
Find the (first) index of the name in the pattern if one exists; otherwise, return the number of names encountered instead.
Alpha Bool | |
Alpha Char | |
Alpha Double | |
Alpha Float | |
Alpha Int | |
Alpha Integer | |
Alpha () | |
Alpha AnyName | |
Alpha a => Alpha [a] | |
Alpha a => Alpha (Maybe a) | |
Rep a => Alpha (R 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 a, Alpha b, Alpha c) => Alpha (a, b, c) | |
(Alpha a, Alpha b, Alpha c, Alpha d) => Alpha (a, b, c, d) | |
(Rep order, Rep card, Alpha p, Alpha t) => Alpha (GenBind order card p t) | |
(Alpha a, Alpha b, Alpha c, Alpha d, Alpha e) => Alpha (a, b, c, d, e) |
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.