652 remove superscripts from rec constr

src/Class/To.agda

@@ -0,0 +1,107 @@
+{-# OPTIONS --safe #-}
+module Class.To where
+
+record To (X : Set) (Y : Set) : Set where
+  field 
+    ⟦_⟧ : X → Y
+  infix 5 ⟦_⟧
+
+open To ⦃...⦄ public
+
+-- Metaprogram to derive instances
+open import Data.List.NonEmpty as NE using (List⁺; _∷_)
+open import Data.List
+open import Meta
+open import MetaPrelude
+open import Reflection.Tactic
+open import Reflection.Utils.Debug
+
+open import Class.MonadTC
+open import Class.Monad
+open import Class.Functor
+open import Class.Traversable
+
+open import Data.Product.Nary.NonDependent using (uncurryₙ)
+
+open MonadTCI
+
+getCodPi : Type → Type
+getCodPi ty =
+  let as , ty_v = stripPis ty
+  in unbumpTerm (length as) ty_v
+  where
+    -- readjust De Bruijn indexes 
+    unbumpTerm : ℕ → Term → Term
+    unbumpArg : ℕ → Arg Term → Arg Term
+    unbumpArgs : ℕ → List (Arg Term) → List (Arg Term)
+
+    unbumpTerm n (var n' args) = var (n' ∸ n) (unbumpArgs n args)
+    unbumpTerm n (con c args) = con c (unbumpArgs n args)
+    unbumpTerm n (def f args) = def f (unbumpArgs n args)
+    unbumpTerm n d = d
+
+    unbumpArg n (arg i x) = arg i (unbumpTerm n x)
+
+    unbumpArgs n [] = []
+    unbumpArgs n (x ∷ xs) = unbumpArg n x ∷ unbumpArgs n xs
+
+-- Map a nonempty record def. to
+-- 1. its constructor
+-- 2. the type of its fields
+-- 3. the number of fields
+fromNERecDef : Definition → TC (Name × List⁺ Type × ℕ)
+fromNERecDef (record′ c (f ∷ fs)) =
+  do ty  ← fmap ⦃ Functor-M ⦄ getCodPi (getType (unArg f))
+     tys ← traverse (λ f → fmap ⦃ Functor-M ⦄ getCodPi (getType (unArg f))) fs
+     return (c , ty ∷ tys , 1 + length fs)
+fromNERecDef (record′ c [])       = typeError [ strErr "Expected a nonempty record type" ]
+fromNERecDef d                    = typeError [ strErr "Expected a record type" ]
+
+getRecConstrName : Name → TC Name
+getRecConstrName rn =
+  do d ← getDefinition rn
+     case d of λ where
+       (record′ c _) → return c
+       _ → typeError [ strErr "Expected a record got something else" ]
+
+-- Derive instance of To
+derive-To-single : Name -- name of the record type
+                 → Name -- name of the instance to be defined
+                 → TC ⊤
+derive-To-single recTyName instName =
+  do To-ctrName             ← getRecConstrName (quote To)
+     recDef                 ← getDefinition recTyName
+     (ctrName , fTys , nfs) ← fromNERecDef recDef
+     arity                  ← quoteTC nfs
+     arity'                 ← normalise arity
+     let tyProd = NE.foldr₁ (λ ty tys → (quote _×_) ∙⟦ ty ∣ tys ⟧) fTys
+     let defTm  = (quote To) ∙⟦ tyProd ∣ recTyName ∙ ⟧
+     let instTm = To-ctrName ◆⟦ quote uncurryₙ ∙⟦ arity' ∣ ctrName ◆ ⟧ ⟧
+     declareDef (iArg instName) defTm
+     defineFun instName [ ⟦⇒ instTm ⟧ ]
+
+module _ ⦃ _ : TCOptions ⦄ where
+  derive-To : List (Name × Name) → UnquoteDecl
+  derive-To rcs = initUnquoteWithGoal (quote To ∙) (traverse (uncurry derive-To-single) rcs >> return tt)
+
+-- Example usage
+private
+  record R : Set where
+    field r : Bool
+
+  record R' : Set where
+    field x : Bool
+          y : ℕ
+
+  unquoteDecl To-R To-R' = derive-To ⦃ defaultTCOptions ⦄ ((quote R , To-R) ∷ (quote R' , To-R') ∷ [])
+
+  p : R
+  p = ⟦ true ⟧
+
+  module _ (x : Set) where
+    record R'' : Set where
+      field a : ℕ
+            b c : Bool
+
+    instance
+      unquoteDecl To-R'' = derive-To ⦃ defaultTCOptions ⦄ ((quote R'' , To-R'') ∷  [])

src/Ledger/Certs.lagda

@@ -94,7 +94,6 @@ cwitness (reg c (suc _))     = just c
 record CertEnv : Type where
 \end{code}
 \begin{code}[hide]
-  constructor ⟦_,_,_,_,_⟧ᶜ
   field
 \end{code}
 \begin{code}
@@ -107,7 +106,6 @@ record CertEnv : Type where
 record DState : Type where
 \end{code}
 \begin{code}[hide]
-  constructor ⟦_,_,_⟧ᵈ
   field
 \end{code}
 \begin{code}
@@ -121,7 +119,6 @@ record DState : Type where
 record PState : Type where
 \end{code}
 \begin{code}[hide]
-  constructor ⟦_,_⟧ᵖ
   field
 \end{code}
 \begin{code}
@@ -134,7 +131,6 @@ record PState : Type where
 record GState : Type where
 \end{code}
 \begin{code}[hide]
-  constructor ⟦_,_⟧ᵛ
   field
 \end{code}
 \begin{code}
@@ -144,7 +140,6 @@ record GState : Type where
 record CertState : Type where
 \end{code}
 \begin{code}[hide]
-  constructor ⟦_,_,_⟧ᶜˢ
   field
 \end{code}
 \begin{code}
@@ -155,7 +150,6 @@ record CertState : Type where
 record DelegEnv : Type where
 \end{code}
 \begin{code}[hide]
-  constructor ⟦_,_,_⟧ᵈᵉ
   field
 \end{code}
 \begin{code}
@@ -180,6 +174,15 @@ instance
 \end{code}
 
 \begin{code}[hide]
+instance
+  unquoteDecl To-CertEnv To-DState To-PState To-GState To-CertState To-DelegEnv = derive-To
+    (   (quote CertEnv , To-CertEnv)
+    ∷   (quote DState , To-DState)
+    ∷   (quote PState , To-PState)
+    ∷   (quote GState , To-GState)
+    ∷   (quote CertState , To-CertState)
+    ∷ [ (quote DelegEnv , To-DelegEnv) ])
+
 private variable
   rwds rewards           : Credential ⇀ Coin
   dReps                  : Credential ⇀ Epoch
@@ -335,24 +338,24 @@ data _⊢_⇀⦇_,DELEG⦈_ where
         fromList ( nothing ∷ just abstainRep ∷ just noConfidenceRep ∷ [] )
     ∙ mkh ∈ mapˢ just (dom pools) ∪ ❴ nothing ❵
       ────────────────────────────────
-      ⟦ pp , pools , delegatees ⟧ᵈᵉ ⊢ ⟦ vDelegs , sDelegs , rwds ⟧ᵈ
+      ⟦ pp , pools , delegatees ⟧ ⊢ ⟦ vDelegs , sDelegs , rwds ⟧
         ⇀⦇ delegate c mv mkh d ,DELEG⦈
-        ⟦ insertIfJust c mv vDelegs , insertIfJust c mkh sDelegs , rwds ∪ˡ ❴ c , 0 ❵ ⟧ᵈ
+        ⟦ insertIfJust c mv vDelegs , insertIfJust c mkh sDelegs , rwds ∪ˡ ❴ c , 0 ❵ ⟧
 
   DELEG-dereg :
     ∙ (c , 0) ∈ rwds
       ────────────────────────────────
-      ⟦ pp , pools , delegatees ⟧ᵈᵉ ⊢ ⟦ vDelegs , sDelegs , rwds ⟧ᵈ ⇀⦇ dereg c md ,DELEG⦈
-        ⟦ vDelegs ∣ ❴ c ❵ ᶜ , sDelegs ∣ ❴ c ❵ ᶜ , rwds ∣ ❴ c ❵ ᶜ ⟧ᵈ
+      ⟦ pp , pools , delegatees ⟧ ⊢ ⟦ vDelegs , sDelegs , rwds ⟧ ⇀⦇ dereg c md ,DELEG⦈
+        ⟦ vDelegs ∣ ❴ c ❵ ᶜ , sDelegs ∣ ❴ c ❵ ᶜ , rwds ∣ ❴ c ❵ ᶜ ⟧
 \end{code}
 \begin{code}[hide]
   DELEG-reg : let open PParams pp in
     ∙ c ∉ dom rwds
     ∙ d ≡ keyDeposit ⊎ d ≡ 0
       ────────────────────────────────
-      ⟦ pp , pools , delegatees ⟧ᵈᵉ ⊢
-        ⟦ vDelegs , sDelegs , rwds ⟧ᵈ ⇀⦇ reg c d ,DELEG⦈
-        ⟦ vDelegs , sDelegs , rwds ∪ˡ ❴ c , 0 ❵ ⟧ᵈ
+      ⟦ pp , pools , delegatees ⟧ ⊢
+        ⟦ vDelegs , sDelegs , rwds ⟧ ⇀⦇ reg c d ,DELEG⦈
+        ⟦ vDelegs , sDelegs , rwds ∪ˡ ❴ c , 0 ❵ ⟧
 \end{code}
 \end{AgdaSuppressSpace}
 \caption{Auxiliary DELEG transition system}
@@ -369,12 +372,12 @@ data _⊢_⇀⦇_,POOL⦈_ where
   POOL-regpool :
     ∙ kh ∉ dom pools
       ────────────────────────────────
-      pp ⊢  ⟦ pools , retiring ⟧ᵖ ⇀⦇ regpool kh poolParams ,POOL⦈
-            ⟦ ❴ kh , poolParams ❵ ∪ˡ pools , retiring ⟧ᵖ
+      pp ⊢  ⟦ pools , retiring ⟧ ⇀⦇ regpool kh poolParams ,POOL⦈
+            ⟦ ❴ kh , poolParams ❵ ∪ˡ pools , retiring ⟧
 
   POOL-retirepool :
     ────────────────────────────────
-    pp ⊢ ⟦ pools , retiring ⟧ᵖ ⇀⦇ retirepool kh e ,POOL⦈ ⟦ pools , ❴ kh , e ❵ ∪ˡ retiring ⟧ᵖ
+    pp ⊢ ⟦ pools , retiring ⟧ ⇀⦇ retirepool kh e ,POOL⦈ ⟦ pools , ❴ kh , e ❵ ∪ˡ retiring ⟧
 \end{code}
 \end{AgdaSuppressSpace}
 \caption{Auxiliary POOL transition system}
@@ -391,19 +394,19 @@ data _⊢_⇀⦇_,GOVCERT⦈_ where
   GOVCERT-regdrep : ∀ {pp} → let open PParams pp in
     ∙ (d ≡ drepDeposit × c ∉ dom dReps) ⊎ (d ≡ 0 × c ∈ dom dReps)
       ────────────────────────────────
-      ⟦ e , pp , vs , wdrls , cc ⟧ᶜ ⊢  ⟦ dReps , ccKeys ⟧ᵛ ⇀⦇ regdrep c d an ,GOVCERT⦈
-                                  ⟦ ❴ c , e + drepActivity ❵ ∪ˡ dReps , ccKeys ⟧ᵛ
+      ⟦ e , pp , vs , wdrls , cc ⟧ ⊢  ⟦ dReps , ccKeys ⟧ ⇀⦇ regdrep c d an ,GOVCERT⦈
+                                  ⟦ ❴ c , e + drepActivity ❵ ∪ˡ dReps , ccKeys ⟧
 
   GOVCERT-deregdrep :
     ∙ c ∈ dom dReps
       ────────────────────────────────
-      ⟦ e , pp , vs , wdrls , cc ⟧ᶜ ⊢ ⟦ dReps , ccKeys ⟧ᵛ ⇀⦇ deregdrep c d ,GOVCERT⦈ ⟦ dReps ∣ ❴ c ❵ ᶜ , ccKeys ⟧ᵛ
+      ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ dReps , ccKeys ⟧ ⇀⦇ deregdrep c d ,GOVCERT⦈ ⟦ dReps ∣ ❴ c ❵ ᶜ , ccKeys ⟧
 
   GOVCERT-ccreghot :
     ∙ (c , nothing) ∉ ccKeys
     ∙ c ∈ cc
       ────────────────────────────────
-      ⟦ e , pp , vs , wdrls , cc ⟧ᶜ ⊢ ⟦ dReps , ccKeys ⟧ᵛ ⇀⦇ ccreghot c mc ,GOVCERT⦈ ⟦ dReps , ❴ c , mc ❵ ∪ˡ ccKeys ⟧ᵛ
+      ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ dReps , ccKeys ⟧ ⇀⦇ ccreghot c mc ,GOVCERT⦈ ⟦ dReps , ❴ c , mc ❵ ∪ˡ ccKeys ⟧
 \end{code}
 \end{AgdaSuppressSpace}
 \caption{Auxiliary GOVCERT transition system}
@@ -431,19 +434,19 @@ data _⊢_⇀⦇_,CERT⦈_ where
 \end{code}
 \begin{code}
   CERT-deleg :
-    ∙ ⟦ pp , PState.pools stᵖ , dom (GState.dreps stᵍ) ⟧ᵈᵉ ⊢ stᵈ ⇀⦇ dCert ,DELEG⦈ stᵈ'
+    ∙ ⟦ pp , PState.pools stᵖ , dom (GState.dreps stᵍ) ⟧ ⊢ stᵈ ⇀⦇ dCert ,DELEG⦈ stᵈ'
       ────────────────────────────────
-      ⟦ e , pp , vs , wdrls , cc ⟧ᶜ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ ⇀⦇ dCert ,CERT⦈ ⟦ stᵈ' , stᵖ , stᵍ ⟧ᶜˢ
+      ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ ⇀⦇ dCert ,CERT⦈ ⟦ stᵈ' , stᵖ , stᵍ ⟧
 
   CERT-pool :
     ∙ pp ⊢ stᵖ ⇀⦇ dCert ,POOL⦈ stᵖ'
       ────────────────────────────────
-      ⟦ e , pp , vs , wdrls , cc ⟧ᶜ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ ⇀⦇ dCert ,CERT⦈ ⟦ stᵈ , stᵖ' , stᵍ ⟧ᶜˢ
+      ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ ⇀⦇ dCert ,CERT⦈ ⟦ stᵈ , stᵖ' , stᵍ ⟧
 
   CERT-vdel :
     ∙ Γ ⊢ stᵍ ⇀⦇ dCert ,GOVCERT⦈ stᵍ'
       ────────────────────────────────
-      Γ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ ⇀⦇ dCert ,CERT⦈ ⟦ stᵈ , stᵖ , stᵍ' ⟧ᶜˢ
+      Γ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ ⇀⦇ dCert ,CERT⦈ ⟦ stᵈ , stᵖ , stᵍ' ⟧
 \end{code}
 \end{AgdaSuppressSpace}
 \emph{CERTBASE transition}
@@ -463,15 +466,15 @@ data _⊢_⇀⦇_,CERTBASE⦈_ where
     ∙ filter isKeyHash wdrlCreds ⊆ dom voteDelegs
     ∙ mapˢ (map₁ stake) (wdrls ˢ) ⊆ rewards ˢ
       ────────────────────────────────
-      ⟦ e , pp , vs , wdrls , cc ⟧ᶜ ⊢
-        ⟦ ⟦ voteDelegs , stakeDelegs , rewards ⟧ᵈ
+      ⟦ e , pp , vs , wdrls , cc ⟧ ⊢
+        ⟦ ⟦ voteDelegs , stakeDelegs , rewards ⟧
         , stᵖ
-        , ⟦ dReps , ccHotKeys ⟧ᵛ
-        ⟧ᶜˢ ⇀⦇ _ ,CERTBASE⦈
-        ⟦ ⟦ validVoteDelegs , stakeDelegs , constMap wdrlCreds 0 ∪ˡ rewards ⟧ᵈ
+        , ⟦ dReps , ccHotKeys ⟧
+        ⟧ ⇀⦇ _ ,CERTBASE⦈
+        ⟦ ⟦ validVoteDelegs , stakeDelegs , constMap wdrlCreds 0 ∪ˡ rewards ⟧
         , stᵖ
-        , ⟦ refreshedDReps , ccHotKeys ⟧ᵛ
-        ⟧ᶜˢ
+        , ⟦ refreshedDReps , ccHotKeys ⟧
+        ⟧
 \end{code}
 \end{AgdaSuppressSpace}
 \caption{CERTS rules}