Allow to delay polymorphic opaque constants.

We had to move the private opaque constraints out of the constant declaration
into the opaque table. The API is not very pretty yet due to a pervasive
confusion between monomorphic global constraints and polymorphic local ones,
but once we get rid of futures in the kernel this should be magically solved.

1 files changed, 46 insertions, 18 deletions

diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index e18b726111..66c50c4b57 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -20,13 +20,24 @@ type cooking_info = {
   modlist : work_list;
   abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t }
 
+type 'a delayed_universes =
+| PrivateMonomorphic of 'a
+| PrivatePolymorphic of Univ.ContextSet.t
+
+type opaque_proofterm = cooking_info list * int * (Constr.t * unit delayed_universes) option
+
 type indirect_accessor = {
-  access_proof : DirPath.t -> int -> constr option;
-  access_discharge : cooking_info list -> int -> constr -> constr;
+  access_proof : DirPath.t -> int -> opaque_proofterm;
+  access_discharge : cooking_info list -> int -> (Constr.t * unit delayed_universes) -> (Constr.t * unit delayed_universes);
 }
 
-type proofterm = (constr * Univ.ContextSet.t) Future.computation
+let drop_mono = function
+| PrivateMonomorphic _ -> PrivateMonomorphic ()
+| PrivatePolymorphic _ as ctx -> ctx
+
+type proofterm = (constr * Univ.ContextSet.t delayed_universes) Future.computation
 type universes = int
+
 type opaque =
   | Indirect of substitution list * DirPath.t * int (* subst, lib, index *)
   | Direct of universes * cooking_info list * proofterm
@@ -59,7 +70,10 @@ let turn_indirect dp o tab = match o with
       hashconsing of their contents, potentially as a future. *)
       let hcons (c, u) =
         let c = Constr.hcons c in
-        let u = Univ.hcons_universe_context_set u in
+        let u = match u with
+        | PrivateMonomorphic u -> PrivateMonomorphic (Univ.hcons_universe_context_set u)
+        | PrivatePolymorphic u -> PrivatePolymorphic (Univ.hcons_universe_context_set u)
+        in
         (c, u)
       in
       let cu = Future.chain cu hcons in
@@ -97,34 +111,42 @@ let join_opaque ?except { opaque_val = prfs; opaque_dir = odp; _ } = function
 
 let force_proof access { opaque_val = prfs; opaque_dir = odp; _ } = function
   | Direct (n, d, cu) ->
-    let (c, _) = Future.force cu in
-    access.access_discharge d n c
+    let (c, u) = Future.force cu in
+    access.access_discharge d n (c, drop_mono u)
   | Indirect (l,dp,i) ->
-      let c =
+      let c, u =
         if DirPath.equal dp odp
         then
           let (n, d, cu) = Int.Map.find i prfs in
-          let (c, _) = Future.force cu in
-          access.access_discharge d n c
-        else match access.access_proof dp i with
-        | None -> not_here ()
-        | Some v -> v
+          let (c, u) = Future.force cu in
+          access.access_discharge d n (c, drop_mono u)
+        else
+          let (n, d, cu) = access.access_proof dp i in
+          match cu with
+          | None -> not_here ()
+          | Some (c, u) -> access.access_discharge n d (c, u)
       in
-      force_constr (List.fold_right subst_substituted l (from_val c))
+      let c = force_constr (List.fold_right subst_substituted l (from_val c)) in
+      (c, u)
+
+let get_mono (_, u) = match u with
+| PrivateMonomorphic ctx -> ctx
+| PrivatePolymorphic _ -> Univ.ContextSet.empty
 
 let force_constraints _access { opaque_val = prfs; opaque_dir = odp; _ } = function
   | Direct (_,_,cu) ->
-    snd(Future.force cu)
+    get_mono (Future.force cu)
   | Indirect (_,dp,i) ->
       if DirPath.equal dp odp
       then
         let (_, _, cu) = Int.Map.find i prfs in
-        snd (Future.force cu)
+        get_mono (Future.force cu)
       else Univ.ContextSet.empty
 
 let get_direct_constraints = function
 | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
-| Direct (_, _, cu) -> Future.chain cu snd
+| Direct (_, _, cu) ->
+  Future.chain cu get_mono
 
 module FMap = Future.UUIDMap
 
@@ -136,8 +158,14 @@ let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _
     let () = f2t_map := FMap.add (Future.uuid cu) n !f2t_map in
     let c =
       if Future.is_val cu then
-        let (c, _) = Future.force cu in
-        Some c
+        let (c, priv) = Future.force cu in
+        let priv = match priv with
+        | PrivateMonomorphic _ ->
+          let () = assert (Int.equal univs 0) in
+          PrivateMonomorphic ()
+        | PrivatePolymorphic _ as priv -> priv
+        in
+        Some (c, priv)
       else if Future.UUIDSet.mem uid except then None
       else
         CErrors.anomaly