diff options
Diffstat (limited to 'proofs')
-rw-r--r-- | proofs/goal_select.ml | 68 | ||||
-rw-r--r-- | proofs/goal_select.mli | 26 | ||||
-rw-r--r-- | proofs/pfedit.ml | 14 | ||||
-rw-r--r-- | proofs/pfedit.mli | 2 | ||||
-rw-r--r-- | proofs/proof_bullet.ml | 70 | ||||
-rw-r--r-- | proofs/proof_bullet.mli | 19 | ||||
-rw-r--r-- | proofs/proof_global.ml | 1 | ||||
-rw-r--r-- | proofs/proofs.mllib | 1 |
8 files changed, 125 insertions, 76 deletions
diff --git a/proofs/goal_select.ml b/proofs/goal_select.ml new file mode 100644 index 000000000..65a94a2c6 --- /dev/null +++ b/proofs/goal_select.ml @@ -0,0 +1,68 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names + +(* spiwack: I'm choosing, for now, to have [goal_selector] be a + different type than [goal_reference] mostly because if it makes sense + to print a goal that is out of focus (or already solved) it doesn't + make sense to apply a tactic to it. Hence it the types may look very + similar, they do not seem to mean the same thing. *) +type t = + | SelectAlreadyFocused + | SelectNth of int + | SelectList of (int * int) list + | SelectId of Id.t + | SelectAll + +(* Default goal selector: selector chosen when a tactic is applied + without an explicit selector. *) +let default_goal_selector = ref (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 + | SelectAlreadyFocused -> Pp.str "!" + | SelectAll -> Pp.str "all" + | SelectNth i -> Pp.int i + | SelectList l -> + Pp.(str "[" + ++ prlist_with_sep pr_comma pr_range_selector l + ++ str "]") + | SelectId id -> Names.Id.print id + +let parse_goal_selector = function + | "!" -> SelectAlreadyFocused + | "all" -> 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); + SelectNth i + with Failure _ -> CErrors.user_err Pp.(str err_msg) + end + +let _ = let open Goptions in + 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/goal_select.mli b/proofs/goal_select.mli new file mode 100644 index 000000000..b1c572388 --- /dev/null +++ b/proofs/goal_select.mli @@ -0,0 +1,26 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names + +(* spiwack: I'm choosing, for now, to have [goal_selector] be a + different type than [goal_reference] mostly because if it makes sense + to print a goal that is out of focus (or already solved) it doesn't + make sense to apply a tactic to it. Hence it the types may look very + similar, they do not seem to mean the same thing. *) +type t = + | SelectAlreadyFocused + | SelectNth of int + | SelectList of (int * int) list + | SelectId of Id.t + | SelectAll + +val pr_goal_selector : t -> Pp.t +val get_default_goal_selector : unit -> t diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 62a38fa32..03c0969fa 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -100,8 +100,8 @@ let solve ?with_end_tac gi info_lvl tac pr = | None -> tac | Some _ -> Proofview.Trace.record_info_trace tac in - let tac = match gi with - | Vernacexpr.SelectAlreadyFocused -> + let tac = let open Goal_select in match gi with + | SelectAlreadyFocused -> let open Proofview.Notations in Proofview.numgoals >>= fun n -> if n == 1 then tac @@ -113,10 +113,10 @@ let solve ?with_end_tac gi info_lvl tac pr = in Proofview.tclZERO e - | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i tac - | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l tac - | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id tac - | Vernacexpr.SelectAll -> tac + | SelectNth i -> Proofview.tclFOCUS i i tac + | SelectList l -> Proofview.tclFOCUSLIST l tac + | SelectId id -> Proofview.tclFOCUSID id tac + | SelectAll -> tac in let tac = if use_unification_heuristics () then @@ -133,7 +133,7 @@ let solve ?with_end_tac gi info_lvl tac pr = with Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof") -let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) None tac) +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) diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 65cde3a3a..805635dfa 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -75,7 +75,7 @@ val current_proof_statement : tac] applies [tac] to all subgoals. *) val solve : ?with_end_tac:unit Proofview.tactic -> - Vernacexpr.goal_selector -> int option -> unit Proofview.tactic -> + Goal_select.t -> int option -> unit Proofview.tactic -> Proof.t -> Proof.t * bool (** [by tac] applies tactic [tac] to the 1st subgoal of the current diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml index d6f7c0e93..cc3e79f85 100644 --- a/proofs/proof_bullet.ml +++ b/proofs/proof_bullet.ml @@ -10,19 +10,22 @@ open Proof -type t = Vernacexpr.bullet +type t = + | Dash of int + | Star of int + | Plus of int 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 +| Dash n1, Dash n2 -> n1 = n2 +| Star n1, Star n2 -> n1 = n2 +| Plus n1, 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 '+')) + | Dash n -> Pp.(str (String.make n '-')) + | Star n -> Pp.(str (String.make n '*')) + | Plus n -> Pp.(str (String.make n '+')) type behavior = { @@ -195,54 +198,5 @@ let 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.SelectAlreadyFocused -> Pp.str "!" - | 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 - | "!" -> Vernacexpr.SelectAlreadyFocused - | "all" -> Vernacexpr.SelectAll - | i -> - let err_msg = "The default selector must be \"all\" or \"!\" 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 - }) - +let pr_goal_selector = Goal_select.pr_goal_selector +let get_default_goal_selector = Goal_select.get_default_goal_selector diff --git a/proofs/proof_bullet.mli b/proofs/proof_bullet.mli index ffbaa0fac..a09a7ec1d 100644 --- a/proofs/proof_bullet.mli +++ b/proofs/proof_bullet.mli @@ -14,7 +14,10 @@ (* *) (**********************************************************) -type t = Vernacexpr.bullet +type t = + | Dash of int + | Star of int + | Plus of int (** A [behavior] is the data of a put function which is called when a bullet prefixes a tactic, a suggest function @@ -42,12 +45,8 @@ val register_behavior : behavior -> unit val put : Proof.t -> t -> Proof.t val suggest : Proof.t -> Pp.t -(**********************************************************) -(* *) -(* Default goal selector *) -(* *) -(**********************************************************) - -val pr_goal_selector : Vernacexpr.goal_selector -> Pp.t -val get_default_goal_selector : unit -> Vernacexpr.goal_selector - +(** Deprecated *) +val pr_goal_selector : Goal_select.t -> Pp.t +[@@ocaml.deprecated "Please use [Goal_select.pr_goal_selector]"] +val get_default_goal_selector : unit -> Goal_select.t +[@@ocaml.deprecated "Please use [Goal_select.get_default_goal_selector]"] diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index fc7c437e6..842003bc8 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -83,6 +83,7 @@ type proof_ending = | Proved of Vernacexpr.opacity_flag * Misctypes.lident option * proof_object + type proof_terminator = proof_ending -> unit type closed_proof = proof_object * proof_terminator diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 058e839b4..197f71ca9 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -5,6 +5,7 @@ Proof_type Logic Refine Proof +Goal_select Proof_bullet Proof_global Redexpr |