From 26169d33b45aae8bf2dfafa2b400a9780c73ea13 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 16 May 2019 22:32:48 +0200
Subject: Remove a last use of opacity-piercing function in Safe_typing.

---
 kernel/opaqueproof.ml  |  4 ++++
 kernel/opaqueproof.mli |  1 +
 kernel/safe_typing.ml  | 31 +++++++++++++++++--------------
 3 files changed, 22 insertions(+), 14 deletions(-)

(limited to 'kernel')

diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 18c1bcc0f8..d168f3cb7e 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -115,6 +115,10 @@ let force_constraints { opaque_val = prfs; opaque_dir = odp; _ } = function
         | None -> Univ.ContextSet.empty
         | Some u -> Future.force u
 
+let get_direct_constraints = function
+| Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
+| Direct (_, cu) -> Future.chain cu snd
+
 let get_constraints { opaque_val = prfs; opaque_dir = odp; _ } = function
   | Direct (_,cu) -> Some(Future.chain cu snd)
   | Indirect (_,dp,i) ->
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 4e8956af06..501779a917 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -39,6 +39,7 @@ val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab
     indirect opaque accessor configured below. *)
 val force_proof : opaquetab -> opaque -> constr
 val force_constraints : opaquetab -> opaque -> Univ.ContextSet.t
+val get_direct_constraints : opaque -> Univ.ContextSet.t Future.computation
 val get_constraints :
   opaquetab -> opaque -> Univ.ContextSet.t Future.computation option
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index a5d8a480ee..873cc2a172 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -458,19 +458,11 @@ let labels_of_mib mib =
   Array.iter visit_mip mib.mind_packets;
   get ()
 
-let globalize_constant_universes env cb =
+let globalize_constant_universes cb =
   match cb.const_universes with
   | Monomorphic cstrs ->
-    Now (false, cstrs) ::
-    (match cb.const_body with
-     | (Undef _ | Def _ | Primitive _) -> []
-     | OpaqueDef lc ->
-       match Opaqueproof.get_constraints (Environ.opaque_tables env) lc with
-       | None -> []
-       | Some fc ->
-            match Future.peek_val fc with
-             | None -> [Later fc]
-             | Some c -> [Now (false, c)])
+    (* Constraints hidden in the opaque body are added by [add_constant_aux] *)
+    [Now (false, cstrs)]
   | Polymorphic _ ->
     [Now (true, Univ.ContextSet.empty)]
       
@@ -480,9 +472,9 @@ let globalize_mind_universes mb =
     [Now (false, ctx)]
   | Polymorphic _ -> [Now (true, Univ.ContextSet.empty)]
 
-let constraints_of_sfb env sfb = 
+let constraints_of_sfb sfb =
   match sfb with
-  | SFBconst cb -> globalize_constant_universes env cb
+  | SFBconst cb -> globalize_constant_universes cb
   | SFBmind mib -> globalize_mind_universes mib
   | SFBmodtype mtb -> [Now (false, mtb.mod_constraints)]
   | SFBmodule mb -> [Now (false, mb.mod_constraints)]
@@ -520,7 +512,8 @@ let add_field ?(is_include=false) ((l,sfb) as field) gn senv =
          separately. *)
       senv
     else
-      let cst = constraints_of_sfb senv.env sfb in
+      (* Delayed constraints from opaque body are added by [add_constant_aux] *)
+      let cst = constraints_of_sfb sfb in
       add_constraints_list cst senv
   in
   let env' = match sfb, gn with
@@ -553,6 +546,15 @@ type exported_private_constant =
 
 let add_constant_aux ~in_section senv (kn, cb) =
   let l = Constant.label kn in
+  let delayed_cst = match cb.const_body with
+  | OpaqueDef o when not (Declareops.constant_is_polymorphic cb) ->
+    let fc = Opaqueproof.get_direct_constraints o in
+    begin match Future.peek_val fc with
+    | None -> [Later fc]
+    | Some c -> [Now (false, c)]
+    end
+  | Undef _ | Def _ | Primitive _ | OpaqueDef _ -> []
+  in
   let cb, otab = match cb.const_body with
     | OpaqueDef lc when not in_section ->
       (* In coqc, opaque constants outside sections will be stored
@@ -565,6 +567,7 @@ let add_constant_aux ~in_section senv (kn, cb) =
   in
   let senv = { senv with env = Environ.set_opaque_tables senv.env otab } in
   let senv' = add_field (l,SFBconst cb) (C kn) senv in
+  let senv' = add_constraints_list delayed_cst senv' in
   let senv'' = match cb.const_body with
     | Undef (Some lev) ->
       update_resolver
-- 
cgit v1.2.3


From ca4b15c2ba733bdff783762bbfc4b53f88014320 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 20 May 2019 11:30:36 +0200
Subject: Remove a useless call to the Future API for opaque proofs in the STM.

We know statically that the check function producing this forces its
argument, so there is no point in chaining futures lazily.
---
 kernel/opaqueproof.ml  | 7 -------
 kernel/opaqueproof.mli | 2 --
 2 files changed, 9 deletions(-)

(limited to 'kernel')

diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index d168f3cb7e..5584b74b36 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -119,13 +119,6 @@ let get_direct_constraints = function
 | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
 | Direct (_, cu) -> Future.chain cu snd
 
-let get_constraints { opaque_val = prfs; opaque_dir = odp; _ } = function
-  | Direct (_,cu) -> Some(Future.chain cu snd)
-  | Indirect (_,dp,i) ->
-      if DirPath.equal dp odp
-      then Some(Future.chain (snd (Int.Map.find i prfs)) snd)
-      else !get_univ dp i
-
 module FMap = Future.UUIDMap
 
 let a_constr = Future.from_val (mkRel 1)
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 501779a917..b84aeaf35a 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -40,8 +40,6 @@ val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab
 val force_proof : opaquetab -> opaque -> constr
 val force_constraints : opaquetab -> opaque -> Univ.ContextSet.t
 val get_direct_constraints : opaque -> Univ.ContextSet.t Future.computation
-val get_constraints :
-  opaquetab -> opaque -> Univ.ContextSet.t Future.computation option
 
 val subst_opaque : substitution -> opaque -> opaque
 
-- 
cgit v1.2.3


From b245a6c46bc3ef70142e8a165f6cde54265b941e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 20 May 2019 11:51:31 +0200
Subject: Statically ensure the content of delayed proofs in vio file.

Before, we would store futures, but it was actually ensured by the
upper layers that they were either evaluated or stored by the STM
somewhere else. We simply replace this type with an option, thus
removing the Future.computation type from vo/vio files.

This also enhances debug printing, as the latter is unable to properly
print futures.
---
 kernel/opaqueproof.ml  | 44 +++++++++++++++++++++++++-------------------
 kernel/opaqueproof.mli | 10 +++++-----
 2 files changed, 30 insertions(+), 24 deletions(-)

(limited to 'kernel')

diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 5584b74b36..9f148ee248 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -43,6 +43,8 @@ let default_get_univ dp _ =
   CErrors.user_err (Pp.pr_sequence Pp.str [
     "Cannot access universe constraints of opaque proofs in library ";
     DirPath.to_string dp])
+let not_here () =
+  CErrors.user_err Pp.(str "Cannot access opaque delayed proof")
 
 let get_opaque = ref default_get_opaque
 let get_univ = ref default_get_univ
@@ -102,7 +104,10 @@ let force_proof { opaque_val = prfs; opaque_dir = odp; _ } = function
       let pt =
         if DirPath.equal dp odp
         then Future.chain (snd (Int.Map.find i prfs)) fst
-        else !get_opaque dp i in
+        else match !get_opaque dp i with
+        | None -> not_here ()
+        | Some v -> Future.from_val v
+      in
       let c = Future.force pt in
       force_constr (List.fold_right subst_substituted l (from_val c))
 
@@ -113,7 +118,7 @@ let force_constraints { opaque_val = prfs; opaque_dir = odp; _ } = function
       then snd (Future.force (snd (Int.Map.find i prfs)))
       else match !get_univ dp i with
         | None -> Univ.ContextSet.empty
-        | Some u -> Future.force u
+        | Some u -> u
 
 let get_direct_constraints = function
 | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
@@ -121,22 +126,23 @@ let get_direct_constraints = function
 
 module FMap = Future.UUIDMap
 
-let a_constr = Future.from_val (mkRel 1)
-let a_univ = Future.from_val Univ.ContextSet.empty
-let a_discharge : cooking_info list = []
-
-let dump { opaque_val = otab; opaque_len = n; _ } =
-  let opaque_table = Array.make n a_constr in
-  let univ_table = Array.make n a_univ in
-  let disch_table = Array.make n a_discharge in
+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
-  Int.Map.iter (fun n (d,cu) ->
-    let c, u = Future.split2 cu in
-    Future.sink u;
-    Future.sink c;
-    opaque_table.(n) <- c;
-    univ_table.(n) <- u;
-    disch_table.(n) <- d;
-    f2t_map := FMap.add (Future.uuid cu) n !f2t_map)
-  otab;
+  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
+      opaque_table.(n) <- Some c
+    else if Future.UUIDSet.mem uid except then
+      disch_table.(n) <- d
+    else
+      CErrors.anomaly
+        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
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index b84aeaf35a..3b61ec71ef 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -59,9 +59,9 @@ val discharge_direct_opaque :
 
 val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit
 
-val dump : opaquetab ->
-  Constr.t Future.computation array *
-  Univ.ContextSet.t Future.computation array *
+val dump : ?except:Future.UUIDSet.t -> opaquetab ->
+  Constr.t option array *
+  Univ.ContextSet.t option array *
   cooking_info list array *
   int Future.UUIDMap.t
 
@@ -73,7 +73,7 @@ val dump : opaquetab ->
 *)
 
 val set_indirect_opaque_accessor :
-  (DirPath.t -> int -> constr Future.computation) -> unit
+  (DirPath.t -> int -> constr option) -> unit
 val set_indirect_univ_accessor :
-  (DirPath.t -> int -> Univ.ContextSet.t Future.computation option) -> unit
+  (DirPath.t -> int -> Univ.ContextSet.t option) -> unit
 
-- 
cgit v1.2.3


From 2fa3dc389a58ca4a390b99995d82e6c089add163 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 21 May 2019 19:00:28 +0200
Subject: Move body_of_constant_body to Global and specialize its uses.

This function is breaking the indirect opaque abstraction, so we move it
outside of the kernel. Unluckily, there is no better place to put it, so
we leave it in Global.

The checker uses it in a fundamental way, so we reimplement it there, but
this will eventually get removed.
---
 kernel/environ.ml  | 10 ----------
 kernel/environ.mli |  6 ------
 2 files changed, 16 deletions(-)

(limited to 'kernel')

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 05f342a82a..c47bde0864 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -483,16 +483,6 @@ let constant_value_and_type env (kn, u) =
   in
   b', subst_instance_constr u cb.const_type, cst
 
-let body_of_constant_body env cb =
-  let otab = opaque_tables env in
-  match cb.const_body with
-  | Undef _ | Primitive _ ->
-     None
-  | Def c ->
-     Some (Mod_subst.force_constr c, Declareops.constant_polymorphic_context cb)
-  | OpaqueDef o ->
-     Some (Opaqueproof.force_proof otab o, Declareops.constant_polymorphic_context cb)
-
 (* These functions should be called under the invariant that [env] 
    already contains the constraints corresponding to the constant 
    application. *)
diff --git a/kernel/environ.mli b/kernel/environ.mli
index f6cd41861e..2abcea148a 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -215,12 +215,6 @@ val constant_value_and_type : env -> Constant.t puniverses ->
     polymorphic *)
 val constant_context : env -> Constant.t -> Univ.AUContext.t
 
-(** Returns the body of the constant if it has any, and the polymorphic context
-    it lives in. For monomorphic constant, the latter is empty, and for
-    polymorphic constants, the term contains De Bruijn universe variables that
-    need to be instantiated. *)
-val body_of_constant_body : env -> Opaqueproof.opaque constant_body -> (Constr.constr * Univ.AUContext.t) option
-
 (* These functions should be called under the invariant that [env] 
    already contains the constraints corresponding to the constant 
    application. *)
-- 
cgit v1.2.3


From d3c931cd8c84d1b7d9d5763e20221d51700f0709 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 21 May 2019 19:22:30 +0200
Subject: Remove the indirect opaque accessor hooks from Opaqueproof.

We simply pass them as arguments, now that they are not called by the
kernel anymore.

The checker definitely needs to access the opaque proofs. In order not to
touch the API at all, I added a hook there, but it could also be provided
as an additional argument, at the cost of changing all the upwards callers.
---
 kernel/opaqueproof.ml  | 27 +++++++++------------------
 kernel/opaqueproof.mli | 28 ++++++++++++----------------
 2 files changed, 21 insertions(+), 34 deletions(-)

(limited to 'kernel')

diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 9f148ee248..75f96da3eb 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -16,6 +16,11 @@ open Mod_subst
 type work_list = (Instance.t * Id.t array) Cmap.t * 
   (Instance.t * Id.t array) Mindmap.t
 
+type indirect_accessor = {
+  access_proof : DirPath.t -> int -> constr option;
+  access_constraints : DirPath.t -> int -> Univ.ContextSet.t option;
+}
+
 type cooking_info = { 
   modlist : work_list; 
   abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t }
@@ -36,23 +41,9 @@ let empty_opaquetab = {
   opaque_dir = DirPath.initial;
 }
 
-(* hooks *)
-let default_get_opaque dp _ =
-  CErrors.user_err Pp.(pr_sequence str ["Cannot access opaque proofs in library"; DirPath.to_string dp])
-let default_get_univ dp _ =
-  CErrors.user_err (Pp.pr_sequence Pp.str [
-    "Cannot access universe constraints of opaque proofs in library ";
-    DirPath.to_string dp])
 let not_here () =
   CErrors.user_err Pp.(str "Cannot access opaque delayed proof")
 
-let get_opaque = ref default_get_opaque
-let get_univ = ref default_get_univ
-
-let set_indirect_opaque_accessor f = (get_opaque := f)
-let set_indirect_univ_accessor f = (get_univ := f)
-(* /hooks *)
-
 let create cu = Direct ([],cu)
 
 let turn_indirect dp o tab = match o with
@@ -97,26 +88,26 @@ let join_opaque ?except { opaque_val = prfs; opaque_dir = odp; _ } = function
         let fp = snd (Int.Map.find i prfs) in
         join except fp
 
-let force_proof { opaque_val = prfs; opaque_dir = odp; _ } = function
+let force_proof access { opaque_val = prfs; opaque_dir = odp; _ } = function
   | Direct (_,cu) ->
       fst(Future.force cu)
   | Indirect (l,dp,i) ->
       let pt =
         if DirPath.equal dp odp
         then Future.chain (snd (Int.Map.find i prfs)) fst
-        else match !get_opaque dp i with
+        else match access.access_proof dp i with
         | None -> not_here ()
         | Some v -> Future.from_val v
       in
       let c = Future.force pt in
       force_constr (List.fold_right subst_substituted l (from_val c))
 
-let force_constraints { 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 !get_univ dp i with
+      else match access.access_constraints dp i with
         | None -> Univ.ContextSet.empty
         | Some u -> u
 
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 3b61ec71ef..4646206e55 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -35,10 +35,19 @@ val create : proofterm -> opaque
   used so far *)
 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
+    this indirect storage, by telling how to retrieve terms.
+*)
+
 (** From a [opaque] back to a [constr]. This might use the
-    indirect opaque accessor configured below. *)
-val force_proof : opaquetab -> opaque -> constr
-val force_constraints : opaquetab -> opaque -> Univ.ContextSet.t
+    indirect opaque accessor given as an argument. *)
+val force_proof : indirect_accessor -> opaquetab -> opaque -> constr
+val force_constraints : indirect_accessor -> opaquetab -> opaque -> Univ.ContextSet.t
 val get_direct_constraints : opaque -> Univ.ContextSet.t Future.computation
 
 val subst_opaque : substitution -> opaque -> opaque
@@ -64,16 +73,3 @@ val dump : ?except:Future.UUIDSet.t -> opaquetab ->
   Univ.ContextSet.t option array *
   cooking_info list array *
   int Future.UUIDMap.t
-
-(** 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_accessor :
-  (DirPath.t -> int -> constr option) -> unit
-val set_indirect_univ_accessor :
-  (DirPath.t -> int -> Univ.ContextSet.t option) -> unit
-
-- 
cgit v1.2.3