[lemmas] Move `Stack` out of Lemmas.

We move the stack of open lemmas from `Lemmas` to `Vernacstate`. The
`Lemmas` module doesn't deal with stacked proofs, so the stack can be
moved to to the proper place; this reduces the size of the API.

Note that `Lemmas` API is still quite imperative, it would be great if
we would return some more information on close proof, for example
about the global environment parts that were modified.

7 files changed, 82 insertions, 90 deletions

diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index 4f5cef648b..129444c3b3 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -49,7 +49,7 @@ let is_focused_goal_simple ~doc id =
   match state_of_id ~doc id with
   | `Expired | `Error _ | `Valid None -> `Not
   | `Valid (Some { Vernacstate.lemmas }) ->
-    Option.cata (Lemmas.Stack.with_top_pstate ~f:(fun proof ->
+    Option.cata (Vernacstate.LemmaStack.with_top_pstate ~f:(fun proof ->
         let proof = Proof_global.get_proof proof in
         let Proof.{ goals=focused; stack=r1; shelf=r2; given_up=r3; sigma } = Proof.data proof in
         let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in
diff --git a/stm/stm.ml b/stm/stm.ml
index 28d5447c44..f3ae32a719 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -881,7 +881,7 @@ end = struct (* {{{ *)
   let invalidate_cur_state () = cur_id := Stateid.dummy
 
   type proof_part =
-    Lemmas.Stack.t option *
+    Vernacstate.LemmaStack.t option *
     int *                                   (* Evarutil.meta_counter_summary_tag *)
     int *                                   (* Evd.evar_counter_summary_tag *)
     DeclareObl.program_info CEphemeron.key Names.Id.Map.t (* Obligations.program_tcc_summary_tag *)
@@ -1168,7 +1168,7 @@ end = struct (* {{{ *)
 
   let get_proof ~doc id =
     match state_of_id ~doc id with
-    | `Valid (Some vstate) -> Option.map (Lemmas.Stack.with_top_pstate ~f:Proof_global.get_proof) vstate.Vernacstate.lemmas
+    | `Valid (Some vstate) -> Option.map (Vernacstate.LemmaStack.with_top_pstate ~f:Proof_global.get_proof) vstate.Vernacstate.lemmas
     | _ -> None
 
   let undo_vernac_classifier v ~doc =
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 173a83f1d1..35b902fff9 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -307,41 +307,6 @@ let initialize_named_context_for_proof () =
       let d = if variable_opacity id then NamedDecl.drop_body d else d in
       Environ.push_named_context_val d signv) sign Environ.empty_named_context_val
 
-module Stack = struct
-
-  type lemma = t
-  type nonrec t = t * t list
-
-  let map f (pf, pfl) = (f pf, List.map f pfl)
-
-  let map_top ~f (pf, pfl) = (f pf, pfl)
-  let map_top_pstate ~f (pf, pfl) = (pf_map f pf, pfl)
-
-  let pop (ps, p) = match p with
-    | [] -> ps, None
-    | pp :: p -> ps, Some (pp, p)
-
-  let with_top (p, _) ~f = f p
-  let with_top_pstate (p, _) ~f = f p.proof
-
-  let push ontop a =
-    match ontop with
-    | None -> a , []
-    | Some (l,ls) -> a, (l :: ls)
-
-  let get_all_proof_names (pf : t) =
-    let prj x = Proof_global.get_proof x in
-    let (pn, pns) = map Proof.(function pf -> (data (prj pf.proof)).name) pf in
-    pn :: pns
-
-  let copy_info ~src ~tgt =
-    let (ps, psl), (ts,tsl) = src, tgt in
-    assert(List.length psl = List.length tsl);
-    { ps with proof = ts.proof },
-    List.map2 (fun op p -> { op with proof = p.proof }) psl tsl
-
-end
-
 (* Starting a goal *)
 let start_lemma ~name ~poly
     ?(udecl=UState.default_univ_decl)
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 88f26a04b7..276d7ae144 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -17,30 +17,11 @@ type t
 (** [Lemmas.t] represents a constant that is being proved, usually
     interactively *)
 
-module Stack : sig
-
-  type lemma = t
-  type t
-
-  val pop : t -> lemma * t option
-  val push : t option -> lemma -> t
-
-  val map_top : f:(lemma -> lemma) -> t -> t
-  val map_top_pstate : f:(Proof_global.t -> Proof_global.t) -> t -> t
-
-  val with_top : t -> f:(lemma -> 'a ) -> 'a
-  val with_top_pstate : t -> f:(Proof_global.t -> 'a ) -> 'a
-
-  val get_all_proof_names : t -> Names.Id.t list
-
-  val copy_info : src:t -> tgt:t -> t
-  (** Gets the current info without checking that the proof has been
-     completed. Useful for the likes of [Admitted]. *)
-
-end
-
 val set_endline_tactic : Genarg.glob_generic_argument -> t -> t
+
 val pf_map : (Proof_global.t -> Proof_global.t) -> t -> t
+(** [pf_map f l] map the underlying proof object *)
+
 val pf_fold : (Proof_global.t -> 'a) -> t -> 'a
 (** [pf_fold f l] fold over the underlying proof object *)
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index dc46aad8af..dba9d5dfc5 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -55,7 +55,7 @@ let vernac_require_open_lemma ~stack f =
 
 let with_pstate ~stack f =
   vernac_require_open_lemma ~stack
-    (fun ~stack -> Stack.with_top_pstate stack ~f:(fun pstate -> f ~pstate))
+    (fun ~stack -> Vernacstate.LemmaStack.with_top_pstate stack ~f:(fun pstate -> f ~pstate))
 
 let get_current_or_global_context ~pstate =
   match pstate with
@@ -645,14 +645,14 @@ let vernac_start_proof ~atts kind l =
 let vernac_end_proof ?stack ?proof = let open Vernacexpr in function
   | Admitted ->
     vernac_require_open_lemma ~stack (fun ~stack ->
-      let lemma, stack = Stack.pop stack in
+      let lemma, stack = Vernacstate.LemmaStack.pop stack in
       save_lemma_admitted ?proof ~lemma;
       stack)
   | Proved (opaque,idopt) ->
     let lemma, stack = match stack with
       | None -> None, None
       | Some stack ->
-        let lemma, stack = Stack.pop stack in
+        let lemma, stack = Vernacstate.LemmaStack.pop stack in
         Some lemma, stack
     in
     save_lemma_proved ?lemma ?proof ~opaque ~idopt;
@@ -2341,15 +2341,15 @@ let interp_typed_vernac c ~stack =
     stack
   | VtCloseProof f ->
     vernac_require_open_lemma ~stack (fun ~stack ->
-        let lemma, stack = Stack.pop stack in
+        let lemma, stack = Vernacstate.LemmaStack.pop stack in
         f ~lemma;
         stack)
   | VtOpenProof f ->
-    Some (Stack.push stack (f ()))
+    Some (Vernacstate.LemmaStack.push stack (f ()))
   | VtModifyProof f ->
-    Option.map (Stack.map_top_pstate ~f:(fun pstate -> f ~pstate)) stack
+    Option.map (Vernacstate.LemmaStack.map_top_pstate ~f:(fun pstate -> f ~pstate)) stack
   | VtReadProofOpt f ->
-    let pstate = Option.map (Stack.with_top_pstate ~f:(fun x -> x)) stack in
+    let pstate = Option.map (Vernacstate.LemmaStack.with_top_pstate ~f:(fun x -> x)) stack in
     f ~pstate;
     stack
   | VtReadProof f ->
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index f9b4aec45e..c81a4abc1b 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -27,10 +27,45 @@ module Parser = struct
 
 end
 
+module LemmaStack = struct
+
+  type t = Lemmas.t * Lemmas.t list
+
+  let map f (pf, pfl) = (f pf, List.map f pfl)
+
+  let map_top_pstate ~f (pf, pfl) = (Lemmas.pf_map f pf, pfl)
+
+  let pop (ps, p) = match p with
+    | [] -> ps, None
+    | pp :: p -> ps, Some (pp, p)
+
+  let with_top (p, _) ~f = f p
+  let with_top_pstate (p, _) ~f = Lemmas.pf_fold f p
+
+  let push ontop a =
+    match ontop with
+    | None -> a , []
+    | Some (l,ls) -> a, (l :: ls)
+
+  let get_all_proof_names (pf : t) =
+    let prj x = Lemmas.pf_fold Proof_global.get_proof x in
+    let (pn, pns) = map Proof.(function pf -> (data (prj pf)).name) pf in
+    pn :: pns
+
+  let copy_info src tgt =
+    Lemmas.pf_map (fun _ -> Lemmas.pf_fold (fun x -> x) tgt) src
+
+  let copy_info ~src ~tgt =
+    let (ps, psl), (ts,tsl) = src, tgt in
+    copy_info ps ts,
+    List.map2 (fun op p -> copy_info op p) psl tsl
+
+end
+
 type t = {
   parsing : Parser.state;
   system  : States.state;          (* summary + libstack *)
-  lemmas  : Lemmas.Stack.t option; (* proofs of lemmas currently opened *)
+  lemmas  : LemmaStack.t option;   (* proofs of lemmas currently opened *)
   shallow : bool                   (* is the state trimmed down (libstack) *)
 }
 
@@ -75,13 +110,11 @@ let make_shallow st =
 (* Compatibility module *)
 module Proof_global = struct
 
-  type t = Lemmas.Stack.t
-
   let get () = !s_lemmas
   let set x = s_lemmas := x
 
   let get_pstate () =
-    Option.map (Lemmas.Stack.with_top ~f:(Lemmas.pf_fold (fun x -> x))) !s_lemmas
+    Option.map (LemmaStack.with_top ~f:(Lemmas.pf_fold (fun x -> x))) !s_lemmas
 
   let freeze ~marshallable:_ = get ()
   let unfreeze x = s_lemmas := Some x
@@ -100,11 +133,11 @@ module Proof_global = struct
 
   let cc f = match !s_lemmas with
     | None -> raise NoCurrentProof
-    | Some x -> Stack.with_top_pstate ~f x
+    | Some x -> LemmaStack.with_top_pstate ~f x
 
   let cc_lemma f = match !s_lemmas with
     | None -> raise NoCurrentProof
-    | Some x -> Stack.with_top ~f x
+    | Some x -> LemmaStack.with_top ~f x
 
   let cc_stack f = match !s_lemmas with
     | None -> raise NoCurrentProof
@@ -112,12 +145,12 @@ module Proof_global = struct
 
   let dd f = match !s_lemmas with
     | None -> raise NoCurrentProof
-    | Some x -> s_lemmas := Some (Stack.map_top_pstate ~f x)
+    | Some x -> s_lemmas := Some (LemmaStack.map_top_pstate ~f x)
 
   let there_are_pending_proofs () = !s_lemmas <> None
   let get_open_goals () = cc get_open_goals
 
-  let give_me_the_proof_opt () = Option.map (Stack.with_top_pstate ~f:get_proof) !s_lemmas
+  let give_me_the_proof_opt () = Option.map (LemmaStack.with_top_pstate ~f:get_proof) !s_lemmas
   let give_me_the_proof () = cc get_proof
   let get_current_proof_name () = cc get_proof_name
 
@@ -126,8 +159,8 @@ module Proof_global = struct
     match !s_lemmas with
     | None -> raise NoCurrentProof
     | Some stack ->
-      let pf, res = Stack.with_top_pstate stack ~f:(map_fold_proof_endline f) in
-      let stack = Stack.map_top_pstate stack ~f:(fun _ -> pf) in
+      let pf, res = LemmaStack.with_top_pstate stack ~f:(map_fold_proof_endline f) in
+      let stack = LemmaStack.map_top_pstate stack ~f:(fun _ -> pf) in
       s_lemmas := Some stack;
       res
 
@@ -150,7 +183,7 @@ module Proof_global = struct
   let get_current_context () = cc Pfedit.get_current_context
 
   let get_all_proof_names () =
-    try cc_stack Lemmas.Stack.get_all_proof_names
+    try cc_stack LemmaStack.get_all_proof_names
     with NoCurrentProof -> []
 
   let copy_terminators ~src ~tgt =
@@ -158,6 +191,6 @@ module Proof_global = struct
     | None, None -> None
     | Some _ , None -> None
     | None, Some x -> Some x
-    | Some src, Some tgt -> Some (Stack.copy_info ~src ~tgt)
+    | Some src, Some tgt -> Some (LemmaStack.copy_info ~src ~tgt)
 
 end
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index 5234ef7a73..b4322eb09a 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -18,11 +18,27 @@ module Parser : sig
 
 end
 
+module LemmaStack : sig
+
+  type t
+
+  val pop : t -> Lemmas.t * t option
+  val push : t option -> Lemmas.t -> t
+
+  val map_top_pstate : f:(Proof_global.t -> Proof_global.t) -> t -> t
+  val with_top_pstate : t -> f:(Proof_global.t -> 'a ) -> 'a
+
+end
+
 type t =
   { parsing : Parser.state
-  ; system  : States.state          (* summary + libstack *)
-  ; lemmas  : Lemmas.Stack.t option (* proofs of lemmas currently opened *)
-  ; shallow : bool                  (* is the state trimmed down (libstack) *)
+  (** parsing state [parsing state may not behave 100% functionally yet, beware] *)
+  ; system  : States.state
+  (** summary + libstack *)
+  ; lemmas  : LemmaStack.t option
+  (** proofs of lemmas currently opened *)
+  ; shallow : bool
+  (** is the state trimmed down (libstack) *)
   }
 
 val freeze_interp_state : marshallable:bool -> t
@@ -67,19 +83,16 @@ module Proof_global : sig
 
   val get_all_proof_names : unit -> Names.Id.t list
 
-  val copy_terminators : src:Lemmas.Stack.t option -> tgt:Lemmas.Stack.t option -> Lemmas.Stack.t option
-
-  (* Handling of the imperative state *)
-  type t = Lemmas.Stack.t
+  val copy_terminators : src:LemmaStack.t option -> tgt:LemmaStack.t option -> LemmaStack.t option
 
   (* Low-level stuff *)
-  val get : unit -> t option
-  val set : t option -> unit
+  val get : unit -> LemmaStack.t option
+  val set : LemmaStack.t option -> unit
 
   val get_pstate : unit -> Proof_global.t option
 
-  val freeze : marshallable:bool -> t option
-  val unfreeze : t -> unit
+  val freeze : marshallable:bool -> LemmaStack.t option
+  val unfreeze : LemmaStack.t -> unit
 
 end
 [@@ocaml.deprecated "This module is internal and should not be used, instead, thread the proof state"]