| changeset 3108 | 335efc3f5632 |
| parent 3098 | a31170b67367 |
| child 3129 | dd3666cbc764 |
| 3107:492a3d5d2b17 | 3108:335efc3f5632 |
|---|---|
1 % This file was generated by '/usr/stud/berghofe/latex/rail/rail' from 'ref.rai' |
1 % This file was generated by 'rail' from 'ref.rai' |
2 \rail@t {lbrace} |
2 \rail@t {lbrace} |
3 \rail@t {rbrace} |
3 \rail@t {rbrace} |
4 \rail@i {1}{ \par theoryDef : id '=' (name + '+') ('+' extension | ()); \par name: id | string; \par extension : (section +) 'end' ( () | ml ); \par section : classes | default | types | arities | consts | constdefs | trans | defs | rules | oracle ; \par classes : 'classes' ( ( id ( () | '<' (id + ',') ) ) + ) ; \par default : 'default' sort ; \par sort : id | lbrace (id * ',') rbrace ; \par types : 'types' ( ( typeDecl ( () | '(' infix ')' ) ) + ) ; \par infix : ( 'infixr' | 'infixl' ) 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 \par arities : 'arities' ((( name + ',' ) '::' arity ) + ) ; \par arity : ( () | '(' (sort + ',') ')' ) id ; \par \par consts : 'consts' ( ( constDecl ( () | ( '(' mixfix ')' ) ) ) + ) ; \par constDecl : ( name + ',') '::' (string | type); \par mixfix : string ( () | ( () | ('[' (nat + ',') ']')) nat ) | infix | 'binder' string nat ; \par constdefs : 'constdefs' (id '::' (string | type) string +) ; \par trans : 'translations' ( pat ( '==' | '=>' | '<=' ) pat + ) ; \par pat : ( () | ( '(' id ')' ) ) string; \par rules : 'rules' (( id string ) + ) ; \par defs : 'defs' (( id string ) + ) ; \par oracle : 'oracle' name ; \par ml : 'ML' text ; \par } |
4 \rail@i {1}{ \par theoryDef : id '=' (name + '+') ('+' extension | ()) ; \par name: id | string ; \par extension : (section +) 'end' ( () | ml ) ; \par section : classes | default | types | arities | consts | syntax | trans | defs | constdefs | rules | axclass | instance | oracle ; \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' ) 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 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 ) | ( 'infixr' | 'infixl' ) (() | string) nat | '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' (id '::' (string | type) string +) ; \par axclass : 'axclass' classDecl (() | ( id string ) +) ; \par instance : 'instance' ( name '<' name | name '::' arity) witness ; \par witness : (() | ((string | longident) + ',')) (() | verbatim) ; \par oracle : 'oracle' name ; \par ml : 'ML' text ; \par } |
5 \rail@o {1}{ |
5 \rail@o {1}{ |
6 \rail@begin{2}{theoryDef} |
6 \rail@begin{2}{theoryDef} |
7 \rail@nont{id}[] |
7 \rail@nont{id}[] |
8 \rail@term{=}[] |
8 \rail@term{=}[] |
9 \rail@plus |
9 \rail@plus |
33 \rail@bar |
33 \rail@bar |
34 \rail@nextbar{1} |
34 \rail@nextbar{1} |
35 \rail@nont{ml}[] |
35 \rail@nont{ml}[] |
36 \rail@endbar |
36 \rail@endbar |
37 \rail@end |
37 \rail@end |
38 \rail@begin{10}{section} |
38 \rail@begin{13}{section} |
39 \rail@bar |
39 \rail@bar |
40 \rail@nont{classes}[] |
40 \rail@nont{classes}[] |
41 \rail@nextbar{1} |
41 \rail@nextbar{1} |
42 \rail@nont{default}[] |
42 \rail@nont{default}[] |
43 \rail@nextbar{2} |
43 \rail@nextbar{2} |
45 \rail@nextbar{3} |
45 \rail@nextbar{3} |
46 \rail@nont{arities}[] |
46 \rail@nont{arities}[] |
47 \rail@nextbar{4} |
47 \rail@nextbar{4} |
48 \rail@nont{consts}[] |
48 \rail@nont{consts}[] |
49 \rail@nextbar{5} |
49 \rail@nextbar{5} |
50 \rail@nont{constdefs}[] |
50 \rail@nont{syntax}[] |
51 \rail@nextbar{6} |
51 \rail@nextbar{6} |
52 \rail@nont{trans}[] |
52 \rail@nont{trans}[] |
53 \rail@nextbar{7} |
53 \rail@nextbar{7} |
54 \rail@nont{defs}[] |
54 \rail@nont{defs}[] |
55 \rail@nextbar{8} |
55 \rail@nextbar{8} |
56 \rail@nont{constdefs}[] |
|
57 \rail@nextbar{9} |
|
56 \rail@nont{rules}[] |
58 \rail@nont{rules}[] |
57 \rail@nextbar{9} |
59 \rail@nextbar{10} |
60 \rail@nont{axclass}[] |
|
61 \rail@nextbar{11} |
|
62 \rail@nont{instance}[] |
|
63 \rail@nextbar{12} |
|
58 \rail@nont{oracle}[] |
64 \rail@nont{oracle}[] |
59 \rail@endbar |
65 \rail@endbar |
60 \rail@end |
66 \rail@end |
61 \rail@begin{4}{classes} |
67 \rail@begin{2}{classes} |
62 \rail@term{classes}[] |
68 \rail@term{classes}[] |
63 \rail@plus |
69 \rail@plus |
70 \rail@nont{classDecl}[] |
|
71 \rail@nextplus{1} |
|
72 \rail@endplus |
|
73 \rail@end |
|
74 \rail@begin{3}{classDecl} |
|
64 \rail@nont{id}[] |
75 \rail@nont{id}[] |
65 \rail@bar |
76 \rail@bar |
66 \rail@nextbar{1} |
77 \rail@nextbar{1} |
67 \rail@term{<}[] |
78 \rail@term{<}[] |
68 \rail@plus |
79 \rail@plus |
69 \rail@nont{id}[] |
80 \rail@nont{id}[] |
70 \rail@nextplus{2} |
81 \rail@nextplus{2} |
71 \rail@cterm{,}[] |
82 \rail@cterm{,}[] |
72 \rail@endplus |
83 \rail@endplus |
73 \rail@endbar |
84 \rail@endbar |
74 \rail@nextplus{3} |
|
75 \rail@endplus |
|
76 \rail@end |
85 \rail@end |
77 \rail@begin{1}{default} |
86 \rail@begin{1}{default} |
78 \rail@term{default}[] |
87 \rail@term{default}[] |
79 \rail@nont{sort}[] |
88 \rail@nont{sort}[] |
80 \rail@end |
89 \rail@end |
211 \rail@nextplus{2} |
220 \rail@nextplus{2} |
212 \rail@cterm{,}[] |
221 \rail@cterm{,}[] |
213 \rail@endplus |
222 \rail@endplus |
214 \rail@term{)}[] |
223 \rail@term{)}[] |
215 \rail@endbar |
224 \rail@endbar |
216 \rail@nont{id}[] |
225 \rail@nont{sort}[] |
217 \rail@end |
226 \rail@end |
218 \rail@begin{3}{consts} |
227 \rail@begin{2}{consts} |
219 \rail@term{consts}[] |
228 \rail@term{consts}[] |
220 \rail@plus |
229 \rail@plus |
230 \rail@nont{mixfixConstDecl}[] |
|
231 \rail@nextplus{1} |
|
232 \rail@endplus |
|
233 \rail@end |
|
234 \rail@begin{2}{syntax} |
|
235 \rail@term{syntax}[] |
|
236 \rail@bar |
|
237 \rail@nextbar{1} |
|
238 \rail@nont{mode}[] |
|
239 \rail@endbar |
|
240 \rail@plus |
|
241 \rail@nont{mixfixConstDecl}[] |
|
242 \rail@nextplus{1} |
|
243 \rail@endplus |
|
244 \rail@end |
|
245 \rail@begin{2}{mode} |
|
246 \rail@term{(}[] |
|
247 \rail@nont{name}[] |
|
248 \rail@bar |
|
249 \rail@nextbar{1} |
|
250 \rail@term{output}[] |
|
251 \rail@endbar |
|
252 \rail@term{)}[] |
|
253 \rail@end |
|
254 \rail@begin{2}{mixfixConstDecl} |
|
221 \rail@nont{constDecl}[] |
255 \rail@nont{constDecl}[] |
222 \rail@bar |
256 \rail@bar |
223 \rail@nextbar{1} |
257 \rail@nextbar{1} |
224 \rail@term{(}[] |
258 \rail@term{(}[] |
225 \rail@nont{mixfix}[] |
259 \rail@nont{mixfix}[] |
226 \rail@term{)}[] |
260 \rail@term{)}[] |
227 \rail@endbar |
261 \rail@endbar |
228 \rail@nextplus{2} |
|
229 \rail@endplus |
|
230 \rail@end |
262 \rail@end |
231 \rail@begin{2}{constDecl} |
263 \rail@begin{2}{constDecl} |
232 \rail@plus |
264 \rail@plus |
233 \rail@nont{name}[] |
265 \rail@nont{name}[] |
234 \rail@nextplus{1} |
266 \rail@nextplus{1} |
239 \rail@nont{string}[] |
271 \rail@nont{string}[] |
240 \rail@nextbar{1} |
272 \rail@nextbar{1} |
241 \rail@nont{type}[] |
273 \rail@nont{type}[] |
242 \rail@endbar |
274 \rail@endbar |
243 \rail@end |
275 \rail@end |
244 \rail@begin{6}{mixfix} |
276 \rail@begin{7}{mixfix} |
245 \rail@bar |
277 \rail@bar |
246 \rail@nont{string}[] |
278 \rail@nont{string}[] |
247 \rail@bar |
279 \rail@bar |
248 \rail@nextbar{1} |
280 \rail@nextbar{1} |
249 \rail@bar |
281 \rail@bar |
257 \rail@term{]}[] |
289 \rail@term{]}[] |
258 \rail@endbar |
290 \rail@endbar |
259 \rail@nont{nat}[] |
291 \rail@nont{nat}[] |
260 \rail@endbar |
292 \rail@endbar |
261 \rail@nextbar{4} |
293 \rail@nextbar{4} |
262 \rail@nont{infix}[] |
294 \rail@bar |
295 \rail@term{infixr}[] |
|
263 \rail@nextbar{5} |
296 \rail@nextbar{5} |
297 \rail@term{infixl}[] |
|
298 \rail@endbar |
|
299 \rail@bar |
|
300 \rail@nextbar{5} |
|
301 \rail@nont{string}[] |
|
302 \rail@endbar |
|
303 \rail@nont{nat}[] |
|
304 \rail@nextbar{6} |
|
264 \rail@term{binder}[] |
305 \rail@term{binder}[] |
265 \rail@nont{string}[] |
306 \rail@nont{string}[] |
266 \rail@nont{nat}[] |
307 \rail@nont{nat}[] |
267 \rail@endbar |
308 \rail@endbar |
309 \rail@end |
|
310 \rail@begin{4}{trans} |
|
311 \rail@term{translations}[] |
|
312 \rail@plus |
|
313 \rail@nont{pat}[] |
|
314 \rail@bar |
|
315 \rail@term{==}[] |
|
316 \rail@nextbar{1} |
|
317 \rail@term{=>}[] |
|
318 \rail@nextbar{2} |
|
319 \rail@term{<=}[] |
|
320 \rail@endbar |
|
321 \rail@nont{pat}[] |
|
322 \rail@nextplus{3} |
|
323 \rail@endplus |
|
324 \rail@end |
|
325 \rail@begin{2}{pat} |
|
326 \rail@bar |
|
327 \rail@nextbar{1} |
|
328 \rail@term{(}[] |
|
329 \rail@nont{id}[] |
|
330 \rail@term{)}[] |
|
331 \rail@endbar |
|
332 \rail@nont{string}[] |
|
333 \rail@end |
|
334 \rail@begin{2}{rules} |
|
335 \rail@term{rules}[] |
|
336 \rail@plus |
|
337 \rail@nont{id}[] |
|
338 \rail@nont{string}[] |
|
339 \rail@nextplus{1} |
|
340 \rail@endplus |
|
341 \rail@end |
|
342 \rail@begin{2}{defs} |
|
343 \rail@term{defs}[] |
|
344 \rail@plus |
|
345 \rail@nont{id}[] |
|
346 \rail@nont{string}[] |
|
347 \rail@nextplus{1} |
|
348 \rail@endplus |
|
268 \rail@end |
349 \rail@end |
269 \rail@begin{3}{constdefs} |
350 \rail@begin{3}{constdefs} |
270 \rail@term{constdefs}[] |
351 \rail@term{constdefs}[] |
271 \rail@plus |
352 \rail@plus |
272 \rail@nont{id}[] |
353 \rail@nont{id}[] |
278 \rail@endbar |
359 \rail@endbar |
279 \rail@nont{string}[] |
360 \rail@nont{string}[] |
280 \rail@nextplus{2} |
361 \rail@nextplus{2} |
281 \rail@endplus |
362 \rail@endplus |
282 \rail@end |
363 \rail@end |
283 \rail@begin{4}{trans} |
364 \rail@begin{3}{axclass} |
284 \rail@term{translations}[] |
365 \rail@term{axclass}[] |
285 \rail@plus |
366 \rail@nont{classDecl}[] |
286 \rail@nont{pat}[] |
367 \rail@bar |
287 \rail@bar |
368 \rail@nextbar{1} |
288 \rail@term{==}[] |
369 \rail@plus |
289 \rail@nextbar{1} |
370 \rail@nont{id}[] |
290 \rail@term{=>}[] |
371 \rail@nont{string}[] |
291 \rail@nextbar{2} |
372 \rail@nextplus{2} |
292 \rail@term{<=}[] |
373 \rail@endplus |
293 \rail@endbar |
374 \rail@endbar |
294 \rail@nont{pat}[] |
375 \rail@end |
376 \rail@begin{2}{instance} |
|
377 \rail@term{instance}[] |
|
378 \rail@bar |
|
379 \rail@nont{name}[] |
|
380 \rail@term{<}[] |
|
381 \rail@nont{name}[] |
|
382 \rail@nextbar{1} |
|
383 \rail@nont{name}[] |
|
384 \rail@term{::}[] |
|
385 \rail@nont{arity}[] |
|
386 \rail@endbar |
|
387 \rail@nont{witness}[] |
|
388 \rail@end |
|
389 \rail@begin{4}{witness} |
|
390 \rail@bar |
|
391 \rail@nextbar{1} |
|
392 \rail@plus |
|
393 \rail@bar |
|
394 \rail@nont{string}[] |
|
395 \rail@nextbar{2} |
|
396 \rail@nont{longident}[] |
|
397 \rail@endbar |
|
295 \rail@nextplus{3} |
398 \rail@nextplus{3} |
296 \rail@endplus |
399 \rail@cterm{,}[] |
297 \rail@end |
400 \rail@endplus |
298 \rail@begin{2}{pat} |
401 \rail@endbar |
299 \rail@bar |
402 \rail@bar |
300 \rail@nextbar{1} |
403 \rail@nextbar{1} |
301 \rail@term{(}[] |
404 \rail@nont{verbatim}[] |
302 \rail@nont{id}[] |
405 \rail@endbar |
303 \rail@term{)}[] |
|
304 \rail@endbar |
|
305 \rail@nont{string}[] |
|
306 \rail@end |
|
307 \rail@begin{2}{rules} |
|
308 \rail@term{rules}[] |
|
309 \rail@plus |
|
310 \rail@nont{id}[] |
|
311 \rail@nont{string}[] |
|
312 \rail@nextplus{1} |
|
313 \rail@endplus |
|
314 \rail@end |
|
315 \rail@begin{2}{defs} |
|
316 \rail@term{defs}[] |
|
317 \rail@plus |
|
318 \rail@nont{id}[] |
|
319 \rail@nont{string}[] |
|
320 \rail@nextplus{1} |
|
321 \rail@endplus |
|
322 \rail@end |
406 \rail@end |
323 \rail@begin{1}{oracle} |
407 \rail@begin{1}{oracle} |
324 \rail@term{oracle}[] |
408 \rail@term{oracle}[] |
325 \rail@nont{name}[] |
409 \rail@nont{name}[] |
326 \rail@end |
410 \rail@end |