From 5316d205993bb3fe3f69e8984fe53d4d50aa8d2a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 4 Jun 2019 13:44:05 +0200
Subject: 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.
---
 kernel/cooking.ml      | 18 +++++++-------
 kernel/cooking.mli     |  4 ++--
 kernel/declarations.ml |  1 -
 kernel/declareops.ml   |  6 -----
 kernel/modops.ml       |  1 -
 kernel/opaqueproof.ml  | 64 ++++++++++++++++++++++++++++++++++++--------------
 kernel/opaqueproof.mli | 17 ++++++++++----
 kernel/safe_typing.ml  | 38 ++++++++++++++++++++----------
 kernel/term_typing.ml  | 40 ++++++++++++++-----------------
 9 files changed, 113 insertions(+), 76 deletions(-)

(limited to 'kernel')

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 1336e3e8bf..fbc0822570 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -159,7 +159,6 @@ type 'opaque result = {
   cook_body : (constr Mod_subst.substituted, 'opaque) constant_def;
   cook_type : types;
   cook_universes : universes;
-  cook_private_univs : Univ.ContextSet.t option;
   cook_relevance : Sorts.relevance;
   cook_inline : inline;
   cook_context : Constr.named_context option;
@@ -202,7 +201,7 @@ 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) =
+let cook_constr { Opaqueproof.modlist ; abstract } (univs, (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
@@ -211,7 +210,15 @@ let cook_constr { Opaqueproof.modlist ; abstract } (univs, c) =
   let hyps = Context.Named.map expmod abstract in
   let hyps = abstract_context hyps in
   let c = abstract_constant_body (expmod c) hyps in
-  univs + AUContext.size abs_ctx, c
+  let priv = match priv with
+  | Opaqueproof.PrivateMonomorphic () ->
+    let () = assert (AUContext.is_empty abs_ctx) in
+    priv
+  | Opaqueproof.PrivatePolymorphic ctx ->
+    let ctx = on_snd (Univ.subst_univs_level_constraints (Univ.make_instance_subst usubst)) ctx in
+    Opaqueproof.PrivatePolymorphic ctx
+  in
+  univs + AUContext.size abs_ctx, (c, priv)
 
 let cook_constr infos univs c =
   let fold info (univs, c) = cook_constr info (univs, c) in
@@ -240,15 +247,10 @@ let cook_constant { from = cb; info } =
 		  hyps)
       hyps0 ~init:cb.const_hyps in
   let typ = abstract_constant_type (expmod cb.const_type) hyps in
-  let private_univs = Option.map (on_snd (Univ.subst_univs_level_constraints
-                                            (Univ.make_instance_subst usubst)))
-      cb.const_private_poly_univs
-  in
   {
     cook_body = body;
     cook_type = typ;
     cook_universes = univs;
-    cook_private_univs = private_univs;
     cook_relevance = cb.const_relevance;
     cook_inline = cb.const_inline_code;
     cook_context = Some const_hyps;
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 934b7c6b50..c98fb0bc3a 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -21,14 +21,14 @@ type 'opaque result = {
   cook_body : (constr Mod_subst.substituted, 'opaque) constant_def;
   cook_type : types;
   cook_universes : universes;
-  cook_private_univs : Univ.ContextSet.t option;
   cook_relevance : Sorts.relevance;
   cook_inline : inline;
   cook_context : Constr.named_context option;
 }
 
 val cook_constant : recipe -> Opaqueproof.opaque result
-val cook_constr : Opaqueproof.cooking_info list -> int -> constr -> constr
+val cook_constr : Opaqueproof.cooking_info list -> int ->
+  (constr * unit Opaqueproof.delayed_universes) -> (constr * unit Opaqueproof.delayed_universes)
 
 val cook_inductive :
   Opaqueproof.cooking_info -> mutual_inductive_body -> Entries.mutual_inductive_entry
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 388b4f14bf..deb01589b6 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -94,7 +94,6 @@ type 'opaque constant_body = {
     const_relevance : Sorts.relevance;
     const_body_code : Cemitcodes.to_patch_substituted option;
     const_universes : universes;
-    const_private_poly_univs : Univ.ContextSet.t option;
     const_inline_code : bool;
     const_typing_flags : typing_flags; (** The typing options which
                                            were used for
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index de9a052096..a8ebed2326 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -113,7 +113,6 @@ let subst_const_body sub cb =
         const_body_code =
           Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code;
         const_universes = cb.const_universes;
-        const_private_poly_univs = cb.const_private_poly_univs;
         const_relevance = cb.const_relevance;
         const_inline_code = cb.const_inline_code;
         const_typing_flags = cb.const_typing_flags }
@@ -144,16 +143,11 @@ let hcons_universes cbu =
   | Polymorphic ctx ->
     Polymorphic (Univ.hcons_abstract_universe_context ctx)
 
-let hcons_const_private_univs = function
-  | None -> None
-  | Some univs -> Some (Univ.hcons_universe_context_set univs)
-
 let hcons_const_body cb =
   { cb with
     const_body = hcons_const_def cb.const_body;
     const_type = Constr.hcons cb.const_type;
     const_universes = hcons_universes cb.const_universes;
-    const_private_poly_univs = hcons_const_private_univs cb.const_private_poly_univs;
   }
 
 (** {6 Inductive types } *)
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 472fddb829..fcd88fd543 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -329,7 +329,6 @@ let strengthen_const mp_from l cb resolver =
     let u = Univ.make_abstract_instance (Declareops.constant_polymorphic_context cb) in
       { cb with
         const_body = Def (Mod_subst.from_val (mkConstU (con,u)));
-        const_private_poly_univs = None;
 	const_body_code = Some (Cemitcodes.from_val (Cbytegen.compile_alias con)) }
 
 let rec strengthen_mod mp_from mp_to mb =
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
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 6e275649cd..20c862c651 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -21,7 +21,11 @@ open Mod_subst
     When it is [turn_indirect] the data is relocated to an opaque table
     and the [opaque] is turned into an index. *)
 
-type proofterm = (constr * Univ.ContextSet.t) Future.computation
+type 'a delayed_universes =
+| PrivateMonomorphic of 'a
+| PrivatePolymorphic of Univ.ContextSet.t
+
+type proofterm = (constr * Univ.ContextSet.t delayed_universes) Future.computation
 type opaquetab
 type opaque
 
@@ -42,9 +46,12 @@ 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 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);
 }
 (** When stored indirectly, opaque terms are indexed by their library
     dirpath and an integer index. The two functions above activate
@@ -53,7 +60,7 @@ type indirect_accessor = {
 
 (** From a [opaque] back to a [constr]. This might use the
     indirect opaque accessor given as an argument. *)
-val force_proof : indirect_accessor -> opaquetab -> opaque -> constr
+val force_proof : indirect_accessor -> opaquetab -> opaque -> constr * unit delayed_universes
 val force_constraints : indirect_accessor -> opaquetab -> opaque -> Univ.ContextSet.t
 val get_direct_constraints : opaque -> Univ.ContextSet.t Future.computation
 
@@ -65,5 +72,5 @@ val discharge_direct_opaque :
 val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit
 
 val dump : ?except:Future.UUIDSet.t -> opaquetab ->
-  (cooking_info list * int * Constr.t option) array *
+  opaque_proofterm array *
   int Future.UUIDMap.t
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 0b0f14eee7..596fcd210c 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -725,11 +725,14 @@ let export_side_effects mb env (b_ctx, eff) =
               let kn = eff.seff_constant in
                let ce = constant_entry_of_side_effect eff in
                let cb = Term_typing.translate_constant Term_typing.Pure env kn ce in
-               let map cu =
+              let map cu =
                 let (c, u) = Future.force cu in
-                let () = assert (Univ.ContextSet.is_empty u) in
+                let () = match u with
+                | Opaqueproof.PrivateMonomorphic ctx | Opaqueproof.PrivatePolymorphic ctx ->
+                  assert (Univ.ContextSet.is_empty ctx)
+                in
                 c
-               in
+              in
                let cb = map_constant map cb in
                let eff = { eff with seff_body = cb } in
                (push_seff env eff, export_eff eff)
@@ -742,13 +745,16 @@ let export_side_effects mb env (b_ctx, eff) =
      in
        translate_seff trusted seff [] env
 
-let n_univs cb = match cb.const_universes with
-| Monomorphic _ -> 0
-| Polymorphic auctx -> Univ.AUContext.size auctx
-
 let export_private_constants ~in_section ce senv =
   let exported, ce = export_side_effects senv.revstruct senv.env ce in
-  let map (kn, cb) = (kn, map_constant (fun p -> Opaqueproof.create ~univs:(n_univs cb) (Future.from_val (p, Univ.ContextSet.empty))) cb) 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
+    in
+    Opaqueproof.create ~univs (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
   let exported = List.map (fun (kn, _) -> kn) exported in
   let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in
@@ -775,7 +781,11 @@ 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 cb = map_constant (fun c -> Opaqueproof.create ~univs:(n_univs cb) c) cb in
+    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
     add_constant_aux ~in_section senv (kn, cb) in
   let senv =
     match decl with
@@ -791,14 +801,16 @@ let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl sen
     | (Primitive _ | Undef _) -> assert false
     | Def c -> (Def c, cb.const_universes)
     | OpaqueDef o ->
-      let (b, ctx) = Future.force o in
-      match cb.const_universes with
-      | Monomorphic ctx' ->
+      let (b, delayed) = Future.force o in
+      match cb.const_universes, delayed with
+      | Monomorphic ctx', Opaqueproof.PrivateMonomorphic ctx ->
         OpaqueDef b, Monomorphic (Univ.ContextSet.union ctx ctx')
-      | Polymorphic auctx ->
+      | 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
+      | (Monomorphic _ | Polymorphic _), (Opaqueproof.PrivateMonomorphic _ | Opaqueproof.PrivatePolymorphic _) ->
+        assert false
     in
     let cb = { cb with const_body = body; const_universes = univs } in
     let from_env = CEphemeron.create senv.revstruct in
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index f984088f47..9ec3269375 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -79,7 +79,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         Cooking.cook_body = Undef nl;
         cook_type = t;
         cook_universes = univs;
-        cook_private_univs = None;
         cook_relevance = r;
         cook_inline = false;
         cook_context = ctx;
@@ -108,7 +107,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
       { Cooking.cook_body = cd;
         cook_type = ty;
         cook_universes = Monomorphic uctxt;
-        cook_private_univs = None;
         cook_inline = false;
         cook_context = None;
         cook_relevance = Sorts.Relevant;
@@ -124,7 +122,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
       let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in
       let tyj = Typeops.infer_type env typ in
       let proofterm =
-        Future.chain body (fun ((body,uctx),side_eff) ->
+        Future.chain body begin fun ((body,uctx),side_eff) ->
           (* don't redeclare universes which are declared for the type *)
           let uctx = Univ.ContextSet.diff uctx univs in
           let j, uctx = match trust with
@@ -145,13 +143,13 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
           in
           let c = j.uj_val in
           feedback_completion_typecheck feedback_id;
-          c, uctx) in
+          c, Opaqueproof.PrivateMonomorphic uctx
+      end in
       let def = OpaqueDef proofterm in
       {
         Cooking.cook_body = def;
         cook_type = tyj.utj_val;
         cook_universes = Monomorphic univs;
-        cook_private_univs = None;
         cook_relevance = Sorts.relevance_of_sort tyj.utj_type;
         cook_inline = c.const_entry_inline_code;
         cook_context = c.const_entry_secctx;
@@ -168,8 +166,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
       let tj = Typeops.infer_type env typ in
       let sbst, auctx = Univ.abstract_universes nas uctx in
       let usubst = Univ.make_instance_subst sbst in
-      let (def, private_univs) =
-        let (body, ctx), side_eff = Future.join body in
+      let proofterm = Future.chain body begin fun ((body, ctx), side_eff) ->
         let body, ctx = match trust with
         | Pure -> body, ctx
         | SideEffects handle ->
@@ -183,16 +180,15 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         let j = Typeops.infer env body in
         let _ = Typeops.judge_of_cast env j DEFAULTcast tj in
         let def = Vars.subst_univs_level_constr usubst j.uj_val in
-        def, private_univs
-      in
-      let def = OpaqueDef (Future.from_val (def, Univ.ContextSet.empty)) in
+        let () = feedback_completion_typecheck feedback_id in
+        def, Opaqueproof.PrivatePolymorphic private_univs
+      end in
+      let def = OpaqueDef proofterm in
       let typ = Vars.subst_univs_level_constr usubst tj.utj_val in
-        feedback_completion_typecheck feedback_id;
       {
         Cooking.cook_body = def;
         cook_type = typ;
         cook_universes = Polymorphic auctx;
-        cook_private_univs = Some private_univs;
         cook_relevance = Sorts.relevance_of_sort tj.utj_type;
         cook_inline = c.const_entry_inline_code;
         cook_context = c.const_entry_secctx;
@@ -211,22 +207,22 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         body, ctx
       | SideEffects _ -> assert false
       in
-      let env, usubst, univs, private_univs = match c.const_entry_universes with
+      let env, usubst, univs = match c.const_entry_universes with
       | Monomorphic_entry univs ->
         let ctx = Univ.ContextSet.union univs ctx in
         let env = push_context_set ~strict:true ctx env in
-        env, Univ.empty_level_subst, Monomorphic ctx, None
+        env, Univ.empty_level_subst, Monomorphic ctx
       | Polymorphic_entry (nas, uctx) ->
         (** [ctx] must contain local universes, such that it has no impact
             on the rest of the graph (up to transitivity). *)
         let env = push_context ~strict:false uctx env in
         let sbst, auctx = Univ.abstract_universes nas uctx in
         let sbst = Univ.make_instance_subst sbst in
-        let env, local =
-          if Univ.ContextSet.is_empty ctx then env, None
-          else CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition.")
+        let () =
+          if not (Univ.ContextSet.is_empty ctx) then
+            CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition.")
         in
-        env, sbst, Polymorphic auctx, local
+        env, sbst, Polymorphic auctx
       in
       let j = Typeops.infer env body in
       let typ = match typ with
@@ -244,7 +240,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         Cooking.cook_body = def;
         cook_type = typ;
         cook_universes = univs;
-        cook_private_univs = private_univs;
         cook_relevance = Retypeops.relevance_of_term env j.uj_val;
         cook_inline = c.const_entry_inline_code;
         cook_context = c.const_entry_secctx;
@@ -341,7 +336,6 @@ let build_constant_declaration env result =
     const_type = typ;
     const_body_code = tps;
     const_universes = univs;
-    const_private_poly_univs = result.cook_private_univs;
     const_relevance = result.cook_relevance;
     const_inline_code = result.cook_inline;
     const_typing_flags = Environ.typing_flags env }
@@ -368,7 +362,6 @@ let translate_recipe env _kn r =
     const_type = result.cook_type;
     const_body_code = tps;
     const_universes = univs;
-    const_private_poly_univs = result.cook_private_univs;
     const_relevance = result.cook_relevance;
     const_inline_code = result.cook_inline;
     const_typing_flags = Environ.typing_flags env }
@@ -407,7 +400,10 @@ let translate_local_def env _id centry =
     let (p, cst) = Future.force o in
     (** Let definitions are ensured to have no extra constraints coming from
         the body by virtue of the typing of [Entries.section_def_entry]. *)
-    let () = assert (Univ.ContextSet.is_empty cst) in
+    let () = match cst with
+    | Opaqueproof.PrivateMonomorphic ctx -> assert (Univ.ContextSet.is_empty ctx)
+    | Opaqueproof.PrivatePolymorphic ctx -> assert (Univ.ContextSet.is_empty ctx)
+    in
     p
   | Undef _ | Primitive _ -> assert false
   in
-- 
cgit v1.2.3


From a69bb15b1d76b71628b61bc42eb8d79c098074a8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 10 Jun 2019 12:27:37 +0200
Subject: Merge universe quantification and delayed constraints in opaque
 proofs.

This enforces more invariants statically.
---
 kernel/cooking.ml      | 33 ++++++++++++++--------------
 kernel/cooking.mli     |  2 +-
 kernel/opaqueproof.ml  | 58 ++++++++++++++++++++++----------------------------
 kernel/opaqueproof.mli |  9 ++++----
 kernel/safe_typing.ml  | 19 +++++++----------
 kernel/term_typing.ml  |  4 ++--
 6 files changed, 59 insertions(+), 66 deletions(-)

(limited to 'kernel')

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
-- 
cgit v1.2.3


From 4d63d20796ecffa1b04668f493bbef029e12f63d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 10 Jun 2019 18:16:53 +0200
Subject: Clean up the code adding monomorphic global constraints in
 Safe_typing.

---
 kernel/safe_typing.ml | 43 ++++++++++++++++++++++---------------------
 1 file changed, 22 insertions(+), 21 deletions(-)

(limited to 'kernel')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 7e7734b247..3a179e261e 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -308,23 +308,24 @@ let env_of_safe_env senv = senv.env
 let env_of_senv = env_of_safe_env
 
 type constraints_addition =
-  | Now of bool * Univ.ContextSet.t
+  | Now of Univ.ContextSet.t
   | Later of Univ.ContextSet.t Future.computation
 
+let push_context_set poly cst senv =
+  { senv with
+    env = Environ.push_context_set ~strict:(not poly) cst senv.env;
+    univ = Univ.ContextSet.union cst senv.univ }
+
 let add_constraints cst senv =
   match cst with
   | Later fc -> 
     {senv with future_cst = fc :: senv.future_cst}
-  | Now (poly,cst) ->
-  { senv with
-    env = Environ.push_context_set ~strict:(not poly) cst senv.env;
-    univ = Univ.ContextSet.union cst senv.univ }
+  | Now cst ->
+    push_context_set false cst senv
 
 let add_constraints_list cst senv =
   List.fold_left (fun acc c -> add_constraints c acc) senv cst
 
-let push_context_set poly ctx = add_constraints (Now (poly,ctx))
-
 let is_curmod_library senv =
   match senv.modvariant with LIBRARY -> true | _ -> false
 
@@ -333,7 +334,7 @@ let join_safe_environment ?(except=Future.UUIDSet.empty) e =
   List.fold_left
     (fun e fc ->
        if Future.UUIDSet.mem (Future.uuid fc) except then e
-       else add_constraints (Now (false, Future.join fc)) e)
+       else add_constraints (Now (Future.join fc)) e)
     {e with future_cst = []} e.future_cst
 
 let is_joined_environment e = List.is_empty e.future_cst 
@@ -456,22 +457,22 @@ let globalize_constant_universes cb =
   match cb.const_universes with
   | Monomorphic cstrs ->
     (* Constraints hidden in the opaque body are added by [add_constant_aux] *)
-    [Now (false, cstrs)]
+    [cstrs]
   | Polymorphic _ ->
-    [Now (true, Univ.ContextSet.empty)]
+    []
       
 let globalize_mind_universes mb =
   match mb.mind_universes with
   | Monomorphic ctx ->
-    [Now (false, ctx)]
-  | Polymorphic _ -> [Now (true, Univ.ContextSet.empty)]
+    [ctx]
+  | Polymorphic _ -> []
 
 let constraints_of_sfb sfb =
   match sfb with
   | 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)]
+  | SFBmodtype mtb -> [mtb.mod_constraints]
+  | SFBmodule mb -> [mb.mod_constraints]
 
 let add_retroknowledge pttc senv =
   { senv with
@@ -508,7 +509,7 @@ let add_field ?(is_include=false) ((l,sfb) as field) gn senv =
     else
       (* Delayed constraints from opaque body are added by [add_constant_aux] *)
       let cst = constraints_of_sfb sfb in
-      add_constraints_list cst senv
+      List.fold_left (fun senv cst -> push_context_set false cst senv) senv cst
   in
   let env' = match sfb, gn with
     | SFBconst cb, C con -> Environ.add_constant con cb senv.env
@@ -544,7 +545,7 @@ let add_constant_aux ~in_section senv (kn, cb) =
     let fc = Opaqueproof.get_direct_constraints o in
     begin match Future.peek_val fc with
     | None -> [Later fc]
-    | Some c -> [Now (false, c)]
+    | Some c -> [Now c]
     end
   | Undef _ | Def _ | Primitive _ | OpaqueDef _ -> []
   in
@@ -851,13 +852,13 @@ let add_modtype l params_mte inl senv =
 (** full_add_module adds module with universes and constraints *)
 
 let full_add_module mb senv =
-  let senv = add_constraints (Now (false, mb.mod_constraints)) senv in
+  let senv = add_constraints (Now mb.mod_constraints) senv in
   let dp = ModPath.dp mb.mod_mp in
   let linkinfo = Nativecode.link_info_of_dirpath dp in
   { senv with env = Modops.add_linked_module mb linkinfo senv.env }
 
 let full_add_module_type mp mt senv =
-  let senv = add_constraints (Now (false, mt.mod_constraints)) senv in
+  let senv = add_constraints (Now mt.mod_constraints) senv in
   { senv with env = Modops.add_module_type mp mt senv.env }
 
 (** Insertion of modules *)
@@ -1037,7 +1038,7 @@ let add_include me is_module inl senv =
   let sign,(),resolver,cst =
     translate_mse_incl is_module senv.env mp_sup inl me
   in
-  let senv = add_constraints (Now (false, cst)) senv in
+  let senv = add_constraints (Now cst) senv in
   (* Include Self support  *)
   let rec compute_sign sign mb resolver senv =
     match sign with
@@ -1045,7 +1046,7 @@ let add_include me is_module inl senv =
       let cst_sub = Subtyping.check_subtypes senv.env mb mtb in
       let senv =
 	add_constraints
-	  (Now (false, Univ.ContextSet.add_constraints cst_sub Univ.ContextSet.empty))
+          (Now (Univ.ContextSet.add_constraints cst_sub Univ.ContextSet.empty))
 	  senv in
       let mpsup_delta =
 	Modops.inline_delta_resolver senv.env inl mp_sup mbid mtb mb.mod_delta
@@ -1275,7 +1276,7 @@ let register_inductive ind prim senv =
 
 let add_constraints c =
   add_constraints
-    (Now (false, Univ.ContextSet.add_constraints c Univ.ContextSet.empty))
+    (Now (Univ.ContextSet.add_constraints c Univ.ContextSet.empty))
 
 
 (* NB: The next old comment probably refers to [propagate_loads] above.
-- 
cgit v1.2.3