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
|
(************************************************************************)
(* * The Rocq Prover / The Rocq 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) *)
(************************************************************************)
type loc = {
loc_start : Lexing.position;
loc_end : Lexing.position;
}
type code = { code : string; loc : loc option; }
type user_symbol =
| Ulist1 of user_symbol
| Ulist1sep of user_symbol * string
| Ulist0 of user_symbol
| Ulist0sep of user_symbol * string
| Uopt of user_symbol
| Uentry of string
| Uentryl of string * int
type token_data =
| TokNone
| TokName of string
type ext_token =
| ExtTerminal of string
| ExtNonTerminal of user_symbol * token_data
type tactic_rule = {
tac_toks : ext_token list;
tac_body : code;
}
type level = string
type position =
| First
| Last
| Before of level
| After of level
type assoc =
| LeftA
| RightA
| NonA
type gram_symbol =
| GSymbString of string
| GSymbQualid of string * level option
| GSymbParen of gram_symbol list
| GSymbProd of gram_prod list
and gram_prod = {
gprod_symbs : (string option * gram_symbol list) list;
gprod_body : code;
}
type symb =
| SymbToken of string * string option
| SymbEntry of string * string option
| SymbSelf
| SymbNext
| SymbList0 of symb * symb option
| SymbList1 of symb * symb option
| SymbOpt of symb
| SymbRules of ((string option * symb) list * code) list
| SymbQuote of string (** Not used by GRAMMAR EXTEND *)
type gram_rule = {
grule_label : string option;
grule_assoc : assoc option;
grule_prods : gram_prod list;
}
type grammar_rules =
| GDataFresh of position option * gram_rule list
| GDataReuse of string option * gram_prod list
type grammar_entry = {
gentry_name : string;
gentry_rules : grammar_rules;
}
type grammar_ext = {
gramext_name : string;
gramext_globals : string list;
gramext_entries : grammar_entry list;
}
type tactic_ext = {
tacext_name : string;
tacext_level : int option;
tacext_deprecated : code option;
tacext_rules : tactic_rule list;
}
type classification =
| ClassifDefault
| ClassifCode of code
| ClassifName of string
type vernac_rule = {
vernac_atts : (string * code) list option;
vernac_state : string option;
vernac_toks : ext_token list;
vernac_class : code option;
vernac_depr : bool;
vernac_body : code;
vernac_synterp : (string * code) option;
}
type vernac_ext = {
vernacext_name : string;
vernacext_entry : code option;
vernacext_class : classification;
vernacext_state : string option;
vernacext_rules : vernac_rule list;
}
type vernac_argument_ext = {
vernacargext_name : string;
vernacargext_printer : code option;
vernacargext_rules : tactic_rule list;
}
type argument_type =
| ListArgType of argument_type
| OptArgType of argument_type
| PairArgType of argument_type * argument_type
| ExtraArgType of string
type argument_ext = {
argext_name : string;
argext_rules : tactic_rule list;
argext_type : argument_type option;
argext_interp : (string option * code) option;
argext_glob : code option;
argext_subst : code option;
argext_rprinter : code option;
argext_gprinter : code option;
argext_tprinter : code option;
}
type node =
| Code of code
| Comment of string
| DeclarePlugin of string option
| GramExt of grammar_ext
| VernacExt of vernac_ext
| VernacArgumentExt of vernac_argument_ext
| TacticExt of tactic_ext
| ArgumentExt of argument_ext
type t = node list
|
