feat: process termination_by syntax

src/Lean/Elab/PreDefinition/Main.lean

@@ -89,10 +89,10 @@ def addPreDefinitions (preDefs : Array PreDefinition) (hints : TerminationHints)
       let mut decrTactic? := none
       if let some wf := terminationBy.find? (preDefs.map (·.declName)) then
         wf? := some wf
-        terminationBy := terminationBy.erase (preDefs.map (·.declName))
+        terminationBy := terminationBy.markAsUsed (preDefs.map (·.declName))
       if let some { ref, value := decrTactic } := decreasingBy.find? (preDefs.map (·.declName)) then
         decrTactic? := some (← withRef ref `(by $decrTactic))
-        decreasingBy := decreasingBy.erase (preDefs.map (·.declName))
+        decreasingBy := decreasingBy.markAsUsed (preDefs.map (·.declName))
       if wf?.isSome || decrTactic?.isSome then
         wfRecursion preDefs wf? decrTactic?
       else
@@ -103,8 +103,8 @@ def addPreDefinitions (preDefs : Array PreDefinition) (hints : TerminationHints)
           (fun msg =>
             let preDefMsgs := preDefs.toList.map (MessageData.ofExpr $ mkConst ·.declName)
             m!"fail to show termination for{indentD (MessageData.joinSep preDefMsgs Format.line)}\nwith errors\n{msg}")
-  liftMacroM <| terminationBy.ensureIsEmpty
-  liftMacroM <| decreasingBy.ensureIsEmpty
+  liftMacroM <| terminationBy.ensureAllUsed
+  liftMacroM <| decreasingBy.ensureAllUsed
 
 builtin_initialize
   registerTraceClass `Elab.definition.body

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

@@ -21,6 +21,8 @@ def elabWFRel (unaryPreDef : PreDefinition) (wf? : Option TerminationWF) : TermE
       let pendingMVarIds ← getMVars wfRel
       discard <| logUnassignedUsingErrorInfos pendingMVarIds
       return wfRel
+  | some (TerminationWF.ext clique) =>
+    throwError "`termination_by` syntax is being modified/simplified. To use the old syntax, please use `termination_by'` instead"
   | none =>
     -- TODO: try to synthesize some default relation
     throwError "'termination_by' modifier missing"

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

@@ -7,6 +7,8 @@ import Lean.Parser.Command
 
 namespace Lean.Elab.WF
 
+/- Support for `decreasing_by` and `termination_by'` notations -/
+
 structure TerminationHintValue where
   ref   : Syntax
   value : Syntax
@@ -44,7 +46,7 @@ def expandTerminationHint (terminationHint? : Option Syntax) (cliques : Array (A
   else
     return TerminationHint.none
 
-def TerminationHint.erase (t : TerminationHint) (clique : Array Name) : TerminationHint :=
+def TerminationHint.markAsUsed (t : TerminationHint) (clique : Array Name) : TerminationHint :=
   match t with
   | TerminationHint.none   => TerminationHint.none
   | TerminationHint.one .. => TerminationHint.none
@@ -65,37 +67,131 @@ def TerminationHint.find? (t : TerminationHint) (clique : Array Name) : Option T
   | TerminationHint.one v  => some v
   | TerminationHint.many m => clique.findSome? m.find?
 
-def TerminationHint.ensureIsEmpty (t : TerminationHint) : MacroM Unit := do
+def TerminationHint.ensureAllUsed (t : TerminationHint) : MacroM Unit := do
   match t with
   | TerminationHint.one v   => Macro.throwErrorAt v.ref "unused termination hint element"
   | TerminationHint.many m  => m.forM fun _ v => Macro.throwErrorAt v.ref "unused termination hint element"
   | _ => pure ()
 
+/- Support for `termination_by` notation -/
+
+structure TerminationByElement where
+  ref       : Syntax
+  declName  : Name
+  vars      : Array Syntax
+  body      : Syntax
+  implicit  : Bool
+  deriving Inhabited
+
+structure TerminationByClique where
+  elements : Array TerminationByElement
+  used     : Bool := false
+
 inductive TerminationBy where
   | core (hint : TerminationHint)
+  | ext  (cliques : Array TerminationByClique)
+  deriving Inhabited
 
 inductive TerminationWF where
   | core (stx : Syntax)
+  | ext  (clique : Array TerminationByElement)
+
+/-
+```
+def terminationByElement   := leading_parser ppLine >> (ident <|> "_") >> many (ident <|> "_") >> " => " >> termParser >> optional ";"
+def terminationBy          := leading_parser ppLine >> "termination_by " >> many1chIndent terminationByElement
+```
+-/
+private def expandTerminationByNonCore (hint : Syntax) (cliques : Array (Array Name)) : MacroM TerminationBy := do
+  let elementStxs := hint[1].getArgs
+  let mut alreadyFound : NameSet := {}
+  let mut elseElemStx? := none
+  for elementStx in elementStxs do
+    let declStx := elementStx[0]
+    let vars := elementStx[1].getArgs
+    if declStx.isIdent then
+      let declSuffix := declStx.getId
+      if alreadyFound.contains declSuffix then
+        withRef elementStx <| Macro.throwError s!"invalid `termination_by` syntax, `{declSuffix}` case has already been provided"
+      alreadyFound := alreadyFound.insert declSuffix
+      if cliques.all fun clique => clique.all fun declName => !declSuffix.isSuffixOf declName then
+        withRef elementStx <| Macro.throwError s!"function '{declSuffix}' not found in current declaration"
+    else if elseElemStx?.isSome then
+      withRef elementStx <| Macro.throwError "invalid `termination_by` syntax, the else-case (i.e., `_ ... => ...`) has already been specified"
+    else
+      elseElemStx? := some elementStx
+  let toElement (declName : Name) (elementStx : Syntax) : TerminationByElement :=
+    let vars     := elementStx[1].getArgs
+    let implicit := !elementStx[0].isIdent
+    let body     := elementStx[3]
+    { ref := elementStx, declName, vars, implicit, body }
+  let mut result := #[]
+  let mut usedElse := false
+  for clique in cliques do
+    let mut elements := #[]
+    for declName in clique do
+      if let some elementStx := elementStxs.find? fun elementStx => elementStx[0].isIdent && elementStx[0].getId.isSuffixOf declName then
+        elements := elements.push (toElement declName elementStx)
+      else if let some elseElemStx := elseElemStx? then
+        elements := elements.push (toElement declName elseElemStx)
+        usedElse := true
+    unless elements.isEmpty do
+      if let some missing := clique.find? fun declName => elements.find? (·.declName == declName) |>.isNone then
+        withRef elements[0].ref <| Macro.throwError s!"invalid `termination_by` syntax, missing case for function '{missing}'"
+      result := result.push { elements }
+  unless usedElse do
+    withRef elseElemStx?.get! <| Macro.throwError s!"invalid `termination_by` syntax, unnecessary else-case"
+  return TerminationBy.ext result
 
 def expandTerminationBy (hint? : Option Syntax) (cliques : Array (Array Name)) : MacroM TerminationBy :=
   if let some hint := hint? then
     if hint.isOfKind ``Parser.Command.terminationByCore then
       return TerminationBy.core (← expandTerminationHint hint? cliques)
+    else if hint.isOfKind ``Parser.Command.terminationBy then
+      expandTerminationByNonCore hint cliques
     else
-      withRef hint <| Macro.throwError "`termination_by` syntax is being modified/simplified. To use the old syntax, please use `termination_by'` instead"
+      Macro.throwUnsupported
   else
       return TerminationBy.core TerminationHint.none
 
-def TerminationBy.erase (t : TerminationBy) (clique : Array Name) : TerminationBy :=
+def TerminationBy.markAsUsed (t : TerminationBy) (cliqueNames : Array Name) : TerminationBy :=
   match t with
-  | core hint => core (hint.erase clique)
+  | core hint   => core (hint.markAsUsed cliqueNames)
+  | ext cliques => ext <| cliques.map fun clique =>
+    if cliqueNames.any fun name => clique.elements.any fun elem => elem.declName == name then
+      { clique with used := true }
+    else
+      clique
 
-def TerminationBy.find? (t : TerminationBy) (clique : Array Name) : Option TerminationWF :=
+def TerminationBy.find? (t : TerminationBy) (cliqueNames : Array Name) : Option TerminationWF :=
   match t with
-  | core hint => hint.find? clique |>.map fun v => TerminationWF.core v.value
+  | core hint => hint.find? cliqueNames |>.map fun v => TerminationWF.core v.value
+  | ext cliques =>
+    cliques.findSome? fun clique =>
+      if cliqueNames.any fun name => clique.elements.any fun elem => elem.declName == name then
+        some <| TerminationWF.ext clique.elements
+      else
+        none
 
-def TerminationBy.ensureIsEmpty (t : TerminationBy) : MacroM Unit :=
+def TerminationByClique.allImplicit (c : TerminationByClique) : Bool :=
+  c.elements.all fun elem => elem.implicit
+
+def TerminationByClique.getExplicitElement? (c : TerminationByClique) : Option TerminationByElement :=
+  c.elements.find? (!·.implicit)
+
+def TerminationBy.ensureAllUsed (t : TerminationBy) : MacroM Unit :=
   match t with
-  | core hint => hint.ensureIsEmpty
+  | core hint => hint.ensureAllUsed
+  | ext cliques => do
+    let hasUsedAllImplicit := cliques.any fun c => c.allImplicit && c.used
+    let mut reportedAllImplicit := true
+    for clique in cliques do
+      unless clique.used do
+        if let some explicitElem := clique.getExplicitElement? then
+          Macro.throwErrorAt explicitElem.ref "unused termination hint element"
+        else if !hasUsedAllImplicit then
+          unless reportedAllImplicit do
+            reportedAllImplicit := true
+            Macro.throwErrorAt clique.elements[0].ref "unused termination hint element"
 
 end Lean.Elab.WF

src/Lean/Parser/Command.lean

@@ -33,7 +33,7 @@ def terminationHint (p : Parser) := terminationHintMany p <|> terminationHint1 p
 def terminationByCore := leading_parser "termination_by' " >> terminationHint termParser
 def decreasingBy := leading_parser "decreasing_by " >> terminationHint Tactic.tacticSeq
 
-def terminationByElement   := leading_parser ppLine >> many (ident <|> "_") >> " => " >> termParser >> optional ";"
+def terminationByElement   := leading_parser ppLine >> (ident <|> "_") >> many (ident <|> "_") >> " => " >> termParser >> optional ";"
 def terminationBy          := leading_parser ppLine >> "termination_by " >> many1Indent terminationByElement
 
 def terminationSuffix := optional (terminationBy <|> terminationByCore) >> optional decreasingBy

tests/lean/termination_by2.lean

@@ -0,0 +1,61 @@
+mutual
+ def f (n : Nat) :=
+   if n == 0 then 0 else f (n / 2) + 1
+ termination_by _ => n
+end
+
+def g' (n : Nat) :=
+  match n with
+  | 0 => 1
+  | n+1 => g' n * 3
+termination_by
+  g' n => n
+  _ n => n
+
+mutual
+  def isEven : Nat → Bool
+    | 0 => true
+    | n+1 => isOdd n
+  def isOdd : Nat → Bool
+    | 0 => false
+    | n+1 => isEven n
+end
+termination_by
+   isEven x => x -- Error
+
+mutual
+  def isEven : Nat → Bool
+    | 0 => true
+    | n+1 => isOdd n
+  def isOdd : Nat → Bool
+    | 0 => false
+    | n+1 => isEven n
+end
+termination_by
+   isEven x => x
+   isOd x => x -- Error
+
+mutual
+  def isEven : Nat → Bool
+    | 0 => true
+    | n+1 => isOdd n
+  def isOdd : Nat → Bool
+    | 0 => false
+    | n+1 => isEven n
+end
+termination_by
+   isEven x => x
+   isEven y => y -- Error
+
+mutual
+  def isEven : Nat → Bool
+    | 0 => true
+    | n+1 => isOdd n
+  def isOdd : Nat → Bool
+    | 0 => false
+    | n+1 => isEven n
+end
+termination_by
+   isEven x => x
+   _ x => x
+   _ x => x + 1 -- Error

tests/lean/termination_by2.lean.expected.out

@@ -0,0 +1,6 @@
+termination_by2.lean:4:1-4:22: error: invalid 'termination_by' in 'mutual' block, it must be used after the 'end' keyword
+termination_by2.lean:13:2-13:10: error: invalid `termination_by` syntax, unnecessary else-case
+termination_by2.lean:24:3-24:16: error: invalid `termination_by` syntax, missing case for function 'isOdd'
+termination_by2.lean:36:3-36:14: error: function 'isOd' not found in current declaration
+termination_by2.lean:48:3-48:16: error: invalid `termination_by` syntax, `isEven` case has already been provided
+termination_by2.lean:61:3-61:15: error: invalid `termination_by` syntax, the else-case (i.e., `_ ... => ...`) has already been specified