1 (* Copyright (C) 2000, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (**************************************************************************)
30 (* Andrea Asperti <asperti@cs.unibo.it> *)
33 (**************************************************************************)
35 module C2P = Cexpr2pres;;
36 module P = Mpresentation;;
54 ?tail:Mpresentation.mpres list ->
55 Content_expressions.cexpr ->
57 ~(cexpr2pres_charcount:
60 ?tail:Mpresentation.mpres list ->
61 Content_expressions.cexpr ->
66 Hashtbl.add C2P.symbol_table "arrow" (binary
67 (fun a b ~priority ~assoc ~tail aattr sattr ->
68 if (priority > 5) || (priority = 5 && assoc) then
69 P.row_with_brackets aattr
70 (cexpr2pres ~priority:5 ~assoc:false ~tail:[] a)
71 (cexpr2pres ~priority:5 ~assoc:true
72 ~tail:(P.Mtext([],")")::tail) b)
73 (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2192))
75 P.row_without_brackets aattr
76 (cexpr2pres ~priority:5 ~assoc:false ~tail:[] a)
77 (cexpr2pres ~priority:5 ~assoc:true ~tail:tail b)
78 (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2192))));
80 Hashtbl.add C2P.symbol_table_charcount "arrow" (binary
81 (fun a b ~priority ~assoc ~tail aattr sattr ->
82 if (priority > 40) || (priority = 40 && assoc) then
83 P.two_rows_table_with_brackets aattr
84 (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:[] a)
85 (cexpr2pres_charcount ~priority:40 ~assoc:true
86 ~tail:(P.Mtext([],")")::tail) b)
87 (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2192))
89 P.two_rows_table_without_brackets aattr
90 (cexpr2pres_charcount ~priority:5 ~assoc:false ~tail:[] a)
91 (cexpr2pres_charcount ~priority:5 ~assoc:true ~tail:tail b)
92 (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2192))));
95 Hashtbl.add C2P.symbol_table "eq" (binary
96 (fun a b ~priority ~assoc ~tail aattr sattr ->
97 if (priority > 40) || (priority = 40 && assoc) then
98 P.row_with_brackets aattr
99 (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
100 (cexpr2pres ~priority:40 ~assoc:false
101 ~tail:(P.Mtext([],")")::tail) b)
104 P.row_without_brackets aattr
105 (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
106 (cexpr2pres ~priority:40 ~assoc:false ~tail:tail b)
109 Hashtbl.add C2P.symbol_table_charcount "eq" (binary
110 (fun a b ~priority ~assoc ~tail aattr sattr ->
111 if (priority > 40) || (priority = 40 && assoc) then
112 P.two_rows_table_with_brackets aattr
113 (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
114 (cexpr2pres_charcount ~priority:40 ~assoc:false
115 ~tail:(P.Mtext([],")")::tail) b)
118 P.two_rows_table_without_brackets aattr
119 (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
120 (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:tail b)
124 Hashtbl.add C2P.symbol_table "and" (binary
125 (fun a b ~priority ~assoc ~tail aattr sattr ->
126 if (priority > 20) || (priority = 20 && assoc) then
127 P.row_with_brackets aattr
128 (cexpr2pres ~priority:20 ~assoc:true ~tail:[] a)
129 (cexpr2pres ~priority:20 ~assoc:false
130 ~tail:(P.Mtext([],")")::tail) b)
131 (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2227))
133 P.row_without_brackets aattr
134 (cexpr2pres ~priority:20 ~assoc:true ~tail:[] a)
135 (cexpr2pres ~priority:20 ~assoc:false ~tail:tail b)
136 (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2227))));
138 Hashtbl.add C2P.symbol_table_charcount "and" (binary
139 (fun a b ~priority ~assoc ~tail aattr sattr ->
140 if (priority > 20) || (priority = 20 && assoc) then
141 P.two_rows_table_with_brackets aattr
142 (cexpr2pres_charcount ~priority:20 ~assoc:true ~tail:[] a)
143 (cexpr2pres_charcount ~priority:20 ~assoc:false
144 ~tail:(P.Mtext([],")")::tail) b)
145 (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2227))
147 P.two_rows_table_without_brackets aattr
148 (cexpr2pres_charcount ~priority:20 ~assoc:true ~tail:[] a)
149 (cexpr2pres_charcount ~priority:20 ~assoc:false ~tail:tail b)
150 (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2227))));
153 Hashtbl.add C2P.symbol_table "or" (binary
154 (fun a b ~priority ~assoc ~tail aattr sattr ->
155 if (priority > 10) || (priority = 10 && assoc) then
156 P.row_with_brackets aattr
157 (cexpr2pres ~priority:10 ~assoc:true ~tail:[] a)
158 (cexpr2pres ~priority:10 ~assoc:false
159 ~tail:(P.Mtext([],")")::tail) b)
160 (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2228))
162 P.row_without_brackets aattr
163 (cexpr2pres ~priority:10 ~assoc:true ~tail:[] a)
164 (cexpr2pres ~priority:10 ~assoc:false ~tail:tail b)
165 (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2228))));
167 Hashtbl.add C2P.symbol_table_charcount "or" (binary
168 (fun a b ~priority ~assoc ~tail aattr sattr ->
169 if (priority > 10) || (priority = 10 && assoc) then
170 P.two_rows_table_with_brackets aattr
171 (cexpr2pres_charcount ~priority:10 ~assoc:true ~tail:[] a)
172 (cexpr2pres_charcount ~priority:10 ~assoc:false
173 ~tail:(P.Mtext([],")")::tail) b)
174 (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2228))
176 P.two_rows_table_without_brackets aattr
177 (cexpr2pres_charcount ~priority:10 ~assoc:true ~tail:[] a)
178 (cexpr2pres_charcount ~priority:10 ~assoc:false ~tail:tail b)
179 (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2228))));
182 Hashtbl.add C2P.symbol_table "iff" (binary
183 (fun a b ~priority ~assoc ~tail aattr sattr ->
184 if (priority > 5) || (priority = 5 && assoc) then
185 P.row_with_brackets aattr
186 (cexpr2pres ~priority:5 ~assoc:true ~tail:[] a)
187 (cexpr2pres ~priority:5 ~assoc:false
188 ~tail:(P.Mtext([],")")::tail) b)
189 (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x21D4))
191 P.row_without_brackets aattr
192 (cexpr2pres ~priority:5 ~assoc:true ~tail:[] a)
193 (cexpr2pres ~priority:5 ~assoc:false ~tail:tail b)
194 (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x21D4))));
196 Hashtbl.add C2P.symbol_table_charcount "iff" (binary
197 (fun a b ~priority ~assoc ~tail aattr sattr ->
198 if (priority > 5) || (priority = 5 && assoc) then
199 P.two_rows_table_with_brackets aattr
200 (cexpr2pres_charcount ~priority:5 ~assoc:true ~tail:[] a)
201 (cexpr2pres_charcount ~priority:5 ~assoc:false
202 ~tail:(P.Mtext([],")")::tail) b)
203 (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x21D4))
205 P.two_rows_table_without_brackets aattr
206 (cexpr2pres_charcount ~priority:5 ~assoc:true ~tail:[] a)
207 (cexpr2pres_charcount ~priority:5 ~assoc:false ~tail:tail b)
208 (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x21D4))));
211 Hashtbl.add C2P.symbol_table "not" (unary
212 (fun a ~priority ~assoc ~tail attr sattr ->
214 P.Mtext([],"(");P.Mo([],Netconversion.ustring_of_uchar `Enc_utf8 0xAC);
215 cexpr2pres a;P.Mtext([],")")])));
218 Hashtbl.add C2P.symbol_table "leq" (binary
219 (fun a b ~priority ~assoc ~tail aattr sattr ->
220 if (priority > 40) || (priority = 40 && assoc) then
221 P.row_with_brackets aattr
222 (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
223 (cexpr2pres ~priority:40 ~assoc:false
224 ~tail:(P.Mtext([],")")::tail) b)
225 (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2264))
227 P.row_without_brackets aattr
228 (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
229 (cexpr2pres ~priority:40 ~assoc:false ~tail:tail b)
230 (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2264))));
232 Hashtbl.add C2P.symbol_table_charcount "leq" (binary
233 (fun a b ~priority ~assoc ~tail aattr sattr ->
234 if (priority > 40) || (priority = 40 && assoc) then
235 P.two_rows_table_with_brackets aattr
236 (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
237 (cexpr2pres_charcount ~priority:40 ~assoc:false
238 ~tail:(P.Mtext([],")")::tail) b)
239 (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2264))
241 P.two_rows_table_without_brackets aattr
242 (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
243 (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:tail b)
244 (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2264))));
247 Hashtbl.add C2P.symbol_table "lt" (binary
248 (fun a b ~priority ~assoc ~tail aattr sattr ->
249 if (priority > 40) || (priority = 40 && assoc) then
250 P.row_with_brackets aattr
251 (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
252 (cexpr2pres ~priority:40 ~assoc:false
253 ~tail:(P.Mtext([],")")::tail) b)
256 P.row_without_brackets aattr
257 (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
258 (cexpr2pres ~priority:40 ~assoc:false ~tail:tail b)
259 (P.Mo(sattr,"<"))));
261 Hashtbl.add C2P.symbol_table_charcount "lt" (binary
262 (fun a b ~priority ~assoc ~tail aattr sattr ->
263 if (priority > 40) || (priority = 40 && assoc) then
264 P.two_rows_table_with_brackets aattr
265 (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
266 (cexpr2pres_charcount ~priority:40 ~assoc:false
267 ~tail:(P.Mtext([],")")::tail) b)
270 P.two_rows_table_without_brackets aattr
271 (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
272 (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:tail b)
273 (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2265))));
276 Hashtbl.add C2P.symbol_table "geq" (binary
277 (fun a b ~priority ~assoc ~tail aattr sattr ->
278 if (priority > 40) || (priority = 40 && assoc) then
279 P.row_with_brackets aattr
280 (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
281 (cexpr2pres ~priority:40 ~assoc:false
282 ~tail:(P.Mtext([],")")::tail) b)
283 (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2265))
285 P.row_without_brackets aattr
286 (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
287 (cexpr2pres ~priority:40 ~assoc:false ~tail:tail b)
288 (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2265))));
290 Hashtbl.add C2P.symbol_table_charcount "geq" (binary
291 (fun a b ~priority ~assoc ~tail aattr sattr ->
292 if (priority > 40) || (priority = 40 && assoc) then
293 P.two_rows_table_with_brackets aattr
294 (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
295 (cexpr2pres_charcount ~priority:40 ~assoc:false
296 ~tail:(P.Mtext([],")")::tail) b)
297 (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2265))
299 P.two_rows_table_without_brackets aattr
300 (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
301 (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:tail b)
302 (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2265))));
305 Hashtbl.add C2P.symbol_table "gt" (binary
306 (fun a b ~priority ~assoc ~tail aattr sattr ->
307 if (priority > 40) || (priority = 40 && assoc) then
308 P.row_with_brackets aattr
309 (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
310 (cexpr2pres ~priority:40 ~assoc:false
311 ~tail:(P.Mtext([],")")::tail) b)
314 P.row_without_brackets aattr
315 (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
316 (cexpr2pres ~priority:40 ~assoc:false ~tail:tail b)
319 Hashtbl.add C2P.symbol_table_charcount "gt" (binary
320 (fun a b ~priority ~assoc ~tail aattr sattr ->
321 if (priority > 40) || (priority = 40 && assoc) then
322 P.two_rows_table_with_brackets aattr
323 (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
324 (cexpr2pres_charcount ~priority:40 ~assoc:false
325 ~tail:(P.Mtext([],")")::tail) b)
328 P.two_rows_table_without_brackets aattr
329 (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
330 (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:tail b)
334 Hashtbl.add C2P.symbol_table "plus" (binary
335 (fun a b ~priority ~assoc ~tail aattr sattr ->
336 if (priority > 60) || (priority = 60 && assoc) then
337 P.row_with_brackets aattr
338 (cexpr2pres ~priority:60 ~assoc:true ~tail:[] a)
339 (cexpr2pres ~priority:60 ~assoc:false
340 ~tail:(P.Mtext([],")")::tail) b)
343 P.row_without_brackets aattr
344 (cexpr2pres ~priority:60 ~assoc:true ~tail:[] a)
345 (cexpr2pres ~priority:60 ~assoc:false ~tail:tail b)
348 Hashtbl.add C2P.symbol_table_charcount "plus" (binary
349 (fun a b ~priority ~assoc ~tail aattr sattr ->
350 if (priority > 60) || (priority = 60 && assoc) then
351 P.two_rows_table_with_brackets aattr
352 (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a)
353 (cexpr2pres_charcount ~priority:60 ~assoc:false
354 ~tail:(P.Mtext([],")")::tail) b)
357 P.two_rows_table_without_brackets aattr
358 (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a)
359 (cexpr2pres_charcount ~priority:60 ~assoc:false ~tail:tail b)
363 Hashtbl.add C2P.symbol_table "times" (binary
364 (fun a b ~priority ~assoc ~tail aattr sattr ->
365 if (priority > 70) || (priority = 70 && assoc) then
366 P.row_with_brackets aattr
367 (cexpr2pres ~priority:70 ~assoc:true ~tail:[] a)
368 (cexpr2pres ~priority:70 ~assoc:false
369 ~tail:(P.Mtext([],")")::tail) b)
372 P.row_without_brackets aattr
373 (cexpr2pres ~priority:70 ~assoc:true ~tail:[] a)
374 (cexpr2pres ~priority:70 ~assoc:false ~tail:tail b)
377 Hashtbl.add C2P.symbol_table_charcount "times" (binary
378 (fun a b ~priority ~assoc ~tail aattr sattr ->
379 if (priority > 70) || (priority = 70 && assoc) then
380 P.two_rows_table_with_brackets aattr
381 (cexpr2pres_charcount ~priority:70 ~assoc:true ~tail:[] a)
382 (cexpr2pres_charcount ~priority:70 ~assoc:false
383 ~tail:(P.Mtext([],")")::tail) b)
386 P.two_rows_table_without_brackets aattr
387 (cexpr2pres_charcount ~priority:70 ~assoc:true ~tail:[] a)
388 (cexpr2pres_charcount ~priority:70 ~assoc:false ~tail:tail b)
392 Hashtbl.add C2P.symbol_table "minus" (binary
393 (fun a b ~priority ~assoc ~tail aattr sattr ->
394 if (priority > 60) || (priority = 60 && assoc) then
395 P.row_with_brackets aattr
396 (cexpr2pres ~priority:60 ~assoc:true ~tail:[] a)
397 (cexpr2pres ~priority:60 ~assoc:false
398 ~tail:(P.Mtext([],")")::tail) b)
401 P.row_without_brackets aattr
402 (cexpr2pres ~priority:60 ~assoc:true ~tail:[] a)
403 (cexpr2pres ~priority:60 ~assoc:false ~tail:tail b)
406 Hashtbl.add C2P.symbol_table_charcount "minus" (binary
407 (fun a b ~priority ~assoc ~tail aattr sattr ->
408 if (priority > 60) || (priority = 60 && assoc) then
409 P.two_rows_table_with_brackets aattr
410 (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a)
411 (cexpr2pres_charcount ~priority:60 ~assoc:false
412 ~tail:(P.Mtext([],")")::tail) b)
415 P.two_rows_table_without_brackets aattr
416 (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a)
417 (cexpr2pres_charcount ~priority:60 ~assoc:false ~tail:tail b)