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 > 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
Nameaware 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 alpharespecting 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
Interal helpers for gfreshen
retractFFM :: Monad m => FFM m a > m a Source