- 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
- close :: Alpha b => AlphaCtx -> b -> a -> a
- open :: Alpha b => AlphaCtx -> b -> a -> a
- acompare' :: AlphaCtx -> a -> a -> Ordering
- isPat :: a -> Maybe [AnyName]
- isTerm :: a -> Bool
- isEmbed :: a -> Bool
- nthpatrec :: a -> NthCont
- findpatrec :: a -> AnyName -> FindResult
- 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
- closeD :: Alpha b => AlphaCtx -> b -> a -> a
- openD :: Alpha b => AlphaCtx -> b -> a -> a
- findpatD :: a -> AnyName -> FindResult
- nthpatD :: a -> NthCont
- acompareD :: AlphaCtx -> a -> a -> Ordering
- 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
- lexord :: Ordering -> Ordering -> 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 never be called directly!
Instead, use other methods provided by this module which are
defined in terms of Alpha
methods. (The only reason they are
exported is to make them available to automatically-generated
code.)
Most of the time, the default definitions of these methods will suffice, so you can make an instance for your data type by simply declaring
instance Alpha MyType
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
.
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.
acompare' :: AlphaCtx -> a -> a -> OrderingSource
See acompare
.
isPat :: a -> Maybe [AnyName]Source
isPat x
dynamically checks whether x
can be used as a valid
pattern. The default instance returns True
if at all
possible.
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] | |
Rep a => Alpha (R a) | |
Alpha a => Alpha (Maybe a) | |
Rep a => Alpha (Name a) | |
Alpha a => Alpha (Shift a) | |
Alpha t => Alpha (Embed t) | |
Alpha p => Alpha (Rec p) | |
(Alpha a, Alpha b) => Alpha (Either a b) | |
(Alpha a, Alpha b) => Alpha (a, b) | |
(Alpha p, Alpha q) => Alpha (Rebind p q) | |
(Alpha p, Alpha t) => Alpha (Bind p t) | |
(Alpha a, Alpha b, Alpha c) => Alpha (a, b, c) | |
(Alpha a, Alpha b, Alpha c, Alpha d) => Alpha (a, b, c, d) | |
(Alpha a, Alpha b, Alpha c, Alpha d, Alpha e) => Alpha (a, b, c, d, e) |
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
(zero-indexed). 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 | |
|