Stability | experimental |
---|---|
Maintainer | Aleksey Kliger |
Safe Haskell | None |
- class Show a => Alpha a where
- aeq' :: AlphaCtx -> a -> a -> Bool
- fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> a -> f a
- close :: Alpha b => AlphaCtx -> b -> a -> a
- open :: Alpha b => AlphaCtx -> b -> a -> a
- isPat :: a -> DisjointSet AnyName
- isTerm :: a -> Bool
- isEmbed :: a -> Bool
- nthPatFind :: a -> NthPatFind
- namePatFind :: a -> NamePatFind
- swaps' :: AlphaCtx -> Perm AnyName -> a -> a
- lfreshen' :: LFresh m => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b
- freshen' :: Fresh m => AlphaCtx -> a -> m (a, Perm AnyName)
- newtype DisjointSet a = DisjointSet (Maybe [a])
- inconsistentDisjointSet :: DisjointSet a
- singletonDisjointSet :: a -> DisjointSet a
- isConsistentDisjointSet :: DisjointSet a -> Bool
- type NthPatFind = Integer -> Either Integer AnyName
- type NamePatFind = AnyName -> Either Integer Integer
- data AlphaCtx
- initialCtx :: AlphaCtx
- patternCtx :: AlphaCtx -> AlphaCtx
- termCtx :: AlphaCtx -> AlphaCtx
- isTermCtx :: AlphaCtx -> Bool
- incrLevelCtx :: AlphaCtx -> AlphaCtx
Name-aware opertions
class Show a => Alpha a whereSource
Types that are instances of Alpha
may participate in name representation.
Minimal instance is entirely empty, provided that your type is an instance of
Generic
.
aeq' :: AlphaCtx -> a -> a -> BoolSource
See aeq
.
fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> a -> f aSource
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 -> DisjointSet AnyNameSource
isPat x
dynamically checks whether x
can be used as a valid pattern.
isPat x
dynamically checks whether x
can be used as a valid term.
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
.
nthPatFind :: a -> NthPatFindSource
If a
is a pattern, finds the n
th name in the pattern
(starting from zero), returning the number of names encountered
if not found.
namePatFind :: a -> NamePatFindSource
If a
is a pattern, find the index of the given name in the pattern.
swaps' :: AlphaCtx -> Perm AnyName -> a -> aSource
See swaps
. Apply
the given permutation of variable names to the given pattern.
lfreshen' :: LFresh m => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m bSource
See freshen
.
freshen' :: Fresh m => AlphaCtx -> a -> m (a, Perm AnyName)Source
See freshen
. Rename the free variables
in the given term to be distinct from all other names seen in the monad m
.
Alpha Bool | |
Alpha Char | |
Alpha Double | |
Alpha Float | |
Alpha Int | |
Alpha Integer | |
Alpha AnyName | |
Alpha a => Alpha [a] | |
(Integral n, Alpha n) => Alpha (Ratio n) | |
Alpha a => Alpha (Maybe a) | |
Typeable a => Alpha (Name a) | |
Alpha t => Alpha (Embed t) | |
(Alpha a, Alpha b) => Alpha (Either a b) | |
(Alpha a, Alpha b) => Alpha (a, b) | |
(Alpha p, Alpha t) => Alpha (Bind p t) | |
(Alpha p1, Alpha p2) => Alpha (Rebind p1 p2) | |
(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) |
Binder variables
newtype DisjointSet a Source
A DisjointSet a
is a Just
a list of distinct a
s. In addition to a monoidal
structure, a disjoint set also has an annihilator inconsistentDisjointSet
.
inconsistentDisjointSet <> s == inconsistentDisjointSet s <> inconsistentDisjoinSet == inconsistentDisjointSet
DisjointSet (Maybe [a]) |
Foldable DisjointSet | |
Eq a => Monoid (DisjointSet a) |
inconsistentDisjointSet :: DisjointSet aSource
Returns a DisjointSet a
that is the annihilator element for the Monoid
instance of DisjointSet
.
singletonDisjointSet :: a -> DisjointSet aSource
singletonDisjointSet x
a DisjointSet a
that contains the single element x
isConsistentDisjointSet :: DisjointSet a -> BoolSource
isConsistentDisjointSet
returns True
iff the given disjoint set is not inconsistent.
Implementation details
type NthPatFind = Integer -> Either Integer AnyNameSource
The result of
is nthPatFind
a iLeft k
where k
is the
number of names in pattern a
with k < i
or Right x
where x
is the i
th name in a
type NamePatFind = AnyName -> Either Integer IntegerSource
The result of
is either namePatFind
a xLeft i
if a
is a pattern that
contains i
free names none of which are x
, or Right j
if x
is the j
th name
in a
Some Alpha
operations need to record information about their
progress. Instances should just pass it through unchanged.
The context records whether we are currently operating on terms or patterns, and how many binding levels we've descended.
The starting context for alpha operations: we are expecting to work on terms and we are under no binders.
patternCtx :: AlphaCtx -> AlphaCtxSource
Switches to a context where we expect to operate on patterns.
isTermCtx :: AlphaCtx -> BoolSource
Returns True
iff we are in a context where we expect to see terms.
incrLevelCtx :: AlphaCtx -> AlphaCtxSource
Increment the number of binders that we are operating under.