|
1 % This file was generated by 'rail' from 'logics-HOL.rai' |
|
2 \rail@i {1}{ typedef : 'typedef' ( () | '(' name ')') type '=' set witness; \par |
|
3 type : typevarlist name ( () | '(' infix ')' ); set : string; witness : () | '(' id ')'; } |
|
4 \rail@o {1}{ |
|
5 \rail@begin{2}{typedef} |
|
6 \rail@term{typedef}[] |
|
7 \rail@bar |
|
8 \rail@nextbar{1} |
|
9 \rail@term{(}[] |
|
10 \rail@nont{name}[] |
|
11 \rail@term{)}[] |
|
12 \rail@endbar |
|
13 \rail@nont{type}[] |
|
14 \rail@term{=}[] |
|
15 \rail@nont{set}[] |
|
16 \rail@nont{witness}[] |
|
17 \rail@end |
|
18 \rail@begin{2}{type} |
|
19 \rail@nont{typevarlist}[] |
|
20 \rail@nont{name}[] |
|
21 \rail@bar |
|
22 \rail@nextbar{1} |
|
23 \rail@term{(}[] |
|
24 \rail@nont{infix}[] |
|
25 \rail@term{)}[] |
|
26 \rail@endbar |
|
27 \rail@end |
|
28 \rail@begin{1}{set} |
|
29 \rail@nont{string}[] |
|
30 \rail@end |
|
31 \rail@begin{2}{witness} |
|
32 \rail@bar |
|
33 \rail@nextbar{1} |
|
34 \rail@term{(}[] |
|
35 \rail@nont{id}[] |
|
36 \rail@term{)}[] |
|
37 \rail@endbar |
|
38 \rail@end |
|
39 } |
|
40 \rail@i {2}{ datatype : 'datatype' typedecls; \par |
|
41 typedecls: ( newtype '=' (cons + '|') ) + 'and' ; newtype : typevarlist id ( () | '(' infix ')' ) ; cons : name (argtype *) ( () | ( '(' mixfix ')' ) ) ; argtype : id | tid | ('(' typevarlist id ')') ; } |
|
42 \rail@o {2}{ |
|
43 \rail@begin{1}{datatype} |
|
44 \rail@term{datatype}[] |
|
45 \rail@nont{typedecls}[] |
|
46 \rail@end |
|
47 \rail@begin{3}{typedecls} |
|
48 \rail@plus |
|
49 \rail@nont{newtype}[] |
|
50 \rail@term{=}[] |
|
51 \rail@plus |
|
52 \rail@nont{cons}[] |
|
53 \rail@nextplus{1} |
|
54 \rail@cterm{|}[] |
|
55 \rail@endplus |
|
56 \rail@nextplus{2} |
|
57 \rail@cterm{and}[] |
|
58 \rail@endplus |
|
59 \rail@end |
|
60 \rail@begin{2}{newtype} |
|
61 \rail@nont{typevarlist}[] |
|
62 \rail@nont{id}[] |
|
63 \rail@bar |
|
64 \rail@nextbar{1} |
|
65 \rail@term{(}[] |
|
66 \rail@nont{infix}[] |
|
67 \rail@term{)}[] |
|
68 \rail@endbar |
|
69 \rail@end |
|
70 \rail@begin{2}{cons} |
|
71 \rail@nont{name}[] |
|
72 \rail@plus |
|
73 \rail@nextplus{1} |
|
74 \rail@cnont{argtype}[] |
|
75 \rail@endplus |
|
76 \rail@bar |
|
77 \rail@nextbar{1} |
|
78 \rail@term{(}[] |
|
79 \rail@nont{mixfix}[] |
|
80 \rail@term{)}[] |
|
81 \rail@endbar |
|
82 \rail@end |
|
83 \rail@begin{3}{argtype} |
|
84 \rail@bar |
|
85 \rail@nont{id}[] |
|
86 \rail@nextbar{1} |
|
87 \rail@nont{tid}[] |
|
88 \rail@nextbar{2} |
|
89 \rail@term{(}[] |
|
90 \rail@nont{typevarlist}[] |
|
91 \rail@nont{id}[] |
|
92 \rail@term{)}[] |
|
93 \rail@endbar |
|
94 \rail@end |
|
95 } |
|
96 \rail@t {verblbrace} |
|
97 \rail@t {verbrbrace} |
|
98 \rail@i {3}{ codegen : ( 'code_module' | 'code_library' ) modespec ? name ? \\ ( 'file' name ) ? ( 'imports' ( name + ) ) ? \\ 'contains' ( ( name '=' term ) + | term + ); \par |
|
99 modespec : '(' ( name * ) ')'; } |
|
100 \rail@o {3}{ |
|
101 \rail@begin{11}{codegen} |
|
102 \rail@bar |
|
103 \rail@term{code_module}[] |
|
104 \rail@nextbar{1} |
|
105 \rail@term{code_library}[] |
|
106 \rail@endbar |
|
107 \rail@bar |
|
108 \rail@nextbar{1} |
|
109 \rail@nont{modespec}[] |
|
110 \rail@endbar |
|
111 \rail@bar |
|
112 \rail@nextbar{1} |
|
113 \rail@nont{name}[] |
|
114 \rail@endbar |
|
115 \rail@cr{3} |
|
116 \rail@bar |
|
117 \rail@nextbar{4} |
|
118 \rail@term{file}[] |
|
119 \rail@nont{name}[] |
|
120 \rail@endbar |
|
121 \rail@bar |
|
122 \rail@nextbar{4} |
|
123 \rail@term{imports}[] |
|
124 \rail@plus |
|
125 \rail@nont{name}[] |
|
126 \rail@nextplus{5} |
|
127 \rail@endplus |
|
128 \rail@endbar |
|
129 \rail@cr{7} |
|
130 \rail@term{contains}[] |
|
131 \rail@bar |
|
132 \rail@plus |
|
133 \rail@nont{name}[] |
|
134 \rail@term{=}[] |
|
135 \rail@nont{term}[] |
|
136 \rail@nextplus{8} |
|
137 \rail@endplus |
|
138 \rail@nextbar{9} |
|
139 \rail@plus |
|
140 \rail@nont{term}[] |
|
141 \rail@nextplus{10} |
|
142 \rail@endplus |
|
143 \rail@endbar |
|
144 \rail@end |
|
145 \rail@begin{2}{modespec} |
|
146 \rail@term{(}[] |
|
147 \rail@plus |
|
148 \rail@nextplus{1} |
|
149 \rail@cnont{name}[] |
|
150 \rail@endplus |
|
151 \rail@term{)}[] |
|
152 \rail@end |
|
153 } |
|
154 \rail@i {4}{ constscode : 'consts_code' (codespec +); \par |
|
155 codespec : const template attachment ?; \par |
|
156 typescode : 'types_code' (tycodespec +); \par |
|
157 tycodespec : name template attachment ?; \par |
|
158 const : term; \par |
|
159 template: '(' string ')'; \par |
|
160 attachment: 'attach' modespec ? verblbrace text verbrbrace; } |
|
161 \rail@o {4}{ |
|
162 \rail@begin{2}{constscode} |
|
163 \rail@term{consts_code}[] |
|
164 \rail@plus |
|
165 \rail@nont{codespec}[] |
|
166 \rail@nextplus{1} |
|
167 \rail@endplus |
|
168 \rail@end |
|
169 \rail@begin{2}{codespec} |
|
170 \rail@nont{const}[] |
|
171 \rail@nont{template}[] |
|
172 \rail@bar |
|
173 \rail@nextbar{1} |
|
174 \rail@nont{attachment}[] |
|
175 \rail@endbar |
|
176 \rail@end |
|
177 \rail@begin{2}{typescode} |
|
178 \rail@term{types_code}[] |
|
179 \rail@plus |
|
180 \rail@nont{tycodespec}[] |
|
181 \rail@nextplus{1} |
|
182 \rail@endplus |
|
183 \rail@end |
|
184 \rail@begin{2}{tycodespec} |
|
185 \rail@nont{name}[] |
|
186 \rail@nont{template}[] |
|
187 \rail@bar |
|
188 \rail@nextbar{1} |
|
189 \rail@nont{attachment}[] |
|
190 \rail@endbar |
|
191 \rail@end |
|
192 \rail@begin{1}{const} |
|
193 \rail@nont{term}[] |
|
194 \rail@end |
|
195 \rail@begin{1}{template} |
|
196 \rail@term{(}[] |
|
197 \rail@nont{string}[] |
|
198 \rail@term{)}[] |
|
199 \rail@end |
|
200 \rail@begin{2}{attachment} |
|
201 \rail@term{attach}[] |
|
202 \rail@bar |
|
203 \rail@nextbar{1} |
|
204 \rail@nont{modespec}[] |
|
205 \rail@endbar |
|
206 \rail@token{verblbrace}[] |
|
207 \rail@nont{text}[] |
|
208 \rail@token{verbrbrace}[] |
|
209 \rail@end |
|
210 } |