Introduce common quoted terms (e.g. refl, yes, no)

Author: WhatisRT

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
 

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)

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
@@ -39,10 +40,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
@@ -77,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₂) =

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 =

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)