From 8fa36c7730bfd139d5cdaa89dda6c3ccfb00002b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 28 Apr 2024 01:56:28 +0200 Subject: [PATCH] fix: `match_expr` parser (#4007) closes #3989 closes #3990 --- src/Lean/Parser/Term.lean | 2 +- tests/lean/3989_1.lean | 3 +++ tests/lean/3989_1.lean.expected.out | 1 + tests/lean/3989_2.lean | 6 ++++++ tests/lean/3989_2.lean.expected.out | 2 ++ 5 files changed, 13 insertions(+), 1 deletion(-) create mode 100644 tests/lean/3989_1.lean create mode 100644 tests/lean/3989_1.lean.expected.out create mode 100644 tests/lean/3989_2.lean create mode 100644 tests/lean/3989_2.lean.expected.out diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 6ffe3e4be7..e71e7788bb 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -870,7 +870,7 @@ def matchExprElseAlt (rhsParser : Parser) := leading_parser "| " >> ppIndent (ho def matchExprAlts (rhsParser : Parser) := leading_parser withPosition $ many (ppLine >> checkColGe "irrelevant" >> notFollowedBy (symbol "| " >> " _ ") "irrelevant" >> matchExprAlt rhsParser) - >> (ppLine >> checkColGe "irrelevant" >> matchExprElseAlt rhsParser) + >> (ppLine >> checkColGe "else-alternative for `match_expr`, i.e., `| _ => ...`" >> matchExprElseAlt rhsParser) @[builtin_term_parser] def matchExpr := leading_parser:leadPrec "match_expr " >> termParser >> " with" >> ppDedent (matchExprAlts termParser) diff --git a/tests/lean/3989_1.lean b/tests/lean/3989_1.lean new file mode 100644 index 0000000000..adbbfb2f42 --- /dev/null +++ b/tests/lean/3989_1.lean @@ -0,0 +1,3 @@ +def foo (ty : Expr) : MetaM Expr := + match_expr ty with + | Nat => sorry diff --git a/tests/lean/3989_1.lean.expected.out b/tests/lean/3989_1.lean.expected.out new file mode 100644 index 0000000000..188b2bb20a --- /dev/null +++ b/tests/lean/3989_1.lean.expected.out @@ -0,0 +1 @@ +3989_1.lean:4:0: error: expected else-alternative for `match_expr`, i.e., `| _ => ...` diff --git a/tests/lean/3989_2.lean b/tests/lean/3989_2.lean new file mode 100644 index 0000000000..962415b0c1 --- /dev/null +++ b/tests/lean/3989_2.lean @@ -0,0 +1,6 @@ +def foo (ty : Expr) : MetaM Expr := + match_expr ty with + | Nat => sorry + | BitVec n => sorry + +#check Nat diff --git a/tests/lean/3989_2.lean.expected.out b/tests/lean/3989_2.lean.expected.out new file mode 100644 index 0000000000..4e1569eb91 --- /dev/null +++ b/tests/lean/3989_2.lean.expected.out @@ -0,0 +1,2 @@ +3989_2.lean:6:0: error: expected else-alternative for `match_expr`, i.e., `| _ => ...` +Nat : Type