Safe Haskell	None
Language	Haskell2010

Ouroboros.Consensus.HardFork.Combinator.Util.Match

Contents

Utilities
SOP operators

Description

Intended for qualified import

import Ouroboros.Consensus.HardFork.Combinator.Util.Match (Mismatch(..))
import qualified Ouroboros.Consensus.HardFork.Combinator.Util.Match as Match

Synopsis

data Mismatch :: (k -> Type ) -> (k -> Type ) -> [k] -> Type where
- ML :: f x -> NS g xs -> Mismatch f g (x ': xs)
- MR :: NS f xs -> g x -> Mismatch f g (x ': xs)
- MS :: Mismatch f g xs -> Mismatch f g (x ': xs)
flip :: Mismatch f g xs -> Mismatch g f xs
matchNS :: NS f xs -> NS g xs -> Either ( Mismatch f g xs) ( NS ( Product f g) xs)
matchTelescope :: NS h xs -> Telescope g f xs -> Either ( Mismatch h f xs) ( Telescope g ( Product h f) xs)
mismatchNotEmpty :: Mismatch f g xs -> ( forall x xs'. xs ~ (x ': xs') => Mismatch f g (x ': xs') -> a) -> a
mismatchNotFirst :: Mismatch f g (x ': xs) -> Either ( NS f xs) ( NS g xs)
mismatchOne :: Mismatch f g '[x] -> Void
mismatchToNS :: Mismatch f g xs -> ( NS f xs, NS g xs)
mismatchTwo :: Mismatch f g '[x, y] -> Either (f x, g y) (f y, g x)
mkMismatchTwo :: Either (f x, g y) (f y, g x) -> Mismatch f g '[x, y]
mustMatchNS :: forall f g xs. HasCallStack => String -> NS f xs -> NS g xs -> NS ( Product f g) xs
bihap :: NP (f -.-> f') xs -> NP (g -.-> g') xs -> Mismatch f g xs -> Mismatch f' g' xs
bihcmap :: All c xs => proxy c -> ( forall x. c x => f x -> f' x) -> ( forall x. c x => g x -> g' x) -> Mismatch f g xs -> Mismatch f' g' xs
bihmap :: SListI xs => ( forall x. f x -> f' x) -> ( forall x. g x -> g' x) -> Mismatch f g xs -> Mismatch f' g' xs

Documentation

data Mismatch :: (k -> Type ) -> (k -> Type ) -> [k] -> Type where Source #

Constructors

ML :: f x -> NS g xs -> Mismatch f g (x ': xs)
MR :: NS f xs -> g x -> Mismatch f g (x ': xs)
MS :: Mismatch f g xs -> Mismatch f g (x ': xs)

Instances

Instances details

HAp ( Mismatch f :: (k -> Type ) -> [k] -> Type ) Source #
Instance details Defined in Ouroboros.Consensus.HardFork.Combinator.Util.Match Methods hap :: forall (f0 :: k0 -> Type ) (g :: k0 -> Type ) (xs :: l). Prod ( Mismatch f) (f0 -.-> g) xs -> Mismatch f f0 xs -> Mismatch f g xs Source #
( All ( Compose Eq f) xs, All ( Compose Eq g) xs) => Eq ( Mismatch f g xs) Source #
Instance details Defined in Ouroboros.Consensus.HardFork.Combinator.Util.Match Methods (==) :: Mismatch f g xs -> Mismatch f g xs -> Bool Source # (/=) :: Mismatch f g xs -> Mismatch f g xs -> Bool Source #
( All ( Compose Eq f) xs, All ( Compose Ord f) xs, All ( Compose Eq g) xs, All ( Compose Ord g) xs) => Ord ( Mismatch f g xs) Source #
Instance details Defined in Ouroboros.Consensus.HardFork.Combinator.Util.Match Methods compare :: Mismatch f g xs -> Mismatch f g xs -> Ordering Source # (<) :: Mismatch f g xs -> Mismatch f g xs -> Bool Source # (<=) :: Mismatch f g xs -> Mismatch f g xs -> Bool Source # (>) :: Mismatch f g xs -> Mismatch f g xs -> Bool Source # (>=) :: Mismatch f g xs -> Mismatch f g xs -> Bool Source # max :: Mismatch f g xs -> Mismatch f g xs -> Mismatch f g xs Source # min :: Mismatch f g xs -> Mismatch f g xs -> Mismatch f g xs Source #
( All ( Compose Show f) xs, All ( Compose Show g) xs) => Show ( Mismatch f g xs) Source #
Instance details Defined in Ouroboros.Consensus.HardFork.Combinator.Util.Match Methods showsPrec :: Int -> Mismatch f g xs -> ShowS Source # show :: Mismatch f g xs -> String Source # showList :: [ Mismatch f g xs] -> ShowS Source #
( All ( Compose NoThunks f) xs, All ( Compose NoThunks g) xs) => NoThunks ( Mismatch f g xs) Source #
Instance details Defined in Ouroboros.Consensus.HardFork.Combinator.Util.Match Methods noThunks :: Context -> Mismatch f g xs -> IO ( Maybe ThunkInfo ) Source # wNoThunks :: Context -> Mismatch f g xs -> IO ( Maybe ThunkInfo ) Source # showTypeOf :: Proxy ( Mismatch f g xs) -> String Source #
type Prod ( Mismatch f :: (k -> Type ) -> [k] -> Type ) Source #
Instance details Defined in Ouroboros.Consensus.HardFork.Combinator.Util.Match type Prod ( Mismatch f :: (k -> Type ) -> [k] -> Type ) = NP :: (k -> Type ) -> [k] -> Type
type SListIN ( Mismatch f :: (k -> Type ) -> [k] -> Type ) Source #
Instance details Defined in Ouroboros.Consensus.HardFork.Combinator.Util.Match type SListIN ( Mismatch f :: (k -> Type ) -> [k] -> Type ) = SListI :: [k] -> Constraint
type AllN ( Mismatch f :: (k -> Type ) -> [k] -> Type ) (c :: k -> Constraint ) Source #
Instance details Defined in Ouroboros.Consensus.HardFork.Combinator.Util.Match type AllN ( Mismatch f :: (k -> Type ) -> [k] -> Type ) (c :: k -> Constraint ) = All c

flip :: Mismatch f g xs -> Mismatch g f xs Source #

matchNS :: NS f xs -> NS g xs -> Either ( Mismatch f g xs) ( NS ( Product f g) xs) Source #

matchTelescope :: NS h xs -> Telescope g f xs -> Either ( Mismatch h f xs) ( Telescope g ( Product h f) xs) Source #

Utilities

mismatchNotEmpty :: Mismatch f g xs -> ( forall x xs'. xs ~ (x ': xs') => Mismatch f g (x ': xs') -> a) -> a Source #

mismatchNotFirst :: Mismatch f g (x ': xs) -> Either ( NS f xs) ( NS g xs) Source #

mismatchOne :: Mismatch f g '[x] -> Void Source #

We cannot give a mismatch if we have only one type variable

mismatchToNS :: Mismatch f g xs -> ( NS f xs, NS g xs) Source #

Project two NS from a Mismatch

We should have the property that

uncurry matchNS (mismatchToNS m) == Left m

mismatchTwo :: Mismatch f g '[x, y] -> Either (f x, g y) (f y, g x) Source #

If we only have two eras, only two possibilities for a mismatch

mkMismatchTwo :: Either (f x, g y) (f y, g x) -> Mismatch f g '[x, y] Source #

mustMatchNS :: forall f g xs. HasCallStack => String -> NS f xs -> NS g xs -> NS ( Product f g) xs Source #

Variant of matchNS for when we know the two NS s must match. Otherwise an error, mentioning the given String , is thrown.

SOP operators

bihap :: NP (f -.-> f') xs -> NP (g -.-> g') xs -> Mismatch f g xs -> Mismatch f' g' xs Source #

bihcmap :: All c xs => proxy c -> ( forall x. c x => f x -> f' x) -> ( forall x. c x => g x -> g' x) -> Mismatch f g xs -> Mismatch f' g' xs Source #

Bifunctor analogue of hcmap

bihmap :: SListI xs => ( forall x. f x -> f' x) -> ( forall x. g x -> g' x) -> Mismatch f g xs -> Mismatch f' g' xs Source #