aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-07-19 16:22:48 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-07-19 16:22:48 +0200
commit4d4ec6a095d01b6117ac3682d8a7882b1a2520e7 (patch)
treed9ad4f412a3d3889ce869a4c0aecbc9dc098271a /proofs
parente273ff57ef82e81ab6b6309584a7d496ae4659c1 (diff)
parentab53757a3bf57ced503023f3cf9dea5b5503dfea (diff)
Merge PR #770: [proof] Move bullets to their own module.
Diffstat (limited to 'proofs')
-rw-r--r--proofs/proof_bullet.ml248
-rw-r--r--proofs/proof_bullet.mli53
-rw-r--r--proofs/proof_global.ml267
-rw-r--r--proofs/proof_global.mli46
-rw-r--r--proofs/proofs.mllib1
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