X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcexpr2pres.ml;h=0b303083d0eb50dc2a4f3e2bbfe95b7d543a5660;hb=68d7d68a5505d58c561d39c9e0c8f59872a9d6b1;hp=841ccf3da57e3f58d4c69070b889ef89b2e22b2f;hpb=f7b2e35a7bdadb4fdf0e640428e694703ddf67a5;p=helm.git diff --git a/helm/ocaml/cic_transformations/cexpr2pres.ml b/helm/ocaml/cic_transformations/cexpr2pres.ml index 841ccf3da..0b303083d 100644 --- a/helm/ocaml/cic_transformations/cexpr2pres.ml +++ b/helm/ocaml/cic_transformations/cexpr2pres.ml @@ -49,7 +49,13 @@ let countterm current_size t = 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.Meta (_,name,l) -> + List.fold_left + (fun i t -> + match t with + None -> i + | Some t' -> aux i t' + ) (current_size + String.length name) l | CE.Num (_,value) -> current_size + (String.length value) | CE.Appl (_,l) -> List.fold_left aux current_size l @@ -89,7 +95,9 @@ let rec make_attributes l1 = function [] -> [] | None::tl -> make_attributes (List.tl l1) tl - | (Some s)::tl -> (List.hd l1,s)::(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 = @@ -100,14 +108,14 @@ let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t = CE.Symbol (xref,name,None,uri) -> let attr = make_attributes - ["helm:xref";"xlink:href"] [xref;uri] in + [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 - ["helm:xref";"xlink:href"] [xref;uri] in + [Some "helm","xref";Some "xlink","href"] [xref;uri] in let rec make_subst = (function [] -> assert false @@ -128,23 +136,32 @@ let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t = (make_subst subst)@ (P.Mtext([],"]")::tail)) | CE.LocalVar (xref,name) -> - let attr = make_attributes ["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 ["helm:xref"] [xref] in + 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,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 ([],"]")] @ tail) | CE.Num (xref,value) -> - let attr = make_attributes ["helm:xref"] [xref] in + 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 ["helm:xref"] [axref] in - let sattr = make_attributes ["helm:xref";"xlink:href"] [sxref;uri] in + 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) @@ -152,11 +169,11 @@ let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t = 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 ["helm:xref"] [xref] in + 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 ["helm:xref"] [xref] in + let attr = make_attributes [Some "helm","xref"] [xref] in let binder = if kind = "Lambda" then Netconversion.ustring_of_uchar `Enc_utf8 0x03bb @@ -168,13 +185,13 @@ let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t = Netconversion.ustring_of_uchar `Enc_utf8 0x2203 else "unknown" in P.Mrow (attr, - P.Mtext([("mathcolor","Blue")],binder):: + 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 ["helm:xref"] [xref] in + let attr = make_attributes [Some "helm","xref"] [xref] in P.Mrow (attr, P.Mtext([],("let ")):: P.Mtext([],(n ^ "=")):: @@ -182,7 +199,7 @@ let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t = P.Mtext([]," in "):: (aux body)::tail) | CE.Letrec (xref,defs,body) -> - let attr = make_attributes ["helm:xref"] [xref] in + let attr = make_attributes [Some "helm","xref"] [xref] in let rec make_defs = (function [] -> assert false @@ -197,7 +214,7 @@ let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t = (P.Mtext([]," in "):: (aux body)::tail)) | CE.Case (xref,a,np) -> - let attr = make_attributes ["helm:xref"] [xref] in + let attr = make_attributes [Some "helm","xref"] [xref] in let rec make_patterns = (function [] -> [] @@ -233,7 +250,7 @@ let rec make_args_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) = 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([("width","0.2cm")]))::(make_args ~tail:tail l)))])] + else [P.Mtr([],[P.Mtd([],P.Mrow([],(P.Mspace([None,"width","0.2cm"]))::(make_args ~tail:tail l)))])] (* function @@ -259,14 +276,14 @@ cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t = CE.Symbol (xref,name,None,uri) -> let attr = make_attributes - ["helm:xref";"xlink:href"] [xref;uri] in + [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 - ["helm:xref";"xlink:href"] [xref;uri] in + [Some "helm","xref";Some "xlink","href"] [xref;uri] in let rec make_subst = (function [] -> assert false @@ -287,23 +304,32 @@ cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t = (make_subst subst)@ (P.Mtext([],"]")::tail)) | CE.LocalVar (xref,name) -> - let attr = make_attributes ["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 ["helm:xref"] [xref] in + 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,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 ([],"]")] @ tail) | CE.Num (xref,value) -> - let attr = make_attributes ["helm:xref"] [xref] in + 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 ["helm:xref"] [axref] in - let sattr = make_attributes ["helm:xref";"xlink:href"] [sxref;uri] in + 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 @@ -316,7 +342,7 @@ cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t = make_args_charcount ~tail:(P.Mtext([],")")::tail) tl)) else cexpr2pres t | CE.Appl (xref,l) as t -> - let attr = make_attributes ["helm:xref"] [xref] in + 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([], @@ -326,7 +352,7 @@ cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t = else cexpr2pres t | CE.Binder (xref, kind,(n,s),body) as t -> if (is_big t) then - let attr = make_attributes ["helm:xref"] [xref] in + let attr = make_attributes [Some "helm","xref"] [xref] in let binder = if kind = "Lambda" then Netconversion.ustring_of_uchar `Enc_utf8 0x03bb @@ -340,7 +366,7 @@ cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t = P.Mtable (attr@P.standard_tbl_attr, [P.Mtr ([],[P.Mtd ([], P.Mrow([], - [P.Mtext([("mathcolor","Blue")],binder); + [P.Mtext([None,"mathcolor","Blue"],binder); P.Mtext([],n ^ ":"); cexpr2pres_charcount s ~tail:[P.Mtext([],".")]]))]); P.Mtr ([],[P.Mtd ([], @@ -348,11 +374,11 @@ cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t = else (cexpr2pres t ~tail:tail) | CE.Letin (xref,(n,s),body) as t -> if (is_big t) then - let attr = make_attributes ["helm:xref"] [xref] in + let attr = make_attributes [Some "helm","xref"] [xref] in P.Mtable (attr@P.standard_tbl_attr, [P.Mtr ([],[P.Mtd ([], P.Mrow([], - [P.Mtext([("mathcolor","Blue")],"let"); + [P.Mtext([None,"mathcolor","Blue"],"let"); P.smallskip; P.Mtext([],n ^ "="); cexpr2pres_charcount s; @@ -363,7 +389,7 @@ cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t = P.indented (cexpr2pres_charcount body))])]) else (cexpr2pres t) | CE.Letrec (xref,defs,body) -> - let attr = make_attributes ["helm:xref"] [xref] in + let attr = make_attributes [Some "helm","xref"] [xref] in let rec make_defs = (function [] -> assert false @@ -378,7 +404,7 @@ cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t = [P.Mtext([]," in "); (aux body)]) | CE.Case (xref,a,np) -> - let attr = make_attributes ["helm:xref"] [xref] in + let attr = make_attributes [Some "helm","xref"] [xref] in let rec make_patterns = (function [] -> []