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 P = Mpresentation;;
37 let symbol_table = Hashtbl.create 503;;
38 let symbol_table_charcount = Hashtbl.create 503;;
42 let countterm current_size t =
43 let module CE = Content_expressions in
44 let rec aux current_size t =
45 if current_size > maxsize then current_size
47 CE.Symbol (_,name,None,_) -> current_size + (String.length name)
48 | CE.Symbol (_,name,Some subst,_) ->
49 let c1 = current_size + (String.length name) in
51 | CE.LocalVar (_,name) -> current_size + (String.length name)
52 | CE.Meta (_,name) -> current_size + (String.length name)
53 | CE.Num (_,value) -> current_size + (String.length value)
55 List.fold_left aux current_size l
56 | CE.Binder (_, _,(n,s),body) ->
57 let cs = aux (current_size + 2 + (String.length n)) s in
59 | CE.Letin (_,(n,s),body) ->
60 let cs = aux (current_size + 3 + (String.length n)) s in
62 | CE.Letrec (_,defs,body) ->
65 (fun c (n,bo) -> aux (c+(String.length n)) bo) current_size defs in
68 let cs = aux (current_size + 4) a in
70 (fun c (n,bo) -> aux (c+(String.length n)) bo) current_size np
72 countsubst subst current_size =
74 (fun current_size (uri,expr) ->
75 if (current_size > maxsize) then current_size
78 (current_size + (String.length (UriManager.name_of_uri uri))) in
79 (aux c1 expr)) current_size subst
85 ((countterm 0 t) > maxsize)
88 let rec make_attributes l1 =
91 | None::tl -> make_attributes (List.tl l1) tl
92 | (Some s)::tl -> (List.hd l1,s)::(make_attributes (List.tl l1) tl)
95 let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t =
96 let module CE = Content_expressions in
97 let module P = Mpresentation in
100 CE.Symbol (xref,name,None,uri) ->
103 ["helm:xref";"xlink:href"] [xref;uri] in
106 else P.Mrow([],P.Mi (attr,name)::tail)
107 | CE.Symbol (xref,name,Some subst,uri) ->
110 ["helm:xref";"xlink:href"] [xref;uri] in
117 P.Mi([],UriManager.name_of_uri uri)]
121 P.Mi([],UriManager.name_of_uri uri)::
129 (P.Mtext([],"]")::tail))
130 | CE.LocalVar (xref,name) ->
131 let attr = make_attributes ["helm:xref"] [xref] in
134 else P.Mrow([],P.Mi (attr,name)::tail)
135 | CE.Meta (xref,name) ->
136 let attr = make_attributes ["helm:xref"] [xref] in
139 else P.Mrow([],P.Mi (attr,name)::tail)
140 | CE.Num (xref,value) ->
141 let attr = make_attributes ["helm:xref"] [xref] in
144 else P.Mrow([],P.Mn (attr,value)::tail)
145 | CE.Appl (axref,CE.Symbol(sxref,n,subst,uri)::tl) ->
146 let aattr = make_attributes ["helm:xref"] [axref] in
147 let sattr = make_attributes ["helm:xref";"xlink:href"] [sxref;uri] in
149 (let f = Hashtbl.find symbol_table n in
150 f tl ~priority ~assoc ~tail aattr sattr)
153 P.Mo([],"(")::P.Mi(sattr,n)::(make_args tl)@(P.Mo([],")")::tail)))
154 | CE.Appl (xref,l) as t ->
155 let attr = make_attributes ["helm:xref"] [xref] in
157 P.Mo([],"(")::(make_args l)@(P.Mo([],")")::tail))
158 | CE.Binder (xref, kind,(n,s),body) ->
159 let attr = make_attributes ["helm:xref"] [xref] in
161 if kind = "Lambda" then
162 Netconversion.ustring_of_uchar `Enc_utf8 0x03bb
163 else if kind = "Prod" then
164 Netconversion.ustring_of_uchar `Enc_utf8 0x03a0
165 else if kind = "Forall" then
166 Netconversion.ustring_of_uchar `Enc_utf8 0x2200
167 else if kind = "Exists" then
168 Netconversion.ustring_of_uchar `Enc_utf8 0x2203
171 P.Mtext([("mathcolor","Blue")],binder)::
172 P.Mtext([],n ^ ":")::
176 | CE.Letin (xref,(n,s),body) ->
177 let attr = make_attributes ["helm:xref"] [xref] in
179 P.Mtext([],("let "))::
180 P.Mtext([],(n ^ "="))::
184 | CE.Letrec (xref,defs,body) ->
185 let attr = make_attributes ["helm:xref"] [xref] in
190 [P.Mtext([],(n ^ "="));(aux body)]
192 P.Mtext([],(n ^ "="))::
193 (aux body)::P.Mtext([]," and")::(make_defs tl)) in
195 P.Mtext([],("let rec "))::
197 (P.Mtext([]," in ")::
199 | CE.Case (xref,a,np) ->
200 let attr = make_attributes ["helm:xref"] [xref] in
201 let rec make_patterns =
205 [P.Mtext([],(n ^ " -> "));(aux p)]
207 P.Mtext([],(n ^ " -> "))::
208 (aux p)::P.Mtext([]," | ")::(make_patterns tl)) in
210 P.Mtext([],("case "))::
212 P.Mtext([],(" of "))::
213 (make_patterns np)@tail) in
218 make_args ?(priority = 0) ?(assoc = false) ?(tail = []) =
219 let module P = Mpresentation in
222 | a::tl -> P.smallskip::(cexpr2pres a)::(make_args ~tail:tail tl)
225 let rec make_args_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) =
226 let module P = Mpresentation in
230 [P.Mtr([],[P.Mtd([],P.indented (cexpr2pres_charcount ~tail:tail a))])]
232 let c = List.fold_left countterm 0 l in
234 P.Mtr([],[P.Mtd([],P.indented (cexpr2pres_charcount a))])::
235 (make_args_charcount ~tail:tail tl)
236 else [P.Mtr([],[P.Mtd([],P.Mrow([],(P.Mspace([("width","0.2cm")]))::(make_args ~tail:tail l)))])]
243 let c = List.fold_left countterm 0 tl in
245 P.Mtable ([("align","baseline 1");("equalrows","false");
246 ("columnalign","left")],
247 (make_args_charcount tl))
249 P.Mrow([], make_args tl) in
250 [P.Mtr([],[P.Mtd([],(cexpr2pres_charcount a))]);
251 P.Mtr([],[P.Mtd([],P.indented tlpres)])] *)
254 cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t =
255 let module CE = Content_expressions in
256 let module P = Mpresentation in
259 CE.Symbol (xref,name,None,uri) ->
262 ["helm:xref";"xlink:href"] [xref;uri] in
265 else P.Mrow ([],P.Mi (attr,name)::tail)
266 | CE.Symbol (xref,name,Some subst,uri) ->
269 ["helm:xref";"xlink:href"] [xref;uri] in
276 P.Mi([],UriManager.name_of_uri uri)]
280 P.Mi([],UriManager.name_of_uri uri)::
288 (P.Mtext([],"]")::tail))
289 | CE.LocalVar (xref,name) ->
290 let attr = make_attributes ["helm:xref"] [xref] in
293 else P.Mrow ([],P.Mi (attr,name)::tail)
294 | CE.Meta (xref,name) ->
295 let attr = make_attributes ["helm:xref"] [xref] in
298 else P.Mrow ([],P.Mi (attr,name)::tail)
299 | CE.Num (xref,value) ->
300 let attr = make_attributes ["helm:xref"] [xref] in
303 else P.Mrow ([],P.Mn (attr,value)::tail)
304 | CE.Appl (axref,CE.Symbol(sxref,n,subst,uri)::tl) ->
305 let aattr = make_attributes ["helm:xref"] [axref] in
306 let sattr = make_attributes ["helm:xref";"xlink:href"] [sxref;uri] in
309 (let f = Hashtbl.find symbol_table_charcount n in
310 f tl ~priority ~assoc ~tail aattr sattr)
312 P.Mtable (aattr@P.standard_tbl_attr,
313 P.Mtr([],[P.Mtd([],P.Mrow([],
315 cexpr2pres (CE.Symbol(sxref,n,subst,uri))]))])::
316 make_args_charcount ~tail:(P.Mtext([],")")::tail) tl))
318 | CE.Appl (xref,l) as t ->
319 let attr = make_attributes ["helm:xref"] [xref] in
321 P.Mtable (attr@P.standard_tbl_attr,
322 P.Mtr([],[P.Mtd([],P.Mrow([],
324 cexpr2pres_charcount (List.hd l)]))])::
325 make_args_charcount ~tail:(P.Mtext([],")")::tail) (List.tl l))
327 | CE.Binder (xref, kind,(n,s),body) as t ->
329 let attr = make_attributes ["helm:xref"] [xref] in
331 if kind = "Lambda" then
332 Netconversion.ustring_of_uchar `Enc_utf8 0x03bb
333 else if kind = "Prod" then
334 Netconversion.ustring_of_uchar `Enc_utf8 0x03a0
335 else if kind = "Forall" then
336 Netconversion.ustring_of_uchar `Enc_utf8 0x2200
337 else if kind = "Exists" then
338 Netconversion.ustring_of_uchar `Enc_utf8 0x2203
340 P.Mtable (attr@P.standard_tbl_attr,
341 [P.Mtr ([],[P.Mtd ([],
343 [P.Mtext([("mathcolor","Blue")],binder);
345 cexpr2pres_charcount s ~tail:[P.Mtext([],".")]]))]);
346 P.Mtr ([],[P.Mtd ([],
347 P.indented (cexpr2pres_charcount body ~tail:tail))])])
348 else (cexpr2pres t ~tail:tail)
349 | CE.Letin (xref,(n,s),body) as t ->
351 let attr = make_attributes ["helm:xref"] [xref] in
352 P.Mtable (attr@P.standard_tbl_attr,
353 [P.Mtr ([],[P.Mtd ([],
355 [P.Mtext([("mathcolor","Blue")],"let");
358 cexpr2pres_charcount s;
362 P.Mtr ([],[P.Mtd ([],
363 P.indented (cexpr2pres_charcount body))])])
365 | CE.Letrec (xref,defs,body) ->
366 let attr = make_attributes ["helm:xref"] [xref] in
371 [P.Mtext([],(n ^ "="));(aux body)]
373 P.Mtext([],(n ^ "="))::
374 (aux body)::P.Mtext([]," and")::(make_defs tl)) in
376 P.Mtext([],("let rec "))::
380 | CE.Case (xref,a,np) ->
381 let attr = make_attributes ["helm:xref"] [xref] in
382 let rec make_patterns =
386 [P.Mtext([],(n ^ " -> "));(aux p)]
388 P.Mtext([],(n ^ " -> "))::
389 (aux p)::P.Mtext([]," | ")::(make_patterns tl)) in
391 P.Mtext([],("case "))::
393 P.Mtext([],(" of "))::
394 (make_patterns np)) in