From a0089d466760122295d4b1dabe4bd3e931222415 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 21 Feb 2024 04:46:26 -0800 Subject: [PATCH] fix: match pattern missing test --- src/Lean/Elab/PatternVar.lean | 13 +++++++++++++ tests/lean/binop_at_pattern_issue.lean | 5 +++++ tests/lean/binop_at_pattern_issue.lean.expected.out | 1 + 3 files changed, 19 insertions(+) create mode 100644 tests/lean/binop_at_pattern_issue.lean create mode 100644 tests/lean/binop_at_pattern_issue.lean.expected.out diff --git a/src/Lean/Elab/PatternVar.lean b/src/Lean/Elab/PatternVar.lean index 7b1d78b790..9904d18545 100644 --- a/src/Lean/Elab/PatternVar.lean +++ b/src/Lean/Elab/PatternVar.lean @@ -159,6 +159,19 @@ partial def collect (stx : Syntax) : M Syntax := withRef stx <| withFreshMacroSc discard <| processVar h ``(_root_.namedPattern $id $pat $h) else if k == ``Lean.Parser.Term.binop then + /- + We support `binop%` syntax in patterns because we + wanted to support `x+1` in patterns. + Recall that the `binop%` syntax was added to improve elaboration of some binary operators: `+` is one of them. + Recall that `HAdd.hAdd` is marked as `[match_pattern]` + TODO for a distant future: make this whole procedure extensible. + -/ + -- Check whether the `binop%` operator is marked with `[match_pattern]`, + -- We must check that otherwise Lean will accept operators that are not tagged with this annotation. + let some (.const fName _) ← resolveId? stx[1] "pattern" + | throwCtorExpected + unless hasMatchPatternAttribute (← getEnv) fName do + throwCtorExpected let lhs ← collect stx[2] let rhs ← collect stx[3] return stx.setArg 2 lhs |>.setArg 3 rhs diff --git a/tests/lean/binop_at_pattern_issue.lean b/tests/lean/binop_at_pattern_issue.lean new file mode 100644 index 0000000000..d5a4f422c7 --- /dev/null +++ b/tests/lean/binop_at_pattern_issue.lean @@ -0,0 +1,5 @@ +open Std BitVec +def f4 (v : Std.BitVec 32) : Nat := + match v with + | 10#20 ++ 0#12 => 0 -- Should be rejected since `++` does not have `[match_pattern]` + | _ => 1 diff --git a/tests/lean/binop_at_pattern_issue.lean.expected.out b/tests/lean/binop_at_pattern_issue.lean.expected.out new file mode 100644 index 0000000000..509b366db8 --- /dev/null +++ b/tests/lean/binop_at_pattern_issue.lean.expected.out @@ -0,0 +1 @@ +binop_at_pattern_issue.lean:4:4-4:17: error: invalid pattern, constructor or constant marked with '[match_pattern]' expected