From 67bfa19ce0264f120087dafe8506cf8a2f4a4b60 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Mon, 18 Dec 2023 11:52:49 -0500
Subject: [PATCH] feat: add `quot_precheck` for expression tree elaborators
 (`binop%`, etc.) (#3078)

There were no `quot_precheck` instances registered for the expression
tree elaborators, which prevented them from being usable in a `notation`
expansion without turning off the quotation prechecker.

Users can evaluate whether `set_option quotPrecheck false` is still
necessary for their `notation` definitions.
---
 src/Lean/Elab/Quotation/Precheck.lean         | 32 +++++++++
 tests/lean/binopQuotPrecheck.lean             | 72 +++++++++++++++++++
 .../lean/binopQuotPrecheck.lean.expected.out  |  3 +
 3 files changed, 107 insertions(+)
 create mode 100644 tests/lean/binopQuotPrecheck.lean
 create mode 100644 tests/lean/binopQuotPrecheck.lean.expected.out

diff --git a/src/Lean/Elab/Quotation/Precheck.lean b/src/Lean/Elab/Quotation/Precheck.lean
index c0df85c2cba6..540c9b6d7814 100644
--- a/src/Lean/Elab/Quotation/Precheck.lean
+++ b/src/Lean/Elab/Quotation/Precheck.lean
@@ -141,4 +141,36 @@ private def isSectionVariable (e : Expr) : TermElabM Bool := do
   runPrecheck singleQuot.getQuotContent
   adaptExpander (fun _ => pure singleQuot) stx expectedType?
 
+section ExpressionTree
+
+@[builtin_quot_precheck Lean.Parser.Term.binrel] def precheckBinrel : Precheck
+  | `(binrel% $f $a $b) => do precheck f; precheck a; precheck b
+  | _ => throwUnsupportedSyntax
+
+@[builtin_quot_precheck Lean.Parser.Term.binrel_no_prop] def precheckBinrelNoProp : Precheck
+  | `(binrel_no_prop% $f $a $b) => do precheck f; precheck a; precheck b
+  | _ => throwUnsupportedSyntax
+
+@[builtin_quot_precheck Lean.Parser.Term.binop] def precheckBinop : Precheck
+  | `(binop% $f $a $b) => do precheck f; precheck a; precheck b
+  | _ => throwUnsupportedSyntax
+
+@[builtin_quot_precheck Lean.Parser.Term.binop_lazy] def precheckBinopLazy : Precheck
+  | `(binop_lazy% $f $a $b) => do precheck f; precheck a; precheck b
+  | _ => throwUnsupportedSyntax
+
+@[builtin_quot_precheck Lean.Parser.Term.leftact] def precheckLeftact : Precheck
+  | `(leftact% $f $a $b) => do precheck f; precheck a; precheck b
+  | _ => throwUnsupportedSyntax
+
+@[builtin_quot_precheck Lean.Parser.Term.rightact] def precheckRightact : Precheck
+  | `(rightact% $f $a $b) => do precheck f; precheck a; precheck b
+  | _ => throwUnsupportedSyntax
+
+@[builtin_quot_precheck Lean.Parser.Term.unop] def precheckUnop : Precheck
+  | `(unop% $f $a) => do precheck f; precheck a
+  | _ => throwUnsupportedSyntax
+
+end ExpressionTree
+
 end Lean.Elab.Term.Quotation
diff --git a/tests/lean/binopQuotPrecheck.lean b/tests/lean/binopQuotPrecheck.lean
new file mode 100644
index 000000000000..737d05eef500
--- /dev/null
+++ b/tests/lean/binopQuotPrecheck.lean
@@ -0,0 +1,72 @@
+/-!
+# Testing that binop% etc. have a quot_precheck
+-/
+
+section
+variable (a b : Nat)
+
+/-!
+binop%
+-/
+local notation "c1" => a + b
+/-!
+rightact%
+-/
+local notation "c2" => a ^ b
+/-!
+binrel%
+-/
+local notation "c3" => a ≤ b
+/-!
+binrel_no_prop%
+-/
+local notation "c4" => a == b
+/-!
+unop%
+-/
+local notation "c5" => -(a : Int)
+/-!
+leftact% (artificial test because there is no notation using it in core Lean)
+-/
+local notation "c6" => leftact% HAdd.hAdd a b
+
+example : c1 = a + b := rfl
+example : c2 = a ^ b := rfl
+example : c3 = (a ≤ b) := rfl
+example : c4 = (a == b) := rfl
+example : c5 = -a := rfl
+example : c6 = a + b := rfl
+end
+
+section
+variable (a b : Option Nat)
+
+/-!
+binop_lazy%
+-/
+local notation "c7" => a <|> b
+
+example : c7 = (a <|> b) := rfl
+
+end
+
+/-!
+Precheck failure in first argument.
+-/
+notation "precheckFailure" x y => binop% a x y
+
+/-!
+Precheck failure in second argument.
+-/
+notation "precheckFailure" y => binop% HAdd.hAdd a y
+
+/-!
+Precheck failure in third argument.
+-/
+notation "precheckFailure" x => binop% HAdd.hAdd x a
+
+/-!
+No precheck failure when `quotPrecheck` is off.
+-/
+set_option quotPrecheck false in
+notation "skipPrecheck" => binop% a b c
diff --git a/tests/lean/binopQuotPrecheck.lean.expected.out b/tests/lean/binopQuotPrecheck.lean.expected.out
new file mode 100644
index 000000000000..d44244f04aaf
--- /dev/null
+++ b/tests/lean/binopQuotPrecheck.lean.expected.out
@@ -0,0 +1,3 @@
+binopQuotPrecheck.lean:56:41-56:42: error: unknown identifier 'a' at quotation precheck; you can use `set_option quotPrecheck false` to disable this check.
+binopQuotPrecheck.lean:61:49-61:50: error: unknown identifier 'a' at quotation precheck; you can use `set_option quotPrecheck false` to disable this check.
+binopQuotPrecheck.lean:66:51-66:52: error: unknown identifier 'a' at quotation precheck; you can use `set_option quotPrecheck false` to disable this check.