aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacticals.mli
blob: cfdc2cffd4f93fa154de79c6713f214326178d73 (plain)
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
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open Pp
open Names
open Term
open Tacmach
open Proof_type
open Tacexpr
open Locus
open Misctypes

(** Tacticals i.e. functions from tactics to tactics. *)

val tclIDTAC         : tactic
val tclIDTAC_MESSAGE : std_ppcmds -> tactic
val tclORELSE0       : tactic -> tactic -> tactic
val tclORELSE        : tactic -> tactic -> tactic
val tclTHEN          : tactic -> tactic -> tactic
val tclTHENSEQ       : tactic list -> tactic
val tclTHENLIST      : tactic list -> tactic
val tclTHEN_i        : tactic -> (int -> tactic) -> tactic
val tclTHENFIRST     : tactic -> tactic -> tactic
val tclTHENLAST      : tactic -> tactic -> tactic
val tclTHENS         : tactic -> tactic list -> tactic
val tclTHENSV        : tactic -> tactic array -> tactic
val tclTHENSLASTn    : tactic -> tactic -> tactic array -> tactic
val tclTHENLASTn     : tactic -> tactic array -> tactic
val tclTHENSFIRSTn   : tactic -> tactic array -> tactic -> tactic
val tclTHENFIRSTn    : tactic -> tactic array -> tactic
val tclREPEAT        : tactic -> tactic
val tclREPEAT_MAIN   : tactic -> tactic
val tclFIRST         : tactic list -> tactic
val tclSOLVE         : tactic list -> tactic
val tclTRY           : tactic -> tactic
val tclCOMPLETE      : tactic -> tactic
val tclAT_LEAST_ONCE : tactic -> tactic
val tclFAIL          : int -> std_ppcmds -> tactic
val tclFAIL_lazy     : int -> std_ppcmds Lazy.t -> tactic
val tclDO            : int -> tactic -> tactic
val tclWEAK_PROGRESS : tactic -> tactic
val tclPROGRESS      : tactic -> tactic
val tclSHOWHYPS      : tactic -> tactic
val tclNOTSAMEGOAL   : tactic -> tactic
val tclTHENTRY       : tactic -> tactic -> tactic
val tclMAP           : ('a -> tactic) -> 'a list -> tactic

val tclIFTHENELSE        : tactic -> tactic -> tactic -> tactic
val tclIFTHENSELSE       : tactic -> tactic list -> tactic -> tactic
val tclIFTHENSVELSE      : tactic -> tactic array -> tactic -> tactic
val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic

(** {6 Tacticals applying to hypotheses } *)

val onNthHypId       : int -> (Id.t -> tactic) -> tactic
val onNthHyp         : int -> (constr -> tactic) -> tactic
val onNthDecl        : int -> (Context.Named.Declaration.t -> tactic) -> tactic
val onLastHypId      : (Id.t -> tactic) -> tactic
val onLastHyp        : (constr -> tactic) -> tactic
val onLastDecl       : (Context.Named.Declaration.t -> tactic) -> tactic
val onNLastHypsId    : int -> (Id.t list -> tactic) -> tactic
val onNLastHyps      : int -> (constr list -> tactic) -> tactic
val onNLastDecls     : int -> (Context.Named.t -> tactic) -> tactic

val lastHypId   : goal sigma -> Id.t
val lastHyp     : goal sigma -> constr
val lastDecl    : goal sigma -> Context.Named.Declaration.t
val nLastHypsId : int -> goal sigma -> Id.t list
val nLastHyps   : int -> goal sigma -> constr list
val nLastDecls  : int -> goal sigma -> Context.Named.t

val afterHyp    : Id.t -> goal sigma -> Context.Named.t

val ifOnHyp     : (Id.t * types -> bool) ->
                  (Id.t -> tactic) -> (Id.t -> tactic) ->
		   Id.t -> tactic

val onHyps      : (goal sigma -> Context.Named.t) ->
                  (Context.Named.t -> tactic) -> tactic

(** {6 Tacticals applying to goal components } *)

(** A [clause] denotes occurrences and hypotheses in a
   goal; in particular, it can abstractly refer to the set of
   hypotheses independently of the effective contents of the current goal *)

val onAllHyps           : (Id.t -> tactic) -> tactic
val onAllHypsAndConcl   : (Id.t option -> tactic) -> tactic

val onClause   : (Id.t option -> tactic) -> clause -> tactic
val onClauseLR : (Id.t option -> tactic) -> clause -> tactic

(** {6 Elimination tacticals. } *)

type branch_args = {
  ity        : pinductive;  (** the type we were eliminating on *)
  largs      : constr list; (** its arguments *)
  branchnum  : int;         (** the branch number *)
  pred       : constr;      (** the predicate we used *)
  nassums    : int;         (** number of assumptions/letin to be introduced *)
  branchsign : bool list;   (** the signature of the branch.
                                true=assumption, false=let-in *)
  branchnames : intro_patterns}

type branch_assumptions = {
  ba        : branch_args;       (** the branch args *)
  assums    : Context.Named.t}   (** the list of assumptions introduced *)

(** [get_and_check_or_and_pattern loc pats branchsign] returns an appropriate
   error message if |pats| <> |branchsign|; extends them if no pattern is given
   for let-ins in the case of a conjunctive pattern *)
val get_and_check_or_and_pattern :
  Loc.t -> delayed_open_constr or_and_intro_pattern_expr ->
  bool list array -> intro_patterns array

(** Tolerate "[]" to mean a disjunctive pattern of any length *)
val fix_empty_or_and_pattern : int -> 
  delayed_open_constr or_and_intro_pattern_expr ->
  delayed_open_constr or_and_intro_pattern_expr

val compute_constructor_signatures : rec_flag -> pinductive -> bool list array

(** Useful for [as intro_pattern] modifier *)
val compute_induction_names :
  bool list array -> or_and_intro_pattern option -> intro_patterns array

val elimination_sort_of_goal : goal sigma -> sorts_family
val elimination_sort_of_hyp  : Id.t -> goal sigma -> sorts_family
val elimination_sort_of_clause : Id.t option -> goal sigma -> sorts_family

val pf_with_evars :  (goal sigma -> Evd.evar_map * 'a) -> ('a -> tactic) -> tactic
val pf_constr_of_global : Globnames.global_reference -> (constr -> tactic) -> tactic

val elim_on_ba : (branch_assumptions -> tactic) -> branch_args  -> tactic
val case_on_ba : (branch_assumptions -> tactic) -> branch_args  -> tactic

(** Tacticals defined directly in term of Proofview *)

(** The tacticals in the module [New] are the tactical of Ltac. Their
    semantics is an extension of the tacticals in this file for the
    multi-goal backtracking tactics. They do not have the same
    semantics as the similarly named tacticals in [Proofview]. The
    tactical of [Proofview] are used in the definition of the
    tacticals of [Tacticals.New], but they are more atomic. In
    particular [Tacticals.New.tclORELSE] sees lack of progress as a
    failure, whereas [Proofview.tclORELSE] doesn't. Additionally every
    tactic which can catch failure ([tclOR], [tclORELSE], [tclTRY],
    [tclREPEAt], etc…) are run into each goal independently (failures
    and backtracks are localised to a given goal). *)
module New : sig
  open Proofview

  (** [catch_failerror e] fails and decreases the level if [e] is an
      Ltac error with level more than 0. Otherwise succeeds. *)
  val catch_failerror : Util.iexn -> unit tactic

  val tclIDTAC : unit tactic
  val tclTHEN : unit tactic -> unit tactic -> unit tactic
  (* [tclFAIL n msg] fails with [msg] as an error message at level [n]
     (meaning that it will jump over [n] error catching tacticals FROM
     THIS MODULE. *)
  val tclFAIL : int -> Pp.std_ppcmds -> 'a tactic

  val tclZEROMSG : ?loc:Loc.t -> Pp.std_ppcmds -> 'a tactic
  (** Fail with a [User_Error] containing the given message. *)

  val tclOR : unit tactic -> unit tactic -> unit tactic
  val tclORD : unit tactic -> (unit -> unit tactic) -> unit tactic
  (** Like {!tclOR} but accepts a delayed tactic as a second argument
      in the form of a function which will be run only in case of
      backtracking. *)

  val tclONCE : unit tactic -> unit tactic
  val tclEXACTLY_ONCE : unit tactic -> unit tactic

  val tclIFCATCH :
             unit tactic  ->
    (unit -> unit tactic) ->
    (unit -> unit tactic) -> unit tactic

  val tclORELSE0 : unit tactic -> unit tactic -> unit tactic
  val tclORELSE  : unit tactic -> unit tactic -> unit tactic

  (** [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|]
      gls] applies the tactic [tac1] to [gls] then, applies [t1], ...,
      [tn] to the first [n] resulting subgoals, [t'1], ..., [t'm] to the
      last [m] subgoals and [tac2] to the rest of the subgoals in the
      middle. Raises an error if the number of resulting subgoals is
      strictly less than [n+m] *)
  val tclTHENS3PARTS     : unit tactic -> unit tactic array -> unit tactic -> unit tactic array -> unit tactic
  val tclTHENSFIRSTn : unit tactic -> unit tactic array -> unit tactic -> unit tactic
  val tclTHENFIRSTn : unit tactic -> unit tactic array -> unit tactic
  (** [tclTHENFIRST tac1 tac2 gls] applies the tactic [tac1] to [gls]
      and [tac2] to the first resulting subgoal *)
  val tclTHENFIRST : unit tactic -> unit tactic -> unit tactic
  val tclTHENLASTn : unit tactic -> unit tactic array -> unit tactic
  val tclTHENLAST  : unit tactic -> unit tactic -> unit tactic
  (* [tclTHENS t l = t <*> tclDISPATCH l] *)
  val tclTHENS : unit tactic -> unit tactic list -> unit tactic
  (* [tclTHENLIST [t1;…;tn]] is [t1<*>…<*>tn] *)
  val tclTHENLIST : unit tactic list -> unit tactic

  (** [tclMAP f [x1..xn]] builds [(f x1);(f x2);...(f xn)] *)
  val tclMAP : ('a -> unit tactic) -> 'a list -> unit tactic

  val tclTRY : unit tactic -> unit tactic
  val tclFIRST : unit tactic list -> unit tactic
  val tclIFTHENELSE : unit tactic -> unit tactic -> unit tactic -> unit tactic
  val tclIFTHENSVELSE : unit tactic -> unit tactic array -> unit tactic -> unit tactic
  val tclIFTHENTRYELSEMUST : unit tactic -> unit tactic -> unit tactic

  val tclDO : int -> unit tactic -> unit tactic
  val tclREPEAT : unit tactic -> unit tactic
  (* Repeat on the first subgoal (no failure if no more subgoal) *)
  val tclREPEAT_MAIN : unit tactic -> unit tactic
  val tclCOMPLETE : 'a tactic -> 'a tactic
  val tclSOLVE : unit tactic list -> unit tactic
  val tclPROGRESS : unit tactic -> unit tactic
  val tclSELECT : goal_selector -> '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 tclTIMEOUT : int -> unit tactic -> unit tactic
  val tclTIME : string option -> 'a tactic -> 'a tactic

  val nLastDecls  : ([ `NF ], 'r) Proofview.Goal.t -> int -> Context.Named.t

  val ifOnHyp     : (identifier * types -> bool) ->
    (identifier -> unit Proofview.tactic) -> (identifier -> unit Proofview.tactic) ->
    identifier -> unit Proofview.tactic

  val onNthHypId : int -> (identifier -> unit tactic) -> unit tactic
  val onLastHypId      : (identifier -> unit tactic) -> unit tactic
  val onLastHyp        : (constr -> unit tactic) -> unit tactic
  val onLastDecl       : (Context.Named.Declaration.t -> unit tactic) -> unit tactic

  val onHyps      : ([ `NF ], Context.Named.t) Proofview.Goal.enter ->
                    (Context.Named.t -> unit tactic) -> unit tactic
  val afterHyp    : Id.t -> (Context.Named.t -> unit tactic) -> unit tactic

  val tryAllHyps          : (identifier -> unit tactic) -> unit tactic
  val tryAllHypsAndConcl  : (identifier option -> unit tactic) -> unit tactic
  val onClause   : (identifier option -> unit tactic) -> clause -> unit tactic

  val elimination_sort_of_goal : ('a, 'r) Proofview.Goal.t -> sorts_family
  val elimination_sort_of_hyp  : Id.t -> ('a, 'r) Proofview.Goal.t -> sorts_family
  val elimination_sort_of_clause : Id.t option -> ('a, 'r) Proofview.Goal.t -> sorts_family

  val elimination_then :
    (branch_args -> unit Proofview.tactic) ->
    constr -> unit Proofview.tactic

  val case_then_using :
    or_and_intro_pattern option -> (branch_args -> unit Proofview.tactic) ->
    constr option -> pinductive -> Term.constr * Term.types -> unit Proofview.tactic

  val case_nodep_then_using :
    or_and_intro_pattern option -> (branch_args -> unit Proofview.tactic) ->
    constr option -> pinductive -> Term.constr * Term.types -> unit Proofview.tactic

  val elim_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args  -> unit Proofview.tactic
  val case_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args  -> unit Proofview.tactic

  val pf_constr_of_global : Globnames.global_reference -> (constr -> unit Proofview.tactic) -> unit Proofview.tactic
end