module Ledger.Conway.Foreign.Ratify where

open import Data.String.Base renaming (_++_ to _+ˢ_) hiding (show; length)
import Data.Rational.Show as Rational
open import Foreign.Convertible 
open import Foreign.Convertible.Deriving
open import Foreign.Haskell
open import Foreign.Haskell.Coerce
open import Foreign.HaskellTypes
open import Foreign.HaskellTypes.Deriving

open import Ledger.Prelude
open import Ledger.Prelude.Foreign.HSTypes

open import Ledger.Core.Foreign.Address
open import Ledger.Conway.Foreign.HSStructures
open import Ledger.Conway.Foreign.Certs
open import Ledger.Conway.Foreign.Enact
open import Ledger.Conway.Foreign.Gov.Core
open import Ledger.Conway.Foreign.Gov
open import Ledger.Conway.Specification.Enact govStructure
open import Ledger.Conway.Specification.Ratify govStructure
  hiding (acceptedByCC; acceptedByDRep; acceptedBySPO)
import Ledger.Conway.Specification.Ratify govStructure as Ratify
open import Ledger.Conway.Specification.Ratify.Properties.Computational it

open Computational

instance
  HsTy-StakeDistrs = autoHsType StakeDistrs
  Conv-StakeDistrs = autoConvert StakeDistrs

  HsTy-RatifyEnv = autoHsType RatifyEnv ⊣ withConstructor "MkRatifyEnv"
                                        • fieldPrefix "re"
  Conv-RatifyEnv = autoConvert RatifyEnv

  HsTy-RatifyState = autoHsType RatifyState ⊣ withConstructor "MkRatifyState"
                                            • fieldPrefix "rs"
                                            • RatifyState.es ↦ "rsEnactState"
  Conv-RatifyState = autoConvert RatifyState

-- ratify-debug : HsType (RatifyEnv → RatifyState → List (GovActionID × GovActionState) → String)
-- ratify-debug env st sig =
--   "Number of govactions: " +ˢ show (length sig) +ˢ "\n" +ˢ
--   foldr (λ x s → s +ˢ govActionInfo x) "" sig
--   where
--     open RatifyEnv (from env)
--     govActionInfo : HsType (GovActionID × GovActionState) → String
--     govActionInfo (gaId F., gas) =
--       let
--         open GovActionState (from gas)
--         open RatifyState (from st)
--         open EnactState es
--         votes'  = actualVotes (from env) (proj₁ pparams) (proj₁ cc) (action .gaType) votes
--         showAcceptedStakeRatio role = Rational.show (acceptedStakeRatio role (dom votes') stakeDistrs votes')
--         showIsAccepted role = case acceptedBy? (from env) es (from gas) role of λ where
--           (yes _) → "✓"
--           (no  _) → "×"
--       in
--         "SPO: \t"  +ˢ showAcceptedStakeRatio SPO  +ˢ "\t" +ˢ showIsAccepted SPO  +ˢ "\n" +ˢ
--         "DRep: \t" +ˢ showAcceptedStakeRatio DRep +ˢ "\t" +ˢ showIsAccepted DRep +ˢ "\n" +ˢ
--         "CC: \t"   +ˢ showAcceptedStakeRatio CC   +ˢ "\t" +ˢ showIsAccepted CC   +ˢ "\n"

-- {-# COMPILE GHC ratify-debug as ratifyDebug #-}

ratify-step : HsType (RatifyEnv → RatifyState → List (GovActionID × GovActionState) → ComputationResult ⊥ RatifyState)
ratify-step = to (compute Computational-RATIFIES)

{-# COMPILE GHC ratify-step as ratifyStep #-}

instance
  Show-RATIFIES : ∀ {Γ s sig s'}
    → Show (Γ ⊢ s ⇀⦇ sig  ,RATIFIES⦈ s')
  Show-RATIFIES {Γ} {s} {sig} .show r = "" -- ratify-debug (to Γ) (to s) (to sig)

-- Expose acceptedBy predicates for conformance

acceptedByCC : HsType (RatifyEnv → EnactState → GovActionState → Bool)
acceptedByCC = λ Γ es st → to (does (acceptedByCC? (from Γ) (from es) (from st)))

acceptedByDRep : HsType (RatifyEnv → EnactState → GovActionState → Bool)
acceptedByDRep = λ Γ es st → to (does (acceptedByDRep? (from Γ) (from es) (from st)))

acceptedBySPO : HsType (RatifyEnv → EnactState → GovActionState → Bool)
acceptedBySPO = λ Γ es st → to (does (acceptedBySPO? (from Γ) (from es) (from st)))

{-# COMPILE GHC acceptedByCC as acceptedByCC #-}
{-# COMPILE GHC acceptedByDRep as acceptedByDRep #-}
{-# COMPILE GHC acceptedBySPO as acceptedBySPO #-}