aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/check.ml37
-rw-r--r--checker/declarations.ml36
-rw-r--r--checker/declarations.mli13
-rw-r--r--checker/mod_checking.ml2
-rw-r--r--checker/safe_typing.ml113
-rw-r--r--checker/safe_typing.mli18
-rw-r--r--doc/refman/RefMan-com.tex14
-rw-r--r--kernel/declareops.ml14
-rw-r--r--kernel/declareops.mli8
-rw-r--r--kernel/lazyconstr.ml57
-rw-r--r--kernel/lazyconstr.mli35
-rw-r--r--kernel/safe_typing.ml149
-rw-r--r--kernel/safe_typing.mli11
-rw-r--r--kernel/term_typing.ml37
-rw-r--r--library/assumptions.ml2
-rw-r--r--library/library.ml133
-rw-r--r--library/states.ml2
-rw-r--r--plugins/funind/functional_principles_proofs.ml6
-rw-r--r--plugins/funind/functional_principles_types.ml3
-rw-r--r--plugins/funind/indfun.ml3
-rw-r--r--plugins/funind/indfun_common.ml2
-rw-r--r--plugins/funind/recdef.ml2
-rw-r--r--plugins/xml/xmlcommand.ml3
-rw-r--r--printing/prettyp.ml2
-rw-r--r--toplevel/coqtop.ml3
-rw-r--r--toplevel/lemmas.ml2
26 files changed, 296 insertions, 411 deletions
diff --git a/checker/check.ml b/checker/check.ml
index eb4016f5f..1b9fd0701 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -40,7 +40,7 @@ type compilation_unit_name = DirPath.t
type library_disk = {
md_name : compilation_unit_name;
- md_compiled : Safe_typing.LightenLibrary.lightened_compiled_library;
+ md_compiled : Safe_typing.compiled_library;
md_objects : library_objects;
md_deps : (compilation_unit_name * Digest.t) array;
md_imports : compilation_unit_name array }
@@ -56,6 +56,7 @@ type library_t = {
library_name : compilation_unit_name;
library_filename : CUnix.physical_path;
library_compiled : Safe_typing.compiled_library;
+ library_opaques : Term.constr array;
library_deps : (compilation_unit_name * Digest.t) array;
library_digest : Digest.t }
@@ -91,6 +92,19 @@ let library_full_filename dir = (find_library dir).library_filename
let register_loaded_library m =
libraries_table := LibraryMap.add m.library_name m !libraries_table
+(* Map from library names to table of opaque terms *)
+let opaque_tables = ref LibraryMap.empty
+
+let access_opaque_table dp i =
+ let t =
+ try LibraryMap.find dp !opaque_tables
+ with Not_found -> assert false
+ in
+ assert (i < Array.length t);
+ t.(i)
+
+let _ = Declarations.indirect_opaque_access := access_opaque_table
+
let check_one_lib admit (dir,m) =
let file = m.library_filename in
let md = m.library_compiled in
@@ -105,7 +119,7 @@ let check_one_lib admit (dir,m) =
else
(Flags.if_verbose ppnl
(str "Checking library: " ++ pr_dirpath dir);
- Safe_typing.import file md dig);
+ Safe_typing.import file md m.library_opaques dig);
Flags.if_verbose pp (fnl());
pp_flush ();
register_loaded_library m
@@ -280,7 +294,8 @@ let with_magic_number_check f a =
let mk_library md f table digest = {
library_name = md.md_name;
library_filename = f;
- library_compiled = Safe_typing.LightenLibrary.load table md.md_compiled;
+ library_compiled = md.md_compiled;
+ library_opaques = table;
library_deps = md.md_deps;
library_digest = digest }
@@ -298,16 +313,24 @@ let intern_from_file (dir, f) =
try
let ch = with_magic_number_check raw_intern_library f in
let (md:library_disk) = System.marshal_in f ch in
- let digest = System.marshal_in f ch in
- let table = (System.marshal_in f ch : Safe_typing.LightenLibrary.table) in
- close_in ch;
+ let (digest:Digest.t) = System.marshal_in f ch in
+ let (table:Term.constr array) = System.marshal_in f ch in
+ (* Verification of the final checksum *)
+ let pos = pos_in ch in
+ let (checksum:Digest.t) = System.marshal_in f ch in
+ let () = close_in ch in
+ let ch = open_in f in
+ if not (String.equal (Digest.channel ch pos) checksum) then
+ errorlabstrm "intern_from_file" (str "Checksum mismatch");
+ let () = close_in ch in
if dir <> md.md_name then
- errorlabstrm "load_physical_library"
+ errorlabstrm "intern_from_file"
(name_clash_message dir md.md_name f);
Flags.if_verbose ppnl (str" done]");
md,table,digest
with e -> Flags.if_verbose ppnl (str" failed!]"); raise e in
depgraph := LibraryMap.add md.md_name md.md_deps !depgraph;
+ opaque_tables := LibraryMap.add md.md_name table !opaque_tables;
mk_library md f table digest
let get_deps (dir, f) =
diff --git a/checker/declarations.ml b/checker/declarations.ml
index af8b1f217..cfaa2f5f7 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -480,24 +480,34 @@ let subst_substituted s r =
let force_constr = force subst_mps
+let from_val c = ref (LSval c)
+
type constr_substituted = constr substituted
let val_cstr_subst = val_substituted val_constr
let subst_constr_subst = subst_substituted
-(** Beware! In .vo files, lazy_constr are stored as integers
- used as indexes for a separate table. The actual lazy_constr is restored
- later, by [Safe_typing.LightenLibrary.load]. This allows us
- to use here a different definition of lazy_constr than coqtop:
- since the checker will inspect all proofs parts, even opaque
- ones, no need to use Lazy.t here *)
+(* Nota : in coqtop, the [lazy_constr] type also have a [Direct]
+ constructor, but it shouldn't occur inside a .vo, so we ignore it *)
+
+type lazy_constr =
+ | Indirect of substitution list * DirPath.t * int
+(* | Direct of constr_substituted *)
+
+let subst_lazy_constr sub = function
+ | Indirect (l,dp,i) -> Indirect (sub::l,dp,i)
+
+let indirect_opaque_access =
+ ref ((fun dp i -> assert false) : DirPath.t -> int -> constr)
+
+let force_lazy_constr = function
+ | Indirect (l,dp,i) ->
+ let c = !indirect_opaque_access dp i in
+ force_constr (List.fold_right subst_constr_subst l (from_val c))
-type lazy_constr = constr_substituted
-let subst_lazy_constr = subst_substituted
-let force_lazy_constr = force_constr
-let lazy_constr_from_val c = c
-let val_lazy_constr = val_cstr_subst
+let val_lazy_constr =
+ val_sum "lazy_constr" 0 [|[|val_list val_subst;val_dp;val_int|]|]
(** Inlining level of parameters at functor applications.
This is ignored by the checker. *)
@@ -532,8 +542,8 @@ type constant_body = {
let body_of_constant cb = match cb.const_body with
| Undef _ -> None
- | Def c -> Some c
- | OpaqueDef c -> Some c
+ | Def c -> Some (force_constr c)
+ | OpaqueDef c -> Some (force_lazy_constr c)
let constant_has_body cb = match cb.const_body with
| Undef _ -> false
diff --git a/checker/declarations.mli b/checker/declarations.mli
index 80c895bbe..cc3123ca7 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -30,16 +30,9 @@ type constr_substituted
val force_constr : constr_substituted -> constr
val from_val : constr -> constr_substituted
-(** Beware! In .vo files, lazy_constr are stored as integers
- used as indexes for a separate table. The actual lazy_constr is restored
- later, by [Safe_typing.LightenLibrary.load]. This allows us
- to use here a different definition of lazy_constr than coqtop:
- since the checker will inspect all proofs parts, even opaque
- ones, no need to use Lazy.t here *)
-
type lazy_constr
-val force_lazy_constr : lazy_constr -> constr
-val lazy_constr_from_val : constr_substituted -> lazy_constr
+
+val indirect_opaque_access : (DirPath.t -> int -> constr) ref
(** Inlining level of parameters at functor applications.
This is ignored by the checker. *)
@@ -63,7 +56,7 @@ type constant_body = {
const_native_name : native_name ref;
const_inline_code : bool }
-val body_of_constant : constant_body -> constr_substituted option
+val body_of_constant : constant_body -> constr option
val constant_has_body : constant_body -> bool
val is_opaque : constant_body -> bool
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index bc4ea7c69..ebe44997d 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -35,7 +35,7 @@ let check_constant_declaration env kn cb =
let _ = infer_type envty ty in
(match body_of_constant cb with
| Some bd ->
- let j = infer env' (force_constr bd) in
+ let j = infer env' bd in
conv_leq envty j ty
| None -> ())
| PolymorphicArity(ctxt,par) ->
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 5cbcc00f5..492f5bc20 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -59,117 +59,19 @@ let check_imports f caller env needed =
in
Array.iter check needed
+type nativecode_symb_array
type compiled_library =
DirPath.t *
module_body *
(DirPath.t * Digest.t) array *
- engagement option
-
- (* Store the body of modules' opaque constants inside a table.
-
- This module is used during the serialization and deserialization
- of vo files.
-
- By adding an indirection to the opaque constant definitions, we
- gain the ability not to load them. As these constant definitions
- are usually big terms, we save a deserialization time as well as
- some memory space. *)
-module LightenLibrary : sig
- type table
- type lightened_compiled_library
- val load : table -> lightened_compiled_library -> compiled_library
-end = struct
-
- (* The table is implemented as an array of [constr_substituted].
- Keys are hence integers. To avoid changing the [compiled_library]
- type, we brutally encode integers into [lazy_constr]. This isn't
- pretty, but shouldn't be dangerous since the produced structure
- [lightened_compiled_library] is abstract and only meant for writing
- to .vo via Marshal (which doesn't care about types).
- *)
- type table = constr_substituted array
- let key_of_lazy_constr (c:lazy_constr) = (Obj.magic c : int)
-
- (* To avoid any future misuse of the lightened library that could
- interpret encoded keys as real [constr_substituted], we hide
- these kind of values behind an abstract datatype. *)
- type lightened_compiled_library = compiled_library
-
- (* Map a [compiled_library] to another one by just updating
- the opaque term [t] to [on_opaque_const_body t]. *)
- let traverse_library on_opaque_const_body =
- let rec traverse_module mb =
- match mb.mod_expr with
- None ->
- { mb with
- mod_expr = None;
- mod_type = traverse_modexpr mb.mod_type;
- }
- | Some impl when impl == mb.mod_type->
- let mtb = traverse_modexpr mb.mod_type in
- { mb with
- mod_expr = Some mtb;
- mod_type = mtb;
- }
- | Some impl ->
- { mb with
- mod_expr = Option.map traverse_modexpr mb.mod_expr;
- mod_type = traverse_modexpr mb.mod_type;
- }
- and traverse_struct struc =
- let traverse_body (l,body) = (l,match body with
- | (SFBconst cb) when is_opaque cb ->
- SFBconst {cb with const_body = on_opaque_const_body cb.const_body}
- | (SFBconst _ | SFBmind _ ) as x ->
- x
- | SFBmodule m ->
- SFBmodule (traverse_module m)
- | SFBmodtype m ->
- SFBmodtype ({m with typ_expr = traverse_modexpr m.typ_expr}))
- in
- List.map traverse_body struc
-
- and traverse_modexpr = function
- | SEBfunctor (mbid,mty,mexpr) ->
- SEBfunctor (mbid,
- ({mty with
- typ_expr = traverse_modexpr mty.typ_expr}),
- traverse_modexpr mexpr)
- | SEBident mp as x -> x
- | SEBstruct (struc) ->
- SEBstruct (traverse_struct struc)
- | SEBapply (mexpr,marg,u) ->
- SEBapply (traverse_modexpr mexpr,traverse_modexpr marg,u)
- | SEBwith (seb,wdcl) ->
- SEBwith (traverse_modexpr seb,wdcl)
- in
- fun (dp,mb,depends,s) -> (dp,traverse_module mb,depends,s)
-
- (* Loading is also a traversing that decodes the embedded keys that
- are inside the [lightened_library]. If the [load_proof] flag is
- set, we lookup inside the table to graft the
- [constr_substituted]. Otherwise, we set the [const_body] field
- to [None].
- *)
- let load table lightened_library =
- let decode_key = function
- | Undef _ | Def _ -> assert false
- | OpaqueDef k ->
- let k = key_of_lazy_constr k in
- let body =
- try table.(k)
- with _ -> error "Error while retrieving an opaque body"
- in
- OpaqueDef (lazy_constr_from_val body)
- in
- traverse_library decode_key lightened_library
-
-end
+ engagement option *
+ nativecode_symb_array
open Validate
let val_deps = val_array (val_tuple ~name:"dep"[|val_dp;no_val|])
-let val_vo = val_tuple ~name:"vo" [|val_dp;val_module;val_deps;val_opt val_eng|]
+let val_vo = val_tuple ~name:"vo"
+ [|val_dp;val_module;val_deps;val_opt val_eng; no_val|]
(* This function should append a certificate to the .vo file.
The digest must be part of the certicate to rule out attackers
@@ -180,8 +82,9 @@ let stamp_library file digest = ()
(* When the module is checked, digests do not need to match, but a
warning is issued in case of mismatch *)
-let import file (dp,mb,depends,engmt as vo) digest =
+let import file (dp,mb,depends,engmt,_ as vo) table digest =
Validate.apply !Flags.debug val_vo vo;
+ Validate.apply !Flags.debug (val_array Term.val_constr) table;
Flags.if_verbose ppnl (str "*** vo structure validated ***"); pp_flush ();
let env = !genv in
check_imports msg_warning dp env depends;
@@ -193,7 +96,7 @@ let import file (dp,mb,depends,engmt as vo) digest =
full_add_module dp mb digest
(* When the module is admitted, digests *must* match *)
-let unsafe_import file (dp,mb,depends,engmt as vo) digest =
+let unsafe_import file (dp,mb,depends,engmt,_ as vo) digest =
if !Flags.debug then ignore vo; (*Validate.apply !Flags.debug val_vo vo;*)
let env = !genv in
check_imports (errorlabstrm"unsafe_import") dp env depends;
diff --git a/checker/safe_typing.mli b/checker/safe_typing.mli
index 4e3c25b1c..a5f014935 100644
--- a/checker/safe_typing.mli
+++ b/checker/safe_typing.mli
@@ -19,22 +19,6 @@ type compiled_library
val set_engagement : Declarations.engagement -> unit
val import :
- CUnix.physical_path -> compiled_library -> Digest.t -> unit
+ CUnix.physical_path -> compiled_library -> constr array -> Digest.t -> unit
val unsafe_import :
CUnix.physical_path -> compiled_library -> Digest.t -> unit
-
-(** Store the body of modules' opaque constants inside a table.
-
- This module is used during the serialization and deserialization
- of vo files.
-*)
-module LightenLibrary :
-sig
- type table
- type lightened_compiled_library
-
- (** [load table lcl] builds a compiled library from a
- lightened library [lcl] by remplacing every index by its related
- opaque terms inside [table]. *)
- val load : table -> lightened_compiled_library -> compiled_library
-end
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 3bf9e7cb5..543dce18f 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -219,25 +219,19 @@ Section~\ref{LongNames}).
\item[{\tt -dont-load-proofs}]\
- Warning: this is an unsafe mode.
- Instead of loading in memory the proofs of opaque theorems, they are
- treated as axioms. This results in smaller memory requirement and
- faster compilation, but the behavior of the system might slightly change
- (for instance during module subtyping), and some features won't be
- available (for example {\tt Print Assumptions}).
+ In this mode, it is an error to access the body of opaque theorems
+ (for example via {\tt Print} or {\tt Print Assumptions}).
\item[{\tt -lazy-load-proofs}]\
This is the default behavior. Proofs of opaque theorems aren't
loaded immediately in memory, but only when necessary, for instance
during some module subtyping or {\tt Print Assumptions}. This should be
- almost as fast and efficient as {\tt -dont-load-proofs}, with none
- of its drawbacks.
+ almost as fast and efficient as {\tt -dont-load-proofs}.
\item[{\tt -force-load-proofs}]\
- Proofs of opaque theorems are loaded in memory as soon as the
- corresponding {\tt Require} is done. This used to be Coq's default behavior.
+ Deprecated, now the same as {\tt -lazy-load-proofs}.
\item[{\tt -no-hash-consing}] \mbox{}
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 90327da6c..3c1f6a415 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -18,8 +18,8 @@ open Util
let body_of_constant cb = match cb.const_body with
| Undef _ -> None
- | Def c -> Some c
- | OpaqueDef lc -> Some (force_lazy_constr lc)
+ | Def c -> Some (Lazyconstr.force c)
+ | OpaqueDef lc -> Some (Lazyconstr.force_opaque lc)
let constant_has_body cb = match cb.const_body with
| Undef _ -> false
@@ -84,14 +84,8 @@ let hcons_const_type = function
let hcons_const_def = function
| Undef inl -> Undef inl
- | Def l_constr ->
- let constr = force l_constr in
- Def (from_val (Term.hcons_constr constr))
- | OpaqueDef lc ->
- if lazy_constr_is_val lc then
- let constr = force_opaque lc in
- OpaqueDef (opaque_from_val (Term.hcons_constr constr))
- else OpaqueDef lc
+ | Def cs -> Def (from_val (Term.hcons_constr (Lazyconstr.force cs)))
+ | OpaqueDef lc -> OpaqueDef (Lazyconstr.hcons_lazy_constr lc)
let hcons_const_body cb =
{ cb with
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 1616e4639..c4d67ba52 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -8,7 +8,6 @@
open Declarations
open Mod_subst
-open Lazyconstr
(** Operations concerning types in [Declarations] :
[constant_body], [mutual_inductive_body], [module_body] ... *)
@@ -18,13 +17,14 @@ open Lazyconstr
val subst_const_def : substitution -> constant_def -> constant_def
val subst_const_body : substitution -> constant_body -> constant_body
-(** Is there a actual body in const_body or const_body_opaque ? *)
+(** Is there a actual body in const_body ? *)
val constant_has_body : constant_body -> bool
-(** Accessing const_body_opaque or const_body *)
+(** Accessing const_body, forcing access to opaque proof term if needed.
+ Only use this function if you know what you're doing. *)
-val body_of_constant : constant_body -> constr_substituted option
+val body_of_constant : constant_body -> Term.constr option
val is_opaque : constant_body -> bool
diff --git a/kernel/lazyconstr.ml b/kernel/lazyconstr.ml
index 31cb76575..21aba6348 100644
--- a/kernel/lazyconstr.ml
+++ b/kernel/lazyconstr.ml
@@ -6,6 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Names
open Term
open Mod_subst
@@ -20,24 +21,56 @@ let force = force subst_mps
let subst_constr_subst = subst_substituted
-(** Opaque proof terms are not loaded immediately, but are there
- in a lazy form. Forcing this lazy may trigger some unmarshal of
- the necessary structure. The ['a substituted] type isn't really great
- here, so we store "manually" a substitution list, the younger one at top.
+(** Opaque proof terms might be in some external tables.
+ The [force_opaque] function below allows to access these tables,
+ this might trigger the read of some extra parts of .vo files.
+ In the [Indirect] case, we accumulate "manually" a substitution
+ list, the younger one coming first. Nota: no [Direct] constructor
+ should end in a .vo, this is checked by coqchk.
*)
-type lazy_constr = constr_substituted Lazy.t * substitution list
+type lazy_constr =
+ | Indirect of substitution list * DirPath.t * int (* lib,index *)
+ | Direct of constr_substituted (* opaque in section or interactive session *)
-let force_lazy_constr (c,l) =
- List.fold_right subst_constr_subst l (Lazy.force c)
+(* TODO : this hcons function could probably be improved (for instance
+ hash the dir_path in the Indirect case) *)
-let lazy_constr_is_val (c,_) = Lazy.lazy_is_val c
+let hcons_lazy_constr = function
+ | Direct c -> Direct (from_val (hcons_constr (force c)))
+ | Indirect _ as lc -> lc
-let make_lazy_constr c = (c, [])
+let subst_lazy_constr sub = function
+ | Direct cs -> Direct (subst_constr_subst sub cs)
+ | Indirect (l,dp,i) -> Indirect (sub::l,dp,i)
-let force_opaque lc = force (force_lazy_constr lc)
+let default_get_opaque dp _ =
+ Errors.error
+ ("Cannot access an opaque term in library " ^ DirPath.to_string dp)
+
+let default_mk_opaque _ = None
+
+let get_opaque = ref default_get_opaque
+let mk_opaque = ref default_mk_opaque
+let set_indirect_opaque_accessor f = (get_opaque := f)
+let set_indirect_opaque_creator f = (mk_opaque := f)
+let reset_indirect_opaque_creator () = (mk_opaque := default_mk_opaque)
-let opaque_from_val c = (Lazy.lazy_from_val (from_val c), [])
+let force_lazy_constr = function
+ | Direct c -> c
+ | Indirect (l,dp,i) ->
+ List.fold_right subst_constr_subst l (from_val (!get_opaque dp i))
-let subst_lazy_constr sub (c,l) = (c,sub::l)
+let turn_indirect lc = match lc with
+ | Indirect _ ->
+ Errors.anomaly (Pp.str "Indirecting an already indirect opaque")
+ | Direct c ->
+ (* this constr_substituted shouldn't have been substituted yet *)
+ assert (fst (Mod_subst.repr_substituted c) == None);
+ match !mk_opaque (force c) with
+ | None -> lc
+ | Some (dp,i) -> Indirect ([],dp,i)
+
+let force_opaque lc = force (force_lazy_constr lc)
+let opaque_from_val c = Direct (from_val c)
diff --git a/kernel/lazyconstr.mli b/kernel/lazyconstr.mli
index 17c9bcc76..f6188f536 100644
--- a/kernel/lazyconstr.mli
+++ b/kernel/lazyconstr.mli
@@ -6,6 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Names
open Term
open Mod_subst
@@ -19,16 +20,34 @@ val force : constr_substituted -> constr
val subst_constr_subst :
substitution -> constr_substituted -> constr_substituted
-(** Opaque proof terms are not loaded immediately, but are there
- in a lazy form. Forcing this lazy may trigger some unmarshal of
- the necessary structure. *)
+(** Opaque proof terms might be in some external tables. The
+ [force_opaque] function below allows to access these tables,
+ this might trigger the read of some extra parts of .vo files *)
type lazy_constr
-val subst_lazy_constr : substitution -> lazy_constr -> lazy_constr
-val force_lazy_constr : lazy_constr -> constr_substituted
-val make_lazy_constr : constr_substituted Lazy.t -> lazy_constr
-val lazy_constr_is_val : lazy_constr -> bool
+(** From a [constr] to some (immediate) [lazy_constr]. *)
+val opaque_from_val : constr -> lazy_constr
+
+(** Turn an immediate [lazy_constr] into an indirect one, thanks
+ to the indirect opaque creator configured below. *)
+val turn_indirect : lazy_constr -> lazy_constr
+(** From a [lazy_constr] back to a [constr]. This might use the
+ indirect opaque accessor configured below. *)
val force_opaque : lazy_constr -> constr
-val opaque_from_val : constr -> lazy_constr
+
+val subst_lazy_constr : substitution -> lazy_constr -> lazy_constr
+
+val hcons_lazy_constr : lazy_constr -> lazy_constr
+
+(** When stored indirectly, opaque terms are indexed by their library
+ dirpath and an integer index. The following two functions activate
+ this indirect storage, by telling how to store and retrieve terms.
+ Default creator always returns [None], preventing the creation of
+ any indirect link, and default accessor always raises an error.
+*)
+
+val set_indirect_opaque_creator : (constr -> (DirPath.t * int) option) -> unit
+val set_indirect_opaque_accessor : (DirPath.t -> int -> constr) -> unit
+val reset_indirect_opaque_creator : unit -> unit
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 20ca16476..a1b820466 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -272,6 +272,13 @@ let add_constant dir l decl senv =
let cb = Term_typing.translate_recipe senv.env r in
if DirPath.is_empty dir then Declareops.hcons_const_body cb else cb
in
+ let cb = match cb.const_body with
+ | OpaqueDef lc when DirPath.is_empty dir ->
+ (* In coqc, opaque constants outside sections will be stored
+ indirectly in a specific table *)
+ { cb with const_body = OpaqueDef (Lazyconstr.turn_indirect lc) }
+ | _ -> cb
+ in
let senv' = add_field (l,SFBconst cb) (C kn) senv in
let senv'' = match cb.const_body with
| Undef (Some lev) ->
@@ -767,148 +774,6 @@ let import lib digest senv =
mp, senv, lib.comp_natsymbs
- (* Store the body of modules' opaque constants inside a table.
-
- This module is used during the serialization and deserialization
- of vo files.
-
- By adding an indirection to the opaque constant definitions, we
- gain the ability not to load them. As these constant definitions
- are usually big terms, we save a deserialization time as well as
- some memory space. *)
-module LightenLibrary : sig
- type table
- type lightened_compiled_library
- val save : compiled_library -> lightened_compiled_library * table
- val load : load_proof:Flags.load_proofs -> table Lazy.t
- -> lightened_compiled_library -> compiled_library
-end = struct
-
- (* The table is implemented as an array of [constr_substituted].
- Keys are hence integers. To avoid changing the [compiled_library]
- type, we brutally encode integers into [lazy_constr]. This isn't
- pretty, but shouldn't be dangerous since the produced structure
- [lightened_compiled_library] is abstract and only meant for writing
- to .vo via Marshal (which doesn't care about types).
- *)
- type table = Lazyconstr.constr_substituted array
- let key_as_lazy_constr (i:int) = (Obj.magic i : Lazyconstr.lazy_constr)
- let key_of_lazy_constr (c:Lazyconstr.lazy_constr) = (Obj.magic c : int)
-
- (* To avoid any future misuse of the lightened library that could
- interpret encoded keys as real [constr_substituted], we hide
- these kind of values behind an abstract datatype. *)
- type lightened_compiled_library = compiled_library
-
- (* Map a [compiled_library] to another one by just updating
- the opaque term [t] to [on_opaque_const_body t]. *)
- let traverse_library on_opaque_const_body =
- let rec traverse_module mb =
- match mb.mod_expr with
- None ->
- { mb with
- mod_expr = None;
- mod_type = traverse_modexpr mb.mod_type;
- }
- | Some impl when impl == mb.mod_type->
- let mtb = traverse_modexpr mb.mod_type in
- { mb with
- mod_expr = Some mtb;
- mod_type = mtb;
- }
- | Some impl ->
- { mb with
- mod_expr = Option.map traverse_modexpr mb.mod_expr;
- mod_type = traverse_modexpr mb.mod_type;
- }
- and traverse_struct struc =
- let traverse_body (l,body) = (l,match body with
- | SFBconst cb when Declareops.is_opaque cb ->
- SFBconst {cb with const_body = on_opaque_const_body cb.const_body}
- | (SFBconst _ | SFBmind _ ) as x ->
- x
- | SFBmodule m ->
- SFBmodule (traverse_module m)
- | SFBmodtype m ->
- SFBmodtype ({m with typ_expr = traverse_modexpr m.typ_expr}))
- in
- List.map traverse_body struc
-
- and traverse_modexpr = function
- | SEBfunctor (mbid,mty,mexpr) ->
- SEBfunctor (mbid,
- ({mty with
- typ_expr = traverse_modexpr mty.typ_expr}),
- traverse_modexpr mexpr)
- | SEBident mp as x -> x
- | SEBstruct (struc) ->
- SEBstruct (traverse_struct struc)
- | SEBapply (mexpr,marg,u) ->
- SEBapply (traverse_modexpr mexpr,traverse_modexpr marg,u)
- | SEBwith (seb,wdcl) ->
- SEBwith (traverse_modexpr seb,wdcl)
- in
- fun clib -> { clib with comp_mod = traverse_module clib.comp_mod }
-
- (* To disburden a library from opaque definitions, we simply
- traverse it and add an indirection between the module body
- and its reference to a [const_body]. *)
- let save library =
- let ((insert : constant_def -> constant_def),
- (get_table : unit -> table)) =
- (* We use an integer as a key inside the table. *)
- let counter = ref (-1) in
-
- (* During the traversal, the table is implemented by a list
- to get constant time insertion. *)
- let opaque_definitions = ref [] in
-
- ((* Insert inside the table. *)
- (fun def ->
- let opaque_definition = match def with
- | OpaqueDef lc -> Lazyconstr.force_lazy_constr lc
- | _ -> assert false
- in
- incr counter;
- opaque_definitions := opaque_definition :: !opaque_definitions;
- OpaqueDef (key_as_lazy_constr !counter)),
-
- (* Get the final table representation. *)
- (fun () -> Array.of_list (List.rev !opaque_definitions)))
- in
- let lightened_library = traverse_library insert library in
- (lightened_library, get_table ())
-
- (* Loading is also a traversing that decodes the embedded keys that
- are inside the [lightened_library]. If the [load_proof] flag is
- set, we lookup inside the table to graft the
- [constr_substituted]. Otherwise, we set the [const_body] field
- to [None].
- *)
- let load ~load_proof (table : table Lazy.t) lightened_library =
- let decode_key = function
- | Undef _ | Def _ -> assert false
- | OpaqueDef k ->
- let k = key_of_lazy_constr k in
- let access key =
- try (Lazy.force table).(key)
- with e when Errors.noncritical e ->
- error "Error while retrieving an opaque body"
- in
- match load_proof with
- | Flags.Force ->
- let lc = Lazy.lazy_from_val (access k) in
- OpaqueDef (Lazyconstr.make_lazy_constr lc)
- | Flags.Lazy ->
- let lc = lazy (access k) in
- OpaqueDef (Lazyconstr.make_lazy_constr lc)
- | Flags.Dont ->
- Undef None
- in
- traverse_library decode_key lightened_library
-
-end
-
type judgment = unsafe_judgment
let j_val j = j.uj_val
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 1bb43a53e..cd24bd8d0 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -112,17 +112,6 @@ val export : safe_environment -> DirPath.t
val import : compiled_library -> Digest.t -> safe_environment
-> module_path * safe_environment * Nativecode.symbol array
-(** Remove the body of opaque constants *)
-
-module LightenLibrary :
-sig
- type table
- type lightened_compiled_library
- val save : compiled_library -> lightened_compiled_library * table
- val load : load_proof:Flags.load_proofs -> table Lazy.t ->
- lightened_compiled_library -> compiled_library
-end
-
(** {6 Typing judgments } *)
type judgment
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index c70a3f2eb..67d80fa50 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -80,26 +80,31 @@ let global_vars_set_constant_type env = function
(fun t c -> Id.Set.union (global_vars_set env t) c))
ctx ~init:Id.Set.empty
+let check_declared_variables declared inferred =
+ let mk_set l = List.fold_right Id.Set.add (List.map pi1 l) Id.Set.empty in
+ let undeclared_set = Id.Set.diff (mk_set inferred) (mk_set declared) in
+ if not (Id.Set.is_empty undeclared_set) then
+ error ("The following section variables are used but not declared:\n"^
+ (String.concat ", "
+ (List.map Id.to_string (Id.Set.elements undeclared_set))))
+
let build_constant_declaration env (def,typ,cst,inline_code,ctx) =
- let hyps =
+ let hyps =
let inferred =
let ids_typ = global_vars_set_constant_type env typ in
let ids_def = match def with
- | Undef _ -> Id.Set.empty
- | Def cs -> global_vars_set env (Lazyconstr.force cs)
- | OpaqueDef lc ->
- global_vars_set env (Lazyconstr.force_opaque lc) in
- keep_hyps env (Id.Set.union ids_typ ids_def) in
- let declared = match ctx with
- | None -> inferred
- | Some declared -> declared in
- let mk_set l = List.fold_right Id.Set.add (List.map pi1 l) Id.Set.empty in
- let inferred_set, declared_set = mk_set inferred, mk_set declared in
- if not (Id.Set.subset inferred_set declared_set) then
- error ("The following section variable are used but not declared:\n"^
- (String.concat ", " (List.map Id.to_string
- (Id.Set.elements (Id.Set.diff inferred_set declared_set)))));
- declared in
+ | Undef _ -> Id.Set.empty
+ | Def cs -> global_vars_set env (Lazyconstr.force cs)
+ | OpaqueDef lc -> global_vars_set env (Lazyconstr.force_opaque lc)
+ in
+ keep_hyps env (Id.Set.union ids_typ ids_def)
+ in
+ match ctx with
+ | None -> inferred
+ | Some declared ->
+ check_declared_variables declared inferred;
+ declared
+ in
let tps = Cemitcodes.from_val (compile_constant_body env def) in
{ const_hyps = hyps;
const_body = def;
diff --git a/library/assumptions.ml b/library/assumptions.ml
index 2d99aca8c..2418f0648 100644
--- a/library/assumptions.ml
+++ b/library/assumptions.ml
@@ -239,7 +239,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st (* t *) =
in
match Declareops.body_of_constant cb with
| None -> do_type (Axiom kn)
- | Some body -> do_constr (Lazyconstr.force body) s acc
+ | Some body -> do_constr body s acc
and do_memoize_kn kn =
try_and_go (Axiom kn) (add_kn kn)
diff --git a/library/library.ml b/library/library.ml
index b7a2f8149..7c34a62d0 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -24,7 +24,7 @@ type compilation_unit_name = DirPath.t
type library_disk = {
md_name : compilation_unit_name;
- md_compiled : Safe_typing.LightenLibrary.lightened_compiled_library;
+ md_compiled : Safe_typing.compiled_library;
md_objects : Declaremods.library_objects;
md_deps : (compilation_unit_name * Digest.t) array;
md_imports : compilation_unit_name array }
@@ -290,42 +290,114 @@ let try_locate_qualified_library (loc,qid) =
| LibNotFound -> error_lib_not_found qid
(************************************************************************)
-(* Internalise libraries *)
+(** {6 Tables of opaque proof terms} *)
-let mk_library md table digest =
- let md_compiled =
- Safe_typing.LightenLibrary.load ~load_proof:!Flags.load_proofs
- table md.md_compiled
- in {
- library_name = md.md_name;
- library_compiled = md_compiled;
- library_objects = md.md_objects;
- library_deps = md.md_deps;
- library_imports = md.md_imports;
- library_digest = digest
- }
+(** We now store opaque proof terms apart from the rest of the environment.
+ See the [Indirect] contructor in [Lazyconstr.lazy_constr]. This way,
+ we can quickly load a first half of a .vo file without these opaque
+ terms, and access them only when a specific command (e.g. Print or
+ Print Assumptions) needs it. *)
+
+exception Faulty
+
+(** Fetching a table of opaque terms at position [pos] in file [f],
+ expecting to find first a copy of [digest]. *)
let fetch_opaque_table (f,pos,digest) =
+ if !Flags.load_proofs == Flags.Dont then
+ error "Not accessing an opaque term due to option -dont-load-proofs.";
try
+ Pp.msg_info (Pp.str "Fetching opaque terms in " ++ str f);
let ch = System.with_magic_number_check raw_intern_library f in
let () = seek_in ch pos in
- if not (String.equal (System.marshal_in f ch) digest) then failwith "File changed!";
- let table = (System.marshal_in f ch : Safe_typing.LightenLibrary.table) in
+ if not (String.equal (System.marshal_in f ch) digest) then raise Faulty;
+ let table = (System.marshal_in f ch : Term.constr array) in
+ (* Verification of the final digest (the one also covering the opaques) *)
+ let pos' = pos_in ch in
+ let digest' = (System.marshal_in f ch : Digest.t) in
let () = close_in ch in
+ let ch' = open_in f in
+ if not (String.equal (Digest.channel ch' pos') digest') then raise Faulty;
+ let () = close_in ch' in
table
with e when Errors.noncritical e ->
error
- ("The file "^f^" is inaccessible or has changed,\n" ^
- "cannot load some opaque constant bodies in it.\n")
+ ("The file "^f^" is inaccessible or corrupted,\n"
+ ^ "cannot load some opaque constant bodies in it.\n")
+
+(** Delayed / available tables of opaque terms *)
+
+type opaque_table_status =
+ | ToFetch of string * int * Digest.t
+ | Fetched of Term.constr array
+
+let opaque_tables = ref (LibraryMap.empty : opaque_table_status LibraryMap.t)
+
+let add_opaque_table dp st =
+ opaque_tables := LibraryMap.add dp st !opaque_tables
+
+let access_opaque_table dp i =
+ let t = match LibraryMap.find dp !opaque_tables with
+ | Fetched t -> t
+ | ToFetch (f,pos,digest) ->
+ let t = fetch_opaque_table (f,pos,digest) in
+ add_opaque_table dp (Fetched t);
+ t
+ in
+ assert (i < Array.length t); t.(i)
+
+(** Table of opaque terms from the library currently being compiled *)
+
+module OpaqueTables = struct
+
+ let a_constr = Term.mkRel 1
+
+ let local_table = ref (Array.make 100 a_constr)
+ let local_index = ref 0
+
+ let get dp i =
+ if DirPath.equal dp (Lib.library_dp ())
+ then (!local_table).(i)
+ else access_opaque_table dp i
+
+ let store c =
+ let n = !local_index in
+ incr local_index;
+ if n = Array.length !local_table then begin
+ let t = Array.make (2*n) a_constr in
+ Array.blit !local_table 0 t 0 n;
+ local_table := t
+ end;
+ (!local_table).(n) <- c;
+ Some (Lib.library_dp (), n)
+
+ let dump () = Array.sub !local_table 0 !local_index
+
+end
+
+let _ = Lazyconstr.set_indirect_opaque_accessor OpaqueTables.get
+
+(************************************************************************)
+(* Internalise libraries *)
+
+let mk_library md digest =
+ {
+ library_name = md.md_name;
+ library_compiled = md.md_compiled;
+ library_objects = md.md_objects;
+ library_deps = md.md_deps;
+ library_imports = md.md_imports;
+ library_digest = digest
+ }
let intern_from_file f =
let ch = System.with_magic_number_check raw_intern_library f in
let lmd = System.marshal_in f ch in
let pos = pos_in ch in
let digest = System.marshal_in f ch in
- let table = lazy (fetch_opaque_table (f,pos,digest)) in
register_library_filename lmd.md_name f;
- let library = mk_library lmd table digest in
+ add_opaque_table lmd.md_name (ToFetch (f,pos,digest));
+ let library = mk_library lmd digest in
close_in ch;
library
@@ -528,6 +600,7 @@ let start_library f =
let id = Id.of_string (Filename.basename f) in
check_coq_overwriting ldir0 id;
let ldir = add_dirpath_suffix ldir0 id in
+ Lazyconstr.set_indirect_opaque_creator OpaqueTables.store;
Declaremods.start_library ldir;
ldir,longf
@@ -546,11 +619,21 @@ let error_recursively_dependent_library dir =
strbrk " to save current library because" ++
strbrk " it already depends on a library of this name.")
+(* We now use two different digests in a .vo file. The first one
+ only covers half of the file, without the opaque table. It is
+ used for identifying this version of this library : this digest
+ is the one leading to "inconsistent assumptions" messages.
+ The other digest comes at the very end, and covers everything
+ before it. This one is used for integrity check of the whole
+ file when loading the opaque table. *)
+
(* Security weakness: file might have been changed on disk between
writing the content and computing the checksum... *)
+
let save_library_to dir f =
+ Lazyconstr.reset_indirect_opaque_creator ();
let cenv, seg, ast = Declaremods.end_library dir in
- let cenv, table = Safe_typing.LightenLibrary.save cenv in
+ let table = OpaqueTables.dump () in
let md = {
md_name = dir;
md_compiled = cenv;
@@ -563,14 +646,12 @@ let save_library_to dir f =
try
System.marshal_out ch md;
flush ch;
- (* The loading of the opaque definitions table is optional whereas
- the digest is loaded all the time. As a consequence, the digest
- must be serialized before the table (if we want to keep the
- current simple layout of .vo files). This also entails that the
- digest does not take opaque terms into account anymore. *)
let di = Digest.file f' in
System.marshal_out ch di;
System.marshal_out ch table;
+ flush ch;
+ let di = Digest.file f' in
+ System.marshal_out ch di;
close_out ch;
if not !Flags.no_native_compiler then begin
let lp = Loadpath.get_load_paths () in
diff --git a/library/states.ml b/library/states.ml
index 9d15dfc6c..eb597670f 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -23,8 +23,6 @@ let (extern_state,intern_state) =
extern_intern Coq_config.state_magic_number in
(fun s ->
let s = ensure_suffix s in
- if !Flags.load_proofs <> Flags.Force then
- Errors.error "Write State only works with option -force-load-proofs";
raw_extern s (freeze())),
(fun s ->
let s = ensure_suffix s in
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index ef4dca26d..74d719438 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -940,8 +940,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
(* observe (str "rec_args_num := " ++ str (string_of_int (rec_args_num + 1) )); *)
let f_def = Global.lookup_constant (destConst f) in
let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in
- let f_body =
- Lazyconstr.force (Option.get (body_of_constant f_def))
+ let f_body = Option.get (body_of_constant f_def)
in
let params,f_body_with_params = decompose_lam_n nb_params f_body in
let (_,num),(_,_,bodies) = destFix f_body_with_params in
@@ -1058,8 +1057,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
in
let get_body const =
match body_of_constant (Global.lookup_constant const) with
- | Some b ->
- let body = Lazyconstr.force b in
+ | Some body ->
Tacred.cbv_norm_flags
(Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
(Global.env ())
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 09637d273..50a4703f6 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -403,8 +403,7 @@ let get_funs_constant mp dp =
function const ->
let find_constant_body const =
match body_of_constant (Global.lookup_constant const) with
- | Some b ->
- let body = Lazyconstr.force b in
+ | Some body ->
let body = Tacred.cbv_norm_flags
(Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
(Global.env ())
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index f0f76860a..609e2916d 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -766,9 +766,8 @@ let make_graph (f_ref:global_reference) =
Dumpglob.pause ();
(match body_of_constant c_body with
| None -> error "Cannot build a graph over an axiom !"
- | Some b ->
+ | Some body ->
let env = Global.env () in
- let body = Lazyconstr.force b in
let extern_body,extern_type =
with_full_print
(fun () ->
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 4d1cefe5a..1e8f4afdf 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -116,7 +116,7 @@ let def_of_const t =
match (Term.kind_of_term t) with
Term.Const sp ->
(try (match Declareops.body_of_constant (Global.lookup_constant sp) with
- | Some c -> Lazyconstr.force c
+ | Some c -> c
| _ -> assert false)
with Not_found -> assert false)
|_ -> assert false
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 597233d01..a8ffd51ef 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -69,7 +69,7 @@ let def_of_const t =
match (kind_of_term t) with
Const sp ->
(try (match body_of_constant (Global.lookup_constant sp) with
- | Some c -> Lazyconstr.force c
+ | Some c -> c
| _ -> raise Not_found)
with Not_found ->
anomaly (str "Cannot find definition of constant " ++
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index a34d4a682..ddc4725c3 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -229,8 +229,7 @@ let mk_constant_obj id bo ty variables hyps =
Acic.Constant (Names.Id.to_string id,None,ty,params)
| Some c ->
Acic.Constant
- (Names.Id.to_string id, Some (Unshare.unshare (Lazyconstr.force c)),
- ty,params)
+ (Names.Id.to_string id, Some (Unshare.unshare c), ty,params)
;;
let mk_inductive_obj sp mib packs variables nparams hyps finite =
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 4d7501ff9..ee6a5e18d 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -400,7 +400,7 @@ let gallina_print_section_variable id =
with_line_skip (print_name_infos (VarRef id))
let print_body = function
- | Some lc -> pr_lconstr (Lazyconstr.force lc)
+ | Some c -> pr_lconstr c
| None -> (str"<no body>")
let print_typed_body (val_0,typ) =
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 386567dee..1f0ccf0fc 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -218,8 +218,7 @@ let parse_args arglist =
| "-batch" :: rem -> set_batch_mode (); parse rem
| "-boot" :: rem -> boot := true; no_load_rc (); parse rem
| "-quality" :: rem -> term_quality := true; no_load_rc (); parse rem
- | "-outputstate" :: s :: rem ->
- Flags.load_proofs := Flags.Force; set_outputstate s; parse rem
+ | "-outputstate" :: s :: rem -> set_outputstate s; parse rem
| "-outputstate" :: [] -> usage ()
| ("-noinit"|"-nois") :: rem -> load_init := false; parse rem
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index e1f17b571..3779815e9 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -41,7 +41,7 @@ let retrieve_first_recthm = function
(pi2 (Global.lookup_named id),variable_opacity id)
| ConstRef cst ->
let cb = Global.lookup_constant cst in
- (Option.map Lazyconstr.force (body_of_constant cb), is_opaque cb)
+ (body_of_constant cb, is_opaque cb)
| _ -> assert false
let adjust_guardness_conditions const = function
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 07:56:31 +0000