From fca82378cd2824534383f1f5bc09d08fade1dc17 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 24 Apr 2018 18:21:49 +0200 Subject: [api] Move bullets and goals selectors to `proofs/` `Vernacexpr` lives conceptually higher than `proof`, however, datatypes for bullets and goal selectors are in `Vernacexpr`. In particular, we move: - `proof_bullet`: to `Proof_bullet` - `goal_selector`: to a new file `Goal_select` --- proofs/goal_select.ml | 68 +++++++++++++++++++++++++++++++++++++++++++++++ proofs/goal_select.mli | 26 ++++++++++++++++++ proofs/pfedit.ml | 14 +++++----- proofs/pfedit.mli | 2 +- proofs/proof_bullet.ml | 70 +++++++++---------------------------------------- proofs/proof_bullet.mli | 19 +++++++------- proofs/proof_global.ml | 1 + proofs/proofs.mllib | 1 + 8 files changed, 125 insertions(+), 76 deletions(-) create mode 100644 proofs/goal_select.ml create mode 100644 proofs/goal_select.mli (limited to 'proofs') diff --git a/proofs/goal_select.ml b/proofs/goal_select.ml new file mode 100644 index 0000000000..65a94a2c60 --- /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 *) +(* 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 0000000000..b1c5723885 --- /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 *) +(* Pp.t +val get_default_goal_selector : unit -> t diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 62a38fa325..03c0969faa 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 65cde3a3ae..805635dfa4 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 d6f7c0e93a..cc3e79f858 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 ffbaa0fac9..a09a7ec1d2 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 fc7c437e6b..842003bc86 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 058e839b47..197f71ca91 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 -- cgit v1.2.3