Merge PR #10215: Refine typing of vernacular commands

Reviewed-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares

3 files changed, 85 insertions, 48 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 7333114eae..66b47a64a7 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -108,7 +108,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
     in
     (p,status)
 
-let by tac = Proof_global.with_current_proof (fun _ -> solve (Goal_select.SelectNth 1) None tac)
+let by tac = Proof_global.with_proof (fun _ -> solve (Goal_select.SelectNth 1) None tac)
 
 (**********************************************************************)
 (* Shortcut to build a term using tactics *)
@@ -121,7 +121,7 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo
   let evd = Evd.from_ctx ctx in
   let terminator = Proof_global.make_terminator (fun _ -> ()) in
   let goals = [ (Global.env_of_context sign , typ) ] in
-  let pf = Proof_global.start_proof ~ontop:None evd id goal_kind goals terminator in
+  let pf = Proof_global.start_proof evd id goal_kind goals terminator in
   try
     let pf, status = by tac pf in
     let open Proof_global in
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 40ae4acc88..b642e8eea7 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -45,7 +45,7 @@ type proof_ending =
 type proof_terminator = proof_ending -> unit
 type closed_proof = proof_object * proof_terminator
 
-type pstate = {
+type t = {
   terminator : proof_terminator CEphemeron.key;
   endline_tactic : Genarg.glob_generic_argument option;
   section_vars : Constr.named_context option;
@@ -56,30 +56,47 @@ type pstate = {
 
 (* The head of [t] is the actual current proof, the other ones are
    to be resumed when the current proof is closed or aborted. *)
-type t = pstate * pstate list
+type stack = t * t list
 
 let pstate_map f (pf, pfl) = (f pf, List.map f pfl)
 
 let make_terminator f = f
 let apply_terminator f = f
 
+let get_current_pstate (ps,_) = ps
+
 (* combinators for the current_proof lists *)
 let push ~ontop a =
   match ontop with
   | None -> a , []
   | Some (l,ls) -> a, (l :: ls)
 
+let maybe_push ~ontop = function
+  | Some pstate -> Some (push ~ontop pstate)
+  | None -> ontop
+
 (*** Proof Global manipulation ***)
 
-let get_all_proof_names (pf : t) =
+let get_all_proof_names (pf : stack) =
   let (pn, pns) = pstate_map Proof.(function pf -> (data pf.proof).name) pf in
   pn :: pns
 
-let give_me_the_proof (ps,_) = ps.proof
-let get_current_proof_name (ps,_) = (Proof.data ps.proof).Proof.name
-let get_current_persistence (ps,_) = ps.strength
+let give_me_the_proof ps = ps.proof
+let get_current_proof_name ps = (Proof.data ps.proof).Proof.name
+let get_current_persistence ps = ps.strength
+
+let with_current_pstate f (ps,psl) =
+  let ps, ret = f ps in
+  (ps, psl), ret
+
+let modify_current_pstate f (ps,psl) =
+  f ps, psl
+
+let modify_proof f ps =
+  let proof = f ps.proof in
+  {ps with proof}
 
-let with_current_proof f (ps, psl) =
+let with_proof f ps =
   let et =
     match ps.endline_tactic with
     | None -> Proofview.tclUNIT ()
@@ -92,16 +109,23 @@ let with_current_proof f (ps, psl) =
   in
   let (newpr,ret) = f et ps.proof in
   let ps = { ps with proof = newpr } in
-  (ps, psl), ret
+  ps, ret
+
+let with_current_proof f (ps,rest) =
+  let ps, ret = with_proof f ps in
+  (ps, rest), ret
 
 let simple_with_current_proof f pf =
   let p, () = with_current_proof (fun t p -> f t p , ()) pf in p
 
-let compact_the_proof pf = simple_with_current_proof (fun _ -> Proof.compact) pf
+let simple_with_proof f ps =
+  let ps, () = with_proof (fun t ps -> f t ps, ()) ps in ps
+
+let compact_the_proof pf = simple_with_proof (fun _ -> Proof.compact) pf
 
 (* Sets the tactic to be used when a tactic line is closed with [...] *)
-let set_endline_tactic tac (ps, psl) =
-  { ps with endline_tactic = Some tac }, psl
+let set_endline_tactic tac ps =
+  { ps with endline_tactic = Some tac }
 
 let pf_name_eq id ps =
   let Proof.{ name } = Proof.data ps.proof in
@@ -112,8 +136,10 @@ let discard {CAst.loc;v=id} (ps, psl) =
   | [] -> None
   | ps :: psl -> Some (ps, psl)
 
-let discard_current (ps, psl) =
-  if List.is_empty psl then None else Some List.(hd psl, tl psl)
+let discard_current (_, psl) =
+  match psl with
+  | [] -> None
+  | ps :: psl -> Some (ps, psl)
 
 (** [start_proof sigma id pl str goals terminator] starts a proof of name
     [id] with goals [goals] (a list of pairs of environment and
@@ -123,30 +149,26 @@ let discard_current (ps, psl) =
     end of the proof to close the proof. The proof is started in the
     evar map [sigma] (which can typically contain universe
     constraints), and with universe bindings pl. *)
-let start_proof ~ontop sigma name ?(pl=UState.default_univ_decl) kind goals terminator =
-  let initial_state = {
-    terminator = CEphemeron.create terminator;
+let start_proof sigma name ?(pl=UState.default_univ_decl) kind goals terminator =
+  { terminator = CEphemeron.create terminator;
     proof = Proof.start ~name ~poly:(pi2 kind) sigma goals;
     endline_tactic = None;
     section_vars = None;
     universe_decl = pl;
-    strength = kind } in
-  push ~ontop initial_state
+    strength = kind }
 
-let start_dependent_proof ~ontop name ?(pl=UState.default_univ_decl) kind goals terminator =
-  let initial_state = {
-    terminator = CEphemeron.create terminator;
+let start_dependent_proof name ?(pl=UState.default_univ_decl) kind goals terminator =
+  { terminator = CEphemeron.create terminator;
     proof = Proof.dependent_start ~name ~poly:(pi2 kind) goals;
     endline_tactic = None;
     section_vars = None;
     universe_decl = pl;
-    strength = kind } in
-  push ~ontop initial_state
+    strength = kind }
 
-let get_used_variables (pf,_) = pf.section_vars
-let get_universe_decl (pf,_) = pf.universe_decl
+let get_used_variables pf = pf.section_vars
+let get_universe_decl pf = pf.universe_decl
 
-let set_used_variables (ps,psl) l =
+let set_used_variables ps l =
   let open Context.Named.Declaration in
   let env = Global.env () in
   let ids = List.fold_right Id.Set.add l Id.Set.empty in
@@ -170,9 +192,9 @@ let set_used_variables (ps,psl) l =
   if not (Option.is_empty ps.section_vars) then
     CErrors.user_err Pp.(str "Used section variables can be declared only once");
   (* EJGA: This is always empty thus we should modify the type *)
-  (ctx, []), ({ ps with section_vars = Some ctx}, psl)
+  (ctx, []), { ps with section_vars = Some ctx}
 
-let get_open_goals (ps, _) =
+let get_open_goals ps =
   let Proof.{ goals; stack; shelf } = Proof.data ps.proof in
   List.length goals +
   List.fold_left (+) 0
@@ -293,7 +315,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
     universes },
   fun pr_ending -> CEphemeron.get terminator pr_ending
 
-let return_proof ?(allow_partial=false) (ps,_) =
+let return_proof ?(allow_partial=false) ps =
  let { proof } = ps in
  if allow_partial then begin
   let proofs = Proof.partial_proof proof in
@@ -322,27 +344,27 @@ let return_proof ?(allow_partial=false) (ps,_) =
     List.map (fun (c, _) -> (proof_opt c, eff)) initial_goals in
     proofs, Evd.evar_universe_context evd
 
-let close_future_proof ~opaque ~feedback_id (ps, psl) proof =
+let close_future_proof ~opaque ~feedback_id ps proof =
   close_proof ~opaque ~keep_body_ucst_separate:true ~feedback_id ~now:false proof ps
 
-let close_proof ~opaque ~keep_body_ucst_separate fix_exn (ps, psl) =
+let close_proof ~opaque ~keep_body_ucst_separate fix_exn ps =
   close_proof ~opaque ~keep_body_ucst_separate ~now:true
-    (Future.from_val ~fix_exn (return_proof (ps,psl))) ps
+    (Future.from_val ~fix_exn (return_proof ps)) ps
 
 (** Gets the current terminator without checking that the proof has
     been completed. Useful for the likes of [Admitted]. *)
-let get_terminator (ps, _) = CEphemeron.get ps.terminator
-let set_terminator hook (ps, psl) =
-  { ps with terminator = CEphemeron.create hook }, psl
+let get_terminator ps = CEphemeron.get ps.terminator
+let set_terminator hook ps =
+  { ps with terminator = CEphemeron.create hook }
 
 let copy_terminators ~src ~tgt =
   let (ps, psl), (ts,tsl) = src, tgt in
   assert(List.length psl = List.length tsl);
   {ts with terminator = ps.terminator}, List.map2 (fun op p -> { p with terminator = op.terminator }) psl tsl
 
-let update_global_env (pf : t) =
+let update_global_env pf =
   let res, () =
-  with_current_proof (fun _ p ->
+  with_proof (fun _ p ->
      Proof.in_proof p (fun sigma ->
        let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in
        let (p,(status,info),()) = Proof.run_tactic (Global.env ()) tac p in
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index e2e457483b..aff48b9636 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -13,12 +13,16 @@
      environment. *)
 
 type t
+type stack
+
+val get_current_pstate : stack -> t
+
 val get_current_proof_name : t -> Names.Id.t
 val get_current_persistence : t -> Decl_kinds.goal_kind
-val get_all_proof_names : t -> Names.Id.t list
+val get_all_proof_names : stack -> Names.Id.t list
 
-val discard : Names.lident -> t -> t option
-val discard_current : t -> t option
+val discard : Names.lident -> stack -> stack option
+val discard_current : stack -> stack option
 
 val give_me_the_proof : t -> Proof.t
 val compact_the_proof : t -> t
@@ -52,6 +56,10 @@ type closed_proof = proof_object * proof_terminator
 val make_terminator : (proof_ending -> unit) -> proof_terminator
 val apply_terminator : proof_terminator -> proof_ending -> unit
 
+val push : ontop:stack option -> t -> stack
+
+val maybe_push : ontop:stack option -> t option -> stack option
+
 (** [start_proof ~ontop id str pl goals terminator] starts a proof of name
    [id] with goals [goals] (a list of pairs of environment and
    conclusion); [str] describes what kind of theorem/definition this
@@ -60,14 +68,14 @@ val apply_terminator : proof_terminator -> proof_ending -> unit
    morphism). The proof is started in the evar map [sigma] (which can
    typically contain universe constraints), and with universe bindings
    pl. *)
-val start_proof : ontop:t option ->
+val start_proof :
   Evd.evar_map -> Names.Id.t -> ?pl:UState.universe_decl ->
   Decl_kinds.goal_kind -> (Environ.env * EConstr.types) list  ->
     proof_terminator -> t
 
 (** Like [start_proof] except that there may be dependencies between
     initial goals. *)
-val start_dependent_proof : ontop:t option ->
+val start_dependent_proof :
   Names.Id.t -> ?pl:UState.universe_decl -> Decl_kinds.goal_kind ->
   Proofview.telescope -> proof_terminator -> t
 
@@ -78,7 +86,8 @@ val update_global_env : t -> t
 
 (* Takes a function to add to the exceptions data relative to the
    state in which the proof was built *)
-val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> t -> closed_proof
+val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn ->
+  t -> closed_proof
 
 (* Intermediate step necessary to delegate the future.
  * Both access the current proof state. The former is supposed to be
@@ -102,9 +111,15 @@ val get_open_goals : t -> int
     no current proof.
     The return boolean is set to [false] if an unsafe tactic has been used. *)
 val with_current_proof :
-  (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> t -> t * 'a
+  (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> stack -> stack * 'a
 val simple_with_current_proof :
-  (unit Proofview.tactic -> Proof.t -> Proof.t) -> t -> t
+  (unit Proofview.tactic -> Proof.t -> Proof.t) -> stack -> stack
+
+val with_proof : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> t -> t * 'a
+val modify_proof : (Proof.t -> Proof.t) -> t -> t
+
+val with_current_pstate : (t -> t * 'a) -> stack -> stack * 'a
+val modify_current_pstate : (t -> t) -> stack -> stack
 
 (** Sets the tactic to be used when a tactic line is closed with [...] *)
 val set_endline_tactic : Genarg.glob_generic_argument -> t -> t
@@ -120,4 +135,4 @@ val get_used_variables : t -> Constr.named_context option
 (** Get the universe declaration associated to the current proof. *)
 val get_universe_decl : t -> UState.universe_decl
 
-val copy_terminators : src:t -> tgt:t -> t
+val copy_terminators : src:stack -> tgt:stack -> stack