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,l) ->
58 ) (current_size + String.length name) l
59 | CE.Num (_,value) -> current_size + (String.length value)
61 List.fold_left aux current_size l
62 | CE.Binder (_, _,(n,s),body) ->
63 let cs = aux (current_size + 2 + (String.length n)) s in
65 | CE.Letin (_,(n,s),body) ->
66 let cs = aux (current_size + 3 + (String.length n)) s in
68 | CE.Letrec (_,defs,body) ->
71 (fun c (n,bo) -> aux (c+(String.length n)) bo) current_size defs in
74 let cs = aux (current_size + 4) a in
76 (fun c (n,bo) -> aux (c+(String.length n)) bo) current_size np
78 countsubst subst current_size =
80 (fun current_size (uri,expr) ->
81 if (current_size > maxsize) then current_size
84 (current_size + (String.length (UriManager.name_of_uri uri))) in
85 (aux c1 expr)) current_size subst
91 ((countterm 0 t) > maxsize)
94 let rec make_attributes l1 =
97 | None::tl -> make_attributes (List.tl l1) tl
99 let p,n = List.hd l1 in
100 (p,n,s)::(make_attributes (List.tl l1) tl)
103 let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t =
104 let module CE = Content_expressions in
105 let module P = Mpresentation in
108 CE.Symbol (xref,name,None,uri) ->
111 [Some "helm","xref";Some "xlink","href"] [xref;uri] in
114 else P.Mrow([],P.Mi (attr,name)::tail)
115 | CE.Symbol (xref,name,Some subst,uri) ->
118 [Some "helm","xref";Some "xlink","href"] [xref;uri] in
125 P.Mi([],UriManager.name_of_uri uri)]
129 P.Mi([],UriManager.name_of_uri uri)::
137 (P.Mtext([],"]")::tail))
138 | CE.LocalVar (xref,name) ->
139 let attr = make_attributes [Some "helm","xref"] [xref] in
142 else P.Mrow([],P.Mi (attr,name)::tail)
143 | CE.Meta (xref,name,l) ->
144 let attr = make_attributes [Some "helm","xref"] [xref] in
149 | Some t -> cexpr2pres t
153 P.Mrow ([],P.Mi (attr,name) :: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")])
156 ([],P.Mi (attr,name):: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")] @ tail)
157 | CE.Num (xref,value) ->
158 let attr = make_attributes [Some "helm","xref"] [xref] in
161 else P.Mrow([],P.Mn (attr,value)::tail)
162 | CE.Appl (axref,CE.Symbol(sxref,n,subst,uri)::tl) ->
163 let aattr = make_attributes [Some "helm","xref"] [axref] in
164 let sattr = make_attributes [Some "helm","xref";Some "xlink","href"] [sxref;uri] in
166 (let f = Hashtbl.find symbol_table n in
167 f tl ~priority ~assoc ~tail aattr sattr)
170 P.Mo([],"(")::P.Mi(sattr,n)::(make_args tl)@(P.Mo([],")")::tail)))
171 | CE.Appl (xref,l) as t ->
172 let attr = make_attributes [Some"helm","xref"] [xref] in
174 P.Mo([],"(")::(make_args l)@(P.Mo([],")")::tail))
175 | CE.Binder (xref, kind,(n,s),body) ->
176 let attr = make_attributes [Some "helm","xref"] [xref] in
178 if kind = "Lambda" then
179 Netconversion.ustring_of_uchar `Enc_utf8 0x03bb
180 else if kind = "Prod" then
181 Netconversion.ustring_of_uchar `Enc_utf8 0x03a0
182 else if kind = "Forall" then
183 Netconversion.ustring_of_uchar `Enc_utf8 0x2200
184 else if kind = "Exists" then
185 Netconversion.ustring_of_uchar `Enc_utf8 0x2203
188 P.Mtext([None,"mathcolor","Blue"],binder)::
189 P.Mtext([],n ^ ":")::
193 | CE.Letin (xref,(n,s),body) ->
194 let attr = make_attributes [Some "helm","xref"] [xref] in
196 P.Mtext([],("let "))::
197 P.Mtext([],(n ^ "="))::
201 | CE.Letrec (xref,defs,body) ->
202 let attr = make_attributes [Some "helm","xref"] [xref] in
207 [P.Mtext([],(n ^ "="));(aux body)]
209 P.Mtext([],(n ^ "="))::
210 (aux body)::P.Mtext([]," and")::(make_defs tl)) in
212 P.Mtext([],("let rec "))::
214 (P.Mtext([]," in ")::
216 | CE.Case (xref,a,np) ->
217 let attr = make_attributes [Some "helm","xref"] [xref] in
218 let rec make_patterns =
222 [P.Mtext([],(n ^ " -> "));(aux p)]
224 P.Mtext([],(n ^ " -> "))::
225 (aux p)::P.Mtext([]," | ")::(make_patterns tl)) in
227 P.Mtext([],("case "))::
229 P.Mtext([],(" of "))::
230 (make_patterns np)@tail) in
235 make_args ?(priority = 0) ?(assoc = false) ?(tail = []) =
236 let module P = Mpresentation in
239 | a::tl -> P.smallskip::(cexpr2pres a)::(make_args ~tail:tail tl)
242 let rec make_args_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) =
243 let module P = Mpresentation in
247 [P.Mtr([],[P.Mtd([],P.indented (cexpr2pres_charcount ~tail:tail a))])]
249 let c = List.fold_left countterm 0 l in
251 P.Mtr([],[P.Mtd([],P.indented (cexpr2pres_charcount a))])::
252 (make_args_charcount ~tail:tail tl)
253 else [P.Mtr([],[P.Mtd([],P.Mrow([],(P.Mspace([None,"width","0.2cm"]))::(make_args ~tail:tail l)))])]
260 let c = List.fold_left countterm 0 tl in
262 P.Mtable ([("align","baseline 1");("equalrows","false");
263 ("columnalign","left")],
264 (make_args_charcount tl))
266 P.Mrow([], make_args tl) in
267 [P.Mtr([],[P.Mtd([],(cexpr2pres_charcount a))]);
268 P.Mtr([],[P.Mtd([],P.indented tlpres)])] *)
271 cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t =
272 let module CE = Content_expressions in
273 let module P = Mpresentation in
276 CE.Symbol (xref,name,None,uri) ->
279 [Some "helm","xref";Some "xlink","href"] [xref;uri] in
282 else P.Mrow ([],P.Mi (attr,name)::tail)
283 | CE.Symbol (xref,name,Some subst,uri) ->
286 [Some "helm","xref";Some "xlink","href"] [xref;uri] in
293 P.Mi([],UriManager.name_of_uri uri)]
297 P.Mi([],UriManager.name_of_uri uri)::
305 (P.Mtext([],"]")::tail))
306 | CE.LocalVar (xref,name) ->
307 let attr = make_attributes [Some "helm","xref"] [xref] in
310 else P.Mrow ([],P.Mi (attr,name)::tail)
311 | CE.Meta (xref,name,l) ->
312 let attr = make_attributes [Some "helm","xref"] [xref] in
317 | Some t -> cexpr2pres t
321 P.Mrow ([],P.Mi (attr,name) :: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")])
324 ([],P.Mi (attr,name):: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")] @ tail)
325 | CE.Num (xref,value) ->
326 let attr = make_attributes [Some "helm","xref"] [xref] in
329 else P.Mrow ([],P.Mn (attr,value)::tail)
330 | CE.Appl (axref,CE.Symbol(sxref,n,subst,uri)::tl) ->
331 let aattr = make_attributes [Some "helm","xref"] [axref] in
332 let sattr = make_attributes [Some "helm","xref";Some "xlink","href"] [sxref;uri] in
335 (let f = Hashtbl.find symbol_table_charcount n in
336 f tl ~priority ~assoc ~tail aattr sattr)
338 P.Mtable (aattr@P.standard_tbl_attr,
339 P.Mtr([],[P.Mtd([],P.Mrow([],
341 cexpr2pres (CE.Symbol(sxref,n,subst,uri))]))])::
342 make_args_charcount ~tail:(P.Mtext([],")")::tail) tl))
344 | CE.Appl (xref,l) as t ->
345 let attr = make_attributes [Some "helm","xref"] [xref] in
347 P.Mtable (attr@P.standard_tbl_attr,
348 P.Mtr([],[P.Mtd([],P.Mrow([],
350 cexpr2pres_charcount (List.hd l)]))])::
351 make_args_charcount ~tail:(P.Mtext([],")")::tail) (List.tl l))
353 | CE.Binder (xref, kind,(n,s),body) as t ->
355 let attr = make_attributes [Some "helm","xref"] [xref] in
357 if kind = "Lambda" then
358 Netconversion.ustring_of_uchar `Enc_utf8 0x03bb
359 else if kind = "Prod" then
360 Netconversion.ustring_of_uchar `Enc_utf8 0x03a0
361 else if kind = "Forall" then
362 Netconversion.ustring_of_uchar `Enc_utf8 0x2200
363 else if kind = "Exists" then
364 Netconversion.ustring_of_uchar `Enc_utf8 0x2203
366 P.Mtable (attr@P.standard_tbl_attr,
367 [P.Mtr ([],[P.Mtd ([],
369 [P.Mtext([None,"mathcolor","Blue"],binder);
371 cexpr2pres_charcount s ~tail:[P.Mtext([],".")]]))]);
372 P.Mtr ([],[P.Mtd ([],
373 P.indented (cexpr2pres_charcount body ~tail:tail))])])
374 else (cexpr2pres t ~tail:tail)
375 | CE.Letin (xref,(n,s),body) as t ->
377 let attr = make_attributes [Some "helm","xref"] [xref] in
378 P.Mtable (attr@P.standard_tbl_attr,
379 [P.Mtr ([],[P.Mtd ([],
381 [P.Mtext([None,"mathcolor","Blue"],"let");
384 cexpr2pres_charcount s;
388 P.Mtr ([],[P.Mtd ([],
389 P.indented (cexpr2pres_charcount body))])])
391 | CE.Letrec (xref,defs,body) ->
392 let attr = make_attributes [Some "helm","xref"] [xref] in
397 [P.Mtext([],(n ^ "="));(aux body)]
399 P.Mtext([],(n ^ "="))::
400 (aux body)::P.Mtext([]," and")::(make_defs tl)) in
402 P.Mtext([],("let rec "))::
406 | CE.Case (xref,a,np) ->
407 let attr = make_attributes [Some "helm","xref"] [xref] in
408 let rec make_patterns =
412 [P.Mtext([],(n ^ " -> "));(aux p)]
414 P.Mtext([],(n ^ " -> "))::
415 (aux p)::P.Mtext([]," | ")::(make_patterns tl)) in
417 P.Mtext([],("case "))::
419 P.Mtext([],(" of "))::
420 (make_patterns np)) in