unbound-generics-0.1: Reimplementation of Unbound using GHC Generics

MaintainerAleksey Kliger
Safe HaskellNone




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


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.

isTerm :: a -> BoolSource

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

isEmbed :: a -> BoolSource

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 nth 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 as. In addition to a monoidal structure, a disjoint set also has an annihilator inconsistentDisjointSet.

   inconsistentDisjointSet <> s == inconsistentDisjointSet
   s <> inconsistentDisjoinSet == inconsistentDisjointSet


DisjointSet (Maybe [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 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 IntegerSource

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 Source

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

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.

termCtx :: AlphaCtx -> AlphaCtxSource

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

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.


gaeq :: GAlpha f => AlphaCtx -> f a -> f a -> BoolSource

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

gclose :: (GAlpha f, Alpha b) => AlphaCtx -> b -> f a -> f aSource

gopen :: (GAlpha f, Alpha b) => AlphaCtx -> b -> f a -> f aSource

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

gisTerm :: GAlpha f => f a -> BoolSource

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

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

gswaps :: GAlpha f => AlphaCtx -> Perm AnyName -> f a -> f aSource

gfreshen :: (GAlpha f, Fresh m) => AlphaCtx -> f a -> m (f a, Perm AnyName)Source

glfreshen :: (GAlpha f, LFresh m) => AlphaCtx -> f a -> (f a -> Perm AnyName -> m b) -> m bSource

gacompare :: GAlpha f => AlphaCtx -> f a -> f a -> OrderingSource