Copyright	(c) 2014 Aleksey Kliger
License	BSD3 (See LICENSE)
Maintainer	Aleksey Kliger
Stability	experimental
Safe Haskell	None
Language	Haskell2010
Extensions	DefaultSignatures FlexibleContexts RankNTypes TypeOperators ExplicitNamespaces ExplicitForAll

Unbound.Generics.LocallyNameless.Alpha

Contents

Name-aware opertions
Binder variables
Implementation details
Internal
- Interal helpers for gfreshen

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.

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 #
Methods aeq' :: AlphaCtx -> Bool -> Bool -> Bool Source # fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Bool -> f Bool Source # close :: AlphaCtx -> NamePatFind -> Bool -> Bool Source # open :: AlphaCtx -> NthPatFind -> Bool -> Bool Source # isPat :: Bool -> DisjointSet AnyName Source # isTerm :: Bool -> All Source # isEmbed :: Bool -> Bool Source # nthPatFind :: Bool -> NthPatFind Source # namePatFind :: Bool -> NamePatFind Source # swaps' :: AlphaCtx -> Perm AnyName -> Bool -> Bool Source # lfreshen' :: LFresh m => AlphaCtx -> Bool -> (Bool -> Perm AnyName -> m b) -> m b Source # freshen' :: Fresh m => AlphaCtx -> Bool -> m (Bool, Perm AnyName) Source # acompare' :: AlphaCtx -> Bool -> Bool -> Ordering Source #
Alpha Char Source #
Methods aeq' :: AlphaCtx -> Char -> Char -> Bool Source # fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Char -> f Char Source # close :: AlphaCtx -> NamePatFind -> Char -> Char Source # open :: AlphaCtx -> NthPatFind -> Char -> Char Source # isPat :: Char -> DisjointSet AnyName Source # isTerm :: Char -> All Source # isEmbed :: Char -> Bool Source # nthPatFind :: Char -> NthPatFind Source # namePatFind :: Char -> NamePatFind Source # swaps' :: AlphaCtx -> Perm AnyName -> Char -> Char Source # lfreshen' :: LFresh m => AlphaCtx -> Char -> (Char -> Perm AnyName -> m b) -> m b Source # freshen' :: Fresh m => AlphaCtx -> Char -> m (Char, Perm AnyName) Source # acompare' :: AlphaCtx -> Char -> Char -> Ordering Source #
Alpha Double Source #
Methods aeq' :: AlphaCtx -> Double -> Double -> Bool Source # fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Double -> f Double Source # close :: AlphaCtx -> NamePatFind -> Double -> Double Source # open :: AlphaCtx -> NthPatFind -> Double -> Double Source # isPat :: Double -> DisjointSet AnyName Source # isTerm :: Double -> All Source # isEmbed :: Double -> Bool Source # nthPatFind :: Double -> NthPatFind Source # namePatFind :: Double -> NamePatFind Source # swaps' :: AlphaCtx -> Perm AnyName -> Double -> Double Source # lfreshen' :: LFresh m => AlphaCtx -> Double -> (Double -> Perm AnyName -> m b) -> m b Source # freshen' :: Fresh m => AlphaCtx -> Double -> m (Double, Perm AnyName) Source # acompare' :: AlphaCtx -> Double -> Double -> Ordering Source #
Alpha Float Source #
Methods aeq' :: AlphaCtx -> Float -> Float -> Bool Source # fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Float -> f Float Source # close :: AlphaCtx -> NamePatFind -> Float -> Float Source # open :: AlphaCtx -> NthPatFind -> Float -> Float Source # isPat :: Float -> DisjointSet AnyName Source # isTerm :: Float -> All Source # isEmbed :: Float -> Bool Source # nthPatFind :: Float -> NthPatFind Source # namePatFind :: Float -> NamePatFind Source # swaps' :: AlphaCtx -> Perm AnyName -> Float -> Float Source # lfreshen' :: LFresh m => AlphaCtx -> Float -> (Float -> Perm AnyName -> m b) -> m b Source # freshen' :: Fresh m => AlphaCtx -> Float -> m (Float, Perm AnyName) Source # acompare' :: AlphaCtx -> Float -> Float -> Ordering Source #
Alpha Int Source #
Methods aeq' :: AlphaCtx -> Int -> Int -> Bool Source # fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Int -> f Int Source # close :: AlphaCtx -> NamePatFind -> Int -> Int Source # open :: AlphaCtx -> NthPatFind -> Int -> Int Source # isPat :: Int -> DisjointSet AnyName Source # isTerm :: Int -> All Source # isEmbed :: Int -> Bool Source # nthPatFind :: Int -> NthPatFind Source # namePatFind :: Int -> NamePatFind Source # swaps' :: AlphaCtx -> Perm AnyName -> Int -> Int Source # lfreshen' :: LFresh m => AlphaCtx -> Int -> (Int -> Perm AnyName -> m b) -> m b Source # freshen' :: Fresh m => AlphaCtx -> Int -> m (Int, Perm AnyName) Source # acompare' :: AlphaCtx -> Int -> Int -> Ordering Source #
Alpha Integer Source #
Methods aeq' :: AlphaCtx -> Integer -> Integer -> Bool Source # fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Integer -> f Integer Source # close :: AlphaCtx -> NamePatFind -> Integer -> Integer Source # open :: AlphaCtx -> NthPatFind -> Integer -> Integer Source # isPat :: Integer -> DisjointSet AnyName Source # isTerm :: Integer -> All Source # isEmbed :: Integer -> Bool Source # nthPatFind :: Integer -> NthPatFind Source # namePatFind :: Integer -> NamePatFind Source # swaps' :: AlphaCtx -> Perm AnyName -> Integer -> Integer Source # lfreshen' :: LFresh m => AlphaCtx -> Integer -> (Integer -> Perm AnyName -> m b) -> m b Source # freshen' :: Fresh m => AlphaCtx -> Integer -> m (Integer, Perm AnyName) Source # acompare' :: AlphaCtx -> Integer -> Integer -> Ordering Source #
Alpha () Source #
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 #
Methods aeq' :: AlphaCtx -> AnyName -> AnyName -> Bool Source # fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> AnyName -> f AnyName Source # close :: AlphaCtx -> NamePatFind -> AnyName -> AnyName Source # open :: AlphaCtx -> NthPatFind -> AnyName -> AnyName Source # isPat :: AnyName -> DisjointSet AnyName Source # isTerm :: AnyName -> All Source # isEmbed :: AnyName -> Bool Source # nthPatFind :: AnyName -> NthPatFind Source # namePatFind :: AnyName -> NamePatFind Source # swaps' :: AlphaCtx -> Perm AnyName -> AnyName -> AnyName Source # lfreshen' :: LFresh m => AlphaCtx -> AnyName -> (AnyName -> Perm AnyName -> m b) -> m b Source # freshen' :: Fresh m => AlphaCtx -> AnyName -> m (AnyName, Perm AnyName) Source # acompare' :: AlphaCtx -> AnyName -> AnyName -> Ordering Source #
Alpha a => Alpha [a] Source #
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 #
Methods aeq' :: AlphaCtx -> Maybe a -> Maybe a -> Bool Source # fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Maybe a -> f (Maybe a) Source # close :: AlphaCtx -> NamePatFind -> Maybe a -> Maybe a Source # open :: AlphaCtx -> NthPatFind -> Maybe a -> Maybe a Source # isPat :: Maybe a -> DisjointSet AnyName Source # isTerm :: Maybe a -> All Source # isEmbed :: Maybe a -> Bool Source # nthPatFind :: Maybe a -> NthPatFind Source # namePatFind :: Maybe a -> NamePatFind Source # swaps' :: AlphaCtx -> Perm AnyName -> Maybe a -> Maybe a Source # lfreshen' :: LFresh m => AlphaCtx -> Maybe a -> (Maybe a -> Perm AnyName -> m b) -> m b Source # freshen' :: Fresh m => AlphaCtx -> Maybe a -> m (Maybe a, Perm AnyName) Source # acompare' :: AlphaCtx -> Maybe a -> Maybe a -> Ordering Source #
(Integral n, Alpha n) => Alpha (Ratio n) Source #
Methods aeq' :: AlphaCtx -> Ratio n -> Ratio n -> Bool Source # fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Ratio n -> f (Ratio n) Source # close :: AlphaCtx -> NamePatFind -> Ratio n -> Ratio n Source # open :: AlphaCtx -> NthPatFind -> Ratio n -> Ratio n Source # isPat :: Ratio n -> DisjointSet AnyName Source # isTerm :: Ratio n -> All Source # isEmbed :: Ratio n -> Bool Source # nthPatFind :: Ratio n -> NthPatFind Source # namePatFind :: Ratio n -> NamePatFind Source # swaps' :: AlphaCtx -> Perm AnyName -> Ratio n -> Ratio n Source # lfreshen' :: LFresh m => AlphaCtx -> Ratio n -> (Ratio n -> Perm AnyName -> m b) -> m b Source # freshen' :: Fresh m => AlphaCtx -> Ratio n -> m (Ratio n, Perm AnyName) Source # acompare' :: AlphaCtx -> Ratio n -> Ratio n -> Ordering Source #
Typeable * a => Alpha (Name a) Source #
Methods aeq' :: AlphaCtx -> Name a -> Name a -> Bool Source # fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Name a -> f (Name a) Source # close :: AlphaCtx -> NamePatFind -> Name a -> Name a Source # open :: AlphaCtx -> NthPatFind -> Name a -> Name a Source # isPat :: Name a -> DisjointSet AnyName Source # isTerm :: Name a -> All Source # isEmbed :: Name a -> Bool Source # nthPatFind :: Name a -> NthPatFind Source # namePatFind :: Name a -> NamePatFind Source # swaps' :: AlphaCtx -> Perm AnyName -> Name a -> Name a Source # lfreshen' :: LFresh m => AlphaCtx -> Name a -> (Name a -> Perm AnyName -> m b) -> m b Source # freshen' :: Fresh m => AlphaCtx -> Name a -> m (Name a, Perm AnyName) Source # acompare' :: AlphaCtx -> Name a -> Name a -> Ordering Source #
Alpha t => Alpha (Embed t) Source #
Methods aeq' :: AlphaCtx -> Embed t -> Embed t -> Bool Source # fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Embed t -> f (Embed t) Source # close :: AlphaCtx -> NamePatFind -> Embed t -> Embed t Source # open :: AlphaCtx -> NthPatFind -> Embed t -> Embed t Source # isPat :: Embed t -> DisjointSet AnyName Source # isTerm :: Embed t -> All Source # isEmbed :: Embed t -> Bool Source # nthPatFind :: Embed t -> NthPatFind Source # namePatFind :: Embed t -> NamePatFind Source # swaps' :: AlphaCtx -> Perm AnyName -> Embed t -> Embed t Source # lfreshen' :: LFresh m => AlphaCtx -> Embed t -> (Embed t -> Perm AnyName -> m b) -> m b Source # freshen' :: Fresh m => AlphaCtx -> Embed t -> m (Embed t, Perm AnyName) Source # acompare' :: AlphaCtx -> Embed t -> Embed t -> Ordering Source #
Alpha e => Alpha (Shift e) Source #
Methods aeq' :: AlphaCtx -> Shift e -> Shift e -> Bool Source # fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Shift e -> f (Shift e) Source # close :: AlphaCtx -> NamePatFind -> Shift e -> Shift e Source # open :: AlphaCtx -> NthPatFind -> Shift e -> Shift e Source # isPat :: Shift e -> DisjointSet AnyName Source # isTerm :: Shift e -> All Source # isEmbed :: Shift e -> Bool Source # nthPatFind :: Shift e -> NthPatFind Source # namePatFind :: Shift e -> NamePatFind Source # swaps' :: AlphaCtx -> Perm AnyName -> Shift e -> Shift e Source # lfreshen' :: LFresh m => AlphaCtx -> Shift e -> (Shift e -> Perm AnyName -> m b) -> m b Source # freshen' :: Fresh m => AlphaCtx -> Shift e -> m (Shift e, Perm AnyName) Source # acompare' :: AlphaCtx -> Shift e -> Shift e -> Ordering Source #
Alpha p => Alpha (TRec p) Source #
Methods aeq' :: AlphaCtx -> TRec p -> TRec p -> Bool Source # fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> TRec p -> f (TRec p) Source # close :: AlphaCtx -> NamePatFind -> TRec p -> TRec p Source # open :: AlphaCtx -> NthPatFind -> TRec p -> TRec p Source # isPat :: TRec p -> DisjointSet AnyName Source # isTerm :: TRec p -> All Source # isEmbed :: TRec p -> Bool Source # nthPatFind :: TRec p -> NthPatFind Source # namePatFind :: TRec p -> NamePatFind Source # swaps' :: AlphaCtx -> Perm AnyName -> TRec p -> TRec p Source # lfreshen' :: LFresh m => AlphaCtx -> TRec p -> (TRec p -> Perm AnyName -> m b) -> m b Source # freshen' :: Fresh m => AlphaCtx -> TRec p -> m (TRec p, Perm AnyName) Source # acompare' :: AlphaCtx -> TRec p -> TRec p -> Ordering Source #
Alpha p => Alpha (Rec p) Source #
Methods aeq' :: AlphaCtx -> Rec p -> Rec p -> Bool Source # fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Rec p -> f (Rec p) Source # close :: AlphaCtx -> NamePatFind -> Rec p -> Rec p Source # open :: AlphaCtx -> NthPatFind -> Rec p -> Rec p Source # isPat :: Rec p -> DisjointSet AnyName Source # isTerm :: Rec p -> All Source # isEmbed :: Rec p -> Bool Source # nthPatFind :: Rec p -> NthPatFind Source # namePatFind :: Rec p -> NamePatFind Source # swaps' :: AlphaCtx -> Perm AnyName -> Rec p -> Rec p Source # lfreshen' :: LFresh m => AlphaCtx -> Rec p -> (Rec p -> Perm AnyName -> m b) -> m b Source # freshen' :: Fresh m => AlphaCtx -> Rec p -> m (Rec p, Perm AnyName) Source # acompare' :: AlphaCtx -> Rec p -> Rec p -> Ordering Source #
(Alpha a, Alpha b) => Alpha (Either a b) Source #
Methods aeq' :: AlphaCtx -> Either a b -> Either a b -> Bool Source # fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Either a b -> f (Either a b) Source # close :: AlphaCtx -> NamePatFind -> Either a b -> Either a b Source # open :: AlphaCtx -> NthPatFind -> Either a b -> Either a b Source # isPat :: Either a b -> DisjointSet AnyName Source # isTerm :: Either a b -> All Source # isEmbed :: Either a b -> Bool Source # nthPatFind :: Either a b -> NthPatFind Source # namePatFind :: Either a b -> NamePatFind Source # swaps' :: AlphaCtx -> Perm AnyName -> Either a b -> Either a b Source # lfreshen' :: LFresh m => AlphaCtx -> Either a b -> (Either a b -> Perm AnyName -> m b) -> m b Source # freshen' :: Fresh m => AlphaCtx -> Either a b -> m (Either a b, Perm AnyName) Source # acompare' :: AlphaCtx -> Either a b -> Either a b -> Ordering Source #
(Alpha a, Alpha b) => Alpha (a, b) Source #
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 b) -> m b 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 #
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 #
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 #
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 b) -> m b 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 #
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 b) -> m b 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 #
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 b) -> m b 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 #
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
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) Source #
Methods mempty :: DisjointSet a # mappend :: DisjointSet a -> DisjointSet a -> DisjointSet a # mconcat :: [DisjointSet a] -> DisjointSet a #

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

Constructors

NthPatFind
Fields runNthPatFind :: Integer -> Either Integer AnyName

Instances

Semigroup NthPatFind Source #	Since: 0.3.2
Methods (<>) :: NthPatFind -> NthPatFind -> NthPatFind # sconcat :: NonEmpty NthPatFind -> NthPatFind # stimes :: Integral b => b -> NthPatFind -> NthPatFind #
Monoid NthPatFind Source #
Methods mempty :: NthPatFind # mappend :: NthPatFind -> NthPatFind -> NthPatFind # mconcat :: [NthPatFind] -> NthPatFind #

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

Constructors

NamePatFind
Fields runNamePatFind :: AnyName -> Either Integer Integer

Instances

Semigroup NamePatFind Source #	Since: 0.3.2
Methods (<>) :: NamePatFind -> NamePatFind -> NamePatFind # sconcat :: NonEmpty NamePatFind -> NamePatFind # stimes :: Integral b => b -> NamePatFind -> NamePatFind #
Monoid NamePatFind Source #
Methods mempty :: NamePatFind # mappend :: NamePatFind -> NamePatFind -> NamePatFind # mconcat :: [NamePatFind] -> NamePatFind #

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 #
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 #
Methods fmap :: (a -> b) -> FFM f a -> FFM f b # (<$) :: a -> FFM f b -> FFM f a #
Applicative (FFM f) Source #
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 #
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 #