0001-speed-up-product-solver.patch

From 681d6cab3a00f0a224b6a86af8e0765a27440fa4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Am=C3=A9lia=20Liao?= <me@amelia.how>
Date: Tue, 17 Dec 2024 11:26:35 -0300
Subject: [PATCH] speed up product solver

---
 src/Cat/Diagram/Product/Solver.lagda.md | 42 ++++++++++++++++++++++---
 1 file changed, 38 insertions(+), 4 deletions(-)

diff --git a/src/Cat/Diagram/Product/Solver.lagda.md b/src/Cat/Diagram/Product/Solver.lagda.md
index a78c33fba..a5540774d 100644
--- a/src/Cat/Diagram/Product/Solver.lagda.md
+++ b/src/Cat/Diagram/Product/Solver.lagda.md
@@ -510,12 +510,46 @@ macro
                     → (𝒞 : Precategory o ℓ) (cartesian : ∀ X Y → Product 𝒞 X Y)
                     → Term → Term → TC ⊤
   products-simpl! = Reflection.simpl-macro
+```
+
+<!--
+```agda
+module _ {o ℓ} (C : Precategory o ℓ) (cart : ∀ X Y → Product C X Y) {x y : ⌞ C ⌟} {h1 h2 : C .Precategory.Hom x y} where
+  open Reflection
 
-  products! : ∀ {o ℓ}
-              → (𝒞 : Precategory o ℓ) (cartesian : ∀ X Y → Product 𝒞 X Y)
-              → Term → TC ⊤
-  products! = Reflection.solve-macro
+  private
+    products-worker : Term → TC ⊤
+    products-worker goal = withReconstructed true $ withNormalisation true do
+      `h1 ← wait-for-type =<< quoteTC h1
+      `h2 ← quoteTC h2
+      `x ← quoteTC x
+      `y ← quoteTC y
+
+      “cart” ← quoteTC cart
+
+      let
+        “x”   = build-obj-expr `x
+        “y”   = build-obj-expr `y
+        “lhs” = build-hom-expr `h1
+        “rhs” = build-hom-expr `h2
+
+      unify goal (Reflection.“solve” unknown “cart” “x” “y” “lhs” “rhs”) <|> do
+        “cat” ← quoteTC C
+        vlhs ← normalise (“nf” “cat” “cart” “x” “y” “lhs”)
+        vrhs ← normalise (“nf” “cat” “cart” “x” “y” “rhs”)
+        typeError
+          [ "Could not equate the following expressions:\n  "
+          , termErr `h1 , "\nAnd\n  " , termErr `h2
+          , "\nReflected expressions\n  "
+          , termErr “lhs” , "\nAnd\n  " , termErr “rhs”
+          , strErr "\nComputed normal forms\n  "
+          , termErr vlhs , strErr "\nAnd\n  " , termErr vrhs
+          ]
+
+  products! : {@(tactic products-worker) p : h1 ≡ h2} → h1 ≡ h2
+  products! {p = p} = p
 ```
+-->
 
 # Demo
 
-- 
2.42.0