summaryrefslogtreecommitdiff
path: root/interp/genarg.mli
blob: c4275589daeadcca614a78625922ce51f655df03 (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
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(*i $Id: genarg.mli 8983 2006-06-23 13:21:49Z herbelin $ i*)

open Util
open Names
open Term
open Libnames
open Rawterm
open Topconstr
open Term

type 'a and_short_name = 'a * identifier located option

(* 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 rawconstr_and_expr = rawconstr * constr_expr option

type open_constr = Evd.evar_map * Term.constr
type open_constr_expr = unit * constr_expr
type open_rawconstr = unit * rawconstr_and_expr

type intro_pattern_expr =
  | IntroOrAndPattern of case_intro_pattern_expr
  | IntroWildcard
  | IntroIdentifier of identifier
  | IntroAnonymous
and case_intro_pattern_expr = intro_pattern_expr list list

val pr_intro_pattern : intro_pattern_expr -> Pp.std_ppcmds
val pr_case_intro_pattern : case_intro_pattern_expr -> Pp.std_ppcmds

(* The route of a generic argument, from parsing to evaluation

\begin{verbatim}
              parsing        in_raw                           out_raw
    char stream ----> rawtype ----> rawconstr generic_argument ---->
                                                                   |
                                                                   | interp
                                                                   V
                          type  <---- constr generic_argument  <----
                                  out                            in
\end{verbatim}

To distinguish between the uninterpreted (raw) and the interpreted
worlds, we annotate the type [generic_argument] by a phantom argument
which is either [constr_expr] or [constr] (actually we add also a second
argument [raw_tactic_expr] and [tactic], but this is only for technical
reasons, because these types are undefined at the type of compilation
of [Genarg]).

Transformation for each type :
\begin{verbatim}
tag                            raw open type            cooked closed type

BoolArgType                    bool                      bool
IntArgType                     int                       int
IntOrVarArgType                int or_var                int
StringArgType                  string (parsed w/ "")     string
PreIdentArgType                string (parsed w/o "")    (vernac only)
IdentArgType                   identifier                identifier
IntroPatternArgType            intro_pattern_expr        intro_pattern_expr
VarArgType                     identifier located        identifier
RefArgType                     reference                 global_reference
QuantHypArgType                quantified_hypothesis     quantified_hypothesis
ConstrArgType                  constr_expr               constr
ConstrMayEvalArgType           constr_expr may_eval      constr
OpenConstrArgType              open_constr_expr          open_constr
ConstrWithBindingsArgType      constr_expr with_bindings constr with_bindings
BindingsArgType                constr_expr bindings      constr bindings
List0ArgType of argument_type
List1ArgType of argument_type
OptArgType of argument_type
ExtraArgType of string         '_a                      '_b
\end{verbatim}
*)

(* All of [rlevel], [glevel] and [tlevel] must be non convertible 
   to ensure the injectivity of the type inference from type
   [('co,'ta) generic_argument] to [('a,'co,'ta) abstract_argument_type]
   is injective; this guarantees that, for 'b fixed, the type of
   out_gen is monomorphic over 'a, hence type-safe 
*)

type rlevel = constr_expr
type glevel = rawconstr_and_expr
type tlevel = constr

type ('a,'co,'ta) abstract_argument_type

val rawwit_bool : (bool,rlevel,'ta) abstract_argument_type
val globwit_bool : (bool,glevel,'ta) abstract_argument_type
val wit_bool : (bool,tlevel,'ta) abstract_argument_type

val rawwit_int : (int,rlevel,'ta) abstract_argument_type
val globwit_int : (int,glevel,'ta) abstract_argument_type
val wit_int : (int,tlevel,'ta) abstract_argument_type

val rawwit_int_or_var : (int or_var,rlevel,'ta) abstract_argument_type
val globwit_int_or_var : (int or_var,glevel,'ta) abstract_argument_type
val wit_int_or_var : (int or_var,tlevel,'ta) abstract_argument_type

val rawwit_string : (string,rlevel,'ta) abstract_argument_type
val globwit_string : (string,glevel,'ta) abstract_argument_type
val wit_string : (string,tlevel,'ta) abstract_argument_type

val rawwit_pre_ident : (string,rlevel,'ta) abstract_argument_type
val globwit_pre_ident : (string,glevel,'ta) abstract_argument_type
val wit_pre_ident : (string,tlevel,'ta) abstract_argument_type

val rawwit_intro_pattern : (intro_pattern_expr,rlevel,'ta) abstract_argument_type
val globwit_intro_pattern : (intro_pattern_expr,glevel,'ta) abstract_argument_type
val wit_intro_pattern : (intro_pattern_expr,tlevel,'ta) abstract_argument_type

val rawwit_ident : (identifier,rlevel,'ta) abstract_argument_type
val globwit_ident : (identifier,glevel,'ta) abstract_argument_type
val wit_ident : (identifier,tlevel,'ta) abstract_argument_type

val rawwit_var : (identifier located,rlevel,'ta) abstract_argument_type
val globwit_var : (identifier located,glevel,'ta) abstract_argument_type
val wit_var : (identifier,tlevel,'ta) abstract_argument_type

val rawwit_ref : (reference,rlevel,'ta) abstract_argument_type
val globwit_ref : (global_reference located or_var,glevel,'ta) abstract_argument_type
val wit_ref : (global_reference,tlevel,'ta) abstract_argument_type

val rawwit_quant_hyp : (quantified_hypothesis,rlevel,'ta) abstract_argument_type
val globwit_quant_hyp : (quantified_hypothesis,glevel,'ta) abstract_argument_type
val wit_quant_hyp : (quantified_hypothesis,tlevel,'ta) abstract_argument_type

val rawwit_sort : (rawsort,rlevel,'ta) abstract_argument_type
val globwit_sort : (rawsort,glevel,'ta) abstract_argument_type
val wit_sort : (sorts,tlevel,'ta) abstract_argument_type

val rawwit_constr : (constr_expr,rlevel,'ta) abstract_argument_type
val globwit_constr : (rawconstr_and_expr,glevel,'ta) abstract_argument_type
val wit_constr : (constr,tlevel,'ta) abstract_argument_type

val rawwit_constr_may_eval : ((constr_expr,reference) may_eval,rlevel,'ta) abstract_argument_type
val globwit_constr_may_eval : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) may_eval,glevel,'ta) abstract_argument_type
val wit_constr_may_eval : (constr,tlevel,'ta) abstract_argument_type

val rawwit_open_constr_gen : bool -> (open_constr_expr,rlevel,'ta) abstract_argument_type
val globwit_open_constr_gen : bool -> (open_rawconstr,glevel,'ta) abstract_argument_type
val wit_open_constr_gen : bool -> (open_constr,tlevel,'ta) abstract_argument_type

val rawwit_open_constr : (open_constr_expr,rlevel,'ta) abstract_argument_type
val globwit_open_constr : (open_rawconstr,glevel,'ta) abstract_argument_type
val wit_open_constr : (open_constr,tlevel,'ta) abstract_argument_type

val rawwit_casted_open_constr : (open_constr_expr,rlevel,'ta) abstract_argument_type
val globwit_casted_open_constr : (open_rawconstr,glevel,'ta) abstract_argument_type
val wit_casted_open_constr : (open_constr,tlevel,'ta) abstract_argument_type

val rawwit_constr_with_bindings : (constr_expr with_bindings,rlevel,'ta) abstract_argument_type
val globwit_constr_with_bindings : (rawconstr_and_expr with_bindings,glevel,'ta) abstract_argument_type
val wit_constr_with_bindings : (constr with_bindings,tlevel,'ta) abstract_argument_type

val rawwit_bindings : (constr_expr bindings,rlevel,'ta) abstract_argument_type
val globwit_bindings : (rawconstr_and_expr bindings,glevel,'ta) abstract_argument_type
val wit_bindings : (constr bindings,tlevel,'ta) abstract_argument_type

val rawwit_red_expr : ((constr_expr,reference) red_expr_gen,rlevel,'ta) abstract_argument_type
val globwit_red_expr : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) red_expr_gen,glevel,'ta) abstract_argument_type
val wit_red_expr : ((constr,evaluable_global_reference) red_expr_gen,tlevel,'ta) abstract_argument_type

val wit_list0 :
  ('a,'co,'ta) abstract_argument_type -> ('a list,'co,'ta) abstract_argument_type

val wit_list1 :
  ('a,'co,'ta) abstract_argument_type -> ('a list,'co,'ta) abstract_argument_type

val wit_opt :
  ('a,'co,'ta) abstract_argument_type -> ('a option,'co,'ta) abstract_argument_type

val wit_pair :
  ('a,'co,'ta) abstract_argument_type ->
  ('b,'co,'ta) abstract_argument_type ->
      ('a * 'b,'co,'ta) abstract_argument_type

(* ['a generic_argument] = (Sigma t:type. t[[constr/'a]]) *)
type ('a,'b) generic_argument

val fold_list0 : 
 (('a,'b) generic_argument -> 'c -> 'c) -> ('a,'b) generic_argument -> 'c -> 'c

val fold_list1 : 
 (('a,'b) generic_argument -> 'c -> 'c) -> ('a,'b) generic_argument -> 'c -> 'c

val fold_opt :
 (('a,'b) generic_argument -> 'c) -> 'c -> ('a,'b) generic_argument -> 'c

val fold_pair :
 (('a,'b) generic_argument -> ('a,'b) generic_argument -> 'c) -> 
      ('a,'b) generic_argument -> 'c

(* [app_list0] fails if applied to an argument not of tag [List0 t]
    for some [t]; it's the responsability of the caller to ensure it *)

val app_list0 : (('a,'b) generic_argument -> ('c,'d) generic_argument) -> 
('a,'b) generic_argument -> ('c,'d) generic_argument

val app_list1 : (('a,'b) generic_argument -> ('c,'d) generic_argument) -> 
('a,'b) generic_argument -> ('c,'d) generic_argument

val app_opt : (('a,'b) generic_argument -> ('c,'d) generic_argument) -> 
('a,'b) generic_argument -> ('c,'d) generic_argument

val app_pair :
  (('a,'b) generic_argument -> ('c,'d) generic_argument) ->
      (('a,'b) generic_argument -> ('c,'d) generic_argument)
   -> ('a,'b) generic_argument -> ('c,'d) generic_argument

(* Manque l'ordre supérieur, on aimerait ('co,'ta) 'a; manque aussi le
   polymorphism, on aimerait que 'b et 'c restent polymorphes à l'appel
   de create *)
val create_arg : string ->
      ('a,tlevel,'ta) abstract_argument_type
      * ('globa,glevel,'globta) abstract_argument_type
      * ('rawa,rlevel,'rawta) abstract_argument_type

val exists_argtype : string -> bool

type argument_type =
  (* Basic types *)
  | BoolArgType
  | IntArgType
  | IntOrVarArgType
  | StringArgType
  | PreIdentArgType
  | IntroPatternArgType
  | IdentArgType
  | VarArgType
  | RefArgType
  (* Specific types *)
  | SortArgType
  | ConstrArgType
  | ConstrMayEvalArgType
  | QuantHypArgType
  | OpenConstrArgType of bool
  | ConstrWithBindingsArgType
  | BindingsArgType
  | RedExprArgType
  | List0ArgType of argument_type
  | List1ArgType of argument_type
  | OptArgType of argument_type
  | PairArgType of argument_type * argument_type
  | ExtraArgType of string

val genarg_tag : ('a,'b) generic_argument -> argument_type

val unquote : ('a,'co,'ta) abstract_argument_type -> argument_type

(* We'd like

  [in_generic: !b:type, !a:argument_type -> (f a) -> b generic_argument]

   with f a = b if a is Constr, f a = c if a is Tactic, otherwise f a = |a|

   [in_generic] is not typable; we replace the second argument by an absurd
   type (with no introduction rule)
*)
type an_arg_of_this_type

val in_generic : 
  argument_type -> an_arg_of_this_type -> ('a,'b) generic_argument

val in_gen :
  ('a,'co,'ta) abstract_argument_type -> 'a -> ('co,'ta) generic_argument
val out_gen :
  ('a,'co,'ta) abstract_argument_type -> ('co,'ta) generic_argument -> 'a