From b22e035b6f70865da0889f10bedc1414209f07aa Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 17 Nov 2020 18:12:28 +0100
Subject: [PATCH] fix: pretty print empty matchers as `nomatch`

/cc @leodemoura
---
 src/Lean/Delaborator.lean           | 18 ++++++++++++------
 tests/lean/match1.lean              |  2 ++
 tests/lean/match1.lean.expected.out |  1 +
 3 files changed, 15 insertions(+), 6 deletions(-)

diff --git a/src/Lean/Delaborator.lean b/src/Lean/Delaborator.lean
index feac4fcaf6..a8c596be41 100644
--- a/src/Lean/Delaborator.lean
+++ b/src/Lean/Delaborator.lean
@@ -442,15 +442,21 @@ def delabAppMatch : Delab := whenPPOption getPPNotation do
       else
         pure { st with moreArgs := st.moreArgs.push (← delab) })
 
-  if st.rhss.size < st.info.altNumParams.size then
+  if st.discrs.size < st.info.numDiscrs || st.rhss.size < st.info.altNumParams.size then
     -- underapplied
     failure
 
-  let pats ← delabPatterns st
-  let discrs := st.discrs.map fun discr => mkNode `Lean.Parser.Term.matchDiscr #[mkNullNode, discr]
-  let alts := pats.zipWith st.rhss fun pat rhs => mkNode `Lean.Parser.Term.matchAlt #[pat, mkAtom "=>", rhs]
-  let stx ← `(match $(mkSepArray discrs (mkAtom ",")):matchDiscr* with | $(mkSepArray alts (mkAtom "|")):matchAlt*)
-  Syntax.mkApp stx st.moreArgs
+  match st.discrs, st.rhss with
+  | #[discr], #[] =>
+    let stx ← `(nomatch $discr)
+    Syntax.mkApp stx st.moreArgs
+  | _,        #[] => failure
+  | _,        _   =>
+    let discrs := st.discrs.map fun discr => mkNode `Lean.Parser.Term.matchDiscr #[mkNullNode, discr]
+    let pats ← delabPatterns st
+    let alts := pats.zipWith st.rhss fun pat rhs => mkNode `Lean.Parser.Term.matchAlt #[pat, mkAtom "=>", rhs]
+    let stx ← `(match $(mkSepArray discrs (mkAtom ",")):matchDiscr* with | $(mkSepArray alts (mkAtom "|")):matchAlt*)
+    Syntax.mkApp stx st.moreArgs
 
 @[builtinDelab mdata]
 def delabMData : Delab := do
diff --git a/tests/lean/match1.lean b/tests/lean/match1.lean
index 3aa7861578..79e72797ce 100644
--- a/tests/lean/match1.lean
+++ b/tests/lean/match1.lean
@@ -148,3 +148,5 @@ def g {α} : List α → Nat
   | _   => 0
 
 #check g.match_1
+
+#check fun (e : Empty) => (nomatch e : False)
diff --git a/tests/lean/match1.lean.expected.out b/tests/lean/match1.lean.expected.out
index f45a5b9748..ce733876eb 100644
--- a/tests/lean/match1.lean.expected.out
+++ b/tests/lean/match1.lean.expected.out
@@ -48,3 +48,4 @@ fun (x : Array Nat) =>
   | x_1 => 4 : Array Nat → Nat
 g.match_1 : (motive : List ?m → Sort _) →
   (x : List ?m) → ((a : ?m) → motive [a]) → ((x_1 : List ?m) → motive x_1) → motive x
+fun (e : Empty) => nomatch e : (e : Empty) → (fun (e_1 : Empty) => False) e