vi2vo: universes handling finally fixed

Universes that are computed in the vi2vo step are not part of the
outermost module stocked in the vo file.  They are part of the
Library.seg_univ segment and are hence added to the safe env when
the vo file is loaded.

The seg_univ has been augmented.  It is now:
- an array of universe constraints, one for each constant whose opaque
  body was computed in the vi2vo phase.  This is useful only to print
  the constants (and its associated constraints).
- a union of all the constraints that come from proofs generated in the
  vi2vo phase.  This is morally the missing bits in the toplevel module
  body stocked in the vo file, and is there to ease the loading of
  a .vo file (obtained from a .vi file).
- a boolean, false if the file is incomplete (.vi) and true if it is
  complete (.vo obtained via vi2vo).

6 files changed, 40 insertions, 24 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index c60e008d1..2b917587c 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -849,7 +849,7 @@ type library_values = Nativecode.symbol array
 let library_values =
   Summary.ref (Dirmap.empty : library_values Dirmap.t) ~name:"LIBVALUES"
 
-let register_library dir cenv (objs:library_objects) digest =
+let register_library dir cenv (objs:library_objects) digest univ =
   let mp = MPfile dir in
   let () =
     try
@@ -857,7 +857,7 @@ let register_library dir cenv (objs:library_objects) digest =
       ignore(Global.lookup_module mp);
     with Not_found ->
       (* If not, let's do it now ... *)
-      let mp', values = Global.import cenv digest in
+      let mp', values = Global.import cenv univ digest in
       if not (ModPath.equal mp mp') then
         anomaly (Pp.str "Unexpected disk module name");
       library_values := Dirmap.add dir values !library_values
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 89bcccef3..5ff471e69 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -72,7 +72,8 @@ type library_objects
 
 val register_library :
   library_name ->
-    Safe_typing.compiled_library -> library_objects -> Digest.t -> unit
+  Safe_typing.compiled_library -> library_objects -> Safe_typing.vodigest ->
+  Univ.constraints -> unit
 
 val get_library_symbols_tbl : library_name -> Nativecode.symbol array
 
diff --git a/library/global.ml b/library/global.ml
index 9515ff1a8..f75c8e592 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -129,7 +129,7 @@ let mind_of_delta_kn kn =
 
 let start_library dir = globalize (Safe_typing.start_library dir)
 let export s = Safe_typing.export !Flags.compilation_mode (safe_env ()) s
-let import cenv digest = globalize (Safe_typing.import cenv digest)
+let import c u d = globalize (Safe_typing.import c u d)
 
 
 (** Function to get an environment from the constants part of the global
diff --git a/library/global.mli b/library/global.mli
index 856956a17..e11e1c017 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -85,7 +85,8 @@ val mind_of_delta_kn : kernel_name -> mutual_inductive
 val start_library : DirPath.t -> module_path
 val export : DirPath.t ->
   module_path * Safe_typing.compiled_library * Safe_typing.native_library
-val import : Safe_typing.compiled_library -> Digest.t ->
+val import :
+  Safe_typing.compiled_library -> Univ.constraints -> Safe_typing.vodigest ->
   module_path * Nativecode.symbol array
 
 (** {6 Misc } *)
diff --git a/library/library.ml b/library/library.ml
index a1760cdf1..b75329a22 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -26,7 +26,7 @@ type library_disk = {
   md_name : compilation_unit_name;
   md_compiled : Safe_typing.compiled_library;
   md_objects : Declaremods.library_objects;
-  md_deps : (compilation_unit_name * Digest.t) array;
+  md_deps : (compilation_unit_name * Safe_typing.vodigest) array;
   md_imports : compilation_unit_name array }
 
 (*s Modules loaded in memory contain the following informations. They are
@@ -36,9 +36,11 @@ type library_t = {
   library_name : compilation_unit_name;
   library_compiled : Safe_typing.compiled_library;
   library_objects : Declaremods.library_objects;
-  library_deps : (compilation_unit_name * Digest.t) array;
+  library_deps : (compilation_unit_name * Safe_typing.vodigest) array;
   library_imports : compilation_unit_name array;
-  library_digest : Digest.t }
+  library_digests : Safe_typing.vodigest;
+  library_extra_univs : Univ.constraints;
+}
 
 module LibraryOrdered = DirPath
 module LibraryMap = Map.Make(LibraryOrdered)
@@ -441,32 +443,40 @@ let () =
 (* Internalise libraries *)
 
 type seg_lib = library_disk
-type seg_univ = Univ.constraints Future.computation array
+type seg_univ = (* true = vivo, false = vi *)
+  Univ.constraints Future.computation array * Univ.constraints * bool
 type seg_discharge = Opaqueproof.cooking_info list array
 type seg_proofs = Term.constr Future.computation array
 
-let mk_library md digest =
+let mk_library md digests univs =
   {
     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
+    library_digests  = digests;
+    library_extra_univs = univs;
   }
 
 let intern_from_file f =
   let ch = System.with_magic_number_check raw_intern_library f in
   let (lmd : seg_lib), pos, digest_lmd = System.marshal_in_segment f ch in
-  let (univs : seg_univ option), _, _ = System.marshal_in_segment f ch in
-  Option.iter (fun univs -> add_univ_table lmd.md_name (Fetched univs)) univs;
+  let (univs : seg_univ option), _, digest_u = System.marshal_in_segment f ch in
   let _ = System.skip_in_segment f ch in
   let pos, digest = System.skip_in_segment f ch in
+  close_in ch;
   register_library_filename lmd.md_name f;
   add_opaque_table lmd.md_name (ToFetch (f,pos,digest));
-  let library = mk_library lmd digest_lmd in
-  close_in ch;
-  library
+  let open Safe_typing in
+  match univs with
+  | None -> mk_library lmd (Dvo_or_vi digest_lmd) Univ.empty_constraint
+  | Some (utab,uall,true) ->
+      add_univ_table lmd.md_name (Fetched utab);
+      mk_library lmd (Dvivo (digest_lmd,digest_u)) uall
+  | Some (utab,_,false) ->
+      add_univ_table lmd.md_name (Fetched utab);
+      mk_library lmd (Dvo_or_vi digest_lmd) Univ.empty_constraint
 
 let rec intern_library needed (dir, f) =
   (* Look if in the current logical environment *)
@@ -489,10 +499,10 @@ and intern_library_deps needed dir m =
 
 and intern_mandatory_library caller needed (dir,d) =
   let m,needed = intern_library needed (try_locate_absolute_library dir) in
-  if not (String.equal d m.library_digest) then
-    errorlabstrm "" (strbrk ("Compiled library "^(DirPath.to_string caller)^
-	   ".vo makes inconsistent assumptions over library "
-	   ^(DirPath.to_string dir)));
+  if not (Safe_typing.digest_match ~actual:m.library_digests ~required:d) then
+    errorlabstrm "" (strbrk ("Compiled library "^ DirPath.to_string caller ^
+      ".vo makes inconsistent assumptions over library " ^
+      DirPath.to_string dir));
   needed
 
 let rec_intern_library needed mref =
@@ -553,7 +563,8 @@ let register_library m =
     m.library_name
     m.library_compiled
     m.library_objects
-    m.library_digest;
+    m.library_digests
+    m.library_extra_univs;
   register_loaded_library m
 
 (* Follow the semantics of Anticipate object:
@@ -686,13 +697,14 @@ let load_library_todo f =
   if tasks = None then errorlabstrm "restart" (str"not a .vi file");
   if s2 = None then errorlabstrm "restart" (str"not a .vi file");
   if s3 = None then errorlabstrm "restart" (str"not a .vi file");
+  if pi3 (Option.get s2) then errorlabstrm "restart" (str"not a .vi file");
   longf, s1, Option.get s2, Option.get s3, Option.get tasks, s5
 
 (************************************************************************)
 (*s [save_library dir] ends library [dir] and save it to the disk. *)
 
 let current_deps () =
-  List.map (fun m -> (m.library_name, m.library_digest)) !libraries_loaded_list
+  List.map (fun m -> m.library_name, m.library_digests) !libraries_loaded_list
 
 let current_reexports () =
   List.map (fun m -> m.library_name) !libraries_exports_list
@@ -722,7 +734,8 @@ let save_library_to ?todo dir f =
         f ^ "o", (fun _ -> None), (fun _ -> None), (fun _ -> None)
     | Some d ->
         assert(!Flags.compilation_mode = Flags.BuildVi);
-        f ^ "i", (fun x -> Some (d x)), (fun x -> Some x), (fun x -> Some x) in
+        f ^ "i", (fun x -> Some (d x)),
+          (fun x -> Some (x,Univ.empty_constraint,false)), (fun x -> Some x) in
   Opaqueproof.reset_indirect_creator ();
   (* HACK: end_library resets Lib and then joins the safe env.  To join the
    * env one needs to access the futures stored in the tables.  Standard
diff --git a/library/library.mli b/library/library.mli
index afcce7f6c..16664d880 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -30,7 +30,8 @@ val require_library_from_file :
 
 (** Segments of a library *)
 type seg_lib
-type seg_univ = Univ.constraints Future.computation array
+type seg_univ = (* cst, all_cst, finished? *)
+  Univ.constraints Future.computation array * Univ.constraints * bool
 type seg_discharge = Opaqueproof.cooking_info list array
 type seg_proofs = Term.constr Future.computation array