From b1a3ea4855b1e150b2e677a6d5466458893d6c60 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 15 May 2019 18:47:22 +0200 Subject: Inverting the responsibility to define logically a constant in Declare. The code was intricate due to the special handling of side-effects, while it was sufficient to extrude the logical definition to make it clearer. We thus declare a constant in two parts, first purely kernel-related, then purely libobject-related. --- library/lib.ml | 3 --- library/lib.mli | 1 - 2 files changed, 4 deletions(-) (limited to 'library') diff --git a/library/lib.ml b/library/lib.ml index a046360822..4be288ed20 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -211,9 +211,6 @@ let split_lib_at_opening sp = let add_entry sp node = lib_state := { !lib_state with lib_stk = (sp,node) :: !lib_state.lib_stk } -let pull_to_head oname = - lib_state := { !lib_state with lib_stk = (oname,List.assoc oname !lib_state.lib_stk) :: List.remove_assoc oname !lib_state.lib_stk } - let anonymous_id = let n = ref 0 in fun () -> incr n; Names.Id.of_string ("_" ^ (string_of_int !n)) diff --git a/library/lib.mli b/library/lib.mli index 30569197bc..5da76961a6 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -57,7 +57,6 @@ val segment_of_objects : val add_leaf : Id.t -> Libobject.obj -> Libobject.object_name val add_anonymous_leaf : ?cache_first:bool -> Libobject.obj -> unit -val pull_to_head : Libobject.object_name -> unit (** this operation adds all objects with the same name and calls [load_object] for each of them *) -- cgit v1.2.3 From 93aa8aad110a2839d16dce53af12f0728b59ed2a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 14 May 2019 20:27:24 +0200 Subject: Merge the definition of constants and private constants in the API. --- library/global.ml | 2 +- library/global.mli | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'library') diff --git a/library/global.ml b/library/global.ml index 06e06a8cf2..33cdbd88ea 100644 --- a/library/global.ml +++ b/library/global.ml @@ -94,7 +94,7 @@ let make_sprop_cumulative () = globalize0 Safe_typing.make_sprop_cumulative let set_allow_sprop b = globalize0 (Safe_typing.set_allow_sprop b) let sprop_allowed () = Environ.sprop_allowed (env()) let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd) -let add_constant ~in_section id d = globalize (Safe_typing.add_constant ~in_section (i2l id) d) +let add_constant ?role ~in_section id d = globalize (Safe_typing.add_constant ?role ~in_section (i2l id) d) let add_mind id mie = globalize (Safe_typing.add_mind (i2l id) mie) let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl) let add_module id me inl = globalize (Safe_typing.add_module (i2l id) me inl) diff --git a/library/global.mli b/library/global.mli index a60de48897..f65ffaa2ee 100644 --- a/library/global.mli +++ b/library/global.mli @@ -46,7 +46,7 @@ val export_private_constants : in_section:bool -> unit Entries.definition_entry * Safe_typing.exported_private_constant list val add_constant : - in_section:bool -> Id.t -> Safe_typing.global_declaration -> Constant.t + ?role:Entries.side_effect_role -> in_section:bool -> Id.t -> Safe_typing.global_declaration -> Constant.t * Safe_typing.private_constants val add_mind : Id.t -> Entries.mutual_inductive_entry -> MutInd.t -- cgit v1.2.3 From 801aed67a90ec49c15a4469e1905aa2835fabe19 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 15 May 2019 23:50:42 +0200 Subject: Parameterize the constant_body type by opaque subproofs. --- library/global.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'library') diff --git a/library/global.mli b/library/global.mli index f65ffaa2ee..eabae89d8d 100644 --- a/library/global.mli +++ b/library/global.mli @@ -84,7 +84,7 @@ val add_module_parameter : (** {6 Queries in the global environment } *) val lookup_named : variable -> Constr.named_declaration -val lookup_constant : Constant.t -> Declarations.constant_body +val lookup_constant : Constant.t -> Opaqueproof.opaque Declarations.constant_body val lookup_inductive : inductive -> Declarations.mutual_inductive_body * Declarations.one_inductive_body val lookup_pinductive : Constr.pinductive -> @@ -105,7 +105,7 @@ val body_of_constant : Constant.t -> (Constr.constr * Univ.AUContext.t) option polymorphic constants, the term contains De Bruijn universe variables that need to be instantiated. *) -val body_of_constant_body : Declarations.constant_body -> (Constr.constr * Univ.AUContext.t) option +val body_of_constant_body : Opaqueproof.opaque Declarations.constant_body -> (Constr.constr * Univ.AUContext.t) option (** Same as {!body_of_constant} but on {!Declarations.constant_body}. *) (** {6 Compiled libraries } *) -- cgit v1.2.3 From 27468ae02bbbf018743d53a9db49efa34b6d6a3e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 16 May 2019 00:02:54 +0200 Subject: Ensure statically that declarations built by Term_typing are direct. This removes a lot of cruft breaking the opaque proof abstraction in Safe_typing and similar. --- library/global.ml | 1 + library/global.mli | 1 + 2 files changed, 2 insertions(+) (limited to 'library') diff --git a/library/global.ml b/library/global.ml index 33cdbd88ea..58e2380440 100644 --- a/library/global.ml +++ b/library/global.ml @@ -95,6 +95,7 @@ let set_allow_sprop b = globalize0 (Safe_typing.set_allow_sprop b) let sprop_allowed () = Environ.sprop_allowed (env()) let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd) let add_constant ?role ~in_section id d = globalize (Safe_typing.add_constant ?role ~in_section (i2l id) d) +let add_recipe ~in_section id d = globalize (Safe_typing.add_recipe ~in_section (i2l id) d) let add_mind id mie = globalize (Safe_typing.add_mind (i2l id) mie) let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl) let add_module id me inl = globalize (Safe_typing.add_module (i2l id) me inl) diff --git a/library/global.mli b/library/global.mli index eabae89d8d..984d8c666c 100644 --- a/library/global.mli +++ b/library/global.mli @@ -47,6 +47,7 @@ val export_private_constants : in_section:bool -> val add_constant : ?role:Entries.side_effect_role -> in_section:bool -> Id.t -> Safe_typing.global_declaration -> Constant.t * Safe_typing.private_constants +val add_recipe : in_section:bool -> Id.t -> Cooking.recipe -> Constant.t val add_mind : Id.t -> Entries.mutual_inductive_entry -> MutInd.t -- cgit v1.2.3