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

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

import qualified Cardano.Ledger.Conway.Rules as Conway
import Cardano.Ledger.Dijkstra (DijkstraEra)
import qualified MAlonzo.Code.Ledger.Dijkstra.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance.SpecTranslate.Base
import Test.Cardano.Ledger.Conformance.SpecTranslate.Dijkstra.Base ()
import Test.Cardano.Ledger.Conformance.SpecTranslate.Dijkstra.Cert ()

instance SpecTranslate DijkstraEra (Conway.GovSignal DijkstraEra) where
  type SpecRep DijkstraEra (Conway.GovSignal DijkstraEra) = [Either Agda.GovVote Agda.GovProposal]

  toSpecRep :: GovSignal DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (GovSignal DijkstraEra))
     (SpecRep DijkstraEra (GovSignal DijkstraEra))
toSpecRep Conway.GovSignal {VotingProcedures DijkstraEra
gsVotingProcedures :: VotingProcedures DijkstraEra
gsVotingProcedures :: forall era. GovSignal era -> VotingProcedures era
gsVotingProcedures, OSet (ProposalProcedure DijkstraEra)
gsProposalProcedures :: OSet (ProposalProcedure DijkstraEra)
gsProposalProcedures :: forall era. GovSignal era -> OSet (ProposalProcedure era)
gsProposalProcedures} = do
    votingProcedures <- VotingProcedures DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (VotingProcedures DijkstraEra))
     (SpecRep DijkstraEra (VotingProcedures DijkstraEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep VotingProcedures DijkstraEra
gsVotingProcedures
    proposalProcedures <- toSpecRep gsProposalProcedures
    pure $
      mconcat
        [ Left <$> votingProcedures
        , Right <$> proposalProcedures
        ]