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

class Show a => Alpha a where
- 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
newtype DisjointSet a = DisjointSet (Maybe [a])
inconsistentDisjointSet :: DisjointSet a
singletonDisjointSet :: a -> DisjointSet a
isConsistentDisjointSet :: DisjointSet a -> Bool
isNullDisjointSet :: DisjointSet a -> Bool
newtype NthPatFind = NthPatFind {
- runNthPatFind :: Integer -> Either Integer AnyName
}
newtype NamePatFind = NamePatFind {
- runNamePatFind :: AnyName -> Either Integer Integer
}
data AlphaCtx
initialCtx :: AlphaCtx
patternCtx :: AlphaCtx -> AlphaCtx
termCtx :: AlphaCtx -> AlphaCtx
isTermCtx :: AlphaCtx -> Bool
incrLevelCtx :: AlphaCtx -> AlphaCtx
decrLevelCtx :: AlphaCtx -> AlphaCtx
isZeroLevelCtx :: AlphaCtx -> Bool
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
data FFM f a
liftFFM :: Monad m => m a -> FFM m a
retractFFM :: Monad m => FFM m a -> m a

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.

Minimal complete definition

Nothing

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 #
Instance details 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 #
Instance details 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 #
Instance details 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 #
Instance details 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 #
Instance details 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 #
Instance details 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 () #
Instance details 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 #
Instance details 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] #
Instance details 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) #
Instance details 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) #
Instance details 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) #
Instance details 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 #
Show t => Alpha (Ignore t) #
Instance details Defined in Unbound.Generics.LocallyNameless.Ignore Methods aeq' :: AlphaCtx -> Ignore t -> Ignore t -> Bool # fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Ignore t -> f (Ignore t) # close :: AlphaCtx -> NamePatFind -> Ignore t -> Ignore t # open :: AlphaCtx -> NthPatFind -> Ignore t -> Ignore t # isPat :: Ignore t -> DisjointSet AnyName # isTerm :: Ignore t -> All # isEmbed :: Ignore t -> Bool # nthPatFind :: Ignore t -> NthPatFind # namePatFind :: Ignore t -> NamePatFind # swaps' :: AlphaCtx -> Perm AnyName -> Ignore t -> Ignore t # lfreshen' :: LFresh m => AlphaCtx -> Ignore t -> (Ignore t -> Perm AnyName -> m b) -> m b # freshen' :: Fresh m => AlphaCtx -> Ignore t -> m (Ignore t, Perm AnyName) # acompare' :: AlphaCtx -> Ignore t -> Ignore t -> Ordering #
Alpha t => Alpha (Embed t) #
Instance details 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) #
Instance details 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) #
Instance details 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) #
Instance details 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) #
Instance details 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) #
Instance details 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) #
Instance details 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) #
Instance details 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) #
Instance details 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) #
Instance details 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) #
Instance details 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 #
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) #	Since: 0.3.2
Instance details 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) #
Instance details 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: 0.3.2
Instance details Defined in Unbound.Generics.LocallyNameless.Alpha Methods (<>) :: NthPatFind -> NthPatFind -> NthPatFind # sconcat :: NonEmpty NthPatFind -> NthPatFind # stimes :: Integral b => b -> NthPatFind -> NthPatFind #
Monoid NthPatFind #
Instance details 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: 0.3.2
Instance details Defined in Unbound.Generics.LocallyNameless.Alpha Methods (<>) :: NamePatFind -> NamePatFind -> NamePatFind # sconcat :: NonEmpty NamePatFind -> NamePatFind # stimes :: Integral b => b -> NamePatFind -> NamePatFind #
Monoid NamePatFind #
Instance details 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) #
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) #
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) #
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) #
Instance details 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 #