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.

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

Defined in Unbound.Generics.LocallyNameless.Alpha

Methods

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

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

close :: AlphaCtx -> NamePatFind -> Bool -> Bool

open :: AlphaCtx -> NthPatFind -> Bool -> Bool

isPat :: Bool -> DisjointSet AnyName

isTerm :: Bool -> All

isEmbed :: Bool -> Bool

nthPatFind :: Bool -> NthPatFind

namePatFind :: Bool -> NamePatFind

swaps' :: AlphaCtx -> Perm AnyName -> Bool -> Bool

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

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

acompare' :: AlphaCtx -> Bool -> Bool -> Ordering

Alpha Char

Defined in Unbound.Generics.LocallyNameless.Alpha

Methods

aeq' :: AlphaCtx -> Char -> Char -> Bool

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

close :: AlphaCtx -> NamePatFind -> Char -> Char

open :: AlphaCtx -> NthPatFind -> Char -> Char

isPat :: Char -> DisjointSet AnyName

isTerm :: Char -> All

isEmbed :: Char -> Bool

nthPatFind :: Char -> NthPatFind

namePatFind :: Char -> NamePatFind

swaps' :: AlphaCtx -> Perm AnyName -> Char -> Char

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

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

acompare' :: AlphaCtx -> Char -> Char -> Ordering

Alpha Double

Defined in Unbound.Generics.LocallyNameless.Alpha

Methods

aeq' :: AlphaCtx -> Double -> Double -> Bool

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

close :: AlphaCtx -> NamePatFind -> Double -> Double

open :: AlphaCtx -> NthPatFind -> Double -> Double

isPat :: Double -> DisjointSet AnyName

isTerm :: Double -> All

isEmbed :: Double -> Bool

nthPatFind :: Double -> NthPatFind

namePatFind :: Double -> NamePatFind

swaps' :: AlphaCtx -> Perm AnyName -> Double -> Double

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

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

acompare' :: AlphaCtx -> Double -> Double -> Ordering

Alpha Float

Defined in Unbound.Generics.LocallyNameless.Alpha

Methods

aeq' :: AlphaCtx -> Float -> Float -> Bool

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

close :: AlphaCtx -> NamePatFind -> Float -> Float

open :: AlphaCtx -> NthPatFind -> Float -> Float

isPat :: Float -> DisjointSet AnyName

isTerm :: Float -> All

isEmbed :: Float -> Bool

nthPatFind :: Float -> NthPatFind

namePatFind :: Float -> NamePatFind

swaps' :: AlphaCtx -> Perm AnyName -> Float -> Float

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

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

acompare' :: AlphaCtx -> Float -> Float -> Ordering

Alpha Int

Defined in Unbound.Generics.LocallyNameless.Alpha

Methods

aeq' :: AlphaCtx -> Int -> Int -> Bool

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

close :: AlphaCtx -> NamePatFind -> Int -> Int

open :: AlphaCtx -> NthPatFind -> Int -> Int

isPat :: Int -> DisjointSet AnyName

isTerm :: Int -> All

isEmbed :: Int -> Bool

nthPatFind :: Int -> NthPatFind

namePatFind :: Int -> NamePatFind

swaps' :: AlphaCtx -> Perm AnyName -> Int -> Int

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

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

acompare' :: AlphaCtx -> Int -> Int -> Ordering

Alpha Integer

Defined in Unbound.Generics.LocallyNameless.Alpha

Methods

aeq' :: AlphaCtx -> Integer -> Integer -> Bool

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

close :: AlphaCtx -> NamePatFind -> Integer -> Integer

open :: AlphaCtx -> NthPatFind -> Integer -> Integer

isPat :: Integer -> DisjointSet AnyName

isTerm :: Integer -> All

isEmbed :: Integer -> Bool

nthPatFind :: Integer -> NthPatFind

namePatFind :: Integer -> NamePatFind

swaps' :: AlphaCtx -> Perm AnyName -> Integer -> Integer

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

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

acompare' :: AlphaCtx -> Integer -> Integer -> Ordering

Alpha ()

Defined in Unbound.Generics.LocallyNameless.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

Defined in Unbound.Generics.LocallyNameless.Alpha

Methods

aeq' :: AlphaCtx -> AnyName -> AnyName -> Bool

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

close :: AlphaCtx -> NamePatFind -> AnyName -> AnyName

open :: AlphaCtx -> NthPatFind -> AnyName -> AnyName

isPat :: AnyName -> DisjointSet AnyName

isTerm :: AnyName -> All

isEmbed :: AnyName -> Bool

nthPatFind :: AnyName -> NthPatFind

namePatFind :: AnyName -> NamePatFind

swaps' :: AlphaCtx -> Perm AnyName -> AnyName -> AnyName

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

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

acompare' :: AlphaCtx -> AnyName -> AnyName -> Ordering

Alpha a => Alpha [a]

Defined in Unbound.Generics.LocallyNameless.Alpha

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)

Defined in Unbound.Generics.LocallyNameless.Alpha

Methods

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

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

close :: AlphaCtx -> NamePatFind -> Maybe a -> Maybe a

open :: AlphaCtx -> NthPatFind -> Maybe a -> Maybe a

isPat :: Maybe a -> DisjointSet AnyName

isTerm :: Maybe a -> All

isEmbed :: Maybe a -> Bool

nthPatFind :: Maybe a -> NthPatFind

namePatFind :: Maybe a -> NamePatFind

swaps' :: AlphaCtx -> Perm AnyName -> Maybe a -> Maybe a

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

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

acompare' :: AlphaCtx -> Maybe a -> Maybe a -> Ordering

(Integral n, Alpha n) => Alpha (Ratio n)

Defined in Unbound.Generics.LocallyNameless.Alpha

Methods

aeq' :: AlphaCtx -> Ratio n -> Ratio n -> Bool

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

close :: AlphaCtx -> NamePatFind -> Ratio n -> Ratio n

open :: AlphaCtx -> NthPatFind -> Ratio n -> Ratio n

isPat :: Ratio n -> DisjointSet AnyName

isTerm :: Ratio n -> All

isEmbed :: Ratio n -> Bool

nthPatFind :: Ratio n -> NthPatFind

namePatFind :: Ratio n -> NamePatFind

swaps' :: AlphaCtx -> Perm AnyName -> Ratio n -> Ratio n

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

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

acompare' :: AlphaCtx -> Ratio n -> Ratio n -> Ordering

Typeable a => Alpha (Name a)

Defined in Unbound.Generics.LocallyNameless.Alpha

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)

Defined in Unbound.Generics.LocallyNameless.Embed

Methods

aeq' :: AlphaCtx -> Embed t -> Embed t -> Bool

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

close :: AlphaCtx -> NamePatFind -> Embed t -> Embed t

open :: AlphaCtx -> NthPatFind -> Embed t -> Embed t

isPat :: Embed t -> DisjointSet AnyName

isTerm :: Embed t -> All

isEmbed :: Embed t -> Bool

nthPatFind :: Embed t -> NthPatFind

namePatFind :: Embed t -> NamePatFind

swaps' :: AlphaCtx -> Perm AnyName -> Embed t -> Embed t

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

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

acompare' :: AlphaCtx -> Embed t -> Embed t -> Ordering

Alpha e => Alpha (Shift e)

Defined in Unbound.Generics.LocallyNameless.Shift

Methods

aeq' :: AlphaCtx -> Shift e -> Shift e -> Bool

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

close :: AlphaCtx -> NamePatFind -> Shift e -> Shift e

open :: AlphaCtx -> NthPatFind -> Shift e -> Shift e

isPat :: Shift e -> DisjointSet AnyName

isTerm :: Shift e -> All

isEmbed :: Shift e -> Bool

nthPatFind :: Shift e -> NthPatFind

namePatFind :: Shift e -> NamePatFind

swaps' :: AlphaCtx -> Perm AnyName -> Shift e -> Shift e

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

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

acompare' :: AlphaCtx -> Shift e -> Shift e -> Ordering

Alpha p => Alpha (TRec p)

Defined in Unbound.Generics.LocallyNameless.Rec

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)

Defined in Unbound.Generics.LocallyNameless.Rec

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 a, Alpha b) => Alpha (Either a b)

Defined in Unbound.Generics.LocallyNameless.Alpha

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 b0) -> m b0

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)

Defined in Unbound.Generics.LocallyNameless.Alpha

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 b0) -> m b0

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

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

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

Defined in Unbound.Generics.LocallyNameless.Rebind

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 p, Alpha t) => Alpha (Bind p t)

Defined in Unbound.Generics.LocallyNameless.Bind

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 a, Alpha b, Alpha c) => Alpha (a, b, c)

Defined in Unbound.Generics.LocallyNameless.Alpha

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 b0) -> m b0

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)

Defined in Unbound.Generics.LocallyNameless.Alpha

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 b0) -> m b0

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)

Defined in Unbound.Generics.LocallyNameless.Alpha

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 b0) -> m b0

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

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)

Since: unbound-generics-0.3.2

Defined in Unbound.Generics.LocallyNameless.Alpha

Methods

(<>) :: DisjointSet a -> DisjointSet a -> DisjointSet a

sconcat :: NonEmpty (DisjointSet a) -> DisjointSet a

stimes :: Integral b => b -> DisjointSet a -> DisjointSet a

Eq a => Monoid (DisjointSet a)

Defined in Unbound.Generics.LocallyNameless.Alpha

Methods

mempty :: DisjointSet a

mappend :: DisjointSet a -> DisjointSet a -> DisjointSet a

mconcat :: [DisjointSet a] -> 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

Constructors

NthPatFind

Fields

• runNthPatFind :: Integer -> Either Integer AnyName

Instances

Semigroup NthPatFind

Since: unbound-generics-0.3.2

Defined in Unbound.Generics.LocallyNameless.Alpha

Methods

(<>) :: NthPatFind -> NthPatFind -> NthPatFind

sconcat :: NonEmpty NthPatFind -> NthPatFind

stimes :: Integral b => b -> NthPatFind -> NthPatFind

Monoid NthPatFind

Defined in Unbound.Generics.LocallyNameless.Alpha

Methods

mempty :: NthPatFind

mappend :: NthPatFind -> NthPatFind -> NthPatFind

mconcat :: [NthPatFind] -> NthPatFind

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

Constructors

NamePatFind

Fields

• runNamePatFind :: AnyName -> Either Integer Integer

Instances

Semigroup NamePatFind

Since: unbound-generics-0.3.2

Defined in Unbound.Generics.LocallyNameless.Alpha

Methods

(<>) :: NamePatFind -> NamePatFind -> NamePatFind

sconcat :: NonEmpty NamePatFind -> NamePatFind

stimes :: Integral b => b -> NamePatFind -> NamePatFind

Monoid NamePatFind

Defined in Unbound.Generics.LocallyNameless.Alpha

Methods

mempty :: NamePatFind

mappend :: NamePatFind -> NamePatFind -> NamePatFind

mconcat :: [NamePatFind] -> NamePatFind

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)

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)

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)

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)

Defined in Unbound.Generics.LocallyNameless.Alpha

Methods

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

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

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