{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Test.Cardano.Ledger.Conformance.SpecTranslate.Dijkstra.Pool () where

import Cardano.Ledger.BaseTypes (Network)
import Cardano.Ledger.Compactible (fromCompact)
import Cardano.Ledger.Core
import Cardano.Ledger.Dijkstra (DijkstraEra)
import Cardano.Ledger.State
import Data.Bitraversable (bimapM)
import qualified Data.Map.Strict as Map
import qualified MAlonzo.Code.Ledger.Dijkstra.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance.SpecTranslate.Base (
  SpecTranslate (..),
  toSpecRepMap,
  withCtxSpecTransM,
 )
import Test.Cardano.Ledger.Conformance.SpecTranslate.Dijkstra.Base ()

instance SpecTranslate DijkstraEra (PState DijkstraEra) where
  type SpecRep DijkstraEra (PState DijkstraEra) = Agda.PState

  type SpecContext DijkstraEra (PState DijkstraEra) = Network

  toSpecRep :: PState DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (PState DijkstraEra))
     (SpecRep DijkstraEra (PState DijkstraEra))
toSpecRep PState {Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
Map (KeyHash StakePool) (StakePoolParams DijkstraEra)
Map (KeyHash StakePool) StakePoolState
Map (KeyHash StakePool) EpochNo
Set BlsVerKeyHash
psVRFKeyHashes :: Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
psStakePools :: Map (KeyHash StakePool) StakePoolState
psFutureStakePoolParams :: Map (KeyHash StakePool) (StakePoolParams DijkstraEra)
psRetiring :: Map (KeyHash StakePool) EpochNo
psBlsKeyHashes :: Set BlsVerKeyHash
psBlsKeyHashes :: forall era. PState era -> Set BlsVerKeyHash
psFutureStakePoolParams :: forall era.
PState era -> Map (KeyHash StakePool) (StakePoolParams era)
psRetiring :: forall era. PState era -> Map (KeyHash StakePool) EpochNo
psStakePools :: forall era. PState era -> Map (KeyHash StakePool) StakePoolState
psVRFKeyHashes :: forall era.
PState era -> Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
..} = do
    stakePools <-
      ([(Integer, StakePoolState)] -> HSMap Integer StakePoolState)
-> SpecTransM DijkstraEra Network [(Integer, StakePoolState)]
-> SpecTransM DijkstraEra Network (HSMap Integer StakePoolState)
forall a b.
(a -> b)
-> SpecTransM DijkstraEra Network a
-> SpecTransM DijkstraEra Network b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(Integer, StakePoolState)] -> HSMap Integer StakePoolState
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap (SpecTransM DijkstraEra Network [(Integer, StakePoolState)]
 -> SpecTransM DijkstraEra Network (HSMap Integer StakePoolState))
-> (Map (KeyHash StakePool) StakePoolState
    -> SpecTransM DijkstraEra Network [(Integer, StakePoolState)])
-> Map (KeyHash StakePool) StakePoolState
-> SpecTransM DijkstraEra Network (HSMap Integer StakePoolState)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((KeyHash StakePool, StakePoolState)
 -> SpecTransM DijkstraEra Network (Integer, StakePoolState))
-> [(KeyHash StakePool, StakePoolState)]
-> SpecTransM DijkstraEra Network [(Integer, StakePoolState)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ((KeyHash StakePool -> SpecTransM DijkstraEra Network Integer)
-> (StakePoolState
    -> SpecTransM DijkstraEra Network StakePoolState)
-> (KeyHash StakePool, StakePoolState)
-> SpecTransM DijkstraEra Network (Integer, StakePoolState)
forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bimapM (()
-> SpecTransM DijkstraEra () Integer
-> SpecTransM DijkstraEra Network Integer
forall ctx era a ctx'.
ctx -> SpecTransM era ctx a -> SpecTransM era ctx' a
withCtxSpecTransM () (SpecTransM DijkstraEra () Integer
 -> SpecTransM DijkstraEra Network Integer)
-> (KeyHash StakePool -> SpecTransM DijkstraEra () Integer)
-> KeyHash StakePool
-> SpecTransM DijkstraEra Network Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. KeyHash StakePool -> SpecTransM DijkstraEra () Integer
KeyHash StakePool
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (KeyHash StakePool))
     (SpecRep DijkstraEra (KeyHash StakePool))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep) StakePoolState -> SpecTransM DijkstraEra Network StakePoolState
StakePoolState
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra StakePoolState)
     (SpecRep DijkstraEra StakePoolState)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep) ([(KeyHash StakePool, StakePoolState)]
 -> SpecTransM DijkstraEra Network [(Integer, StakePoolState)])
-> (Map (KeyHash StakePool) StakePoolState
    -> [(KeyHash StakePool, StakePoolState)])
-> Map (KeyHash StakePool) StakePoolState
-> SpecTransM DijkstraEra Network [(Integer, StakePoolState)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (KeyHash StakePool) StakePoolState
-> [(KeyHash StakePool, StakePoolState)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map (KeyHash StakePool) StakePoolState
 -> SpecTransM DijkstraEra Network (HSMap Integer StakePoolState))
-> Map (KeyHash StakePool) StakePoolState
-> SpecTransM DijkstraEra Network (HSMap Integer StakePoolState)
forall a b. (a -> b) -> a -> b
$
        Map (KeyHash StakePool) StakePoolState
psStakePools
    withCtxSpecTransM () $
      Agda.MkPState stakePools
        <$> toSpecRepMap psFutureStakePoolParams
        <*> toSpecRepMap psRetiring
        <*> toSpecRepMap (fromCompact . spsDeposit <$> psStakePools)

instance SpecTranslate DijkstraEra (PoolCert DijkstraEra) where
  type SpecRep DijkstraEra (PoolCert DijkstraEra) = Agda.DCert

  toSpecRep :: PoolCert DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (PoolCert DijkstraEra))
     (SpecRep DijkstraEra (PoolCert DijkstraEra))
toSpecRep (RegPool p :: StakePoolParams DijkstraEra
p@StakePoolParams {sppId :: forall era. StakePoolParams era -> KeyHash StakePool
sppId = KeyHash Hash ADDRHASH (VerKeyDSIGN DSIGN)
ppHash}) =
    Integer -> StakePoolParams -> DCert
Agda.Regpool
      (Integer -> StakePoolParams -> DCert)
-> SpecTransM DijkstraEra () Integer
-> SpecTransM DijkstraEra () (StakePoolParams -> DCert)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Hash ADDRHASH (VerKeyDSIGN DSIGN)
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (Hash ADDRHASH (VerKeyDSIGN DSIGN)))
     (SpecRep DijkstraEra (Hash ADDRHASH (VerKeyDSIGN DSIGN)))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Hash ADDRHASH (VerKeyDSIGN DSIGN)
ppHash
      SpecTransM DijkstraEra () (StakePoolParams -> DCert)
-> SpecTransM DijkstraEra () StakePoolParams
-> SpecTransM DijkstraEra () DCert
forall a b.
SpecTransM DijkstraEra () (a -> b)
-> SpecTransM DijkstraEra () a -> SpecTransM DijkstraEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StakePoolParams DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (StakePoolParams DijkstraEra))
     (SpecRep DijkstraEra (StakePoolParams DijkstraEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep StakePoolParams DijkstraEra
p
  toSpecRep (RetirePool (KeyHash Hash ADDRHASH (VerKeyDSIGN DSIGN)
ppHash) EpochNo
e) =
    Integer -> Integer -> DCert
Agda.Retirepool
      (Integer -> Integer -> DCert)
-> SpecTransM DijkstraEra () Integer
-> SpecTransM DijkstraEra () (Integer -> DCert)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Hash ADDRHASH (VerKeyDSIGN DSIGN)
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (Hash ADDRHASH (VerKeyDSIGN DSIGN)))
     (SpecRep DijkstraEra (Hash ADDRHASH (VerKeyDSIGN DSIGN)))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Hash ADDRHASH (VerKeyDSIGN DSIGN)
ppHash
      SpecTransM DijkstraEra () (Integer -> DCert)
-> SpecTransM DijkstraEra () Integer
-> SpecTransM DijkstraEra () DCert
forall a b.
SpecTransM DijkstraEra () (a -> b)
-> SpecTransM DijkstraEra () a -> SpecTransM DijkstraEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> EpochNo
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra EpochNo)
     (SpecRep DijkstraEra EpochNo)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep EpochNo
e