From c1dab62a4ee116e20c53b442dd91084b47bced9f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 27 May 2019 15:47:46 +0200
Subject: Remove the delayed universe table from object files.

This was virtually dead code. The only place really accessing this data was the
user pretty-printer, but actually the tables were not installed for vanilla vo
files.

In practice, that meant that the only case where an access to this table could
have been triggered would have been to print a term coming from a vio file,
or a vo file generated via vio2vo. In all other cases, the printer would not
have displayed the internal universes. While the latter might be considered
a bug, I am instead convinced that this notion of user-facing internal universes
needs to be handled by another mechanism, the current one making little sense.
The fact it was broken all along without anybody noticing proves my point.
---
 checker/check.ml        | 12 ++++--------
 checker/mod_checking.ml |  1 -
 checker/values.ml       |  2 +-
 kernel/opaqueproof.ml   | 13 ++++---------
 kernel/opaqueproof.mli  |  2 --
 library/library.ml      | 25 ++++++-------------------
 library/library.mli     |  4 ++--
 stm/stm.ml              | 13 ++++++-------
 8 files changed, 23 insertions(+), 49 deletions(-)

diff --git a/checker/check.ml b/checker/check.ml
index 76f40dbac2..c5bc59e72a 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -50,6 +50,7 @@ let pr_path sp =
 
 type compilation_unit_name = DirPath.t
 
+type seg_univ = Univ.ContextSet.t * bool
 type seg_proofs = Constr.constr option array
 
 type library_t = {
@@ -90,7 +91,6 @@ let register_loaded_library m =
 
 (* Map from library names to table of opaque terms *)
 let opaque_tables = ref LibraryMap.empty
-let opaque_univ_tables = ref LibraryMap.empty
 
 let access_opaque_table dp i =
   let t =
@@ -326,7 +326,7 @@ let intern_from_file ~intern_mode (dir, f) =
       let ch = System.with_magic_number_check raw_intern_library f in
       let (sd:summary_disk), _, digest = marshal_in_segment f ch in
       let (md:library_disk), _, digest = marshal_in_segment f ch in
-      let (opaque_csts:'a option), _, udg = marshal_in_segment f ch in
+      let (opaque_csts:seg_univ option), _, udg = marshal_in_segment f ch in
       let (discharging:'a option), _, _ = marshal_in_segment f ch in
       let (tasks:'a option), _, _ = marshal_in_segment f ch in
       let (table:seg_proofs option), pos, checksum =
@@ -345,7 +345,7 @@ let intern_from_file ~intern_mode (dir, f) =
           (str "The file "++str f++str " contains unfinished tasks");
       if opaque_csts <> None then begin
        Flags.if_verbose chk_pp (str " (was a vio file) ");
-      Option.iter (fun (_,_,b) -> if not b then
+      Option.iter (fun (_,b) -> if not b then
         user_err ~hdr:"intern_from_file"
           (str "The file "++str f++str " is still a .vio"))
         opaque_csts;
@@ -363,13 +363,9 @@ let intern_from_file ~intern_mode (dir, f) =
     with e -> Flags.if_verbose chk_pp (str" failed!]" ++ fnl ()); raise e in
   depgraph := LibraryMap.add sd.md_name sd.md_deps !depgraph;
   Option.iter (fun table -> opaque_tables := LibraryMap.add sd.md_name table !opaque_tables) table;
-  Option.iter (fun (opaque_csts,_,_) ->
-    opaque_univ_tables :=
-      LibraryMap.add sd.md_name opaque_csts !opaque_univ_tables)
-    opaque_csts;
   let extra_cst =
     Option.default Univ.ContextSet.empty
-      (Option.map (fun (_,cs,_) -> cs) opaque_csts) in
+      (Option.map (fun (cs,_) -> cs) opaque_csts) in
   mk_library sd md f table digest extra_cst
 
 let get_deps (dir, f) =
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 1cf07e7cc7..1bc5891517 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -13,7 +13,6 @@ let set_indirect_accessor f = get_proof := f
 
 let indirect_accessor = {
   Opaqueproof.access_proof = (fun dp n -> !get_proof dp n);
-  Opaqueproof.access_constraints = (fun _ _ -> assert false);
 }
 
 let check_constant_declaration env kn cb =
diff --git a/checker/values.ml b/checker/values.ml
index 4b651cafb6..2e4b9036d9 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -385,4 +385,4 @@ let v_lib =
 
 let v_opaques = Array (Opt v_constr)
 let v_univopaques =
-  Opt (Tuple ("univopaques",[|Array (Opt v_context_set);v_context_set;v_bool|]))
+  Opt (Tuple ("univopaques",[|v_context_set;v_bool|]))
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 0ff27eb4ea..1971c67c61 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -18,7 +18,6 @@ type work_list = (Instance.t * Id.t array) Cmap.t *
 
 type indirect_accessor = {
   access_proof : DirPath.t -> int -> constr option;
-  access_constraints : DirPath.t -> int -> Univ.ContextSet.t option;
 }
 
 type cooking_info = { 
@@ -107,14 +106,12 @@ let force_proof access { opaque_val = prfs; opaque_dir = odp; _ } = function
       let c = Future.force pt in
       force_constr (List.fold_right subst_substituted l (from_val c))
 
-let force_constraints access { opaque_val = prfs; opaque_dir = odp; _ } = function
+let force_constraints _access { opaque_val = prfs; opaque_dir = odp; _ } = function
   | Direct (_,cu) -> snd(Future.force cu)
   | Indirect (_,dp,i) ->
       if DirPath.equal dp odp
       then snd (Future.force (snd (Int.Map.find i prfs)))
-      else match access.access_constraints dp i with
-        | None -> Univ.ContextSet.empty
-        | Some u -> u
+      else Univ.ContextSet.empty
 
 let get_direct_constraints = function
 | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
@@ -124,15 +121,13 @@ module FMap = Future.UUIDMap
 
 let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _ } =
   let opaque_table = Array.make n None in
-  let univ_table = Array.make n None in
   let disch_table = Array.make n [] in
   let f2t_map = ref FMap.empty in
   let iter n (d, cu) =
     let uid = Future.uuid cu in
     let () = f2t_map := FMap.add (Future.uuid cu) n !f2t_map in
     if Future.is_val cu then
-      let (c, u) = Future.force cu in
-      let () = univ_table.(n) <- Some u in
+      let (c, _) = Future.force cu in
       opaque_table.(n) <- Some c
     else if Future.UUIDSet.mem uid except then
       disch_table.(n) <- d
@@ -141,4 +136,4 @@ let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _
         Pp.(str"Proof object "++int n++str" is not checked nor to be checked")
   in
   let () = Int.Map.iter iter otab in
-  opaque_table, univ_table, disch_table, !f2t_map
+  opaque_table, disch_table, !f2t_map
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 4646206e55..46b0500507 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -37,7 +37,6 @@ val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab
 
 type indirect_accessor = {
   access_proof : DirPath.t -> int -> constr option;
-  access_constraints : DirPath.t -> int -> Univ.ContextSet.t option;
 }
 (** When stored indirectly, opaque terms are indexed by their library
     dirpath and an integer index. The two functions above activate
@@ -70,6 +69,5 @@ val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit
 
 val dump : ?except:Future.UUIDSet.t -> opaquetab ->
   Constr.t option array *
-  Univ.ContextSet.t option array *
   cooking_info list array *
   int Future.UUIDMap.t
diff --git a/library/library.ml b/library/library.ml
index 039124635e..e3b8511af1 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -281,13 +281,9 @@ type 'a table_status =
 
 let opaque_tables =
   ref (LibraryMap.empty : (Constr.constr table_status) LibraryMap.t)
-let univ_tables =
-  ref (LibraryMap.empty : (Univ.ContextSet.t table_status) LibraryMap.t)
 
 let add_opaque_table dp st =
   opaque_tables := LibraryMap.add dp st !opaque_tables
-let add_univ_table dp st =
-  univ_tables := LibraryMap.add dp st !univ_tables
 
 let access_table what tables dp i =
   let t = match LibraryMap.find dp !tables with
@@ -312,15 +308,8 @@ let access_opaque_table dp i =
   let what = "opaque proofs" in
   access_table what opaque_tables dp i
 
-let access_univ_table dp i =
-  try
-    let what = "universe contexts of opaque proofs" in
-    access_table what univ_tables dp i
-  with Not_found -> None
-
 let indirect_accessor = {
   Opaqueproof.access_proof = access_opaque_table;
-  Opaqueproof.access_constraints = access_univ_table;
 }
 
 (************************************************************************)
@@ -329,7 +318,7 @@ let indirect_accessor = {
 type seg_sum = summary_disk
 type seg_lib = library_disk
 type seg_univ = (* true = vivo, false = vi *)
-  Univ.ContextSet.t option array * Univ.ContextSet.t * bool
+  Univ.ContextSet.t * bool
 type seg_discharge = Opaqueproof.cooking_info list array
 type seg_proofs = Constr.constr option array
 
@@ -363,11 +352,9 @@ let intern_from_file f =
   let open Safe_typing in
   match univs with
   | None -> mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty
-  | Some (utab,uall,true) ->
-      add_univ_table lsd.md_name (Fetched utab);
+  | Some (uall,true) ->
       mk_library lsd lmd (Dvivo (digest_lmd,digest_u)) uall
-  | Some (utab,_,false) ->
-      add_univ_table lsd.md_name (Fetched utab);
+  | Some (_,false) ->
       mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty
 
 module DPMap = Map.Make(DirPath)
@@ -547,7 +534,7 @@ let load_library_todo f =
   if tasks = None then user_err ~hdr:"restart" (str"not a .vio file");
   if s2 = None then user_err ~hdr:"restart" (str"not a .vio file");
   if s3 = None then user_err ~hdr:"restart" (str"not a .vio file");
-  if pi3 (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file");
+  if snd (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file");
   s0, s1, Option.get s2, Option.get s3, Option.get tasks, s5
 
 (************************************************************************)
@@ -591,7 +578,7 @@ let save_library_to ?todo ~output_native_objects dir f otab =
         List.fold_left (fun e (r,_) -> Future.UUIDSet.add r.Stateid.uuid e)
           Future.UUIDSet.empty l in
   let cenv, seg, ast = Declaremods.end_library ~output_native_objects ~except dir in
-  let opaque_table, univ_table, disch_table, f2t_map = Opaqueproof.dump ~except otab in
+  let opaque_table, disch_table, f2t_map = Opaqueproof.dump ~except otab in
   let tasks, utab, dtab =
     match todo with
     | None -> None, None, None
@@ -602,7 +589,7 @@ let save_library_to ?todo ~output_native_objects dir f otab =
             with Not_found -> assert b; { r with uuid = -1 }, b)
           tasks in
         Some (tasks,rcbackup),
-        Some (univ_table,Univ.ContextSet.empty,false),
+        Some (Univ.ContextSet.empty,false),
         Some disch_table in
   let sd = {
     md_name = dir;
diff --git a/library/library.mli b/library/library.mli
index 2c0673c3b1..142206e2c5 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -33,8 +33,8 @@ val require_library_from_dirpath
 (** Segments of a library *)
 type seg_sum
 type seg_lib
-type seg_univ = (* cst, all_cst, finished? *)
-  Univ.ContextSet.t option array * Univ.ContextSet.t * bool
+type seg_univ = (* all_cst, finished? *)
+  Univ.ContextSet.t * bool
 type seg_discharge = Opaqueproof.cooking_info list array
 type seg_proofs = Constr.constr option array
 
diff --git a/stm/stm.ml b/stm/stm.ml
index e32b6c9f1c..21f5ece244 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1819,15 +1819,15 @@ end = struct (* {{{ *)
                       str (Printexc.to_string e)));
       if drop then `ERROR_ADMITTED else `ERROR
 
-  let finish_task name (u,cst,_) d p l i =
+  let finish_task name (cst,_) d p l i =
     let { Stateid.uuid = bucket }, drop = List.nth l i in
     let bucket_name =
       if bucket < 0 then (assert drop; ", no bucket")
       else Printf.sprintf ", bucket %d" bucket in
     match check_task_aux bucket_name name l i with
     | `ERROR -> exit 1
-    | `ERROR_ADMITTED -> u, cst, false
-    | `OK_ADMITTED -> u, cst, false
+    | `ERROR_ADMITTED -> cst, false
+    | `OK_ADMITTED -> cst, false
     | `OK (po,_) ->
         let discharge c = List.fold_right Cooking.cook_constr d.(bucket) c in
         let con =
@@ -1846,9 +1846,8 @@ end = struct (* {{{ *)
         let pr = map (Option.get (Global.body_of_constant_body Library.indirect_accessor c)) in
         let pr = discharge pr in
         let pr = Constr.hcons pr in
-        u.(bucket) <- Some uc;
         p.(bucket) <- Some pr;
-        u, Univ.ContextSet.union cst uc, false
+        Univ.ContextSet.union cst uc, false
 
   let check_task name l i =
     match check_task_aux "" name l i with
@@ -2851,8 +2850,8 @@ let finish_tasks name u d p (t,rcbackup as tasks) =
     VCS.restore vcs;
     u in
   try
-    let u, a, _ = List.fold_left finish_task u (info_tasks tasks) in
-    (u,a,true), p
+    let a, _ = List.fold_left finish_task u (info_tasks tasks) in
+    (a,true), p
   with e ->
     let e = CErrors.push e in
     msg_warning (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e);
-- 
cgit v1.2.3