3108
|
1 |
% This file was generated by 'rail' from 'ref.rai'
|
3098
|
2 |
\rail@t {lbrace}
|
|
3 |
\rail@t {rbrace}
|
5372
|
4 |
\rail@i {1}{ \par theoryDef : id '=' (name + '+') ('+' extension | ()) ; \par name : id | string ; \par extension : (section +) 'end' ( () | ml ) ; \par section : classes | default | types | arities | nonterminals | consts | syntax | trans | defs | constdefs | rules | axclass | instance | oracle | local | global | setup ; \par classes : 'classes' ( classDecl + ) ; \par classDecl : (id (() | '<' (id + ','))) ; \par default : 'default' sort ; \par sort : id | lbrace (id * ',') rbrace ; \par types : 'types' ( ( typeDecl ( () | '(' infix ')' ) ) + ) ; \par infix : ( 'infixr' | 'infixl' ) (() | string) nat ; \par typeDecl : typevarlist name ( () | '=' ( string | type ) ); \par typevarlist : () | tid | '(' ( tid + ',' ) ')'; \par type : simpleType | '(' type ')' | type '=>' type | '[' ( type + "," ) ']' '=>' type; \par simpleType: id | ( tid ( () | '::' id ) ) | '(' ( type + "," ) ')' id | simpleType id ; \par arities : 'arities' ((name + ',') '::' arity +) ; \par arity : ( () | '(' (sort + ',') ')' ) sort ; \par nonterminals : 'nonterminals' (name+) ; \par consts : 'consts' ( mixfixConstDecl + ) ; \par syntax : 'syntax' (() | mode) ( mixfixConstDecl + ); \par mode : '(' name (() | 'output') ')' ; \par mixfixConstDecl : constDecl (() | ( '(' mixfix ')' )) ; \par constDecl : ( name + ',') '::' (string | type); \par mixfix : string ( () | ( () | ('[' (nat + ',') ']')) nat ) | infix | 'binder' string nat ; \par trans : 'translations' ( pat ( '==' | '=>' | '<=' ) pat + ) ; \par pat : ( () | ( '(' id ')' ) ) string; \par rules : 'rules' (( id string ) + ) ; \par defs : 'defs' (( id string ) + ) ; \par constdefs : 'constdefs' (name '::' (string | type) (() | mixfix) string +) ; \par axclass : 'axclass' classDecl (() | ( id string ) +) ; \par instance : 'instance' ( name '<' name | name '::' arity) witness ; \par witness : (() | '(' ((string | id | longident) + ',') ')') (() | verbatim) ; \par oracle : 'oracle' name '=' name ; \par local : 'local' ; \par global : 'global' ; \par setup : 'setup' (id | longident) ; \par ml : 'ML' text ; \par }
|
2657
|
5 |
\rail@o {1}{
|
|
6 |
\rail@begin{2}{theoryDef}
|
3098
|
7 |
\rail@nont{id}[]
|
|
8 |
\rail@term{=}[]
|
2657
|
9 |
\rail@plus
|
3098
|
10 |
\rail@nont{name}[]
|
2657
|
11 |
\rail@nextplus{1}
|
3098
|
12 |
\rail@cterm{+}[]
|
2657
|
13 |
\rail@endplus
|
|
14 |
\rail@bar
|
3098
|
15 |
\rail@term{+}[]
|
|
16 |
\rail@nont{extension}[]
|
2657
|
17 |
\rail@nextbar{1}
|
|
18 |
\rail@endbar
|
|
19 |
\rail@end
|
|
20 |
\rail@begin{2}{name}
|
|
21 |
\rail@bar
|
3098
|
22 |
\rail@nont{id}[]
|
2657
|
23 |
\rail@nextbar{1}
|
3098
|
24 |
\rail@nont{string}[]
|
2657
|
25 |
\rail@endbar
|
|
26 |
\rail@end
|
|
27 |
\rail@begin{2}{extension}
|
|
28 |
\rail@plus
|
3098
|
29 |
\rail@nont{section}[]
|
2657
|
30 |
\rail@nextplus{1}
|
|
31 |
\rail@endplus
|
3098
|
32 |
\rail@term{end}[]
|
2657
|
33 |
\rail@bar
|
|
34 |
\rail@nextbar{1}
|
3098
|
35 |
\rail@nont{ml}[]
|
2657
|
36 |
\rail@endbar
|
|
37 |
\rail@end
|
5372
|
38 |
\rail@begin{17}{section}
|
2657
|
39 |
\rail@bar
|
3098
|
40 |
\rail@nont{classes}[]
|
2657
|
41 |
\rail@nextbar{1}
|
3098
|
42 |
\rail@nont{default}[]
|
2657
|
43 |
\rail@nextbar{2}
|
3098
|
44 |
\rail@nont{types}[]
|
2657
|
45 |
\rail@nextbar{3}
|
3098
|
46 |
\rail@nont{arities}[]
|
2657
|
47 |
\rail@nextbar{4}
|
5372
|
48 |
\rail@nont{nonterminals}[]
|
2657
|
49 |
\rail@nextbar{5}
|
5372
|
50 |
\rail@nont{consts}[]
|
|
51 |
\rail@nextbar{6}
|
3108
|
52 |
\rail@nont{syntax}[]
|
5372
|
53 |
\rail@nextbar{7}
|
3098
|
54 |
\rail@nont{trans}[]
|
5372
|
55 |
\rail@nextbar{8}
|
3098
|
56 |
\rail@nont{defs}[]
|
5372
|
57 |
\rail@nextbar{9}
|
3108
|
58 |
\rail@nont{constdefs}[]
|
5372
|
59 |
\rail@nextbar{10}
|
3098
|
60 |
\rail@nont{rules}[]
|
5372
|
61 |
\rail@nextbar{11}
|
3108
|
62 |
\rail@nont{axclass}[]
|
|
63 |
\rail@nextbar{12}
|
5372
|
64 |
\rail@nont{instance}[]
|
|
65 |
\rail@nextbar{13}
|
3098
|
66 |
\rail@nont{oracle}[]
|
5372
|
67 |
\rail@nextbar{14}
|
4543
|
68 |
\rail@nont{local}[]
|
5372
|
69 |
\rail@nextbar{15}
|
4543
|
70 |
\rail@nont{global}[]
|
5372
|
71 |
\rail@nextbar{16}
|
|
72 |
\rail@nont{setup}[]
|
2657
|
73 |
\rail@endbar
|
|
74 |
\rail@end
|
3108
|
75 |
\rail@begin{2}{classes}
|
3098
|
76 |
\rail@term{classes}[]
|
2657
|
77 |
\rail@plus
|
3108
|
78 |
\rail@nont{classDecl}[]
|
|
79 |
\rail@nextplus{1}
|
|
80 |
\rail@endplus
|
|
81 |
\rail@end
|
|
82 |
\rail@begin{3}{classDecl}
|
3098
|
83 |
\rail@nont{id}[]
|
2657
|
84 |
\rail@bar
|
|
85 |
\rail@nextbar{1}
|
3098
|
86 |
\rail@term{<}[]
|
2657
|
87 |
\rail@plus
|
3098
|
88 |
\rail@nont{id}[]
|
2657
|
89 |
\rail@nextplus{2}
|
3098
|
90 |
\rail@cterm{,}[]
|
2657
|
91 |
\rail@endplus
|
|
92 |
\rail@endbar
|
|
93 |
\rail@end
|
|
94 |
\rail@begin{1}{default}
|
3098
|
95 |
\rail@term{default}[]
|
|
96 |
\rail@nont{sort}[]
|
2657
|
97 |
\rail@end
|
|
98 |
\rail@begin{4}{sort}
|
|
99 |
\rail@bar
|
3098
|
100 |
\rail@nont{id}[]
|
2657
|
101 |
\rail@nextbar{1}
|
3098
|
102 |
\rail@token{lbrace}[]
|
2657
|
103 |
\rail@bar
|
|
104 |
\rail@nextbar{2}
|
|
105 |
\rail@plus
|
3098
|
106 |
\rail@nont{id}[]
|
2657
|
107 |
\rail@nextplus{3}
|
3098
|
108 |
\rail@cterm{,}[]
|
2657
|
109 |
\rail@endplus
|
|
110 |
\rail@endbar
|
3098
|
111 |
\rail@token{rbrace}[]
|
2657
|
112 |
\rail@endbar
|
|
113 |
\rail@end
|
|
114 |
\rail@begin{3}{types}
|
3098
|
115 |
\rail@term{types}[]
|
2657
|
116 |
\rail@plus
|
3098
|
117 |
\rail@nont{typeDecl}[]
|
2657
|
118 |
\rail@bar
|
|
119 |
\rail@nextbar{1}
|
3098
|
120 |
\rail@term{(}[]
|
|
121 |
\rail@nont{infix}[]
|
|
122 |
\rail@term{)}[]
|
2657
|
123 |
\rail@endbar
|
|
124 |
\rail@nextplus{2}
|
|
125 |
\rail@endplus
|
|
126 |
\rail@end
|
|
127 |
\rail@begin{2}{infix}
|
|
128 |
\rail@bar
|
3098
|
129 |
\rail@term{infixr}[]
|
2657
|
130 |
\rail@nextbar{1}
|
3098
|
131 |
\rail@term{infixl}[]
|
2657
|
132 |
\rail@endbar
|
3213
|
133 |
\rail@bar
|
|
134 |
\rail@nextbar{1}
|
|
135 |
\rail@nont{string}[]
|
|
136 |
\rail@endbar
|
3098
|
137 |
\rail@nont{nat}[]
|
2657
|
138 |
\rail@end
|
|
139 |
\rail@begin{3}{typeDecl}
|
3098
|
140 |
\rail@nont{typevarlist}[]
|
|
141 |
\rail@nont{name}[]
|
2657
|
142 |
\rail@bar
|
|
143 |
\rail@nextbar{1}
|
3098
|
144 |
\rail@term{=}[]
|
2657
|
145 |
\rail@bar
|
3098
|
146 |
\rail@nont{string}[]
|
2657
|
147 |
\rail@nextbar{2}
|
3098
|
148 |
\rail@nont{type}[]
|
2657
|
149 |
\rail@endbar
|
|
150 |
\rail@endbar
|
|
151 |
\rail@end
|
|
152 |
\rail@begin{4}{typevarlist}
|
|
153 |
\rail@bar
|
|
154 |
\rail@nextbar{1}
|
3098
|
155 |
\rail@nont{tid}[]
|
2657
|
156 |
\rail@nextbar{2}
|
3098
|
157 |
\rail@term{(}[]
|
2657
|
158 |
\rail@plus
|
3098
|
159 |
\rail@nont{tid}[]
|
2657
|
160 |
\rail@nextplus{3}
|
3098
|
161 |
\rail@cterm{,}[]
|
2657
|
162 |
\rail@endplus
|
3098
|
163 |
\rail@term{)}[]
|
2657
|
164 |
\rail@endbar
|
|
165 |
\rail@end
|
|
166 |
\rail@begin{5}{type}
|
|
167 |
\rail@bar
|
3098
|
168 |
\rail@nont{simpleType}[]
|
2657
|
169 |
\rail@nextbar{1}
|
3098
|
170 |
\rail@term{(}[]
|
|
171 |
\rail@nont{type}[]
|
|
172 |
\rail@term{)}[]
|
2657
|
173 |
\rail@nextbar{2}
|
3098
|
174 |
\rail@nont{type}[]
|
|
175 |
\rail@term{=>}[]
|
|
176 |
\rail@nont{type}[]
|
2657
|
177 |
\rail@nextbar{3}
|
3098
|
178 |
\rail@term{[}[]
|
2657
|
179 |
\rail@plus
|
3098
|
180 |
\rail@nont{type}[]
|
2657
|
181 |
\rail@nextplus{4}
|
3098
|
182 |
\rail@cterm{,}[]
|
2657
|
183 |
\rail@endplus
|
3098
|
184 |
\rail@term{]}[]
|
|
185 |
\rail@term{=>}[]
|
|
186 |
\rail@nont{type}[]
|
2657
|
187 |
\rail@endbar
|
|
188 |
\rail@end
|
|
189 |
\rail@begin{6}{simpleType}
|
|
190 |
\rail@bar
|
3098
|
191 |
\rail@nont{id}[]
|
2657
|
192 |
\rail@nextbar{1}
|
3098
|
193 |
\rail@nont{tid}[]
|
2657
|
194 |
\rail@bar
|
|
195 |
\rail@nextbar{2}
|
3098
|
196 |
\rail@term{::}[]
|
|
197 |
\rail@nont{id}[]
|
2657
|
198 |
\rail@endbar
|
|
199 |
\rail@nextbar{3}
|
3098
|
200 |
\rail@term{(}[]
|
2657
|
201 |
\rail@plus
|
3098
|
202 |
\rail@nont{type}[]
|
2657
|
203 |
\rail@nextplus{4}
|
3098
|
204 |
\rail@cterm{,}[]
|
2657
|
205 |
\rail@endplus
|
3098
|
206 |
\rail@term{)}[]
|
|
207 |
\rail@nont{id}[]
|
2657
|
208 |
\rail@nextbar{5}
|
3098
|
209 |
\rail@nont{simpleType}[]
|
|
210 |
\rail@nont{id}[]
|
2657
|
211 |
\rail@endbar
|
|
212 |
\rail@end
|
|
213 |
\rail@begin{3}{arities}
|
3098
|
214 |
\rail@term{arities}[]
|
2657
|
215 |
\rail@plus
|
|
216 |
\rail@plus
|
3098
|
217 |
\rail@nont{name}[]
|
2657
|
218 |
\rail@nextplus{1}
|
3098
|
219 |
\rail@cterm{,}[]
|
2657
|
220 |
\rail@endplus
|
3098
|
221 |
\rail@term{::}[]
|
|
222 |
\rail@nont{arity}[]
|
2657
|
223 |
\rail@nextplus{2}
|
|
224 |
\rail@endplus
|
|
225 |
\rail@end
|
|
226 |
\rail@begin{3}{arity}
|
|
227 |
\rail@bar
|
|
228 |
\rail@nextbar{1}
|
3098
|
229 |
\rail@term{(}[]
|
2657
|
230 |
\rail@plus
|
3098
|
231 |
\rail@nont{sort}[]
|
2657
|
232 |
\rail@nextplus{2}
|
3098
|
233 |
\rail@cterm{,}[]
|
2657
|
234 |
\rail@endplus
|
3098
|
235 |
\rail@term{)}[]
|
2657
|
236 |
\rail@endbar
|
3108
|
237 |
\rail@nont{sort}[]
|
2657
|
238 |
\rail@end
|
5372
|
239 |
\rail@begin{2}{nonterminals}
|
|
240 |
\rail@term{nonterminals}[]
|
|
241 |
\rail@plus
|
|
242 |
\rail@nont{name}[]
|
|
243 |
\rail@nextplus{1}
|
|
244 |
\rail@endplus
|
|
245 |
\rail@end
|
3108
|
246 |
\rail@begin{2}{consts}
|
3098
|
247 |
\rail@term{consts}[]
|
2657
|
248 |
\rail@plus
|
3108
|
249 |
\rail@nont{mixfixConstDecl}[]
|
|
250 |
\rail@nextplus{1}
|
|
251 |
\rail@endplus
|
|
252 |
\rail@end
|
|
253 |
\rail@begin{2}{syntax}
|
|
254 |
\rail@term{syntax}[]
|
|
255 |
\rail@bar
|
|
256 |
\rail@nextbar{1}
|
|
257 |
\rail@nont{mode}[]
|
|
258 |
\rail@endbar
|
|
259 |
\rail@plus
|
|
260 |
\rail@nont{mixfixConstDecl}[]
|
|
261 |
\rail@nextplus{1}
|
|
262 |
\rail@endplus
|
|
263 |
\rail@end
|
|
264 |
\rail@begin{2}{mode}
|
|
265 |
\rail@term{(}[]
|
|
266 |
\rail@nont{name}[]
|
|
267 |
\rail@bar
|
|
268 |
\rail@nextbar{1}
|
|
269 |
\rail@term{output}[]
|
|
270 |
\rail@endbar
|
|
271 |
\rail@term{)}[]
|
|
272 |
\rail@end
|
|
273 |
\rail@begin{2}{mixfixConstDecl}
|
3098
|
274 |
\rail@nont{constDecl}[]
|
2657
|
275 |
\rail@bar
|
|
276 |
\rail@nextbar{1}
|
3098
|
277 |
\rail@term{(}[]
|
|
278 |
\rail@nont{mixfix}[]
|
|
279 |
\rail@term{)}[]
|
2657
|
280 |
\rail@endbar
|
|
281 |
\rail@end
|
|
282 |
\rail@begin{2}{constDecl}
|
|
283 |
\rail@plus
|
3098
|
284 |
\rail@nont{name}[]
|
2657
|
285 |
\rail@nextplus{1}
|
3098
|
286 |
\rail@cterm{,}[]
|
2657
|
287 |
\rail@endplus
|
3098
|
288 |
\rail@term{::}[]
|
2657
|
289 |
\rail@bar
|
3098
|
290 |
\rail@nont{string}[]
|
2657
|
291 |
\rail@nextbar{1}
|
3098
|
292 |
\rail@nont{type}[]
|
2657
|
293 |
\rail@endbar
|
|
294 |
\rail@end
|
3213
|
295 |
\rail@begin{6}{mixfix}
|
2657
|
296 |
\rail@bar
|
3098
|
297 |
\rail@nont{string}[]
|
2657
|
298 |
\rail@bar
|
|
299 |
\rail@nextbar{1}
|
|
300 |
\rail@bar
|
|
301 |
\rail@nextbar{2}
|
3098
|
302 |
\rail@term{[}[]
|
2657
|
303 |
\rail@plus
|
3098
|
304 |
\rail@nont{nat}[]
|
2657
|
305 |
\rail@nextplus{3}
|
3098
|
306 |
\rail@cterm{,}[]
|
2657
|
307 |
\rail@endplus
|
3098
|
308 |
\rail@term{]}[]
|
2657
|
309 |
\rail@endbar
|
3098
|
310 |
\rail@nont{nat}[]
|
2657
|
311 |
\rail@endbar
|
|
312 |
\rail@nextbar{4}
|
3213
|
313 |
\rail@nont{infix}[]
|
2657
|
314 |
\rail@nextbar{5}
|
3098
|
315 |
\rail@term{binder}[]
|
|
316 |
\rail@nont{string}[]
|
|
317 |
\rail@nont{nat}[]
|
2657
|
318 |
\rail@endbar
|
|
319 |
\rail@end
|
|
320 |
\rail@begin{4}{trans}
|
3098
|
321 |
\rail@term{translations}[]
|
2657
|
322 |
\rail@plus
|
3098
|
323 |
\rail@nont{pat}[]
|
2657
|
324 |
\rail@bar
|
3098
|
325 |
\rail@term{==}[]
|
2657
|
326 |
\rail@nextbar{1}
|
3098
|
327 |
\rail@term{=>}[]
|
2657
|
328 |
\rail@nextbar{2}
|
3098
|
329 |
\rail@term{<=}[]
|
2657
|
330 |
\rail@endbar
|
3098
|
331 |
\rail@nont{pat}[]
|
2657
|
332 |
\rail@nextplus{3}
|
|
333 |
\rail@endplus
|
|
334 |
\rail@end
|
|
335 |
\rail@begin{2}{pat}
|
|
336 |
\rail@bar
|
|
337 |
\rail@nextbar{1}
|
3098
|
338 |
\rail@term{(}[]
|
|
339 |
\rail@nont{id}[]
|
|
340 |
\rail@term{)}[]
|
2657
|
341 |
\rail@endbar
|
3098
|
342 |
\rail@nont{string}[]
|
2657
|
343 |
\rail@end
|
|
344 |
\rail@begin{2}{rules}
|
3098
|
345 |
\rail@term{rules}[]
|
2657
|
346 |
\rail@plus
|
3098
|
347 |
\rail@nont{id}[]
|
|
348 |
\rail@nont{string}[]
|
2657
|
349 |
\rail@nextplus{1}
|
|
350 |
\rail@endplus
|
|
351 |
\rail@end
|
|
352 |
\rail@begin{2}{defs}
|
3098
|
353 |
\rail@term{defs}[]
|
2657
|
354 |
\rail@plus
|
3098
|
355 |
\rail@nont{id}[]
|
|
356 |
\rail@nont{string}[]
|
2657
|
357 |
\rail@nextplus{1}
|
|
358 |
\rail@endplus
|
|
359 |
\rail@end
|
3108
|
360 |
\rail@begin{3}{constdefs}
|
|
361 |
\rail@term{constdefs}[]
|
|
362 |
\rail@plus
|
4543
|
363 |
\rail@nont{name}[]
|
3108
|
364 |
\rail@term{::}[]
|
|
365 |
\rail@bar
|
|
366 |
\rail@nont{string}[]
|
|
367 |
\rail@nextbar{1}
|
|
368 |
\rail@nont{type}[]
|
|
369 |
\rail@endbar
|
4891
|
370 |
\rail@bar
|
|
371 |
\rail@nextbar{1}
|
|
372 |
\rail@nont{mixfix}[]
|
|
373 |
\rail@endbar
|
3108
|
374 |
\rail@nont{string}[]
|
|
375 |
\rail@nextplus{2}
|
|
376 |
\rail@endplus
|
|
377 |
\rail@end
|
|
378 |
\rail@begin{3}{axclass}
|
|
379 |
\rail@term{axclass}[]
|
|
380 |
\rail@nont{classDecl}[]
|
|
381 |
\rail@bar
|
|
382 |
\rail@nextbar{1}
|
|
383 |
\rail@plus
|
|
384 |
\rail@nont{id}[]
|
|
385 |
\rail@nont{string}[]
|
|
386 |
\rail@nextplus{2}
|
|
387 |
\rail@endplus
|
|
388 |
\rail@endbar
|
|
389 |
\rail@end
|
|
390 |
\rail@begin{2}{instance}
|
|
391 |
\rail@term{instance}[]
|
|
392 |
\rail@bar
|
|
393 |
\rail@nont{name}[]
|
|
394 |
\rail@term{<}[]
|
|
395 |
\rail@nont{name}[]
|
|
396 |
\rail@nextbar{1}
|
|
397 |
\rail@nont{name}[]
|
|
398 |
\rail@term{::}[]
|
|
399 |
\rail@nont{arity}[]
|
|
400 |
\rail@endbar
|
|
401 |
\rail@nont{witness}[]
|
|
402 |
\rail@end
|
5372
|
403 |
\rail@begin{5}{witness}
|
3108
|
404 |
\rail@bar
|
|
405 |
\rail@nextbar{1}
|
3129
|
406 |
\rail@term{(}[]
|
3108
|
407 |
\rail@plus
|
|
408 |
\rail@bar
|
|
409 |
\rail@nont{string}[]
|
|
410 |
\rail@nextbar{2}
|
5372
|
411 |
\rail@nont{id}[]
|
|
412 |
\rail@nextbar{3}
|
3108
|
413 |
\rail@nont{longident}[]
|
|
414 |
\rail@endbar
|
5372
|
415 |
\rail@nextplus{4}
|
3108
|
416 |
\rail@cterm{,}[]
|
|
417 |
\rail@endplus
|
3129
|
418 |
\rail@term{)}[]
|
3108
|
419 |
\rail@endbar
|
|
420 |
\rail@bar
|
|
421 |
\rail@nextbar{1}
|
|
422 |
\rail@nont{verbatim}[]
|
|
423 |
\rail@endbar
|
|
424 |
\rail@end
|
2657
|
425 |
\rail@begin{1}{oracle}
|
3098
|
426 |
\rail@term{oracle}[]
|
|
427 |
\rail@nont{name}[]
|
4316
|
428 |
\rail@term{=}[]
|
|
429 |
\rail@nont{name}[]
|
2657
|
430 |
\rail@end
|
4543
|
431 |
\rail@begin{1}{local}
|
|
432 |
\rail@term{local}[]
|
|
433 |
\rail@end
|
|
434 |
\rail@begin{1}{global}
|
|
435 |
\rail@term{global}[]
|
|
436 |
\rail@end
|
5372
|
437 |
\rail@begin{2}{setup}
|
|
438 |
\rail@term{setup}[]
|
|
439 |
\rail@bar
|
|
440 |
\rail@nont{id}[]
|
|
441 |
\rail@nextbar{1}
|
|
442 |
\rail@nont{longident}[]
|
|
443 |
\rail@endbar
|
|
444 |
\rail@end
|
2657
|
445 |
\rail@begin{1}{ml}
|
3098
|
446 |
\rail@term{ML}[]
|
|
447 |
\rail@nont{text}[]
|
2657
|
448 |
\rail@end
|
|
449 |
}
|