Unbound.Generics.LocallyNameless.Alpha

Use the Alpha typeclass to mark types that may contain Names.

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.

Minimal complete definition

Nothing

Methods

aeq' :: AlphaCtx -> a -> a -> Bool

See aeq.

fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> a -> f a

See fvAny.

 fvAny' :: Fold a AnyName

close :: Alpha b => AlphaCtx -> b -> a -> a

Replace free names by bound names.

open :: Alpha b => AlphaCtx -> b -> 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.

isTerm :: a -> Bool

isPat x dynamically checks whether x can be used as a valid term.

isEmbed :: a -> Bool

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

swaps' :: 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.

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.

acompare' :: 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]

(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

A DisjointSet a is a Just a list of distinct as. 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

type NthPatFind = Integer -> Either Integer AnyName

The result of nthPatFind a i is Left k where k is the number of names in pattern a with k < i or Right x where x is the ith name in a

type NamePatFind = AnyName -> Either Integer Integer

The result of namePatFind a x is either Left i if a is a pattern that contains i free names none of which are x, or Right j if x is the jth name in a

data AlphaCtx

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.

termCtx :: AlphaCtx -> AlphaCtx

Switches to a context where we expect to operate on terms.

isTermCtx :: AlphaCtx -> Bool

Returns True iff we are in a context where we expect to see terms.

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

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

Interal helpers for gfreshen

data FFM f a

Instances

Monad (FFM f)

Functor (FFM f)

Applicative (FFM f)

Fresh m => Fresh (FFM m)

liftFFM :: Monad m => m a -> FFM m a

retractFFM :: Monad m => FFM m a -> m a