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 #

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

Monoid NthPatFind #
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

Monoid NamePatFind #
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) #
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 #