Parse derecursifyWith also with mutual

This is not meant to be merged!

This branch can be used to prototype derecursifiers outside the lean4
tree. Example:

```
import Lean.Elab.PreDefinition.Main

set_option autoImplicit false

open Lean Elab

def foo (n : Nat) : Nat := match n with
  | .zero => .zero
  | .succ n => foo n
derecursify_with Structural.structuralRecursion

def derec (preDefs : Array PreDefinition) : TermElabM Unit := do
  logInfo m!"{preDefs.map (·.declName)}"
  return

def foo2 (n : Nat) : Nat := match n with
  | .zero => .zero
  | .succ n => foo2 n
derecursify_with derec
```

_Maybe_ a proper designed version of this feature is useful at some
point, see #2812 for that.

src/Lean/Elab/Declaration.lean

@@ -192,7 +192,9 @@ def getTerminationHints (stx : Syntax) : TerminationHints :=
   let k := decl.getKind
   if k == ``Parser.Command.def || k == ``Parser.Command.abbrev || k == ``Parser.Command.theorem || k == ``Parser.Command.instance then
     let args := decl.getArgs
-    { terminationBy? := args[args.size - 2]!.getOptional?, decreasingBy? := args[args.size - 1]!.getOptional? }
+    { derecursifyWith? := args[args.size - 3]!.getOptional?,
+      terminationBy? := args[args.size - 2]!.getOptional?,
+      decreasingBy? := args[args.size - 1]!.getOptional? }
   else
     {}
 
@@ -332,7 +334,11 @@ def expandMutualPreamble : Macro := fun stx =>
 
 @[builtin_command_elab «mutual»]
 def elabMutual : CommandElab := fun stx => do
-  let hints := { terminationBy? := stx[3].getOptional?, decreasingBy? := stx[4].getOptional? }
+  let hints := {
+      derecursifyWith? := stx[3].getOptional?
+      terminationBy? := stx[4].getOptional?
+      decreasingBy? := stx[5].getOptional?
+  }
   if isMutualInductive stx then
     if let some bad := hints.terminationBy? then
       throwErrorAt bad "invalid 'termination_by' in mutually inductive datatype declaration"

src/Lean/Elab/PreDefinition/Main.lean

@@ -8,12 +8,14 @@ import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.Structural
 import Lean.Elab.PreDefinition.WF.Main
 import Lean.Elab.PreDefinition.MkInhabitant
+import Lean.Elab.Eval
 
 namespace Lean.Elab
 open Meta
 open Term
 
 structure TerminationHints where
+  derecursifyWith? : Option Syntax := none
   terminationBy? : Option Syntax := none
   decreasingBy? : Option Syntax := none
   deriving Inhabited
@@ -68,6 +70,10 @@ private def ensureNoUnassignedMVarsAtPreDef (preDef : PreDefinition) : TermElabM
   else
     return preDef
 
+/-- Code that turns a predefinition into non-recursive definitions and adds them to the environment
+-/
+def Derecursifier := Array PreDefinition → Option WF.TerminationWF → Option Syntax → TermElabM Unit
+
 /--
   Letrec declarations produce terms of the form `(fun .. => ..) d` where `d` is a (partial) application of an auxiliary declaration for a letrec declaration.
   This method beta-reduces them to make sure they can be eliminated by the well-founded recursion module. -/
@@ -94,6 +100,13 @@ private def addAsAxioms (preDefs : Array PreDefinition) : TermElabM Unit := do
     applyAttributesOf #[preDef] AttributeApplicationTime.afterTypeChecking
     applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation
 
+
+unsafe def evalDerecursifierImpl (value : Syntax) : TermElabM Derecursifier :=
+  evalTerm Derecursifier (mkConst ``Derecursifier) value
+
+@[implemented_by evalDerecursifierImpl]
+opaque evalDerecursifier (value : Syntax)  : TermElabM Derecursifier
+
 def addPreDefinitions (preDefs : Array PreDefinition) (hints : TerminationHints) : TermElabM Unit := withLCtx {} {} do
   for preDef in preDefs do
     trace[Elab.definition.body] "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
@@ -133,7 +146,10 @@ def addPreDefinitions (preDefs : Array PreDefinition) (hints : TerminationHints)
         if let some { ref, value := decrTactic } := decreasingBy.find? (preDefs.map (·.declName)) then
           decrTactic? := some (← withRef ref `(by $(⟨decrTactic⟩)))
           decreasingBy := decreasingBy.markAsUsed (preDefs.map (·.declName))
-        if wf?.isSome || decrTactic?.isSome then
+        if let some s := hints.derecursifyWith? then
+          let derec ← evalDerecursifier s[1]
+          derec preDefs wf? decrTactic?
+        else if wf?.isSome || decrTactic?.isSome then
           wfRecursion preDefs wf? decrTactic?
         else
           withRef (preDefs[0]!.ref) <| mapError

src/Lean/Parser/Command.lean

@@ -52,8 +52,13 @@ def terminationByElement   := leading_parser
 def terminationBy          := leading_parser
   ppDedent ppLine >> "termination_by" >> many1Indent terminationByElement
 
+def derecursifyWith := leading_parser
+  ppDedent ppLine >> "derecursify_with " >> termParser
+
 def terminationSuffix :=
-  optional (terminationBy <|> terminationByCore) >> optional decreasingBy
+  optional derecursifyWith >>
+  optional (terminationBy <|> terminationByCore) >>
+  optional decreasingBy
 
 @[builtin_command_parser]
 def moduleDoc := leading_parser ppDedent <|

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/StxQuot.lean.expected.out

@@ -8,8 +8,8 @@ StxQuot.lean:8:12-8:13: error: unexpected token ')'; expected identifier or term
 "(«term_+_» (num \"1\") \"+\" (num \"1\"))"
 StxQuot.lean:19:15-19:16: error: unexpected token ']'; expected term
 "(Term.fun \"fun\" (Term.basicFun [`a._@.UnhygienicMain._hyg.1] [] \"=>\" `a._@.UnhygienicMain._hyg.1))"
-"(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n  \"def\"\n  (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n  (Command.optDeclSig [] [])\n  (Command.declValSimple \":=\" (num \"1\") [])\n  []\n  []\n  []))"
-"[(Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"1\") [])\n   []\n   []\n   []))\n (Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"2\") [])\n   []\n   []\n   []))]"
+"(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n  \"def\"\n  (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n  (Command.optDeclSig [] [])\n  (Command.declValSimple \":=\" (num \"1\") [])\n  []\n  []\n  []\n  []))"
+"[(Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"1\") [])\n   []\n   []\n   []\n   []))\n (Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"2\") [])\n   []\n   []\n   []\n   []))]"
 "`Nat.one._@.UnhygienicMain._hyg.1"
 "`Nat.one._@.UnhygienicMain._hyg.1"
 "(Term.app `f._@.UnhygienicMain._hyg.1 [`Nat.one._@.UnhygienicMain._hyg.1 `Nat.one._@.UnhygienicMain._hyg.1])"
@@ -18,8 +18,8 @@ StxQuot.lean:19:15-19:16: error: unexpected token ']'; expected term
 "(Term.proj `Nat.one._@.UnhygienicMain._hyg.1 \".\" `b._@.UnhygienicMain._hyg.1)"
 "(«term_+_» (num \"2\") \"+\" (num \"1\"))"
 "(«term_+_» («term_+_» (num \"1\") \"+\" (num \"2\")) \"+\" (num \"1\"))"
-"(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n  \"def\"\n  (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n  (Command.optDeclSig [] [])\n  (Command.declValSimple \":=\" (num \"1\") [])\n  []\n  []\n  []))"
-"[(Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"2\") [])\n   []\n   []\n   []))\n (Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"1\") [])\n   []\n   []\n   []))]"
+"(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n  \"def\"\n  (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n  (Command.optDeclSig [] [])\n  (Command.declValSimple \":=\" (num \"1\") [])\n  []\n  []\n  []\n  []))"
+"[(Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"2\") [])\n   []\n   []\n   []\n   []))\n (Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"1\") [])\n   []\n   []\n   []\n   []))]"
 "0"
 0
 1