From 8736b4d7e21eca7aedf999ae0af6f0b6e4bfcff2 Mon Sep 17 00:00:00 2001 From: whatisRT Date: Wed, 25 Jun 2025 11:32:34 +0200 Subject: [PATCH 1/4] Move ``yes` and ``no` to `Reflection.Syntax` --- Reflection/Syntax.agda | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/Reflection/Syntax.agda b/Reflection/Syntax.agda index 307429da..fb1d2ed0 100644 --- a/Reflection/Syntax.agda +++ b/Reflection/Syntax.agda @@ -111,3 +111,11 @@ Context = Args Type TTerm = Term × Type Hole = Term THole = Hole × Type + +-- Syntax for quoting `yes` and `no` +open import Relation.Nullary +open import Relation.Nullary.Decidable + +`yes `no : Term → Term +`yes x = quote _because_ ◆⟦ quote true ◆ ∣ quote ofʸ ◆⟦ x ⟧ ⟧ +`no x = quote _because_ ◆⟦ quote false ◆ ∣ quote ofⁿ ◆⟦ x ⟧ ⟧ From 842c68d531e40fcb46d77b8b10015ab75170bd0d Mon Sep 17 00:00:00 2001 From: whatisRT Date: Mon, 30 Jun 2025 14:02:08 +0200 Subject: [PATCH 2/4] Add some more common quoted syntax --- Reflection/QuotedDefinitions.agda | 31 +++++++++++++++++++++++++++++++ Reflection/Syntax.agda | 8 -------- 2 files changed, 31 insertions(+), 8 deletions(-) create mode 100644 Reflection/QuotedDefinitions.agda diff --git a/Reflection/QuotedDefinitions.agda b/Reflection/QuotedDefinitions.agda new file mode 100644 index 00000000..38e90064 --- /dev/null +++ b/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 ⟧ ⟧ diff --git a/Reflection/Syntax.agda b/Reflection/Syntax.agda index fb1d2ed0..307429da 100644 --- a/Reflection/Syntax.agda +++ b/Reflection/Syntax.agda @@ -111,11 +111,3 @@ Context = Args Type TTerm = Term × Type Hole = Term THole = Hole × Type - --- Syntax for quoting `yes` and `no` -open import Relation.Nullary -open import Relation.Nullary.Decidable - -`yes `no : Term → Term -`yes x = quote _because_ ◆⟦ quote true ◆ ∣ quote ofʸ ◆⟦ x ⟧ ⟧ -`no x = quote _because_ ◆⟦ quote false ◆ ∣ quote ofⁿ ◆⟦ x ⟧ ⟧ From d459f65812b7eb73f8ebec771c2f6c17c9d79dc3 Mon Sep 17 00:00:00 2001 From: whatisRT Date: Wed, 9 Jul 2025 17:07:41 +0200 Subject: [PATCH 3/4] Rewrite `DecEq` deriving with better performance I see ~47% speedup in instance generation time (typechecking) and ~22% speedup at runtime (normalization) with admittedly flaky benchmarks. Crucially, the generated instances should now only ever force booleans during normalization if all we want to know is the boolean equality. --- Tactic/Derive/DecEq.agda | 90 +++++++++++++++++++++++----------------- 1 file changed, 52 insertions(+), 38 deletions(-) diff --git a/Tactic/Derive/DecEq.agda b/Tactic/Derive/DecEq.agda index 7ad115f3..479ae7d8 100644 --- a/Tactic/Derive/DecEq.agda +++ b/Tactic/Derive/DecEq.agda @@ -17,17 +17,12 @@ 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 Class.DecEq.Core open import Class.Functor -open import Class.Monad open import Class.MonadTC.Instances open import Class.Traversable @@ -40,14 +35,21 @@ open ClauseExprM 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 +59,48 @@ 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) , _)) = do + typeList ← traverse inferType (applyUpTo ♯ (length l)) + let eqs = L.map eqFromTerm typeList + return $ foldl (λ t eq → genCase eq t) genTrueCase eqs 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 + genCase _`≟_ t = `case ♯ (2 * k ∸ 1) `≟ ♯ (k ∸ 1) 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 From 36349fe6b4a61d2fce111975684f75074f072b7d Mon Sep 17 00:00:00 2001 From: whatisRT Date: Mon, 14 Jul 2025 14:25:50 +0200 Subject: [PATCH 4/4] Add type annotations to the generated `case_of_` terms This improves instance generation time by another ~10% in the existing benchmarks and prevents exponential blowup in constructors with many arguments. --- Tactic/Derive/DecEq.agda | 23 ++++++++++++++++++----- Tactic/Derive/TestTypes.agda | 3 +++ 2 files changed, 21 insertions(+), 5 deletions(-) diff --git a/Tactic/Derive/DecEq.agda b/Tactic/Derive/DecEq.agda index 479ae7d8..08e850c3 100644 --- a/Tactic/Derive/DecEq.agda +++ b/Tactic/Derive/DecEq.agda @@ -20,6 +20,7 @@ open import Relation.Nullary open import Reflection.Tactic open import Reflection.QuotedDefinitions +open import Reflection.AST.DeBruijn open import Class.DecEq.Core open import Class.Functor @@ -32,6 +33,11 @@ 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 @@ -65,10 +71,14 @@ private genBranch : Maybe SinglePattern → TC Term genBranch nothing = return $ `no `λ⦅ [ ("" , vArg?) ] ⦆∅ genBranch (just ([] , _)) = return $ `yes `refl - genBranch (just p@(l@(x ∷ xs) , _)) = do + 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 eqs = L.map eqFromTerm typeList - return $ foldl (λ t eq → genCase eq t) genTrueCase eqs + 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 k = ℕ.suc (length xs) @@ -78,8 +88,10 @@ private -- 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 - genCase _`≟_ t = `case ♯ (2 * k ∸ 1) `≟ ♯ (k ∸ 1) of clauseExprToPatLam (MatchExpr + 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 @@ -132,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₂) ∷ [] diff --git a/Tactic/Derive/TestTypes.agda b/Tactic/Derive/TestTypes.agda index 5d161352..254eda7c 100644 --- a/Tactic/Derive/TestTypes.agda +++ b/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