Equations
- Lean.Meta.mkSizeOfFn recName declName = let cls := `Meta.sizeOf; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM Unit := fun y => do let recInfo ← Lean.getConstInfoRec recName Lean.Meta.forallTelescopeReducing recInfo.toConstantVal.type fun xs type => let levelParams := List.tail! recInfo.toConstantVal.levelParams; let params := Array.toSubarray xs 0 recInfo.numParams; let motiveFVars := Array.toSubarray xs recInfo.numParams (recInfo.numParams + recInfo.numMotives); let minorFVars := Array.toSubarray xs (Lean.RecursorVal.getFirstMinorIdx recInfo) (Lean.RecursorVal.getFirstMinorIdx recInfo + recInfo.numMinors); let indices := Array.toSubarray xs (Lean.RecursorVal.getFirstIndexIdx recInfo) (Lean.RecursorVal.getFirstIndexIdx recInfo + recInfo.numIndices); let major := Array.getOp xs (Lean.RecursorVal.getMajorIdx recInfo); let nat := Lean.mkConst `Nat; Lean.Meta.mkLocalInstances (Array.ofSubarray params) fun localInsts => Lean.Meta.mkSizeOfMotives (Array.ofSubarray motiveFVars) fun motives => let us := Lean.levelOne :: List.map Lean.mkLevelParam levelParams; let recFn := Lean.mkConst recName us; let val := Lean.mkAppN recFn (Array.ofSubarray params ++ motives); do let a ← Lean.Meta.inferType val Lean.Meta.forallBoundedTelescope a (some recInfo.numMinors) fun minorFVars' x => Lean.Meta.mkSizeOfMinors (Array.ofSubarray motiveFVars) (Array.ofSubarray minorFVars) minorFVars' fun minors => let sizeOfParams := Array.ofSubarray params ++ localInsts ++ Array.ofSubarray indices ++ #[major]; do let sizeOfType ← Lean.Meta.mkForallFVars sizeOfParams nat false true let val : Lean.Expr := Lean.mkAppN val (minors ++ Array.ofSubarray indices ++ #[major]) let cls : Lean.Name := `Meta.sizeOf let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM Unit := fun y => do let sizeOfValue ← Lean.Meta.mkLambdaFVars sizeOfParams val false true Lean.addDecl (Lean.Declaration.defnDecl { toConstantVal := { name := declName, levelParams := levelParams, type := sizeOfType }, value := sizeOfValue, hints := Lean.ReducibilityHints.abbrev, safety := Lean.DefinitionSafety.safe }) if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "val: " ++ Lean.toMessageData val ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "recName: " ++ Lean.toMessageData recName ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y
Equations
- Lean.Meta.mkSizeOfFns typeName = do let indInfo ← Lean.getConstInfoInduct typeName let recInfo ← Lean.getConstInfoRec (Lean.mkRecName typeName) let numExtra : Nat := recInfo.numMotives - List.length indInfo.all let result : Array Lean.Name := #[] let baseName : Lean.Name := List.head! indInfo.all ++ `_sizeOf let i : Nat := 1 let recMap : Lean.NameMap Lean.Name := ∅ let r ← let col := indInfo.all; forIn col { fst := i, snd := { fst := recMap, snd := result } } fun indTypeName r => let i := r.fst; let x := r.snd; let recMap := x.fst; let result := x.snd; let sizeOfName := Lean.Name.appendIndexAfter baseName i; let recName := Lean.mkRecName indTypeName; do Lean.Meta.mkSizeOfFn recName sizeOfName let recMap : Std.RBMap Lean.Name Lean.Name Lean.Name.quickCmp := Lean.NameMap.insert recMap recName sizeOfName let result : Array Lean.Name := Array.push result sizeOfName let i : Nat := i + 1 pure PUnit.unit pure (ForInStep.yield { fst := i, snd := { fst := recMap, snd := result } }) let x : MProd Nat (MProd (Lean.NameMap Lean.Name) (Array Lean.Name)) := r match x with | { fst := i, snd := { fst := recMap, snd := result } } => do let r ← let col := { start := 0, stop := numExtra, step := 1 }; forIn col { fst := i, snd := { fst := recMap, snd := result } } fun j r => let i := r.fst; let x := r.snd; let recMap := x.fst; let result := x.snd; let recName := Lean.Name.appendIndexAfter (Lean.mkRecName (List.head! indInfo.all)) (j + 1); let sizeOfName := Lean.Name.appendIndexAfter baseName i; do Lean.Meta.mkSizeOfFn recName sizeOfName let recMap : Std.RBMap Lean.Name Lean.Name Lean.Name.quickCmp := Lean.NameMap.insert recMap recName sizeOfName let result : Array Lean.Name := Array.push result sizeOfName let i : Nat := i + 1 pure PUnit.unit pure (ForInStep.yield { fst := i, snd := { fst := recMap, snd := result } }) let x : MProd Nat (MProd (Lean.NameMap Lean.Name) (Array Lean.Name)) := r match x with | { fst := i, snd := { fst := recMap, snd := result } } => pure (result, recMap)
Equations
- Lean.Meta.mkSizeOfSpecLemmaName ctorName = ctorName ++ `sizeOf_spec
Equations
- Lean.Meta.mkSizeOfSpecLemmaInstance ctorApp = Lean.matchConstCtor (Lean.Expr.getAppFn ctorApp) (fun x => Lean.throwError (Lean.toMessageData "failed to apply 'sizeOf' spec, constructor expected" ++ Lean.toMessageData (Lean.indentExpr ctorApp) ++ Lean.toMessageData "")) fun ctorInfo ctorLevels => let ctorArgs := Lean.Expr.getAppArgs ctorApp; let ctorFields := let a := ctorArgs; Array.toSubarray a (Array.size ctorArgs - ctorInfo.numFields) (Array.size a); let lemmaName := Lean.Meta.mkSizeOfSpecLemmaName ctorInfo.toConstantVal.name; do let lemmaInfo ← Lean.getConstInfo lemmaName let lemmaArity ← Lean.Meta.forallTelescopeReducing (Lean.ConstantInfo.type lemmaInfo) fun xs x => pure (Array.size xs) let lemmaArgMask : Array (Option Lean.Expr) := mkArray (lemmaArity - ctorInfo.numFields) none let lemmaArgMask : Array (Option Lean.Expr) := lemmaArgMask ++ Array.map some (Subarray.toArray ctorFields) Lean.Meta.mkAppOptM lemmaName lemmaArgMask
- indInfo : Lean.InductiveVal
- sizeOfFns : Array Lean.Name
- ctorName : Lean.Name
- params : Array Lean.Expr
- localInsts : Array Lean.Expr
- recMap : Lean.NameMap Lean.Name
@[inline]
Equations
- Lean.Meta.SizeOfSpecNested.throwUnexpected msg = do let a ← read Lean.throwError (Lean.toMessageData "failed to generate sizeOf theorem for " ++ Lean.toMessageData a.ctorName ++ Lean.toMessageData " (use `set_option genSizeOfSpec false` to disable theorem generation), " ++ Lean.toMessageData msg ++ Lean.toMessageData "")
Equations
- Lean.Meta.SizeOfSpecNested.throwFailed = do let a ← read Lean.throwError (Lean.toMessageData "failed to generate sizeOf theorem for " ++ Lean.toMessageData a.ctorName ++ Lean.toMessageData ", (use `set_option genSizeOfSpec false` to disable theorem generation)")
Equations
- Lean.Meta.SizeOfSpecNested.main lhs rhs = (fun step => do let a ← liftM (Lean.Meta.isDefEq lhs rhs) if a = true then liftM (Lean.Meta.mkEqRefl rhs) else do let lhs ← liftM (Lean.Meta.whnfI lhs) let lhs ← liftM (Lean.Meta.unfoldDefinition lhs) loop lhs rhs) Lean.Meta.SizeOfSpecNested.main.loop Lean.Meta.SizeOfSpecNested.main.step
Equations
- Lean.Meta.SizeOfSpecNested.main.step lhs rhs = do let a ← liftM (Lean.Meta.isDefEq lhs rhs) if a = true then liftM (Lean.Meta.mkEqRefl rhs) else do let lhs ← Lean.Meta.SizeOfSpecNested.recToSizeOf lhs Lean.Meta.SizeOfSpecNested.mkSizeOfAuxLemma lhs rhs
Equations
- Lean.Meta.mkSizeOfInstances typeName = do let a ← Lean.getEnv let a_1 ← Lean.getOptions let a_2 ← Lean.Meta.isInductivePredicate typeName if (Lean.Environment.contains a `SizeOf && Lean.Option.get a_1 Lean.Meta.genSizeOf && !a_2) = true then do let indInfo ← Lean.getConstInfoInduct typeName if indInfo.isUnsafe = true then pure PUnit.unit else do let discr ← Lean.Meta.mkSizeOfFns typeName let x : Array Lean.Name × Lean.NameMap Lean.Name := discr match x with | (fns, recMap) => let s := toStream fns; do let r ← let col := indInfo.all; forIn col s fun indTypeName r => let s := r; match Stream.next? s with | none => pure (ForInStep.done s) | some (fn, s') => let s := s'; do let indInfo ← Lean.getConstInfoInduct indTypeName Lean.Meta.forallTelescopeReducing indInfo.toConstantVal.type fun xs x => let params := Array.toSubarray xs 0 indInfo.numParams; let indices := let a := xs; Array.toSubarray a indInfo.numParams (Array.size a); Lean.Meta.mkLocalInstances (Array.ofSubarray params) fun localInsts => let us := List.map Lean.mkLevelParam indInfo.toConstantVal.levelParams; let indType := Lean.mkAppN (Lean.mkConst indTypeName us) xs; do let sizeOfIndType ← Lean.Meta.mkAppM `SizeOf #[indType] Lean.Meta.withLocalDeclD `m indType fun m => do let v ← Lean.Meta.mkLambdaFVars #[m] (Lean.mkAppN (Lean.mkConst fn us) (Array.ofSubarray params ++ localInsts ++ Array.ofSubarray indices ++ #[m])) false true let sizeOfMk ← Lean.Meta.mkAppM `SizeOf.mk #[v] let instDeclName : Lean.Name := indTypeName ++ `_sizeOf_inst let instDeclType ← Lean.Meta.mkForallFVars (xs ++ localInsts) sizeOfIndType false true let instDeclValue ← Lean.Meta.mkLambdaFVars (xs ++ localInsts) sizeOfMk false true Lean.addDecl (Lean.Declaration.defnDecl { toConstantVal := { name := instDeclName, levelParams := indInfo.toConstantVal.levelParams, type := instDeclType }, value := instDeclValue, hints := Lean.ReducibilityHints.abbrev, safety := Lean.DefinitionSafety.safe }) Lean.Meta.addInstance instDeclName Lean.AttributeKind.global 1000 pure (ForInStep.yield s) let x : Subarray Lean.Name := r let s : Subarray Lean.Name := x let a ← Lean.getOptions if Lean.Option.get a Lean.Meta.genSizeOfSpec = true then Lean.Meta.mkSizeOfSpecTheorems (List.toArray indInfo.all) fns recMap else pure PUnit.unit else pure PUnit.unit