feat: termination_by?

src/Lean/Elab/PreDefinition/Main.lean

@@ -121,8 +121,7 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLC
       preDefs.forM (·.termination.ensureNone "partial")
     else
       try
-        let hasHints := preDefs.any  fun preDef =>
-          preDef.termination.decreasing_by?.isSome || preDef.termination.termination_by?.isSome
+        let hasHints := preDefs.any fun preDef => preDef.termination.isNotNone
         if hasHints then
           wfRecursion preDefs
         else

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

@@ -8,6 +8,7 @@ import Lean.Util.HasConstCache
 import Lean.Meta.Match.MatcherApp.Transform
 import Lean.Meta.Tactic.Cleanup
 import Lean.Meta.Tactic.Refl
+import Lean.Meta.Tactic.TryThis
 import Lean.Elab.Quotation
 import Lean.Elab.RecAppSyntax
 import Lean.Elab.PreDefinition.Basic
@@ -702,17 +703,19 @@ def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition)
   -- Collect all recursive calls and extract their context
   let recCalls ← collectRecCalls unaryPreDef fixedPrefixSize arities
   let recCalls := filterSubsumed recCalls
-  let rcs ← recCalls.mapM (RecCallCache.mk (preDefs.map (·.termination.decreasing_by?)) ·)
+  let rcs ← recCalls.mapM (RecCallCache.mk (preDefs.map (·.termination.decreasingBy?)) ·)
   let callMatrix := rcs.map (inspectCall ·)
 
   match ← liftMetaM <| solve measures callMatrix with
   | .some solution => do
     let wf ← buildTermWF originalVarNamess varNamess solution
 
-    if showInferredTerminationBy.get (← getOptions) then
-      let wf' := trimTermWF extraParamss wf
-      for preDef in preDefs, term in wf' do
-        logInfoAt preDef.ref m!"Inferred termination argument: {← term.unexpand}"
+    let wf' := trimTermWF extraParamss wf
+    for preDef in preDefs, term in wf' do
+      if showInferredTerminationBy.get (← getOptions) then
+        logInfoAt preDef.ref m!"Inferred termination argument:\n{← term.unexpand}"
+      if let some ref := preDef.termination.terminationBy?? then
+        Tactic.TryThis.addSuggestion ref (← term.unexpand)
 
     return wf
   | .none =>

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

@@ -94,12 +94,12 @@ def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
     return (← packMutual fixedPrefixSize preDefs unaryPreDefs, fixedPrefixSize)
 
   let wf ← do
-    let (preDefsWith, preDefsWithout) := preDefs.partition (·.termination.termination_by?.isSome)
+    let (preDefsWith, preDefsWithout) := preDefs.partition (·.termination.terminationBy?.isSome)
     if preDefsWith.isEmpty then
       -- No termination_by anywhere, so guess one
       guessLex preDefs unaryPreDef fixedPrefixSize
     else if preDefsWithout.isEmpty then
-      pure <| preDefsWith.map (·.termination.termination_by?.get!)
+      pure <| preDefsWith.map (·.termination.terminationBy?.get!)
     else
       -- Some have, some do not, so report errors
       preDefsWithout.forM fun preDef => do
@@ -114,7 +114,7 @@ def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
       trace[Elab.definition.wf] "wfRel: {wfRel}"
       let (value, envNew) ← withoutModifyingEnv' do
         addAsAxiom unaryPreDef
-        let value ← mkFix unaryPreDef prefixArgs wfRel (preDefs.map (·.termination.decreasing_by?))
+        let value ← mkFix unaryPreDef prefixArgs wfRel (preDefs.map (·.termination.decreasingBy?))
         eraseRecAppSyntaxExpr value
       /- `mkFix` invokes `decreasing_tactic` which may add auxiliary theorems to the environment. -/
       let value ← unfoldDeclsFrom envNew value

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

@@ -27,7 +27,7 @@ structure TerminationBy where
   deriving Inhabited
 
 open Parser.Termination in
-def TerminationBy.unexpand (wf : TerminationBy) : MetaM Syntax := do
+def TerminationBy.unexpand (wf : TerminationBy) : MetaM (TSyntax ``terminationBy) := do
   -- TODO: Why can I not just use $wf.vars in the quotation below?
   let vars : TSyntaxArray `ident := wf.vars.map (⟨·.raw⟩)
   if vars.isEmpty then
@@ -50,8 +50,9 @@ is what `Term.runTactic` expects.
  -/
 structure TerminationHints where
   ref : Syntax
-  termination_by? : Option TerminationBy
-  decreasing_by?  : Option DecreasingBy
+  terminationBy?? : Option Syntax
+  terminationBy? : Option TerminationBy
+  decreasingBy?  : Option DecreasingBy
   /-- Here we record the number of parameters past the `:`. It is set by
   `TerminationHints.rememberExtraParams` and used as folows:
 
@@ -63,19 +64,27 @@ structure TerminationHints where
   extraParams : Nat
   deriving Inhabited
 
-def TerminationHints.none : TerminationHints := ⟨.missing, .none, .none, 0⟩
+def TerminationHints.none : TerminationHints := ⟨.missing, .none, .none, .none, 0⟩
 
 /-- Logs warnings when the `TerminationHints` are present.  -/
 def TerminationHints.ensureNone (hints : TerminationHints) (reason : String): CoreM Unit := do
-  match hints.termination_by?, hints.decreasing_by? with
-  | .none, .none => pure ()
-  | .none, .some dec_by =>
+  match hints.terminationBy??, hints.terminationBy?, hints.decreasingBy? with
+  | .none, .none, .none => pure ()
+  | .none, .none, .some dec_by =>
     logErrorAt dec_by.ref m!"unused `decreasing_by`, function is {reason}"
-  | .some term_by, .none =>
+  | .some term_by?, .none, .none =>
+    logErrorAt term_by? m!"unused `termination_by?`, function is {reason}"
+  | .none, .some term_by, .none =>
     logErrorAt term_by.ref m!"unused `termination_by`, function is {reason}"
-  | .some _, .some _ =>
+  | _, _, _ =>
     logErrorAt hints.ref m!"unused termination hints, function is {reason}"
 
+/-- True if any form of termination hint is present. -/
+def TerminationHints.isNotNone (hints : TerminationHints) : Bool :=
+  hints.terminationBy??.isSome ||
+  hints.terminationBy?.isSome ||
+  hints.decreasingBy?.isSome
+
 /--
 Remembers `extraParams` for later use. Needs to happen early enough where we still know
 how many parameters came from the function header (`headerParams`).
@@ -111,19 +120,23 @@ def elabTerminationHints {m} [Monad m] [MonadError m] (stx : TSyntax ``suffix) :
   if let .missing := stx.raw then
     return { TerminationHints.none with ref := stx }
   match stx with
-  | `(suffix| $[$t?:terminationBy]? $[$d?:decreasingBy]? ) => do
-    let termination_by? ← t?.mapM fun t => match t with
-      | `(terminationBy|termination_by $vars* => $body) =>
-        if vars.isEmpty then
-          throwErrorAt t "no extra parameters bounds, please omit the `=>`"
-        else
-          pure {ref := t, vars, body}
-      | `(terminationBy|termination_by $body:term) => pure {ref := t, vars := #[], body}
+  | `(suffix| $[$t?]? $[$d?:decreasingBy]? ) => do
+    let terminationBy?? : Option Syntax ← if let some t := t? then match t with
+      | `(terminationBy?|termination_by?) => pure (some t)
+      | _ => pure none
+      else pure none
+    let terminationBy? : Option TerminationBy ← if let some t := t? then match t with
+      | `(terminationBy|termination_by => $_body) =>
+        throwErrorAt t "no extra parameters bounds, please omit the `=>`"
+      | `(terminationBy|termination_by $vars* => $body) => pure (some {ref := t, vars, body})
+      | `(terminationBy|termination_by $body:term) => pure (some {ref := t, vars := #[], body})
+      | `(terminationBy?|termination_by?) => pure none
       | _ => throwErrorAt t "unexpected `termination_by` syntax"
-    let decreasing_by? ← d?.mapM fun d => match d with
+      else pure none
+    let decreasingBy? ← d?.mapM fun d => match d with
       | `(decreasingBy|decreasing_by $tactic) => pure {ref := d, tactic}
       | _ => throwErrorAt d "unexpected `decreasing_by` syntax"
-    return { ref := stx, termination_by?, decreasing_by?, extraParams := 0 }
+    return { ref := stx, terminationBy??, terminationBy?, decreasingBy?, extraParams := 0 }
   | _ => throwErrorAt stx s!"Unexpected Termination.suffix syntax: {stx} of kind {stx.raw.getKind}"
 
 end Lean.Elab.WF

src/Lean/Parser/Term.lean

@@ -118,14 +118,18 @@ def example (a : Nat) : Nat → Nat → Nat :=
 termination_by b c => a - b
 ```
 
-If omitted, a termination argument will be inferred.
+If omitted, a termination argument will be inferred. If written as `termination_by?`,
+the inferrred termination argument will be suggested.
 -/
 def terminationBy := leading_parser
-  ppDedent ppLine >>
   "termination_by " >>
   optional (atomic (many (ppSpace >> (ident <|> "_")) >> " => ")) >>
   termParser
 
+@[inherit_doc terminationBy]
+def terminationBy? := leading_parser
+  "termination_by?"
+
 /--
 Manually prove that the termination argument (as specified with `termination_by` or inferred)
 decreases at each recursive call.
@@ -139,7 +143,7 @@ def decreasingBy := leading_parser
 Termination hints are `termination_by` and `decreasing_by`, in that order.
 -/
 def suffix := leading_parser
-  optional terminationBy >> optional decreasingBy
+  optional (ppDedent ppLine >> (terminationBy? <|> terminationBy)) >> optional decreasingBy
 
 end Termination
 

stage0/src/stdlib_flags.h

@@ -8,7 +8,7 @@ options get_default_options() {
     // switch to `true` for ABI-breaking changes affecting meta code
     opts = opts.update({"interpreter", "prefer_native"}, false);
     // switch to `true` for changing built-in parsers used in quotations
-    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false);
+    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true);
     // toggling `parseQuotWithCurrentStage` may also require toggling the following option if macros/syntax
     // with custom precheck hooks were affected
     opts = opts.update({"quotPrecheck"}, true);

tests/lean/guessLex.lean.expected.out

@@ -1,41 +1,41 @@
-Inferred termination argument: 
+Inferred termination argument:
 termination_by (sizeOf n, sizeOf m)
-Inferred termination argument: 
+Inferred termination argument:
 termination_by (sizeOf m, sizeOf n)
-Inferred termination argument: 
+Inferred termination argument:
 termination_by (sizeOf n, sizeOf m)
-Inferred termination argument: 
+Inferred termination argument:
 termination_by x1 x2 => (sizeOf x2, sizeOf x1)
-Inferred termination argument: 
+Inferred termination argument:
 termination_by x1 => sizeOf x1
-Inferred termination argument: 
+Inferred termination argument:
 termination_by x1 => sizeOf x1
-Inferred termination argument: 
+Inferred termination argument:
 termination_by x1 => sizeOf x1
-Inferred termination argument: 
+Inferred termination argument:
 termination_by x1 => sizeOf x1
-Inferred termination argument: 
+Inferred termination argument:
 termination_by x1 => (sizeOf x1, 0)
-Inferred termination argument: 
+Inferred termination argument:
 termination_by (sizeOf n, 1)
-Inferred termination argument: 
+Inferred termination argument:
 termination_by (sizeOf m, sizeOf n)
-Inferred termination argument: 
+Inferred termination argument:
 termination_by x1 x2 x3 x4 x5 x6 x7 x8 =>
   (sizeOf x8, sizeOf x7, sizeOf x6, sizeOf x5, sizeOf x4, sizeOf x3, sizeOf x2, sizeOf x1)
-Inferred termination argument: 
+Inferred termination argument:
 termination_by x1 x2 => (sizeOf x1, sizeOf x2)
-Inferred termination argument: 
+Inferred termination argument:
 termination_by (sizeOf a, 1)
-Inferred termination argument: 
+Inferred termination argument:
 termination_by (sizeOf a, 0)
-Inferred termination argument: 
+Inferred termination argument:
 termination_by x2' => sizeOf x2'
-Inferred termination argument: 
+Inferred termination argument:
 termination_by x2 => sizeOf x2
-Inferred termination argument: 
+Inferred termination argument:
 termination_by x2 => SizeOf.sizeOf x2
-Inferred termination argument: 
+Inferred termination argument:
 termination_by x1 x2 => SizeOf.sizeOf x1
-Inferred termination argument: 
+Inferred termination argument:
 termination_by x2 => SizeOf.sizeOf x2

tests/lean/guessLexTricky.lean.expected.out

@@ -1,6 +1,6 @@
-Inferred termination argument: 
+Inferred termination argument:
 termination_by (sizeOf y, 1, 0)
-Inferred termination argument: 
+Inferred termination argument:
 termination_by (sizeOf y, 0, 1)
-Inferred termination argument: 
+Inferred termination argument:
 termination_by (sizeOf y, 0, 0)

tests/lean/guessLexTricky2.lean.expected.out

@@ -1,4 +1,4 @@
-Inferred termination argument: 
+Inferred termination argument:
 termination_by x1 x2 x3 => (sizeOf x1, sizeOf x2, 0)
-Inferred termination argument: 
+Inferred termination argument:
 termination_by x1 x2 x3 => (sizeOf x1, sizeOf x2, 1)

tests/lean/interactive/terminationBySuggestion.lean

@@ -0,0 +1,7 @@
+
+def ackermann (n m : Nat) := match n, m with
+  | 0, m => m + 1
+  | .succ n, 0 => ackermann n 1
+  | .succ n, .succ m => ackermann n (ackermann (n + 1) m)
+termination_by?
+   --^ codeAction

tests/lean/interactive/terminationBySuggestion.lean.expected.out

@@ -0,0 +1,12 @@
+{"title": "Try this: termination_by (sizeOf n, sizeOf m)",
+ "kind": "quickfix",
+ "isPreferred": true,
+ "edit":
+ {"documentChanges":
+  [{"textDocument":
+    {"version": 1, "uri": "file:///terminationBySuggestion.lean"},
+    "edits":
+    [{"range":
+      {"start": {"line": 5, "character": 0},
+       "end": {"line": 5, "character": 15}},
+      "newText": "termination_by (sizeOf n, sizeOf m)"}]}]}}