max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: trace nodes for SizeOf and injectivity theorem generation

Browse source
This commit is contained in:
Sebastian Ullrich 2023-06-13 23:09:59 +02:00 • committed by Leonardo de Moura
parent ba4bfe26f2
commit f0583c3fd6
2 changed files with 41 additions and 36 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/Lean/Meta/Injective.lean
View file

@ -158,9 +158,13 @@ def mkInjectiveTheorems (declName : Name) : MetaM Unit := do
-- See https://github.com/leanprover/lean4/issues/2188
withLCtx {} {} do
for ctor in info.ctors do
let ctorVal ← getConstInfoCtor ctor
if ctorVal.numFields > 0 then
mkInjectiveTheorem ctorVal
mkInjectiveEqTheorem ctorVal
withTraceNode `Meta.injective (fun _ => return m!"{ctor}") do
let ctorVal ← getConstInfoCtor ctor
if ctorVal.numFields > 0 then
mkInjectiveTheorem ctorVal
mkInjectiveEqTheorem ctorVal
builtin_initialize
registerTraceClass `Meta.injective
end Lean.Meta

65
src/Lean/Meta/SizeOf.lean
View file

@ -471,42 +471,43 @@ register_builtin_option genSizeOf : Bool := {
register_builtin_option genSizeOfSpec : Bool := {
defValue := true
descr := "generate `SizeOf` specificiation theorems for automatically generated instances"
descr := "generate `SizeOf` specification theorems for automatically generated instances"
}
def mkSizeOfInstances (typeName : Name) : MetaM Unit := do
if (← getEnv).contains ``SizeOf && genSizeOf.get (← getOptions) && !(← isInductivePredicate typeName) then
let indInfo ← getConstInfoInduct typeName
unless indInfo.isUnsafe do
let (fns, recMap) ← mkSizeOfFns typeName
for indTypeName in indInfo.all, fn in fns do
let indInfo ← getConstInfoInduct indTypeName
forallTelescopeReducing indInfo.type fun xs _ =>
let params := xs[:indInfo.numParams]
withInstImplicitAsImplict params do
let indices := xs[indInfo.numParams:]
mkLocalInstances params fun localInsts => do
let us := indInfo.levelParams.map mkLevelParam
let indType := mkAppN (mkConst indTypeName us) xs
let sizeOfIndType ← mkAppM ``SizeOf #[indType]
withLocalDeclD `m indType fun m => do
let v ← mkLambdaFVars #[m] <| mkAppN (mkConst fn us) (params ++ localInsts ++ indices ++ #[m])
let sizeOfMk ← mkAppM ``SizeOf.mk #[v]
let instDeclName := indTypeName ++ `_sizeOf_inst
let instDeclType ← mkForallFVars (xs ++ localInsts) sizeOfIndType
let instDeclValue ← mkLambdaFVars (xs ++ localInsts) sizeOfMk
trace[Meta.sizeOf] ">> {instDeclName} : {instDeclType}"
addDecl <| Declaration.defnDecl {
name := instDeclName
levelParams := indInfo.levelParams
type := instDeclType
value := instDeclValue
safety := .safe
hints := .abbrev
}
addInstance instDeclName AttributeKind.global (eval_prio default)
if genSizeOfSpec.get (← getOptions) then
mkSizeOfSpecTheorems indInfo.all.toArray fns recMap
withTraceNode `Meta.sizeOf (fun _ => return m!"{typeName}") do
let indInfo ← getConstInfoInduct typeName
unless indInfo.isUnsafe do
let (fns, recMap) ← mkSizeOfFns typeName
for indTypeName in indInfo.all, fn in fns do
let indInfo ← getConstInfoInduct indTypeName
forallTelescopeReducing indInfo.type fun xs _ =>
let params := xs[:indInfo.numParams]
withInstImplicitAsImplict params do
let indices := xs[indInfo.numParams:]
mkLocalInstances params fun localInsts => do
let us := indInfo.levelParams.map mkLevelParam
let indType := mkAppN (mkConst indTypeName us) xs
let sizeOfIndType ← mkAppM ``SizeOf #[indType]
withLocalDeclD `m indType fun m => do
let v ← mkLambdaFVars #[m] <| mkAppN (mkConst fn us) (params ++ localInsts ++ indices ++ #[m])
let sizeOfMk ← mkAppM ``SizeOf.mk #[v]
let instDeclName := indTypeName ++ `_sizeOf_inst
let instDeclType ← mkForallFVars (xs ++ localInsts) sizeOfIndType
let instDeclValue ← mkLambdaFVars (xs ++ localInsts) sizeOfMk
trace[Meta.sizeOf] ">> {instDeclName} : {instDeclType}"
addDecl <| Declaration.defnDecl {
name := instDeclName
levelParams := indInfo.levelParams
type := instDeclType
value := instDeclValue
safety := .safe
hints := .abbrev
}
addInstance instDeclName AttributeKind.global (eval_prio default)
if genSizeOfSpec.get (← getOptions) then
mkSizeOfSpecTheorems indInfo.all.toArray fns recMap
builtin_initialize
registerTraceClass `Meta.sizeOf