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;;
36 module CE = Content_expressions;;
38 let symbol_table = Hashtbl.create 503;;
39 let symbol_table_charcount = Hashtbl.create 503;;
43 let rec countterm current_size t =
44 if current_size > maxsize then current_size
46 CE.Symbol (_,name,None,_) -> current_size + (String.length name)
47 | CE.Symbol (_,name,Some subst,_) ->
48 let c1 = current_size + (String.length name) in
50 | CE.LocalVar (_,name) -> current_size + (String.length name)
51 | CE.Meta (_,name,l) ->
56 | Some t' -> countterm i t'
57 ) (current_size + String.length name) l
58 | CE.Num (_,value) -> current_size + (String.length value)
60 List.fold_left countterm current_size l
61 | CE.Binder (_, _,(n,s),body) ->
62 let cs = countterm (current_size + 2 + (String.length n)) s in
64 | CE.Letin (_,(n,s),body) ->
65 let cs = countterm (current_size + 3 + (String.length n)) s in
67 | CE.Letrec (_,defs,body) ->
70 (fun c (n,bo) -> countterm (c+(String.length n)) bo) current_size defs in
73 let cs = countterm (current_size + 4) a in
75 (fun c (n,bo) -> countterm (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 (countterm c1 expr)) current_size subst
89 ((countterm 0 t) > maxsize)
92 let rec make_attributes l1 =
95 | None::tl -> make_attributes (List.tl l1) tl
97 let p,n = List.hd l1 in
98 (p,n,s)::(make_attributes (List.tl l1) tl)
101 let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t =
102 let module CE = Content_expressions in
103 let module P = Mpresentation in
106 CE.Symbol (xref,name,None,uri) ->
109 [Some "helm","xref";Some "xlink","href"] [xref;uri] in
112 else P.Mrow([],P.Mi (attr,name)::tail)
113 | CE.Symbol (xref,name,Some subst,uri) ->
116 [Some "helm","xref";Some "xlink","href"] [xref;uri] in
123 P.Mi([],UriManager.name_of_uri uri)]
127 P.Mi([],UriManager.name_of_uri uri)::
135 (P.Mtext([],"]")::tail))
136 | CE.LocalVar (xref,name) ->
137 let attr = make_attributes [Some "helm","xref"] [xref] in
140 else P.Mrow([],P.Mi (attr,name)::tail)
141 | CE.Meta (xref,name,l) ->
142 let attr = make_attributes [Some "helm","xref"] [xref] in
147 | Some t -> cexpr2pres t
151 P.Mrow ([],P.Mi (attr,name) :: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")])
154 ([],P.Mi (attr,name):: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")] @ tail)
155 | CE.Num (xref,value) ->
156 let attr = make_attributes [Some "helm","xref"] [xref] in
159 else P.Mrow([],P.Mn (attr,value)::tail)
160 | CE.Appl (axref,CE.Symbol(sxref,n,subst,uri)::tl) ->
161 let aattr = make_attributes [Some "helm","xref"] [axref] in
162 let sattr = make_attributes [Some "helm","xref";Some "xlink","href"] [sxref;uri] in
164 (let f = Hashtbl.find symbol_table n in
165 f tl ~priority ~assoc ~tail aattr sattr)
168 P.Mo([],"(")::P.Mi(sattr,n)::(make_args tl)@(P.Mo([],")")::tail)))
169 | CE.Appl (xref,l) as t ->
170 let attr = make_attributes [Some"helm","xref"] [xref] in
172 P.Mo([],"(")::(make_args l)@(P.Mo([],")")::tail))
173 | CE.Binder (xref, kind,(n,s),body) ->
174 let attr = make_attributes [Some "helm","xref"] [xref] in
176 if kind = "Lambda" then
177 Netconversion.ustring_of_uchar `Enc_utf8 0x03bb
178 else if kind = "Prod" then
179 Netconversion.ustring_of_uchar `Enc_utf8 0x03a0
180 else if kind = "Forall" then
181 Netconversion.ustring_of_uchar `Enc_utf8 0x2200
182 else if kind = "Exists" then
183 Netconversion.ustring_of_uchar `Enc_utf8 0x2203
186 P.Mtext([None,"mathcolor","Blue"],binder)::
187 P.Mtext([],n ^ ":")::
191 | CE.Letin (xref,(n,s),body) ->
192 let attr = make_attributes [Some "helm","xref"] [xref] in
194 P.Mtext([],("let "))::
195 P.Mtext([],(n ^ "="))::
199 | CE.Letrec (xref,defs,body) ->
200 let attr = make_attributes [Some "helm","xref"] [xref] in
205 [P.Mtext([],(n ^ "="));(aux body)]
207 P.Mtext([],(n ^ "="))::
208 (aux body)::P.Mtext([]," and")::(make_defs tl)) in
210 P.Mtext([],("let rec "))::
212 (P.Mtext([]," in ")::
214 | CE.Case (xref,a,np) ->
215 let attr = make_attributes [Some "helm","xref"] [xref] in
216 let rec make_patterns =
219 | [(n,p)] -> make_pattern n p
221 (make_pattern n p)@(P.smallskip::
222 P.Mtext([],"|")::P.smallskip::(make_patterns tl)))
223 and make_pattern n p =
224 let rec get_vars_and_body =
226 CE.Binder (_, "Lambda",(n,_),body) ->
227 let v,b = get_vars_and_body body in
230 let vars,body = get_vars_and_body p in
234 | l -> "(" ^ n ^" "^(String.concat " " l) ^ ")" ^ " -> " in
235 [P.Mtext([],lhs);P.smallskip;aux body] in
237 P.Mtext([],"match")::P.smallskip::
238 (aux a)::P.smallskip::
239 P.Mtext([],"with")::P.smallskip::
240 P.Mtext([],"[")::P.smallskip::
241 (make_patterns np)@(P.smallskip::P.Mtext([],("]"))::tail)) in
246 make_args ?(priority = 0) ?(assoc = false) ?(tail = []) =
247 let module P = Mpresentation in
250 | a::tl -> P.smallskip::(cexpr2pres a)::(make_args ~tail:tail tl)
253 let rec make_args_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) =
254 let module P = Mpresentation in
258 [P.Mtr([],[P.Mtd([],P.indented (cexpr2pres_charcount ~tail:tail a))])]
260 let c = List.fold_left countterm 0 l in
262 P.Mtr([],[P.Mtd([],P.indented (cexpr2pres_charcount a))])::
263 (make_args_charcount ~tail:tail tl)
264 else [P.Mtr([],[P.Mtd([],P.Mrow([],(P.Mspace([None,"width","0.2cm"]))::(make_args ~tail:tail l)))])]
271 let c = List.fold_left countterm 0 tl in
273 P.Mtable ([("align","baseline 1");("equalrows","false");
274 ("columnalign","left")],
275 (make_args_charcount tl))
277 P.Mrow([], make_args tl) in
278 [P.Mtr([],[P.Mtd([],(cexpr2pres_charcount a))]);
279 P.Mtr([],[P.Mtd([],P.indented tlpres)])] *)
282 cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t =
283 if not(is_big t) then (cexpr2pres ~priority ~assoc ~tail t)
284 else let aux = cexpr2pres_charcount in
286 CE.Symbol (xref,name,None,uri) ->
289 [Some "helm","xref";Some "xlink","href"] [xref;uri] in
292 else P.Mrow ([],P.Mi (attr,name)::tail)
293 | CE.Symbol (xref,name,Some subst,uri) ->
296 [Some "helm","xref";Some "xlink","href"] [xref;uri] in
303 P.Mi([],UriManager.name_of_uri uri)]
307 P.Mi([],UriManager.name_of_uri uri)::
315 (P.Mtext([],"]")::tail))
316 | CE.LocalVar (xref,name) ->
317 let attr = make_attributes [Some "helm","xref"] [xref] in
320 else P.Mrow ([],P.Mi (attr,name)::tail)
321 | CE.Meta (xref,name,l) ->
322 let attr = make_attributes [Some "helm","xref"] [xref] in
327 | Some t -> cexpr2pres t
331 P.Mrow ([],P.Mi (attr,name) :: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")])
334 ([],P.Mi (attr,name):: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")] @ tail)
335 | CE.Num (xref,value) ->
336 let attr = make_attributes [Some "helm","xref"] [xref] in
339 else P.Mrow ([],P.Mn (attr,value)::tail)
340 | CE.Appl (axref,CE.Symbol(sxref,n,subst,uri)::tl) ->
341 let aattr = make_attributes [Some "helm","xref"] [axref] in
342 let sattr = make_attributes [Some "helm","xref";Some "xlink","href"] [sxref;uri] in
344 (let f = Hashtbl.find symbol_table_charcount n in
345 f tl ~priority ~assoc ~tail aattr sattr)
347 P.Mtable (aattr@P.standard_tbl_attr,
348 P.Mtr([],[P.Mtd([],P.Mrow([],
350 cexpr2pres (CE.Symbol(sxref,n,subst,uri))]))])::
351 make_args_charcount ~tail:(P.Mtext([],")")::tail) tl))
352 | CE.Appl (xref,l) as t ->
353 let attr = make_attributes [Some "helm","xref"] [xref] in
354 P.Mtable (attr@P.standard_tbl_attr,
355 P.Mtr([],[P.Mtd([],P.Mrow([],
357 cexpr2pres_charcount (List.hd l)]))])::
358 make_args_charcount ~tail:(P.Mtext([],")")::tail) (List.tl l))
359 | CE.Binder (xref, kind,(n,s),body) as t ->
360 let attr = make_attributes [Some "helm","xref"] [xref] in
362 if kind = "Lambda" then
363 Netconversion.ustring_of_uchar `Enc_utf8 0x03bb
364 else if kind = "Prod" then
365 Netconversion.ustring_of_uchar `Enc_utf8 0x03a0
366 else if kind = "Forall" then
367 Netconversion.ustring_of_uchar `Enc_utf8 0x2200
368 else if kind = "Exists" then
369 Netconversion.ustring_of_uchar `Enc_utf8 0x2203
371 P.Mtable (attr@P.standard_tbl_attr,
372 [P.Mtr ([],[P.Mtd ([],
374 [P.Mtext([None,"mathcolor","Blue"],binder);
376 cexpr2pres_charcount s ~tail:[P.Mtext([],".")]]))]);
377 P.Mtr ([],[P.Mtd ([],
378 P.indented (cexpr2pres_charcount body ~tail:tail))])])
379 | CE.Letin (xref,(n,s),body) as t ->
380 let attr = make_attributes [Some "helm","xref"] [xref] in
381 P.Mtable (attr@P.standard_tbl_attr,
382 [P.Mtr ([],[P.Mtd ([],
384 [P.Mtext([None,"mathcolor","Blue"],"let");
387 cexpr2pres_charcount s;
391 P.Mtr ([],[P.Mtd ([],
392 P.indented (cexpr2pres_charcount body))])])
393 | CE.Letrec (xref,defs,body) ->
394 let attr = make_attributes [Some "helm","xref"] [xref] in
399 [P.Mtext([],(n ^ "="));(aux body)]
401 P.Mtext([],(n ^ "="))::
402 (aux body)::P.Mtext([]," and")::(make_defs tl)) in
404 P.Mtext([],("let rec "))::
408 | CE.Case (xref,a,np) ->
409 let attr = make_attributes [Some "helm","xref"] [xref] in
412 let tail = P.Mtext([],(" with"))::tail in
413 [P.Mtr ([],[P.Mtd ([],P.Mtext([],("match ")))]);
414 P.Mtr ([],[P.Mtd ([],aux a ~tail:tail)])]
416 [P.Mtr ([],[P.Mtd ([],P.Mrow([],[P.Mtext([],("match"));P.smallskip;aux a ~tail:tail; P.smallskip;P.Mtext([],("with"))]))])] in
417 let rec make_patterns is_first ~tail =
422 if is_first then "[ " else "| " in
425 make_pattern sep ~tail n p)])]
428 if is_first then "[ " else "| " in
431 make_pattern sep [] n p)])
432 ::(make_patterns false ~tail tl)
433 and make_pattern sep ~tail n p =
434 let rec get_vars_and_body =
436 CE.Binder (_, "Lambda",(n,_),body) ->
437 let v,b = get_vars_and_body body in
440 let vars,body = get_vars_and_body p in
443 [] -> sep ^ n ^ " -> "
444 | l -> sep ^"(" ^n^" "^(String.concat " " l) ^ ")" ^ " -> " in
445 if (is_big body) then
446 P.Mtable (P.standard_tbl_attr,
448 [P.Mtd ([],P.Mtext([],lhs))]);
450 [P.Mtd ([],P.indented (aux ~tail body ))])])
452 P.Mrow([],[P.Mtext([],lhs);aux ~tail body]) in
454 make_patterns true np ~tail:(P.Mtext([],"]")::tail) in
455 P.Mtable (attr@P.standard_tbl_attr,