From 5ce886cf965cf2bac144bb0cb9b2dfe93ca103fd Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 5 Jul 2024 10:25:44 +0200 Subject: [PATCH] refactor: Split Constructions module (#4656) for better build paralleization and less rebuilding when editing one of these files. --- src/Lean/Elab/ComputedFields.lean | 2 +- src/Lean/Meta/Constructions.lean | 132 +------------------ src/Lean/Meta/Constructions/CasesOn.lean | 23 ++++ src/Lean/Meta/Constructions/NoConfusion.lean | 126 ++++++++++++++++++ src/Lean/Meta/IndPredBelow.lean | 2 +- 5 files changed, 153 insertions(+), 132 deletions(-) create mode 100644 src/Lean/Meta/Constructions/CasesOn.lean create mode 100644 src/Lean/Meta/Constructions/NoConfusion.lean diff --git a/src/Lean/Elab/ComputedFields.lean b/src/Lean/Elab/ComputedFields.lean index 7f9c30b2d0..6c385ed659 100644 --- a/src/Lean/Elab/ComputedFields.lean +++ b/src/Lean/Elab/ComputedFields.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Gabriel Ebner -/ prelude -import Lean.Meta.Constructions +import Lean.Meta.Constructions.CasesOn import Lean.Compiler.ImplementedByAttr import Lean.Elab.PreDefinition.WF.Eqns diff --git a/src/Lean/Meta/Constructions.lean b/src/Lean/Meta/Constructions.lean index bafb7e7052..469d6a3af5 100644 --- a/src/Lean/Meta/Constructions.lean +++ b/src/Lean/Meta/Constructions.lean @@ -4,135 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ prelude -import Lean.AuxRecursor -import Lean.AddDecl -import Lean.Meta.AppBuilder -import Lean.Meta.CompletionName +import Lean.Meta.Constructions.CasesOn +import Lean.Meta.Constructions.NoConfusion import Lean.Meta.Constructions.RecOn import Lean.Meta.Constructions.BRecOn - -namespace Lean - -@[extern "lean_mk_cases_on"] opaque mkCasesOnImp (env : Environment) (declName : @& Name) : Except KernelException Declaration -@[extern "lean_mk_no_confusion_type"] opaque mkNoConfusionTypeCoreImp (env : Environment) (declName : @& Name) : Except KernelException Declaration -@[extern "lean_mk_no_confusion"] opaque mkNoConfusionCoreImp (env : Environment) (declName : @& Name) : Except KernelException Declaration - -open Meta - -def mkCasesOn (declName : Name) : MetaM Unit := do - let name := mkCasesOnName declName - let decl ← ofExceptKernelException (mkCasesOnImp (← getEnv) declName) - addDecl decl - setReducibleAttribute name - modifyEnv fun env => markAuxRecursor env name - modifyEnv fun env => addProtected env name - -def mkNoConfusionCore (declName : Name) : MetaM Unit := do - -- Do not do anything unless can_elim_to_type. TODO: Extract to util - let .inductInfo indVal ← getConstInfo declName | return - let recInfo ← getConstInfo (mkRecName declName) - unless recInfo.levelParams.length > indVal.levelParams.length do return - - let name := Name.mkStr declName "noConfusionType" - let decl ← ofExceptKernelException (mkNoConfusionTypeCoreImp (← getEnv) declName) - addDecl decl - setReducibleAttribute name - modifyEnv fun env => addToCompletionBlackList env name - modifyEnv fun env => addProtected env name - - let name := Name.mkStr declName "noConfusion" - let decl ← ofExceptKernelException (mkNoConfusionCoreImp (← getEnv) declName) - addDecl decl - setReducibleAttribute name - modifyEnv fun env => markNoConfusion env name - modifyEnv fun env => addProtected env name - -def mkNoConfusionEnum (enumName : Name) : MetaM Unit := do - if (← getEnv).contains ``noConfusionEnum then - mkToCtorIdx - mkNoConfusionType - mkNoConfusion - else - -- `noConfusionEnum` was not defined yet, so we use `mkNoConfusionCore` - mkNoConfusionCore enumName -where - mkToCtorIdx : MetaM Unit := do - let ConstantInfo.inductInfo info ← getConstInfo enumName | unreachable! - let us := info.levelParams.map mkLevelParam - let numCtors := info.ctors.length - let declName := Name.mkStr enumName "toCtorIdx" - let enumType := mkConst enumName us - let natType := mkConst ``Nat - let declType ← mkArrow enumType natType - let mut minors := #[] - for i in [:numCtors] do - minors := minors.push <| mkNatLit i - withLocalDeclD `x enumType fun x => do - let motive ← mkLambdaFVars #[x] natType - let declValue ← mkLambdaFVars #[x] <| mkAppN (mkApp2 (mkConst (mkCasesOnName enumName) (levelOne::us)) motive x) minors - addAndCompile <| Declaration.defnDecl { - name := declName - levelParams := info.levelParams - type := declType - value := declValue - safety := DefinitionSafety.safe - hints := ReducibilityHints.abbrev - } - setReducibleAttribute declName - - mkNoConfusionType : MetaM Unit := do - let ConstantInfo.inductInfo info ← getConstInfo enumName | unreachable! - let us := info.levelParams.map mkLevelParam - let v ← mkFreshUserName `v - let enumType := mkConst enumName us - let sortV := mkSort (mkLevelParam v) - let toCtorIdx := mkConst (Name.mkStr enumName "toCtorIdx") us - withLocalDeclD `P sortV fun P => - withLocalDeclD `x enumType fun x => - withLocalDeclD `y enumType fun y => do - let declType ← mkForallFVars #[P, x, y] sortV - let declValue ← mkLambdaFVars #[P, x, y] (← mkAppM ``noConfusionTypeEnum #[toCtorIdx, P, x, y]) - let declName := Name.mkStr enumName "noConfusionType" - addAndCompile <| Declaration.defnDecl { - name := declName - levelParams := v :: info.levelParams - type := declType - value := declValue - safety := DefinitionSafety.safe - hints := ReducibilityHints.abbrev - } - setReducibleAttribute declName - - mkNoConfusion : MetaM Unit := do - let ConstantInfo.inductInfo info ← getConstInfo enumName | unreachable! - let us := info.levelParams.map mkLevelParam - let v ← mkFreshUserName `v - let enumType := mkConst enumName us - let sortV := mkSort (mkLevelParam v) - let toCtorIdx := mkConst (Name.mkStr enumName "toCtorIdx") us - let noConfusionType := mkConst (Name.mkStr enumName "noConfusionType") (mkLevelParam v :: us) - withLocalDecl `P BinderInfo.implicit sortV fun P => - withLocalDecl `x BinderInfo.implicit enumType fun x => - withLocalDecl `y BinderInfo.implicit enumType fun y => do - withLocalDeclD `h (← mkEq x y) fun h => do - let declType ← mkForallFVars #[P, x, y, h] (mkApp3 noConfusionType P x y) - let declValue ← mkLambdaFVars #[P, x, y, h] (← mkAppOptM ``noConfusionEnum #[none, none, none, toCtorIdx, P, x, y, h]) - let declName := Name.mkStr enumName "noConfusion" - addAndCompile <| Declaration.defnDecl { - name := declName - levelParams := v :: info.levelParams - type := declType - value := declValue - safety := DefinitionSafety.safe - hints := ReducibilityHints.abbrev - } - setReducibleAttribute declName - modifyEnv fun env => markNoConfusion env declName - -def mkNoConfusion (declName : Name) : MetaM Unit := do - if (← isEnumType declName) then - mkNoConfusionEnum declName - else - mkNoConfusionCore declName - -end Lean diff --git a/src/Lean/Meta/Constructions/CasesOn.lean b/src/Lean/Meta/Constructions/CasesOn.lean new file mode 100644 index 0000000000..57a642ddcb --- /dev/null +++ b/src/Lean/Meta/Constructions/CasesOn.lean @@ -0,0 +1,23 @@ +/- +Copyright (c) 2020 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +prelude +import Lean.AddDecl +import Lean.Meta.Basic + +namespace Lean + +@[extern "lean_mk_cases_on"] opaque mkCasesOnImp (env : Environment) (declName : @& Name) : Except KernelException Declaration + +open Meta + +def mkCasesOn (declName : Name) : MetaM Unit := do + let name := mkCasesOnName declName + let decl ← ofExceptKernelException (mkCasesOnImp (← getEnv) declName) + addDecl decl + setReducibleAttribute name + modifyEnv fun env => markAuxRecursor env name + +end Lean diff --git a/src/Lean/Meta/Constructions/NoConfusion.lean b/src/Lean/Meta/Constructions/NoConfusion.lean new file mode 100644 index 0000000000..d3ed5033fa --- /dev/null +++ b/src/Lean/Meta/Constructions/NoConfusion.lean @@ -0,0 +1,126 @@ +/- +Copyright (c) 2020 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +prelude +import Lean.AddDecl +import Lean.Meta.AppBuilder +import Lean.Meta.CompletionName + +namespace Lean + +@[extern "lean_mk_no_confusion_type"] opaque mkNoConfusionTypeCoreImp (env : Environment) (declName : @& Name) : Except KernelException Declaration +@[extern "lean_mk_no_confusion"] opaque mkNoConfusionCoreImp (env : Environment) (declName : @& Name) : Except KernelException Declaration + +open Meta + +def mkNoConfusionCore (declName : Name) : MetaM Unit := do + -- Do not do anything unless can_elim_to_type. TODO: Extract to util + let .inductInfo indVal ← getConstInfo declName | return + let recInfo ← getConstInfo (mkRecName declName) + unless recInfo.levelParams.length > indVal.levelParams.length do return + + let name := Name.mkStr declName "noConfusionType" + let decl ← ofExceptKernelException (mkNoConfusionTypeCoreImp (← getEnv) declName) + addDecl decl + setReducibleAttribute name + modifyEnv fun env => addToCompletionBlackList env name + modifyEnv fun env => addProtected env name + + let name := Name.mkStr declName "noConfusion" + let decl ← ofExceptKernelException (mkNoConfusionCoreImp (← getEnv) declName) + addDecl decl + setReducibleAttribute name + modifyEnv fun env => markNoConfusion env name + modifyEnv fun env => addProtected env name + +def mkNoConfusionEnum (enumName : Name) : MetaM Unit := do + if (← getEnv).contains ``noConfusionEnum then + mkToCtorIdx + mkNoConfusionType + mkNoConfusion + else + -- `noConfusionEnum` was not defined yet, so we use `mkNoConfusionCore` + mkNoConfusionCore enumName +where + mkToCtorIdx : MetaM Unit := do + let ConstantInfo.inductInfo info ← getConstInfo enumName | unreachable! + let us := info.levelParams.map mkLevelParam + let numCtors := info.ctors.length + let declName := Name.mkStr enumName "toCtorIdx" + let enumType := mkConst enumName us + let natType := mkConst ``Nat + let declType ← mkArrow enumType natType + let mut minors := #[] + for i in [:numCtors] do + minors := minors.push <| mkNatLit i + withLocalDeclD `x enumType fun x => do + let motive ← mkLambdaFVars #[x] natType + let declValue ← mkLambdaFVars #[x] <| mkAppN (mkApp2 (mkConst (mkCasesOnName enumName) (levelOne::us)) motive x) minors + addAndCompile <| Declaration.defnDecl { + name := declName + levelParams := info.levelParams + type := declType + value := declValue + safety := DefinitionSafety.safe + hints := ReducibilityHints.abbrev + } + setReducibleAttribute declName + + mkNoConfusionType : MetaM Unit := do + let ConstantInfo.inductInfo info ← getConstInfo enumName | unreachable! + let us := info.levelParams.map mkLevelParam + let v ← mkFreshUserName `v + let enumType := mkConst enumName us + let sortV := mkSort (mkLevelParam v) + let toCtorIdx := mkConst (Name.mkStr enumName "toCtorIdx") us + withLocalDeclD `P sortV fun P => + withLocalDeclD `x enumType fun x => + withLocalDeclD `y enumType fun y => do + let declType ← mkForallFVars #[P, x, y] sortV + let declValue ← mkLambdaFVars #[P, x, y] (← mkAppM ``noConfusionTypeEnum #[toCtorIdx, P, x, y]) + let declName := Name.mkStr enumName "noConfusionType" + addAndCompile <| Declaration.defnDecl { + name := declName + levelParams := v :: info.levelParams + type := declType + value := declValue + safety := DefinitionSafety.safe + hints := ReducibilityHints.abbrev + } + setReducibleAttribute declName + + mkNoConfusion : MetaM Unit := do + let ConstantInfo.inductInfo info ← getConstInfo enumName | unreachable! + let us := info.levelParams.map mkLevelParam + let v ← mkFreshUserName `v + let enumType := mkConst enumName us + let sortV := mkSort (mkLevelParam v) + let toCtorIdx := mkConst (Name.mkStr enumName "toCtorIdx") us + let noConfusionType := mkConst (Name.mkStr enumName "noConfusionType") (mkLevelParam v :: us) + withLocalDecl `P BinderInfo.implicit sortV fun P => + withLocalDecl `x BinderInfo.implicit enumType fun x => + withLocalDecl `y BinderInfo.implicit enumType fun y => do + withLocalDeclD `h (← mkEq x y) fun h => do + let declType ← mkForallFVars #[P, x, y, h] (mkApp3 noConfusionType P x y) + let declValue ← mkLambdaFVars #[P, x, y, h] (← mkAppOptM ``noConfusionEnum #[none, none, none, toCtorIdx, P, x, y, h]) + let declName := Name.mkStr enumName "noConfusion" + addAndCompile <| Declaration.defnDecl { + name := declName + levelParams := v :: info.levelParams + type := declType + value := declValue + safety := DefinitionSafety.safe + hints := ReducibilityHints.abbrev + } + setReducibleAttribute declName + modifyEnv fun env => markNoConfusion env declName + +def mkNoConfusion (declName : Name) : MetaM Unit := do + if (← isEnumType declName) then + mkNoConfusionEnum declName + else + mkNoConfusionCore declName + +end Lean diff --git a/src/Lean/Meta/IndPredBelow.lean b/src/Lean/Meta/IndPredBelow.lean index b9fc37fc53..8e18fdc2a9 100644 --- a/src/Lean/Meta/IndPredBelow.lean +++ b/src/Lean/Meta/IndPredBelow.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Dany Fabian -/ prelude -import Lean.Meta.Constructions +import Lean.Meta.Constructions.CasesOn import Lean.Meta.Match.Match namespace Lean.Meta.IndPredBelow