Improve performance of DecEq deriving

Reflection/QuotedDefinitions.agda

@@ -0,0 +1,31 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Reflection.QuotedDefinitions where
+
+open import Meta.Prelude
+
+open import Reflection.Syntax
+
+infix 4 _`≡_ _``≡_
+_`≡_ : Term → Term → Term
+t `≡ t' = quote _≡_ ∙⟦ t ∣ t' ⟧
+
+pattern _``≡_ t t' = def (quote _≡_) (_ ∷ _ ∷ vArg t ∷ vArg t' ∷ [])
+
+`refl : Term
+`refl = quote refl ◆
+
+pattern ``refl = quote refl ◇
+
+`case_of_ : Term → Term → Term
+`case t of t' = quote case_of_ ∙⟦ t ∣ t' ⟧
+
+-- Syntax for quoting `yes` and `no`
+open import Relation.Nullary
+
+`yes `no : Term → Term
+`yes x = quote _because_ ◆⟦ quote true  ◆ ∣ quote ofʸ ◆⟦ x ⟧ ⟧
+`no  x = quote _because_ ◆⟦ quote false ◆ ∣ quote ofⁿ ◆⟦ x ⟧ ⟧
+
+pattern ``yes x = quote _because_ ◇⟦ quote true  ◇ ∣ quote ofʸ ◇⟦ x ⟧ ⟧
+pattern ``no x  = quote _because_ ◇⟦ quote false ◇ ∣ quote ofⁿ ◇⟦ x ⟧ ⟧

Tactic/Derive/DecEq.agda

@@ -17,17 +17,13 @@ import Data.List as L
 import Data.List.NonEmpty as NE
 
 open import Relation.Nullary
-open import Relation.Nullary.Decidable
 
 open import Reflection.Tactic
-open import Reflection.AST.Term using (_≟-Pattern_)
-open import Reflection.Utils
-open import Reflection.Utils.TCI
 open import Reflection.QuotedDefinitions
+open import Reflection.AST.DeBruijn
 
 open import Class.DecEq.Core
 open import Class.Functor
-open import Class.Monad
 open import Class.MonadTC.Instances
 open import Class.Traversable
 
@@ -37,17 +33,29 @@ open import Tactic.Derive (quote DecEq) (quote _≟_)
 
 open ClauseExprM
 
+-- simply typed annotated case_of_, giving better performance than without a type annotation
+-- the type annotation prevents elaboration time from doubling on every argument to a constructor
+`case_returning_of_ : Term → Term → Term → Term
+`case t returning t' of t'' = def (quote case_of_) (hArg? ∷ hArg? ∷ hArg? ∷ hArg t' ∷ vArg t ∷ vArg t'' ∷ [])
+
 private
   instance _ = ContextMonad-MonadTC
 
-  -- We take the Dec P argument first to improve type checking performance.
-  -- It's easy to infer the type of P from this argument and we need to know
-  -- P to be able to check the pattern lambda generated for the P → Q direction
-  -- of the isomorphism. Having the isomorphism first would cause the type checker
-  -- to go back and forth between the pattern lambda and the Dec P argument,
-  -- inferring just enough of the type of make progress on the lambda.
-  map' : ∀ {p q} {P : Set p} {Q : Set q} → Dec P → P ⇔ Q → Dec Q
-  map' d record { to = to ; from = from } = map′ to from d
+  -- Here's an example of what code this generates, here for a record R with 3 fields:
+  -- DecEq : DecEq R
+  -- DecEq ._≟_ ⟪ x₁ , x₂ , x₃ ⟫ ⟪ y₁ , y₂ , y₃ ⟫ =
+  --   case (x₁ ≟ y₁) of λ where
+  --     (false because ¬p) → no (case ¬p of λ where (ofⁿ ¬p) refl → ¬p refl)
+  --     (true because p₁) → case (x₂ ≟ y₂) of λ where
+  --       (false because ¬p) → no (case ¬p of λ where (ofⁿ ¬p) refl → ¬p refl)
+  --       (true because p₂) → case (x₃ ≟ y₃) of λ where
+  --         (false because ¬p) → no (case ¬p of λ where (ofⁿ ¬p) refl → ¬p refl)
+  --         (true because p₃) →  yes (case p₁ , p₂ , p₃ of λ where (ofʸ refl , ofʸ refl , ofʸ refl) → refl)
+
+  -- patterns almost like `yes` and `no`, except that they don't match the `Reflects` proof
+  -- delaying maching on the `Reflects` proof as late as possible results in a major speed increase
+  pattern ``yes' x = quote _because_ ◇⟦ quote true  ◇ ∣ x ⟧
+  pattern ``no'  x = quote _because_ ◇⟦ quote false ◇ ∣ x ⟧
 
   module _ (transName : Name → Maybe Name) where
 
@@ -57,36 +65,54 @@ private
     ... | nothing     = quote _≟_ ∙⟦ t ∣ t' ⟧
     eqFromTerm _ t t' = quote _≟_ ∙⟦ t ∣ t' ⟧
 
-    toDecEqName : SinglePattern → List (Term → Term → Term)
-    toDecEqName (l , _) = L.map (λ where (_ , arg _ t) → eqFromTerm t) l
-
-    -- on the diagonal we have one pattern, outside we don't care
+    -- `nothing`: outside of the diagonal, not equal
+    -- `just`: on the diagonal, with that pattern, could be equal
     -- assume that the types in the pattern are properly normalized
-    mapDiag : Maybe SinglePattern → TC Term
-    mapDiag nothing          = return $ `no `λ⦅ [ ("" , vArg?) ] ⦆∅
-    mapDiag (just p@(l , _)) = let k = length l in do
-      typeList ← traverse ⦃ Functor-List ⦄ inferType (applyDownFrom ♯ (length l))
-      return $ quote map' ∙⟦ genPf k (L.map eqFromTerm typeList) ∣ genEquiv k ⟧
+    genBranch : Maybe SinglePattern → TC Term
+    genBranch nothing         = return $ `no `λ⦅ [ ("" , vArg?) ] ⦆∅
+    genBranch (just ([] , _)) = return $ `yes `refl
+    genBranch (just p@(l@(x ∷ xs) , arg _ pat)) = do
+      (con n args) ← return pat
+        where _ → error1 "BUG: genBranch"
+      typeList ← traverse inferType (applyUpTo ♯ (length l))
+      let info = L.zip typeList (downFrom (length l))
+      let ty = quote Dec ∙⟦ con n (applyDownFrom (vArg ∘ ♯ ∘ (_+ length l)) (length l))
+                         `≡ con n (applyDownFrom (vArg ∘ ♯) (length l)) ⟧
+      return $ foldl (λ t (eq , k) → genCase (weaken k ty) (eqFromTerm eq) t) genTrueCase info
       where
-        genPf : ℕ → List (Term → Term → Term) → Term
-        genPf k []      = `yes (quote tt ◆)
-        genPf k (n ∷ l) = quote _×-dec_ ∙⟦ genPf k l ∣ n (♯ (length l)) (♯ (length l + k)) ⟧
-
-        -- c x1 .. xn ≡ c y1 .. yn ⇔ x1 ≡ y1 .. xn ≡ yn
-        genEquiv : ℕ → Term
-        genEquiv n = quote mk⇔ ∙⟦ `λ⟦ reflPattern n ⇒ `refl ⟧ ∣ `λ⟦ ``refl ⇒ reflTerm n ⟧ ⟧
-          where
-            reflPattern : ℕ → Pattern
-            reflPattern 0       = quote tt ◇
-            reflPattern (suc n) = quote _,_ ◇⟦ reflPattern n ∣ ``refl ⟧
-
-            reflTerm : ℕ → Term
-            reflTerm 0       = quote tt ◆
-            reflTerm (suc n) = quote _,_ ◆⟦ reflTerm n ∣ `refl ⟧
+        k = ℕ.suc (length xs)
+
+        vars : NE.List⁺ ℕ
+        vars = 0 NE.∷ applyUpTo ℕ.suc (length xs)
+
+        -- case (xᵢ ≟ yᵢ) of λ { (false because ...) → no ... ; (true because p) → t }
+        -- since we always add one variable to the scope of t the uncompared terms
+        -- are always at index 2k+1 and k
+        genCase : Term → (Term → Term → Term) → Term → Term
+        genCase goalTy _`≟_ t = `case ♯ (2 * k ∸ 1) `≟ ♯ (k ∸ 1)
+          returning goalTy
+          of clauseExprToPatLam (MatchExpr
+          ( (singlePatternFromPattern (vArg (``yes' (` 0))) , inj₂ (just t))
+          ∷ (singlePatternFromPattern (vArg (``no'  (` 0))) , inj₂ (just (`no $
+              -- case ¬p of λ where (ofⁿ ¬p) refl → ¬p refl
+              `case ♯ 0 of clauseExprToPatLam (multiClauseExpr
+                [(     singlePatternFromPattern (vArg (quote ofⁿ ◇⟦ ` 0 ⟧))
+                  NE.∷ singlePatternFromPattern (vArg ``refl) ∷ []
+                  , inj₂ (just ♯ 0 ⟦ `refl ⟧)) ]))))
+          ∷ []))
+
+        -- yes (case p₁ , ... , pₖ of λ where (ofʸ refl , ... , ofʸ refl) → refl)
+        genTrueCase : Term
+        genTrueCase = `yes $
+          `case NE.foldl₁ (quote _,′_ ∙⟦_∣_⟧) (NE.map ♯ vars)
+           of clauseExprToPatLam (MatchExpr
+             [ (singlePatternFromPattern
+                 (vArg (NE.foldl₁ (quote _,_ ◇⟦_∣_⟧) (NE.map (λ _ → quote ofʸ ◇⟦ ``refl ⟧) vars)))
+             , inj₂ (just `refl)) ])
 
     toMapDiag : SinglePattern → SinglePattern → NE.List⁺ SinglePattern × TC (ClauseExpr ⊎ Maybe Term)
     toMapDiag p@(_ , arg _ p₁) p'@(_ , arg _ p₂) =
-      (p NE.∷ [ p' ] , finishMatch (if ⌊ p₁ ≟-Pattern p₂ ⌋ then mapDiag (just p) else mapDiag nothing))
+      (p NE.∷ [ p' ] , finishMatch (if ⌊ p₁ ≟-Pattern p₂ ⌋ then genBranch (just p) else genBranch nothing))
 
 module _ ⦃ _ : TCOptions ⦄ where
   derive-DecEq : List (Name × Name) → UnquoteDecl
@@ -118,6 +144,7 @@ private
 
   unquoteDecl DecEq-R1 = derive-DecEq [ (quote R1 , DecEq-R1) ]
   unquoteDecl DecEq-R2 = derive-DecEq [ (quote R2 , DecEq-R2) ]
+  unquoteDecl DecEq-R20 = derive-DecEq [ (quote R20 , DecEq-R20) ]
 
   unquoteDecl DecEq-M₁ DecEq-M₂ = derive-DecEq $ (quote M₁ , DecEq-M₁) ∷ (quote M₂ , DecEq-M₂) ∷ []
 

Tactic/Derive/TestTypes.agda

@@ -42,6 +42,9 @@ record R2 {a} (A : Set a) : Set a where
         f5R2 : A
         f6R2 : A
 
+record R20 : Set where
+  field r0 r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11 r12 r13 r14 r15 r16 r17 r18 r19 : Bool
+
 data M₁ : Set
 data M₂ : Set
 data M₁ where