Merge PR #770: [proof] Move bullets to their own module.

5 files changed, 310 insertions, 305 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
+                                 })
+
diff --git a/proofs/proof_bullet.mli b/proofs/proof_bullet.mli
new file mode 100644
index 000000000..9ae521d3f
--- /dev/null
+++ b/proofs/proof_bullet.mli
@@ -0,0 +1,53 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(**********************************************************)
+(*                                                        *)
+(*                                 Bullets                *)
+(*                                                        *)
+(**********************************************************)
+
+open Proof
+
+type t = Vernacexpr.bullet
+
+(** A [behavior] is the data of a put function which
+    is called when a bullet prefixes a tactic, a suggest function
+    suggesting the right bullet to use on a given proof, together
+    with a name to identify the behavior. *)
+type behavior = {
+  name : string;
+  put : proof -> t -> proof;
+  suggest: proof -> Pp.t
+}
+
+(** A registered behavior can then be accessed in Coq
+    through the command [Set Bullet Behavior "name"].
+
+    Two modes are registered originally:
+    * "Strict Subproofs":
+      - If this bullet follows another one of its kind, defocuses then focuses
+        (which fails if the focused subproof is not complete).
+      - If it is the first bullet of its kind, then focuses a new subproof.
+    * "None": bullets don't do anything *)
+val register_behavior : behavior -> unit
+
+(** Handles focusing/defocusing with bullets:
+     *)
+val put : proof -> t -> proof
+val suggest : proof -> Pp.t
+
+(**********************************************************)
+(*                                                        *)
+(*                     Default goal selector              *)
+(*                                                        *)
+(**********************************************************)
+
+val pr_goal_selector : Vernacexpr.goal_selector -> Pp.std_ppcmds
+val get_default_goal_selector : unit -> Vernacexpr.goal_selector
+
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 703bdff64..52d6787d4 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -446,265 +446,6 @@ let set_terminator hook =
   | [] -> raise NoCurrentProof
   | p :: ps -> pstates := { p with terminator = CEphemeron.create hook } :: ps
 
-
-
-
-(**********************************************************)
-(*                                                        *)
-(*                                 Bullets                *)
-(*                                                        *)
-(**********************************************************)
-
-module Bullet = struct
-
-  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 -> str (String.make n '-')
-    | Vernacexpr.Star n -> str (String.make n '*')
-    | Vernacexpr.Plus n -> str (String.make n '+')
-
-
-  type behavior = {
-    name : string;
-    put : Proof.proof -> t -> Proof.proof;
-    suggest: Proof.proof -> std_ppcmds
-  }
-
-  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 _ -> 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 -> str"Try unfocusing with \"}\"."
-      | NoBulletInUse -> mt ()
-      | ProofFinished -> mt ()
-      | Suggest b -> str"Focus next goal with bullet " ++ pr_bullet b ++ str"."
-      | Unfinished b -> str"The current bullet " ++ pr_bullet b ++ str" is unfinished."
-
-    (* give always a message. *)
-    let suggest_on_error sugg =
-      match sugg with
-      | NeedClosingBrace -> str"Try unfocusing with \"}\"."
-      | NoBulletInUse -> assert false (* This should never raise an error. *)
-      | ProofFinished -> str"No more subgoals."
-      | Suggest b -> str"Expecting " ++ pr_bullet b ++ str"."
-      | Unfinished b -> 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 = str"Wrong bullet " ++ pr_bullet b ++ str": " in
-	  CErrors.user_err ~hdr:"Focus" (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 = (Proof.new_focus_kind () : t list Proof.focus_kind)
-    let bullet_cond = Proof.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 Proof.is_last_focus bullet_kind pr then
-	Proof.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::_ -> Proof.unfocus bullet_kind pr () , b
-      | _ -> assert false
-
-    let push (b:t) pr =
-      Proof.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.proof): suggestion =
-      if Proof.is_done prf then ProofFinished
-      else if not (Proof.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.proof) bul: Proof.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 Proof.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
-end
-
-
-let _ =
-  let hook n =
-    let prf = give_me_the_proof () in
-    (Bullet.suggest prf) in
-  Proofview.set_nosuchgoals_hook hook
-
-
-(**********************************************************)
-(*                                                        *)
-(*                     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 int i
-  else int i ++ str "-" ++ int j
-
-let pr_goal_selector = function
-  | Vernacexpr.SelectAll -> str "all"
-  | Vernacexpr.SelectNth i -> int i
-  | Vernacexpr.SelectList l ->
-     str "["
-     ++ prlist_with_sep pr_comma pr_range_selector l
-     ++ str "]"
-  | Vernacexpr.SelectId id -> 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 () ->
-                                            string_of_ppcmds
-                                              (pr_goal_selector !default_goal_selector)
-                                            end;
-                                  optwrite = begin fun n ->
-                                    default_goal_selector := parse_goal_selector n
-                                  end
-                                 })
-
-
 module V82 = struct
   let get_current_initial_conclusions () =
   let { pid; strength; proof } = cur_pstate () in
@@ -733,3 +474,11 @@ let update_global_env () =
        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
          (p, ())))
+
+(* XXX: Bullet hook, should be really moved elsewhere *)
+let _ =
+  let hook n =
+    let prf = give_me_the_proof () in
+    (Proof_bullet.suggest prf) in
+  Proofview.set_nosuchgoals_hook hook
+
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 2c3938975..52f5f7404 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -121,52 +121,6 @@ val get_used_variables : unit -> Context.Named.t option
 
 val get_universe_binders : unit -> universe_binders option
 
-(**********************************************************)
-(*                                                        *)
-(*                                 Bullets                *)
-(*                                                        *)
-(**********************************************************)
-
-module Bullet : sig
-  type t = Vernacexpr.bullet
-
-  (** A [behavior] is the data of a put function which
-      is called when a bullet prefixes a tactic, a suggest function
-      suggesting the right bullet to use on a given proof, together
-      with a name to identify the behavior. *)
-  type behavior = {
-    name : string;
-    put : Proof.proof -> t -> Proof.proof;
-    suggest: Proof.proof -> Pp.std_ppcmds
-  }
-
-  (** A registered behavior can then be accessed in Coq
-      through the command [Set Bullet Behavior "name"].
-
-      Two modes are registered originally:
-      * "Strict Subproofs":
-        - If this bullet follows another one of its kind, defocuses then focuses
-          (which fails if the focused subproof is not complete).
-        - If it is the first bullet of its kind, then focuses a new subproof.
-      * "None": bullets don't do anything *)
-  val register_behavior : behavior -> unit
-
-  (** Handles focusing/defocusing with bullets:
-       *)
-  val put : Proof.proof -> t -> Proof.proof
-  val suggest : Proof.proof -> Pp.std_ppcmds
-end
-
-
-(**********************************************************)
-(*                                                        *)
-(*                     Default goal selector              *)
-(*                                                        *)
-(**********************************************************)
-
-val pr_goal_selector : Vernacexpr.goal_selector -> Pp.std_ppcmds
-val get_default_goal_selector : unit -> Vernacexpr.goal_selector
-
 module V82 : sig
   val get_current_initial_conclusions : unit -> Names.Id.t *(EConstr.types list *
   Decl_kinds.goal_kind)
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 804a54360..0ea2bd66b 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -5,6 +5,7 @@ Proof_using
 Logic
 Refine
 Proof
+Proof_bullet
 Proof_global
 Redexpr
 Refiner