unbound-generics-0.3.1: Support for programming with names and binders using GHC Generics

Copyright(c) 2014 Aleksey Kliger
LicenseBSD3 (See LICENSE)
MaintainerAleksey Kliger
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010
Extensions
  • DefaultSignatures
  • FlexibleContexts
  • RankNTypes
  • TypeOperators
  • ExplicitNamespaces
  • ExplicitForAll

Unbound.Generics.LocallyNameless.Alpha

Contents

Description

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

Synopsis

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.

isTerm :: a -> All #

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

nthPatFind :: (Generic a, GAlpha (Rep a)) => 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.

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 () # 

Methods

aeq' :: AlphaCtx -> () -> () -> Bool #

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

close :: AlphaCtx -> NamePatFind -> () -> () #

open :: AlphaCtx -> NthPatFind -> () -> () #

isPat :: () -> DisjointSet AnyName #

isTerm :: () -> All #

isEmbed :: () -> Bool #

nthPatFind :: () -> NthPatFind #

namePatFind :: () -> NamePatFind #

swaps' :: AlphaCtx -> Perm AnyName -> () -> () #

lfreshen' :: LFresh m => AlphaCtx -> () -> (() -> Perm AnyName -> m b) -> m b #

freshen' :: Fresh m => AlphaCtx -> () -> m ((), Perm AnyName) #

acompare' :: AlphaCtx -> () -> () -> Ordering #

Alpha AnyName # 
Alpha a => Alpha [a] # 

Methods

aeq' :: AlphaCtx -> [a] -> [a] -> Bool #

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

close :: AlphaCtx -> NamePatFind -> [a] -> [a] #

open :: AlphaCtx -> NthPatFind -> [a] -> [a] #

isPat :: [a] -> DisjointSet AnyName #

isTerm :: [a] -> All #

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 #

Alpha a => Alpha (Maybe a) # 
(Integral n, Alpha n) => Alpha (Ratio n) # 
Typeable * a => Alpha (Name a) # 

Methods

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

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

close :: AlphaCtx -> NamePatFind -> Name a -> Name a #

open :: AlphaCtx -> NthPatFind -> Name a -> Name a #

isPat :: Name a -> DisjointSet AnyName #

isTerm :: Name a -> All #

isEmbed :: Name a -> Bool #

nthPatFind :: Name a -> NthPatFind #

namePatFind :: Name a -> NamePatFind #

swaps' :: AlphaCtx -> Perm AnyName -> Name a -> Name a #

lfreshen' :: LFresh m => AlphaCtx -> Name a -> (Name a -> Perm AnyName -> m b) -> m b #

freshen' :: Fresh m => AlphaCtx -> Name a -> m (Name a, Perm AnyName) #

acompare' :: AlphaCtx -> Name a -> Name a -> Ordering #

Alpha t => Alpha (Embed t) # 
Alpha p => Alpha (TRec p) # 

Methods

aeq' :: AlphaCtx -> TRec p -> TRec p -> Bool #

fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> TRec p -> f (TRec p) #

close :: AlphaCtx -> NamePatFind -> TRec p -> TRec p #

open :: AlphaCtx -> NthPatFind -> TRec p -> TRec p #

isPat :: TRec p -> DisjointSet AnyName #

isTerm :: TRec p -> All #

isEmbed :: TRec p -> Bool #

nthPatFind :: TRec p -> NthPatFind #

namePatFind :: TRec p -> NamePatFind #

swaps' :: AlphaCtx -> Perm AnyName -> TRec p -> TRec p #

lfreshen' :: LFresh m => AlphaCtx -> TRec p -> (TRec p -> Perm AnyName -> m b) -> m b #

freshen' :: Fresh m => AlphaCtx -> TRec p -> m (TRec p, Perm AnyName) #

acompare' :: AlphaCtx -> TRec p -> TRec p -> Ordering #

Alpha p => Alpha (Rec p) # 

Methods

aeq' :: AlphaCtx -> Rec p -> Rec p -> Bool #

fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Rec p -> f (Rec p) #

close :: AlphaCtx -> NamePatFind -> Rec p -> Rec p #

open :: AlphaCtx -> NthPatFind -> Rec p -> Rec p #

isPat :: Rec p -> DisjointSet AnyName #

isTerm :: Rec p -> All #

isEmbed :: Rec p -> Bool #

nthPatFind :: Rec p -> NthPatFind #

namePatFind :: Rec p -> NamePatFind #

swaps' :: AlphaCtx -> Perm AnyName -> Rec p -> Rec p #

lfreshen' :: LFresh m => AlphaCtx -> Rec p -> (Rec p -> Perm AnyName -> m b) -> m b #

freshen' :: Fresh m => AlphaCtx -> Rec p -> m (Rec p, Perm AnyName) #

acompare' :: AlphaCtx -> Rec p -> Rec p -> Ordering #

Alpha e => Alpha (Shift e) # 
(Alpha a, Alpha b) => Alpha (Either a b) # 

Methods

aeq' :: AlphaCtx -> Either a b -> Either a b -> Bool #

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

close :: AlphaCtx -> NamePatFind -> Either a b -> Either a b #

open :: AlphaCtx -> NthPatFind -> Either a b -> Either a b #

isPat :: Either a b -> DisjointSet AnyName #

isTerm :: Either a b -> All #

isEmbed :: Either a b -> Bool #

nthPatFind :: Either a b -> NthPatFind #

namePatFind :: Either a b -> NamePatFind #

swaps' :: AlphaCtx -> Perm AnyName -> Either a b -> Either a b #

lfreshen' :: LFresh m => AlphaCtx -> Either a b -> (Either a b -> Perm AnyName -> m b) -> m b #

freshen' :: Fresh m => AlphaCtx -> Either a b -> m (Either a b, Perm AnyName) #

acompare' :: AlphaCtx -> Either a b -> Either a b -> Ordering #

(Alpha a, Alpha b) => Alpha (a, b) # 

Methods

aeq' :: AlphaCtx -> (a, b) -> (a, b) -> Bool #

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

close :: AlphaCtx -> NamePatFind -> (a, b) -> (a, b) #

open :: AlphaCtx -> NthPatFind -> (a, b) -> (a, b) #

isPat :: (a, b) -> DisjointSet AnyName #

isTerm :: (a, b) -> All #

isEmbed :: (a, b) -> Bool #

nthPatFind :: (a, b) -> NthPatFind #

namePatFind :: (a, b) -> NamePatFind #

swaps' :: AlphaCtx -> Perm AnyName -> (a, b) -> (a, b) #

lfreshen' :: LFresh m => AlphaCtx -> (a, b) -> ((a, b) -> Perm AnyName -> m b) -> m b #

freshen' :: Fresh m => AlphaCtx -> (a, b) -> m ((a, b), Perm AnyName) #

acompare' :: AlphaCtx -> (a, b) -> (a, b) -> Ordering #

(Alpha p, Alpha t) => Alpha (Bind p t) # 

Methods

aeq' :: AlphaCtx -> Bind p t -> Bind p t -> Bool #

fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Bind p t -> f (Bind p t) #

close :: AlphaCtx -> NamePatFind -> Bind p t -> Bind p t #

open :: AlphaCtx -> NthPatFind -> Bind p t -> Bind p t #

isPat :: Bind p t -> DisjointSet AnyName #

isTerm :: Bind p t -> All #

isEmbed :: Bind p t -> Bool #

nthPatFind :: Bind p t -> NthPatFind #

namePatFind :: Bind p t -> NamePatFind #

swaps' :: AlphaCtx -> Perm AnyName -> Bind p t -> Bind p t #

lfreshen' :: LFresh m => AlphaCtx -> Bind p t -> (Bind p t -> Perm AnyName -> m b) -> m b #

freshen' :: Fresh m => AlphaCtx -> Bind p t -> m (Bind p t, Perm AnyName) #

acompare' :: AlphaCtx -> Bind p t -> Bind p t -> Ordering #

(Alpha p1, Alpha p2) => Alpha (Rebind p1 p2) # 

Methods

aeq' :: AlphaCtx -> Rebind p1 p2 -> Rebind p1 p2 -> Bool #

fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Rebind p1 p2 -> f (Rebind p1 p2) #

close :: AlphaCtx -> NamePatFind -> Rebind p1 p2 -> Rebind p1 p2 #

open :: AlphaCtx -> NthPatFind -> Rebind p1 p2 -> Rebind p1 p2 #

isPat :: Rebind p1 p2 -> DisjointSet AnyName #

isTerm :: Rebind p1 p2 -> All #

isEmbed :: Rebind p1 p2 -> Bool #

nthPatFind :: Rebind p1 p2 -> NthPatFind #

namePatFind :: Rebind p1 p2 -> NamePatFind #

swaps' :: AlphaCtx -> Perm AnyName -> Rebind p1 p2 -> Rebind p1 p2 #

lfreshen' :: LFresh m => AlphaCtx -> Rebind p1 p2 -> (Rebind p1 p2 -> Perm AnyName -> m b) -> m b #

freshen' :: Fresh m => AlphaCtx -> Rebind p1 p2 -> m (Rebind p1 p2, Perm AnyName) #

acompare' :: AlphaCtx -> Rebind p1 p2 -> Rebind p1 p2 -> Ordering #

(Alpha a, Alpha b, Alpha c) => Alpha (a, b, c) # 

Methods

aeq' :: AlphaCtx -> (a, b, c) -> (a, b, c) -> Bool #

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

close :: AlphaCtx -> NamePatFind -> (a, b, c) -> (a, b, c) #

open :: AlphaCtx -> NthPatFind -> (a, b, c) -> (a, b, c) #

isPat :: (a, b, c) -> DisjointSet AnyName #

isTerm :: (a, b, c) -> All #

isEmbed :: (a, b, c) -> Bool #

nthPatFind :: (a, b, c) -> NthPatFind #

namePatFind :: (a, b, c) -> NamePatFind #

swaps' :: AlphaCtx -> Perm AnyName -> (a, b, c) -> (a, b, c) #

lfreshen' :: LFresh m => AlphaCtx -> (a, b, c) -> ((a, b, c) -> Perm AnyName -> m b) -> m b #

freshen' :: Fresh m => AlphaCtx -> (a, b, c) -> m ((a, b, c), Perm AnyName) #

acompare' :: AlphaCtx -> (a, b, c) -> (a, b, c) -> Ordering #

(Alpha a, Alpha b, Alpha c, Alpha d) => Alpha (a, b, c, d) # 

Methods

aeq' :: AlphaCtx -> (a, b, c, d) -> (a, b, c, d) -> Bool #

fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> (a, b, c, d) -> f (a, b, c, d) #

close :: AlphaCtx -> NamePatFind -> (a, b, c, d) -> (a, b, c, d) #

open :: AlphaCtx -> NthPatFind -> (a, b, c, d) -> (a, b, c, d) #

isPat :: (a, b, c, d) -> DisjointSet AnyName #

isTerm :: (a, b, c, d) -> All #

isEmbed :: (a, b, c, d) -> Bool #

nthPatFind :: (a, b, c, d) -> NthPatFind #

namePatFind :: (a, b, c, d) -> NamePatFind #

swaps' :: AlphaCtx -> Perm AnyName -> (a, b, c, d) -> (a, b, c, d) #

lfreshen' :: LFresh m => AlphaCtx -> (a, b, c, d) -> ((a, b, c, d) -> Perm AnyName -> m b) -> m b #

freshen' :: Fresh m => AlphaCtx -> (a, b, c, d) -> m ((a, b, c, d), Perm AnyName) #

acompare' :: AlphaCtx -> (a, b, c, d) -> (a, b, c, d) -> Ordering #

(Alpha a, Alpha b, Alpha c, Alpha d, Alpha e) => Alpha (a, b, c, d, e) # 

Methods

aeq' :: AlphaCtx -> (a, b, c, d, e) -> (a, b, c, d, e) -> Bool #

fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> (a, b, c, d, e) -> f (a, b, c, d, e) #

close :: AlphaCtx -> NamePatFind -> (a, b, c, d, e) -> (a, b, c, d, e) #

open :: AlphaCtx -> NthPatFind -> (a, b, c, d, e) -> (a, b, c, d, e) #

isPat :: (a, b, c, d, e) -> DisjointSet AnyName #

isTerm :: (a, b, c, d, e) -> All #

isEmbed :: (a, b, c, d, e) -> Bool #

nthPatFind :: (a, b, c, d, e) -> NthPatFind #

namePatFind :: (a, b, c, d, e) -> NamePatFind #

swaps' :: AlphaCtx -> Perm AnyName -> (a, b, c, d, e) -> (a, b, c, d, e) #

lfreshen' :: LFresh m => AlphaCtx -> (a, b, c, d, e) -> ((a, b, c, d, e) -> Perm AnyName -> m b) -> m b #

freshen' :: Fresh m => AlphaCtx -> (a, b, c, d, e) -> m ((a, b, c, d, e), Perm AnyName) #

acompare' :: AlphaCtx -> (a, b, c, d, e) -> (a, b, c, d, e) -> Ordering #

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 # 

Methods

fold :: Monoid m => DisjointSet m -> m #

foldMap :: Monoid m => (a -> m) -> DisjointSet a -> m #

foldr :: (a -> b -> b) -> b -> DisjointSet a -> b #

foldr' :: (a -> b -> b) -> b -> DisjointSet a -> b #

foldl :: (b -> a -> b) -> b -> DisjointSet a -> b #

foldl' :: (b -> a -> b) -> b -> DisjointSet a -> b #

foldr1 :: (a -> a -> a) -> DisjointSet a -> a #

foldl1 :: (a -> a -> a) -> DisjointSet a -> a #

toList :: DisjointSet a -> [a] #

null :: DisjointSet a -> Bool #

length :: DisjointSet a -> Int #

elem :: Eq a => a -> DisjointSet a -> Bool #

maximum :: Ord a => DisjointSet a -> a #

minimum :: Ord a => DisjointSet a -> a #

sum :: Num a => DisjointSet a -> a #

product :: Num a => DisjointSet a -> a #

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 nthPatFind a i is Left k where i-k is the number of names in pattern a (with k < i) or Right x where x is the ith name in a

newtype NamePatFind #

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

Interal helpers for gfreshen

data FFM f a #

Instances

Monad (FFM f) # 

Methods

(>>=) :: FFM f a -> (a -> FFM f b) -> FFM f b #

(>>) :: FFM f a -> FFM f b -> FFM f b #

return :: a -> FFM f a #

fail :: String -> FFM f a #

Functor (FFM f) # 

Methods

fmap :: (a -> b) -> FFM f a -> FFM f b #

(<$) :: a -> FFM f b -> FFM f a #

Applicative (FFM f) # 

Methods

pure :: a -> FFM f a #

(<*>) :: FFM f (a -> b) -> FFM f a -> FFM f b #

(*>) :: FFM f a -> FFM f b -> FFM f b #

(<*) :: FFM f a -> FFM f b -> FFM f a #

Fresh m => Fresh (FFM m) # 

Methods

fresh :: Name a -> FFM m (Name a) #

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

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