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

@@ -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

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

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.