Merge universe quantification and delayed constraints in opaque proofs.

This enforces more invariants statically.

11 files changed, 70 insertions, 76 deletions

diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 7e49e741ad..9b41fbcb7a 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -10,7 +10,7 @@ open Environ
 
 let indirect_accessor = ref {
   Opaqueproof.access_proof = (fun _ _ -> assert false);
-  Opaqueproof.access_discharge = (fun _ _ _ -> assert false);
+  Opaqueproof.access_discharge = (fun _ _ -> assert false);
 }
 
 let set_indirect_accessor f = indirect_accessor := f
@@ -39,7 +39,7 @@ let check_constant_declaration env kn cb =
     let c, u = Opaqueproof.force_proof !indirect_accessor otab o in
     let env' = match u, cb.const_universes with
     | Opaqueproof.PrivateMonomorphic (), Monomorphic _ -> env'
-    | Opaqueproof.PrivatePolymorphic local, Polymorphic _ ->
+    | Opaqueproof.PrivatePolymorphic (_, local), Polymorphic _ ->
       push_subgraph local env'
     | _ -> assert false
     in
diff --git a/checker/values.ml b/checker/values.ml
index 7b869cd130..9f1baa4d37 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -399,8 +399,8 @@ let v_cooking_info =
   Tuple ("cooking_info", [|v_work_list; v_abstract|])
 
 let v_delayed_universes =
-  Sum ("delayed_universes", 0, [| [| v_unit |]; [| v_context_set |] |])
+  Sum ("delayed_universes", 0, [| [| v_unit |]; [| Int; v_context_set |] |])
 
-let v_opaques = Array (Tuple ("opaque", [| List v_cooking_info; Int; Opt (v_pair v_constr v_delayed_universes) |]))
+let v_opaques = Array (Tuple ("opaque", [| List v_cooking_info; Opt (v_pair v_constr v_delayed_universes) |]))
 let v_univopaques =
   Opt (Tuple ("univopaques",[|v_context_set;v_bool|]))
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index fbc0822570..4e1917eb1d 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -201,29 +201,30 @@ let lift_univs cb subst auctx0 =
     let subst, auctx = discharge_abstract_universe_context subst auctx0 auctx in
     subst, (Polymorphic auctx)
 
-let cook_constr { Opaqueproof.modlist ; abstract } (univs, (c, priv)) =
+let cook_constr { Opaqueproof.modlist ; abstract } (c, priv) =
   let cache = RefTable.create 13 in
   let abstract, usubst, abs_ctx = abstract in
-  let ainst = Instance.of_array (Array.init univs Level.var) in
-  let usubst = Instance.append usubst ainst in
-  let expmod = expmod_constr_subst cache modlist usubst in
-  let hyps = Context.Named.map expmod abstract in
-  let hyps = abstract_context hyps in
-  let c = abstract_constant_body (expmod c) hyps in
-  let priv = match priv with
+  let usubst, priv = match priv with
   | Opaqueproof.PrivateMonomorphic () ->
     let () = assert (AUContext.is_empty abs_ctx) in
-    priv
-  | Opaqueproof.PrivatePolymorphic ctx ->
+    let () = assert (Instance.is_empty usubst) in
+    usubst, priv
+  | Opaqueproof.PrivatePolymorphic (univs, ctx) ->
+    let ainst = Instance.of_array (Array.init univs Level.var) in
+    let usubst = Instance.append usubst ainst in
     let ctx = on_snd (Univ.subst_univs_level_constraints (Univ.make_instance_subst usubst)) ctx in
-    Opaqueproof.PrivatePolymorphic ctx
+    let univs = univs + AUContext.size abs_ctx in
+    usubst, Opaqueproof.PrivatePolymorphic (univs, ctx)
   in
-  univs + AUContext.size abs_ctx, (c, priv)
+  let expmod = expmod_constr_subst cache modlist usubst in
+  let hyps = Context.Named.map expmod abstract in
+  let hyps = abstract_context hyps in
+  let c = abstract_constant_body (expmod c) hyps in
+  (c, priv)
 
-let cook_constr infos univs c =
-  let fold info (univs, c) = cook_constr info (univs, c) in
-  let (_, c) = List.fold_right fold infos (univs, c) in
-  c
+let cook_constr infos c =
+  let fold info c = cook_constr info c in
+  List.fold_right fold infos c
 
 let cook_constant { from = cb; info } =
   let { Opaqueproof.modlist; abstract } = info in
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index c98fb0bc3a..b22eff7c32 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -27,7 +27,7 @@ type 'opaque result = {
 }
 
 val cook_constant : recipe -> Opaqueproof.opaque result
-val cook_constr : Opaqueproof.cooking_info list -> int ->
+val cook_constr : Opaqueproof.cooking_info list ->
   (constr * unit Opaqueproof.delayed_universes) -> (constr * unit Opaqueproof.delayed_universes)
 
 val cook_inductive :
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
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 20c862c651..8b844e0812 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -23,7 +23,8 @@ open Mod_subst
 
 type 'a delayed_universes =
 | PrivateMonomorphic of 'a
-| PrivatePolymorphic of Univ.ContextSet.t
+| PrivatePolymorphic of int * Univ.ContextSet.t
+  (** Number of surrounding bound universes + local constraints *)
 
 type proofterm = (constr * Univ.ContextSet.t delayed_universes) Future.computation
 type opaquetab
@@ -32,7 +33,7 @@ type opaque
 val empty_opaquetab : opaquetab
 
 (** From a [proofterm] to some [opaque]. *)
-val create : univs:int -> proofterm -> opaque
+val create : proofterm -> opaque
 
 (** Turn a direct [opaque] into an indirect one. It is your responsibility to
   hashcons the inner term beforehand. The integer is an hint of the maximum id
@@ -46,11 +47,11 @@ type cooking_info = {
   modlist : work_list;
   abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.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 ->
+  access_discharge : cooking_info list ->
     (Constr.t * unit delayed_universes) -> (Constr.t * unit delayed_universes);
 }
 (** When stored indirectly, opaque terms are indexed by their library
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 596fcd210c..7e7734b247 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -728,7 +728,8 @@ let export_side_effects mb env (b_ctx, eff) =
               let map cu =
                 let (c, u) = Future.force cu in
                 let () = match u with
-                | Opaqueproof.PrivateMonomorphic ctx | Opaqueproof.PrivatePolymorphic ctx ->
+                | Opaqueproof.PrivateMonomorphic ctx
+                | Opaqueproof.PrivatePolymorphic (_, ctx) ->
                   assert (Univ.ContextSet.is_empty ctx)
                 in
                 c
@@ -748,11 +749,11 @@ let export_side_effects mb env (b_ctx, eff) =
 let export_private_constants ~in_section ce senv =
   let exported, ce = export_side_effects senv.revstruct senv.env ce in
   let map univs p =
-    let univs, local = match univs with
-    | Monomorphic _ -> 0, Opaqueproof.PrivateMonomorphic Univ.ContextSet.empty
-    | Polymorphic auctx -> Univ.AUContext.size auctx, Opaqueproof.PrivatePolymorphic Univ.ContextSet.empty
+    let local = match univs with
+    | Monomorphic _ -> Opaqueproof.PrivateMonomorphic Univ.ContextSet.empty
+    | Polymorphic auctx -> Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, Univ.ContextSet.empty)
     in
-    Opaqueproof.create ~univs (Future.from_val (p, local))
+    Opaqueproof.create (Future.from_val (p, local))
   in
   let map (kn, cb) = (kn, map_constant (fun c -> map cb.const_universes c) cb) in
   let bodies = List.map map exported in
@@ -781,11 +782,7 @@ let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl sen
         Term_typing.translate_constant Term_typing.Pure senv.env kn ce
     in
   let senv =
-    let univs = match cb.const_universes with
-    | Monomorphic _ -> 0
-    | Polymorphic auctx -> Univ.AUContext.size auctx
-    in
-    let cb = map_constant (fun c -> Opaqueproof.create ~univs c) cb in
+    let cb = map_constant (fun c -> Opaqueproof.create c) cb in
     add_constant_aux ~in_section senv (kn, cb) in
   let senv =
     match decl with
@@ -805,7 +802,7 @@ let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl sen
       match cb.const_universes, delayed with
       | Monomorphic ctx', Opaqueproof.PrivateMonomorphic ctx ->
         OpaqueDef b, Monomorphic (Univ.ContextSet.union ctx ctx')
-      | Polymorphic auctx, Opaqueproof.PrivatePolymorphic ctx ->
+      | Polymorphic auctx, Opaqueproof.PrivatePolymorphic (_, ctx) ->
         (* Upper layers enforce that there are no internal constraints *)
         let () = assert (Univ.ContextSet.is_empty ctx) in
         OpaqueDef b, Polymorphic auctx
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 9ec3269375..6c065292d4 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -181,7 +181,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         let _ = Typeops.judge_of_cast env j DEFAULTcast tj in
         let def = Vars.subst_univs_level_constr usubst j.uj_val in
         let () = feedback_completion_typecheck feedback_id in
-        def, Opaqueproof.PrivatePolymorphic private_univs
+        def, Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, private_univs)
       end in
       let def = OpaqueDef proofterm in
       let typ = Vars.subst_univs_level_constr usubst tj.utj_val in
@@ -402,7 +402,7 @@ let translate_local_def env _id centry =
         the body by virtue of the typing of [Entries.section_def_entry]. *)
     let () = match cst with
     | Opaqueproof.PrivateMonomorphic ctx -> assert (Univ.ContextSet.is_empty ctx)
-    | Opaqueproof.PrivatePolymorphic ctx -> assert (Univ.ContextSet.is_empty ctx)
+    | Opaqueproof.PrivatePolymorphic (_, ctx) -> assert (Univ.ContextSet.is_empty ctx)
     in
     p
   | Undef _ | Primitive _ -> assert false
diff --git a/library/global.ml b/library/global.ml
index 44e4a9b7e1..d28ca0acc1 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -141,7 +141,7 @@ let body_of_constant_body access env cb =
   | Def c ->
     let u = match cb.const_universes with
     | Monomorphic _ -> Opaqueproof.PrivateMonomorphic ()
-    | Polymorphic _ -> Opaqueproof.PrivatePolymorphic Univ.ContextSet.empty
+    | Polymorphic auctx -> Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, Univ.ContextSet.empty)
     in
     Some (Mod_subst.force_constr c, u, Declareops.constant_polymorphic_context cb)
   | OpaqueDef o ->
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 396c954b42..65197edb9d 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -587,7 +587,7 @@ let print_constant with_values sep sp udecl =
     | Some (c, priv, ctx) ->
       let priv = match priv with
       | Opaqueproof.PrivateMonomorphic () -> None
-      | Opaqueproof.PrivatePolymorphic ctx -> Some ctx
+      | Opaqueproof.PrivatePolymorphic (_, ctx) -> Some ctx
       in
 	print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++
 	(if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++
diff --git a/stm/stm.ml b/stm/stm.ml
index bae51d1794..6577309909 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1751,13 +1751,14 @@ end = struct (* {{{ *)
         let () = assert (Univ.AUContext.is_empty ctx) in
         let () = match priv with
         | Opaqueproof.PrivateMonomorphic () -> ()
-        | Opaqueproof.PrivatePolymorphic ctx -> assert (Univ.ContextSet.is_empty ctx)
+        | Opaqueproof.PrivatePolymorphic (univs, uctx) ->
+          let () = assert (Int.equal (Univ.AUContext.size ctx) univs) in
+          assert (Univ.ContextSet.is_empty uctx)
         in
         let pr = Constr.hcons pr in
-        let (ci, univs, dummy) = p.(bucket) in
+        let (ci, dummy) = p.(bucket) in
         let () = assert (Option.is_empty dummy) in
-        let () = assert (Int.equal (Univ.AUContext.size ctx) univs) in
-        p.(bucket) <- ci, univs, Some (pr, priv);
+        p.(bucket) <- ci, Some (pr, priv);
         Univ.ContextSet.union cst uc, false
 
   let check_task name l i =