blob: 46ecd11d24bf94d61e547c6d734b8bd2026166c5 (
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
|
(************************************************************************)
(* 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$ i*)
open Util
open Names
open Rawterm
open Extend
open Genarg
open Topconstr
open Tacexpr
open Vernacexpr
open Libnames
(* The lexer and parser of Coq. *)
val lexer : Token.lexer
module Gram : Grammar.S with type te = Token.t
(* The superclass of all grammar entries *)
type grammar_object
(* The type of typed grammar objects *)
type typed_entry
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
val get_constr_entry :
bool -> constr_entry -> grammar_object Gram.Entry.e * int option * bool
val grammar_extend :
grammar_object Gram.Entry.e -> Gramext.position option ->
(string option * Gramext.g_assoc option *
(Token.t Gramext.g_symbol list * Gramext.g_action) list) list
-> unit
val remove_grammars : int -> unit
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
(* Entry types *)
(* Table of Coq's grammar entries *)
type gram_universe
val create_univ_if_new : string -> string * gram_universe
val get_univ : string -> string * gram_universe
val get_entry : string * gram_universe -> string -> typed_entry
val entry_type : string * gram_universe -> string -> entry_type option
val get_entry_type : string * string -> entry_type
val create_entry_if_new :
string * gram_universe -> string -> entry_type -> unit
val create_entry :
string * gram_universe -> string -> entry_type -> typed_entry
val force_entry_type :
string * gram_universe -> string -> entry_type -> typed_entry
val create_constr_entry :
string * gram_universe -> string -> constr_expr Gram.Entry.e
val create_generic_entry : string -> ('a, constr_expr,raw_tactic_expr) abstract_argument_type -> 'a Gram.Entry.e
val get_generic_entry : string -> grammar_object Gram.Entry.e
val get_generic_entry_type : string * gram_universe -> string -> Genarg.argument_type
(* The main entry: reads an optional vernac command *)
val main_entry : (loc * vernac_expr) option Gram.Entry.e
(* Initial state of the grammar *)
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 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 dirpath : dir_path Gram.Entry.e
val ne_string : string 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 annot : constr_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 * constr_expr) Gram.Entry.e
val binder_let : local_binder Gram.Entry.e
end
module Module :
sig
val module_expr : module_ast Gram.Entry.e
val module_type : module_type_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) 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 Gram.Entry.e
val tactic_arg : raw_tactic_arg Gram.Entry.e
val tactic_expr : raw_tactic_expr Gram.Entry.e
val tactic_main_level : int
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
end
(* Binding entry names to campl4 entries *)
val symbol_of_production : Gramext.g_assoc option -> constr_entry ->
bool -> constr_production_entry -> Token.t Gramext.g_symbol
(* Registering/resetting the level of an entry *)
val find_position :
bool -> bool -> Gramext.g_assoc option -> int option ->
Gramext.position option * Gramext.g_assoc option * string option
val remove_levels : int -> unit
val coerce_global_to_id : reference -> identifier
|
