From c7d65e0c40fb257979316c321a4ae0730c1764c1 Mon Sep 17 00:00:00 2001
From: Jesper Cockx <jesper@sikanda.be>
Date: Fri, 5 Jul 2024 19:49:44 +0200
Subject: [PATCH] Compatibility with Agda PR #7322: add quantity to reflected
 syntax of constructor

---
 src/Reflection/AST/Definition.agda | 42 ++++++++++++++++++------------
 src/Reflection/AST/Show.agda       |  2 +-
 2 files changed, 26 insertions(+), 18 deletions(-)

diff --git a/src/Reflection/AST/Definition.agda b/src/Reflection/AST/Definition.agda
index 3f06fef070..dab8ab2505 100644
--- a/src/Reflection/AST/Definition.agda
+++ b/src/Reflection/AST/Definition.agda
@@ -15,9 +15,10 @@ open import Relation.Nullary.Decidable.Core            using (map′; _×-dec_;
 open import Relation.Binary.Definitions                using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; cong₂)
 
-import Reflection.AST.Argument as Arg
-import Reflection.AST.Name     as Name
-import Reflection.AST.Term     as Term
+import Reflection.AST.Argument          as Arg
+import Reflection.AST.Argument.Quantity as Quantity
+import Reflection.AST.Name              as Name
+import Reflection.AST.Term              as Term
 
 ------------------------------------------------------------------------
 -- Re-exporting type publically
@@ -56,8 +57,14 @@ record′-injective₂ refl = refl
 record′-injective : ∀ {c c′ fs fs′} → record′ c fs ≡ record′ c′ fs′ → c ≡ c′ × fs ≡ fs′
 record′-injective = < record′-injective₁ , record′-injective₂ >
 
-constructor′-injective : ∀ {c c′} → constructor′ c ≡ constructor′ c′ → c ≡ c′
-constructor′-injective refl = refl
+constructor′-injective₁ : ∀ {c c′ q q′} → constructor′ c q ≡ constructor′ c′ q′ → c ≡ c′
+constructor′-injective₁ refl = refl
+
+constructor′-injective₂ : ∀ {c c′ q q′} → constructor′ c q ≡ constructor′ c′ q′ → q ≡ q′
+constructor′-injective₂ refl = refl
+
+constructor′-injective : ∀ {c c′ q q′} → constructor′ c q ≡ constructor′ c′ q′ → c ≡ c′ × q ≡ q′
+constructor′-injective = < constructor′-injective₁ , constructor′-injective₂ >
 
 infix 4 _≟_
 
@@ -70,39 +77,40 @@ data-type pars cs ≟ data-type pars′ cs′ =
 record′ c fs      ≟ record′ c′ fs′      =
   map′ (uncurry (cong₂ record′)) record′-injective
            (c Name.≟ c′ ×-dec List.≡-dec (Arg.≡-dec Name._≟_) fs fs′)
-constructor′ d    ≟ constructor′ d′     =
-  map′ (cong constructor′) constructor′-injective (d Name.≟ d′)
+constructor′ d q  ≟ constructor′ d′ q′  =
+  map′ (uncurry (cong₂ constructor′)) constructor′-injective
+           (d Name.≟ d′ ×-dec q Quantity.≟ q′)
 axiom             ≟ axiom               = yes refl
 primitive′        ≟ primitive′          = yes refl
 
 -- antidiagonal
 function cs ≟ data-type pars cs₁ = no (λ ())
 function cs ≟ record′ c fs = no (λ ())
-function cs ≟ constructor′ d = no (λ ())
+function cs ≟ constructor′ d q = no (λ ())
 function cs ≟ axiom = no (λ ())
 function cs ≟ primitive′ = no (λ ())
 data-type pars cs ≟ function cs₁ = no (λ ())
 data-type pars cs ≟ record′ c fs = no (λ ())
-data-type pars cs ≟ constructor′ d = no (λ ())
+data-type pars cs ≟ constructor′ d q = no (λ ())
 data-type pars cs ≟ axiom = no (λ ())
 data-type pars cs ≟ primitive′ = no (λ ())
 record′ c fs ≟ function cs = no (λ ())
 record′ c fs ≟ data-type pars cs = no (λ ())
-record′ c fs ≟ constructor′ d = no (λ ())
+record′ c fs ≟ constructor′ d q = no (λ ())
 record′ c fs ≟ axiom = no (λ ())
 record′ c fs ≟ primitive′ = no (λ ())
-constructor′ d ≟ function cs = no (λ ())
-constructor′ d ≟ data-type pars cs = no (λ ())
-constructor′ d ≟ record′ c fs = no (λ ())
-constructor′ d ≟ axiom = no (λ ())
-constructor′ d ≟ primitive′ = no (λ ())
+constructor′ d q ≟ function cs = no (λ ())
+constructor′ d q ≟ data-type pars cs = no (λ ())
+constructor′ d q ≟ record′ c fs = no (λ ())
+constructor′ d q ≟ axiom = no (λ ())
+constructor′ d q ≟ primitive′ = no (λ ())
 axiom ≟ function cs = no (λ ())
 axiom ≟ data-type pars cs = no (λ ())
 axiom ≟ record′ c fs = no (λ ())
-axiom ≟ constructor′ d = no (λ ())
+axiom ≟ constructor′ d q = no (λ ())
 axiom ≟ primitive′ = no (λ ())
 primitive′ ≟ function cs = no (λ ())
 primitive′ ≟ data-type pars cs = no (λ ())
 primitive′ ≟ record′ c fs = no (λ ())
-primitive′ ≟ constructor′ d = no (λ ())
+primitive′ ≟ constructor′ d q = no (λ ())
 primitive′ ≟ axiom = no (λ ())
diff --git a/src/Reflection/AST/Show.agda b/src/Reflection/AST/Show.agda
index 467120b4ba..8757e3aef1 100644
--- a/src/Reflection/AST/Show.agda
+++ b/src/Reflection/AST/Show.agda
@@ -149,6 +149,6 @@ showDefinition (data-type pars cs) =
  "datatype" <+> ℕ.show pars <+> braces (intersperse ", " (map showName cs))
 showDefinition (record′ c fs)      =
  "record" <+> showName c <+> braces (intersperse ", " (map (showName ∘′ unArg) fs))
-showDefinition (constructor′ d)    = "constructor" <+> showName d
+showDefinition (constructor′ d q)  = "constructor" <+> showName d <+> showQuantity q
 showDefinition axiom               = "axiom"
 showDefinition primitive′          = "primitive"