Copyright | (c) 2014, Aleksey Kliger |
---|---|
License | BSD3 (See LICENSE) |
Maintainer | Aleksey Kliger |
Stability | experimental |
Safe Haskell | None |
Language | Haskell2010 |
Extensions |
|
- 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)
- acompare' :: AlphaCtx -> a -> a -> Ordering
- newtype DisjointSet a = DisjointSet (Maybe [a])
- inconsistentDisjointSet :: DisjointSet a
- singletonDisjointSet :: a -> DisjointSet a
- isConsistentDisjointSet :: DisjointSet a -> Bool
- isNullDisjointSet :: 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
- decrLevelCtx :: AlphaCtx -> AlphaCtx
- isZeroLevelCtx :: AlphaCtx -> Bool
- gaeq :: GAlpha f => AlphaCtx -> f a -> f a -> Bool
- gfvAny :: (GAlpha f, Contravariant g, Applicative g) => AlphaCtx -> (AnyName -> g AnyName) -> f a -> g (f a)
- gclose :: (GAlpha f, Alpha b) => AlphaCtx -> b -> f a -> f a
- gopen :: (GAlpha f, Alpha b) => AlphaCtx -> b -> f a -> f a
- gisPat :: GAlpha f => f a -> DisjointSet AnyName
- gisTerm :: GAlpha f => f a -> Bool
- gnthPatFind :: GAlpha f => f a -> NthPatFind
- gnamePatFind :: GAlpha f => f a -> NamePatFind
- gswaps :: GAlpha f => AlphaCtx -> Perm AnyName -> f a -> f a
- gfreshen :: (GAlpha f, Fresh m) => AlphaCtx -> f a -> m (f a, Perm AnyName)
- glfreshen :: (GAlpha f, LFresh m) => AlphaCtx -> f a -> (f a -> Perm AnyName -> m b) -> m b
- gacompare :: GAlpha f => AlphaCtx -> f a -> f a -> Ordering
Name-aware opertions
class Show a => Alpha a where Source
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
.
Nothing
aeq' :: AlphaCtx -> a -> a -> Bool Source
See aeq
.
fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> a -> f a Source
See fvAny
.
fvAny' :: Fold a AnyName
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 -> DisjointSet AnyName Source
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 -> NthPatFind Source
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 -> NamePatFind Source
If a
is a pattern, find the index of the given name in the pattern.
swaps' :: AlphaCtx -> Perm AnyName -> a -> a Source
See swaps
. Apply
the given permutation of variable names to the given pattern.
lfreshen' :: LFresh m => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b Source
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
.
acompare' :: AlphaCtx -> a -> a -> Ordering Source
See acompare
. An alpha-respecting total order on terms involving binders.
Alpha Bool | |
Alpha Char | |
Alpha Double | |
Alpha Float | |
Alpha Int | |
Alpha Integer | |
Alpha () | |
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 e => Alpha (Shift e) | |
Alpha p => Alpha (TRec p) | |
Alpha p => Alpha (Rec p) | |
(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 a Source
Returns a DisjointSet a
that is the annihilator element for the Monoid
instance of DisjointSet
.
singletonDisjointSet :: a -> DisjointSet a Source
singletonDisjointSet x
a DisjointSet a
that contains the single element x
isConsistentDisjointSet :: DisjointSet a -> Bool Source
isConsistentDisjointSet
returns True
iff the given disjoint set is not inconsistent.
isNullDisjointSet :: DisjointSet a -> Bool Source
isNullDisjointSet
return True
iff the given disjoint set is mempty
.
Implementation details
type NthPatFind = Integer -> Either Integer AnyName Source
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 Integer Source
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 -> AlphaCtx Source
Switches to a context where we expect to operate on patterns.
isTermCtx :: AlphaCtx -> Bool Source
Returns True
iff we are in a context where we expect to see terms.
incrLevelCtx :: AlphaCtx -> AlphaCtx Source
Increment the number of binders that we are operating under.
decrLevelCtx :: AlphaCtx -> AlphaCtx Source
Decrement the number of binders that we are operating under.
isZeroLevelCtx :: AlphaCtx -> Bool Source
Are we operating under no binders?
Internal
gfvAny :: (GAlpha f, Contravariant g, Applicative g) => AlphaCtx -> (AnyName -> g AnyName) -> f a -> g (f a) Source
gisPat :: GAlpha f => f a -> DisjointSet AnyName Source
gnthPatFind :: GAlpha f => f a -> NthPatFind Source
gnamePatFind :: GAlpha f => f a -> NamePatFind Source