Do not substitute opaque constants when discharging.

Instead we do that on a by-need basis by reusing the section info already
stored in the opaque proof.

5 files changed, 64 insertions, 48 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 620efbafd6..1336e3e8bf 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -202,17 +202,21 @@ 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 } c =
+let cook_constr { Opaqueproof.modlist ; abstract } (univs, c) =
   let cache = RefTable.create 13 in
   let abstract, usubst, abs_ctx = abstract in
-  (* For now the STM only handles deferred computation of monomorphic
-    constants. The API will need to be adapted when it's not the case
-    anymore. *)
-  let () = assert (AUContext.is_empty abs_ctx) 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
-  abstract_constant_body (expmod c) hyps
+  let c = abstract_constant_body (expmod c) hyps in
+  univs + AUContext.size abs_ctx, c
+
+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_constant { from = cb; info } =
   let { Opaqueproof.modlist; abstract } = info in
@@ -227,7 +231,7 @@ let cook_constant { from = cb; info } =
   | Undef _ as x -> x
   | Def cs -> Def (Mod_subst.from_val (map (Mod_subst.force_constr cs)))
   | OpaqueDef o ->
-    OpaqueDef (Opaqueproof.discharge_direct_opaque ~cook_constr:map info o)
+    OpaqueDef (Opaqueproof.discharge_direct_opaque info o)
   | Primitive _ -> CErrors.anomaly (Pp.str "Primitives cannot be cooked")
   in
   let const_hyps =
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index abae3880d7..934b7c6b50 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -28,7 +28,7 @@ type 'opaque result = {
 }
 
 val cook_constant : recipe -> Opaqueproof.opaque result
-val cook_constr : Opaqueproof.cooking_info -> constr -> constr
+val cook_constr : Opaqueproof.cooking_info list -> int -> constr -> constr
 
 val cook_inductive :
   Opaqueproof.cooking_info -> mutual_inductive_body -> Entries.mutual_inductive_entry
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 1971c67c61..ee549dee4f 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -16,19 +16,22 @@ open Mod_subst
 type work_list = (Instance.t * Id.t array) Cmap.t * 
   (Instance.t * Id.t array) Mindmap.t
 
+type cooking_info = {
+  modlist : work_list;
+  abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t }
+
 type indirect_accessor = {
   access_proof : DirPath.t -> int -> constr option;
+  access_discharge : cooking_info list -> int -> constr -> constr;
 }
 
-type cooking_info = { 
-  modlist : work_list; 
-  abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t }
 type proofterm = (constr * Univ.ContextSet.t) Future.computation
+type universes = int
 type opaque =
   | Indirect of substitution list * DirPath.t * int (* subst, lib, index *)
-  | Direct of cooking_info list * proofterm
+  | Direct of universes * cooking_info list * proofterm
 type opaquetab = {
-  opaque_val : (cooking_info list * proofterm) Int.Map.t;
+  opaque_val : (int * cooking_info list * proofterm) Int.Map.t;
   (** Actual proof terms *)
   opaque_len : int;
   (** Size of the above map *)
@@ -43,14 +46,14 @@ let empty_opaquetab = {
 let not_here () =
   CErrors.user_err Pp.(str "Cannot access opaque delayed proof")
 
-let create cu = Direct ([],cu)
+let create ~univs cu = Direct (univs, [],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 (d,cu) ->
+  | Direct (nunivs, 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. *)
@@ -61,7 +64,7 @@ let turn_indirect dp o tab = match o with
       in
       let cu = Future.chain cu hcons in
       let id = tab.opaque_len in
-      let opaque_val = Int.Map.add id (d,cu) tab.opaque_val in
+      let opaque_val = Int.Map.add id (nunivs, 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
@@ -74,10 +77,10 @@ let subst_opaque sub = function
   | Indirect (s,dp,i) -> Indirect (sub::s,dp,i)
   | Direct _ -> CErrors.anomaly (Pp.str "Substituting a Direct opaque.")
 
-let discharge_direct_opaque ~cook_constr ci = function
+let discharge_direct_opaque ci = function
   | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
-  | Direct (d,cu) ->
-      Direct (ci::d,Future.chain cu (fun (c, u) -> cook_constr c, u))
+  | Direct (n, d, cu) ->
+      Direct (n, ci :: d, cu)
 
 let join except cu = match except with
 | None -> ignore (Future.join cu)
@@ -86,36 +89,42 @@ 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 = snd (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 (_,cu) ->
-      fst(Future.force cu)
+  | Direct (n, d, cu) ->
+    let (c, _) = Future.force cu in
+    access.access_discharge d n c
   | Indirect (l,dp,i) ->
-      let pt =
+      let c =
         if DirPath.equal dp odp
-        then Future.chain (snd (Int.Map.find i prfs)) fst
+        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 -> Future.from_val v
+        | Some v -> v
       in
-      let c = Future.force pt in
       force_constr (List.fold_right subst_substituted l (from_val c))
 
 let force_constraints _access { opaque_val = prfs; opaque_dir = odp; _ } = function
-  | Direct (_,cu) -> snd(Future.force cu)
+  | Direct (_,_,cu) ->
+    snd(Future.force cu)
   | Indirect (_,dp,i) ->
       if DirPath.equal dp odp
-      then snd (Future.force (snd (Int.Map.find i prfs)))
+      then
+        let (_, _, cu) = Int.Map.find i prfs in
+        snd (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 snd
 
 module FMap = Future.UUIDMap
 
@@ -123,13 +132,15 @@ let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _
   let opaque_table = Array.make n None in
   let disch_table = Array.make n [] in
   let f2t_map = ref FMap.empty in
-  let iter n (d, cu) =
+  let iter n (univs, 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, _) = Future.force cu in
-      opaque_table.(n) <- Some c
+      opaque_table.(n) <- Some (d, univs, c)
     else if Future.UUIDSet.mem uid except then
+      (* Only monomorphic constraints can be delayed currently *)
+      let () = assert (Int.equal univs 0) in
       disch_table.(n) <- d
     else
       CErrors.anomaly
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 46b0500507..47439a787d 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -28,15 +28,23 @@ type opaque
 val empty_opaquetab : opaquetab
 
 (** From a [proofterm] to some [opaque]. *)
-val create : proofterm -> opaque
+val create : univs:int -> 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
   used so far *)
 val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab
 
+type work_list = (Univ.Instance.t * Id.t array) Cmap.t *
+  (Univ.Instance.t * Id.t array) Mindmap.t
+
+type cooking_info = {
+  modlist : work_list;
+  abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t }
+
 type indirect_accessor = {
   access_proof : DirPath.t -> int -> constr option;
+  access_discharge : cooking_info list -> int -> constr -> constr;
 }
 (** When stored indirectly, opaque terms are indexed by their library
     dirpath and an integer index. The two functions above activate
@@ -51,23 +59,12 @@ val get_direct_constraints : opaque -> Univ.ContextSet.t Future.computation
 
 val subst_opaque : substitution -> opaque -> opaque
 
-type work_list = (Univ.Instance.t * Id.t array) Cmap.t * 
-  (Univ.Instance.t * Id.t array) Mindmap.t
-
-type cooking_info = { 
-  modlist : work_list; 
-  abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t }
-
-(* The type has two caveats:
-   1) cook_constr is defined after
-   2) we have to store the input in the [opaque] in order to be able to
-      discharge it when turning a .vi into a .vo *)
 val discharge_direct_opaque :
-  cook_constr:(constr -> constr) -> cooking_info -> opaque -> opaque
+  cooking_info -> opaque -> opaque
 
 val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit
 
 val dump : ?except:Future.UUIDSet.t -> opaquetab ->
-  Constr.t option array *
+  (cooking_info list * int * Constr.t) option array *
   cooking_info list array *
   int Future.UUIDMap.t
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 9f7466902d..759cbe22ee 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -749,9 +749,13 @@ 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 (Future.from_val p)) cb) in
+  let map (kn, cb, _) = (kn, map_constant (fun p -> Opaqueproof.create ~univs:(n_univs cb) (Future.from_val p)) cb) in
   let bodies = List.map map exported in
   let exported = List.map (fun (kn, _, r) -> (kn, r)) exported in
   let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in
@@ -778,7 +782,7 @@ let add_constant ?role ~in_section l decl senv =
         Term_typing.translate_constant Term_typing.Pure senv.env kn ce
     in
   let senv =
-    let cb = map_constant Opaqueproof.create cb in
+    let cb = map_constant (fun c -> Opaqueproof.create ~univs:(n_univs cb) c) cb in
     add_constant_aux ~in_section senv (kn, cb) in
   let senv =
     match decl with