(* Copyright (C) 2000, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science * Department, University of Bologna, Italy. * * HELM is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License * as published by the Free Software Foundation; either version 2 * of the License, or (at your option) any later version. * * HELM is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU General Public License for more details. * * You should have received a copy of the GNU General Public License * along with HELM; if not, write to the Free Software * Foundation, Inc., 59 Temple Place - Suite 330, Boston, * MA 02111-1307, USA. * * For details, see the HELM World-Wide-Web page, * http://cs.unibo.it/helm/. *) (**************************************************************************) (* *) (* PROJECT HELM *) (* *) (* Andrea Asperti *) (* 28/6/2003 *) (* *) (**************************************************************************) module P = Mpresentation;; let symbol_table = Hashtbl.create 503;; let symbol_table_charcount = Hashtbl.create 503;; let maxsize = 25;; let countterm current_size t = let module CE = Content_expressions in let rec aux current_size t = if current_size > maxsize then current_size else match t with CE.Symbol (_,name,None,_) -> current_size + (String.length name) | CE.Symbol (_,name,Some subst,_) -> let c1 = current_size + (String.length name) in countsubst subst c1 | CE.LocalVar (_,name) -> current_size + (String.length name) | CE.Meta (_,name) -> current_size + (String.length name) | CE.Num (_,value) -> current_size + (String.length value) | CE.Appl (_,l) -> List.fold_left aux current_size l | CE.Binder (_, _,(n,s),body) -> let cs = aux (current_size + 2 + (String.length n)) s in aux cs body | CE.Letin (_,(n,s),body) -> let cs = aux (current_size + 3 + (String.length n)) s in aux cs body | CE.Letrec (_,defs,body) -> let cs = List.fold_left (fun c (n,bo) -> aux (c+(String.length n)) bo) current_size defs in aux cs body | CE.Case (_,a,np) -> let cs = aux (current_size + 4) a in List.fold_left (fun c (n,bo) -> aux (c+(String.length n)) bo) current_size np and countsubst subst current_size = List.fold_left (fun current_size (uri,expr) -> if (current_size > maxsize) then current_size else let c1 = (current_size + (String.length (UriManager.name_of_uri uri))) in (aux c1 expr)) current_size subst in (aux current_size t) ;; let is_big t = ((countterm 0 t) > maxsize) ;; let rec make_attributes l1 = function [] -> [] | None::tl -> make_attributes (List.tl l1) tl | (Some s)::tl -> let p,n = List.hd l1 in (p,n,s)::(make_attributes (List.tl l1) tl) ;; let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t = let module CE = Content_expressions in let module P = Mpresentation in let rec aux = function CE.Symbol (xref,name,None,uri) -> let attr = make_attributes [Some "helm","xref";Some "xlink","href"] [xref;uri] in if tail = [] then P.Mi (attr,name) else P.Mrow([],P.Mi (attr,name)::tail) | CE.Symbol (xref,name,Some subst,uri) -> let attr = make_attributes [Some "helm","xref";Some "xlink","href"] [xref;uri] in let rec make_subst = (function [] -> assert false | [(uri,a)] -> [(aux a); P.Mtext([],"/"); P.Mi([],UriManager.name_of_uri uri)] | (uri,a)::tl -> (aux a):: P.Mtext([],"/"):: P.Mi([],UriManager.name_of_uri uri):: P.Mtext([],"; "):: P.smallskip:: (make_subst tl)) in P.Mrow ([], P.Mi (attr,name):: P.Mtext([],"["):: (make_subst subst)@ (P.Mtext([],"]")::tail)) | CE.LocalVar (xref,name) -> let attr = make_attributes [Some "helm","xref"] [xref] in if tail = [] then P.Mi (attr,name) else P.Mrow([],P.Mi (attr,name)::tail) | CE.Meta (xref,name) -> let attr = make_attributes [Some "helm","xref"] [xref] in if tail = [] then P.Mi (attr,name) else P.Mrow([],P.Mi (attr,name)::tail) | CE.Num (xref,value) -> let attr = make_attributes [Some "helm","xref"] [xref] in if tail = [] then P.Mn (attr,value) else P.Mrow([],P.Mn (attr,value)::tail) | CE.Appl (axref,CE.Symbol(sxref,n,subst,uri)::tl) -> let aattr = make_attributes [Some "helm","xref"] [axref] in let sattr = make_attributes [Some "helm","xref";Some "xlink","href"] [sxref;uri] in (try (let f = Hashtbl.find symbol_table n in f tl ~priority ~assoc ~tail aattr sattr) with notfound -> P.Mrow(aattr, P.Mo([],"(")::P.Mi(sattr,n)::(make_args tl)@(P.Mo([],")")::tail))) | CE.Appl (xref,l) as t -> let attr = make_attributes [Some"helm","xref"] [xref] in P.Mrow(attr, P.Mo([],"(")::(make_args l)@(P.Mo([],")")::tail)) | CE.Binder (xref, kind,(n,s),body) -> let attr = make_attributes [Some "helm","xref"] [xref] in let binder = if kind = "Lambda" then Netconversion.ustring_of_uchar `Enc_utf8 0x03bb else if kind = "Prod" then Netconversion.ustring_of_uchar `Enc_utf8 0x03a0 else if kind = "Forall" then Netconversion.ustring_of_uchar `Enc_utf8 0x2200 else if kind = "Exists" then Netconversion.ustring_of_uchar `Enc_utf8 0x2203 else "unknown" in P.Mrow (attr, P.Mtext([None,"mathcolor","Blue"],binder):: P.Mtext([],n ^ ":"):: (aux s):: P.Mo([],"."):: (aux body)::tail) | CE.Letin (xref,(n,s),body) -> let attr = make_attributes [Some "helm","xref"] [xref] in P.Mrow (attr, P.Mtext([],("let ")):: P.Mtext([],(n ^ "=")):: (aux s):: P.Mtext([]," in "):: (aux body)::tail) | CE.Letrec (xref,defs,body) -> let attr = make_attributes [Some "helm","xref"] [xref] in let rec make_defs = (function [] -> assert false | [(n,bo)] -> [P.Mtext([],(n ^ "="));(aux body)] | (n,bo)::tl -> P.Mtext([],(n ^ "=")):: (aux body)::P.Mtext([]," and")::(make_defs tl)) in P.Mrow (attr, P.Mtext([],("let rec ")):: (make_defs defs)@ (P.Mtext([]," in "):: (aux body)::tail)) | CE.Case (xref,a,np) -> let attr = make_attributes [Some "helm","xref"] [xref] in let rec make_patterns = (function [] -> [] | [(n,p)] -> [P.Mtext([],(n ^ " -> "));(aux p)] | (n,p)::tl -> P.Mtext([],(n ^ " -> ")):: (aux p)::P.Mtext([]," | ")::(make_patterns tl)) in P.Mrow (attr, P.Mtext([],("case ")):: (aux a):: P.Mtext([],(" of ")):: (make_patterns np)@tail) in aux t and make_args ?(priority = 0) ?(assoc = false) ?(tail = []) = let module P = Mpresentation in function [] -> tail | a::tl -> P.smallskip::(cexpr2pres a)::(make_args ~tail:tail tl) ;; let rec make_args_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) = let module P = Mpresentation in function [] -> [] | [a] -> [P.Mtr([],[P.Mtd([],P.indented (cexpr2pres_charcount ~tail:tail a))])] | (a::tl) as l -> let c = List.fold_left countterm 0 l in if c > maxsize then P.Mtr([],[P.Mtd([],P.indented (cexpr2pres_charcount a))]):: (make_args_charcount ~tail:tail tl) else [P.Mtr([],[P.Mtd([],P.Mrow([],(P.Mspace([None,"width","0.2cm"]))::(make_args ~tail:tail l)))])] (* function [] -> [] | a::tl -> let tlpres = let c = List.fold_left countterm 0 tl in if c > maxsize then P.Mtable ([("align","baseline 1");("equalrows","false"); ("columnalign","left")], (make_args_charcount tl)) else P.Mrow([], make_args tl) in [P.Mtr([],[P.Mtd([],(cexpr2pres_charcount a))]); P.Mtr([],[P.Mtd([],P.indented tlpres)])] *) and cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t = let module CE = Content_expressions in let module P = Mpresentation in let rec aux = function CE.Symbol (xref,name,None,uri) -> let attr = make_attributes [Some "helm","xref";Some "xlink","href"] [xref;uri] in if tail = [] then P.Mi (attr,name) else P.Mrow ([],P.Mi (attr,name)::tail) | CE.Symbol (xref,name,Some subst,uri) -> let attr = make_attributes [Some "helm","xref";Some "xlink","href"] [xref;uri] in let rec make_subst = (function [] -> assert false | [(uri,a)] -> [(cexpr2pres a); P.Mtext([],"/"); P.Mi([],UriManager.name_of_uri uri)] | (uri,a)::tl -> (cexpr2pres a):: P.Mtext([],"/"):: P.Mi([],UriManager.name_of_uri uri):: P.Mtext([],"; "):: P.smallskip:: (make_subst tl)) in P.Mrow ([], P.Mi (attr,name):: P.Mtext([],"["):: (make_subst subst)@ (P.Mtext([],"]")::tail)) | CE.LocalVar (xref,name) -> let attr = make_attributes [Some "helm","xref"] [xref] in if tail = [] then P.Mi (attr,name) else P.Mrow ([],P.Mi (attr,name)::tail) | CE.Meta (xref,name) -> let attr = make_attributes [Some "helm","xref"] [xref] in if tail = [] then P.Mi (attr,name) else P.Mrow ([],P.Mi (attr,name)::tail) | CE.Num (xref,value) -> let attr = make_attributes [Some "helm","xref"] [xref] in if tail = [] then P.Mn (attr,value) else P.Mrow ([],P.Mn (attr,value)::tail) | CE.Appl (axref,CE.Symbol(sxref,n,subst,uri)::tl) -> let aattr = make_attributes [Some "helm","xref"] [axref] in let sattr = make_attributes [Some "helm","xref";Some "xlink","href"] [sxref;uri] in if (is_big t) then (try (let f = Hashtbl.find symbol_table_charcount n in f tl ~priority ~assoc ~tail aattr sattr) with notfound -> P.Mtable (aattr@P.standard_tbl_attr, P.Mtr([],[P.Mtd([],P.Mrow([], [P.Mtext([],"("); cexpr2pres (CE.Symbol(sxref,n,subst,uri))]))]):: make_args_charcount ~tail:(P.Mtext([],")")::tail) tl)) else cexpr2pres t | CE.Appl (xref,l) as t -> let attr = make_attributes [Some "helm","xref"] [xref] in if (is_big t) then P.Mtable (attr@P.standard_tbl_attr, P.Mtr([],[P.Mtd([],P.Mrow([], [P.Mtext([],"("); cexpr2pres_charcount (List.hd l)]))]):: make_args_charcount ~tail:(P.Mtext([],")")::tail) (List.tl l)) else cexpr2pres t | CE.Binder (xref, kind,(n,s),body) as t -> if (is_big t) then let attr = make_attributes [Some "helm","xref"] [xref] in let binder = if kind = "Lambda" then Netconversion.ustring_of_uchar `Enc_utf8 0x03bb else if kind = "Prod" then Netconversion.ustring_of_uchar `Enc_utf8 0x03a0 else if kind = "Forall" then Netconversion.ustring_of_uchar `Enc_utf8 0x2200 else if kind = "Exists" then Netconversion.ustring_of_uchar `Enc_utf8 0x2203 else "unknown" in P.Mtable (attr@P.standard_tbl_attr, [P.Mtr ([],[P.Mtd ([], P.Mrow([], [P.Mtext([None,"mathcolor","Blue"],binder); P.Mtext([],n ^ ":"); cexpr2pres_charcount s ~tail:[P.Mtext([],".")]]))]); P.Mtr ([],[P.Mtd ([], P.indented (cexpr2pres_charcount body ~tail:tail))])]) else (cexpr2pres t ~tail:tail) | CE.Letin (xref,(n,s),body) as t -> if (is_big t) then let attr = make_attributes [Some "helm","xref"] [xref] in P.Mtable (attr@P.standard_tbl_attr, [P.Mtr ([],[P.Mtd ([], P.Mrow([], [P.Mtext([None,"mathcolor","Blue"],"let"); P.smallskip; P.Mtext([],n ^ "="); cexpr2pres_charcount s; P.smallskip; P.Mtext([],"in"); ]))]); P.Mtr ([],[P.Mtd ([], P.indented (cexpr2pres_charcount body))])]) else (cexpr2pres t) | CE.Letrec (xref,defs,body) -> let attr = make_attributes [Some "helm","xref"] [xref] in let rec make_defs = (function [] -> assert false | [(n,bo)] -> [P.Mtext([],(n ^ "="));(aux body)] | (n,bo)::tl -> P.Mtext([],(n ^ "=")):: (aux body)::P.Mtext([]," and")::(make_defs tl)) in P.Mrow (attr, P.Mtext([],("let rec ")):: (make_defs defs)@ [P.Mtext([]," in "); (aux body)]) | CE.Case (xref,a,np) -> let attr = make_attributes [Some "helm","xref"] [xref] in let rec make_patterns = (function [] -> [] | [(n,p)] -> [P.Mtext([],(n ^ " -> "));(aux p)] | (n,p)::tl -> P.Mtext([],(n ^ " -> ")):: (aux p)::P.Mtext([]," | ")::(make_patterns tl)) in P.Mrow (attr, P.Mtext([],("case ")):: (aux a):: P.Mtext([],(" of ")):: (make_patterns np)) in aux t ;;