refactor: rewrite TerminationHint elaborators (leanprover#2958)

In order to familiarize myself with this code, and so that the next
person has an easier time, I

* added docstrings explaining what I found out these things to
* rewrote the syntax expansion functions using syntax pattern matches,
  to the extend possible

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

@@ -20,31 +20,38 @@ inductive TerminationHint where
   | many (map : NameMap TerminationHintValue)
   deriving Inhabited
 
+open Parser.Command in
+/--
+This function takes a user-specified `decreasing_by` or `termination_by'` clause (as `Sytnax`).
+If it is a `terminathionHintMany` (a set of clauses guarded by the function name) then
+* checks that all mentioned names exist in the current declaration
+* check that at most one function from each clique is mentioned
+and sort the entries by function name.
+-/
 def expandTerminationHint (terminationHint? : Option Syntax) (cliques : Array (Array Name)) : MacroM TerminationHint := do
-  if let some terminationHint := terminationHint? then
-    let ref := terminationHint
-    let terminationHint := terminationHint[1]
-    if terminationHint.getKind == ``Parser.Command.terminationHint1 then
-      return TerminationHint.one { ref, value := terminationHint[0] }
-    else if terminationHint.getKind == ``Parser.Command.terminationHintMany then
-      let m ← terminationHint[0].getArgs.foldlM (init := {}) fun m arg =>
-        let declName? := cliques.findSome? fun clique => clique.findSome? fun declName =>
-          if arg[0].getId.isSuffixOf declName then some declName else none
-        match declName? with
-        | none => Macro.throwErrorAt arg[0] s!"function '{arg[0].getId}' not found in current declaration"
-        | some declName => return m.insert declName { ref := arg, value := arg[2] }
-      for clique in cliques do
-        let mut found? := Option.none
-        for declName in clique do
-          if let some { ref, .. } := m.find? declName then
-            if let some found := found? then
-              Macro.throwErrorAt ref s!"invalid termination hint element, '{declName}' and '{found}' are in the same clique"
-            found? := some declName
-      return TerminationHint.many m
-    else
-      Macro.throwUnsupported
-  else
-    return TerminationHint.none
+  let some terminationHint := terminationHint? | return TerminationHint.none
+  let ref := terminationHint
+  match terminationHint with
+  | `(terminationByCore|termination_by' $hint1:terminationHint1)
+  | `(decreasingBy|decreasing_by $hint1:terminationHint1) =>
+    return TerminationHint.one { ref, value := hint1.raw[0] }
+  | `(terminationByCore|termination_by' $hints:terminationHintMany)
+  | `(decreasingBy|decreasing_by $hints:terminationHintMany) => do
+    let m ← hints.raw[0].getArgs.foldlM (init := {}) fun m arg =>
+      let declName? := cliques.findSome? fun clique => clique.findSome? fun declName =>
+        if arg[0].getId.isSuffixOf declName then some declName else none
+      match declName? with
+      | none => Macro.throwErrorAt arg[0] s!"function '{arg[0].getId}' not found in current declaration"
+      | some declName => return m.insert declName { ref := arg, value := arg[2] }
+    for clique in cliques do
+      let mut found? := Option.none
+      for declName in clique do
+        if let some { ref, .. } := m.find? declName then
+          if let some found := found? then
+            Macro.throwErrorAt ref s!"invalid termination hint element, '{declName}' and '{found}' are in the same clique"
+          found? := some declName
+    return TerminationHint.many m
+  | _ => Macro.throwUnsupported
 
 def TerminationHint.markAsUsed (t : TerminationHint) (clique : Array Name) : TerminationHint :=
   match t with
@@ -72,8 +79,9 @@ def TerminationHint.ensureAllUsed (t : TerminationHint) : MacroM Unit := do
   | TerminationHint.many m  => m.forM fun _ v => Macro.throwErrorAt v.ref "unused termination hint element"
   | _ => pure ()
 
-/-! # Support for `termination_by` notation -/
+/-! # Support for `termination_by` and `termination_by'` notation -/
 
+/-- A single `termination_by` clause -/
 structure TerminationByElement where
   ref       : Syntax
   declName  : Name
@@ -82,53 +90,76 @@ structure TerminationByElement where
   implicit  : Bool
   deriving Inhabited
 
+/-- `terminatoin_by` clauses, grouped by clique -/
 structure TerminationByClique where
   elements : Array TerminationByElement
   used     : Bool := false
 
+/--
+A `termination_by'` or `termination_by` hint, as specified by the user
+-/
 inductive TerminationBy where
+  /-- `termination_by'` -/
   | core (hint : TerminationHint)
+  /-- `termination_by` -/
   | ext  (cliques : Array TerminationByClique)
   deriving Inhabited
 
+/--
+A `termination_by'` or `termination_by` hint, as applicable to a single clique
+-/
 inductive TerminationWF where
   | core (stx : Syntax)
   | ext  (clique : Array TerminationByElement)
 
 /-
+Expands the syntax for a `termination_by` clause, checking that
+* each function is mentioned once
+* each function mentioned actually occurs in the current declaration
+* if anything is specified, then all functions have a clause
+* the else-case (`_`) occurs only once, and only when needed
+
+NB:
 ```
 def terminationByElement   := leading_parser ppLine >> (ident <|> hole) >> many (ident <|> hole) >> " => " >> termParser >> optional ";"
 def terminationBy          := leading_parser ppLine >> "termination_by " >> many1chIndent terminationByElement
 ```
 -/
+open Parser.Command in
 private def expandTerminationByNonCore (hint : Syntax) (cliques : Array (Array Name)) : MacroM TerminationBy := do
-  let elementStxs := hint[1].getArgs
+  let `(terminationBy|termination_by $elementStxs*) := hint | Macro.throwUnsupported
   let mut alreadyFound : NameSet := {}
   let mut elseElemStx? := none
   for elementStx in elementStxs do
-    let declStx := elementStx[0]
-    if declStx.isIdent then
-      let declSuffix := declStx.getId
+    match elementStx with
+    | `(terminationByElement|$ident:ident $_* => $_) =>
+      let declSuffix := ident.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]
+    | `(terminationByElement|_ $_vars* => $_term) =>
+      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
+    | _ => Macro.throwUnsupported
+  let toElement (declName : Name) (elementStx : TSyntax ``terminationByElement) : TerminationByElement :=
+    match elementStx with
+    | `(terminationByElement|$ioh $vars* => $body:term) =>
+    let implicit := !ioh.raw.isIdent
     { ref := elementStx, declName, vars, implicit, body }
+    | _ => unreachable!
+  let elementAppliesTo (declName : Name) : TSyntax ``terminationByElement → Bool
+    | `(terminationByElement|$ident:ident $_* => $_) => ident.getId.isSuffixOf declName
+    | _ => false
   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
+      if let some elementStx := elementStxs.find? (elementAppliesTo declName) then
         elements := elements.push (toElement declName elementStx)
       else if let some elseElemStx := elseElemStx? then
         elements := elements.push (toElement declName elseElemStx)
@@ -141,6 +172,9 @@ private def expandTerminationByNonCore (hint : Syntax) (cliques : Array (Array N
     withRef elseElemStx?.get! <| Macro.throwError s!"invalid `termination_by` syntax, unnecessary else-case"
   return TerminationBy.ext result
 
+/--
+Expands the syntax for a `termination_by` or `termination_by'` clause, using the appropriate function
+-/
 def expandTerminationBy (hint? : Option Syntax) (cliques : Array (Array Name)) : MacroM TerminationBy :=
   if let some hint := hint? then
     if hint.isOfKind ``Parser.Command.terminationByCore then

src/Lean/Parser/Command.lean

@@ -37,7 +37,7 @@ We provide two kinds of hints to the termination checker:
 -/
 def terminationHintMany (p : Parser) := leading_parser
   atomic (lookahead (ident >> " => ")) >>
-  many1Indent (group (ppLine >> ppIndent (ident >> " => " >> p >> optional ";")))
+  many1Indent (group (ppLine >> ppIndent (ident >> " => " >> p >> patternIgnore (optional ";"))))
 def terminationHint1 (p : Parser) := leading_parser p
 def terminationHint (p : Parser) := terminationHintMany p <|> terminationHint1 p
 
@@ -48,7 +48,7 @@ def decreasingBy := leading_parser
 
 def terminationByElement   := leading_parser
   ppLine >> (ident <|> Term.hole) >> many (ppSpace >> (ident <|> Term.hole)) >>
-  " => " >> termParser >> optional ";"
+  " => " >> termParser >> patternIgnore (optional ";")
 def terminationBy          := leading_parser
   ppDedent ppLine >> "termination_by" >> many1Indent terminationByElement
 

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/termination_by2.lean

@@ -4,6 +4,13 @@ mutual
  termination_by _ => n
 end
 
+mutual
+ def f (n : Nat) :=
+   if n == 0 then 0 else f (n / 2) + 1
+end
+termination_by n => n
+
+
 def g' (n : Nat) :=
   match n with
   | 0 => 1

tests/lean/termination_by2.lean.expected.out

@@ -1,6 +1,7 @@
 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
+termination_by2.lean:11:15-11:21: error: function 'n' not found in current declaration
+termination_by2.lean:20:2-20:10: error: invalid `termination_by` syntax, unnecessary else-case
+termination_by2.lean:31:3-31:16: error: invalid `termination_by` syntax, missing case for function 'isOdd'
+termination_by2.lean:43:3-43:14: error: function 'isOd' not found in current declaration
+termination_by2.lean:55:3-55:16: error: invalid `termination_by` syntax, `isEven` case has already been provided
+termination_by2.lean:68:3-68:15: error: invalid `termination_by` syntax, the else-case (i.e., `_ ... => ...`) has already been specified