Fix foreign interface for ENTITIES

Author: carlostome

src/Ledger/Dijkstra/Foreign/Certs.agda

@@ -33,6 +33,11 @@ instance
     • withName "DelegEnv"
   Conv-DelegEnv = autoConvert DelegEnv
 
+  HsTy-GovCertEnv = autoHsType GovCertEnv
+    ⊣ withConstructor "MkGovCertEnv"
+    • fieldPrefix "gce"
+  Conv-GovCertEnv = autoConvert GovCertEnv
+
   HsTy-PState = autoHsType PState
     ⊣ withConstructor "MkPState"
     • fieldPrefix "ps"
@@ -49,32 +54,11 @@ instance
     • fieldPrefix "gs"
   Conv-GState = autoConvert GState
 
--- CertEnv needs a wrapper because the votes field uses GovVote
--- which requires non-trivial conversion through GovVote'.
-
-record CertEnv' : Type where
-  field
-    epoch          : Epoch
-    pp             : PParams
-    votes          : List GovVote'
-    wdrls          : RewardAddress ⇀ Coin
-    coldCreds      : ℙ Credential
-    directDeposits : DirectDeposits
-
-instance
-  HsTy-CertEnv' = autoHsType CertEnv'
+  HsTy-CertEnv = autoHsType CertEnv
     ⊣ withConstructor "MkCertEnv"
     • withName "CertEnv"
     • fieldPrefix "ce"
-  Conv-CertEnv' = autoConvert CertEnv'
-
-  mkCertEnv' : Convertible CertEnv CertEnv'
-  mkCertEnv' = λ where
-    .to   ce → let module ce = CertEnv ce in record { epoch = ce.epoch ; pp = ce.pp ; votes = to ce.votes ; wdrls = ce.wdrls ; coldCreds = ce.coldCreds ; directDeposits = ce.directDeposits }
-    .from ce → let module ce = CertEnv' ce in record { epoch = ce.epoch ; pp = ce.pp ; votes = from ce.votes ; wdrls = ce.wdrls ; coldCreds = ce.coldCreds ; directDeposits = ce.directDeposits }
-
-  HsTy-CertEnv = mkHsType CertEnv (HsType CertEnv')
-  Conv-CertEnv = mkCertEnv' ⨾ Conv-CertEnv'
+  Conv-CertEnv = autoConvert CertEnv
 
 -- Computational step functions
 
@@ -88,7 +72,7 @@ pool-step = to (compute Computational-POOL)
 
 {-# COMPILE GHC pool-step as poolStep #-}
 
-govcert-step : HsType (CertEnv → GState → DCert → ComputationResult String GState)
+govcert-step : HsType (GovCertEnv → GState → DCert → ComputationResult String GState)
 govcert-step = to (compute Computational-GOVCERT)
 
 {-# COMPILE GHC govcert-step as govCertStep #-}

src/Ledger/Dijkstra/Foreign/Entities.agda

@@ -12,12 +12,31 @@ open import Ledger.Core.Foreign.Address
 open import Ledger.Dijkstra.Foreign.HSStructures
 open import Ledger.Dijkstra.Foreign.Gov.Core
 open import Ledger.Dijkstra.Foreign.PParams
-open import Ledger.Dijkstra.Foreign.Cert
+open import Ledger.Dijkstra.Specification.Entities DummyGovStructure
 open import Ledger.Dijkstra.Specification.Entities.Properties.Computational DummyGovStructure
 
 open Computational
 
-entities-step : HsType (CertEnv → CertState → List DCert → ComputationResult String CertState)
-entities-step = to (compute Computational-ENTITIES)
+record EntitiesEnv' : Type where
+  field
+    epoch           : Epoch
+    pp              : PParams
+    votes           : List GovVote'
+    withdrawals     : RewardAddress ⇀ Coin
+    coldCredentials : ℙ Credential
+    directDeposits  : DirectDeposits
 
-{-# COMPILE GHC entities-step as entitiesStep #-}
+instance
+  HsTy-EntitiesEnv' = autoHsType EntitiesEnv'
+    ⊣ withConstructor "MkEntitiesEnv"
+    • withName "EntitiesEnv"
+    • fieldPrefix "ce"
+  Conv-EntitiesEnv' = autoConvert EntitiesEnv'
+
+  mkEntitiesEnv' : Convertible EntitiesEnv EntitiesEnv'
+  mkEntitiesEnv' = λ where
+    .to   ee → let module ee = EntitiesEnv ee in record { epoch = ee.epoch ; pp = ee.pp ; votes = to ee.votes ; withdrawals = ee.withdrawals ; coldCredentials = ee.coldCredentials ; directDeposits = ee.directDeposits }
+    .from ee → let module ee = EntitiesEnv' ee in record { epoch = ee.epoch ; pp = ee.pp ; votes = from ee.votes ; withdrawals = ee.withdrawals ; coldCredentials = ee.coldCredentials ; directDeposits = ee.directDeposits }
+
+  HsTy-EntitiesEnv = mkHsType EntitiesEnv (HsType EntitiesEnv')
+  Conv-EntitiesEnv = mkEntitiesEnv' ⨾ Conv-EntitiesEnv'