feat: improve #print recursor rules

src/Lean/Elab/Print.lean

@@ -96,18 +96,71 @@ private def printInduct (id : Name) (levelParams : List Name) (numParams : Nat)
     m := m ++ Format.line ++ ctor ++ " : " ++ cinfo.type
   logInfo m
 
-private def printRecursor (recInfo : RecursorVal) : CommandElabM Unit := do
-  let mut m ← mkHeader "recursor" recInfo.name recInfo.levelParams recInfo.type (if recInfo.isUnsafe then .unsafe else .safe)
-  m := m ++ Format.line ++ m!"number of parameters: {recInfo.numParams}"
-  m := m ++ Format.line ++ m!"number of indices: {recInfo.numIndices}"
-  m := m ++ Format.line ++ m!"number of motives: {recInfo.numMotives}"
-  m := m ++ Format.line ++ m!"number of minors: {recInfo.numMinors}"
-  if recInfo.k then
-    m := m ++ Format.line ++ m!"supports k-like reduction"
-  m := m ++ Format.line ++ "rules:"
-  for rule in recInfo.rules do
-    m := m ++ Format.line ++ m!"for {rule.ctor} ({rule.nfields} fields): {rule.rhs}"
+open Meta in
+private def printRecursor (sigOnly : Bool) (recInfo : RecursorVal) : CommandElabM Unit := do
+  let mut m ← mkHeader "recursor" recInfo.name recInfo.levelParams recInfo.type (if recInfo.isUnsafe then .unsafe else .safe) (sig := false)
+  m := m!"{m} {.signature recInfo.name}"
+  unless sigOnly do
+    m := m ++ Format.line ++ m!"number of parameters: {recInfo.numParams}{positionsString 0 recInfo.numParams}"
+    m := m ++ Format.line ++ m!"number of motives: {recInfo.numMotives}{positionsString recInfo.numParams recInfo.numMotives}"
+    m := m ++ Format.line ++ m!"number of minor premises: {recInfo.numMinors}{positionsString recInfo.getFirstMinorIdx recInfo.numMinors}"
+    m := m ++ Format.line ++ m!"number of indices: {recInfo.numIndices}{positionsString recInfo.getFirstIndexIdx recInfo.numIndices}"
+    m := m ++ Format.line ++ m!"major premise position: {recInfo.getMajorIdx+1}"
+    if recInfo.k then
+      m := m ++ Format.line ++ m!"supports K-like reduction"
+    if recInfo.rules.isEmpty then
+      m := m ++ Format.line ++ "rules: (none)"
+    else
+      m := m ++ Format.line ++ "rules:"
+      for rule in recInfo.rules do
+        let ruleMsg ← liftTermElabM do mkRuleMsg rule
+        m := m ++ indentD ruleMsg
   logInfo m
+where
+  positionsString (firstIndex count : Nat) : String :=
+    if count = 0 then ""
+    else if count = 1 then s!" (position {firstIndex+1})"
+    else s!" (positions {firstIndex+1}–{firstIndex+count})"
+  /--
+  Given the recursor rule, creates a message like `List.rec nil cons (List.cons x xs) ==> cons x xs`.
+  Recall that each rule is a lambda expression whose parameters correspond to the arguments
+  of the recursor followed by the fields of the constructor.
+  We need to synthesize a major premise from this to fully render the reduction rule.
+  The main complication is the recursors for nested inductive types, since the number of inductive
+  parameters for the rule is for the auxiliary inductive type as part of the kernel's internal
+  construction, *not* the number of inductive parameters for the type being nested through.
+  -/
+  mkRuleMsg (rule : RecursorRule) : TermElabM MessageData := do
+    lambdaTelescope rule.rhs fun xs rhs => do
+      -- Start building the recursor application, applying parameters, motives, and minor premises
+      let numRecArgs := recInfo.numParams + recInfo.numMotives + recInfo.numMinors
+      let levels := recInfo.levelParams.map Level.param
+      let recApp := mkAppN (.const recInfo.name levels) xs[0...numRecArgs]
+      -- The remaining rule parameters correspond to constructor fields. These are the last `nfields`
+      -- of the constructor. Note that in nested inductive types, the number of inductive parameters
+      -- for the constructor might not equal the number of inductive parameters for the recursor.
+      let fields := xs[numRecArgs...*]
+      assert! fields.size == rule.nfields
+      -- We can get the constructor inductive parameters from the type of the major premise,
+      -- taking all arguments before the reported number of indices.
+      -- We can also get the constructor universe levels from this.
+      let (majorLevels, params) ←
+        forallBoundedTelescope (← inferType recApp) (some (recInfo.numIndices + 1)) fun xs' _ => do
+          let major := xs'[recInfo.numIndices]!
+          (← inferType major).withApp fun t args => do
+            let us := t.constLevels!
+            let params := args[0...(args.size - recInfo.numIndices)]
+            pure (us, params)
+      -- Now we can build the major premise
+      let major := mkAppN (mkAppN (.const rule.ctor majorLevels) params) fields
+      -- From this we can compute the indices for the recursor
+      let majorTypeArgs := (← inferType major).getAppArgs
+      let indices := majorTypeArgs[(majorTypeArgs.size - recInfo.numIndices)...*]
+      -- Then we can build the left-hand side of the rule and the final message
+      let lhs := mkApp (mkAppN recApp indices) major
+      -- Inductive predicates should pretty print. We universally enable pretty printing proofs here.
+      withOptions (fun opts => opts.set pp.proofs.name true) do
+        addMessageContext <| lhs ++ indentD m!"==> {rhs}"
 
 /--
 Computes the origin of a field. Returns its `StructureFieldInfo` at the origin.
@@ -209,7 +262,7 @@ private def printIdCore (sigOnly : Bool) (id : Name) : CommandElabM Unit := do
   | ConstantInfo.opaqueInfo  { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "opaque" id us t (if u then .unsafe else .safe)
   | ConstantInfo.quotInfo  { levelParams := us, type := t, .. } => printQuot id us t
   | ConstantInfo.ctorInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "constructor" id us t (if u then .unsafe else .safe)
-  | ConstantInfo.recInfo recInfo => printRecursor recInfo
+  | ConstantInfo.recInfo recInfo => printRecursor sigOnly recInfo
   | ConstantInfo.inductInfo { levelParams := us, numParams, type := t, ctors, isUnsafe := u, .. } =>
     if isStructure env id then
       printStructure id us numParams t ctors[0]! u

tests/elab/new_inductive.lean.out.expected

@@ -62,29 +62,31 @@ fun {P} {α β} {t} {α' β'} {t'} eq_1 eq_2 eq_3 =>
 13
 @Rbnode.brecOn : {α : Type u_2} →
   {motive : Rbnode α → Sort u_1} → (t : Rbnode α) → ((t : Rbnode α) → Rbnode.below t → motive t) → motive t
-recursor test.Trie.rec.{u} : {motive_1 : Trie → Sort u} →
-  {motive_2 : Rbnode (myPair Char Trie) → Sort u} →
-    {motive_3 : myPair Char Trie → Sort u} →
-      motive_1 Trie.Empty →
-        ((a : Char) → (a_1 : Rbnode (myPair Char Trie)) → motive_2 a_1 → motive_1 (Trie.mk a a_1)) →
-          motive_2 Rbnode.leaf →
-            ((lchild : Rbnode (myPair Char Trie)) →
-                (val : myPair Char Trie) →
-                  (rchild : Rbnode (myPair Char Trie)) →
-                    motive_2 lchild → motive_3 val → motive_2 rchild → motive_2 (lchild.redNode val rchild)) →
-              ((lchild : Rbnode (myPair Char Trie)) →
-                  (val : myPair Char Trie) →
-                    (rchild : Rbnode (myPair Char Trie)) →
-                      motive_2 lchild → motive_3 val → motive_2 rchild → motive_2 (lchild.blackNode val rchild)) →
-                ((a : Char) → (a_1 : Trie) → motive_1 a_1 → motive_3 (myPair.mk a a_1)) → (t : Trie) → motive_1 t
+recursor test.Trie.rec.{u} {motive_1 : Trie → Sort u} {motive_2 : Rbnode (myPair Char Trie) → Sort u}
+  {motive_3 : myPair Char Trie → Sort u} (Empty : motive_1 Trie.Empty)
+  (mk : (a : Char) → (a_1 : Rbnode (myPair Char Trie)) → motive_2 a_1 → motive_1 (Trie.mk a a_1))
+  (leaf : motive_2 Rbnode.leaf)
+  (redNode :
+    (lchild : Rbnode (myPair Char Trie)) →
+      (val : myPair Char Trie) →
+        (rchild : Rbnode (myPair Char Trie)) →
+          motive_2 lchild → motive_3 val → motive_2 rchild → motive_2 (lchild.redNode val rchild))
+  (blackNode :
+    (lchild : Rbnode (myPair Char Trie)) →
+      (val : myPair Char Trie) →
+        (rchild : Rbnode (myPair Char Trie)) →
+          motive_2 lchild → motive_3 val → motive_2 rchild → motive_2 (lchild.blackNode val rchild)) :
+  ((a : Char) → (a_1 : Trie) → motive_1 a_1 → motive_3 (myPair.mk a a_1)) → (t : Trie) → motive_1 t
 number of parameters: 0
+number of motives: 3 (positions 1–3)
+number of minor premises: 6 (positions 4–9)
 number of indices: 0
-number of motives: 3
-number of minors: 6
+major premise position: 10
 rules:
-for test.Trie.Empty (0 fields): fun motive_1 motive_2 motive_3 Empty mk leaf redNode blackNode mk_1 => Empty
-for test.Trie.mk (2 fields): fun motive_1 motive_2 motive_3 Empty mk leaf redNode blackNode mk_1 a a_1 =>
-  mk a a_1 (Trie.rec_1 Empty mk leaf redNode blackNode mk_1 a_1)
+  Trie.rec Empty mk✝ leaf redNode blackNode mk Trie.Empty
+    ==> Empty
+  Trie.rec Empty mk✝ leaf redNode blackNode mk (Trie.mk a✝¹ a✝)
+    ==> mk✝ a✝¹ a✝ (Trie.rec_1 Empty mk✝ leaf redNode blackNode mk a✝)
 @[reducible] protected def test.Trie.noConfusion.{u} : {P : Sort u} →
   {t t' : Trie} → t = t' → Trie.noConfusionType P t t' :=
 fun {P} {t t'} eq => eq ▸ t.casesOn (fun k => k) fun a a_1 k => k ⋯ ⋯

tests/elab/new_inductive2.lean.out.expected

@@ -1,13 +1,14 @@
-recursor foo.rec.{u} : {motive_1 : foo → Sort u} →
-  {motive_2 : arrow Nat foo → Sort u} →
-    ((a : arrow Nat foo) → motive_2 a → motive_1 (foo.mk a)) →
-      ((a : Nat → foo) → ((a_1 : Nat) → motive_1 (a a_1)) → motive_2 (arrow.mk a)) → (t : foo) → motive_1 t
+recursor foo.rec.{u} {motive_1 : foo → Sort u} {motive_2 : arrow Nat foo → Sort u}
+  (mk : (a : arrow Nat foo) → motive_2 a → motive_1 (foo.mk a)) :
+  ((a : Nat → foo) → ((a_1 : Nat) → motive_1 (a a_1)) → motive_2 (arrow.mk a)) → (t : foo) → motive_1 t
 number of parameters: 0
+number of motives: 2 (positions 1–2)
+number of minor premises: 2 (positions 3–4)
 number of indices: 0
-number of motives: 2
-number of minors: 2
+major premise position: 5
 rules:
-for foo.mk (1 fields): fun motive_1 motive_2 mk mk_1 a => mk a (foo.rec_1 mk mk_1 a)
+  foo.rec mk✝ mk (foo.mk a✝)
+    ==> mk✝ a✝ (foo.rec_1 mk✝ mk a✝)
 @[reducible] protected def foo.below.{u} : {motive_1 : (t : foo) → Sort u} →
   {motive_2 : (t : arrow.{0, 0} Nat foo) → Sort u} → (t : foo) → Sort (max 1 u) :=
 fun {motive_1 : (t : foo) → Sort u} {motive_2 : (t : arrow.{0, 0} Nat foo) → Sort u} (t : foo) =>