[proof] Move bullets to their own module.

Bullets were placed inside the `Proof_global` module, I guess that due
to the global registration function. However, it has logically nothing
to do with the functionality of `Proof_global` and the current
placement may create some interference between the developers
reworking proof state handling and bullets.

We thus put the bullet functionality into its own, independent file.

1 files changed, 248 insertions, 0 deletions

diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml
new file mode 100644
index 000000000..f80cb7cc6
--- /dev/null
+++ b/proofs/proof_bullet.ml
@@ -0,0 +1,248 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Proof
+
+type t = Vernacexpr.bullet
+
+let bullet_eq b1 b2 = match b1, b2 with
+| Vernacexpr.Dash n1, Vernacexpr.Dash n2 -> n1 = n2
+| Vernacexpr.Star n1, Vernacexpr.Star n2 -> n1 = n2
+| Vernacexpr.Plus n1, Vernacexpr.Plus n2 -> n1 = n2
+| _ -> false
+
+let pr_bullet b =
+  match b with
+  | Vernacexpr.Dash n -> Pp.(str (String.make n '-'))
+  | Vernacexpr.Star n -> Pp.(str (String.make n '*'))
+  | Vernacexpr.Plus n -> Pp.(str (String.make n '+'))
+
+
+type behavior = {
+  name : string;
+  put : proof -> t -> proof;
+  suggest: proof -> Pp.t
+}
+
+let behaviors = Hashtbl.create 4
+let register_behavior b = Hashtbl.add behaviors b.name b
+
+(*** initial modes ***)
+let none = {
+  name = "None";
+  put = (fun x _ -> x);
+  suggest = (fun _ -> Pp.mt ())
+}
+let _ = register_behavior none
+
+module Strict = struct
+  type suggestion =
+  | Suggest of t (* this bullet is mandatory here *)
+  | Unfinished of t (* no mandatory bullet here, but this bullet is unfinished *)
+  | NoBulletInUse (* No mandatory bullet (or brace) here, no bullet pending,
+      	       some focused goals exists. *)
+  | NeedClosingBrace (* Some unfocussed goal exists "{" needed to focus them *)
+  | ProofFinished (* No more goal anywhere *)
+
+  (* give a message only if more informative than the standard coq message *)
+  let suggest_on_solved_goal sugg =
+    match sugg with
+    | NeedClosingBrace -> Pp.(str"Try unfocusing with \"}\".")
+    | NoBulletInUse -> Pp.mt ()
+    | ProofFinished -> Pp.mt ()
+    | Suggest b -> Pp.(str"Focus next goal with bullet " ++ pr_bullet b ++ str".")
+    | Unfinished b -> Pp.(str"The current bullet " ++ pr_bullet b ++ str" is unfinished.")
+
+  (* give always a message. *)
+  let suggest_on_error sugg =
+    match sugg with
+    | NeedClosingBrace -> Pp.(str"Try unfocusing with \"}\".")
+    | NoBulletInUse -> assert false (* This should never raise an error. *)
+    | ProofFinished -> Pp.(str"No more subgoals.")
+    | Suggest b -> Pp.(str"Expecting " ++ pr_bullet b ++ str".")
+    | Unfinished b -> Pp.(str"Current bullet " ++ pr_bullet b ++ str" is not finished.")
+
+  exception FailedBullet of t * suggestion
+
+  let _ =
+    CErrors.register_handler
+      (function
+      | FailedBullet (b,sugg) ->
+        let prefix = Pp.(str"Wrong bullet " ++ pr_bullet b ++ str": ") in
+        CErrors.user_err ~hdr:"Focus" Pp.(prefix ++ suggest_on_error sugg)
+      | _ -> raise CErrors.Unhandled)
+
+
+  (* spiwack: we need only one focus kind as we keep a stack of (distinct!) bullets *)
+  let bullet_kind = (new_focus_kind () : t list focus_kind)
+  let bullet_cond = done_cond ~loose_end:true bullet_kind
+
+  (* spiwack: as it is bullets are reset (locally) by *any* non-bullet focusing command
+     experience will tell if this is the right discipline of if we want to be finer and
+     reset them only for a choice of bullets. *)
+  let get_bullets pr =
+    if is_last_focus bullet_kind pr then
+      get_at_focus bullet_kind pr
+    else
+      []
+
+  let has_bullet bul pr =
+    let rec has_bullet = function
+      | b'::_ when bullet_eq bul b' -> true
+      | _::l -> has_bullet l
+      | [] -> false
+    in
+    has_bullet (get_bullets pr)
+
+  (* pop a bullet from proof [pr]. There should be at least one
+     bullet in use. If pop impossible (pending proofs on this level
+     of bullet or higher) then raise [Proof.CannotUnfocusThisWay]. *)
+  let pop pr =
+    match get_bullets pr with
+    | b::_ -> unfocus bullet_kind pr () , b
+    | _ -> assert false
+
+  let push (b:t) pr =
+    focus bullet_cond (b::get_bullets pr) 1 pr
+
+  (* Used only in the next function.
+     TODO: use a recursive function instead? *)
+  exception SuggestFound of t
+
+  let suggest_bullet (prf : proof): suggestion =
+    if is_done prf then ProofFinished
+    else if not (no_focused_goal prf)
+    then (* No suggestion if a bullet is not mandatory, look for an unfinished bullet *)
+      match get_bullets prf with
+      | b::_ -> Unfinished b
+      | _ -> NoBulletInUse
+    else (* There is no goal under focus but some are unfocussed,
+            let us look at the bullet needed. If no  *)
+      let pcobaye = ref prf in
+      try
+        while true do
+          let pcobaye', b = pop !pcobaye in
+         (* pop went well, this means that there are no more goals
+          *under this* bullet b, see if a new b can be pushed. *)
+          (try let _ = push b pcobaye' in (* push didn't fail so a new b can be pushed. *)
+      	 raise (SuggestFound b)
+           with SuggestFound _ as e -> raise e
+           | _ -> ()); (* b could not be pushed, so we must look for a outer bullet *)
+          pcobaye := pcobaye'
+        done;
+        assert false
+      with SuggestFound b -> Suggest b
+      | _ -> NeedClosingBrace (* No push was possible, but there are still
+      			   subgoals somewhere: there must be a "}" to use. *)
+
+
+  let rec pop_until (prf : proof) bul : proof =
+    let prf', b = pop prf in
+    if bullet_eq bul b then prf'
+    else pop_until prf' bul
+
+  let put p bul =
+    try
+      if not (has_bullet bul p) then
+        (* bullet is not in use, so pushing it is always ok unless
+           no goal under focus. *)
+        push bul p
+      else
+        match suggest_bullet p with
+        | Suggest suggested_bullet when bullet_eq bul suggested_bullet
+            -> (* suggested_bullet is mandatory and you gave the right one *)
+          let p' = pop_until p bul in
+          push bul p'
+      (* the bullet you gave is in use but not the right one *)
+        | sugg -> raise (FailedBullet (bul,sugg))
+    with NoSuchGoals _ -> (* push went bad *)
+      raise (FailedBullet (bul,suggest_bullet p))
+
+  let strict = {
+    name = "Strict Subproofs";
+    put = put;
+    suggest = (fun prf -> suggest_on_solved_goal (suggest_bullet prf))
+
+  }
+  let _ = register_behavior strict
+end
+
+(* Current bullet behavior, controlled by the option *)
+let current_behavior = ref Strict.strict
+
+let _ =
+  Goptions.(declare_string_option {
+    optdepr = false;
+    optname = "bullet behavior";
+    optkey = ["Bullet";"Behavior"];
+    optread = begin fun () ->
+      (!current_behavior).name
+    end;
+    optwrite = begin fun n ->
+      current_behavior :=
+        try Hashtbl.find behaviors n
+        with Not_found ->
+          CErrors.user_err Pp.(str ("Unknown bullet behavior: \"" ^ n ^ "\"."))
+    end
+  })
+
+let put p b =
+  (!current_behavior).put p b
+
+let suggest p =
+  (!current_behavior).suggest p
+
+(**********************************************************)
+(*                                                        *)
+(*                     Default goal selector              *)
+(*                                                        *)
+(**********************************************************)
+
+
+(* Default goal selector: selector chosen when a tactic is applied
+   without an explicit selector. *)
+let default_goal_selector = ref (Vernacexpr.SelectNth 1)
+let get_default_goal_selector () = !default_goal_selector
+
+let pr_range_selector (i, j) =
+  if i = j then Pp.int i
+  else Pp.(int i ++ str "-" ++ int j)
+
+let pr_goal_selector = function
+  | Vernacexpr.SelectAll -> Pp.str "all"
+  | Vernacexpr.SelectNth i -> Pp.int i
+  | Vernacexpr.SelectList l ->
+    Pp.(str "["
+     ++ prlist_with_sep pr_comma pr_range_selector l
+     ++ str "]")
+  | Vernacexpr.SelectId id -> Names.Id.print id
+
+let parse_goal_selector = function
+  | "all" -> Vernacexpr.SelectAll
+  | i ->
+      let err_msg = "The default selector must be \"all\" or a natural number." in
+      begin try
+              let i = int_of_string i in
+              if i < 0 then CErrors.user_err Pp.(str err_msg);
+              Vernacexpr.SelectNth i
+        with Failure _ -> CErrors.user_err Pp.(str err_msg)
+      end
+
+let _ =
+  Goptions.(declare_string_option{optdepr = false;
+                                  optname = "default goal selector" ;
+                                  optkey = ["Default";"Goal";"Selector"] ;
+                                  optread = begin fun () ->
+                                            Pp.string_of_ppcmds
+                                              (pr_goal_selector !default_goal_selector)
+                                            end;
+                                  optwrite = begin fun n ->
+                                    default_goal_selector := parse_goal_selector n
+                                  end
+                                 })
+