{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module Ouroboros.Consensus.HardFork.Combinator.State.Instances (
decodeCurrent
, decodePast
, encodeCurrent
, encodePast
) where
import Cardano.Binary (enforceSize)
import Codec.CBOR.Decoding (Decoder)
import Codec.CBOR.Encoding (Encoding, encodeListLen)
import Codec.Serialise
import Data.Coerce
import Data.Proxy
import Data.SOP.BasicFunctors
import Data.SOP.Constraint
import Data.SOP.Strict
import qualified Data.SOP.Telescope as Telescope
import NoThunks.Class (NoThunks)
import Ouroboros.Consensus.HardFork.Combinator.Abstract.SingleEraBlock
import Ouroboros.Consensus.HardFork.Combinator.Lifting
import Ouroboros.Consensus.HardFork.Combinator.State.Lift
import Ouroboros.Consensus.HardFork.Combinator.State.Types
import Prelude hiding (sequence)
type instance Prod HardForkState = NP
type instance SListIN HardForkState = SListI
type instance AllN HardForkState c = All c
type instance CollapseTo HardForkState a = a
instance HAp HardForkState where
hap :: forall (f :: * -> *) (g :: * -> *) (xs :: [*]).
Prod HardForkState (f -.-> g) xs
-> HardForkState f xs -> HardForkState g xs
hap Prod HardForkState (f -.-> g) xs
np (HardForkState Telescope (K Past) (Current f) xs
st) = Telescope (K Past) (Current g) xs -> HardForkState g xs
forall (f :: * -> *) (xs :: [*]).
Telescope (K Past) (Current f) xs -> HardForkState f xs
HardForkState (Telescope (K Past) (Current g) xs -> HardForkState g xs)
-> Telescope (K Past) (Current g) xs -> HardForkState g xs
forall a b. (a -> b) -> a -> b
$
Prod (Telescope (K Past)) (Current f -.-> Current g) xs
-> Telescope (K Past) (Current f) xs
-> Telescope (K Past) (Current g) xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
(xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
forall (f :: * -> *) (g :: * -> *) (xs :: [*]).
Prod (Telescope (K Past)) (f -.-> g) xs
-> Telescope (K Past) f xs -> Telescope (K Past) g xs
hap ((forall a. (-.->) f g a -> (-.->) (Current f) (Current g) a)
-> NP (f -.-> g) xs -> NP (Current f -.-> Current g) xs
forall {k} (f :: k -> *) (g :: k -> *) (xs :: [k]).
(forall (a :: k). f a -> g a) -> NP f xs -> NP g xs
map_NP' ((Current f a -> Current g a) -> (-.->) (Current f) (Current g) a
forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
(f a -> g a) -> (-.->) f g a
Fn ((Current f a -> Current g a) -> (-.->) (Current f) (Current g) a)
-> ((-.->) f g a -> Current f a -> Current g a)
-> (-.->) f g a
-> (-.->) (Current f) (Current g) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f a -> g a) -> Current f a -> Current g a
forall (f :: * -> *) blk (f' :: * -> *).
(f blk -> f' blk) -> Current f blk -> Current f' blk
lift ((f a -> g a) -> Current f a -> Current g a)
-> ((-.->) f g a -> f a -> g a)
-> (-.->) f g a
-> Current f a
-> Current g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (-.->) f g a -> f a -> g a
forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
(-.->) f g a -> f a -> g a
apFn) Prod HardForkState (f -.-> g) xs
NP (f -.-> g) xs
np) Telescope (K Past) (Current f) xs
st
instance HSequence HardForkState where
hctraverse' :: forall (c :: * -> Constraint) (xs :: [*]) (g :: * -> *)
(proxy :: (* -> Constraint) -> *) (f :: * -> *) (f' :: * -> *).
(AllN HardForkState c xs, Applicative g) =>
proxy c
-> (forall a. c a => f a -> g (f' a))
-> HardForkState f xs
-> g (HardForkState f' xs)
hctraverse' = \proxy c
p forall a. c a => f a -> g (f' a)
f (HardForkState Telescope (K Past) (Current f) xs
st) -> Telescope (K Past) (Current f') xs -> HardForkState f' xs
forall (f :: * -> *) (xs :: [*]).
Telescope (K Past) (Current f) xs -> HardForkState f xs
HardForkState (Telescope (K Past) (Current f') xs -> HardForkState f' xs)
-> g (Telescope (K Past) (Current f') xs)
-> g (HardForkState f' xs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
proxy c
-> (forall a. c a => Current f a -> g (Current f' a))
-> Telescope (K Past) (Current f) xs
-> g (Telescope (K Past) (Current f') xs)
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
(xs :: l) (g :: * -> *) (proxy :: (k -> Constraint) -> *)
(f :: k -> *) (f' :: k -> *).
(HSequence h, AllN h c xs, Applicative g) =>
proxy c
-> (forall (a :: k). c a => f a -> g (f' a))
-> h f xs
-> g (h f' xs)
forall (c :: * -> Constraint) (xs :: [*]) (g :: * -> *)
(proxy :: (* -> Constraint) -> *) (f :: * -> *) (f' :: * -> *).
(AllN (Telescope (K Past)) c xs, Applicative g) =>
proxy c
-> (forall a. c a => f a -> g (f' a))
-> Telescope (K Past) f xs
-> g (Telescope (K Past) f' xs)
hctraverse' proxy c
p ((f a -> g (f' a)) -> Current f a -> g (Current f' a)
forall (m :: * -> *) (f :: * -> *) blk (f' :: * -> *).
Functor m =>
(f blk -> m (f' blk)) -> Current f blk -> m (Current f' blk)
liftM f a -> g (f' a)
forall a. c a => f a -> g (f' a)
f) Telescope (K Past) (Current f) xs
st
htraverse' :: forall (xs :: [*]) (g :: * -> *) (f :: * -> *) (f' :: * -> *).
(SListIN HardForkState xs, Applicative g) =>
(forall a. f a -> g (f' a))
-> HardForkState f xs -> g (HardForkState f' xs)
htraverse' = Proxy Top
-> (forall a. Top a => f a -> g (f' a))
-> HardForkState f xs
-> g (HardForkState f' xs)
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
(xs :: l) (g :: * -> *) (proxy :: (k -> Constraint) -> *)
(f :: k -> *) (f' :: k -> *).
(HSequence h, AllN h c xs, Applicative g) =>
proxy c
-> (forall (a :: k). c a => f a -> g (f' a))
-> h f xs
-> g (h f' xs)
forall (c :: * -> Constraint) (xs :: [*]) (g :: * -> *)
(proxy :: (* -> Constraint) -> *) (f :: * -> *) (f' :: * -> *).
(AllN HardForkState c xs, Applicative g) =>
proxy c
-> (forall a. c a => f a -> g (f' a))
-> HardForkState f xs
-> g (HardForkState f' xs)
hctraverse' (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @Top)
hsequence' :: forall (xs :: [*]) (f :: * -> *) (g :: * -> *).
(SListIN HardForkState xs, Applicative f) =>
HardForkState (f :.: g) xs -> f (HardForkState g xs)
hsequence' = (forall a. (:.:) f g a -> f (g a))
-> HardForkState (f :.: g) xs -> f (HardForkState g xs)
forall (xs :: [*]) (g :: * -> *) (f :: * -> *) (f' :: * -> *).
(SListIN HardForkState xs, Applicative g) =>
(forall a. f a -> g (f' a))
-> HardForkState f xs -> g (HardForkState f' xs)
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (g :: * -> *)
(f :: k -> *) (f' :: k -> *).
(HSequence h, SListIN h xs, Applicative g) =>
(forall (a :: k). f a -> g (f' a)) -> h f xs -> g (h f' xs)
htraverse' (:.:) f g a -> f (g a)
forall a. (:.:) f g a -> f (g a)
forall {l} {k} (f :: l -> *) (g :: k -> l) (p :: k).
(:.:) f g p -> f (g p)
unComp
instance HCollapse HardForkState where
hcollapse :: forall (xs :: [*]) a.
SListIN HardForkState xs =>
HardForkState (K a) xs -> CollapseTo HardForkState a
hcollapse = NS (K a) xs -> a
NS (K a) xs -> CollapseTo NS a
forall (xs :: [*]) a.
SListIN NS xs =>
NS (K a) xs -> CollapseTo NS a
forall k l (h :: (k -> *) -> l -> *) (xs :: l) a.
(HCollapse h, SListIN h xs) =>
h (K a) xs -> CollapseTo h a
hcollapse (NS (K a) xs -> a)
-> (HardForkState (K a) xs -> NS (K a) xs)
-> HardForkState (K a) xs
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Current (K a) a -> K a a)
-> NS (Current (K a)) xs -> NS (K a) xs
forall {k} {l} (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
(f' :: k -> *).
(SListIN (Prod h) xs, HAp h) =>
(forall (a :: k). f a -> f' a) -> h f xs -> h f' xs
hmap Current (K a) a -> K a a
forall a. Current (K a) a -> K a a
forall (f :: * -> *) blk. Current f blk -> f blk
currentState (NS (Current (K a)) xs -> NS (K a) xs)
-> (HardForkState (K a) xs -> NS (Current (K a)) xs)
-> HardForkState (K a) xs
-> NS (K a) xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope (K Past) (Current (K a)) xs -> NS (Current (K a)) xs
forall {k} (g :: k -> *) (f :: k -> *) (xs :: [k]).
Telescope g f xs -> NS f xs
Telescope.tip (Telescope (K Past) (Current (K a)) xs -> NS (Current (K a)) xs)
-> (HardForkState (K a) xs
-> Telescope (K Past) (Current (K a)) xs)
-> HardForkState (K a) xs
-> NS (Current (K a)) xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HardForkState (K a) xs -> Telescope (K Past) (Current (K a)) xs
forall (f :: * -> *) (xs :: [*]).
HardForkState f xs -> Telescope (K Past) (Current f) xs
getHardForkState
instance HTrans HardForkState HardForkState where
htrans :: forall (c :: * -> * -> Constraint) (xs :: [*]) (ys :: [*])
(proxy :: (* -> * -> Constraint) -> *) (f :: * -> *) (g :: * -> *).
AllZipN (Prod HardForkState) c xs ys =>
proxy c
-> (forall x y. c x y => f x -> g y)
-> HardForkState f xs
-> HardForkState g ys
htrans proxy c
p forall x y. c x y => f x -> g y
t (HardForkState Telescope (K Past) (Current f) xs
st) = Telescope (K Past) (Current g) ys -> HardForkState g ys
forall (f :: * -> *) (xs :: [*]).
Telescope (K Past) (Current f) xs -> HardForkState f xs
HardForkState (Telescope (K Past) (Current g) ys -> HardForkState g ys)
-> Telescope (K Past) (Current g) ys -> HardForkState g ys
forall a b. (a -> b) -> a -> b
$
proxy c
-> (forall x y. c x y => Current f x -> Current g y)
-> Telescope (K Past) (Current f) xs
-> Telescope (K Past) (Current g) ys
forall k1 l1 k2 l2 (h1 :: (k1 -> *) -> l1 -> *)
(h2 :: (k2 -> *) -> l2 -> *) (c :: k1 -> k2 -> Constraint)
(xs :: l1) (ys :: l2) (proxy :: (k1 -> k2 -> Constraint) -> *)
(f :: k1 -> *) (g :: k2 -> *).
(HTrans h1 h2, AllZipN (Prod h1) c xs ys) =>
proxy c
-> (forall (x :: k1) (y :: k2). c x y => f x -> g y)
-> h1 f xs
-> h2 g ys
forall (c :: * -> * -> Constraint) (xs :: [*]) (ys :: [*])
(proxy :: (* -> * -> Constraint) -> *) (f :: * -> *) (g :: * -> *).
AllZipN (Prod (Telescope (K Past))) c xs ys =>
proxy c
-> (forall x y. c x y => f x -> g y)
-> Telescope (K Past) f xs
-> Telescope (K Past) g ys
htrans proxy c
p (\(Current Bound
b f x
fx) -> Bound -> g y -> Current g y
forall (f :: * -> *) blk. Bound -> f blk -> Current f blk
Current Bound
b (g y -> Current g y) -> g y -> Current g y
forall a b. (a -> b) -> a -> b
$ f x -> g y
forall x y. c x y => f x -> g y
t f x
fx) Telescope (K Past) (Current f) xs
st
hcoerce ::
forall f g xs ys. AllZipN (Prod HardForkState) (LiftedCoercible f g) xs ys
=> HardForkState f xs
-> HardForkState g ys
hcoerce :: forall (f :: * -> *) (g :: * -> *) (xs :: [*]) (ys :: [*]).
AllZipN (Prod HardForkState) (LiftedCoercible f g) xs ys =>
HardForkState f xs -> HardForkState g ys
hcoerce (HardForkState Telescope (K Past) (Current f) xs
st) = Telescope (K Past) (Current g) ys -> HardForkState g ys
forall (f :: * -> *) (xs :: [*]).
Telescope (K Past) (Current f) xs -> HardForkState f xs
HardForkState (Telescope (K Past) (Current g) ys -> HardForkState g ys)
-> Telescope (K Past) (Current g) ys -> HardForkState g ys
forall a b. (a -> b) -> a -> b
$
Proxy (LiftedCoercible f g)
-> (forall x y.
LiftedCoercible f g x y =>
Current f x -> Current g y)
-> Telescope (K Past) (Current f) xs
-> Telescope (K Past) (Current g) ys
forall k1 l1 k2 l2 (h1 :: (k1 -> *) -> l1 -> *)
(h2 :: (k2 -> *) -> l2 -> *) (c :: k1 -> k2 -> Constraint)
(xs :: l1) (ys :: l2) (proxy :: (k1 -> k2 -> Constraint) -> *)
(f :: k1 -> *) (g :: k2 -> *).
(HTrans h1 h2, AllZipN (Prod h1) c xs ys) =>
proxy c
-> (forall (x :: k1) (y :: k2). c x y => f x -> g y)
-> h1 f xs
-> h2 g ys
forall (c :: * -> * -> Constraint) (xs :: [*]) (ys :: [*])
(proxy :: (* -> * -> Constraint) -> *) (f :: * -> *) (g :: * -> *).
AllZipN (Prod (Telescope (K Past))) c xs ys =>
proxy c
-> (forall x y. c x y => f x -> g y)
-> Telescope (K Past) f xs
-> Telescope (K Past) g ys
htrans
(forall {k} (t :: k). Proxy t
forall (t :: * -> * -> Constraint). Proxy t
Proxy @(LiftedCoercible f g))
(\(Current Bound
b f x
fx) -> Bound -> g y -> Current g y
forall (f :: * -> *) blk. Bound -> f blk -> Current f blk
Current Bound
b (g y -> Current g y) -> g y -> Current g y
forall a b. (a -> b) -> a -> b
$ f x -> g y
forall a b. Coercible a b => a -> b
coerce f x
fx)
Telescope (K Past) (Current f) xs
st
type instance Same HardForkState = HardForkState
deriving instance Eq (f blk) => Eq (Current f blk)
deriving instance Show (f blk) => Show (Current f blk)
deriving instance NoThunks (f blk) => NoThunks (Current f blk)
deriving via LiftTelescope (K Past) (Current f) xs
instance ( All SingleEraBlock xs
, forall blk. SingleEraBlock blk => Show (f blk)
) => Show (HardForkState f xs)
deriving via LiftTelescope (K Past) (Current f) xs
instance ( All SingleEraBlock xs
, forall blk. SingleEraBlock blk => Eq (f blk)
) => Eq (HardForkState f xs)
deriving via LiftNamedTelescope "HardForkState" (K Past) (Current f) xs
instance ( All SingleEraBlock xs
, forall blk. SingleEraBlock blk => NoThunks (f blk)
) => NoThunks (HardForkState f xs)
encodeCurrent :: (f blk -> Encoding) -> Current f blk -> Encoding
encodeCurrent :: forall (f :: * -> *) blk.
(f blk -> Encoding) -> Current f blk -> Encoding
encodeCurrent f blk -> Encoding
f Current{f blk
Bound
currentState :: forall (f :: * -> *) blk. Current f blk -> f blk
currentStart :: Bound
currentState :: f blk
currentStart :: forall (f :: * -> *) blk. Current f blk -> Bound
..} = [Encoding] -> Encoding
forall a. Monoid a => [a] -> a
mconcat [
Word -> Encoding
encodeListLen Word
2
, Bound -> Encoding
forall a. Serialise a => a -> Encoding
encode Bound
currentStart
, f blk -> Encoding
f f blk
currentState
]
decodeCurrent :: Decoder s (f blk) -> Decoder s (Current f blk)
decodeCurrent :: forall s (f :: * -> *) blk.
Decoder s (f blk) -> Decoder s (Current f blk)
decodeCurrent Decoder s (f blk)
f = do
Text -> Int -> Decoder s ()
forall s. Text -> Int -> Decoder s ()
enforceSize Text
"decodeCurrent" Int
2
Bound
currentStart <- Decoder s Bound
forall s. Decoder s Bound
forall a s. Serialise a => Decoder s a
decode
f blk
currentState <- Decoder s (f blk)
f
Current f blk -> Decoder s (Current f blk)
forall a. a -> Decoder s a
forall (m :: * -> *) a. Monad m => a -> m a
return Current{f blk
Bound
currentState :: f blk
currentStart :: Bound
currentStart :: Bound
currentState :: f blk
..}
encodePast :: Past -> Encoding
encodePast :: Past -> Encoding
encodePast Past{Bound
pastStart :: Bound
pastEnd :: Bound
pastStart :: Past -> Bound
pastEnd :: Past -> Bound
..} = [Encoding] -> Encoding
forall a. Monoid a => [a] -> a
mconcat [
Word -> Encoding
encodeListLen Word
2
, Bound -> Encoding
forall a. Serialise a => a -> Encoding
encode Bound
pastStart
, Bound -> Encoding
forall a. Serialise a => a -> Encoding
encode Bound
pastEnd
]
decodePast :: Decoder s Past
decodePast :: forall s. Decoder s Past
decodePast = do
Text -> Int -> Decoder s ()
forall s. Text -> Int -> Decoder s ()
enforceSize Text
"decodePast" Int
2
Bound
pastStart <- Decoder s Bound
forall s. Decoder s Bound
forall a s. Serialise a => Decoder s a
decode
Bound
pastEnd <- Decoder s Bound
forall s. Decoder s Bound
forall a s. Serialise a => Decoder s a
decode
Past -> Decoder s Past
forall a. a -> Decoder s a
forall (m :: * -> *) a. Monad m => a -> m a
return Past{Bound
pastStart :: Bound
pastEnd :: Bound
pastStart :: Bound
pastEnd :: Bound
..}
instance Serialise (f blk) => Serialise (Current f blk) where
encode :: Current f blk -> Encoding
encode = (f blk -> Encoding) -> Current f blk -> Encoding
forall (f :: * -> *) blk.
(f blk -> Encoding) -> Current f blk -> Encoding
encodeCurrent f blk -> Encoding
forall a. Serialise a => a -> Encoding
encode
decode :: forall s. Decoder s (Current f blk)
decode = Decoder s (f blk) -> Decoder s (Current f blk)
forall s (f :: * -> *) blk.
Decoder s (f blk) -> Decoder s (Current f blk)
decodeCurrent Decoder s (f blk)
forall s. Decoder s (f blk)
forall a s. Serialise a => Decoder s a
decode
instance Serialise Past where
encode :: Past -> Encoding
encode = Past -> Encoding
encodePast
decode :: forall s. Decoder s Past
decode = Decoder s Past
forall s. Decoder s Past
decodePast