From b0b922bae499e6380ed3e48ad8efb25c963d5aaf Mon Sep 17 00:00:00 2001
From: David Christiansen <david@davidchristiansen.dk>
Date: Thu, 5 Oct 2023 21:25:18 +0200
Subject: [PATCH] feat: list the valid case tags when the user writes an
 invalid one

Before, Lean would simply emit the message "tag not found". With this
change, it also tells the user what they could have written that would
be accepted.
---
 src/Lean/Elab/Tactic/BuiltinTactic.lean      | 30 ++++++++++++-
 tests/lean/caseSuggestions.lean              | 45 ++++++++++++++++++++
 tests/lean/caseSuggestions.lean.expected.out | 42 ++++++++++++++++++
 3 files changed, 116 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/caseSuggestions.lean
 create mode 100644 tests/lean/caseSuggestions.lean.expected.out

diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean
index ea22016709..e7fb5b0a0d 100644
--- a/src/Lean/Elab/Tactic/BuiltinTactic.lean
+++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean
@@ -369,12 +369,40 @@ private def getCaseGoals (tag : TSyntax ``binderIdent) : TacticM (MVarId × List
   let gs ← getUnsolvedGoals
   let g ← if let `(binderIdent| $tag:ident) := tag then
     let tag := tag.getId
-    let some g ← findTag? gs tag | throwError "tag not found"
+    let some g ← findTag? gs tag | notFound gs tag
     pure g
   else
     getMainGoal
   return (g, gs.erase g)
 
+where
+  -- When the case tag is not found, construct a message that tells
+  -- the user what they could have written
+  notFound (available : List MVarId) (tag : Name) := do
+    let firstLine := m!"Case tag {showTagName tag} not found."
+    -- We must filter out the anonymous name because there may be an
+    -- anonymous goal, but users shouldn't be mistakenly encouraged
+    -- to write `case anonymous`
+    match (← available.mapM getUserName).filter (· ≠ Name.anonymous) with
+    | [] =>
+      throwError "{firstLine}\n\nThere are no cases to select."
+    | [availableName] =>
+      throwError "{firstLine}\n\nThe only available case tag is {showTagName availableName}."
+    | availableNames =>
+      throwError "Case tag {showTagName tag} not found.\n\nAvailable tags:{commaList <| availableNames.map showTagName}"
+
+  getUserName (mv : MVarId) := do return (← mv.getDecl).userName
+
+  showTagName (tagName : Name) : MessageData := m!"'{tagName}'"
+
+  -- Construct a comma-separated list that renders one per line,
+  -- indented, if it's too long
+  commaList (items : List MessageData) : MessageData :=
+    let sep := MessageData.ofFormat "," ++ Format.line
+    .group <| .nest 2 <|
+    .ofFormat .line ++ .joinSep items sep
+
+
 @[builtin_tactic «case»] def evalCase : Tactic
   | stx@`(tactic| case $[$tag $hs*]|* =>%$arr $tac:tacticSeq) =>
     for tag in tag, hs in hs do
diff --git a/tests/lean/caseSuggestions.lean b/tests/lean/caseSuggestions.lean
new file mode 100644
index 0000000000..5b212658cc
--- /dev/null
+++ b/tests/lean/caseSuggestions.lean
@@ -0,0 +1,45 @@
+/-!
+
+  # Provide case alternatives in "nonexistent tag" message
+
+  Test that the available case tags are suggested when a nonexistent
+  tag is requested. -/
+
+/-!
+  This example tests what happens when no cases are available. -/
+theorem noCases : Nat := by
+  case nonexistent =>
+    skip
+
+/-!
+  This example tests what happens when just one case is available, but
+  it wasn't picked. -/
+
+theorem oneCase : Nat := by
+  cases ()
+  case nonexistent =>
+    skip
+
+/-!
+  Check varying numbers of cases to make sure the pretty-print setup for
+  the list is correct. -/
+
+theorem twoCases : Nat := by
+  cases true
+  case nonexistent =>
+    skip
+
+theorem fourCases : Nat := by
+  cases true <;> cases true
+  case nonexistent =>
+    skip
+
+theorem eightCases : Nat := by
+  cases true <;> cases true <;> cases true
+  case nonexistent =>
+    skip
+
+theorem sixteenCases : Nat := by
+  cases true <;> cases true <;> cases true <;> cases true
+  case nonexistent =>
+    skip
diff --git a/tests/lean/caseSuggestions.lean.expected.out b/tests/lean/caseSuggestions.lean.expected.out
new file mode 100644
index 0000000000..eb7b2cb2cc
--- /dev/null
+++ b/tests/lean/caseSuggestions.lean.expected.out
@@ -0,0 +1,42 @@
+caseSuggestions.lean:11:2-12:8: error: Case tag 'nonexistent' not found.
+
+There are no cases to select.
+caseSuggestions.lean:20:2-21:8: error: Case tag 'nonexistent' not found.
+
+The only available case tag is 'unit'.
+caseSuggestions.lean:29:2-30:8: error: Case tag 'nonexistent' not found.
+
+Available tags: 'false', 'true'
+caseSuggestions.lean:34:2-35:8: error: Case tag 'nonexistent' not found.
+
+Available tags: 'false.false', 'false.true', 'true.false', 'true.true'
+caseSuggestions.lean:39:2-40:8: error: Case tag 'nonexistent' not found.
+
+Available tags:
+  'false.false.false',
+  'false.false.true',
+  'false.true.false',
+  'false.true.true',
+  'true.false.false',
+  'true.false.true',
+  'true.true.false',
+  'true.true.true'
+caseSuggestions.lean:44:2-45:8: error: Case tag 'nonexistent' not found.
+
+Available tags:
+  'false.false.false.false',
+  'false.false.false.true',
+  'false.false.true.false',
+  'false.false.true.true',
+  'false.true.false.false',
+  'false.true.false.true',
+  'false.true.true.false',
+  'false.true.true.true',
+  'true.false.false.false',
+  'true.false.false.true',
+  'true.false.true.false',
+  'true.false.true.true',
+  'true.true.false.false',
+  'true.true.false.true',
+  'true.true.true.false',
+  'true.true.true.true'