Copyright | (c) 2014 Aleksey Kliger |
---|---|
License | BSD3 (See LICENSE) |
Maintainer | Aleksey Kliger |
Stability | experimental |
Safe Haskell | None |
Language | Haskell2010 |
Extensions |
|
Unbound.Generics.LocallyNameless.Alpha
Contents
- class Show a => Alpha a where
- newtype DisjointSet a = DisjointSet (Maybe [a])
- inconsistentDisjointSet :: DisjointSet a
- singletonDisjointSet :: a -> DisjointSet a
- isConsistentDisjointSet :: DisjointSet a -> Bool
- isNullDisjointSet :: DisjointSet a -> Bool
- newtype NthPatFind = NthPatFind {
- runNthPatFind :: Integer -> Either Integer AnyName
- newtype NamePatFind = NamePatFind {}
- 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 => AlphaCtx -> NamePatFind -> f a -> f a
- gopen :: GAlpha f => AlphaCtx -> NthPatFind -> f a -> f a
- gisPat :: GAlpha f => f a -> DisjointSet AnyName
- gisTerm :: GAlpha f => f a -> All
- 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 -> FFM 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
- data FFM f a
- liftFFM :: Monad m => m a -> FFM m a
- retractFFM :: Monad m => FFM m a -> m a
Name-aware opertions
class Show a => Alpha a where #
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
.
Methods
aeq' :: AlphaCtx -> a -> a -> Bool #
See aeq
.
aeq' :: (Generic a, GAlpha (Rep a)) => AlphaCtx -> a -> a -> Bool #
See aeq
.
fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> a -> f a #
See fvAny
.
fvAny' :: Fold a AnyName
fvAny' :: (Generic a, GAlpha (Rep a), Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> a -> f a #
See fvAny
.
fvAny' :: Fold a AnyName
close :: AlphaCtx -> NamePatFind -> a -> a #
Replace free names by bound names.
close :: (Generic a, GAlpha (Rep a)) => AlphaCtx -> NamePatFind -> a -> a #
Replace free names by bound names.
open :: AlphaCtx -> NthPatFind -> a -> a #
Replace bound names by free names.
open :: (Generic a, GAlpha (Rep a)) => AlphaCtx -> NthPatFind -> a -> a #
Replace bound names by free names.
isPat :: a -> DisjointSet AnyName #
isPat x
dynamically checks whether x
can be used as a valid pattern.
isPat :: (Generic a, GAlpha (Rep a)) => a -> DisjointSet AnyName #
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.
isTerm :: (Generic a, GAlpha (Rep a)) => a -> All #
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 #
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.
nthPatFind :: (Generic a, GAlpha (Rep a)) => a -> NthPatFind #
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 #
If a
is a pattern, find the index of the given name in the pattern.
namePatFind :: (Generic a, GAlpha (Rep a)) => a -> NamePatFind #
If a
is a pattern, find the index of the given name in the pattern.
swaps' :: AlphaCtx -> Perm AnyName -> a -> a #
See swaps
. Apply
the given permutation of variable names to the given pattern.
swaps' :: (Generic a, GAlpha (Rep a)) => AlphaCtx -> Perm AnyName -> a -> a #
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 #
See freshen
.
lfreshen' :: (LFresh m, Generic a, GAlpha (Rep a)) => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b #
See freshen
.
freshen' :: Fresh m => AlphaCtx -> a -> m (a, Perm AnyName) #
See freshen
. Rename the free variables
in the given term to be distinct from all other names seen in the monad m
.
freshen' :: (Generic a, GAlpha (Rep a), Fresh m) => AlphaCtx -> a -> m (a, Perm AnyName) #
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 #
See acompare
. An alpha-respecting total order on terms involving binders.
acompare' :: (Generic a, GAlpha (Rep a)) => AlphaCtx -> a -> a -> Ordering #
See acompare
. An alpha-respecting total order on terms involving binders.
Instances
Alpha Bool # | |
Alpha Char # | |
Alpha Double # | |
Alpha Float # | |
Alpha Int # | |
Alpha Integer # | |
Alpha () # | |
Alpha AnyName # | |
Alpha a => Alpha [a] # | |
Alpha a => Alpha (Maybe a) # | |
(Integral n, Alpha n) => Alpha (Ratio n) # | |
Typeable * a => Alpha (Name a) # | |
Alpha t => Alpha (Embed t) # | |
Alpha p => Alpha (TRec p) # | |
Alpha p => Alpha (Rec p) # | |
Alpha e => Alpha (Shift e) # | |
(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 #
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
Constructors
DisjointSet (Maybe [a]) |
Instances
Foldable DisjointSet # | |
Eq a => Monoid (DisjointSet a) # | |
inconsistentDisjointSet :: DisjointSet a #
Returns a DisjointSet a
that is the annihilator element for the Monoid
instance of DisjointSet
.
singletonDisjointSet :: a -> DisjointSet a #
singletonDisjointSet x
a DisjointSet a
that contains the single element x
isConsistentDisjointSet :: DisjointSet a -> Bool #
isConsistentDisjointSet
returns True
iff the given disjoint set is not inconsistent.
isNullDisjointSet :: DisjointSet a -> Bool #
isNullDisjointSet
return True
iff the given disjoint set is mempty
.
Implementation details
newtype NthPatFind #
The result of
is nthPatFind
a iLeft k
where i-k
is the
number of names in pattern a
(with k < i
) or Right x
where x
is the i
th name in a
Constructors
NthPatFind | |
Fields
|
Instances
newtype NamePatFind #
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
Constructors
NamePatFind | |
Fields |
Instances
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.
initialCtx :: AlphaCtx #
The starting context for alpha operations: we are expecting to work on terms and we are under no binders.
patternCtx :: AlphaCtx -> AlphaCtx #
Switches to a context where we expect to operate on patterns.
incrLevelCtx :: AlphaCtx -> AlphaCtx #
Increment the number of binders that we are operating under.
decrLevelCtx :: AlphaCtx -> AlphaCtx #
Decrement the number of binders that we are operating under.
isZeroLevelCtx :: AlphaCtx -> Bool #
Are we operating under no binders?
Internal
gfvAny :: (GAlpha f, Contravariant g, Applicative g) => AlphaCtx -> (AnyName -> g AnyName) -> f a -> g (f a) #
gclose :: GAlpha f => AlphaCtx -> NamePatFind -> f a -> f a #
gopen :: GAlpha f => AlphaCtx -> NthPatFind -> f a -> f a #
gisPat :: GAlpha f => f a -> DisjointSet AnyName #
gnthPatFind :: GAlpha f => f a -> NthPatFind #
gnamePatFind :: GAlpha f => f a -> NamePatFind #
Interal helpers for gfreshen
retractFFM :: Monad m => FFM m a -> m a #