|
1 % This file was generated by 'rail' from 'ref.rai' |
|
2 \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 | '\protect \relax $\mathsurround =\z@ \delimiter "4266308 $' (id * ',') '\protect \relax $\mathsurround =\z@ \delimiter "5267309 $' ; \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 } |
|
3 \rail@o {1}{ |
|
4 \rail@begin{2}{theoryDef} |
|
5 \rail@nont{id} |
|
6 \rail@term{=} |
|
7 \rail@plus |
|
8 \rail@nont{name} |
|
9 \rail@nextplus{1} |
|
10 \rail@cterm{+} |
|
11 \rail@endplus |
|
12 \rail@bar |
|
13 \rail@term{+} |
|
14 \rail@nont{extension} |
|
15 \rail@nextbar{1} |
|
16 \rail@endbar |
|
17 \rail@end |
|
18 \rail@begin{2}{name} |
|
19 \rail@bar |
|
20 \rail@nont{id} |
|
21 \rail@nextbar{1} |
|
22 \rail@nont{string} |
|
23 \rail@endbar |
|
24 \rail@end |
|
25 \rail@begin{2}{extension} |
|
26 \rail@plus |
|
27 \rail@nont{section} |
|
28 \rail@nextplus{1} |
|
29 \rail@endplus |
|
30 \rail@term{end} |
|
31 \rail@bar |
|
32 \rail@nextbar{1} |
|
33 \rail@nont{ml} |
|
34 \rail@endbar |
|
35 \rail@end |
|
36 \rail@begin{10}{section} |
|
37 \rail@bar |
|
38 \rail@nont{classes} |
|
39 \rail@nextbar{1} |
|
40 \rail@nont{default} |
|
41 \rail@nextbar{2} |
|
42 \rail@nont{types} |
|
43 \rail@nextbar{3} |
|
44 \rail@nont{arities} |
|
45 \rail@nextbar{4} |
|
46 \rail@nont{consts} |
|
47 \rail@nextbar{5} |
|
48 \rail@nont{constdefs} |
|
49 \rail@nextbar{6} |
|
50 \rail@nont{trans} |
|
51 \rail@nextbar{7} |
|
52 \rail@nont{defs} |
|
53 \rail@nextbar{8} |
|
54 \rail@nont{rules} |
|
55 \rail@nextbar{9} |
|
56 \rail@nont{oracle} |
|
57 \rail@endbar |
|
58 \rail@end |
|
59 \rail@begin{4}{classes} |
|
60 \rail@term{classes} |
|
61 \rail@plus |
|
62 \rail@nont{id} |
|
63 \rail@bar |
|
64 \rail@nextbar{1} |
|
65 \rail@term{<} |
|
66 \rail@plus |
|
67 \rail@nont{id} |
|
68 \rail@nextplus{2} |
|
69 \rail@cterm{,} |
|
70 \rail@endplus |
|
71 \rail@endbar |
|
72 \rail@nextplus{3} |
|
73 \rail@endplus |
|
74 \rail@end |
|
75 \rail@begin{1}{default} |
|
76 \rail@term{default} |
|
77 \rail@nont{sort} |
|
78 \rail@end |
|
79 \rail@begin{4}{sort} |
|
80 \rail@bar |
|
81 \rail@nont{id} |
|
82 \rail@nextbar{1} |
|
83 \rail@term{\protect \relax $\mathsurround =\z@ \delimiter "4266308 $} |
|
84 \rail@bar |
|
85 \rail@nextbar{2} |
|
86 \rail@plus |
|
87 \rail@nont{id} |
|
88 \rail@nextplus{3} |
|
89 \rail@cterm{,} |
|
90 \rail@endplus |
|
91 \rail@endbar |
|
92 \rail@term{\protect \relax $\mathsurround =\z@ \delimiter "5267309 $} |
|
93 \rail@endbar |
|
94 \rail@end |
|
95 \rail@begin{3}{types} |
|
96 \rail@term{types} |
|
97 \rail@plus |
|
98 \rail@nont{typeDecl} |
|
99 \rail@bar |
|
100 \rail@nextbar{1} |
|
101 \rail@term{(} |
|
102 \rail@nont{infix} |
|
103 \rail@term{)} |
|
104 \rail@endbar |
|
105 \rail@nextplus{2} |
|
106 \rail@endplus |
|
107 \rail@end |
|
108 \rail@begin{2}{infix} |
|
109 \rail@bar |
|
110 \rail@term{infixr} |
|
111 \rail@nextbar{1} |
|
112 \rail@term{infixl} |
|
113 \rail@endbar |
|
114 \rail@nont{nat} |
|
115 \rail@end |
|
116 \rail@begin{3}{typeDecl} |
|
117 \rail@nont{typevarlist} |
|
118 \rail@nont{name} |
|
119 \rail@bar |
|
120 \rail@nextbar{1} |
|
121 \rail@term{=} |
|
122 \rail@bar |
|
123 \rail@nont{string} |
|
124 \rail@nextbar{2} |
|
125 \rail@nont{type} |
|
126 \rail@endbar |
|
127 \rail@endbar |
|
128 \rail@end |
|
129 \rail@begin{4}{typevarlist} |
|
130 \rail@bar |
|
131 \rail@nextbar{1} |
|
132 \rail@nont{tid} |
|
133 \rail@nextbar{2} |
|
134 \rail@term{(} |
|
135 \rail@plus |
|
136 \rail@nont{tid} |
|
137 \rail@nextplus{3} |
|
138 \rail@cterm{,} |
|
139 \rail@endplus |
|
140 \rail@term{)} |
|
141 \rail@endbar |
|
142 \rail@end |
|
143 \rail@begin{5}{type} |
|
144 \rail@bar |
|
145 \rail@nont{simpleType} |
|
146 \rail@nextbar{1} |
|
147 \rail@term{(} |
|
148 \rail@nont{type} |
|
149 \rail@term{)} |
|
150 \rail@nextbar{2} |
|
151 \rail@nont{type} |
|
152 \rail@term{=>} |
|
153 \rail@nont{type} |
|
154 \rail@nextbar{3} |
|
155 \rail@term{[} |
|
156 \rail@plus |
|
157 \rail@nont{type} |
|
158 \rail@nextplus{4} |
|
159 \rail@cterm{,} |
|
160 \rail@endplus |
|
161 \rail@term{]} |
|
162 \rail@term{=>} |
|
163 \rail@nont{type} |
|
164 \rail@endbar |
|
165 \rail@end |
|
166 \rail@begin{6}{simpleType} |
|
167 \rail@bar |
|
168 \rail@nont{id} |
|
169 \rail@nextbar{1} |
|
170 \rail@nont{tid} |
|
171 \rail@bar |
|
172 \rail@nextbar{2} |
|
173 \rail@term{::} |
|
174 \rail@nont{id} |
|
175 \rail@endbar |
|
176 \rail@nextbar{3} |
|
177 \rail@term{(} |
|
178 \rail@plus |
|
179 \rail@nont{type} |
|
180 \rail@nextplus{4} |
|
181 \rail@cterm{,} |
|
182 \rail@endplus |
|
183 \rail@term{)} |
|
184 \rail@nont{id} |
|
185 \rail@nextbar{5} |
|
186 \rail@nont{simpleType} |
|
187 \rail@nont{id} |
|
188 \rail@endbar |
|
189 \rail@end |
|
190 \rail@begin{3}{arities} |
|
191 \rail@term{arities} |
|
192 \rail@plus |
|
193 \rail@plus |
|
194 \rail@nont{name} |
|
195 \rail@nextplus{1} |
|
196 \rail@cterm{,} |
|
197 \rail@endplus |
|
198 \rail@term{::} |
|
199 \rail@nont{arity} |
|
200 \rail@nextplus{2} |
|
201 \rail@endplus |
|
202 \rail@end |
|
203 \rail@begin{3}{arity} |
|
204 \rail@bar |
|
205 \rail@nextbar{1} |
|
206 \rail@term{(} |
|
207 \rail@plus |
|
208 \rail@nont{sort} |
|
209 \rail@nextplus{2} |
|
210 \rail@cterm{,} |
|
211 \rail@endplus |
|
212 \rail@term{)} |
|
213 \rail@endbar |
|
214 \rail@nont{id} |
|
215 \rail@end |
|
216 \rail@begin{3}{consts} |
|
217 \rail@term{consts} |
|
218 \rail@plus |
|
219 \rail@nont{constDecl} |
|
220 \rail@bar |
|
221 \rail@nextbar{1} |
|
222 \rail@term{(} |
|
223 \rail@nont{mixfix} |
|
224 \rail@term{)} |
|
225 \rail@endbar |
|
226 \rail@nextplus{2} |
|
227 \rail@endplus |
|
228 \rail@end |
|
229 \rail@begin{2}{constDecl} |
|
230 \rail@plus |
|
231 \rail@nont{name} |
|
232 \rail@nextplus{1} |
|
233 \rail@cterm{,} |
|
234 \rail@endplus |
|
235 \rail@term{::} |
|
236 \rail@bar |
|
237 \rail@nont{string} |
|
238 \rail@nextbar{1} |
|
239 \rail@nont{type} |
|
240 \rail@endbar |
|
241 \rail@end |
|
242 \rail@begin{6}{mixfix} |
|
243 \rail@bar |
|
244 \rail@nont{string} |
|
245 \rail@bar |
|
246 \rail@nextbar{1} |
|
247 \rail@bar |
|
248 \rail@nextbar{2} |
|
249 \rail@term{[} |
|
250 \rail@plus |
|
251 \rail@nont{nat} |
|
252 \rail@nextplus{3} |
|
253 \rail@cterm{,} |
|
254 \rail@endplus |
|
255 \rail@term{]} |
|
256 \rail@endbar |
|
257 \rail@nont{nat} |
|
258 \rail@endbar |
|
259 \rail@nextbar{4} |
|
260 \rail@nont{infix} |
|
261 \rail@nextbar{5} |
|
262 \rail@term{binder} |
|
263 \rail@nont{string} |
|
264 \rail@nont{nat} |
|
265 \rail@endbar |
|
266 \rail@end |
|
267 \rail@begin{3}{constdefs} |
|
268 \rail@term{constdefs} |
|
269 \rail@plus |
|
270 \rail@nont{id} |
|
271 \rail@term{::} |
|
272 \rail@bar |
|
273 \rail@nont{string} |
|
274 \rail@nextbar{1} |
|
275 \rail@nont{type} |
|
276 \rail@endbar |
|
277 \rail@nont{string} |
|
278 \rail@nextplus{2} |
|
279 \rail@endplus |
|
280 \rail@end |
|
281 \rail@begin{4}{trans} |
|
282 \rail@term{translations} |
|
283 \rail@plus |
|
284 \rail@nont{pat} |
|
285 \rail@bar |
|
286 \rail@term{==} |
|
287 \rail@nextbar{1} |
|
288 \rail@term{=>} |
|
289 \rail@nextbar{2} |
|
290 \rail@term{<=} |
|
291 \rail@endbar |
|
292 \rail@nont{pat} |
|
293 \rail@nextplus{3} |
|
294 \rail@endplus |
|
295 \rail@end |
|
296 \rail@begin{2}{pat} |
|
297 \rail@bar |
|
298 \rail@nextbar{1} |
|
299 \rail@term{(} |
|
300 \rail@nont{id} |
|
301 \rail@term{)} |
|
302 \rail@endbar |
|
303 \rail@nont{string} |
|
304 \rail@end |
|
305 \rail@begin{2}{rules} |
|
306 \rail@term{rules} |
|
307 \rail@plus |
|
308 \rail@nont{id} |
|
309 \rail@nont{string} |
|
310 \rail@nextplus{1} |
|
311 \rail@endplus |
|
312 \rail@end |
|
313 \rail@begin{2}{defs} |
|
314 \rail@term{defs} |
|
315 \rail@plus |
|
316 \rail@nont{id} |
|
317 \rail@nont{string} |
|
318 \rail@nextplus{1} |
|
319 \rail@endplus |
|
320 \rail@end |
|
321 \rail@begin{1}{oracle} |
|
322 \rail@term{oracle} |
|
323 \rail@nont{name} |
|
324 \rail@end |
|
325 \rail@begin{1}{ml} |
|
326 \rail@term{ML} |
|
327 \rail@nont{text} |
|
328 \rail@end |
|
329 } |