Factorize goal selector handling

As a bonus ltac2 can produce bullet suggestions.

8 files changed, 33 insertions, 48 deletions

diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 54d7c310aa..da95869abb 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1180,7 +1180,7 @@ and eval_tactic_ist ist tac : unit Proofview.tactic = match tac with
   | TacSolve l -> Tacticals.New.tclSOLVE (List.map (interp_tactic ist) l)
   | TacComplete tac -> Tacticals.New.tclCOMPLETE (interp_tactic ist tac)
   | TacArg {CAst.loc} -> Ftactic.run (val_interp (ensure_loc loc ist) tac) (fun v -> tactic_of_value ist v)
-  | TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac)
+  | TacSelect (sel, tac) -> Goal_select.tclSELECT sel (interp_tactic ist tac)
   (* For extensions *)
   | TacAlias {loc; v=(s,l)} ->
       let alias = Tacenv.interp_alias s in
diff --git a/proofs/goal_select.ml b/proofs/goal_select.ml
index e847535aaf..68646c93c9 100644
--- a/proofs/goal_select.ml
+++ b/proofs/goal_select.ml
@@ -57,3 +57,22 @@ let get_default_goal_selector =
     ~value:(SelectNth 1)
     parse_goal_selector
     (fun v -> Pp.string_of_ppcmds @@ pr_goal_selector v)
+
+(* Select a subset of the goals *)
+let tclSELECT ?nosuchgoal g tac = match g with
+  | SelectNth i -> Proofview.tclFOCUS ?nosuchgoal i i tac
+  | SelectList l -> Proofview.tclFOCUSLIST ?nosuchgoal l tac
+  | SelectId id -> Proofview.tclFOCUSID ?nosuchgoal id tac
+  | SelectAll -> tac
+  | SelectAlreadyFocused ->
+    let open Proofview.Notations in
+    Proofview.numgoals >>= fun n ->
+    if n == 1 then tac
+    else
+      let e = CErrors.UserError
+          (None,
+           Pp.(str "Expected a single focused goal but " ++
+               int n ++ str " goals are focused."))
+      in
+      let info = Exninfo.reify () in
+      Proofview.tclZERO ~info e
diff --git a/proofs/goal_select.mli b/proofs/goal_select.mli
index 977392baa6..c6726300f0 100644
--- a/proofs/goal_select.mli
+++ b/proofs/goal_select.mli
@@ -24,3 +24,5 @@ type t =
 
 val pr_goal_selector : t -> Pp.t
 val get_default_goal_selector : unit -> t
+
+val tclSELECT : ?nosuchgoal:'a Proofview.tactic -> t -> 'a Proofview.tactic -> 'a Proofview.tactic
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 50a0e63700..e535536472 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -538,25 +538,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
       let info = Exninfo.reify () in
       Proofview.tclZERO ~info (SuggestNoSuchGoals (1,pr))
     in
-    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
-        else
-          let e = CErrors.UserError
-              (None,
-               Pp.(str "Expected a single focused goal but " ++
-                   int n ++ str " goals are focused."))
-          in
-          let info = Exninfo.reify () in
-          Proofview.tclZERO ~info e
-
-      | SelectNth i -> Proofview.tclFOCUS ~nosuchgoal i i tac
-      | SelectList l -> Proofview.tclFOCUSLIST ~nosuchgoal l tac
-      | SelectId id -> Proofview.tclFOCUSID ~nosuchgoal id tac
-      | SelectAll -> tac
-    in
+    let tac = Goal_select.tclSELECT ~nosuchgoal gi tac in
     let tac =
       if use_unification_heuristics () then
         Proofview.tclTHEN tac Refine.solve_constraints
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 5f19c1bb09..43cde83e58 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -2,9 +2,9 @@ Miscprint
 Goal
 Evar_refiner
 Refine
+Goal_select
 Proof
 Logic
-Goal_select
 Proof_bullet
 Tacmach
 Clenv
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 68afd9a128..2d69047d1e 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -683,15 +683,6 @@ module New = struct
   let tclPROGRESS t =
     Proofview.tclINDEPENDENT (Proofview.tclPROGRESS t)
 
-  (* Select a subset of the goals *)
-  let tclSELECT = let open Goal_select in function
-    | SelectNth i -> Proofview.tclFOCUS i i
-    | SelectList l -> Proofview.tclFOCUSLIST l
-    | SelectId id -> Proofview.tclFOCUSID id
-    | SelectAll -> anomaly ~label:"tclSELECT" Pp.(str "SelectAll not allowed here")
-    | SelectAlreadyFocused ->
-      anomaly ~label:"tclSELECT" Pp.(str "SelectAlreadyFocused not allowed here")
-
   (* Check that holes in arguments have been resolved *)
 
   let check_evars env sigma extsigma origsigma =
@@ -905,4 +896,6 @@ module New = struct
       let (sigma, t) = Typing.type_of ?refresh env sigma c in
       Proofview.Unsafe.tclEVARS sigma <*> tac sigma t)
 
+  let tclSELECT = Goal_select.tclSELECT
+
 end
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 19d08dcc36..c09d268c40 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -206,7 +206,6 @@ module New : sig
   val tclCOMPLETE : 'a tactic -> 'a tactic
   val tclSOLVE : unit tactic list -> unit tactic
   val tclPROGRESS : unit tactic -> unit tactic
-  val tclSELECT : Goal_select.t -> 'a tactic -> 'a tactic
   val tclWITHHOLES : bool -> 'a tactic -> Evd.evar_map -> 'a tactic
   val tclDELAYEDWITHHOLES : bool -> 'a delayed_open -> ('a -> unit tactic) -> unit tactic
   val tclMAPDELAYEDWITHHOLES : bool -> 'a delayed_open list -> ('a -> unit tactic) -> unit tactic
@@ -250,4 +249,7 @@ module New : sig
   val pf_constr_of_global : GlobRef.t -> constr Proofview.tactic
 
   val tclTYPEOFTHEN : ?refresh:bool -> constr -> (evar_map -> types -> unit Proofview.tactic) -> unit Proofview.tactic
+
+  val tclSELECT : ?nosuchgoal:'a tactic -> Goal_select.t -> 'a tactic -> 'a tactic
+  [@@ocaml.deprecated "Use [Goal_select.tclSELECT]"]
 end
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index faa1e74728..5ddf56402f 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -811,24 +811,11 @@ let perform_eval ~pstate e =
       Goal_select.get_default_goal_selector (),
       Declare.Proof.get pstate
   in
-  let v = match selector with
-  | Goal_select.SelectNth i -> Proofview.tclFOCUS i i v
-  | Goal_select.SelectList l -> Proofview.tclFOCUSLIST l v
-  | Goal_select.SelectId id -> Proofview.tclFOCUSID id v
-  | Goal_select.SelectAll -> v
-  | Goal_select.SelectAlreadyFocused ->
-    let open Proofview.Notations in
-    Proofview.numgoals >>= fun n ->
-    if Int.equal n 1 then v
-    else
-      let e = CErrors.UserError
-          (None,
-            Pp.(str "Expected a single focused goal but " ++
-                int n ++ str " goals are focused."))
-      in
-      let info = Exninfo.reify () in
-      Proofview.tclZERO ~info e
+  let nosuchgoal =
+    let info = Exninfo.reify () in
+    Proofview.tclZERO ~info (Proof.SuggestNoSuchGoals (1,proof))
   in
+  let v = Goal_select.tclSELECT ~nosuchgoal selector v in
   let (proof, _, ans) = Proof.run_tactic (Global.env ()) v proof in
   let { Proof.sigma } = Proof.data proof in
   let name = int_name () in