summaryrefslogtreecommitdiff
path: root/parsing/pcoq.mli
blob: 88bf9c1c85e1866d15567461087d145685c6d462 (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
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(*i $Id$ i*)

open Util
open Names
open Rawterm
open Extend
open Vernacexpr
open Genarg
open Topconstr
open Tacexpr
open Libnames

(**********************************************************************)
(* The parser of Coq                                                  *)

module Gram : Grammar.S with type te = Compat.token

(**********************************************************************)
(* The parser of Coq is built from three kinds of rule declarations:
   - dynamic rules declared at the evaluation of Coq files (using
     e.g. Notation, Infix, or Tactic Notation)
   - static rules explicitly defined in files g_*.ml4
   - static rules macro-generated by ARGUMENT EXTEND, TACTIC EXTEND and
     VERNAC EXTEND (see e.g. file extratactics.ml4)
*)

(* Dynamic extension of rules

    For constr notations, dynamic addition of new rules is done in
    several steps:

    - "x + y" (user gives a notation string of type Topconstr.notation)
        |     (together with a constr entry level, e.g. 50, and indications of)
        |     (subentries, e.g. x in constr next level and y constr same level)
        |
        | spliting into tokens by Metasyntax.split_notation_string
        V
      [String "x"; String "+"; String "y"] : symbol_token list
        |
        | interpreted as a mixed parsing/printing production
        | by Metasyntax.analyse_notation_tokens
        V
      [NonTerminal "x"; Terminal "+"; NonTerminal "y"] : symbol list
        |
        | translated to a parsing production by Metasyntax.make_production
        V
      [GramConstrNonTerminal (ETConstr (NextLevel,(BorderProd Left,LeftA)),
                              Some "x");
       GramConstrTerminal ("","+");
       GramConstrNonTerminal (ETConstr (NextLevel,(BorderProd Right,LeftA)),
                              Some "y")]
       : grammar_constr_prod_item list
        |
        | Egrammar.make_constr_prod_item
        V
      Gramext.g_symbol list which is sent to camlp4

    For user level tactic notations, dynamic addition of new rules is
    also done in several steps:

    - "f" constr(x) (user gives a Tactic Notation command)
        |
        | parsing
        V
      [TacTerm "f"; TacNonTerm ("constr", Some "x")]
      : grammar_tactic_prod_item_expr list
        |
        | Metasyntax.interp_prod_item
        V
      [GramTerminal "f";
       GramNonTerminal (ConstrArgType, Aentry ("constr","constr"), Some "x")]
      : grammar_prod_item list
        |
        | Egrammar.make_prod_item
        V
      Gramext.g_symbol list

    For TACTIC/VERNAC/ARGUMENT EXTEND, addition of new rules is done as follows:

    - "f" constr(x) (developer gives an EXTEND rule)
        |
        | macro-generation in tacextend.ml4/vernacextend.ml4/argextend.ml4
        V
      [GramTerminal "f";
       GramNonTerminal (ConstrArgType, Aentry ("constr","constr"), Some "x")]
        |
        | Egrammar.make_prod_item
        V
      Gramext.g_symbol list

*)

(* The superclass of all grammar entries *)
type grammar_object

type camlp4_rule =
    Compat.token Gramext.g_symbol list * Gramext.g_action

type camlp4_entry_rules =
    (* first two parameters are name and assoc iff a level is created *)
    string option * Gramext.g_assoc option * camlp4_rule list

(* Add one extension at some camlp4 position of some camlp4 entry *)
val grammar_extend :
  grammar_object Gram.Entry.e -> Gramext.position option ->
   (* for reinitialization if ever needed: *) Gramext.g_assoc option ->
     camlp4_entry_rules list -> unit

(* Remove the last n extensions *)
val remove_grammars : int -> unit




(* The type of typed grammar objects *)
type typed_entry

(* The possible types for extensible grammars *)
type entry_type = argument_type

val type_of_typed_entry : typed_entry -> entry_type
val object_of_typed_entry : typed_entry -> grammar_object Gram.Entry.e
val weaken_entry : 'a Gram.Entry.e -> grammar_object Gram.Entry.e

(* Temporary activate camlp4 verbosity *)

val camlp4_verbosity : bool -> ('a -> unit) -> 'a -> unit

(* Parse a string *)

val parse_string : 'a Gram.Entry.e -> string -> 'a
val eoi_entry : 'a Gram.Entry.e -> 'a Gram.Entry.e
val map_entry : ('a -> 'b) -> 'a Gram.Entry.e -> 'b Gram.Entry.e

(**********************************************************************)
(* Table of Coq statically defined grammar entries                    *)

type gram_universe

(* There are four predefined universes: "prim", "constr", "tactic", "vernac" *)

val get_univ : string -> gram_universe

val uprim : gram_universe
val uconstr : gram_universe
val utactic : gram_universe
val uvernac : gram_universe

(*
val get_entry : gram_universe -> string -> typed_entry
val get_entry_type : gram_universe -> string -> entry_type
*)

val create_entry : gram_universe -> string -> entry_type -> typed_entry
val create_generic_entry : string -> ('a, rlevel) abstract_argument_type ->
  'a Gram.Entry.e

module Prim :
  sig
    open Util
    open Names
    open Libnames
    val preident : string Gram.Entry.e
    val ident : identifier Gram.Entry.e
    val name : name located Gram.Entry.e
    val identref : identifier located Gram.Entry.e
    val pattern_ident : identifier Gram.Entry.e
    val pattern_identref : identifier located Gram.Entry.e
    val base_ident : identifier Gram.Entry.e
    val natural : int Gram.Entry.e
    val bigint : Bigint.bigint Gram.Entry.e
    val integer : int Gram.Entry.e
    val string : string Gram.Entry.e
    val qualid : qualid located Gram.Entry.e
    val fullyqualid : identifier list located Gram.Entry.e
    val reference : reference Gram.Entry.e
    val by_notation : (loc * string * string option) Gram.Entry.e
    val smart_global : reference or_by_notation Gram.Entry.e
    val dirpath : dir_path Gram.Entry.e
    val ne_string : string Gram.Entry.e
    val ne_lstring : string located Gram.Entry.e
    val var : identifier located Gram.Entry.e
  end

module Constr :
  sig
    val constr : constr_expr Gram.Entry.e
    val constr_eoi : constr_expr Gram.Entry.e
    val lconstr : constr_expr Gram.Entry.e
    val binder_constr : constr_expr Gram.Entry.e
    val operconstr : constr_expr Gram.Entry.e
    val ident : identifier Gram.Entry.e
    val global : reference Gram.Entry.e
    val sort : rawsort Gram.Entry.e
    val pattern : cases_pattern_expr Gram.Entry.e
    val constr_pattern : constr_expr Gram.Entry.e
    val lconstr_pattern : constr_expr Gram.Entry.e
    val binder : (name located list * binder_kind * constr_expr) Gram.Entry.e
    val binder_let : local_binder list Gram.Entry.e
    val binders_let : local_binder list Gram.Entry.e
    val binders_let_fixannot : (local_binder list * (identifier located option * recursion_order_expr)) Gram.Entry.e
    val typeclass_constraint : (name located * bool * constr_expr) Gram.Entry.e
    val record_declaration : constr_expr Gram.Entry.e
    val appl_arg : (constr_expr * explicitation located option) Gram.Entry.e
  end

module Module :
  sig
    val module_expr : module_ast Gram.Entry.e
    val module_type : module_ast Gram.Entry.e
  end

module Tactic :
  sig
    open Rawterm
    val open_constr : open_constr_expr Gram.Entry.e
    val casted_open_constr : open_constr_expr Gram.Entry.e
    val constr_with_bindings : constr_expr with_bindings Gram.Entry.e
    val bindings : constr_expr bindings Gram.Entry.e
    val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.Entry.e
    val quantified_hypothesis : quantified_hypothesis Gram.Entry.e
    val int_or_var : int or_var Gram.Entry.e
    val red_expr : raw_red_expr Gram.Entry.e
    val simple_tactic : raw_atomic_tactic_expr Gram.Entry.e
    val simple_intropattern : Genarg.intro_pattern_expr located Gram.Entry.e
    val tactic_arg : raw_tactic_arg Gram.Entry.e
    val tactic_expr : raw_tactic_expr Gram.Entry.e
    val binder_tactic : raw_tactic_expr Gram.Entry.e
    val tactic : raw_tactic_expr Gram.Entry.e
    val tactic_eoi : raw_tactic_expr Gram.Entry.e
  end

module Vernac_ :
  sig
    open Decl_kinds
    val gallina : vernac_expr Gram.Entry.e
    val gallina_ext : vernac_expr Gram.Entry.e
    val command : vernac_expr Gram.Entry.e
    val syntax : vernac_expr Gram.Entry.e
    val vernac : vernac_expr Gram.Entry.e
    val vernac_eoi : vernac_expr Gram.Entry.e
    val proof_instr : Decl_expr.raw_proof_instr Gram.Entry.e
  end

(* The main entry: reads an optional vernac command *)
val main_entry : (loc * vernac_expr) option Gram.Entry.e

(**********************************************************************)
(* Mapping formal entries into concrete ones                          *)

(* Binding constr entry keys to entries and symbols *)

val interp_constr_entry_key : bool (* true for cases_pattern *) ->
  constr_entry_key -> grammar_object Gram.Entry.e * int option

val symbol_of_constr_prod_entry_key : Gramext.g_assoc option ->
  constr_entry_key -> bool -> constr_prod_entry_key ->
    Compat.token Gramext.g_symbol

(* Binding general entry keys to symbols *)

val symbol_of_prod_entry_key :
  Gram.te prod_entry_key -> Gram.te Gramext.g_symbol

(**********************************************************************)
(* Interpret entry names of the form "ne_constr_list" as entry keys   *)

val interp_entry_name : bool (* true to fail on unknown entry *) ->
  int option -> string -> string -> entry_type * Gram.te prod_entry_key

(**********************************************************************)
(* Registering/resetting the level of a constr entry                  *)

val find_position :
  bool (* true if for creation in pattern entry; false if in constr entry *) ->
  Gramext.g_assoc option -> int option ->
    Gramext.position option * Gramext.g_assoc option * string option *
    (* for reinitialization: *) Gramext.g_assoc option

val synchronize_level_positions : unit -> unit

val register_empty_levels : bool -> int list ->
    (Gramext.position option * Gramext.g_assoc option *
     string option * Gramext.g_assoc option) list

val remove_levels : int -> unit