From 5f502998759711c4b036a63a2ecc78688946c0e8 Mon Sep 17 00:00:00 2001
From: Ana Pantilie <ana.pantilie95@gmail.com>
Date: Mon, 25 Nov 2024 17:52:43 +0200
Subject: [PATCH 1/2] Try Agda Reflection again

---
 nix/agda.nix                                  | 32 +++++++++++++++-
 plutus-metatheory/Plutus.agda-lib             |  2 +-
 .../src/VerifiedCompilation.lagda.md          | 37 +++++++++++++++++++
 3 files changed, 69 insertions(+), 2 deletions(-)

diff --git a/nix/agda.nix b/nix/agda.nix
index 9c13969464f..c115b0db7d4 100644
--- a/nix/agda.nix
+++ b/nix/agda.nix
@@ -26,6 +26,35 @@ rec {
     '';
   });
 
+  agda-stdlib-classes = agda-packages.mkDerivation {
+    pname = "agda-stdlib-classes";
+    version = "2.0";
+    src = pkgs.fetchFromGitHub {
+      repo = "agda-stdlib-classes";
+      owner = "omelkonian";
+      rev = "28df278381c94a25c54f6819524cd9f8cb99f092";
+      sha256 = "sha256-TdPJ3K4jyAIQgX1sUrqd0QeA72n2mkBVzlg8WfrqWWY=";
+    };
+    meta = { };
+    libraryFile = "agda-stdlib-classes.agda-lib";
+    everythingFile = "standard-library-classes.agda";
+    buildInputs = [ agda-stdlib ];
+  };
+
+  agda-stdlib-meta = agda-packages.mkDerivation {
+    pname = "agda-stdlib-meta";
+    version = "2.1.1";
+    src = pkgs.fetchFromGitHub {
+      repo = "stdlib-meta";
+      owner = "omelkonian";
+      rev = "v2.1.1";
+      sha256 = "qOoThYMG0dzjKvwmzzVZmGcerfb++MApbaGRzLEq3/4=";
+    };
+    meta = { };
+    libraryFile = "agda-stdlib-meta.agda-lib";
+    everythingFile = "Main.agda";
+    buildInputs = [ agda-stdlib agda-stdlib-classes ];
+  };
 
   # We want to keep control of which version of Agda we use, so we supply our own and override
   # the one from nixpkgs.
@@ -119,7 +148,8 @@ rec {
   };
 
 
-  agda-with-stdlib = agda-packages.agda.withPackages [ agda-stdlib ];
+  agda-with-stdlib =
+    agda-packages.agda.withPackages [ agda-stdlib agda-stdlib-classes agda-stdlib-meta ];
 
 
   agda-project = pkgs.haskell-nix.hackage-project {
diff --git a/plutus-metatheory/Plutus.agda-lib b/plutus-metatheory/Plutus.agda-lib
index b05fc13accc..c33b00995b9 100644
--- a/plutus-metatheory/Plutus.agda-lib
+++ b/plutus-metatheory/Plutus.agda-lib
@@ -1,2 +1,2 @@
-depend: standard-library
+depend: standard-library, standard-library-classes, standard-library-meta
 include: src
diff --git a/plutus-metatheory/src/VerifiedCompilation.lagda.md b/plutus-metatheory/src/VerifiedCompilation.lagda.md
index 970a81e02fa..5d38e640607 100644
--- a/plutus-metatheory/src/VerifiedCompilation.lagda.md
+++ b/plutus-metatheory/src/VerifiedCompilation.lagda.md
@@ -60,6 +60,7 @@ import Relation.Binary as Binary using (Decidable)
 import Relation.Unary as Unary using (Decidable)
 import Agda.Builtin.Int
 import Relation.Nary as Nary using (Decidable)
+
 ```
 
 ## Compiler optimisation traces
@@ -186,3 +187,39 @@ runCertifier : List (SimplifierTag × Untyped × Untyped) → Maybe Proof
 runCertifier rawInput with traverseEitherList (toWellScoped {⊥}) rawInput
 ... | inj₁ _ = nothing
 ... | inj₂ inputTrace = just (proof (isTrace? inputTrace))
+
+open import Tactic.Derive.Show
+import Data.List.Base as L
+import Agda.Builtin.Sigma as S
+open import Class.MonadTC.Instances
+open import Tactic.Defaults
+open import Relation.Nullary using (Reflects)
+open import Data.Bool.Base using (Bool)
+open import Class.Show.Core
+open import Agda.Primitive using (Level)
+
+variable
+  l : Level
+  A : Set l
+
+instance 
+  Show-Neg : Show (A → ⊥)
+  Show-Neg = ?
+
+unquoteDecl
+    Show-Dec
+    Show-Trace
+    Show-Reflects
+    Show-Bool
+    Show-Transformation
+    Show-Translation
+  =
+    derive-Show 
+      ( (quote Dec S., Show-Dec)
+      L.∷ (quote Trace S., Show-Trace)
+      L.∷ (quote Reflects S., Show-Reflects)
+      L.∷ (quote Bool S., Show-Bool)
+      L.∷ (quote Transformation S., Show-Transformation)
+      L.∷ (quote Translation S., Show-Translation)
+      L.∷ L.[]
+      )
\ No newline at end of file

From a743213212f3218ce77725aa7bf3948df54fddb6 Mon Sep 17 00:00:00 2001
From: Ana Pantilie <ana.pantilie95@gmail.com>
Date: Tue, 26 Nov 2024 12:42:03 +0200
Subject: [PATCH 2/2] Manual Pointwise instance breaks meta

---
 plutus-metatheory/src/VerifiedCompilation.lagda.md | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/plutus-metatheory/src/VerifiedCompilation.lagda.md b/plutus-metatheory/src/VerifiedCompilation.lagda.md
index 5d38e640607..45c2f226b3f 100644
--- a/plutus-metatheory/src/VerifiedCompilation.lagda.md
+++ b/plutus-metatheory/src/VerifiedCompilation.lagda.md
@@ -197,15 +197,25 @@ open import Relation.Nullary using (Reflects)
 open import Data.Bool.Base using (Bool)
 open import Class.Show.Core
 open import Agda.Primitive using (Level)
+open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise)
+open import Relation.Binary.Core using (REL)
 
 variable
   l : Level
+  l' : Level
+  l'' : Level
   A : Set l
+  B : Set l'
+  X : Set
 
 instance 
   Show-Neg : Show (A → ⊥)
   Show-Neg = ?
 
+instance
+  Show-Pointwise : {xs : L.List A} {ys : L.List B} {r : REL A B l''} {{ _ : Show A }} → Show (Pointwise r xs ys)
+  Show-Pointwise = ?
+
 unquoteDecl
     Show-Dec
     Show-Trace