package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

doc/src/rocq-runtime.proofs/goal_select.ml.html

Source file goal_select.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \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
  | SelectList of Proofview.goal_range_selector list
  | SelectAll

let select_nth n = SelectList [NthSelector n]

let pr_id_selector id =
  Pp.(str "[" ++ Id.print id ++ str "]")

let pr_range_selector = let open Proofview in function
  | NthSelector i -> Pp.int i
  | RangeSelector (i, j) -> Pp.(int i ++ str "-" ++ int j)
  | IdSelector id -> pr_id_selector id

let pr_goal_selector = let open Pp in function
  | SelectAlreadyFocused -> str "!"
  | SelectAll -> str "all"
  | SelectList l -> prlist_with_sep pr_comma pr_range_selector l

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);
              select_nth i
        with Failure _ -> CErrors.user_err Pp.(str err_msg)
      end

(* Default goal selector: selector chosen when a tactic is applied
   without an explicit selector. *)
let { Goptions.get = get_default_goal_selector } =
  Goptions.declare_interpreted_string_option_and_ref
    parse_goal_selector
    (fun v -> Pp.string_of_ppcmds @@ pr_goal_selector v)
    ~key:["Default";"Goal";"Selector"]
    ~value:(select_nth 1)
    ()

(* Select a subset of the goals *)
let tclSELECT ?nosuchgoal g tac = match g with
  | SelectList [NthSelector i] -> Proofview.tclFOCUS ?nosuchgoal i i tac
  | SelectList [IdSelector id] -> Proofview.tclFOCUSID ?nosuchgoal id tac
  | SelectList l -> Proofview.tclFOCUSSELECTORLIST ?nosuchgoal l tac
  | SelectAll -> tac
  | SelectAlreadyFocused ->
    let open Proofview.Notations in
    Proofview.numgoals >>= fun n ->
    if n == 1 then tac
    else
      let e = CErrors.UserError
          Pp.(str "Expected a single focused goal but " ++
              int n ++ str " goals are focused.")
      in
      let info = Exninfo.reify () in
      Proofview.tclZERO ~info e