X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Focaml%2Fcic_transformations%2Fcexpr2pres.ml;fp=helm%2Focaml%2Fcic_transformations%2Fcexpr2pres.ml;h=0000000000000000000000000000000000000000;hb=29969baf115afff7eb9ea9e2ca98d40ab7006dcc;hp=5789232bb4e54780fee001461edffd4d4da71e34;hpb=844c8ec10832e5b03456b622db240e18ce014a57;p=helm.git diff --git a/helm/ocaml/cic_transformations/cexpr2pres.ml b/helm/ocaml/cic_transformations/cexpr2pres.ml deleted file mode 100644 index 5789232bb..000000000 --- a/helm/ocaml/cic_transformations/cexpr2pres.ml +++ /dev/null @@ -1,473 +0,0 @@ -(* 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;; -module CE = Content_expressions;; - -let symbol_table = Hashtbl.create 503;; -let symbol_table_charcount = Hashtbl.create 503;; - -let maxsize = 25;; - -let rec countterm 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,l) -> - List.fold_left - (fun i t -> - match t with - None -> i - | Some t' -> countterm i t' - ) (current_size + String.length name) l - | CE.Num (_,value) -> current_size + (String.length value) - | CE.Appl (_,l) -> - List.fold_left countterm current_size l - | CE.Binder (_, _,(n,s),body) -> - let cs = countterm (current_size + 2 + (String.length n)) s in - countterm cs body - | CE.Letin (_,(n,s),body) -> - let cs = countterm (current_size + 3 + (String.length n)) s in - countterm cs body - | CE.Letrec (_,defs,body) -> - let cs = - List.fold_left - (fun c (n,bo) -> countterm (c+(String.length n)) bo) current_size defs in - countterm cs body - | CE.Case (_,a,np) -> - let cs = countterm (current_size + 4) a in - List.fold_left - (fun c (n,bo) -> countterm (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 - (countterm c1 expr)) current_size subst -;; - -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 make_math_tail = List.map (fun s -> P.Mtext ([], s)) - -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)::(make_math_tail 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([],"]")::(make_math_tail 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)::(make_math_tail tail)) - | CE.Meta (xref,name,l) -> - let attr = make_attributes [Some "helm","xref"] [xref] in - let l' = - List.map - (function - None -> P.Mo([],"_") - | Some t -> cexpr2pres t - ) l - in - if tail = [] then - P.Mrow ([],P.Mi (attr,name) :: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")]) - else - P.Mrow - ([],P.Mi (attr,name):: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")] @ (make_math_tail 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)::(make_math_tail 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([],")")::(make_math_tail 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([],")")::(make_math_tail 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)::(make_math_tail 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)::(make_math_tail 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)::(make_math_tail tail))) - | CE.Case (xref,a,np) -> - let attr = make_attributes [Some "helm","xref"] [xref] in - let rec make_patterns = - (function - [] -> [] - | [(n,p)] -> make_pattern n p - | (n,p)::tl -> - (make_pattern n p)@(P.smallskip:: - P.Mtext([],"|")::P.smallskip::(make_patterns tl))) - and make_pattern n p = - let rec get_vars_and_body = - (function - CE.Binder (_, "Lambda",(n,_),body) -> - let v,b = get_vars_and_body body in - n::v,b - | t -> [],t) in - let vars,body = get_vars_and_body p in - let lhs = - match vars with - [] -> n ^ " -> " - | l -> "(" ^ n ^" "^(String.concat " " l) ^ ")" ^ " -> " in - [P.Mtext([],lhs);P.smallskip;aux body] in - P.Mrow (attr, - P.Mtext([],"match")::P.smallskip:: - (aux a)::P.smallskip:: - P.Mtext([],"with")::P.smallskip:: - P.Mtext([],"[")::P.smallskip:: - (make_patterns np)@(P.smallskip::P.Mtext([],("]"))::(make_math_tail tail))) in - aux t - -and - -make_args ?(priority = 0) ?(assoc = false) ?(tail = []) = - function - [] -> List.map (fun s -> P.Mtext ([], s)) tail - | a::tl -> P.smallskip::(cexpr2pres a)::(make_args ~tail:tail tl) -;; - -let make_box_tail = List.map (Box.b_text []) -;; - -let rec make_args_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) = - function - [] -> [] - | [a] -> [Box.indent (cexpr2pres_charcount ~tail:tail a)] - | (a::tl) as l -> - let c = List.fold_left countterm 0 l in - if c > maxsize then - (Box.indent (cexpr2pres_charcount a)):: - (make_args_charcount ~tail:tail tl) - else - [Box.indent (Box.b_object (P.Mrow ([], (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 = - if not (is_big t) then - Box.b_object (cexpr2pres ~priority ~assoc ~tail t) - else let aux = cexpr2pres_charcount in - match t with - CE.Symbol (xref,name,None,uri) -> - let attr = - make_attributes - [Some "helm","xref";Some "xlink","href"] [xref;uri] in - if tail = [] then - Box.b_object (P.Mi (attr,name)) - else - Box.b_h [] (Box.b_object (P.Mi (attr,name)) :: (make_box_tail 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)] -> - [Box.b_object (cexpr2pres a); - Box.b_text [] "/"; - Box.b_object (P.Mi([],UriManager.name_of_uri uri))] - | (uri,a)::tl -> - Box.b_object (cexpr2pres a) :: - Box.b_text [] "/" :: - Box.b_object (P.Mi([],UriManager.name_of_uri uri)) :: - Box.b_text [] "; " :: - Box.smallskip :: - (make_subst tl)) in - Box.b_h [] ( - Box.b_object (P.Mi (attr,name)):: - Box.b_text [] "[":: - (make_subst subst)@ - (Box.b_text [] "]")::(make_box_tail tail) ) - | CE.LocalVar (xref,name) -> - let attr = make_attributes [Some "helm","xref"] [xref] in - if tail = [] then - Box.b_object (P.Mi (attr,name)) - else - Box.b_object (P.Mrow ([], P.Mi (attr,name)::(make_math_tail tail))) - | CE.Meta (xref,name,l) -> - let attr = make_attributes [Some "helm","xref"] [xref] in - let l' = - List.map - (function - None -> P.Mo([],"_") - | Some t -> cexpr2pres t - ) l - in - Box.b_object (P.Mrow ([],P.Mi (attr,name) :: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")] @ (make_math_tail tail))) - | CE.Num (xref,value) -> - let attr = make_attributes [Some "helm","xref"] [xref] in - if tail = [] then - Box.b_object (P.Mn (attr,value)) - else - Box.b_object (P.Mrow ([], P.Mn (attr,value)::(make_math_tail 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_charcount n in - f tl ~priority ~assoc ~tail aattr sattr) - with notfound -> - Box.b_v aattr ( - Box.b_h [] [ - Box.b_text [] "("; - Box.b_object (cexpr2pres (CE.Symbol(sxref,n,subst,uri))) - ] :: - make_args_charcount ~tail:(")"::tail) tl - )) - | CE.Appl (xref,l) as t -> - let attr = make_attributes [Some "helm","xref"] [xref] in - Box.b_v attr ( - Box.b_h [] [ - Box.b_text [] "("; - cexpr2pres_charcount (List.hd l) - ] :: - make_args_charcount ~tail:(")"::tail) (List.tl l) - ) - | CE.Binder (xref, kind,(n,s),body) as t -> - 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 - Box.b_v attr [ - Box.b_h [] [ - Box.b_text [None,"color","blue"] binder; - Box.b_text [] (n ^ ":"); - cexpr2pres_charcount s ~tail:["."] - ]; - Box.b_h [] [ Box.indent (cexpr2pres_charcount body ~tail:tail) ] - ] - | CE.Letin (xref,(n,s),body) as t -> - let attr = make_attributes [Some "helm","xref"] [xref] in - Box.b_v attr [ - Box.b_h [] [ - Box.b_kw "let"; - Box.smallskip; - Box.b_text [] (n ^ "="); - cexpr2pres_charcount s; - Box.smallskip; - Box.b_kw "in" - ]; - Box.indent (cexpr2pres_charcount body) - ] - | CE.Letrec (xref,defs,body) -> - let attr = make_attributes [Some "helm","xref"] [xref] in - let rec make_defs = - (function - [] -> assert false - | [(n,bo)] -> - [Box.b_text [] (n ^ "="); (aux body)] - | (n,bo)::tl -> - Box.b_text [] (n ^ "="):: - (aux body):: - Box.smallskip:: - Box.b_kw "and":: - (make_defs tl)) in - Box.b_h attr ( - Box.b_kw "let" :: - Box.smallskip :: - Box.b_kw "rec" :: - Box.smallskip :: - make_defs defs @ - [ Box.smallskip; Box.b_kw "in"; Box.smallskip; aux body ] - ) - | CE.Case (xref,a,np) -> - let attr = make_attributes [Some "helm","xref"] [xref] in - let arg = - if (is_big a) then - let tail = " with"::tail in (* LUCA: porcheria all'ennesima potenza, TODO ripensare il meccanismo del tail *) - [ Box.b_h [] [ Box.b_kw "match"; Box.smallskip ]; - aux a ~tail - ] - else - [ Box.b_h [] [ - Box.b_kw "match"; - Box.smallskip; - aux a ~tail; - Box.smallskip; - Box.b_kw "with" - ] - ] in - let rec make_patterns is_first ~tail = - function - [] -> [] - | [(n,p)] -> - let sep = if is_first then "[ " else "| " in - [ Box.b_h [] [make_pattern sep ~tail n p] ] - | (n,p)::tl -> - let sep = - if is_first then "[ " else "| " in - [ Box.b_h [] ((make_pattern sep [] n p) :: (make_patterns false ~tail tl)) ] - and make_pattern sep ~tail n p = - let rec get_vars_and_body = - function - CE.Binder (_, "Lambda",(n,_),body) -> - let v,b = get_vars_and_body body in - n::v,b - | t -> [],t in - let vars,body = get_vars_and_body p in - let lhs = - match vars with - [] -> sep ^ n ^ " -> " - | l -> sep ^"(" ^n^" "^(String.concat " " l) ^ ")" ^ " -> " in - if (is_big body) then - Box.b_v [] [ - Box.b_text [] lhs; - Box.indent (aux ~tail body) - ] - else - Box.b_h [] [ Box.b_text [] lhs; aux ~tail body ] - in - let patterns = - make_patterns true np ~tail:("]"::tail) in - Box.b_v attr (arg@patterns) -;; - - -