{-# 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
  ( -- * Serialisation support
    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)

{-------------------------------------------------------------------------------
  SOP class instances

  These are convenient, allowing us to treat the 'HardForkState' just like any
  other SOP type; in particular, they deal with lifting functions to 'Current'.
-------------------------------------------------------------------------------}

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

{-------------------------------------------------------------------------------
  Eq, Show, NoThunks
-------------------------------------------------------------------------------}

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)

{-------------------------------------------------------------------------------
  Serialisation

  The 'Serialise' instances are primarily useful for the tests, but the general
  encoders/decoders are used by the HFC to store the ledger state.
-------------------------------------------------------------------------------}

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
  currentStart <- Decoder s Bound
forall s. Decoder s Bound
forall a s. Serialise a => Decoder s a
decode
  currentState <- f
  return Current{..}

encodePast :: Past -> Encoding
encodePast :: Past -> Encoding
encodePast Past{Bound
pastStart :: Bound
pastEnd :: Bound
pastEnd :: Past -> Bound
pastStart :: 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
  pastStart <- Decoder s Bound
forall s. Decoder s Bound
forall a s. Serialise a => Decoder s a
decode
  pastEnd <- decode
  return Past{..}

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