From 69a446c8d1a494feaed00cb9a940754dbcc80692 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 23 Jun 2022 15:54:04 -0700 Subject: [PATCH] feat: add field `all` to `DefinitionVal` and `TheoremVal` Remark: we need an update stage0, and the field is not being updated correctly set yet. --- src/Lean/Declaration.lean | 33 ++++++++++++++++---------- src/Lean/Elab/Binders.lean | 8 +++---- src/Lean/Elab/PreDefinition/Basic.lean | 7 ++++-- src/Lean/Elab/Tactic/ElabTerm.lean | 8 +++---- src/Lean/Elab/Term.lean | 6 ++--- src/Lean/Meta/Closure.lean | 10 ++++---- src/Lean/Meta/Injective.lean | 3 ++- src/Lean/Meta/Tactic/AuxLemma.lean | 6 ++--- src/Lean/ParserCompiler.lean | 5 ++-- src/kernel/declaration.cpp | 18 +++++++------- src/kernel/declaration.h | 4 ++-- 11 files changed, 59 insertions(+), 49 deletions(-) diff --git a/src/Lean/Declaration.lean b/src/Lean/Declaration.lean index 04e5c5769e..f93a11f1c3 100644 --- a/src/Lean/Declaration.lean +++ b/src/Lean/Declaration.lean @@ -95,16 +95,19 @@ structure DefinitionVal extends ConstantVal where value : Expr hints : ReducibilityHints safety : DefinitionSafety + /-- + List of all (including this one) declarations in the same mutual block. + Note that this information is not used by the kernel, and is only used + to save the information provided by the user when using mutual blocks. + Recall that the Lean kernel does not support recursive definitions and they + are compiled using recursors and `WellFounded.fix`. + -/ + all : List Name := [name] deriving Inhabited @[export lean_mk_definition_val] -def mkDefinitionValEx (name : Name) (levelParams : List Name) (type : Expr) (val : Expr) (hints : ReducibilityHints) (safety : DefinitionSafety) : DefinitionVal := { - name := name, - levelParams := levelParams, - type := type, - value := val, - hints := hints, - safety := safety +def mkDefinitionValEx (name : Name) (levelParams : List Name) (type : Expr) (value : Expr) (hints : ReducibilityHints) (safety : DefinitionSafety) (all : List Name) : DefinitionVal := { + name, levelParams, type, hints, safety, value, all } @[export lean_definition_val_get_safety] def DefinitionVal.getSafetyEx (v : DefinitionVal) : DefinitionSafety := @@ -112,21 +115,25 @@ def mkDefinitionValEx (name : Name) (levelParams : List Name) (type : Expr) (val structure TheoremVal extends ConstantVal where value : Expr + /-- + List of all (including this one) declarations in the same mutual block. + See comment at `DefinitionVal.all`. -/ + all : List Name := [name] deriving Inhabited /- Value for an opaque constant declaration `constant x : t := e` -/ structure OpaqueVal extends ConstantVal where value : Expr isUnsafe : Bool + /-- + List of all (including this one) declarations in the same mutual block. + See comment at `DefinitionVal.all`. -/ + all : List Name := [name] deriving Inhabited @[export lean_mk_opaque_val] -def mkOpaqueValEx (name : Name) (levelParams : List Name) (type : Expr) (val : Expr) (isUnsafe : Bool) : OpaqueVal := { - name := name, - levelParams := levelParams, - type := type, - value := val, - isUnsafe := isUnsafe +def mkOpaqueValEx (name : Name) (levelParams : List Name) (type : Expr) (value : Expr) (isUnsafe : Bool) (all : List Name) : OpaqueVal := { + name, levelParams, type, value, isUnsafe, all } @[export lean_opaque_val_is_unsafe] def OpaqueVal.isUnsafeEx (v : OpaqueVal) : Bool := diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean index e3f803607c..f09d3834bb 100644 --- a/src/Lean/Elab/Binders.lean +++ b/src/Lean/Elab/Binders.lean @@ -65,10 +65,10 @@ def declareTacticSyntax (tactic : Syntax) : TermElabM Name := let name ← MonadQuotation.addMacroScope `_auto let type := Lean.mkConst `Lean.Syntax let tactic ← quoteAutoTactic tactic - let val ← elabTerm tactic type - let val ← instantiateMVars val - trace[Elab.autoParam] val - let decl := Declaration.defnDecl { name := name, levelParams := [], type := type, value := val, hints := ReducibilityHints.opaque, + let value ← elabTerm tactic type + let value ← instantiateMVars value + trace[Elab.autoParam] value + let decl := Declaration.defnDecl { name, levelParams := [], type, value, hints := .opaque, safety := DefinitionSafety.safe } addDecl decl compileDecl decl diff --git a/src/Lean/Elab/PreDefinition/Basic.lean b/src/Lean/Elab/PreDefinition/Basic.lean index 200bebccd0..aa9c37a5ec 100644 --- a/src/Lean/Elab/PreDefinition/Basic.lean +++ b/src/Lean/Elab/PreDefinition/Basic.lean @@ -98,11 +98,14 @@ private def addNonRecAux (preDef : PreDefinition) (compile : Bool) (applyAttrAft let decl ← match preDef.kind with | DefKind.«theorem» => - pure <| Declaration.thmDecl { name := preDef.declName, levelParams := preDef.levelParams, type := preDef.type, value := preDef.value } + pure <| Declaration.thmDecl { + name := preDef.declName, levelParams := preDef.levelParams, type := preDef.type, value := preDef.value + } | DefKind.«opaque» => pure <| Declaration.opaqueDecl { name := preDef.declName, levelParams := preDef.levelParams, type := preDef.type, value := preDef.value - isUnsafe := preDef.modifiers.isUnsafe } + isUnsafe := preDef.modifiers.isUnsafe + } | DefKind.«abbrev» => pure <| Declaration.defnDecl { name := preDef.declName, levelParams := preDef.levelParams, type := preDef.type, value := preDef.value diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean index b3d2efc8f3..c19ebbc9fe 100644 --- a/src/Lean/Elab/Tactic/ElabTerm.lean +++ b/src/Lean/Elab/Tactic/ElabTerm.lean @@ -283,12 +283,12 @@ private def preprocessPropToDecide (expectedType : Expr) : TermElabM Expr := do let rflPrf ← mkEqRefl (toExpr true) return mkApp3 (Lean.mkConst ``of_decide_eq_true) expectedType s rflPrf -private def mkNativeAuxDecl (baseName : Name) (type val : Expr) : TermElabM Name := do +private def mkNativeAuxDecl (baseName : Name) (type value : Expr) : TermElabM Name := do let auxName ← Term.mkAuxName baseName let decl := Declaration.defnDecl { - name := auxName, levelParams := [], type := type, value := val, - hints := ReducibilityHints.abbrev, - safety := DefinitionSafety.safe + name := auxName, levelParams := [], type, value + hints := .abbrev + safety := .safe } addDecl decl compileDecl decl diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index f08f935a3c..b0ccbce943 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -1590,9 +1590,9 @@ unsafe def evalExpr (α) (typeName : Name) (value : Expr) : TermElabM α := unless type.isConstOf typeName do throwError "unexpected type at evalExpr{indentExpr type}" let decl := Declaration.defnDecl { - name := name, levelParams := [], type := type, - value := value, hints := ReducibilityHints.opaque, - safety := DefinitionSafety.unsafe + name, levelParams := [], type + value, hints := ReducibilityHints.opaque, + safety := .unsafe } ensureNoUnassignedMVars decl addAndCompile decl diff --git a/src/Lean/Meta/Closure.lean b/src/Lean/Meta/Closure.lean index 42de3cdd28..2a9def77bc 100644 --- a/src/Lean/Meta/Closure.lean +++ b/src/Lean/Meta/Closure.lean @@ -350,11 +350,11 @@ def mkAuxDefinition (name : Name) (type : Expr) (value : Expr) (zeta : Bool := f let result ← Closure.mkValueTypeClosure type value zeta let env ← getEnv let decl := Declaration.defnDecl { - name := name, - levelParams := result.levelParams.toList, - type := result.type, - value := result.value, - hints := ReducibilityHints.regular (getMaxHeight env result.value + 1), + name := name + levelParams := result.levelParams.toList + type := result.type + value := result.value + hints := ReducibilityHints.regular (getMaxHeight env result.value + 1) safety := if env.hasUnsafe result.type || env.hasUnsafe result.value then DefinitionSafety.unsafe else DefinitionSafety.safe } addDecl decl diff --git a/src/Lean/Meta/Injective.lean b/src/Lean/Meta/Injective.lean index 31a4fe9750..65ea5e2fdb 100644 --- a/src/Lean/Meta/Injective.lean +++ b/src/Lean/Meta/Injective.lean @@ -101,8 +101,9 @@ private def mkInjectiveTheorem (ctorVal : ConstructorVal) : MetaM Unit := do let some type ← mkInjectiveTheoremType? ctorVal | return () let value ← mkInjectiveTheoremValue ctorVal.name type + let name := mkInjectiveTheoremNameFor ctorVal.name addDecl <| Declaration.thmDecl { - name := mkInjectiveTheoremNameFor ctorVal.name + name levelParams := ctorVal.levelParams type := (← instantiateMVars type) value := (← instantiateMVars value) diff --git a/src/Lean/Meta/Tactic/AuxLemma.lean b/src/Lean/Meta/Tactic/AuxLemma.lean index 95c72863a7..1e9a3ba288 100644 --- a/src/Lean/Meta/Tactic/AuxLemma.lean +++ b/src/Lean/Meta/Tactic/AuxLemma.lean @@ -29,10 +29,8 @@ def mkAuxLemma (levelParams : List Name) (type : Expr) (value : Expr) : MetaM Na let mkNewAuxLemma := do let auxName := Name.mkNum (env.mainModule ++ `_auxLemma) s.idx addDecl <| Declaration.thmDecl { - name := auxName - levelParams := levelParams - type := type - value := value + name := auxName + levelParams, type, value } modifyEnv fun env => auxLemmasExt.modifyState env fun ⟨idx, lemmas⟩ => ⟨idx + 1, lemmas.insert type (auxName, levelParams)⟩ return auxName diff --git a/src/Lean/ParserCompiler.lean b/src/Lean/ParserCompiler.lean index 64d126467c..a8692e0aba 100644 --- a/src/Lean/ParserCompiler.lean +++ b/src/Lean/ParserCompiler.lean @@ -97,8 +97,9 @@ partial def compileParserExpr (e : Expr) : MetaM Expr := do let paramTy ← replaceParserTy ctx <$> inferType param return mkForall `_ BinderInfo.default paramTy ty let decl := Declaration.defnDecl { - name := c', levelParams := [], - type := ty, value := value, hints := ReducibilityHints.opaque, safety := DefinitionSafety.safe } + name := c', levelParams := [] + type := ty, value := value, hints := ReducibilityHints.opaque, safety := DefinitionSafety.safe + } let env ← getEnv let env ← match env.addAndCompile {} decl with | Except.ok env => pure env diff --git a/src/kernel/declaration.cpp b/src/kernel/declaration.cpp index 408d218ed7..122de461e9 100644 --- a/src/kernel/declaration.cpp +++ b/src/kernel/declaration.cpp @@ -62,12 +62,12 @@ axiom_val::axiom_val(name const & n, names const & lparams, expr const & type, b bool axiom_val::is_unsafe() const { return lean_axiom_val_is_unsafe(to_obj_arg()); } -extern "C" object * lean_mk_definition_val(object * n, object * lparams, object * type, object * value, object * hints, uint8 safety); +extern "C" object * lean_mk_definition_val(object * n, object * lparams, object * type, object * value, object * hints, uint8 safety, object * all); extern "C" uint8 lean_definition_val_get_safety(object * v); -definition_val::definition_val(name const & n, names const & lparams, expr const & type, expr const & val, reducibility_hints const & hints, definition_safety safety): +definition_val::definition_val(name const & n, names const & lparams, expr const & type, expr const & val, reducibility_hints const & hints, definition_safety safety, names const & all): object_ref(lean_mk_definition_val(n.to_obj_arg(), lparams.to_obj_arg(), type.to_obj_arg(), val.to_obj_arg(), - hints.to_obj_arg(), static_cast(safety))) { + hints.to_obj_arg(), static_cast(safety), all.to_obj_arg())) { } definition_safety definition_val::get_safety() const { return static_cast(lean_definition_val_get_safety(to_obj_arg())); } @@ -76,11 +76,11 @@ theorem_val::theorem_val(name const & n, names const & lparams, expr const & typ object_ref(mk_cnstr(0, constant_val(n, lparams, type), val)) { } -extern "C" object * lean_mk_opaque_val(object * n, object * lparams, object * type, object * value, uint8 is_unsafe); +extern "C" object * lean_mk_opaque_val(object * n, object * lparams, object * type, object * value, uint8 is_unsafe, object * all); extern "C" uint8 lean_opaque_val_is_unsafe(object * v); -opaque_val::opaque_val(name const & n, names const & lparams, expr const & type, expr const & val, bool is_unsafe): - object_ref(lean_mk_opaque_val(n.to_obj_arg(), lparams.to_obj_arg(), type.to_obj_arg(), val.to_obj_arg(), is_unsafe)) { +opaque_val::opaque_val(name const & n, names const & lparams, expr const & type, expr const & val, bool is_unsafe, names const & all): + object_ref(lean_mk_opaque_val(n.to_obj_arg(), lparams.to_obj_arg(), type.to_obj_arg(), val.to_obj_arg(), is_unsafe, all.to_obj_arg())) { } bool opaque_val::is_unsafe() const { return lean_opaque_val_is_unsafe(to_obj_arg()); } @@ -193,12 +193,12 @@ static unsigned get_max_height(environment const & env, expr const & v) { definition_val mk_definition_val(environment const & env, name const & n, names const & params, expr const & t, expr const & v, definition_safety s) { unsigned h = get_max_height(env, v); - return definition_val(n, params, t, v, reducibility_hints::mk_regular(h+1), s); + return definition_val(n, params, t, v, reducibility_hints::mk_regular(h+1), s, names(n)); } declaration mk_definition(name const & n, names const & params, expr const & t, expr const & v, reducibility_hints const & h, definition_safety safety) { - return declaration(mk_cnstr(static_cast(declaration_kind::Definition), definition_val(n, params, t, v, h, safety))); + return declaration(mk_cnstr(static_cast(declaration_kind::Definition), definition_val(n, params, t, v, h, safety, names(n)))); } declaration mk_definition(environment const & env, name const & n, names const & params, expr const & t, @@ -207,7 +207,7 @@ declaration mk_definition(environment const & env, name const & n, names const & } declaration mk_opaque(name const & n, names const & params, expr const & t, expr const & v, bool is_unsafe) { - return declaration(mk_cnstr(static_cast(declaration_kind::Opaque), opaque_val(n, params, t, v, is_unsafe))); + return declaration(mk_cnstr(static_cast(declaration_kind::Opaque), opaque_val(n, params, t, v, is_unsafe, names(n)))); } declaration mk_axiom(name const & n, names const & params, expr const & t, bool unsafe) { diff --git a/src/kernel/declaration.h b/src/kernel/declaration.h index 265482de61..470363fed8 100644 --- a/src/kernel/declaration.h +++ b/src/kernel/declaration.h @@ -95,7 +95,7 @@ structure definition_val extends constant_val := */ class definition_val : public object_ref { public: - definition_val(name const & n, names const & lparams, expr const & type, expr const & val, reducibility_hints const & hints, definition_safety safety); + definition_val(name const & n, names const & lparams, expr const & type, expr const & val, reducibility_hints const & hints, definition_safety safety, names const & all); definition_val(definition_val const & other):object_ref(other) {} definition_val(definition_val && other):object_ref(other) {} definition_val & operator=(definition_val const & other) { object_ref::operator=(other); return *this; } @@ -135,7 +135,7 @@ structure opaque_val extends constant_val := */ class opaque_val : public object_ref { public: - opaque_val(name const & n, names const & lparams, expr const & type, expr const & val, bool is_unsafe); + opaque_val(name const & n, names const & lparams, expr const & type, expr const & val, bool is_unsafe, names const & all); opaque_val(opaque_val const & other):object_ref(other) {} opaque_val(opaque_val && other):object_ref(other) {} opaque_val & operator=(opaque_val const & other) { object_ref::operator=(other); return *this; }