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
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq 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) *)
(************************************************************************)
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
open Names
open Ltac_plugin
(* Names of variables to be cleared (automatic check: not a section var) *)
type ssrhyp = SsrHyp of Id.t Loc.located
(* Variant of the above *)
type ssrhyp_or_id = Hyp of ssrhyp | Id of ssrhyp
(* Variant of the above *)
type ssrhyps = ssrhyp list
(* Direction to be used for rewriting as in -> or rewrite flag *)
type ssrdir = Ssrmatching_plugin.Ssrmatching.ssrdir = L2R | R2L
(* simpl: "/=", cut: "//", simplcut: "//=" nop: commodity placeholder *)
type ssrsimpl = Simpl of int | Cut of int | SimplCut of int * int | Nop
(* modality for rewrite and do: ! ? *)
type ssrmmod = May | Must | Once
(* modality with a bound for rewrite and do: !n ?n *)
type ssrmult = int * ssrmmod
(** Occurrence switch {1 2}, all is Some(false,[]) *)
type ssrocc = (bool * int list) option
(* index MAYBE REMOVE ONLY INTERNAL stuff between {} *)
type ssrindex = int Locus.or_var
(* clear switch {H G} *)
type ssrclear = ssrhyps
(* Discharge occ switch (combined occurrence / clear switch) *)
type ssrdocc = ssrclear option * ssrocc
(* OLD ssr terms *)
(* terms are pre constr, the kind is a parsing/printing flag to distinguish
* between x, @x and (x). It affects automatic clear and let-in preservation. *)
(* FIXME *)
(* Cpattern is a temporary flag that becomes InParens ASAP. *)
type ssrtermkind = Ssrmatching_plugin.Ssrmatching.ssrtermkind
type ssrterm = ssrtermkind * Genintern.glob_constr_and_expr
(* NEW ssr term *)
type ast_glob_env = {
ast_ltacvars : Id.Set.t;
ast_extra : Genintern.Store.t;
ast_intern_sign : Genintern.intern_variable_status;
}
(* These terms are raw but closed with the intenalization/interpretation
* context. It is up to the tactic receiving it to decide if such contexts
* are useful or not, and eventually manipulate the term before turning it
* into a constr *)
type ast_closure_term = {
body : Constrexpr.constr_expr;
glob_env : ast_glob_env option; (* for Tacintern.intern_constr *)
interp_env : Geninterp.interp_sign option; (* for Tacinterp.interp_open_constr_with_bindings *)
annotation : [ `None | `Parens | `DoubleParens | `At ];
}
type ssrview = ast_closure_term list
type id_block = Prefix of Id.t | SuffixId of Id.t | SuffixNum of int
(* Only [One] forces an introduction, possibly reducing the goal. *)
type anon_kind =
| One of string option (* name hint *)
| Drop
| All
| Temporary
type ssripat =
| IPatNoop
| IPatId of Id.t
| IPatAnon of anon_kind (* inaccessible name *)
| IPatDispatch of ssripatss_or_block (* (..|..) *)
| IPatCase of ssripatss_or_block (* [..|..] *)
| IPatInj of ssripatss
| IPatRewrite of (*occurrence option * rewrite_pattern **) ssrocc * ssrdir
| IPatView of ssrview (* /view *)
| IPatClear of ssrclear (* {H1 H2} *)
| IPatSimpl of ssrsimpl
| IPatAbstractVars of Id.t list
| IPatFastNondep
and ssripats = ssripat list
and ssripatss = ssripats list
and ssripatss_or_block =
| Block of id_block
| Regular of ssripats list
type ssrhpats = ((ssrclear option * ssripats) * ssripats) * ssripats
type ssrhpats_wtransp = bool * ssrhpats
(* tac => inpats *)
type ssrintrosarg = Tacexpr.raw_tactic_expr * ssripats
type ssrfwdid = Id.t
(** Binders (for fwd tactics) *)
type 'term ssrbind =
| Bvar of Name.t
| Bdecl of Name.t list * 'term
| Bdef of Name.t * 'term option * 'term
| Bstruct of Name.t
| Bcast of 'term
(* We use an intermediate structure to correctly render the binder list *)
(* abbreviations. We use a list of hints to extract the binders and *)
(* base term from a term, for the two first levels of representation of *)
(* of constr terms. *)
type ssrbindfmt =
| BFvar
| BFdecl of int (* #xs *)
| BFcast (* final cast *)
| BFdef (* has cast? *)
| BFrec of bool * bool (* has struct? * has cast? *)
type 'term ssrbindval = 'term ssrbind list * 'term
(** Forward chaining argument *)
(* There are three kinds of forward definitions: *)
(* - Hint: type only, cast to Type, may have proof hint. *)
(* - Have: type option + value, no space before type *)
(* - Pose: binders + value, space before binders. *)
type ssrfwdkind = FwdHint of string * bool | FwdHave | FwdPose
type ssrfwdfmt = ssrfwdkind * ssrbindfmt list
(* in *)
type ssrclseq = InGoal | InHyps
| InHypsGoal | InHypsSeqGoal | InSeqGoal | InHypsSeq | InAll | InAllHyps
type 'tac ssrhint = bool * 'tac option list
type 'tac fwdbinders =
bool * (ssrhpats * ((ssrfwdfmt * ast_closure_term) * 'tac ssrhint))
type 'tac ffwbinders =
(ssrhpats * ((ssrfwdfmt * ast_closure_term) * 'tac ssrhint))
type clause =
(ssrclear * ((ssrhyp_or_id * string) *
Ssrmatching_plugin.Ssrmatching.cpattern option) option)
type clauses = clause list * ssrclseq
type wgen =
(ssrclear *
((ssrhyp_or_id * string) *
Ssrmatching_plugin.Ssrmatching.cpattern option)
option)
type 'a ssrdoarg = ((ssrindex * ssrmmod) * 'a ssrhint) * clauses
type 'a ssrseqarg = ssrindex * ('a ssrhint * 'a option)
open Ssrmatching_plugin
open Ssrmatching
type 'a ssrcasearg = ssripat option * ('a * ssripats)
type 'a ssrmovearg = ssrview * 'a ssrcasearg
type ssrdgens = { dgens : (ssrdocc * cpattern) list;
gens : (ssrdocc * cpattern) list;
clr : ssrclear }
type 'a ssragens = (ssrdocc * 'a) list list * ssrclear
type ssrapplyarg = ssrterm list * (ssrterm ssragens * ssripats)
(* OOP : these are general shortcuts *)
type gist = Tacintern.glob_sign
type ist = Tacinterp.interp_sign
type goal = Evar.t
|
