aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf/tacexpr.mli
blob: 6c5e4406436aa2427aca30cf55629483f3c4fabd (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
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
(************************************************************************)
(*  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 Loc
open Names
open Constrexpr
open Libnames
open Nametab
open Genredexpr
open Genarg
open Pattern
open Misctypes
open Locus

type direction_flag = bool (* true = Left-to-right    false = right-to-right *)
type lazy_flag =
  | General (* returns all possible successes *)
  | Select  (* returns all successes of the first matching branch *)
  | Once    (* returns the first success in a maching branch
               (not necessarily the first) *)
type global_flag = (* [gfail] or [fail] *)
  | TacGlobal
  | TacLocal
type evars_flag = bool     (* true = pose evars       false = fail on evars *)
type rec_flag = bool       (* true = recursive        false = not recursive *)
type advanced_flag = bool  (* true = advanced         false = basic *)
type letin_flag = bool     (* true = use local def    false = use Leibniz *)
type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)

type debug = Debug | Info | Off (* for trivial / auto / eauto ... *)

type 'a core_induction_arg =
  | ElimOnConstr of 'a
  | ElimOnIdent of Id.t located
  | ElimOnAnonHyp of int

type 'a induction_arg =
  clear_flag * 'a core_induction_arg

type inversion_kind =
  | SimpleInversion
  | FullInversion
  | FullInversionClear

type ('c,'d,'id) inversion_strength =
  | NonDepInversion of
      inversion_kind * 'id list * 'd or_and_intro_pattern_expr located or_var option
  | DepInversion of
      inversion_kind * 'c option * 'd or_and_intro_pattern_expr located or_var option
  | InversionUsing of 'c * 'id list

type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b

type 'id message_token =
  | MsgString of string
  | MsgInt of int
  | MsgIdent of 'id

type ('dconstr,'id) induction_clause =
    'dconstr with_bindings induction_arg *
    (intro_pattern_naming_expr located option (* eqn:... *)
    * 'dconstr or_and_intro_pattern_expr located or_var option) (* as ... *)
    * 'id clause_expr option (* in ... *)

type ('constr,'dconstr,'id) induction_clause_list =
    ('dconstr,'id) induction_clause list
    * 'constr with_bindings option (* using ... *)

type 'a with_bindings_arg = clear_flag * 'a with_bindings

type multi =
  | Precisely of int
  | UpTo of int
  | RepeatStar
  | RepeatPlus

(* Type of patterns *)
type 'a match_pattern =
  | Term of 'a
  | Subterm of bool * Id.t option * 'a

(* Type of hypotheses for a Match Context rule *)
type 'a match_context_hyps =
  | Hyp of Name.t located * 'a match_pattern
  | Def of Name.t located * 'a match_pattern * 'a match_pattern

(* Type of a Match rule for Match Context and Match *)
type ('a,'t) match_rule =
  | Pat of 'a match_context_hyps list * 'a match_pattern * 't
  | All of 't

(** Extension indentifiers for the TACTIC EXTEND mechanism. *)
type ml_tactic_name = {
  (** Name of the plugin where the tactic is defined, typically coming from a
      DECLARE PLUGIN statement in the source. *)
  mltac_plugin : string;
  (** Name of the tactic entry where the tactic is defined, typically found
      after the TACTIC EXTEND statement in the source. *)
  mltac_tactic : string;
}

(** Composite types *)

(** In globalize tactics, we need to keep the initial [constr_expr] to recompute
   in the environment by the effective calls to Intro, Inversion, etc 
   The [constr_expr] field is [None] in TacDef though *)
type glob_constr_and_expr = Glob_term.glob_constr * constr_expr option

type open_constr_expr = unit * constr_expr
type open_glob_constr = unit * glob_constr_and_expr

type binding_bound_vars = Id.Set.t
type glob_constr_pattern_and_expr = glob_constr_and_expr * constr_pattern

type delayed_open_constr_with_bindings =
    Environ.env -> Evd.evar_map -> Evd.evar_map * Term.constr with_bindings

type delayed_open_constr =
    Environ.env -> Evd.evar_map -> Evd.evar_map * Term.constr

type intro_pattern = delayed_open_constr intro_pattern_expr located
type intro_patterns = delayed_open_constr intro_pattern_expr located list
type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr located
type intro_pattern_naming = intro_pattern_naming_expr located

(** Generic expressions for atomic tactics *)

type 'a gen_atomic_tactic_expr =
  (* Basic tactics *)
  | TacIntroPattern of 'dtrm intro_pattern_expr located list
  | TacIntroMove of Id.t option * 'nam move_location
  | TacExact of 'trm
  | TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list *
      ('nam * 'dtrm intro_pattern_expr located option) option
  | TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option
  | TacCase of evars_flag * 'trm with_bindings_arg
  | TacFix of Id.t option * int
  | TacMutualFix of Id.t * int * (Id.t * int * 'trm) list
  | TacCofix of Id.t option
  | TacMutualCofix of Id.t * (Id.t * 'trm) list
  | TacAssert of
      bool * 'tacexpr option *
      'dtrm intro_pattern_expr located option * 'trm
  | TacGeneralize of ('trm with_occurrences * Name.t) list
  | TacGeneralizeDep of 'trm
  | TacLetTac of Name.t * 'trm * 'nam clause_expr * letin_flag *
      intro_pattern_naming_expr located option

  (* Derived basic tactics *)
  | TacInductionDestruct of
      rec_flag * evars_flag * ('trm,'dtrm,'nam) induction_clause_list
  | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis

  (* Automation tactics *)
  | TacTrivial of debug * 'trm list * string list option
  | TacAuto of debug * int or_var option * 'trm list * string list option

  (* Context management *)
  | TacClear of bool * 'nam list
  | TacClearBody of 'nam list
  | TacMove of 'nam * 'nam move_location
  | TacRename of ('nam *'nam) list

  (* Trmuctors *)
  | TacSplit of evars_flag * 'trm bindings list

  (* Conversion *)
  | TacReduce of ('trm,'cst,'pat) red_expr_gen * 'nam clause_expr
  | TacChange of 'pat option * 'dtrm * 'nam clause_expr

  (* Equivalence relations *)
  | TacSymmetry of 'nam clause_expr

  (* Equality and inversion *)
  | TacRewrite of evars_flag *
      (bool * multi * 'dtrm with_bindings_arg) list * 'nam clause_expr *
      (* spiwack: using ['dtrm] here is a small hack, may not be
         stable by a change in the representation of delayed
         terms. Because, in fact, it is the whole "with_bindings"
         which is delayed. But because the "t" level for ['dtrm] is
         uninterpreted, it works fine here too, and avoid more
         disruption of this file. *)
      'tacexpr option
  | TacInversion of ('trm,'dtrm,'nam) inversion_strength * quantified_hypothesis

constraint 'a = <
    term:'trm;
    utrm: 'utrm;
    dterm: 'dtrm;
    pattern:'pat;
    constant:'cst;
    reference:'ref;
    name:'nam;
    tacexpr:'tacexpr;
    level:'lev
>

(** Possible arguments of a tactic definition *)

and 'a gen_tactic_arg =
  | TacDynamic     of Loc.t * Dyn.t
  | TacGeneric     of 'lev generic_argument
  | MetaIdArg      of Loc.t * bool * string
  | ConstrMayEval  of ('trm,'cst,'pat) may_eval
  | UConstr        of 'utrm
  | Reference      of 'ref
  | TacCall of Loc.t * 'ref *
      'a gen_tactic_arg list
  | TacFreshId of string or_var list
  | Tacexp of 'tacexpr
  | TacPretype of 'trm
  | TacNumgoals

constraint 'a = <
    term:'trm;
    utrm: 'utrm;
    dterm: 'dtrm;
    pattern:'pat;
    constant:'cst;
    reference:'ref;
    name:'nam;
    tacexpr:'tacexpr;
    level:'lev
>

(** Generic ltac expressions.
    't : terms, 'p : patterns, 'c : constants, 'i : inductive,
    'r : ltac refs, 'n : idents, 'l : levels *)

and 'a gen_tactic_expr =
  | TacAtom of Loc.t * 'a gen_atomic_tactic_expr
  | TacThen of
      'a gen_tactic_expr *
      'a gen_tactic_expr
  | TacDispatch of
      'a gen_tactic_expr list
  | TacExtendTac of
      'a gen_tactic_expr array *
      'a gen_tactic_expr *
      'a gen_tactic_expr array
  | TacThens of
      'a gen_tactic_expr *
      'a gen_tactic_expr list
  | TacThens3parts of
      'a gen_tactic_expr *
      'a gen_tactic_expr array *
      'a gen_tactic_expr *
      'a gen_tactic_expr array
  | TacFirst of 'a gen_tactic_expr list
  | TacComplete of 'a gen_tactic_expr
  | TacSolve of 'a gen_tactic_expr list
  | TacTry of 'a gen_tactic_expr
  | TacOr of
      'a gen_tactic_expr *
      'a gen_tactic_expr
  | TacOnce of
      'a gen_tactic_expr
  | TacExactlyOnce of
      'a gen_tactic_expr
  | TacIfThenCatch of
      'a gen_tactic_expr *
      'a gen_tactic_expr *
      'a gen_tactic_expr
  | TacOrelse of
      'a gen_tactic_expr *
      'a gen_tactic_expr
  | TacDo of int or_var * 'a gen_tactic_expr
  | TacTimeout of int or_var * 'a gen_tactic_expr
  | TacTime of string option * 'a gen_tactic_expr
  | TacRepeat of 'a gen_tactic_expr
  | TacProgress of 'a gen_tactic_expr
  | TacShowHyps of 'a gen_tactic_expr
  | TacAbstract of
      'a gen_tactic_expr * Id.t option
  | TacId of 'n message_token list
  | TacFail of global_flag * int or_var * 'n message_token list
  | TacInfo of 'a gen_tactic_expr
  | TacLetIn of rec_flag *
      (Id.t located * 'a gen_tactic_arg) list *
      'a gen_tactic_expr
  | TacMatch of lazy_flag *
      'a gen_tactic_expr *
      ('p,'a gen_tactic_expr) match_rule list
  | TacMatchGoal of lazy_flag * direction_flag *
      ('p,'a gen_tactic_expr) match_rule list
  | TacFun of 'a gen_tactic_fun_ast
  | TacArg of 'a gen_tactic_arg located
  (* For ML extensions *)
  | TacML of Loc.t * ml_tactic_name * 'l generic_argument list
  (* For syntax extensions *)
  | TacAlias of Loc.t * KerName.t * (Id.t * 'l generic_argument) list

constraint 'a = <
    term:'t;
    utrm: 'utrm;
    dterm: 'dtrm;
    pattern:'p;
    constant:'c;
    reference:'r;
    name:'n;
    tacexpr:'tacexpr;
    level:'l
>

and 'a gen_tactic_fun_ast =
    Id.t option list * 'a gen_tactic_expr

constraint 'a = <
    term:'t;
    utrm: 'utrm;
    dterm: 'dtrm;
    pattern:'p;
    constant:'c;
    reference:'r;
    name:'n;
    tacexpr:'te;
    level:'l
>

(** Globalized tactics *)

type g_trm = glob_constr_and_expr
type g_utrm = g_trm
type g_pat = glob_constr_pattern_and_expr
type g_cst = evaluable_global_reference and_short_name or_var
type g_ref = ltac_constant located or_var
type g_nam  = Id.t located

type g_dispatch =  <
    term:g_trm;
    utrm:g_utrm;
    dterm:g_trm;
    pattern:g_pat;
    constant:g_cst;
    reference:g_ref;
    name:g_nam;
    tacexpr:glob_tactic_expr;
    level:glevel
>

and glob_tactic_expr =
    g_dispatch gen_tactic_expr

type glob_atomic_tactic_expr =
    g_dispatch gen_atomic_tactic_expr

type glob_tactic_arg =
    g_dispatch gen_tactic_arg

(** Raw tactics *)

type r_trm = constr_expr
type r_utrm = r_trm
type r_pat = constr_pattern_expr
type r_cst = reference or_by_notation
type r_ref = reference
type r_nam  = Id.t located
type r_lev = rlevel

type r_dispatch =  <
    term:r_trm;
    utrm:r_utrm;
    dterm:r_trm;
    pattern:r_pat;
    constant:r_cst;
    reference:r_ref;
    name:r_nam;
    tacexpr:raw_tactic_expr;
    level:rlevel
>

and raw_tactic_expr =
    r_dispatch gen_tactic_expr

type raw_atomic_tactic_expr =
    r_dispatch gen_atomic_tactic_expr

type raw_tactic_arg =
    r_dispatch gen_tactic_arg

(** Interpreted tactics *)

type t_trm = Term.constr
type t_utrm = Glob_term.closed_glob_constr
type t_pat = glob_constr_pattern_and_expr
type t_cst = evaluable_global_reference and_short_name
type t_ref = ltac_constant located
type t_nam  = Id.t

type t_dispatch =  <
    term:t_trm;
    utrm:t_utrm;
    dterm:g_trm;
    pattern:t_pat;
    constant:t_cst;
    reference:t_ref;
    name:t_nam;
    tacexpr:glob_tactic_expr;
    level:tlevel
>

type tactic_expr =
    t_dispatch gen_tactic_expr

type atomic_tactic_expr =
    t_dispatch gen_atomic_tactic_expr

type tactic_arg =
    t_dispatch gen_tactic_arg

(** Misc *)

type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen
type glob_red_expr = (g_trm, g_cst, g_pat) red_expr_gen