Merge universe quantification and delayed constraints in opaque proofs.

This enforces more invariants statically.

1 files changed, 26 insertions, 32 deletions

diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 66c50c4b57..bbc90ef9db 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -22,13 +22,13 @@ type cooking_info = {
 
 type 'a delayed_universes =
 | PrivateMonomorphic of 'a
-| PrivatePolymorphic of Univ.ContextSet.t
+| PrivatePolymorphic of int * Univ.ContextSet.t
 
-type opaque_proofterm = cooking_info list * int * (Constr.t * unit delayed_universes) option
+type opaque_proofterm = cooking_info list * (Constr.t * unit delayed_universes) option
 
 type indirect_accessor = {
   access_proof : DirPath.t -> int -> opaque_proofterm;
-  access_discharge : cooking_info list -> int -> (Constr.t * unit delayed_universes) -> (Constr.t * unit delayed_universes);
+  access_discharge : cooking_info list -> (Constr.t * unit delayed_universes) -> (Constr.t * unit delayed_universes);
 }
 
 let drop_mono = function
@@ -36,13 +36,12 @@ let drop_mono = function
 | 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
+  | Direct of cooking_info list * proofterm
 type opaquetab = {
-  opaque_val : (int * cooking_info list * proofterm) Int.Map.t;
+  opaque_val : (cooking_info list * proofterm) Int.Map.t;
   (** Actual proof terms *)
   opaque_len : int;
   (** Size of the above map *)
@@ -57,14 +56,14 @@ let empty_opaquetab = {
 let not_here () =
   CErrors.user_err Pp.(str "Cannot access opaque delayed proof")
 
-let create ~univs cu = Direct (univs, [],cu)
+let create cu = Direct ([],cu)
 
 let turn_indirect dp o tab = match o with
   | Indirect (_,_,i) ->
       if not (Int.Map.mem i tab.opaque_val)
       then CErrors.anomaly (Pp.str "Indirect in a different table.")
       else CErrors.anomaly (Pp.str "Already an indirect opaque.")
-  | Direct (nunivs, d, cu) ->
+  | Direct (d, cu) ->
     (* Invariant: direct opaques only exist inside sections, we turn them
       indirect as soon as we are at toplevel. At this moment, we perform
       hashconsing of their contents, potentially as a future. *)
@@ -72,13 +71,13 @@ let turn_indirect dp o tab = match o with
         let c = Constr.hcons c in
         let u = match u with
         | PrivateMonomorphic u -> PrivateMonomorphic (Univ.hcons_universe_context_set u)
-        | PrivatePolymorphic u -> PrivatePolymorphic (Univ.hcons_universe_context_set u)
+        | PrivatePolymorphic (n, u) -> PrivatePolymorphic (n, Univ.hcons_universe_context_set u)
         in
         (c, u)
       in
       let cu = Future.chain cu hcons in
       let id = tab.opaque_len in
-      let opaque_val = Int.Map.add id (nunivs, d,cu) tab.opaque_val in
+      let opaque_val = Int.Map.add id (d,cu) tab.opaque_val in
       let opaque_dir =
         if DirPath.equal dp tab.opaque_dir then tab.opaque_dir
         else if DirPath.equal tab.opaque_dir DirPath.initial then dp
@@ -93,8 +92,8 @@ let subst_opaque sub = function
 
 let discharge_direct_opaque ci = function
   | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
-  | Direct (n, d, cu) ->
-      Direct (n, ci :: d, cu)
+  | Direct (d, cu) ->
+      Direct (ci :: d, cu)
 
 let join except cu = match except with
 | None -> ignore (Future.join cu)
@@ -103,28 +102,28 @@ let join except cu = match except with
   else ignore (Future.join cu)
 
 let join_opaque ?except { opaque_val = prfs; opaque_dir = odp; _ } = function
-  | Direct (_,_,cu) -> join except cu
+  | Direct (_,cu) -> join except cu
   | Indirect (_,dp,i) ->
       if DirPath.equal dp odp then
-        let (_, _, fp) = Int.Map.find i prfs in
+        let (_, fp) = Int.Map.find i prfs in
         join except fp
 
 let force_proof access { opaque_val = prfs; opaque_dir = odp; _ } = function
-  | Direct (n, d, cu) ->
+  | Direct (d, cu) ->
     let (c, u) = Future.force cu in
-    access.access_discharge d n (c, drop_mono u)
+    access.access_discharge d (c, drop_mono u)
   | Indirect (l,dp,i) ->
       let c, u =
         if DirPath.equal dp odp
         then
-          let (n, d, cu) = Int.Map.find i prfs in
+          let (d, cu) = Int.Map.find i prfs in
           let (c, u) = Future.force cu in
-          access.access_discharge d n (c, drop_mono u)
+          access.access_discharge d (c, drop_mono u)
         else
-          let (n, d, cu) = access.access_proof dp i in
+          let (d, cu) = access.access_proof dp i in
           match cu with
           | None -> not_here ()
-          | Some (c, u) -> access.access_discharge n d (c, u)
+          | Some (c, u) -> access.access_discharge d (c, u)
       in
       let c = force_constr (List.fold_right subst_substituted l (from_val c)) in
       (c, u)
@@ -134,44 +133,39 @@ let get_mono (_, u) = match u with
 | PrivatePolymorphic _ -> Univ.ContextSet.empty
 
 let force_constraints _access { opaque_val = prfs; opaque_dir = odp; _ } = function
-  | Direct (_,_,cu) ->
+  | Direct (_,cu) ->
     get_mono (Future.force cu)
   | Indirect (_,dp,i) ->
       if DirPath.equal dp odp
       then
-        let (_, _, cu) = Int.Map.find i prfs in
+        let ( _, cu) = Int.Map.find i prfs in
         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) ->
+| Direct (_, cu) ->
   Future.chain cu get_mono
 
 module FMap = Future.UUIDMap
 
 let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _ } =
-  let opaque_table = Array.make n ([], 0, None) in
+  let opaque_table = Array.make n ([], None) in
   let f2t_map = ref FMap.empty in
-  let iter n (univs, d, cu) =
+  let iter n (d, cu) =
     let uid = Future.uuid cu in
     let () = f2t_map := FMap.add (Future.uuid cu) n !f2t_map in
     let c =
       if Future.is_val cu then
         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
+        let priv = drop_mono priv in
         Some (c, priv)
       else if Future.UUIDSet.mem uid except then None
       else
         CErrors.anomaly
           Pp.(str"Proof object "++int n++str" is not checked nor to be checked")
     in
-    opaque_table.(n) <- (d, univs, c)
+    opaque_table.(n) <- (d, c)
   in
   let () = Int.Map.iter iter otab in
   opaque_table, !f2t_map