|
1 /* Title: Tools/8bit/c-sources/a2isa/xlex.x |
|
2 ID: $Id$ |
|
3 Author: David von Oheimb |
|
4 Copyright 1996 TU Muenchen |
|
5 |
|
6 Isabelle ASCII to 8bit converter |
|
7 definitions for the lexical analyzer |
|
8 |
|
9 WARNING: the translations should be consistent with the configuration in |
|
10 8bit/config/conv-tables.inp |
|
11 */ |
|
12 |
|
13 |
|
14 %{ |
|
15 extern FILE *finput, *foutput; |
|
16 |
|
17 void put(char *s) |
|
18 { |
|
19 while(*s) |
|
20 { |
|
21 fputc(*s++, yyout); |
|
22 } |
|
23 } |
|
24 %} |
|
25 |
|
26 %option 8bit |
|
27 %option yylineno |
|
28 %option noyywrap |
|
29 %x STRING |
|
30 |
|
31 %% |
|
32 yyin = finput; |
|
33 yyout = foutput; |
|
34 |
|
35 \\I@ { ECHO; BEGIN(STRING); } |
|
36 . { ECHO; } |
|
37 <STRING>\\I@ { ECHO; BEGIN(INITIAL); } |
|
38 <STRING>\\[ \t]*\n[ \t]*\\ { ECHO; } |
|
39 <STRING>\n { ECHO; /* fprintf(stderr, |
|
40 "WARNING: line %d ends inside string\n", |
|
41 yylineno-1); */} |
|
42 <STRING><<EOF>> { fprintf(stderr, |
|
43 "WARNING: EOF inside string\n"); |
|
44 yyterminate(); } |
|
45 |
|
46 <STRING>{ |
|
47 /* Pure */ |
|
48 !! put("Ä"); |
|
49 \[\| put("Ë"); |
|
50 \|\] put("Ì"); |
|
51 ==> put("êë"); |
|
52 == put("Ú"); |
|
53 => put("ë"); |
|
54 :: put("å"); |
|
55 'a put("ª"); |
|
56 'b put("«"); |
|
57 'c put("¬"); |
|
58 'r put("¸"); |
|
59 's put("¹"); |
|
60 't put("º"); |
|
61 |
|
62 /* HOL */ |
|
63 \ \*\ put(" ò "); |
|
64 @[ A-Za-z] { *yytext='®'; put(yytext); } |
|
65 \ &\ put(" À "); |
|
66 \ \|\ put(" Á "); |
|
67 ~\ put("¿ "); |
|
68 --> put("çè"); |
|
69 ~= put("Û"); |
|
70 \%[ A-Za-z] { *yytext='³'; put(yytext); } |
|
71 EX! put("Ã!"); |
|
72 \?! put("Ã!"); |
|
73 EX\ put("Ã"); |
|
74 \?\ put("Ã"); |
|
75 ALL\ put("Â"); |
|
76 ![ A-Za-z] { *yytext='Â'; put(yytext); } |
|
77 |
|
78 /* Set */ |
|
79 ~: put("ñ"); |
|
80 : put("Î"); |
|
81 /* |
|
82 > "{}" "\mbox{$\emptyset$}" |
|
83 # > "<=" "\mbox{$\subseteq$}" |
|
84 */ |
|
85 \ Int\ put("Ð"); |
|
86 \ Un\ put("Ñ"); |
|
87 Inter\ put("Ò"); |
|
88 Union\ put("Ó"); |
|
89 |
|
90 /* Nat */ |
|
91 LEAST\ put("´"); |
|
92 |
|
93 /* HOLCF */ |
|
94 -> put("è"); |
|
95 \*\* put("õ"); |
|
96 \+\+ put("ó"); |
|
97 |
|
98 \<\<\| put("<<|"); |
|
99 \<\| put("<|"); |
|
100 \<\< put("Ý"); |
|
101 LAM\ put("¤"); |
|
102 lub\ put("×"); |
|
103 UU put("Ø"); |
|
104 |
|
105 /* misc */ |
|
106 \|- put("É"); |
|
107 \|= put("Ê"); |
|
108 |
|
109 /* |
|
110 > "\Gamma\ " "\mbox{$\Gamma$}" |
|
111 > "\Delta\ " "\mbox{$\Delta$}" |
|
112 > "\Theta\ " "\mbox{$\Theta$}" |
|
113 > "\Pi\ " "\mbox{$\Pi$}" |
|
114 > "\Sigma\ " "\mbox{$\Sigma$}" |
|
115 > "\Phi\ " "\mbox{$\Phi$}" |
|
116 > "\Psi\ " "\mbox{$\Psi$}" |
|
117 > "\Omega\ " "\mbox{$\Omega$}" |
|
118 |
|
119 > "\delta\ " "\mbox{$\delta$}" |
|
120 > "\epsilon\ " "\mbox{$\varepsilon$}" |
|
121 > "\zeta\ " "\mbox{$\zeta$}" |
|
122 > "\eta\ " "\mbox{$\eta$}" |
|
123 > "\theta\ " "\mbox{$\vartheta$}" |
|
124 > "\kappa\ " "\mbox{$\kappa$}" |
|
125 > "\mu\ " "\mbox{$\mu$}" |
|
126 > "\nu\ " "\mbox{$\nu$}" |
|
127 > "\xi\ " "\mbox{$\xi$}" |
|
128 > "\pi\ " "\mbox{$\pi$}" |
|
129 > "\phi\ " "\mbox{$\varphi$}" |
|
130 > "\chi\ " "\mbox{$\chi$}" |
|
131 > "\psi\ " "\mbox{$\psi$}" |
|
132 > "\omega\ " "\mbox{$\omega$}" |
|
133 |
|
134 > "\lceil\ " "\mbox{$\lceil$}" |
|
135 > "\rceil\ " "\mbox{$\rceil$}" |
|
136 > "\lfloor\ " "\mbox{$\lfloor$}" |
|
137 > "\rfloor\ " "\mbox{$\rfloor$}" |
|
138 > "\sqcap\ " "\mbox{$\sqcap$}" |
|
139 > "\sqcup\ " "\mbox{$\sqcup$}" |
|
140 > "\cdot\ " "\mbox{$\cdot$}" |
|
141 |
|
142 glb\ put("Ö"); |
|
143 === put("Ù"); |
|
144 |
|
145 /* |
|
146 > "\sqsubset\ " "\mbox{$\sqsubset$}" |
|
147 > "\prec\ " "\mbox{$\prec$}" |
|
148 > "\preceq\ " "\mbox{$\preceq$}" |
|
149 > "\Succ\ " "\mbox{$\succ$}" |
|
150 > "\approx\ " "\mbox{$\approx$}" |
|
151 > "\sim\ " "\mbox{$\sim$}" |
|
152 > "\simeq\ " "\mbox{$\simeq$}" |
|
153 > "\le\ " "\mbox{$\le$}" |
|
154 > "\ge\ " "\mbox{$\ge$}" |
|
155 */ |
|
156 |
|
157 \<== put("éê"); |
|
158 \<=> put("éë"); |
|
159 \<-- put("æç"); |
|
160 \<-> put("æè"); |
|
161 \<- put("æ"); |
|
162 |
|
163 /* |
|
164 > "\frown\ " "\mbox{$\frown$}" |
|
165 > "\mapsto\ " "\mbox{$\mapsto$}" |
|
166 > "\leadsto\ " "\mbox{$\leadsto$}" |
|
167 > "\uparrow\ " "\mbox{$\uparrow$}" |
|
168 > "\downarrow\ " "\mbox{$\downarrow$}" |
|
169 |
|
170 > "\ominus\ " "\mbox{$\varominus$}" |
|
171 > "\oslash\ " "\mbox{$\varoslash$}" |
|
172 > "\subset\ " "\mbox{$\subset$}" |
|
173 > "\infty\ " "\mbox{$\infty$}" |
|
174 > "\Box\ " "\mbox{$\Box$}" |
|
175 > "\Diamond\ " "\mbox{$\Diamond$}" |
|
176 > "\circ\ " "\mbox{$\circ$}" |
|
177 > "\bullet\ " "\mbox{$\bullet$}" |
|
178 > "||" "\mbox{$\parallel$}" |
|
179 > "\tick\ " "\mbox{$\surd$}" |
|
180 > "\filter\ " "\mbox{\copyright}" |
|
181 */ |
|
182 } |
|
183 %% |