{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# 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 qualified Data.Map.Strict as Map
import qualified MAlonzo.Code.Ledger.Dijkstra.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance.SpecTranslate.Base (
  SpecTranslate (..),
  askSpecTransM,
  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 (KeyHash StakePool) StakePoolParams
Map (KeyHash StakePool) StakePoolState
Map (KeyHash StakePool) EpochNo
Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
psVRFKeyHashes :: Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
psStakePools :: Map (KeyHash StakePool) StakePoolState
psFutureStakePoolParams :: Map (KeyHash StakePool) StakePoolParams
psRetiring :: Map (KeyHash StakePool) EpochNo
psFutureStakePoolParams :: forall era. PState era -> Map (KeyHash StakePool) StakePoolParams
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
    netId <- SpecTransM DijkstraEra Network Network
forall era ctx. SpecTransM era ctx ctx
askSpecTransM
    withCtxSpecTransM () $
      Agda.MkPState
        <$> toSpecRepMap (Map.mapWithKey (stakePoolStateToStakePoolParams netId) psStakePools)
        <*> toSpecRepMap psFutureStakePoolParams
        <*> toSpecRepMap psRetiring
        <*> toSpecRepMap (fromCompact . spsDeposit <$> psStakePools)

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

  toSpecRep :: PoolCert
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra PoolCert)
     (SpecRep DijkstraEra PoolCert)
toSpecRep (RegPool p :: StakePoolParams
p@StakePoolParams {sppId :: StakePoolParams -> 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
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra StakePoolParams)
     (SpecRep DijkstraEra StakePoolParams)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep StakePoolParams
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