From a2549c7f716e870ea19fdbfd7b5493117fe21e76 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 9 Dec 2018 05:50:12 +0100
Subject: [proof] Rework proof interface.

- deprecate the old 5-tuple accessor in favor of a view record,

- move `name` and `kind` proof data from `Proof_global` to `Proof`,
  this will prove useful in subsequent functionalizations of the
  interface, in particular this is what abstract, which lives in the
  monads, needs in order no to access global state.

- Note that `Proof.t` and `Proof_global.t` are redundant anyways.
---
 proofs/pfedit.ml       | 13 +++----
 proofs/pfedit.mli      |  9 +++--
 proofs/proof.ml        | 97 ++++++++++++++++++++++++++++++++++++--------------
 proofs/proof.mli       | 63 +++++++++++++++++++++++++++-----
 proofs/proof_global.ml | 70 ++++++++++++++++++------------------
 5 files changed, 174 insertions(+), 78 deletions(-)

(limited to 'proofs')

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index acf5510aa0..e2b7df19de 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -33,7 +33,7 @@ let () = CErrors.register_handler begin function
 end
 
 let get_nth_V82_goal p i =
-  let goals,_,_,_,sigma = Proof.proof p in
+  let Proof.{ sigma; goals } = Proof.data p in
   try { it = List.nth goals (i-1) ; sigma }
   with Failure _ -> raise NoSuchGoal
 
@@ -120,7 +120,8 @@ let solve ?with_end_tac gi info_lvl tac pr =
 let by tac = Proof_global.with_current_proof (fun _ -> solve (Goal_select.SelectNth 1) None tac)
 
 let instantiate_nth_evar_com n com = 
-  Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.instantiate_evar n com p)
+  Proof_global.simple_with_current_proof (fun _ p ->
+      Proof.V82.instantiate_evar Global.(env ())n com p)
 
 
 (**********************************************************************)
@@ -166,7 +167,7 @@ let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac =
   let univs = UState.merge ~sideff:side_eff ~extend:true Evd.univ_rigid univs ctx in
   cb, status, univs
 
-let refine_by_tactic env sigma ty tac =
+let refine_by_tactic ~name ~poly env sigma ty tac =
   (* Save the initial side-effects to restore them afterwards. We set the
      current set of side-effects to be empty so that we can retrieve the
      ones created during the tactic invocation easily. *)
@@ -175,7 +176,7 @@ let refine_by_tactic env sigma ty tac =
   (* Save the existing goals *)
   let prev_future_goals = save_future_goals sigma in
   (* Start a proof *)
-  let prf = Proof.start sigma [env, ty] in
+  let prf = Proof.start ~name ~poly sigma [env, ty] in
   let (prf, _) =
     try Proof.run_tactic env tac prf
     with Logic_monad.TacticFailure e as src ->
@@ -184,9 +185,9 @@ let refine_by_tactic env sigma ty tac =
       iraise (e, info)
   in
   (* Plug back the retrieved sigma *)
-  let (goals,stack,shelf,given_up,sigma) = Proof.proof prf in
+  let Proof.{ goals; stack; shelf; given_up; sigma; entry } = Proof.data prf in
   assert (stack = []);
-  let ans = match Proof.initial_goals prf with
+  let ans = match Proofview.initial_goals entry with
   | [c, _] -> c
   | _ -> assert false
   in
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 155221947a..5699320af5 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -81,8 +81,13 @@ val build_by_tactic : ?side_eff:bool -> env -> UState.t -> ?poly:polymorphic ->
   EConstr.types -> unit Proofview.tactic -> 
   constr * bool * UState.t
 
-val refine_by_tactic : env -> Evd.evar_map -> EConstr.types -> unit Proofview.tactic ->
-  constr * Evd.evar_map
+val refine_by_tactic
+  :  name:Id.t
+  -> poly:bool
+  -> env -> Evd.evar_map
+  -> EConstr.types
+  -> unit Proofview.tactic
+  -> constr * Evd.evar_map
 (** A variant of the above function that handles open terms as well.
     Caveat: all effects are purged in the returned term at the end, but other
     evars solved by side-effects are NOT purged, so that unexpected failures may
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 6c13c4946a..1aeb24606b 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -105,22 +105,29 @@ let done_cond ?(loose_end=false) k = CondDone (loose_end,k)
 
 (* Subpart of the type of proofs. It contains the parts of the proof which
    are under control of the undo mechanism *)
-type t = {
-  (* Current focused proofview *)
-  proofview: Proofview.proofview;
-  (* Entry for the proofview *)
-  entry : Proofview.entry;
-  (* History of the focusings, provides information on how
-     to unfocus the proof and the extra information stored while focusing.
-     The list is empty when the proof is fully unfocused. *)
-  focus_stack: (_focus_condition*focus_info*Proofview.focus_context) list;
-  (* List of goals that have been shelved. *)
-  shelf : Goal.goal list;
-  (* List of goals that have been given up *)
-  given_up : Goal.goal list;
-  (* The initial universe context (for the statement) *)
-  initial_euctx : UState.t
-}
+type t =
+  { proofview: Proofview.proofview
+  (** Current focused proofview *)
+  ; entry : Proofview.entry
+  (** Entry for the proofview *)
+  ; focus_stack: (_focus_condition*focus_info*Proofview.focus_context) list
+  (** History of the focusings, provides information on how to unfocus
+     the proof and the extra information stored while focusing.  The
+     list is empty when the proof is fully unfocused. *)
+  ; shelf : Goal.goal list
+  (** List of goals that have been shelved. *)
+  ; given_up : Goal.goal list
+  (** List of goals that have been given up *)
+  ; initial_euctx : UState.t
+  (** The initial universe context (for the statement) *)
+  ; name : Names.Id.t
+  (** the name of the theorem whose proof is being constructed *)
+  ; poly : bool
+  (** Locality, polymorphism, and "kind" [Coercion, Definition, etc...] *)
+  }
+
+let initial_goals pf = Proofview.initial_goals pf.entry
+let initial_euctx pf = pf.initial_euctx
 
 (*** General proof functions ***)
 
@@ -141,7 +148,7 @@ let proof p =
   (goals,stack,shelf,given_up,sigma)
 
 type 'a pre_goals = {
-    fg_goals : 'a list;
+  fg_goals : 'a list;
   (** List of the focussed goals *)
   bg_goals : ('a list * 'a list) list;
   (** Zipper representing the unfocussed background goals *)
@@ -311,7 +318,7 @@ let end_of_stack = CondEndStack end_of_stack_kind
 
 let unfocused = is_last_focus end_of_stack_kind
 
-let start sigma goals =
+let start ~name ~poly sigma goals =
   let entry, proofview = Proofview.init sigma goals in
   let pr = {
     proofview;
@@ -320,9 +327,13 @@ let start sigma goals =
     shelf = [] ;
     given_up = [];
     initial_euctx =
-      Evd.evar_universe_context (snd (Proofview.proofview proofview)) } in
+      Evd.evar_universe_context (snd (Proofview.proofview proofview))
+    ; name
+    ; poly
+  } in
   _focus end_of_stack (Obj.repr ()) 1 (List.length goals) pr
-let dependent_start goals =
+
+let dependent_start ~name ~poly goals =
   let entry, proofview = Proofview.dependent_init goals in
   let pr = {
     proofview;
@@ -331,7 +342,10 @@ let dependent_start goals =
     shelf = [] ;
     given_up = [];
     initial_euctx =
-      Evd.evar_universe_context (snd (Proofview.proofview proofview)) } in
+      Evd.evar_universe_context (snd (Proofview.proofview proofview))
+    ; name
+    ; poly
+  } in
   let number_of_goals = List.length (Proofview.initial_goals pr.entry) in
   _focus end_of_stack (Obj.repr ()) 1 number_of_goals pr
 
@@ -375,9 +389,6 @@ let return ?pid (p : t) =
     let p = unfocus end_of_stack_kind p () in
     Proofview.return p.proofview
 
-let initial_goals p = Proofview.initial_goals p.entry
-let initial_euctx p = p.initial_euctx
-
 let compact p =
   let entry, proofview = Proofview.compact p.entry p.proofview in
   { p with proofview; entry }
@@ -468,7 +479,7 @@ module V82 = struct
       { p with proofview = Proofview.V82.grab p.proofview }
 
   (* Main component of vernac command Existential *)
-  let instantiate_evar n com pr =
+  let instantiate_evar env n com pr =
     let tac =
       Proofview.tclBIND Proofview.tclEVARMAP begin fun sigma ->
       let (evk, evi) =
@@ -487,7 +498,7 @@ module V82 = struct
       let sigma = Evar_refiner.w_refine (evk, evi) (ltac_vars, rawc) sigma in
       Proofview.Unsafe.tclEVARS sigma
     end in
-    let ((), proofview, _, _) = Proofview.apply (Global.env ()) tac pr.proofview in
+    let ((), proofview, _, _) = Proofview.apply env tac pr.proofview in
     let shelf =
       List.filter begin fun g ->
         Evd.is_undefined (Proofview.return proofview) g
@@ -507,3 +518,37 @@ let all_goals p =
     let set = add given_up set in
     let { Evd.it = bgoals ; sigma = bsigma } = V82.background_subgoals p in
     add bgoals set
+
+type data =
+  { sigma : Evd.evar_map
+  (** A representation of the evar_map [EJGA wouldn't it better to just return the proofview?] *)
+  ; goals : Evar.t list
+  (** Focused goals *)
+  ; entry : Proofview.entry
+  (** Entry for the proofview *)
+  ; stack : (Evar.t list * Evar.t list) list
+  (** A representation of the focus stack *)
+  ; shelf : Evar.t list
+  (** A representation of the shelf  *)
+  ; given_up : Evar.t list
+  (** A representation of the given up goals  *)
+  ; initial_euctx : UState.t
+  (** The initial universe context (for the statement) *)
+  ; name : Names.Id.t
+  (** The name of the theorem whose proof is being constructed *)
+  ; poly : bool
+  (** Locality, polymorphism, and "kind" [Coercion, Definition, etc...] *)
+  }
+
+let data { proofview; focus_stack; entry; shelf; given_up; initial_euctx; name; poly } =
+  let goals, sigma = Proofview.proofview proofview in
+  (* spiwack: beware, the bottom of the stack is used by [Proof]
+     internally, and should not be exposed. *)
+  let rec map_minus_one f = function
+    | [] -> assert false
+    | [_] -> []
+    | a::l -> f a :: (map_minus_one f l)
+  in
+  let stack =
+    map_minus_one (fun (_,_,c) -> Proofview.focus_context c) focus_stack in
+  { sigma; goals; entry; stack; shelf; given_up; initial_euctx; name; poly }
diff --git a/proofs/proof.mli b/proofs/proof.mli
index aaabea3454..fd5e905a3b 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -50,27 +50,70 @@ val proof : t ->
   * Goal.goal list
   * Goal.goal list
   * Evd.evar_map
+[@@ocaml.deprecated "use [Proof.data]"]
+
+val initial_goals : t -> (EConstr.constr * EConstr.types) list
+[@@ocaml.deprecated "use [Proof.data]"]
+
+val initial_euctx : t -> UState.t
+[@@ocaml.deprecated "use [Proof.data]"]
+
+type data =
+  { sigma : Evd.evar_map
+  (** A representation of the evar_map [EJGA wouldn't it better to just return the proofview?] *)
+  ; goals : Evar.t list
+  (** Focused goals *)
+  ; entry : Proofview.entry
+  (** Entry for the proofview *)
+  ; stack : (Evar.t list * Evar.t list) list
+  (** A representation of the focus stack *)
+  ; shelf : Evar.t list
+  (** A representation of the shelf  *)
+  ; given_up : Evar.t list
+  (** A representation of the given up goals  *)
+  ; initial_euctx : UState.t
+  (** The initial universe context (for the statement) *)
+  ; name : Names.Id.t
+  (** The name of the theorem whose proof is being constructed *)
+  ; poly : bool;
+  (** polymorphism *)
+  }
+
+val data : t -> data
 
 (* Generic records structured like the return type of proof *)
 type 'a pre_goals = {
   fg_goals : 'a list;
+  [@ocaml.deprecated "use [Proof.data]"]
   (** List of the focussed goals *)
   bg_goals : ('a list * 'a list) list;
+  [@ocaml.deprecated "use [Proof.data]"]
   (** Zipper representing the unfocussed background goals *)
   shelved_goals : 'a list;
+  [@ocaml.deprecated "use [Proof.data]"]
   (** List of the goals on the shelf. *)
   given_up_goals : 'a list;
+  [@ocaml.deprecated "use [Proof.data]"]
   (** List of the goals that have been given up *)
 }
+[@@ocaml.deprecated "use [Proof.data]"]
 
-val map_structured_proof : t -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre_goals)
-
+(* needed in OCaml 4.05.0, not needed in newer ones *)
+[@@@ocaml.warning "-3"]
+val map_structured_proof : t -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre_goals) [@ocaml.warning "-3"]
+[@@ocaml.deprecated "use [Proof.data]"]
+[@@@ocaml.warning "+3"]
 
 (*** General proof functions ***)
-val start : Evd.evar_map -> (Environ.env * EConstr.types) list -> t
-val dependent_start : Proofview.telescope -> t
-val initial_goals : t -> (EConstr.constr * EConstr.types) list
-val initial_euctx : t -> UState.t
+val start
+  :  name:Names.Id.t
+  -> poly:bool
+  -> Evd.evar_map -> (Environ.env * EConstr.types) list -> t
+
+val dependent_start
+  :  name:Names.Id.t
+  -> poly:bool
+  -> Proofview.telescope -> t
 
 (* Returns [true] if the considered proof is completed, that is if no goal remain
     to be considered (this does not require that all evars have been solved). *)
@@ -177,8 +220,9 @@ val no_focused_goal : t -> bool
 
 (* the returned boolean signal whether an unsafe tactic has been
    used. In which case it is [false]. *)
-val run_tactic : Environ.env ->
-  unit Proofview.tactic -> t -> t * (bool*Proofview_monad.Info.tree)
+val run_tactic
+  :  Environ.env
+  -> unit Proofview.tactic -> t -> t * (bool*Proofview_monad.Info.tree)
 
 val maximal_unfocus : 'a focus_kind -> t -> t
 
@@ -208,7 +252,8 @@ module V82 : sig
   val grab_evars : t -> t
 
   (* Implements the Existential command *)
-  val instantiate_evar : int -> Constrexpr.constr_expr -> t -> t
+  val instantiate_evar :
+    Environ.env -> int -> Constrexpr.constr_expr -> t -> t
 end
 
 (* returns the set of all goals in the proof *)
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 76a1e61ad2..2027ad4e21 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -90,14 +90,13 @@ type proof_terminator = proof_ending -> unit
 type closed_proof = proof_object * proof_terminator
 
 type pstate = {
-  pid : Id.t;  (* the name of the theorem whose proof is being constructed *)
   terminator : proof_terminator CEphemeron.key;
   endline_tactic : Genarg.glob_generic_argument option;
   section_vars : Constr.named_context option;
   proof : Proof.t;
-  strength : Decl_kinds.goal_kind;
   mode : proof_mode CEphemeron.key;
   universe_decl: UState.universe_decl;
+  strength : Decl_kinds.goal_kind;
 }
 
 type t = pstate list
@@ -142,7 +141,7 @@ end
 (*** Proof Global manipulation ***)
 
 let get_all_proof_names () =
-  List.map (function { pid = id } -> id) !pstates
+  List.map Proof.(function pf -> (data pf.proof).name) !pstates
 
 let cur_pstate () =
   match !pstates with
@@ -151,7 +150,7 @@ let cur_pstate () =
 
 let give_me_the_proof () = (cur_pstate ()).proof
 let give_me_the_proof_opt () = try Some (give_me_the_proof ()) with | NoCurrentProof -> None
-let get_current_proof_name () = (cur_pstate ()).pid
+let get_current_proof_name () = (Proof.data (cur_pstate ()).proof).Proof.name
 
 let with_current_proof f =
   match !pstates with
@@ -205,8 +204,12 @@ let check_no_pending_proof () =
        str"Use \"Abort All\" first or complete proof(s).")
   end
 
+let pf_name_eq id ps =
+  let Proof.{ name } = Proof.data ps.proof in
+  Id.equal name id
+
 let discard_gen id =
-  pstates := List.filter (fun { pid = id' } -> not (Id.equal id id')) !pstates
+  pstates := List.filter (fun pf -> not (pf_name_eq id pf)) !pstates
 
 let discard {CAst.loc;v=id} =
   let n = List.length !pstates in
@@ -223,9 +226,9 @@ let discard_all () = pstates := []
 (* [set_proof_mode] sets the proof mode to be used after it's called. It is
     typically called by the Proof Mode command. *)
 let set_proof_mode m id =
-  pstates :=
-    List.map (function { pid = id' } as p ->
-      if Id.equal id' id then { p with mode = m } else p) !pstates;
+  pstates := List.map
+      (fun ps -> if pf_name_eq id ps then { ps with mode = m } else ps)
+      !pstates;
   update_proof_mode ()
 
 let set_proof_mode mn =
@@ -244,28 +247,26 @@ let disactivate_current_proof_mode () =
     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 sigma id ?(pl=UState.default_univ_decl) str goals terminator =
+let start_proof sigma name ?(pl=UState.default_univ_decl) kind goals terminator =
   let initial_state = {
-    pid = id;
     terminator = CEphemeron.create terminator;
-    proof = Proof.start sigma goals;
+    proof = Proof.start ~name ~poly:(pi2 kind) sigma goals;
     endline_tactic = None;
     section_vars = None;
-    strength = str;
     mode = find_proof_mode "No";
-    universe_decl = pl } in
+    universe_decl = pl;
+    strength = kind } in
   push initial_state pstates
 
-let start_dependent_proof id ?(pl=UState.default_univ_decl) str goals terminator =
+let start_dependent_proof name ?(pl=UState.default_univ_decl) kind goals terminator =
   let initial_state = {
-    pid = id;
     terminator = CEphemeron.create terminator;
-    proof = Proof.dependent_start goals;
+    proof = Proof.dependent_start ~name ~poly:(pi2 kind) goals;
     endline_tactic = None;
     section_vars = None;
-    strength = str;
     mode = find_proof_mode "No";
-    universe_decl = pl } in
+    universe_decl = pl;
+    strength = kind } in
   push initial_state pstates
 
 let get_used_variables () = (cur_pstate ()).section_vars
@@ -301,10 +302,10 @@ let set_used_variables l =
       ctx, []
 
 let get_open_goals () =
-  let gl, gll, shelf , _ , _ = Proof.proof (cur_pstate ()).proof in
-  List.length gl +
+  let Proof.{ goals; stack; shelf } = Proof.data (cur_pstate ()).proof in
+  List.length goals +
     List.fold_left (+) 0
-    (List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) +
+    (List.map (fun (l1,l2) -> List.length l1 + List.length l2) stack) +
     List.length shelf
 
 type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * UState.t
@@ -323,12 +324,9 @@ let private_poly_univs =
 
 let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
                 (fpl : closed_proof_output Future.computation) =
-  let { pid; section_vars; strength; proof; terminator; universe_decl } =
-    cur_pstate () in
+  let { section_vars; proof; terminator; universe_decl; strength } = cur_pstate () in
+  let Proof.{ name; poly; entry; initial_euctx } = Proof.data proof in
   let opaque = match opaque with Opaque -> true | Transparent -> false in
-  let poly = pi2 strength (* Polymorphic *) in
-  let initial_goals = Proof.initial_goals proof in
-  let initial_euctx = Proof.initial_euctx proof in
   let constrain_variables ctx =
     UState.constrain_variables (fst (UState.context_set initial_euctx)) ctx
   in
@@ -411,16 +409,16 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
       const_entry_opaque = opaque;
       const_entry_universes = univs; }
   in
-  let entries = Future.map2 entry_fn fpl initial_goals in
-  { id = pid; entries = entries; persistence = strength;
+  let entries = Future.map2 entry_fn fpl Proofview.(initial_goals entry) in
+  { id = name; entries = entries; persistence = strength;
     universes },
   fun pr_ending -> CEphemeron.get terminator pr_ending
 
 let return_proof ?(allow_partial=false) () =
- let { pid; proof; strength = (_,poly,_) } = cur_pstate () in
+ let { proof } = cur_pstate () in
  if allow_partial then begin
   let proofs = Proof.partial_proof proof in
-  let _,_,_,_, evd = Proof.proof proof in
+  let Proof.{sigma=evd} = Proof.data proof in
   let eff = Evd.eval_side_effects evd 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
@@ -428,7 +426,8 @@ let return_proof ?(allow_partial=false) () =
   let proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in
     proofs, Evd.evar_universe_context evd
  end else
-  let initial_goals = Proof.initial_goals proof in
+  let Proof.{name=pid;entry} = 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
@@ -455,10 +454,11 @@ let set_terminator hook =
 
 module V82 = struct
   let get_current_initial_conclusions () =
-  let { pid; strength; proof } = cur_pstate () in
-  let initial = Proof.initial_goals proof in
+  let { proof; strength } = cur_pstate () in
+  let Proof.{ name; entry } = Proof.data proof in
+  let initial = Proofview.initial_goals entry in
   let goals = List.map (fun (o, c) -> c) initial in
-    pid, (goals, strength)
+  name, (goals, strength)
 end
 
 let freeze ~marshallable =
@@ -473,7 +473,7 @@ let copy_terminators ~src ~tgt =
   assert(List.length src = List.length tgt);
   List.map2 (fun op p -> { p with terminator = op.terminator }) src tgt
 
-let update_global_env () =
+let update_global_env pf_info =
   with_current_proof (fun _ p ->
      Proof.in_proof p (fun sigma ->
        let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in
-- 
cgit v1.2.3