From f9745217832568aa45aa8d2b055673770becf9bd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 10 Aug 2020 11:15:44 -0700
Subject: [PATCH] fix: missing `node`

---
 src/Lean/Elab/Match.lean  | 23 ++++++++++++++++++++++-
 src/Lean/Parser/Term.lean |  2 +-
 2 files changed, 23 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index 2ebaa132c1..7626b9093d 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -17,6 +17,23 @@ private def expandSimpleMatchWithType (stx discr lhsVar type rhs : Syntax) (expe
 newStx ← `(let $lhsVar : $type := $discr; $rhs);
 withMacroExpansion stx newStx $ elabTerm newStx expectedType?
 
+/-
+
+```
+def matchDiscr := optIdent >> termParser
+parser!:leadPrec "match " >> sepBy1 matchDiscr ", " >> optType >> " with " >> matchAlts
+```
+Remark the `optIdent` must be `none` at `matchDiscr`. They are expanded by `expandMatchDiscr?`.
+-/
+private def elabMatchCore (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do
+tryPostponeIfNoneOrMVar expectedType?;
+let discrs := (stx.getArg 1).getArgs.getSepElems.map fun d => d.getArg 1;
+throwError stx ("WIP " ++ stx ++ "\n" ++ toString discrs)
+
+/-- Expand discriminants of the form `h : t` -/
+private def expandMatchDiscr? (stx : Syntax) : MacroM (Option Syntax) := do
+pure none -- TODO
+
 -- parser! "match " >> sepBy1 termParser ", " >> optType >> " with " >> matchAlts
 @[builtinTermElab «match»] def elabMatch : TermElab :=
 fun stx expectedType? => match_syntax stx with
@@ -24,7 +41,11 @@ fun stx expectedType? => match_syntax stx with
   | `(match $discr:term with | $y:ident => $rhs:term)         => expandSimpleMatch stx discr y rhs expectedType?
   | `(match $discr:term : $type with $y:ident => $rhs:term)   => expandSimpleMatchWithType stx discr y type rhs expectedType?
   | `(match $discr:term : $type with | $y:ident => $rhs:term) => expandSimpleMatchWithType stx discr y type rhs expectedType?
-  | _ => throwUnsupportedSyntax
+  | _ => do
+    stxNew? ← liftMacroM $ expandMatchDiscr? stx;
+    match stxNew? with
+    | some stxNew => withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
+    | none        => elabMatchCore stx expectedType?
 
 end Term
 end Elab
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index b20ed8aeac..baee6ff4a5 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -106,7 +106,7 @@ withPosition $ fun pos =>
   (if optionalFirstBar then optional "| " else "| ") >>
   sepBy1 matchAlt (checkColGe pos.column "alternatives must be indented" >> "|")
 
-def matchDiscr := optIdent >> termParser
+def matchDiscr := parser! optIdent >> termParser
 
 @[builtinTermParser] def «match» := parser!:leadPrec "match " >> sepBy1 matchDiscr ", " >> optType >> " with " >> matchAlts
 @[builtinTermParser] def «nomatch»  := parser!:leadPrec "nomatch " >> termParser