Merge branch 'master' of github.com:leanprover/lean4 into joachim/use_numNested

follow-up to #4684

src/Lean/Declaration.lean

@@ -286,6 +286,7 @@ def mkInductiveValEx (name : Name) (levelParams : List Name) (type : Expr) (numP
 
 def InductiveVal.numCtors (v : InductiveVal) : Nat := v.ctors.length
 def InductiveVal.isNested (v : InductiveVal) : Bool := v.numNested > 0
+def InductiveVal.numTypeFormers (v : InductiveVal) : Nat := v.all.length + v.numNested
 
 structure ConstructorVal extends ConstantVal where
   /-- Inductive type this constructor is a member of -/

src/Lean/Elab/PreDefinition/Structural/BRecOn.lean

@@ -61,19 +61,19 @@ private partial def toBelowAux (C : Expr) (belowDict : Expr) (arg : Expr) (F : E
 /-- See `toBelow` -/
 private def withBelowDict [Inhabited α] (below : Expr) (numIndParams : Nat)
     (positions : Positions) (k : Array Expr → Expr → MetaM α) : MetaM α := do
-  let numIndAll := positions.size
+  let numTypeFormers := positions.size
   let belowType ← inferType below
   trace[Elab.definition.structural] "belowType: {belowType}"
   unless (← isTypeCorrect below) do
     trace[Elab.definition.structural] "not type correct!"
   belowType.withApp fun f args => do
-    unless numIndParams + numIndAll < args.size do
+    unless numIndParams + numTypeFormers < args.size do
       trace[Elab.definition.structural] "unexpected 'below' type{indentExpr belowType}"
       throwToBelowFailed
     let params := args[:numIndParams]
-    let finalArgs := args[numIndParams+numIndAll:]
+    let finalArgs := args[numIndParams+numTypeFormers:]
     let pre := mkAppN f params
-    let motiveTypes ← inferArgumentTypesN numIndAll pre
+    let motiveTypes ← inferArgumentTypesN numTypeFormers pre
     let numMotives : Nat := positions.numIndices
     trace[Elab.definition.structural] "numMotives: {numMotives}"
     let mut CTypes := Array.mkArray numMotives (.sort 37) -- dummy value
@@ -278,6 +278,7 @@ It also undoes the permutation and packing done by `packMotives`
 -/
 def inferBRecOnFTypes (recArgInfos : Array RecArgInfo) (positions : Positions)
     (brecOnConst : Name → Expr) : MetaM (Array Expr) := do
+  let numTypeFormers := positions.size
   let recArgInfo := recArgInfos[0]! -- pick an arbitrary one
   let brecOn := brecOnConst recArgInfo.indName
   check brecOn
@@ -285,7 +286,7 @@ def inferBRecOnFTypes (recArgInfos : Array RecArgInfo) (positions : Positions)
   -- Skip the indices and major argument
   let packedFTypes ← forallBoundedTelescope brecOnType (some (recArgInfo.indicesPos.size + 1)) fun _ brecOnType =>
     -- And return the types of of the next arguments
-    arrowDomainsN recArgInfo.indAll.size brecOnType
+    arrowDomainsN numTypeFormers brecOnType
 
   let mut FTypes := Array.mkArray recArgInfos.size (Expr.sort 0)
   for packedFType in packedFTypes, poss in positions do

src/Lean/Elab/PreDefinition/Structural/Basic.lean

@@ -91,10 +91,11 @@ and for each such type, keep track of the order of the functions.
 
 We represent these positions as an `Array (Array Nat)`. We have that
 
-* `positions.size = indInfo.all.length`
+* `positions.size = indInfo.numTypeFormers`
 * `positions.flatten` is a permutation of `[0:n]`, so each of the `n` functions has exactly one
   position, and each position refers to one of the `n` functions.
 * if `k ∈ positions[i]` then the recursive argument of function `k` is has type `indInfo.all[i]`
+  (or corresponding nested inductive type)
 
 -/
 abbrev Positions := Array (Array Nat)

src/Lean/Meta/SizeOf.lean

@@ -164,8 +164,6 @@ partial def mkSizeOfFn (recName : Name) (declName : Name): MetaM Unit := do
 -/
 def mkSizeOfFns (typeName : Name) : MetaM (Array Name × NameMap Name) := do
   let indInfo ← getConstInfoInduct typeName
-  let recInfo ← getConstInfoRec (mkRecName typeName)
-  let numExtra := recInfo.numMotives - indInfo.all.length -- numExtra > 0 for nested inductive types
   let mut result := #[]
   let baseName := indInfo.all.head! ++ `_sizeOf -- we use the first inductive type as the base name for `sizeOf` functions
   let mut i := 1
@@ -177,7 +175,7 @@ def mkSizeOfFns (typeName : Name) : MetaM (Array Name × NameMap Name) := do
     recMap := recMap.insert recName sizeOfName
     result := result.push sizeOfName
     i := i + 1
-  for j in [:numExtra] do
+  for j in [:indInfo.numNested] do
     let recName := (mkRecName indInfo.all.head!).appendIndexAfter (j+1)
     let sizeOfName := baseName.appendIndexAfter i
     mkSizeOfFn recName sizeOfName

src/Lean/Meta/Tactic/FunInd.lean

@@ -744,8 +744,8 @@ def findRecursor {α} (name : Name) (varNames : Array Name) (e : Expr)
         -- Bail out on mutual or nested inductives
         let .str indName _ := f.constName! | unreachable!
         let indInfo ← getConstInfoInduct indName
-        if indInfo.all.length > 1 then
-          throwError "functional induction: cannot handle mutual inductives"
+        if indInfo.numTypeFormers > 1 then
+          throwError "functional induction: cannot handle mutual or nested inductives"
 
         let elimInfo ← getElimExprInfo f
         let targets : Array Expr := elimInfo.targetsPos.map (args[·]!)

src/Lean/MonadEnv.lean

@@ -142,8 +142,8 @@ def findModuleOf? [Monad m] [MonadEnv m] [MonadError m] (declName : Name) : m (O
 
 def isEnumType  [Monad m] [MonadEnv m] [MonadError m] (declName : Name) : m Bool := do
   if let ConstantInfo.inductInfo info ← getConstInfo declName then
-    if !info.type.isProp && info.all.length == 1 && info.numIndices == 0 && info.numParams == 0
-       && !info.ctors.isEmpty && !info.isRec && !info.isNested && !info.isUnsafe then
+    if !info.type.isProp && info.numTypeFormers == 1 && info.numIndices == 0 && info.numParams == 0
+       && !info.ctors.isEmpty && !info.isRec && !info.isUnsafe then
       info.ctors.allM fun ctorName => do
         let ConstantInfo.ctorInfo info ← getConstInfo ctorName | return false
         return info.numFields == 0

tests/lean/run/structuralMutual.lean

@@ -527,10 +527,10 @@ namespace FunIndTests
 
 /--
 error: Failed to realize constant A.size.induct:
-  functional induction: cannot handle mutual inductives
+  functional induction: cannot handle mutual or nested inductives
 ---
 error: Failed to realize constant A.size.induct:
-  functional induction: cannot handle mutual inductives
+  functional induction: cannot handle mutual or nested inductives
 ---
 error: unknown identifier 'A.size.induct'
 -/
@@ -539,10 +539,10 @@ error: unknown identifier 'A.size.induct'
 
 /--
 error: Failed to realize constant A.subs.induct:
-  functional induction: cannot handle mutual inductives
+  functional induction: cannot handle mutual or nested inductives
 ---
 error: Failed to realize constant A.subs.induct:
-  functional induction: cannot handle mutual inductives
+  functional induction: cannot handle mutual or nested inductives
 ---
 error: unknown identifier 'A.subs.induct'
 -/
@@ -551,10 +551,10 @@ error: unknown identifier 'A.subs.induct'
 
 /--
 error: Failed to realize constant MutualIndNonMutualFun.A.self_size.induct:
-  functional induction: cannot handle mutual inductives
+  functional induction: cannot handle mutual or nested inductives
 ---
 error: Failed to realize constant MutualIndNonMutualFun.A.self_size.induct:
-  functional induction: cannot handle mutual inductives
+  functional induction: cannot handle mutual or nested inductives
 ---
 error: unknown identifier 'MutualIndNonMutualFun.A.self_size.induct'
 -/
@@ -563,10 +563,10 @@ error: unknown identifier 'MutualIndNonMutualFun.A.self_size.induct'
 
 /--
 error: Failed to realize constant A.hasNoBEmpty.induct:
-  functional induction: cannot handle mutual inductives
+  functional induction: cannot handle mutual or nested inductives
 ---
 error: Failed to realize constant A.hasNoBEmpty.induct:
-  functional induction: cannot handle mutual inductives
+  functional induction: cannot handle mutual or nested inductives
 ---
 error: unknown identifier 'A.hasNoBEmpty.induct'
 -/
@@ -587,10 +587,4 @@ error: unknown identifier 'EvenOdd.isEven.induct'
 #guard_msgs in
 #check EvenOdd.isEven.induct -- TODO: This error message can be improved
 
-
--- For Tree.size this would actually work already:
-
-run_meta
-  Lean.modifyEnv fun env => Lean.markAuxRecursor env ``NestedWithTuple.Tree.brecOn
-
 end FunIndTests