Simplify, fix table in presence of hidden names

src/Lean/Elab/PreDefinition/WF/GuessLex.lean

@@ -582,7 +582,7 @@ def formatTable : Array (Array String) → String := fun xss => Id.run do
       str := str ++ "\n"
   return str
 
-/-- Concice textual representation of the source location of a recursive call  -/
+/-- Concise textual representation of the source location of a recursive call  -/
 def RecCallWithContext.posString (rcc : RecCallWithContext) : MetaM String := do
   let fileMap ← getFileMap
   let .some pos := rcc.ref.getPos? | return ""
@@ -598,24 +598,21 @@ def RecCallWithContext.posString (rcc : RecCallWithContext) : MetaM String := do
   return s!"{position.line}:{position.column}{endPosStr}"
 
 
-def explainNonMutualFailure (varNames : Array Name) (measures : Array MutualMeasure)
-    (rcs : Array RecCallCache) : MetaM Format := do
-
-  let header := measures.map fun
-    | .args #[idx] => varNames[idx]!.eraseMacroScopes.toString
-    | _ => unreachable! -- should not happen in non-mutual case
-
+/-- Explain what we found out about the recursive calls (non-mutual case) -/
+def explainNonMutualFailure (varNames : Array Name) (rcs : Array RecCallCache) : MetaM Format := do
+  let header := varNames.map (·.eraseMacroScopes.toString)
   let mut table : Array (Array String) := #[#[""] ++ header]
   for i in [:rcs.size], rc in rcs do
     let mut row := #[s!"{i+1}) {← rc.rcc.posString}"]
-    for measureIdx in [:measures.size] do
-      row := row.push (← rc.prettyEntry measureIdx measureIdx)
+    for argIdx in [:varNames.size] do
+      row := row.push (← rc.prettyEntry argIdx argIdx)
     table := table.push row
 
   return formatTable table
 
+/-- Explain what we found out about the recursive calls (mutual case) -/
 def explainMutualFailure (declNames : Array Name) (varNamess : Array (Array Name))
-  (_measures : Array MutualMeasure) (rcs : Array RecCallCache) : MetaM Format := do
+    (rcs : Array RecCallCache) : MetaM Format := do
   let mut r := Format.nil
 
   for rc in rcs do
@@ -644,13 +641,13 @@ def explainMutualFailure (declNames : Array Name) (varNamess : Array (Array Name
   return r
 
 def explainFailure (declNames : Array Name) (varNamess : Array (Array Name))
-  (measures : Array MutualMeasure) (rcs : Array RecCallCache) : MetaM Format := do
+    (rcs : Array RecCallCache) : MetaM Format := do
   let mut r : Format := "The arguments relate at each recursive call as follows:\n" ++
-           "(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)\n"
+    "(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)\n"
   if declNames.size = 1 then
-    r := r ++ (← explainNonMutualFailure varNamess[0]! measures rcs)
+    r := r ++ (← explainNonMutualFailure varNamess[0]! rcs)
   else
-    r := r ++ (← explainMutualFailure declNames varNamess measures rcs)
+    r := r ++ (← explainMutualFailure declNames varNamess rcs)
   return r
 
 end Lean.Elab.WF.GuessLex
@@ -693,7 +690,7 @@ def guessLex (preDefs : Array PreDefinition)  (unaryPreDef : PreDefinition)
     let wf ← buildTermWF (preDefs.map (·.declName)) varNamess solution
     return wf
   | .none =>
-    let explanation ← explainFailure (preDefs.map (·.declName)) varNamess measures rcs
+    let explanation ← explainFailure (preDefs.map (·.declName)) varNamess rcs
     Lean.throwError <| "Could not find a decreasing measure.\n" ++
       explanation ++ "\n" ++
       "Please use `termination_by` to specify a decreasing measure."

tests/lean/guessLexFailures.lean.expected.out

@@ -46,10 +46,10 @@ Please use `termination_by` to specify a decreasing measure.
 guessLexFailures.lean:37:0-43:31: error: Could not find a decreasing measure.
 The arguments relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
-           x1 x2 x4
-1) 39:6-27  =  =  _
-2) 40:6-25  =  ?  _
-3) 41:6-25  <  _  _
+           x1 x2 x3 x4
+1) 39:6-27  =  =  _  =
+2) 40:6-25  =  ?  _  <
+3) 41:6-25  <  _  _  _
 Please use `termination_by` to specify a decreasing measure.
 guessLexFailures.lean:48:0-54:31: error: Could not find a decreasing measure.
 The arguments relate at each recursive call as follows: