diff --git a/src/Lean/Declaration.lean b/src/Lean/Declaration.lean index fbd1674964..80425257bd 100644 --- a/src/Lean/Declaration.lean +++ b/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 -/ diff --git a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean index 7d9aeb0de9..117bfd750d 100644 --- a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean +++ b/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 diff --git a/src/Lean/Elab/PreDefinition/Structural/Basic.lean b/src/Lean/Elab/PreDefinition/Structural/Basic.lean index cfe47e0efb..c285bcba16 100644 --- a/src/Lean/Elab/PreDefinition/Structural/Basic.lean +++ b/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) diff --git a/src/Lean/Meta/SizeOf.lean b/src/Lean/Meta/SizeOf.lean index 1f5a500ef0..0947ca2e3c 100644 --- a/src/Lean/Meta/SizeOf.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/FunInd.lean b/src/Lean/Meta/Tactic/FunInd.lean index a1644596d3..973f0143fd 100644 --- a/src/Lean/Meta/Tactic/FunInd.lean +++ b/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[·]!) diff --git a/src/Lean/MonadEnv.lean b/src/Lean/MonadEnv.lean index 87925d7303..82c529cb6e 100644 --- a/src/Lean/MonadEnv.lean +++ b/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 diff --git a/tests/lean/run/structuralMutual.lean b/tests/lean/run/structuralMutual.lean index b67d680141..9ce12e9602 100644 --- a/tests/lean/run/structuralMutual.lean +++ b/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