From 4812f2aa648c5bb0610b17671b18fdfe9afd6d80 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 15 Dec 2020 18:26:50 +0100
Subject: [PATCH] chore: restore correct position for match errors

---
 src/Lean/Elab/Match.lean            | 20 ++++++++++++--------
 tests/lean/match1.lean.expected.out |  6 +++---
 tests/lean/run/macroid.lean         |  8 ++++----
 tests/lean/run/newfrontend2.lean    |  4 ++--
 4 files changed, 21 insertions(+), 17 deletions(-)

diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index 43cef0a4c9..cb7c98be2d 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -11,6 +11,7 @@ import Lean.Parser.Term
 
 namespace Lean.Elab.Term
 open Meta
+open Lean.Parser.Term
 
 /- This modules assumes "match"-expressions use the following syntax.
 
@@ -25,6 +26,7 @@ structure MatchAltView where
   ref      : Syntax
   patterns : Array Syntax
   rhs      : Syntax
+  deriving Inhabited
 
 private def expandSimpleMatch (stx discr lhsVar rhs : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do
   let newStx ← `(let $lhsVar := $discr; $rhs)
@@ -115,13 +117,15 @@ def expandMacrosInPatterns (matchAlts : Array MatchAltView) : MacroM (Array Matc
 
 /- Given `stx` a match-expression, return its alternatives. -/
 private def getMatchAlts : Syntax → Array MatchAltView
-  | `(match $discrs,* $[: $ty?]? with $[| $patternss,* => $rhss]*) =>
-    patternss.zipWith rhss fun patterns rhs => {
-      ref      := patterns[0],
-      patterns := patterns,
-      rhs      := rhs
-    }
-  | stx => dbgTrace s!"{stx}" fun _ => unreachable!
+  | `(match $discrs,* $[: $ty?]? with $alts:matchAlt*) =>
+    alts.map fun alt => match alt with
+      | `(matchAltExpr| | $patterns,* => $rhs) => {
+          ref      := alt,
+          patterns := patterns,
+          rhs      := rhs
+        }
+      | _ => unreachable!
+  | _ => unreachable!
 
 /--
   Auxiliary annotation used to mark terms marked with the "inaccessible" annotation `.(t)` and
@@ -451,7 +455,7 @@ partial def collect : Syntax → M Syntax
       discard <| processVar id
       let pat := stx[2]
       let pat ← collect pat
-      `(namedPattern $id $pat)
+      `(_root_.namedPattern $id $pat)
     else if k == `Lean.Parser.Term.inaccessible then
       pure stx
     else if k == strLitKind then
diff --git a/tests/lean/match1.lean.expected.out b/tests/lean/match1.lean.expected.out
index eb014efe8f..89a5352b4c 100644
--- a/tests/lean/match1.lean.expected.out
+++ b/tests/lean/match1.lean.expected.out
@@ -10,16 +10,16 @@
 4
 ---- inv
 10
-match1.lean:82:2: error: type mismatch during dependent match-elimination at pattern variable 'w' with type
+match1.lean:82:0: error: type mismatch during dependent match-elimination at pattern variable 'w' with type
   VecPred P Vec.nil
 expected type
   VecPred P tail✝
 [false, true, true]
-match1.lean:113:2: error: dependent match elimination failed, inaccessible pattern found
+match1.lean:113:0: error: dependent match elimination failed, inaccessible pattern found
   .(j + j)
 constructor expected
 [false, true, true]
-match1.lean:124:11: error: invalid match-expression, type of pattern variable 'a' contains metavariables
+match1.lean:124:0: error: invalid match-expression, type of pattern variable 'a' contains metavariables
   ?m
 fun (x : ?m × ?m) => ?m x : ?m × ?m → ?m
 fun (x : Nat × Nat) =>
diff --git a/tests/lean/run/macroid.lean b/tests/lean/run/macroid.lean
index 83c661799d..6205a2a308 100644
--- a/tests/lean/run/macroid.lean
+++ b/tests/lean/run/macroid.lean
@@ -1,19 +1,19 @@
 syntax "[" ident "↦" term "]" : term
-macro_rules `([$x ↦ $v]) => `(fun $x => $v)
+macro_rules | `([$x ↦ $v]) => `(fun $x => $v)
 
 #check [x ↦ x + 1]
 
 syntax "case!" ident ":" term "with" term "," term : term
-macro_rules `(case! $h : $c with $t, $e) => `((fun $h => cond $h $t $e) $c)
+macro_rules | `(case! $h : $c with $t, $e) => `((fun $h => cond $h $t $e) $c)
 
 #check case! h : 0 == 0 with h, not h
 
 syntax "case2!" ident ":" term "with" term "," term : term
-macro_rules `(case2! $h : $c with $t, $e) => `(let $h := $c; cond $h $t $e)
+macro_rules | `(case2! $h : $c with $t, $e) => `(let $h := $c; cond $h $t $e)
 
 #check case2! h : 0 == 0 with h, not h
 
 syntax "test" term : term
-macro_rules `(test $x:ident) => `(let $x := 0; $x)
+macro_rules | `(test $x:ident) => `(let $x := 0; $x)
 
 #check fun (x : Nat) => test x
diff --git a/tests/lean/run/newfrontend2.lean b/tests/lean/run/newfrontend2.lean
index 4f9f2c4347..984749b2ad 100644
--- a/tests/lean/run/newfrontend2.lean
+++ b/tests/lean/run/newfrontend2.lean
@@ -17,8 +17,8 @@ def x := 1
 
 #check foo x x
 
-#check match 1 with x => x + 1
-#check match 1 : Int with x => x + 1
+#check match 1 with | x => x + 1
+#check match 1 : Int with | x => x + 1
 #check match 1 with | x => x + 1
 #check match 1 : Int with | x => x + 1