1 # Title: Tools/8bit/config/conf-tables.inp |
|
2 # ID: $Id$ |
|
3 # Author: Franz Regensburger and David von Oheimb |
|
4 # Copyright 1995 TU Muenchen |
|
5 ############################################################ |
|
6 # |
|
7 # This is the configuration file for the converter isa2latex |
|
8 # It is interpreted by the perl script `gen-isa2latex' which |
|
9 # produces rsp. changes the followong files of the converter |
|
10 # sources: |
|
11 # |
|
12 # Makefile, conv-tables.h, conv-defs.h and conv-lex.x |
|
13 # |
|
14 # In the perl script, regular expressions are used to identify |
|
15 # the keywords. In order to be sure that something is treated |
|
16 # as a comment, simply begin the line with a # sign. This is |
|
17 # fool proof. |
|
18 # |
|
19 ############################################################ |
|
20 |
|
21 ############################################################ |
|
22 # General setup |
|
23 # |
|
24 ### path to the sources of the converter, |
|
25 # Must be readable for user. |
|
26 # |
|
27 # Must be delimited by " |
|
28 # |
|
29 |
|
30 CONV_SOURCE_DIR "/usr/wiss/oheimb/isabelle/src/Tools/8bit/c-sources/isa2latex" |
|
31 |
|
32 # End of general setup |
|
33 ############################################################ |
|
34 |
|
35 ############################################################ |
|
36 # Setup for translationTableLow in file conv-tables.h |
|
37 # |
|
38 |
|
39 ### Start index START_LOW_TABLE of translationTableLow |
|
40 # The index END_LOW_TABLE is computed from the length |
|
41 # of the translation table LOW_TABLE below. |
|
42 # |
|
43 # constraints: 32 <= START_LOW_TABLE <= 127 |
|
44 # START_LOW_TABLE + length(LOW_TABLE) - 1 <= 127 |
|
45 # |
|
46 # Must be delimited by " |
|
47 # |
|
48 |
|
49 START_LOW_TABLE "32" |
|
50 |
|
51 ### The translation table LOW_TABLE |
|
52 # |
|
53 # Keyword for the begin of the table is BEGIN_LOW_TABLE |
|
54 # Keyword for the end of the table is END_LOW_TABLE |
|
55 # |
|
56 # Lines beginning with # are ignored as everywhere in this file. |
|
57 # Lines obeying the syntax given below are treated as table entries. |
|
58 # All other lines are ignored, too. This is for comments. |
|
59 # |
|
60 # Syntax of a table entry: |
|
61 # |
|
62 # > "LaTeX replacement" anything |
|
63 # |
|
64 # The double quotes enclose the LaTeX replacement in pure |
|
65 # LaTeX syntax. |
|
66 # Every \ in the string except when used for hex-notation \x?? is |
|
67 # automatically duplicated by the script! The strings are used in |
|
68 # printf output statements in the C code. |
|
69 # |
|
70 # Attention: you have to use hex-notation \x22 to produce a " inside |
|
71 # the double quoted strings. An explicit " will terminate the string. |
|
72 # |
|
73 # The following `anything' is ignored by the perl script. |
|
74 # This is for comments. |
|
75 # |
|
76 # The ordering of entries in the table LOW_TABLE is relevant! |
|
77 # Empty table is not allowed. |
|
78 # |
|
79 # |
|
80 |
|
81 BEGIN_LOW_TABLE |
|
82 > "\ " Blank |
|
83 > "!" |
|
84 # |
|
85 # if you don't like double quotes to be removed insert the following |
|
86 #> "\\x22{}" double quotes are not removed |
|
87 > "\x22{}" double quotes are not removed |
|
88 # |
|
89 > "\#" |
|
90 > "\$" |
|
91 > "\%" |
|
92 > "\&" |
|
93 > "'" |
|
94 > "(" |
|
95 > ")" |
|
96 > "{*}" |
|
97 > "+" |
|
98 > "," |
|
99 > "-" |
|
100 > "." |
|
101 > "/" |
|
102 > "0" |
|
103 > "1" |
|
104 > "2" |
|
105 > "3" |
|
106 > "4" |
|
107 > "5" |
|
108 > "6" |
|
109 > "7" |
|
110 > "8" |
|
111 > "9" |
|
112 > ":" |
|
113 > ";" |
|
114 > "<" |
|
115 > "=" |
|
116 > ">" |
|
117 > "?" |
|
118 > "@" |
|
119 > "A" |
|
120 > "B" |
|
121 > "C" |
|
122 > "D" |
|
123 > "E" |
|
124 > "F" |
|
125 > "G" |
|
126 > "H" |
|
127 > "I" |
|
128 > "J" |
|
129 > "K" |
|
130 > "L" |
|
131 > "M" |
|
132 > "N" |
|
133 > "O" |
|
134 > "P" |
|
135 > "Q" |
|
136 > "R" |
|
137 > "S" |
|
138 > "T" |
|
139 > "U" |
|
140 > "V" |
|
141 > "W" |
|
142 > "X" |
|
143 > "Y" |
|
144 > "Z" |
|
145 > "[" |
|
146 > "\ttbackslash{}" #????? |
|
147 > "]" |
|
148 > "\^{}" |
|
149 > "{\_\hspace{.344ex}}" |
|
150 > "`" |
|
151 > "a" |
|
152 > "b" |
|
153 > "c" |
|
154 > "d" |
|
155 > "e" |
|
156 > "f" |
|
157 > "g" |
|
158 > "h" |
|
159 > "i" |
|
160 > "j" |
|
161 > "k" |
|
162 > "l" |
|
163 > "m" |
|
164 > "n" |
|
165 > "o" |
|
166 > "p" |
|
167 > "q" |
|
168 > "r" |
|
169 > "s" |
|
170 > "t" |
|
171 > "u" |
|
172 > "v" |
|
173 > "w" |
|
174 > "x" |
|
175 > "y" |
|
176 > "z" |
|
177 > "\{" #"\ttlbrace{}" |
|
178 > "|" |
|
179 > "\}" #"\ttrbrace{}" |
|
180 > "\tttilde{}" |
|
181 END_LOW_TABLE |
|
182 |
|
183 ############################################################ |
|
184 # Setup for translationTableHi in file conv-tables.h |
|
185 # |
|
186 |
|
187 ### Start index START_HI_TABLE of translationTableHi |
|
188 # The index END_HI_TABLE is computed from the length |
|
189 # of the translation table HI_TABLE below. |
|
190 # |
|
191 # constraints: 128 <= START_HI_TABLE <= 255 |
|
192 # START_HI_TABLE + length(HI_TABLE) - 1 <= 255 |
|
193 # |
|
194 # |
|
195 # Must be delimited by " |
|
196 # |
|
197 |
|
198 START_HI_TABLE "160" |
|
199 |
|
200 ### The translation table HI_TABLE |
|
201 # |
|
202 # Keyword for the begin of the table is BEGIN_HI_TABLE |
|
203 # Keyword for the end of the table is END_HI_TABLE |
|
204 # |
|
205 # Lines beginning with # are ignored as everywhere in this file. |
|
206 # Lines obeying the syntax given below are treated as table entries. |
|
207 # All other lines are ignored, too. This is for comments. |
|
208 # |
|
209 # Syntax of a table entry: |
|
210 # |
|
211 # > "lex expression ascii" "ascii replacement" "LaTeX replacement" anything |
|
212 # |
|
213 # The double quotes enclose the lex expression, the ascii replacement, and the |
|
214 # LaTeX replacement in pure lex rsp. pure ascii rsp. LaTeX syntax. |
|
215 # |
|
216 # The string for the lex expression is literally passed to lex. Backslashes |
|
217 # are not duplicated! |
|
218 # Every \ in the replacements except when used for hex-notation \x?? is |
|
219 # automatically duplicated by the script! The strings are used in |
|
220 # printf output statements in the C code. |
|
221 # |
|
222 # Attention: you have to use hex-notation \x22 to produce a " inside |
|
223 # the double quoted strings. An explicit " will terminate the string. |
|
224 # |
|
225 # The following `anything' is ignored by the perl script. |
|
226 # This is for comments. |
|
227 # |
|
228 # The ordering of entries in the table HI_TABLE is relevant! |
|
229 # Empty table is not allowed. |
|
230 # |
|
231 # |
|
232 |
|
233 BEGIN_HI_TABLE |
|
234 |
|
235 # big (i.e. double) blank space, for compensation of other too long symbols |
|
236 > "\ \ " " " "\ \ " |
|
237 |
|
238 # big greek letters |
|
239 > "\\Gamma" "\Gamma" "\mbox{$\Gamma$}" |
|
240 > "\\Delta" "\Delta" "\mbox{$\Delta$}" |
|
241 > "\\Theta" "\Theta" "\mbox{$\Theta$}" |
|
242 > "LAM\ " "LAM " "\mbox{$\Lambda$}" |
|
243 > "\\Pi" "\Pi" "\mbox{$\Pi$}" |
|
244 > "\\Sigma" "SIGMA" "\mbox{$\Sigma$}" |
|
245 > "\\Phi" "\Phi" "\mbox{$\Phi$}" |
|
246 > "\\Psi" "\Psi" "\mbox{$\Psi$}" |
|
247 > "\\Omega" "\Omega" "\mbox{$\Omega$}" |
|
248 |
|
249 # small greek letters, HOL, HOLCF |
|
250 > "'a" "'a" "\mbox{$\alpha$}" |
|
251 > "'b" "'b" "\mbox{$\beta$}" |
|
252 > "'c" "'c" "\mbox{$\gamma$}" |
|
253 > "\\delta" "\delta" "\mbox{$\delta$}" |
|
254 > "\\varepsilon" "@" "\mbox{$\varepsilon$}" |
|
255 > "\\zeta" "\zeta" "\mbox{$\zeta$}" |
|
256 > "\\eta" "\eta" "\mbox{$\eta$}" |
|
257 > "\\vartheta" "\vartheta" "\mbox{$\vartheta$}" |
|
258 > "\\kappa" "\kappa" "\mbox{$\kappa$}" |
|
259 > "%\ " "%" "\mbox{$\lambda$}" |
|
260 > "\\mu" "\mu" "\mbox{$\mu$}" |
|
261 > "\\nu" "\nu" "\mbox{$\nu$}" |
|
262 > "\\xi" "\xi" "\mbox{$\xi$}" |
|
263 > "\\pi" "\p" "\mbox{$\pi$}" |
|
264 > "'r" "'r" "\mbox{$\rho$}" |
|
265 > "'s" "'s" "\mbox{$\sigma$}" |
|
266 > "'t" "'t" "\mbox{$\tau$}" |
|
267 > "\\varphi" "\varphi" "\mbox{$\varphi$}" |
|
268 > "\\chi" "\chi" "\mbox{$\chi$}" |
|
269 > "\\psi" "\psi" "\mbox{$\psi$}" |
|
270 > "\\omega" "\omega" "\mbox{$\omega$}" |
|
271 |
|
272 # logical symbols, HOL |
|
273 > "~\ " "~ " "\mbox{$\hspace{-.33ex}\neg$}" |
|
274 > "&\ " "& " "\mbox{$\hspace{-.185ex}\wedge\hspace{-.185ex}$}\ " |
|
275 > "\|\ " "| " "\mbox{$\hspace{-.185ex}\vee\hspace{-.185ex}$}\ " |
|
276 > "!\ " "!" "\mbox{$\hspace{-.07ex}\forall$}" |
|
277 > "\?\ " "? " "\mbox{$\hspace{-.07ex}\exists$}" |
|
278 > "!!" "!!" "\mbox{$\bigwedge$}" |
|
279 |
|
280 # parenthesis. Pure, HOLCF, ... |
|
281 > "\\lceil" "\lceil" "\mbox{$\lceil$}" |
|
282 > "\\rceil" "\rceil" "\mbox{$\rceil$}" |
|
283 > "\\lfloor" "\lfloor" "\mbox{$\lfloor$}" |
|
284 > "\\rfloor" "\rfloor" "\mbox{$\rfloor$}" |
|
285 #> "\|-" "|-" "\mbox{$\vdash\hspace{-.2ex}$}" |
|
286 > "\|-" "|-" "\mbox{$\hspace{.49ex}\vdash\hspace{.49ex}$}" |
|
287 > "\|=" "|=" "\mbox{$\models$}" |
|
288 > "\[\|" "[|" "\mbox{$[\![\hspace{.32ex}$}"#\llbracket |
|
289 > "\|\]" "|]" "\mbox{$\hspace{.32ex}]\!]$}"#\rrbracket |
|
290 > "\\cdot" "." "\mbox{$\hspace{.28ex}\cdot\hspace{.28ex}$}" |
|
291 |
|
292 # set theory, HOL |
|
293 > "\ :\ " ":" "\mbox{$\hspace{.445ex}\in\hspace{.445ex}$}" |
|
294 > "\ \subseteq\ " " <= " "\mbox{$\subseteq$}" |
|
295 > "\ Int\ " " Int " "\mbox{$\cap$}" |
|
296 > "\ Un\ " " Un " "\mbox{$\cup$}" |
|
297 > "Inter\ " "INT " "\mbox{$\bigcap$}" |
|
298 > "Union\ " "UN " "\mbox{$\bigcup$}" |
|
299 |
|
300 # domain theory, HOLCF |
|
301 > "\\sqcap" "\sqcap" "\mbox{$\hspace{.29ex}\sqcap\hspace{.29ex}$}" |
|
302 > "\\sqcup" "\sqcup" "\mbox{$\hspace{.29ex}\sqcup\hspace{.29ex}$}" |
|
303 > "glb\ " "glb " "\mbox{$\overline{|\,\,|}$}"#\bigsqcap |
|
304 > "LUB\ " "LUB " "\mbox{$\bigsqcup$}" |
|
305 > "UU" "UU" "\mbox{$\hspace{-.29ex}\bot\hspace{-.29ex}$}" |
|
306 |
|
307 # relational symbols, Pure, HOLCF |
|
308 > "===" ".=" "\mbox{$\doteq$}" |
|
309 > "==" "==" "\mbox{$\hspace{.29ex}\equiv\hspace{.29ex}$}" |
|
310 > "~=" "~=" "\mbox{$\hspace{-.34ex}\not\hspace{-.3ex}\mbox{=}$}" |
|
311 > "\\sqsubset" "\sqsubset" "\mbox{$\hspace{.29ex}\sqsubset\hspace{.29ex}$}" |
|
312 > "<<" "<<" "\mbox{$\hspace{.29ex}\sqsubseteq\hspace{.29ex}$}" |
|
313 > "<:" "<:" "\mbox{$\hspace{.29ex}\prec\hspace{.29ex}$}\ " |
|
314 > "<=:" "<=:" "\mbox{$\hspace{.29ex}\preceq\hspace{.29ex}$}" |
|
315 > ":>" ":>" "\mbox{$\hspace{.29ex}\succ\hspace{.29ex}$}\ " |
|
316 > "~~" "~~" "\mbox{$\hspace{.29ex}\approx\hspace{.29ex}$}" |
|
317 > "\\sim\ " "\sim " "\mbox{$\hspace{.29ex}\sim\hspace{.29ex}$}\ " |
|
318 > "\\simeq" "\simeq" "\mbox{$\hspace{.29ex}\simeq\hspace{.29ex}$}" |
|
319 > "<=" "<=" "\mbox{$\hspace{.29ex}\le\hspace{.29ex}$}" |
|
320 > "::" "::" "\mbox{$:\hspace{-.07ex}:$}" #"\mbox{$\hspace{-.1ex}:\hspace{-.07ex}:\hspace{.1ex}$}" |
|
321 |
|
322 # arrows, Pure, HOL |
|
323 > "<-" "<-" "\mbox{$\leftarrow$}" |
|
324 > "-@@@@@" "-" "\mbox{$-$}" |
|
325 > "->" "->" "\mbox{$\rightarrow$}" |
|
326 > "\\Leftarrow" "<=" "\mbox{$\Leftarrow$}" |
|
327 > "=@@@@@" "=" "\mbox{$=$}" |
|
328 > "=>" "=>" "\mbox{$\hspace{.12ex}\Rightarrow$}" |
|
329 > "\\frown" "\frown" "\mbox{$\frown$}" |
|
330 > "\\mapsto" "|->" "\mbox{$\mapsto$}" |
|
331 > "\\leadsto" "~>" "\mbox{$\hspace{.05ex}\leadsto$}" |
|
332 > "\\uparrow" "\uparrow" "\mbox{$\uparrow$}" |
|
333 > "\\downarrow" "\downarrow" "\mbox{$\downarrow$}" |
|
334 > "~:" "~:" "\mbox{$\hspace{.445ex}\notin\hspace{.445ex}$}" |
|
335 |
|
336 # arithmetic, HOLCF |
|
337 > "\\times" "*" "\mbox{$\hspace{-.29ex}\times\hspace{-.29ex}$}" |
|
338 > "\+\+" "++" "\mbox{$\hspace{.29ex}\oplus\hspace{.29ex}$}" #\varoplus |
|
339 > "\\ominus" "--" "\mbox{$\hspace{.29ex}\ominus\hspace{.29ex}$}" #\varominus |
|
340 > "\*\*" "**" "\mbox{$\hspace{.29ex}\otimes\hspace{.29ex}$}" #\varotimes |
|
341 > "\\oslash" "//" "\mbox{$\hspace{.29ex}\oslash\hspace{.29ex}$}" #\varoslash |
|
342 > "\\subset" "\subset" "\mbox{$\subset$}" |
|
343 > "\\infty" "\infty" "\mbox{$\infty$}" |
|
344 |
|
345 # misc |
|
346 > "\\Box" "\Box" "\mbox{$\Box$}" |
|
347 > "\\Diamond" "<>" "\mbox{$\hspace{.29ex}\Diamond\hspace{.29ex}$}" |
|
348 > "\\circ" " o " "\mbox{$\circ$}" |
|
349 > "\\bullet" "\bullet" "\mbox{$\bullet$}" |
|
350 > "\|\|" "||" "\mbox{$\parallel$}" |
|
351 > "\\tick" "\tick" "\mbox{$\surd$}" |
|
352 > "\\filter" "\filter" "\mbox{\copyright}" |
|
353 END_HI_TABLE |
|
354 |
|
355 ############################################################ |
|
356 # Setup for translationTableSeq in file conv-tables.h |
|
357 # and lexer source conv-lex.x |
|
358 # |
|
359 # Keyword for the being of the table is BEGIN_SEQ_TABLE |
|
360 # Keyword for the end of the table is END_SEQ_TABLE |
|
361 # |
|
362 # Lines beginning with # are ignored as everywhere in this file. |
|
363 # Lines obeying the syntax given below are treated as table entries. |
|
364 # All other lines are ignored, too. This is for comments. |
|
365 # |
|
366 # Syntax of a table entry: |
|
367 # |
|
368 # > "lex expr 8bit" "lex expr ascii" "ascii replace" "LaTeX replace" anything |
|
369 # |
|
370 # The double quotes enclose the lex expressions, the ascii replacement, and |
|
371 # the LaTeX replacement in pure lex rsp. pure ascii rsp. LaTeX syntax. |
|
372 # |
|
373 # The strings for the lex expressions are literally passed to lex. Backslashes |
|
374 # are not duplicated! |
|
375 # Every \ in the replacements except when used for hex-notation \x?? is |
|
376 # automatically duplicated by the script! The strings are used in |
|
377 # printf output statements in the C code. |
|
378 # |
|
379 # Attention: you have to use hex-notation \x22 to produce a " inside |
|
380 # the double quoted strings. An explicit " will terminate the string. |
|
381 # |
|
382 # The following `anything' is ignored by the perl script. |
|
383 # This is for comments. |
|
384 # |
|
385 # The ordering of entries in table SEQ_TABLE is irrelevant! |
|
386 # Empty table is allowed. |
|
387 # |
|
388 |
|
389 BEGIN_SEQ_TABLE |
|
390 |
|
391 # Pure |
|
392 > "êë" "==>" "==>" "\mbox{$\hspace{-.083ex}\Longrightarrow$}" |
|
393 |
|
394 # HOL |
|
395 > "çè" "-->" "-->" "\mbox{$\longrightarrow$}" |
|
396 > "Ã!" "\?!" "?!" "\mbox{$\exists_1$}" |
|
397 > "ALL@@@@@" "ALL\ " "ALL " "\mbox{$\forall$}" |
|
398 > "EX@@@@@" "EX\ " "EX " "\mbox{$\exists$}" |
|
399 |
|
400 #HOLCF |
|
401 > "<<\|" "@<<\|" "<<|" "\mbox{$\ll\!\mid$}" |
|
402 > "<\|" "@<\|" "<|" "\mbox{$<\!\mid$}" |
|
403 |
|
404 # misc ? |
|
405 > "éê" "<==" "<==" "\mbox{$\Longleftarrow$}" |
|
406 > "éë" "<=>" "<=>" "\mbox{$\Leftrightarrow$}" |
|
407 > "æç" "<--" "<--" "\mbox{$\longleftarrow$}" |
|
408 > "æè" "<->" "<->" "\mbox{$\leftrightarrow$}" |
|
409 #> "\^-1" "@\^-1" "^-1" "\mbox{$^{\tt -1}$}" |
|
410 |
|
411 #Isabelle |
|
412 > "^and" "^@and" "and" "\mbox{\bf and}" |
|
413 > "^arities" "^@arities" "arities" "\mbox{\bf arities}" |
|
414 > "^axclass" "^@axclass" "axclass" "\mbox{\bf axclass}" |
|
415 > "^constdefs" "^@constdefs" "constdefs" "\mbox{\bf constdefs}" |
|
416 > "^consts" "^@consts" "consts" "\mbox{\bf consts}" |
|
417 > "^datatype" "^@datatype" "datatype" "\mbox{\bf datatype}" |
|
418 > "^defs" "^@defs" "defs" "\mbox{\bf defs}" |
|
419 > "^domain" "^@domain" "domain" "\mbox{\bf domain}" |
|
420 > "^end" "^@end" "end" "\mbox{\bf end}" |
|
421 > "^inductive" "^@inductive" "inductive" "\mbox{\bf inductive}" |
|
422 > "^instance" "^@instance" "instance" "\mbox{\bf instance}" |
|
423 > "^primrec" "^@primrec" "primrec" "\mbox{\bf primrec}" |
|
424 > "^recdef" "^@recdef" "recdef" "\mbox{\bf recdef}" |
|
425 > "^rules" "^@rules" "rules" "\mbox{\bf rules}" |
|
426 > "^syntax" "^@syntax" "syntax" "\mbox{\bf syntax}" |
|
427 > "^translations""^@translations""translations""\mbox{\bf translations}" |
|
428 > "^typedef" "^@typedef" "typedef" "\mbox{\bf typedef}" |
|
429 > "^types" "^@types" "types" "\mbox{\bf types}" |
|
430 END_SEQ_TABLE |
|
431 |
|
432 |
|