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).

8 files changed, 45 insertions, 28 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 85324ec442..668ee3705c 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -45,7 +45,8 @@ type library_t = {
   library_compiled : Cic.compiled_library;
   library_opaques : Cic.opaque_table;
   library_deps : Cic.library_deps;
-  library_digest : Digest.t }
+  library_digest : Cic.vodigest;
+  library_extra_univs : Univ.constraints }
 
 module LibraryOrdered =
   struct
@@ -112,11 +113,11 @@ let check_one_lib admit (dir,m) =
   if LibrarySet.mem dir admit then
     (Flags.if_verbose ppnl
       (str "Admitting library: " ++ pr_dirpath dir);
-      Safe_typing.unsafe_import file md dig)
+      Safe_typing.unsafe_import file md m.library_extra_univs dig)
   else
     (Flags.if_verbose ppnl
       (str "Checking library: " ++ pr_dirpath dir);
-      Safe_typing.import file md dig);
+      Safe_typing.import file md m.library_extra_univs dig);
   Flags.if_verbose pp (fnl());
   pp_flush ();
   register_loaded_library m
@@ -290,13 +291,14 @@ let with_magic_number_check f a =
 
 open Cic
 
-let mk_library md f table digest = {
+let mk_library md f table digest cst = {
   library_name = md.md_name;
   library_filename = f;
   library_compiled = md.md_compiled;
   library_opaques = table;
   library_deps = md.md_deps;
-  library_digest = digest }
+  library_digest = digest;
+  library_extra_univs = cst }
 
 let name_clash_message dir mdir f =
   str ("The file " ^ f ^ " contains library") ++ spc () ++
@@ -312,7 +314,7 @@ let intern_from_file (dir, f) =
     try
       let ch = with_magic_number_check raw_intern_library f in
       let (md:Cic.library_disk), _, digest = System.marshal_in_segment f ch in
-      let (opaque_csts:'a option), _, _ = System.marshal_in_segment f ch in
+      let (opaque_csts:'a option), _, udg = System.marshal_in_segment f ch in
       let (discharging:'a option), _, _ = System.marshal_in_segment f ch in
       let (tasks:'a option), _, _ = System.marshal_in_segment f ch in
       let (table:Cic.opaque_table), pos, checksum =
@@ -331,21 +333,30 @@ let intern_from_file (dir, f) =
           (str "The file "++str f++str " contains unfinished tasks");
       if opaque_csts <> None then begin
         pp (str " (was a vi file) ");
-        Validate.validate !Flags.debug Values.v_univopaques opaque_csts
+      Option.iter (fun (_,_,b) -> if not b then
+        errorlabstrm "intern_from_file"
+          (str "The file "++str f++str " is still a .vi"))
+        opaque_csts;
+      Validate.validate !Flags.debug Values.v_univopaques opaque_csts;
       end;
       (* Verification of the unmarshalled values *)
       Validate.validate !Flags.debug Values.v_lib md;
       Validate.validate !Flags.debug Values.v_opaques table;
       Flags.if_verbose ppnl (str" done]"); pp_flush ();
+      let digest =
+        if opaque_csts <> None then Cic.Dvivo (digest,udg)
+        else (Cic.Dvo digest) in
       md,table,opaque_csts,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;
-  Option.iter (fun opaque_csts ->
+  Option.iter (fun (opaque_csts,_,_) ->
     opaque_univ_tables :=
       LibraryMap.add md.md_name opaque_csts !opaque_univ_tables)
     opaque_csts;
-  mk_library md f table digest
+  let extra_cst =
+    Option.default Univ.empty_constraint (Option.map pi2 opaque_csts) in
+  mk_library md f table digest extra_cst
 
 let get_deps (dir, f) =
   try LibraryMap.find dir !depgraph
diff --git a/checker/cic.mli b/checker/cic.mli
index 8e6c5580da..bfea853277 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -362,7 +362,11 @@ type nativecode_symb_array
 
 type compilation_unit_name = DirPath.t
 
-type library_info = compilation_unit_name * Digest.t
+type vodigest =
+  | Dvo of Digest.t              (* The digest of the seg_lib part *)
+  | Dvivo of Digest.t * Digest.t (* The digest of the seg_lib + seg_univ part *)
+
+type library_info = compilation_unit_name * vodigest
 
 type library_deps = library_info array
 
@@ -388,7 +392,8 @@ type library_disk = {
   md_imports : compilation_unit_name array }
 
 type opaque_table = constr Future.computation array
-type univ_table = Univ.constraints Future.computation array option
+type univ_table =
+  (Univ.constraints Future.computation array * Univ.constraints * bool) option
 
 (** A .vo file is currently made of :
 
diff --git a/checker/environ.ml b/checker/environ.ml
index 1485d6bf0e..be6bdec113 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -22,7 +22,7 @@ type env = {
     env_globals       : globals;
     env_rel_context   : rel_context;
     env_stratification : stratification;
-    env_imports : Digest.t MPmap.t }
+    env_imports : Cic.vodigest MPmap.t }
 
 let empty_env = {
   env_globals =
diff --git a/checker/environ.mli b/checker/environ.mli
index a4162d67f2..46b390d0ac 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -17,7 +17,7 @@ type env = {
   env_globals : globals;
   env_rel_context : rel_context;
   env_stratification : stratification;
-  env_imports : Digest.t MPmap.t;
+  env_imports : Cic.vodigest MPmap.t;
 }
 val empty_env : env
 
@@ -26,8 +26,8 @@ val engagement : env -> Cic.engagement option
 val set_engagement : Cic.engagement -> env -> env
 
 (* Digests *)
-val add_digest : env -> DirPath.t -> Digest.t -> env
-val lookup_digest : env -> DirPath.t -> Digest.t
+val add_digest : env -> DirPath.t -> Cic.vodigest -> env
+val lookup_digest : env -> DirPath.t -> Cic.vodigest
 
 (* de Bruijn variables *)
 val rel_context : env -> rel_context
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index ec0014175a..add9935816 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -26,9 +26,6 @@ let refresh_arity ar =
 let check_constant_declaration env kn cb =
   Flags.if_verbose ppnl (str "  checking cst: " ++ prcon kn);
 (*  let env = add_constraints cb.const_constraints env in*)
-  (* Constraints of an opauqe proof are not in the module *)
-  let env =
-    add_constraints (Declarations.force_lazy_constr_univs cb.const_body) env in
   (match cb.const_type with
       NonPolymorphicType ty ->
         let ty, cu = refresh_arity ty in
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 7fcd749f59..0d7364ce6a 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -25,9 +25,10 @@ let set_engagement c =
   genv := set_engagement c !genv
 
 (* full_add_module adds module with universes and constraints *)
-let full_add_module dp mb digest =
+let full_add_module dp mb univs digest =
   let env = !genv in
   let env = add_constraints mb.mod_constraints env in
+  let env = add_constraints univs env in
   let env = Modops.add_module mb env in
   genv := add_digest env dp digest
 
@@ -68,19 +69,20 @@ 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 clib digest =
+let import file clib univs digest =
   let env = !genv in
   check_imports msg_warning clib.comp_name env clib.comp_deps;
   check_engagement env clib.comp_enga;
   let mb = clib.comp_mod in
   Mod_checking.check_module
-    (add_constraints mb.mod_constraints env) mb.mod_mp mb;
+    (add_constraints univs
+      (add_constraints mb.mod_constraints env)) mb.mod_mp mb;
   stamp_library file digest;
-  full_add_module clib.comp_name mb digest
+  full_add_module clib.comp_name mb univs digest
 
 (* When the module is admitted, digests *must* match *)
-let unsafe_import file clib digest =
+let unsafe_import file clib univs digest =
   let env = !genv in
   check_imports (errorlabstrm"unsafe_import") clib.comp_name env clib.comp_deps;
   check_engagement env clib.comp_enga;
-  full_add_module clib.comp_name clib.comp_mod digest
+  full_add_module clib.comp_name clib.comp_mod univs digest
diff --git a/checker/safe_typing.mli b/checker/safe_typing.mli
index 59d95c36d6..e2aad1d935 100644
--- a/checker/safe_typing.mli
+++ b/checker/safe_typing.mli
@@ -15,6 +15,6 @@ val get_env : unit -> env
 
 val set_engagement : engagement -> unit
 val import         :
-  CUnix.physical_path -> compiled_library -> Digest.t -> unit
+  CUnix.physical_path -> compiled_library -> Univ.constraints -> Cic.vodigest -> unit
 val unsafe_import  :
-  CUnix.physical_path -> compiled_library -> Digest.t -> unit
+  CUnix.physical_path -> compiled_library -> Univ.constraints -> Cic.vodigest -> unit
diff --git a/checker/values.ml b/checker/values.ml
index 0a2e53799b..f73f83d168 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -284,7 +284,8 @@ and v_modtype =
 
 (** kernel/safe_typing *)
 
-let v_deps = Array (v_tuple "dep" [|v_dp;String|])
+let v_vodigest = Sum ("module_impl",0, [| [|String|]; [|String;String|] |])
+let v_deps = Array (v_tuple "dep" [|v_dp;v_vodigest|])
 let v_compiled_lib =
   v_tuple "compiled" [|v_dp;v_module;v_deps;Opt v_engagement;Any|]
 
@@ -301,7 +302,8 @@ let v_lib =
   Tuple ("library",[|v_dp;v_compiled_lib;v_libraryobjs;v_deps;Array v_dp|])
 
 let v_opaques = Array (v_computation v_constr)
-let v_univopaques = Opt (Array (v_computation v_cstrs))
+let v_univopaques =
+  Opt (Tuple ("univopaques",[|Array (v_computation v_cstrs);v_cstrs;v_bool|]))
 
 (** Registering dynamic values *)