Revert "Made it possible to update PParams (#394)"

This reverts commit ccca650.

src/Ledger/Foreign/HSLedger.agda

@@ -65,7 +65,7 @@ module Implementation where
     }) where open import Algebra.PairOp ℕ zero _≡_ _+_
   _≥ᵉ_ : ExUnits → ExUnits → Set
   _≥ᵉ_ = _≡_
-  CostModel    = ⊤
+  CostModel    = ⊥
   Language     = ⊤
   LangDepView  = ⊤
   Prices       = ⊤
@@ -142,23 +142,16 @@ HSScriptStructure = record
 instance _ = HSScriptStructure
 
 open import Ledger.PParams it it it hiding (PParams)
-open import Axiom.Set.Properties List-Model using (∉-∅)
-
-opaque 
-  unfolding List-Model
-
-  singleton-≢-∅ : ∀ {a} {x : a} → ⦃ DecEq a ⦄ → singleton x ≢ ∅
-  singleton-≢-∅ {x = x} ()
 
 HsGovParams : GovParams
 HsGovParams = record
   { Implementation
   ; ppUpd = let open PParamsDiff in λ where
-      .UpdateT                → ℕ -- cost parameter `a`
-      .updateGroups           → λ _ → ❴ EconomicGroup ❵
-      .applyUpdate            → λ p a → record p { a = a }
-      .ppdWellFormed          → λ _ → true
-      .ppdWellFormed⇒hasGroup → λ _ → singleton-≢-∅
+      .UpdateT                → ⊤
+      .updateGroups           → λ _ → ∅
+      .applyUpdate            → λ p _ → p
+      .ppdWellFormed          → λ _ → false
+      .ppdWellFormed⇒hasGroup → λ ()
       .ppdWellFormed⇒WF       → λ _ _ x → x
   ; ppHashingScheme = it
   }
@@ -262,11 +255,6 @@ instance
   Convertible-DCert : Convertible DCert F.TxCert
   Convertible-DCert = autoConvertible
 
-  Convertible-TxId : Convertible ℕ F.TxId
-  Convertible-TxId = λ where
-    .to x → record { txid = x }
-    .from → F.TxId.txid
-
   Convertible-TxBody : Convertible TxBody F.TxBody
   Convertible-TxBody = λ where
     .to txb → let open TxBody txb in record
@@ -276,7 +264,7 @@ instance
       ; txfee  = txfee
       ; txvldt = to txvldt
       ; txsize = txsize
-      ; txid   = to txid
+      ; txid   = txid
       ; collateral = to collateral
       ; reqSigHash = to reqSigHash
       ; scriptIntHash = nothing
@@ -295,7 +283,7 @@ instance
       ; txADhash   = nothing
       ; netwrk     = nothing
       ; txsize     = txsize
-      ; txid       = from txid
+      ; txid       = txid
       ; txvote     = []
       ; txprop     = []
       ; txdonation = ε
@@ -452,8 +440,8 @@ fromNeedsHash {NewCommittee _ _ _} x = to x
 fromNeedsHash {NewConstitution _ _} x = to x
 fromNeedsHash {TriggerHF _} x = to x
 fromNeedsHash {ChangePParams _} x = to x
-fromNeedsHash {TreasuryWdrl _} x = to 0 F., 0
-fromNeedsHash {Info} x = to 0 F., 0
+fromNeedsHash {TreasuryWdrl _} x = 0 F., 0
+fromNeedsHash {Info} x = 0 F., 0
 
 instance
   Convertible-GovActionState : Convertible GovActionState F.GovActionState

src/Ledger/Foreign/LedgerTypes.agda

@@ -22,6 +22,7 @@ data Empty : Set where
 
 {-# FOREIGN GHC
   data AgdaEmpty deriving (Show, Generic)
+  instance ToExpr AgdaEmpty
 #-}
 
 data ComputationResult E A : Set where
@@ -40,6 +41,8 @@ data ComputationResult E A : Set where
     return = pure
     (Success a) >>= m = m a
     (Failure e) >>= _ = Failure e
+
+  instance (ToExpr e, ToExpr a) => ToExpr (ComputationResult e a)
 #-}
 {-# COMPILE GHC ComputationResult = data ComputationResult (Success | Failure) #-}
 
@@ -49,12 +52,10 @@ HSMap : Set → Set → Set
 HSMap K V = List (Pair K V)
 Rational = Pair ℤ ℕ
 
-record TxId : Set where
-  field txid : ℕ
-
 Coin          = ℕ
 Addr          = ℕ -- just payment credential
 
+TxId          = ℕ
 Ix            = ℕ
 Epoch         = ℕ
 ScriptHash    = ℕ
@@ -65,7 +66,7 @@ Datum         = ⊤
 Redeemer      = ⊤
 Anchor        = ⊤
 Network       = ⊤
-PParamsUpdate = ℕ
+PParamsUpdate = ⊤
 Script        = ⊤
 
 TxIn          = Pair TxId Ix
@@ -93,7 +94,6 @@ ProtVer = Pair ℕ ℕ
   type Ix      = Integer
   type Epoch   = Integer
   type ScriptHash    = Integer
-  type PParamsUpdate = Integer
 
   type AuxiliaryData = ()
   type DataHash      = ()
@@ -109,20 +109,20 @@ ProtVer = Pair ℕ ℕ
   type Hash  = Integer
 
   data Tag     = Spend | Mint | Cert | Rewrd | Vote | Propose deriving (Show, Generic)
+  instance ToExpr Tag
   type RdmrPtr = (Tag, Ix)
   type ExUnits = (Integer, Integer)
   type ProtVer = (Integer, Integer)
   type GovActionID = (TxId, Integer)
-  newtype TxId = MkTxId Integer
 #-}
 {-# COMPILE GHC Tag = data Tag (Spend | Mint | Cert | Rewrd | Vote | Propose) #-}
-{-# COMPILE GHC TxId = data TxId (MkTxId) #-}
 
 {-# FOREIGN GHC
   data Credential
     = ScriptObj Integer
     | KeyHashObj Integer
     deriving (Show, Eq, Generic)
+  instance ToExpr Credential
 #-}
 data Credential : Set where
   ScriptObj  : Hash → Credential
@@ -141,6 +141,7 @@ RwdAddr = Pair Network Credential
     | DRep
     | SPO
     deriving (Show, Eq, Generic)
+  instance ToExpr GovRole
 #-}
 data GovRole : Set where
   CC DRep SPO : GovRole
@@ -152,6 +153,7 @@ data GovRole : Set where
     | AbstainRep
     | NoConfidenceRep
     deriving (Show, Eq, Generic)
+  instance ToExpr VDeleg
 #-}
 data VDeleg : Set where
   CredVoter        : GovRole → Credential →  VDeleg
@@ -169,6 +171,7 @@ data VDeleg : Set where
     | DeRegDRep Credential
     | CCRegHot Credential (Maybe Credential)
     deriving (Show, Eq, Generic)
+  instance ToExpr TxCert
 #-}
 data TxCert : Set where
   Delegate    : Credential → Maybe VDeleg → Maybe Credential → Coin → TxCert
@@ -209,6 +212,7 @@ record TxBody : Set where
     , scriptIntHash :: Maybe Hash
     , txcerts :: [TxCert]
     } deriving (Show, Generic)
+  instance ToExpr TxBody
 #-}
 {-# COMPILE GHC TxBody = data TxBody (MkTxBody) #-}
 
@@ -224,6 +228,7 @@ record TxWitnesses : Set where
     , txdats  :: [(DataHash, Datum)]
     , txrdmrs :: [(RdmrPtr, (Redeemer, ExUnits))]
     } deriving (Show, Generic)
+  instance ToExpr TxWitnesses
 #-}
 {-# COMPILE GHC TxWitnesses = data TxWitnesses (MkTxWitnesses) #-}
 
@@ -237,6 +242,7 @@ record Tx : Set where
     , wits :: TxWitnesses
     , txAD :: Maybe AuxiliaryData
     } deriving (Show, Generic)
+  instance ToExpr Tx
 #-}
 {-# COMPILE GHC Tx = data Tx (MkTx) #-}
 
@@ -259,7 +265,7 @@ record PParams : Set where
         drepActivity        : Epoch
         ccMinSize           : ℕ
         ccMaxTermLength     : ℕ
-        costmdls            : ⊤
+        costmdls            : Empty
         prices              : ⊤
         maxTxExUnits        : ExUnits
         maxBlockExUnits     : ExUnits
@@ -286,13 +292,14 @@ record PParams : Set where
     , drepActivity        :: Epoch
     , ccMinSize           :: Integer
     , ccMaxTermLength     :: Integer
-    , costmdls            :: ()
+    , costmdls            :: AgdaEmpty
     , prices              :: ()
     , maxTxExUnits        :: ExUnits
     , maxBlockExUnits     :: ExUnits
     , coinsPerUTxOWord    :: Coin
     , maxCollateralInputs :: Integer
     } deriving (Show, Generic)
+  instance ToExpr PParams
 #-}
 {-# COMPILE GHC PParams = data PParams (MkPParams) #-}
 
@@ -304,6 +311,7 @@ record UTxOEnv : Set where
     { slot    :: Integer
     , pparams :: PParams
     } deriving (Show, Generic)
+  instance ToExpr UTxOEnv
 #-}
 {-# COMPILE GHC UTxOEnv = data UTxOEnv (MkUTxOEnv) #-}
 
@@ -315,6 +323,7 @@ record UTxOState : Set where
     { utxo :: UTxO
     , fees :: Coin
     } deriving (Show, Generic)
+  instance ToExpr UTxOState
 #-}
 {-# COMPILE GHC UTxOState = data UTxOState (MkUTxOState) #-}
 
@@ -403,7 +412,7 @@ GovState = List (Pair GovActionID GovActionState)
     | NewCommittee [(Credential, Epoch)] [Credential] Rational
     | NewConstitution DataHash (Maybe ScriptHash)
     | TriggerHF ProtVer
-    | ChangePParams PParamsUpdate
+    | ChangePParams ()
     | TreasuryWdrl [(RwdAddr, Coin)]
     | Info
 

src/Ledger/PParams.lagda

@@ -168,8 +168,6 @@ instance
     ((quote PoolThresholds , DecEq-PoolThresholds) ∷ [])
   unquoteDecl DecEq-PParams        = derive-DecEq
     ((quote PParams , DecEq-PParams) ∷ [])
-  unquoteDecl DecEq-PParamGroup    = derive-DecEq
-    ((quote PParamGroup , DecEq-PParamGroup) ∷ [])
 
 instance
   pvCanFollow? : ∀ {pv} {pv'} → Dec (pvCanFollow pv pv')