Merge PR #11916: [proof] Introduce `prepare_proof` to improve normalization workflow.

Reviewed-by: SkySkimmer
Ack-by: gares
Ack-by: ppedrot

4 files changed, 27 insertions, 21 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 181ec4860c..50922ffc52 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -301,6 +301,7 @@ sig
   type t
   val repr : t -> side_effect list
   val empty : t
+  val is_empty : t -> bool
   val add : side_effect -> t -> t
   val concat : t -> t -> t
 end =
@@ -319,6 +320,7 @@ type t = { seff : side_effect list; elts : SeffSet.t }
 
 let repr eff = eff.seff
 let empty = { seff = []; elts = SeffSet.empty }
+let is_empty { seff; elts } = List.is_empty seff && SeffSet.is_empty elts
 let add x es =
   if SeffSet.mem x es.elts then es
   else { seff = x :: es.seff; elts = SeffSet.add x es.elts }
@@ -349,6 +351,7 @@ let push_private_constants env eff =
   List.fold_left add_if_undefined env eff
 
 let empty_private_constants = SideEffects.empty
+let is_empty_private_constants c = SideEffects.is_empty c
 let concat_private = SideEffects.concat
 
 let universes_of_private eff =
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index f8d5d319a9..b42746a882 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -50,6 +50,8 @@ type 'a safe_transformer = safe_environment -> 'a * safe_environment
 type private_constants
 
 val empty_private_constants : private_constants
+val is_empty_private_constants : private_constants -> bool
+
 val concat_private : private_constants -> private_constants -> private_constants
 (** [concat_private e1 e2] adds the constants of [e1] to [e2], i.e. constants in
     [e1] must be more recent than those of [e2]. *)
diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml
index 68de9c7a00..98de0c848b 100644
--- a/tactics/proof_global.ml
+++ b/tactics/proof_global.ml
@@ -136,17 +136,21 @@ let private_poly_univs =
     ~value:true
 
 (* XXX: This is still separate from close_proof below due to drop_pt in the STM *)
-let return_proof { proof } =
-  let Proof.{name=pid;entry} = Proof.data proof in
+(* XXX: Unsafe_typ:true is needed by vio files, see bf0499bc507d5a39c3d5e3bf1f69191339270729 *)
+let prepare_proof ~unsafe_typ { proof } =
+  let Proof.{name=pid;entry;poly} = Proof.data proof in
   let initial_goals = Proofview.initial_goals entry in
   let evd = Proof.return ~pid proof in
   let eff = Evd.eval_side_effects evd in
   let evd = Evd.minimize_universes evd in
-  let proof_opt c =
+  let to_constr_body c =
     match EConstr.to_constr_opt evd c with
     | Some p -> p
     | None -> CErrors.user_err Pp.(str "Some unresolved existential variables remain")
   in
+  let to_constr_typ t =
+    if unsafe_typ then EConstr.Unsafe.to_constr t else to_constr_body t
+  in
   (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
      side-effects... This may explain why one need to uniquize side-effects
      thereafter... *)
@@ -159,31 +163,24 @@ let return_proof { proof } =
      equations and so far there is no code in the CI that will
      actually call those and do a side-effect, TTBOMK *)
   (* EJGA: likely the right solution is to attach side effects to the first constant only? *)
-  let proofs = List.map (fun (c, _) -> (proof_opt c, eff)) initial_goals in
+  let proofs = List.map (fun (body, typ) -> (to_constr_body body, eff), to_constr_typ typ) initial_goals in
   proofs, Evd.evar_universe_context evd
 
 let close_proof ~opaque ~keep_body_ucst_separate ps =
-  let elist, uctx = return_proof ps in
+
   let { section_vars; proof; udecl; initial_euctx } = ps in
-  let { Proof.name; poly; entry; sigma } = Proof.data proof in
+  let { Proof.name; poly } = Proof.data proof in
+  let unsafe_typ = keep_body_ucst_separate && not poly in
+  let elist, uctx = prepare_proof ~unsafe_typ ps in
   let opaque = match opaque with Opaque -> true | Transparent -> false 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 = Evd.existential_opt_value0 sigma k in
-  let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar (UState.subst uctx) in
+  let make_entry ((body, eff), typ) =
 
-  let make_entry (body, eff) (_, typ) =
     let allow_deferred =
-      not poly && (keep_body_ucst_separate ||
-                   not (Safe_typing.empty_private_constants = eff.Evd.seff_private))
+      not poly &&
+      (keep_body_ucst_separate
+       || not (Safe_typing.is_empty_private_constants eff.Evd.seff_private))
     in
-    (* EJGA: Why are we doing things this way? *)
-    let typ = EConstr.Unsafe.to_constr typ in
-    let typ = if allow_deferred then typ else nf typ in
-    (* EJGA: End "Why are we doing things this way?" *)
-
     let used_univs_body = Vars.universes_of_constr body in
     let used_univs_typ = Vars.universes_of_constr typ in
     let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
@@ -218,7 +215,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ps =
     in
     Declare.definition_entry ~opaque ?section_vars ~univs:utyp ~univsbody:ubody ~types:typ ~eff body
   in
-  let entries = CList.map2 make_entry elist (Proofview.initial_goals entry) in
+  let entries = CList.map make_entry elist  in
   { name; entries; uctx }
 
 let close_proof_delayed ~feedback_id ps (fpl : closed_proof_output Future.computation) =
@@ -275,6 +272,10 @@ let return_partial_proof { proof } =
  let proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in
  proofs, Evd.evar_universe_context evd
 
+let return_proof ps =
+  let p, uctx = prepare_proof ~unsafe_typ:false ps in
+  List.map fst p, uctx
+
 let update_global_env =
   map_proof (fun p ->
       let { Proof.sigma } = Proof.data p in
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 1607771598..601e7e060c 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -171,7 +171,7 @@ let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma =
   let ce = definition_entry ?opaque ?inline ?types ~univs body in
   let env = Global.env () in
   let (c,ctx), sideff = Future.force ce.Declare.proof_entry_body in
-  assert(Safe_typing.empty_private_constants = sideff.Evd.seff_private);
+  assert(Safe_typing.is_empty_private_constants sideff.Evd.seff_private);
   assert(Univ.ContextSet.is_empty ctx);
   RetrieveObl.check_evars env sigma;
   let c = EConstr.of_constr c in