Portability  GHC only (XKitchenSink) 

Maintainer  Brent Yorgey <byorgey@cis.upenn.edu> 
 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
 class IsEmbed e where
 data FindResult
 findpat :: Alpha a => a > AnyName > Maybe Integer
 data NthResult
 newtype NthCont = NthCont {
 runNthCont :: Integer > NthResult
 nthName :: AnyName > NthCont
 nthpat :: Alpha a => a > Integer > AnyName
 data AlphaCtx = AC {}
 initial :: AlphaCtx
 incr :: AlphaCtx > AlphaCtx
 decr :: AlphaCtx > AlphaCtx
 pat :: AlphaCtx > AlphaCtx
 term :: AlphaCtx > AlphaCtx
 data Mode
 openT :: (Alpha p, Alpha t) => p > t > t
 openP :: (Alpha p1, Alpha p2) => p1 > p2 > p2
 closeT :: (Alpha p, Alpha t) => p > t > t
 closeP :: (Alpha p1, Alpha p2) => p1 > p2 > p2
 data AlphaD a = AlphaD {
 isPatD :: a > Maybe [AnyName]
 isTermD :: a > Bool
 isEmbedD :: a > Bool
 swapsD :: AlphaCtx > Perm AnyName > a > a
 fvD :: Collection f => AlphaCtx > a > f AnyName
 freshenD :: Fresh m => AlphaCtx > a > m (a, Perm AnyName)
 lfreshenD :: LFresh m => AlphaCtx > a > (a > Perm AnyName > m b) > m b
 aeqD :: AlphaCtx > a > a > Bool
 acompareD :: AlphaCtx > a > a > Ordering
 closeD :: Alpha b => AlphaCtx > b > a > a
 openD :: Alpha b => AlphaCtx > b > a > a
 findpatD :: a > AnyName > FindResult
 nthpatD :: a > NthCont
 closeR1 :: Alpha b => R1 AlphaD a > AlphaCtx > b > a > a
 openR1 :: Alpha b => R1 AlphaD a > AlphaCtx > b > a > a
 swapsR1 :: R1 AlphaD a > AlphaCtx > Perm AnyName > a > a
 fvR1 :: Collection f => R1 AlphaD a > AlphaCtx > a > f AnyName
 fv1 :: Collection f => MTup AlphaD l > AlphaCtx > l > f AnyName
 aeqR1 :: R1 AlphaD a > AlphaCtx > a > a > Bool
 aeq1 :: MTup AlphaD l > AlphaCtx > l > l > Bool
 freshenR1 :: Fresh m => R1 AlphaD a > AlphaCtx > a > m (a, Perm AnyName)
 freshenL :: Fresh m => MTup AlphaD l > AlphaCtx > l > m (l, Perm AnyName)
 lfreshenR1 :: LFresh m => R1 AlphaD a > AlphaCtx > a > (a > Perm AnyName > m b) > m b
 lfreshenL :: LFresh m => MTup AlphaD l > AlphaCtx > l > (l > Perm AnyName > m b) > m b
 findpatR1 :: R1 AlphaD b > b > AnyName > FindResult
 findpatL :: MTup AlphaD l > l > AnyName > FindResult
 nthpatR1 :: R1 AlphaD b > b > NthCont
 nthpatL :: MTup AlphaD l > l > NthCont
 combine :: Maybe [AnyName] > Maybe [AnyName] > Maybe [AnyName]
 isPatR1 :: R1 AlphaD b > b > Maybe [AnyName]
 isTermR1 :: R1 AlphaD b > b > Bool
 acompareR1 :: R1 AlphaD a > AlphaCtx > a > a > Ordering
 compareTupM :: MTup AlphaD l > AlphaCtx > l > l > Ordering
Documentation
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 alphaequivalence. 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
(zeroindexed), 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]  
Rep a => Alpha (R a)  
Alpha a => Alpha (Maybe a)  
Rep a => Alpha (Name a)  
Alpha a => Alpha (Shift a)  
Alpha t => Alpha (Embed t)  
Alpha p => Alpha (Rec p)  
(Alpha a, Alpha b) => Alpha (Either a b)  
(Alpha a, Alpha b) => Alpha (a, b)  
(Alpha p, Alpha q) => Alpha (Rebind p q)  
(Alpha 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) 
Type class for embedded terms (either Embed
or Shift
).
embed :: Embedded e > eSource
Construct an embedded term, which is an instance of Embed
with any number of enclosing Shift
s. 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 :: e > Embedded eSource
Destruct an embedded term. unembed
can have any of the types
Embed t > t
Shift (Embed t) > t
and so on.
data FindResult Source
The result of a findpatrec
operation.
Index Integer  The (first) index of the name we sought 
NamesSeen Integer  We haven't found the name (yet), but have seen this many others while looking for it 
Eq FindResult  
Ord FindResult  
Show FindResult  
Monoid FindResult 

findpat :: Alpha a => a > AnyName > Maybe IntegerSource
Find the (first) index of the name in the pattern, if it exists.
The result of an nthpatrec
operation.
A continuation which takes the remaining index and searches for that location in a pattern, yielding a name or a remaining index if the end of the pattern was reached too soon.
NthCont  

nthName :: AnyName > NthContSource
If we see a name, check whether the index is 0: if it is, we've found the name we're looking for, otherwise continue with a decremented index.
nthpat :: Alpha a => a > Integer > AnyNameSource
looks up up the nthpat
b nn
th name in the pattern b
(zeroindexed). PRECONDITION: the number of names in the pattern
must be at least n
.
A mode is basically a flag that tells us whether we should be
looking at the names in the term, or if we are in a pattern and
should only be looking at the names in the annotations. The
standard mode is to use Term
; many functions do this by default.
openP :: (Alpha p1, Alpha p2) => p1 > p2 > p2Source
openP p1 p2
opens the pattern p2
using the pattern p1
.
closeP :: (Alpha p1, Alpha p2) => p1 > p2 > p2Source
closeP p1 p2
closes the pattern p2
using the pattern p1
.
Class constraint hackery to allow us to override the default
definitions for certain classes. AlphaD
is essentially a
reified dictionary for the Alpha
class.
AlphaD  
