[proof] Split delayed and regular proof closing functions, part I

We split the `close_proof` into two variants, one for delayed proof,
and one for the regular proof closing path, _à la_ interactive.

This makes sense as the typing in both cases is different, even if we
still haven't changed it.

We strongly enforce the invariant (for now) that universe polymorphic
proofs cannot be delayed using this API, as the STM expects.

It introduces some minimal, non-interesting code duplication, which
will go away in the next commits.

1 files changed, 96 insertions, 65 deletions

diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml
index 620afbaf23..b97acdafa6 100644
--- a/tactics/proof_global.ml
+++ b/tactics/proof_global.ml
@@ -141,7 +141,7 @@ let private_poly_univs =
   in
   fun () -> !b
 
-let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
+let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id
                 (fpl : closed_proof_output Future.computation) ps =
   let { section_vars; proof; udecl; initial_euctx } = ps in
   let Proof.{ name; poly; entry } = Proof.data proof in
@@ -150,7 +150,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
     UState.constrain_variables (fst (UState.context_set initial_euctx)) ctx
   in
   let fpl, univs = Future.split2 fpl in
-  let uctx = if poly || now then Future.force univs else initial_euctx in
+  let uctx = Future.force univs in
   (* Because of dependent subgoals at the beginning of proofs, we could
      have existential variables in the initial types of goals, we need to
      normalise them for the kernel. *)
@@ -160,69 +160,100 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
   let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar
     (UState.subst uctx) in
 
-  let make_body =
-    if poly || now then
-      let make_body t (c, eff) =
-        let body = c in
-        let allow_deferred =
-          not poly && (keep_body_ucst_separate ||
-          not (Safe_typing.empty_private_constants = eff.Evd.seff_private))
-        in
-        let typ = if allow_deferred then t else nf t in
-        let used_univs_body = Vars.universes_of_constr body in
-        let used_univs_typ = Vars.universes_of_constr typ in
-        if allow_deferred then
-          let initunivs = UState.univ_entry ~poly initial_euctx in
-          let ctx = constrain_variables uctx in
-          (* For vi2vo compilation proofs are computed now but we need to
-             complement the univ constraints of the typ with the ones of
-             the body.  So we keep the two sets distinct. *)
-          let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
-          let ctx_body = UState.restrict ctx used_univs in
-          let univs = UState.check_mono_univ_decl ctx_body udecl in
-          (initunivs, typ), ((body, univs), eff)
-        else if poly && opaque && private_poly_univs () then
-          let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
-          let universes = UState.restrict uctx used_univs in
-          let typus = UState.restrict universes used_univs_typ in
-          let udecl = UState.check_univ_decl ~poly typus udecl in
-          let ubody = Univ.ContextSet.diff
-              (UState.context_set universes)
-              (UState.context_set typus)
-          in
-          (udecl, typ), ((body, ubody), eff)
-        else
-          (* Since the proof is computed now, we can simply have 1 set of
-             constraints in which we merge the ones for the body and the ones
-             for the typ. We recheck the declaration after restricting with
-             the actually used universes.
-             TODO: check if restrict is really necessary now. *)
-          let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
-          let ctx = UState.restrict uctx used_univs in
-          let univs = UState.check_univ_decl ~poly ctx udecl in
-          (univs, typ), ((body, Univ.ContextSet.empty), eff)
+  let make_body t (c, eff) =
+    let body = c in
+    let allow_deferred =
+      not poly && (keep_body_ucst_separate ||
+                   not (Safe_typing.empty_private_constants = eff.Evd.seff_private))
+    in
+    let typ = if allow_deferred then t else nf t in
+    let used_univs_body = Vars.universes_of_constr body in
+    let used_univs_typ = Vars.universes_of_constr typ in
+    if allow_deferred then
+      let initunivs = UState.univ_entry ~poly initial_euctx in
+      let ctx = constrain_variables uctx in
+      (* For vi2vo compilation proofs are computed now but we need to
+         complement the univ constraints of the typ with the ones of
+         the body.  So we keep the two sets distinct. *)
+      let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
+      let ctx_body = UState.restrict ctx used_univs in
+      let univs = UState.check_mono_univ_decl ctx_body udecl in
+      (initunivs, typ), ((body, univs), eff)
+    else if poly && opaque && private_poly_univs () then
+      let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
+      let universes = UState.restrict uctx used_univs in
+      let typus = UState.restrict universes used_univs_typ in
+      let udecl = UState.check_univ_decl ~poly typus udecl in
+      let ubody = Univ.ContextSet.diff
+          (UState.context_set universes)
+          (UState.context_set typus)
       in
-       fun t p -> Future.split2 (Future.chain p (make_body t))
+      (udecl, typ), ((body, ubody), eff)
     else
-      fun t p ->
-        (* Already checked the univ_decl for the type universes when starting the proof. *)
-        let univctx = UState.univ_entry ~poly:false uctx in
-        let t = nf t in
-        Future.from_val (univctx, t),
-        Future.chain p (fun (pt,eff) ->
-          (* Deferred proof, we already checked the universe declaration with
-             the initial universes, ensure that the final universes respect
-             the declaration as well. If the declaration is non-extensible,
-             this will prevent the body from adding universes and constraints. *)
-          let univs = Future.force univs in
-          let univs = constrain_variables univs in
-          let used_univs = Univ.LSet.union
-              (Vars.universes_of_constr t)
-              (Vars.universes_of_constr pt)
-          in
-          let univs = UState.restrict univs used_univs in
-          let univs = UState.check_mono_univ_decl univs udecl in
-          (pt,univs),eff)
+      (* Since the proof is computed now, we can simply have 1 set of
+         constraints in which we merge the ones for the body and the ones
+         for the typ. We recheck the declaration after restricting with
+         the actually used universes.
+         TODO: check if restrict is really necessary now. *)
+      let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
+      let ctx = UState.restrict uctx used_univs in
+      let univs = UState.check_univ_decl ~poly ctx udecl in
+      (univs, typ), ((body, Univ.ContextSet.empty), eff)
+  in
+  let make_body t p = Future.split2 (Future.chain p (make_body t)) in
+  let entry_fn p (_, t) =
+    let t = EConstr.Unsafe.to_constr t in
+    let univstyp, body = make_body t p in
+    let univs, typ = Future.force univstyp in
+    Declare.delayed_definition_entry ~opaque ?feedback_id ?section_vars ~univs ~types:typ body
+  in
+  let entries = Future.map2 entry_fn fpl (Proofview.initial_goals entry) in
+  { name; entries; uctx; udecl }
+
+let close_proof_delayed ~opaque ~keep_body_ucst_separate ?feedback_id
+                (fpl : closed_proof_output Future.computation) ps =
+  let { section_vars; proof; udecl; initial_euctx } = ps in
+  let Proof.{ name; poly; entry } = Proof.data proof in
+
+  (* We don't allow poly = true in this path *)
+  if poly then
+    CErrors.anomaly (Pp.str "Cannot delay universe-polymorphic constants.");
+
+  let opaque = match opaque with Opaque -> true | Transparent -> false in
+  let constrain_variables ctx =
+    UState.constrain_variables (fst (UState.context_set initial_euctx)) ctx
+  in
+  let fpl, univs = Future.split2 fpl in
+  let uctx = initial_euctx in
+  (* Because of dependent subgoals at the beginning of proofs, we could
+     have existential variables in the initial types of goals, we need to
+     normalise them for the kernel. *)
+  let subst_evar k =
+    let { Proof.sigma } = Proof.data proof in
+    Evd.existential_opt_value0 sigma k in
+
+  let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar
+    (UState.subst uctx) in
+
+  let make_body t p =
+    (* Already checked the univ_decl for the type universes when starting the proof. *)
+    let univctx = UState.univ_entry ~poly:false uctx in
+    let t = nf t in
+    Future.from_val (univctx, t),
+    Future.chain p (fun (pt,eff) ->
+        (* Deferred proof, we already checked the universe declaration with
+           the initial universes, ensure that the final universes respect
+           the declaration as well. If the declaration is non-extensible,
+           this will prevent the body from adding universes and constraints. *)
+        let univs = Future.force univs in
+        let univs = constrain_variables univs in
+        let used_univs = Univ.LSet.union
+            (Vars.universes_of_constr t)
+            (Vars.universes_of_constr pt)
+        in
+        let univs = UState.restrict univs used_univs in
+        let univs = UState.check_mono_univ_decl univs udecl in
+        (pt,univs),eff)
   in
   let entry_fn p (_, t) =
     let t = EConstr.Unsafe.to_constr t in
@@ -271,10 +302,10 @@ let return_proof ?(allow_partial=false) ps =
     proofs, Evd.evar_universe_context evd
 
 let close_future_proof ~opaque ~feedback_id ps proof =
-  close_proof ~opaque ~keep_body_ucst_separate:true ~feedback_id ~now:false proof ps
+  close_proof_delayed ~opaque ~keep_body_ucst_separate:true ~feedback_id proof ps
 
 let close_proof ~opaque ~keep_body_ucst_separate fix_exn ps =
-  close_proof ~opaque ~keep_body_ucst_separate ~now:true
+  close_proof ~opaque ~keep_body_ucst_separate
     (Future.from_val ~fix_exn (return_proof ps)) ps
 
 let update_global_env =