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)
- acompare' :: AlphaCtx -> a -> a -> Ordering

- 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
- 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 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

See `fvAny`

.

fvAny' :: Fold a AnyName

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`

.

acompare' :: AlphaCtx -> a -> a -> OrderingSource

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 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 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 i`Left 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 x`Left 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.

# Internal

gfvAny :: (GAlpha f, Contravariant g, Applicative g) => AlphaCtx -> (AnyName -> g AnyName) -> f a -> g (f a)Source

gisPat :: GAlpha f => f a -> DisjointSet AnyNameSource

gnthPatFind :: GAlpha f => f a -> NthPatFindSource

gnamePatFind :: GAlpha f => f a -> NamePatFindSource