From 2f90d3ec05059eaf6050ce85704e0388398cc3e9 Mon Sep 17 00:00:00 2001 From: whatisRT Date: Wed, 25 Jun 2025 11:32:34 +0200 Subject: [PATCH 1/2] Move ``yes` and ``no` to `Reflection.Syntax` --- Reflection/Syntax.agda | 8 ++++++++ Tactic/Derive/DecEq.agda | 4 ---- 2 files changed, 8 insertions(+), 4 deletions(-) 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 ⟧ ⟧ diff --git a/Tactic/Derive/DecEq.agda b/Tactic/Derive/DecEq.agda index ed7650db..22b22b07 100644 --- a/Tactic/Derive/DecEq.agda +++ b/Tactic/Derive/DecEq.agda @@ -39,10 +39,6 @@ open ClauseExprM private instance _ = ContextMonad-MonadTC - `yes `no : Term → Term - `yes x = quote _because_ ◆⟦ quote true ◆ ∣ quote ofʸ ◆⟦ x ⟧ ⟧ - `no x = quote _because_ ◆⟦ quote false ◆ ∣ quote ofⁿ ◆⟦ x ⟧ ⟧ - -- 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 From a72521a0e0e6ac2b15539f07c6596b75f672567f Mon Sep 17 00:00:00 2001 From: whatisRT Date: Mon, 30 Jun 2025 14:02:08 +0200 Subject: [PATCH 2/2] Add some more common quoted syntax --- Reflection/Syntax.agda | 8 -------- Tactic/ByEq.agda | 5 +++-- Tactic/ClauseBuilder.agda | 3 ++- Tactic/Derive/DecEq.agda | 7 ++++--- Tactic/ReduceDec.agda | 5 +++-- Tactic/Rewrite.agda | 3 ++- 6 files changed, 14 insertions(+), 17 deletions(-) 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 ⟧ ⟧ diff --git a/Tactic/ByEq.agda b/Tactic/ByEq.agda index 6c07acda..fd1fb289 100644 --- a/Tactic/ByEq.agda +++ b/Tactic/ByEq.agda @@ -7,6 +7,7 @@ open import Class.Functor open import Class.Monad open import Reflection using (TC; withNormalisation; inferType; unify) open import Reflection.Utils using (argTys) +open import Reflection.QuotedDefinitions -- Introduce as many arguments as possible and then: -- 1. for those of type `_ ≡ _`, unify with `refl` @@ -16,8 +17,8 @@ by-eq : Hole → TC ⊤ by-eq hole = do ty ← withNormalisation true $ inferType hole let ps : Args Pattern - ps = argTys ty <&> fmap λ {(def (quote _≡_) _) → quote refl ◇; _ → dot unknown} - unify hole $ pat-lam [ clause [] ps (quote refl ◆) ] [] + ps = argTys ty <&> fmap λ { (_ ``≡ _) → ``refl ; _ → dot unknown } + unify hole $ pat-lam [ clause [] ps `refl ] [] macro $by-eq = by-eq diff --git a/Tactic/ClauseBuilder.agda b/Tactic/ClauseBuilder.agda index 0713c566..7b35dc5f 100644 --- a/Tactic/ClauseBuilder.agda +++ b/Tactic/ClauseBuilder.agda @@ -15,6 +15,7 @@ open import Data.List.Sort using (SortingAlgorithm) open import Data.List.Sort.MergeSort using (mergeSort) open SortingAlgorithm ≤-decTotalOrder (mergeSort ≤-decTotalOrder) public +open import Reflection.QuotedDefinitions open import Reflection.Utils open import Reflection.Utils.TCI @@ -213,7 +214,7 @@ module _ {M : ∀ {a} → Set a → Set a} ⦃ _ : Monad M ⦄ ⦃ me : MonadErr return $ ref x' caseMatch : Term → M ClauseExpr → M Term - caseMatch t expr = debugLog ("Match" ∷ᵈ t ∷ᵈ []) >> (refineWithSingle (quote case_of_ ∙⟦ t ∣_⟧) $ + caseMatch t expr = debugLog ("Match" ∷ᵈ t ∷ᵈ []) >> (refineWithSingle (`case_of_ t) $ (λ expr' → pat-lam (clauseExprToClauses expr') []) <$> expr) currentTyConstrPatterns : M (List SinglePattern) diff --git a/Tactic/Derive/DecEq.agda b/Tactic/Derive/DecEq.agda index 22b22b07..7ad115f3 100644 --- a/Tactic/Derive/DecEq.agda +++ b/Tactic/Derive/DecEq.agda @@ -23,6 +23,7 @@ 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 @@ -73,15 +74,15 @@ private -- c x1 .. xn ≡ c y1 .. yn ⇔ x1 ≡ y1 .. xn ≡ yn genEquiv : ℕ → Term - genEquiv n = quote mk⇔ ∙⟦ `λ⟦ reflPattern n ⇒ quote refl ◆ ⟧ ∣ `λ⟦ quote refl ◇ ⇒ reflTerm n ⟧ ⟧ + genEquiv n = quote mk⇔ ∙⟦ `λ⟦ reflPattern n ⇒ `refl ⟧ ∣ `λ⟦ ``refl ⇒ reflTerm n ⟧ ⟧ where reflPattern : ℕ → Pattern reflPattern 0 = quote tt ◇ - reflPattern (suc n) = quote _,_ ◇⟦ reflPattern n ∣ quote refl ◇ ⟧ + reflPattern (suc n) = quote _,_ ◇⟦ reflPattern n ∣ ``refl ⟧ reflTerm : ℕ → Term reflTerm 0 = quote tt ◆ - reflTerm (suc n) = quote _,_ ◆⟦ reflTerm n ∣ quote refl ◆ ⟧ + reflTerm (suc n) = quote _,_ ◆⟦ reflTerm n ∣ `refl ⟧ toMapDiag : SinglePattern → SinglePattern → NE.List⁺ SinglePattern × TC (ClauseExpr ⊎ Maybe Term) toMapDiag p@(_ , arg _ p₁) p'@(_ , arg _ p₂) = diff --git a/Tactic/ReduceDec.agda b/Tactic/ReduceDec.agda index 8f3ad23c..d4412cb2 100644 --- a/Tactic/ReduceDec.agda +++ b/Tactic/ReduceDec.agda @@ -9,6 +9,7 @@ open import Meta.Prelude open import Meta.Init open import Reflection.Tactic +open import Reflection.QuotedDefinitions open import Reflection.Utils open import Reflection.Utils.TCI open import Relation.Nullary @@ -79,8 +80,8 @@ fromWitnessFalse' (yes p) h = ⊥-elim $ h p fromWitnessFalse' (no ¬p) h = refl fromWitness'Type : Bool → Term → Term -fromWitness'Type true dec = def (quote _≡_) (hArg? ∷ hArg? ∷ def (quote isYes) (hArg? ∷ hArg? ∷ dec ⟨∷⟩ []) ⟨∷⟩ quote true ◆ ⟨∷⟩ []) -fromWitness'Type false dec = def (quote _≡_) (hArg? ∷ hArg? ∷ def (quote isYes) (hArg? ∷ hArg? ∷ dec ⟨∷⟩ []) ⟨∷⟩ quote false ◆ ⟨∷⟩ []) +fromWitness'Type true dec = quote isYes ∙⟦ dec ⟧ `≡ quote true ◆ +fromWitness'Type false dec = quote isYes ∙⟦ dec ⟧ `≡ quote false ◆ findDecRWHypWith : ITactic → Term → TC Term findDecRWHypWith tac dec = diff --git a/Tactic/Rewrite.agda b/Tactic/Rewrite.agda index d5dd7c39..46514700 100644 --- a/Tactic/Rewrite.agda +++ b/Tactic/Rewrite.agda @@ -9,6 +9,7 @@ open import Data.Product using (map₂) open import Relation.Nullary.Decidable using (⌊_⌋) open import Reflection hiding (_>>=_; _>>_; _≟_) +open import Reflection.QuotedDefinitions open import Reflection.Syntax open import Reflection.Tactic open import Reflection.Utils.Debug; open Debug ("tactic.rewrite" , 100) @@ -21,7 +22,7 @@ open import Class.Show viewEq : Term → TC (Term × Term) viewEq eq = do - (def (quote _≡_) (_ ∷ _ ∷ vArg x ∷ vArg y ∷ [])) ← inferType eq + x ``≡ y ← inferType eq where _ → error "Can only write with equalities `x ≡ y`." return (x , y)