unbound-generics-0.4.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 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.

Minimal complete definition

Nothing

Methods

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

See aeq.

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

fvAny' :: (Generic a, GAlpha (Rep a), Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> a -> f a Source #

See fvAny.

 fvAny' :: Fold a AnyName

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

Replace free names by bound names.

close :: (Generic a, GAlpha (Rep a)) => AlphaCtx -> NamePatFind -> a -> a Source #

Replace free names by bound names.

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

Replace bound names by free names.

open :: (Generic a, GAlpha (Rep a)) => AlphaCtx -> NthPatFind -> 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 :: (Generic a, GAlpha (Rep a)) => a -> DisjointSet AnyName Source #

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

isTerm :: a -> All Source #

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

isTerm :: (Generic a, GAlpha (Rep a)) => a -> All Source #

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

isEmbed :: a -> Bool Source #

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

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

If a is a pattern, find the index of the given name in the pattern.

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

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

lfreshen' :: (LFresh m, Generic a, GAlpha (Rep a)) => 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.

freshen' :: (Generic a, GAlpha (Rep a), 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 alpha-respecting total order on terms involving binders.

acompare' :: (Generic a, GAlpha (Rep a)) => AlphaCtx -> a -> a -> Ordering Source #

See acompare. An alpha-respecting total order on terms involving binders.

Instances
Alpha Bool Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Alpha

Alpha Char Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Alpha

Alpha Double Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Alpha

Alpha Float Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Alpha

Alpha Int Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Alpha

Alpha Integer Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Alpha

Alpha () Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Alpha

Methods

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

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

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

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

isPat :: () -> DisjointSet AnyName Source #

isTerm :: () -> All Source #

isEmbed :: () -> Bool Source #

nthPatFind :: () -> NthPatFind Source #

namePatFind :: () -> NamePatFind Source #

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

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

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

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

Alpha AnyName Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Alpha

Alpha a => Alpha [a] Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Alpha

Methods

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

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

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

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

isPat :: [a] -> DisjointSet AnyName Source #

isTerm :: [a] -> All Source #

isEmbed :: [a] -> Bool Source #

nthPatFind :: [a] -> NthPatFind Source #

namePatFind :: [a] -> NamePatFind Source #

swaps' :: AlphaCtx -> Perm AnyName -> [a] -> [a] Source #

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

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

acompare' :: AlphaCtx -> [a] -> [a] -> Ordering Source #

Alpha a => Alpha (Maybe a) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Alpha

(Integral n, Alpha n) => Alpha (Ratio n) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Alpha

Typeable a => Alpha (Name a) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Alpha

Show t => Alpha (Ignore t) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Ignore

Alpha t => Alpha (Embed t) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Embed

Alpha e => Alpha (Shift e) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Shift

Alpha p => Alpha (TRec p) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Rec

Alpha p => Alpha (Rec p) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Rec

(Alpha a, Alpha b) => Alpha (Either a b) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Alpha

(Alpha a, Alpha b) => Alpha (a, b) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Alpha

Methods

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

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

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

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

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

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

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

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

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

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

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

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

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

(Alpha p1, Alpha p2) => Alpha (Rebind p1 p2) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Rebind

Methods

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

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

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

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

isPat :: Rebind p1 p2 -> DisjointSet AnyName Source #

isTerm :: Rebind p1 p2 -> All Source #

isEmbed :: Rebind p1 p2 -> Bool Source #

nthPatFind :: Rebind p1 p2 -> NthPatFind Source #

namePatFind :: Rebind p1 p2 -> NamePatFind Source #

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

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

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

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

(Alpha p, Alpha t) => Alpha (Bind p t) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Bind

Methods

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

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

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

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

isPat :: Bind p t -> DisjointSet AnyName Source #

isTerm :: Bind p t -> All Source #

isEmbed :: Bind p t -> Bool Source #

nthPatFind :: Bind p t -> NthPatFind Source #

namePatFind :: Bind p t -> NamePatFind Source #

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

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

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

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

(Alpha a, Alpha b, Alpha c) => Alpha (a, b, c) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Alpha

Methods

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

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

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

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

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

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

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

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

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

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

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

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

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

(Alpha a, Alpha b, Alpha c, Alpha d) => Alpha (a, b, c, d) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Alpha

Methods

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Defined in Unbound.Generics.LocallyNameless.Alpha

Methods

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Constructors

DisjointSet (Maybe [a]) 
Instances
Foldable DisjointSet Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Alpha

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 => Semigroup (DisjointSet a) Source #

Since: 0.3.2

Instance details

Defined in Unbound.Generics.LocallyNameless.Alpha

Eq a => Monoid (DisjointSet a) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Alpha

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

newtype NthPatFind Source #

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

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 :: AlphaCtx Source #

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.

termCtx :: AlphaCtx -> AlphaCtx Source #

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

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

gaeq :: GAlpha f => AlphaCtx -> f a -> f a -> Bool Source #

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

gclose :: GAlpha f => AlphaCtx -> NamePatFind -> f a -> f a Source #

gopen :: GAlpha f => AlphaCtx -> NthPatFind -> f a -> f a Source #

gisPat :: GAlpha f => f a -> DisjointSet AnyName Source #

gisTerm :: GAlpha f => f a -> All Source #

gnthPatFind :: GAlpha f => f a -> NthPatFind Source #

gnamePatFind :: GAlpha f => f a -> NamePatFind Source #

gswaps :: GAlpha f => AlphaCtx -> Perm AnyName -> f a -> f a Source #

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

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

gacompare :: GAlpha f => AlphaCtx -> f a -> f a -> Ordering Source #

Interal helpers for gfreshen

data FFM f a Source #

Instances
Monad (FFM f) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Alpha

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) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Alpha

Methods

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

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

Applicative (FFM f) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Alpha

Methods

pure :: a -> FFM f a #

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

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

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

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

Fresh m => Fresh (FFM m) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Alpha

Methods

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

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

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