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