| License | BSD-like (see LICENSE) |
|---|---|
| Maintainer | Stephanie Weirich <sweirich@cis.upenn.edu> |
| Portability | GHC only (-XKitchenSink) |
| Safe Haskell | None |
| Language | Haskell2010 |
Unbound.LocallyNameless.Alpha
Description
- class Rep1 AlphaD a => Alpha a where
- 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 :: forall f. Collection f => AlphaCtx -> a -> f AnyName
- freshenD :: forall m. Fresh m => AlphaCtx -> a -> m (a, Perm AnyName)
- lfreshenD :: forall m b. LFresh m => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b
- aeqD :: AlphaCtx -> a -> a -> Bool
- acompareD :: AlphaCtx -> a -> a -> Ordering
- closeD :: forall b. Alpha b => AlphaCtx -> b -> a -> a
- openD :: forall b. 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
- 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 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 Termwhere 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 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 -> NthCont Source #
nthpatrec p nnth 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 # | |
| Alpha AnyName Source # | |
| Alpha a => Alpha [a] Source # | |
| Alpha a => Alpha (Maybe a) Source # | |
| Rep a => Alpha (R a) Source # | |
| Rep a => Alpha (Name a) Source # | |
| Alpha a => Alpha (Shift a) Source # | |
| Alpha t => Alpha (Embed t) Source # | |
| Alpha p => Alpha (Rec p) Source # | |
| (Alpha a, Alpha b) => Alpha (Either a b) Source # | |
| (Alpha a, Alpha b) => Alpha (a, b) Source # | |
| (Alpha p, Alpha q) => Alpha (Rebind p q) Source # | |
| (Alpha a, Alpha b, Alpha c) => Alpha (a, b, c) Source # | |
| (Alpha a, Alpha b, Alpha c, Alpha d) => Alpha (a, b, c, d) Source # | |
| (Rep order, Rep card, Alpha p, Alpha t) => Alpha (GenBind order card p t) Source # | |
| (Alpha a, Alpha b, Alpha c, Alpha d, Alpha e) => Alpha (a, b, c, d, e) Source # | |
class IsEmbed e where Source #
Type class for embedded terms (either Embed or Shift).
Methods
embed :: 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 :: 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.
data FindResult Source #
The result of a findpatrec operation.
Constructors
| 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 |
Instances
| Eq FindResult Source # | |
| Ord FindResult Source # | |
| Monoid FindResult Source # |
|
findpat :: Alpha a => a -> AnyName -> Maybe Integer Source #
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.
Constructors
| NthCont | |
Fields
| |
nthName :: AnyName -> NthCont Source #
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 -> AnyName Source #
nthpat b nnth 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 -> p2 Source #
openP p1 p2 opens the pattern p2 using the pattern p1.
closeP :: (Alpha p1, Alpha p2) => p1 -> p2 -> p2 Source #
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.
Constructors
| AlphaD | |
Fields
| |
freshenR1 :: Fresh m => R1 AlphaD a -> AlphaCtx -> a -> m (a, Perm AnyName) Source #
Generic version of freshen
freshenL :: Fresh m => MTup AlphaD l -> AlphaCtx -> l -> m (l, Perm AnyName) Source #
Generic list version of freshen
lfreshenR1 :: LFresh m => R1 AlphaD a -> AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b Source #