From f0ac477d2ede7c83fdea588dcfb2ca6336097de6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 1 Jan 2021 18:31:28 -0800 Subject: [PATCH] feat: add sanity checks --- src/Lean/Declaration.lean | 23 ++++++++------ src/Lean/Elab/Binders.lean | 3 +- src/Lean/Elab/BuiltinNotation.lean | 3 +- src/Lean/Elab/Command.lean | 4 ++- src/Lean/Elab/PreDefinition/Basic.lean | 13 ++++---- src/Lean/Elab/PreDefinition/Main.lean | 2 +- src/Lean/Elab/PreDefinition/Structural.lean | 2 +- src/Lean/Elab/Print.lean | 21 ++++++++----- src/Lean/Elab/Term.lean | 2 +- src/Lean/KeyedDeclsAttribute.lean | 3 +- src/Lean/Meta/Closure.lean | 2 +- src/Lean/Parser/Extension.lean | 3 +- src/Lean/ParserCompiler.lean | 2 +- src/kernel/declaration.cpp | 34 ++++++++++++--------- src/kernel/declaration.h | 13 +++++--- src/kernel/environment.cpp | 12 +++++--- src/library/compiler/util.cpp | 4 +-- 17 files changed, 88 insertions(+), 58 deletions(-) diff --git a/src/Lean/Declaration.lean b/src/Lean/Declaration.lean index 63d56a1704..71d9f8c902 100644 --- a/src/Lean/Declaration.lean +++ b/src/Lean/Declaration.lean @@ -78,23 +78,28 @@ def mkAxiomValEx (name : Name) (lparams : List Name) (type : Expr) (isUnsafe : B @[export lean_axiom_val_is_unsafe] def AxiomVal.isUnsafeEx (v : AxiomVal) : Bool := v.isUnsafe +inductive DefinitionSafety where + | «unsafe» | safe | «partial» + deriving Inhabited, BEq, Repr + structure DefinitionVal extends ConstantVal where - value : Expr - hints : ReducibilityHints - isUnsafe : Bool + value : Expr + hints : ReducibilityHints + safety : DefinitionSafety + deriving Inhabited @[export lean_mk_definition_val] -def mkDefinitionValEx (name : Name) (lparams : List Name) (type : Expr) (val : Expr) (hints : ReducibilityHints) (isUnsafe : Bool) : DefinitionVal := { +def mkDefinitionValEx (name : Name) (lparams : List Name) (type : Expr) (val : Expr) (hints : ReducibilityHints) (safety : DefinitionSafety) : DefinitionVal := { name := name, lparams := lparams, type := type, value := val, hints := hints, - isUnsafe := isUnsafe + safety := safety } -@[export lean_definition_val_is_unsafe] def DefinitionVal.isUnsafeEx (v : DefinitionVal) : Bool := - v.isUnsafe +@[export lean_definition_val_get_safety] def DefinitionVal.getSafetyEx (v : DefinitionVal) : DefinitionSafety := + v.safety structure TheoremVal extends ConstantVal where value : Expr @@ -132,7 +137,7 @@ inductive Declaration where | thmDecl (val : TheoremVal) | opaqueDecl (val : OpaqueVal) | quotDecl - | mutualDefnDecl (defns : List DefinitionVal) -- All definitions must be marked as `unsafe` + | mutualDefnDecl (defns : List DefinitionVal) -- All definitions must be marked as `unsafe` or `partial` | inductDecl (lparams : List Name) (nparams : Nat) (types : List InductiveType) (isUnsafe : Bool) deriving Inhabited @@ -301,7 +306,7 @@ def toConstantVal : ConstantInfo → ConstantVal | recInfo {toConstantVal := d, ..} => d def isUnsafe : ConstantInfo → Bool - | defnInfo v => v.isUnsafe + | defnInfo v => v.safety == DefinitionSafety.unsafe | axiomInfo v => v.isUnsafe | thmInfo v => false | opaqueInfo v => v.isUnsafe diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean index 8d1a59a1c8..1f4d35cc01 100644 --- a/src/Lean/Elab/Binders.lean +++ b/src/Lean/Elab/Binders.lean @@ -65,7 +65,8 @@ def declareTacticSyntax (tactic : Syntax) : TermElabM Name := let val ← elabTerm tactic type let val ← instantiateMVars val trace[Elab.autoParam]! val - let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque, isUnsafe := false } + let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque, + safety := DefinitionSafety.safe } addDecl decl compileDecl decl pure name diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean index e878044ec2..0c01369f39 100644 --- a/src/Lean/Elab/BuiltinNotation.lean +++ b/src/Lean/Elab/BuiltinNotation.lean @@ -95,7 +95,8 @@ private def mkNativeReflAuxDecl (type val : Expr) : TermElabM Name := do let decl := Declaration.defnDecl { name := auxName, lparams := [], type := type, value := val, hints := ReducibilityHints.abbrev, - isUnsafe := false } + safety := DefinitionSafety.safe + } addDecl decl compileDecl decl pure auxName diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index 09dd52f722..de46f6d427 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -582,7 +582,9 @@ unsafe def elabEvalUnsafe : CommandElab let type ← inferType value let decl := Declaration.defnDecl { name := n, lparams := [], type := type, - value := value, hints := ReducibilityHints.opaque, isUnsafe := true } + value := value, hints := ReducibilityHints.opaque, + safety := DefinitionSafety.unsafe + } Term.ensureNoUnassignedMVars decl addAndCompile decl let elabMetaEval : CommandElabM Unit := runTermElabM (some n) fun _ => do diff --git a/src/Lean/Elab/PreDefinition/Basic.lean b/src/Lean/Elab/PreDefinition/Basic.lean index 78b4aa494f..8d41c52e38 100644 --- a/src/Lean/Elab/PreDefinition/Basic.lean +++ b/src/Lean/Elab/PreDefinition/Basic.lean @@ -103,11 +103,12 @@ private def addNonRecAux (preDef : PreDefinition) (compile : Bool) : TermElabM U isUnsafe := preDef.modifiers.isUnsafe } | DefKind.«abbrev» => Declaration.defnDecl { name := preDef.declName, lparams := preDef.lparams, type := preDef.type, value := preDef.value, - hints := ReducibilityHints.«abbrev», isUnsafe := preDef.modifiers.isUnsafe } + hints := ReducibilityHints.«abbrev», + safety := if preDef.modifiers.isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe } | DefKind.«def» => Declaration.defnDecl { name := preDef.declName, lparams := preDef.lparams, type := preDef.type, value := preDef.value, hints := ReducibilityHints.regular (getMaxHeight env preDef.value + 1), - isUnsafe := preDef.modifiers.isUnsafe } + safety := if preDef.modifiers.isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe } addDecl decl applyAttributesOf #[preDef] AttributeApplicationTime.afterTypeChecking if compile && !preDef.kind.isTheorem then @@ -121,13 +122,13 @@ def addAndCompileNonRec (preDef : PreDefinition) : TermElabM Unit := do def addNonRec (preDef : PreDefinition) : TermElabM Unit := do addNonRecAux preDef false -def addAndCompileUnsafe (preDefs : Array PreDefinition) : TermElabM Unit := do +def addAndCompileUnsafe (preDefs : Array PreDefinition) (safety := DefinitionSafety.unsafe) : TermElabM Unit := do let decl := Declaration.mutualDefnDecl $ preDefs.toList.map fun preDef => { name := preDef.declName, lparams := preDef.lparams, type := preDef.type, value := preDef.value, - isUnsafe := true, + safety := safety, hints := ReducibilityHints.opaque } addDecl decl @@ -136,8 +137,8 @@ def addAndCompileUnsafe (preDefs : Array PreDefinition) : TermElabM Unit := do applyAttributesOf preDefs AttributeApplicationTime.afterCompilation pure () -def addAndCompileUnsafeRec (preDefs : Array PreDefinition) : TermElabM Unit := do - addAndCompileUnsafe $ preDefs.map fun preDef => +def addAndCompilePartialRec (preDefs : Array PreDefinition) : TermElabM Unit := do + addAndCompileUnsafe (safety := DefinitionSafety.partial) <| preDefs.map fun preDef => { preDef with declName := Compiler.mkUnsafeRecName preDef.declName, value := preDef.value.replace fun e => match e with diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean index b575dcd66b..540c8d6b0b 100644 --- a/src/Lean/Elab/PreDefinition/Main.lean +++ b/src/Lean/Elab/PreDefinition/Main.lean @@ -20,7 +20,7 @@ private def addAndCompilePartial (preDefs : Array PreDefinition) : TermElabM Uni kind := DefKind.«opaque», value := inh } - addAndCompileUnsafeRec preDefs + addAndCompilePartialRec preDefs private def isNonRecursive (preDef : PreDefinition) : Bool := Option.isNone $ preDef.value.find? fun diff --git a/src/Lean/Elab/PreDefinition/Structural.lean b/src/Lean/Elab/PreDefinition/Structural.lean index 5a5bf35fc5..6dbb97d403 100644 --- a/src/Lean/Elab/PreDefinition/Structural.lean +++ b/src/Lean/Elab/PreDefinition/Structural.lean @@ -433,7 +433,7 @@ def structuralRecursion (preDefs : Array PreDefinition) : TermElabM Unit := else do let (preDefNonRec, state) ← run $ elimRecursion preDefs[0] mapError (addNonRec preDefNonRec) (fun msg => m!"structural recursion failed, produced type incorrect term{indentD msg}") - addAndCompileUnsafeRec preDefs + addAndCompilePartialRec preDefs addSmartUnfoldingDef preDefs[0] state builtin_initialize diff --git a/src/Lean/Elab/Print.lean b/src/Lean/Elab/Print.lean index ec06bb0378..8335e4ff26 100644 --- a/src/Lean/Elab/Print.lean +++ b/src/Lean/Elab/Print.lean @@ -20,8 +20,12 @@ private def lparamsToMessageData (lparams : List Name) : MessageData := m := m ++ ", " ++ u return m ++ "}" -private def mkHeader (kind : String) (id : Name) (lparams : List Name) (type : Expr) (isUnsafe : Bool) : CommandElabM MessageData := do - let m : MessageData := if isUnsafe then "unsafe " else "" +private def mkHeader (kind : String) (id : Name) (lparams : List Name) (type : Expr) (safety : DefinitionSafety) : CommandElabM MessageData := do + let m : MessageData := + match safety with + | DefinitionSafety.unsafe => "unsafe " + | DefinitionSafety.partial => "partial " + | DefinitionSafety.safe => "" let m := if isProtected (← getEnv) id then m ++ "protected " else m let (m, id) := match privateToUserName? id with | some id => (m ++ "private ", id) @@ -29,20 +33,23 @@ private def mkHeader (kind : String) (id : Name) (lparams : List Name) (type : E let m := m ++ kind ++ " " ++ id ++ lparamsToMessageData lparams ++ " : " ++ type pure m -private def printDefLike (kind : String) (id : Name) (lparams : List Name) (type : Expr) (value : Expr) (isUnsafe := false) : CommandElabM Unit := do - let m ← mkHeader kind id lparams type isUnsafe +private def mkHeader' (kind : String) (id : Name) (lparams : List Name) (type : Expr) (isUnsafe : Bool) : CommandElabM MessageData := + mkHeader kind id lparams type (if isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe) + +private def printDefLike (kind : String) (id : Name) (lparams : List Name) (type : Expr) (value : Expr) (safety := DefinitionSafety.safe) : CommandElabM Unit := do + let m ← mkHeader kind id lparams type safety let m := m ++ " :=" ++ Format.line ++ value logInfo m private def printAxiomLike (kind : String) (id : Name) (lparams : List Name) (type : Expr) (isUnsafe := false) : CommandElabM Unit := do - logInfo (← mkHeader kind id lparams type isUnsafe) + logInfo (← mkHeader' kind id lparams type isUnsafe) private def printQuot (kind : QuotKind) (id : Name) (lparams : List Name) (type : Expr) : CommandElabM Unit := do printAxiomLike "Quotient primitive" id lparams type private def printInduct (id : Name) (lparams : List Name) (nparams : Nat) (nindices : Nat) (type : Expr) (ctors : List Name) (isUnsafe : Bool) : CommandElabM Unit := do - let mut m ← mkHeader "inductive" id lparams type isUnsafe + let mut m ← mkHeader' "inductive" id lparams type isUnsafe m := m ++ Format.line ++ "constructors:" for ctor in ctors do let cinfo ← getConstInfo ctor @@ -52,7 +59,7 @@ private def printInduct (id : Name) (lparams : List Name) (nparams : Nat) (nindi private def printIdCore (id : Name) : CommandElabM Unit := do match (← getEnv).find? id with | ConstantInfo.axiomInfo { lparams := us, type := t, isUnsafe := u, .. } => printAxiomLike "axiom" id us t u - | ConstantInfo.defnInfo { lparams := us, type := t, value := v, isUnsafe := u, .. } => printDefLike "def" id us t v u + | ConstantInfo.defnInfo { lparams := us, type := t, value := v, safety := s, .. } => printDefLike "def" id us t v s | ConstantInfo.thmInfo { lparams := us, type := t, value := v, .. } => printDefLike "theorem" id us t v | ConstantInfo.opaqueInfo { lparams := us, type := t, isUnsafe := u, .. } => printAxiomLike "constant" id us t u | ConstantInfo.quotInfo { kind := kind, lparams := us, type := t, .. } => printQuot kind id us t diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 2664607bcf..7c41939ba1 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -1361,7 +1361,7 @@ unsafe def evalExpr (α) (typeName : Name) (value : Expr) : TermElabM α := let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := value, hints := ReducibilityHints.opaque, - isUnsafe := true + safety := DefinitionSafety.unsafe } ensureNoUnassignedMVars decl addAndCompile decl diff --git a/src/Lean/KeyedDeclsAttribute.lean b/src/Lean/KeyedDeclsAttribute.lean index 42bd84f0b3..28060870d6 100644 --- a/src/Lean/KeyedDeclsAttribute.lean +++ b/src/Lean/KeyedDeclsAttribute.lean @@ -102,7 +102,8 @@ def declareBuiltin {γ} (df : Def γ) (attrDeclName : Name) (env : Environment) let name := `_regBuiltin ++ declName let type := mkApp (mkConst `IO) (mkConst `Unit) let val := mkAppN (mkConst `Lean.KeyedDeclsAttribute.addBuiltin) #[mkConst df.valueTypeName, mkConst attrDeclName, toExpr key, mkConst declName] - let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque, isUnsafe := false } + let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque, + safety := DefinitionSafety.safe } match env.addAndCompile {} decl with -- TODO: pretty print error | Except.error e => do diff --git a/src/Lean/Meta/Closure.lean b/src/Lean/Meta/Closure.lean index d76f23d68d..b80e5ddfd0 100644 --- a/src/Lean/Meta/Closure.lean +++ b/src/Lean/Meta/Closure.lean @@ -356,7 +356,7 @@ def mkAuxDefinition (name : Name) (type : Expr) (value : Expr) (zeta : Bool := f type := result.type, value := result.value, hints := ReducibilityHints.regular (getMaxHeight env result.value + 1), - isUnsafe := env.hasUnsafe result.type || env.hasUnsafe result.value + safety := if env.hasUnsafe result.type || env.hasUnsafe result.value then DefinitionSafety.unsafe else DefinitionSafety.safe } trace[Meta.debug]! "{name} : {result.type} := {result.value}" addDecl decl diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean index 6a9ec81abf..87a299462e 100644 --- a/src/Lean/Parser/Extension.lean +++ b/src/Lean/Parser/Extension.lean @@ -422,7 +422,8 @@ def declareBuiltinParser (env : Environment) (addFnName : Name) (catName : Name) let name := `_regBuiltinParser ++ declName let type := mkApp (mkConst `IO) (mkConst `Unit) let val := mkAppN (mkConst addFnName) #[toExpr catName, toExpr declName, mkConst declName, mkNatLit prio] - let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque, isUnsafe := false } + let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque, + safety := DefinitionSafety.safe } match env.addAndCompile {} decl with -- TODO: pretty print error | Except.error _ => throw (IO.userError ("failed to emit registration code for builtin parser '" ++ toString declName ++ "'")) diff --git a/src/Lean/ParserCompiler.lean b/src/Lean/ParserCompiler.lean index 51cfb1089f..0076f3c4e8 100644 --- a/src/Lean/ParserCompiler.lean +++ b/src/Lean/ParserCompiler.lean @@ -83,7 +83,7 @@ partial def compileParserExpr (e : Expr) : MetaM Expr := do pure $ mkForall `_ BinderInfo.default paramTy ty let decl := Declaration.defnDecl { name := c', lparams := [], - type := ty, value := value, hints := ReducibilityHints.opaque, isUnsafe := false } + 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 9f5f90c757..4119dc5406 100644 --- a/src/kernel/declaration.cpp +++ b/src/kernel/declaration.cpp @@ -62,15 +62,15 @@ 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 is_unsafe); -extern "C" uint8 lean_definition_val_is_unsafe(object * v); +extern "C" object * lean_mk_definition_val(object * n, object * lparams, object * type, object * value, object * hints, uint8 safety); +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, bool is_unsafe): +definition_val::definition_val(name const & n, names const & lparams, expr const & type, expr const & val, reducibility_hints const & hints, definition_safety safety): 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(), is_unsafe)) { + hints.to_obj_arg(), static_cast(safety))) { } -bool definition_val::is_unsafe() const { return lean_definition_val_is_unsafe(to_obj_arg()); } +definition_safety definition_val::get_safety() const { return static_cast(lean_definition_val_get_safety(to_obj_arg())); } theorem_val::theorem_val(name const & n, names const & lparams, expr const & type, expr const & val): object_ref(mk_cnstr(0, constant_val(n, lparams, type), val)) { @@ -147,7 +147,7 @@ bool recursor_val::is_unsafe() const { return lean_recursor_is_unsafe(to_obj_arg bool declaration::is_unsafe() const { switch (kind()) { - case declaration_kind::Definition: return to_definition_val().is_unsafe(); + case declaration_kind::Definition: return to_definition_val().get_safety() == definition_safety::unsafe; case declaration_kind::Axiom: return to_axiom_val().is_unsafe(); case declaration_kind::Theorem: return false; case declaration_kind::Opaque: return to_opaque_val().is_unsafe(); @@ -191,19 +191,19 @@ static unsigned get_max_height(environment const & env, expr const & v) { return h; } -definition_val mk_definition_val(environment const & env, name const & n, names const & params, expr const & t, expr const & v, bool unsafe) { +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), unsafe); + return definition_val(n, params, t, v, reducibility_hints::mk_regular(h+1), s); } declaration mk_definition(name const & n, names const & params, expr const & t, expr const & v, - reducibility_hints const & h, bool unsafe) { - return declaration(mk_cnstr(static_cast(declaration_kind::Definition), definition_val(n, params, t, v, h, unsafe))); + reducibility_hints const & h, definition_safety safety) { + return declaration(mk_cnstr(static_cast(declaration_kind::Definition), definition_val(n, params, t, v, h, safety))); } declaration mk_definition(environment const & env, name const & n, names const & params, expr const & t, - expr const & v, bool unsafe) { - return declaration(mk_cnstr(static_cast(declaration_kind::Definition), mk_definition_val(env, n, params, t, v, unsafe))); + expr const & v, definition_safety safety) { + return declaration(mk_cnstr(static_cast(declaration_kind::Definition), mk_definition_val(env, n, params, t, v, safety))); } declaration mk_theorem(name const & n, names const & params, expr const & t, expr const & v) { @@ -218,17 +218,21 @@ declaration mk_axiom(name const & n, names const & params, expr const & t, bool return declaration(mk_cnstr(static_cast(declaration_kind::Axiom), axiom_val(n, params, t, unsafe))); } +static definition_safety to_safety(bool unsafe) { + return unsafe ? definition_safety::unsafe : definition_safety::safe; +} + declaration mk_definition_inferring_unsafe(environment const & env, name const & n, names const & params, expr const & t, expr const & v, reducibility_hints const & hints) { bool unsafe = use_unsafe(env, t) || use_unsafe(env, v); - return mk_definition(n, params, t, v, hints, unsafe); + return mk_definition(n, params, t, v, hints, to_safety(unsafe)); } declaration mk_definition_inferring_unsafe(environment const & env, name const & n, names const & params, expr const & t, expr const & v) { bool unsafe = use_unsafe(env, t) && use_unsafe(env, v); unsigned h = get_max_height(env, v); - return mk_definition(n, params, t, v, reducibility_hints::mk_regular(h+1), unsafe); + return mk_definition(n, params, t, v, reducibility_hints::mk_regular(h+1), to_safety(unsafe)); } declaration mk_axiom_inferring_unsafe(environment const & env, name const & n, @@ -301,7 +305,7 @@ reducibility_hints const & constant_info::get_hints() const { bool constant_info::is_unsafe() const { switch (kind()) { case constant_info_kind::Axiom: return to_axiom_val().is_unsafe(); - case constant_info_kind::Definition: return to_definition_val().is_unsafe(); + case constant_info_kind::Definition: return to_definition_val().get_safety() == definition_safety::unsafe; case constant_info_kind::Theorem: return false; case constant_info_kind::Opaque: return to_opaque_val().is_unsafe(); case constant_info_kind::Quot: return false; diff --git a/src/kernel/declaration.h b/src/kernel/declaration.h index 4fb4158fc3..5148c26222 100644 --- a/src/kernel/declaration.h +++ b/src/kernel/declaration.h @@ -92,13 +92,15 @@ public: bool is_unsafe() const; }; +enum class definition_safety { unsafe, safe, partial }; + /* structure definition_val extends constant_val := (value : expr) (hints : reducibility_hints) (is_unsafe : bool) */ 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, bool is_unsafe); + 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 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; } @@ -109,7 +111,8 @@ public: expr const & get_type() const { return to_constant_val().get_type(); } expr const & get_value() const { return static_cast(cnstr_get_ref(*this, 1)); } reducibility_hints const & get_hints() const { return static_cast(cnstr_get_ref(*this, 2)); } - bool is_unsafe() const; + definition_safety get_safety() const; + bool is_unsafe() const { return get_safety() == definition_safety::unsafe; } }; typedef list_ref definition_vals; @@ -232,11 +235,11 @@ inline optional none_declaration() { return optional() inline optional some_declaration(declaration const & o) { return optional(o); } inline optional some_declaration(declaration && o) { return optional(std::forward(o)); } -definition_val mk_definition_val(environment const & env, name const & n, names const & lparams, expr const & t, expr const & v, bool unsafe); +definition_val mk_definition_val(environment const & env, name const & n, names const & lparams, expr const & t, expr const & v, definition_safety safety); declaration mk_definition(name const & n, names const & lparams, expr const & t, expr const & v, - reducibility_hints const & hints, bool unsafe = false); + reducibility_hints const & hints, definition_safety safety = definition_safety::safe); declaration mk_definition(environment const & env, name const & n, names const & lparams, expr const & t, expr const & v, - bool unsafe = false); + definition_safety safety = definition_safety::safe); declaration mk_theorem(name const & n, names const & lparams, expr const & t, expr const & v); declaration mk_theorem(name const & n, names const & lparams, expr const & t, expr const & v); declaration mk_opaque(name const & n, names const & lparams, expr const & t, expr const & v, bool unsafe); diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 8f950753f9..e2c6513d90 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -199,13 +199,18 @@ environment environment::add_opaque(declaration const & d, bool check) const { environment environment::add_mutual(declaration const & d, bool check) const { definition_vals const & vs = d.to_definition_vals(); + if (empty(vs)) + throw kernel_exception(*this, "invalid empty mutual definition"); + definition_safety safety = head(vs).get_safety(); + if (safety == definition_safety::safe) + throw kernel_exception(*this, "invalid mutual definition, declaration is not tagged as unsafe/partial"); + bool safe_only = safety == definition_safety::partial; /* Check declarations header */ if (check) { - bool safe_only = false; type_checker checker(*this, safe_only); for (definition_val const & v : vs) { - if (!v.is_unsafe()) - throw kernel_exception(*this, "invalid mutual definition, declaration is not tagged as meta"); + if (v.get_safety() != safety) + throw kernel_exception(*this, "invalid mutual definition, declarations must have the same safety annotation"); check_constant_val(*this, v.to_constant_val(), checker); } } @@ -216,7 +221,6 @@ environment environment::add_mutual(declaration const & d, bool check) const { } /* Check actual definitions */ if (check) { - bool safe_only = false; type_checker checker(new_env, safe_only); for (definition_val const & v : vs) { check_no_metavar_no_fvar(new_env, v.get_name(), v.get_value()); diff --git a/src/library/compiler/util.cpp b/src/library/compiler/util.cpp index faf77c868b..4d46bf7904 100644 --- a/src/library/compiler/util.cpp +++ b/src/library/compiler/util.cpp @@ -545,7 +545,7 @@ expr mk_runtime_type(type_checker::state & st, local_ctx const & lctx, expr e) { } environment register_stage1_decl(environment const & env, name const & n, names const & ls, expr const & t, expr const & v) { - declaration aux_decl = mk_definition(mk_cstage1_name(n), ls, t, v, reducibility_hints::mk_opaque(), true); + declaration aux_decl = mk_definition(mk_cstage1_name(n), ls, t, v, reducibility_hints::mk_opaque(), definition_safety::unsafe); return env.add(aux_decl, false); } @@ -555,7 +555,7 @@ bool is_stage2_decl(environment const & env, name const & n) { environment register_stage2_decl(environment const & env, name const & n, expr const & t, expr const & v) { declaration aux_decl = mk_definition(mk_cstage2_name(n), names(), t, - v, reducibility_hints::mk_opaque(), true); + v, reducibility_hints::mk_opaque(), definition_safety::unsafe); return env.add(aux_decl, false); }