From 9ab5ca8acba80b19a939eea2cd87761507e7128b Mon Sep 17 00:00:00 2001 From: Luca Padovani Date: Tue, 28 Sep 2004 16:00:52 +0000 Subject: [PATCH] * the transformations have been ported so to generate BoxML + MathML instead of MathML alone. All the affected files have been heavily changed both in the interface and in the implementation, many solutions are certainly temporary and the code would benefit from extensive cleanup --- helm/ocaml/cic_transformations/.depend | 37 +- helm/ocaml/cic_transformations/Makefile | 4 +- .../applyTransformation.ml | 13 +- helm/ocaml/cic_transformations/box.ml | 49 +- helm/ocaml/cic_transformations/box.mli | 9 + helm/ocaml/cic_transformations/cexpr2pres.ml | 217 ++++--- helm/ocaml/cic_transformations/cexpr2pres.mli | 12 +- .../cic_transformations/cexpr2pres_hashtbl.ml | 204 +++--- .../cexpr2pres_hashtbl.mli | 6 +- helm/ocaml/cic_transformations/cicAstPp.ml | 2 +- .../ocaml/cic_transformations/content2pres.ml | 604 ++++++++---------- .../cic_transformations/content2pres.mli | 2 +- .../cic_transformations/mpresentation.ml | 2 +- .../cic_transformations/mpresentation.mli | 4 +- .../ocaml/cic_transformations/sequent2pres.ml | 41 +- .../cic_transformations/sequent2pres.mli | 2 +- helm/ocaml/cic_transformations/xml2Gdome.ml | 4 + 17 files changed, 610 insertions(+), 602 deletions(-) diff --git a/helm/ocaml/cic_transformations/.depend b/helm/ocaml/cic_transformations/.depend index c35209cdb..3678d39ba 100644 --- a/helm/ocaml/cic_transformations/.depend +++ b/helm/ocaml/cic_transformations/.depend @@ -1,9 +1,10 @@ contentTable.cmi: cicAst.cmo +box.cmi: mpresentation.cmi cexpr2pres.cmi: content_expressions.cmi mpresentation.cmi -content2pres.cmi: mpresentation.cmi +content2pres.cmi: box.cmi mpresentation.cmi cicAstPp.cmi: cicAst.cmo ast2pres.cmi: box.cmi cicAst.cmo -sequent2pres.cmi: mpresentation.cmi +sequent2pres.cmi: box.cmi mpresentation.cmi cexpr2pres_hashtbl.cmi: content_expressions.cmi mpresentation.cmi acic2Ast.cmi: cicAst.cmo tacticAstPp.cmi: cicAst.cmo tacticAst.cmo @@ -11,8 +12,6 @@ boxPp.cmi: box.cmi cicAst.cmo tacticAst2Box.cmi: box.cmi cicAst.cmo tacticAst.cmo tacticAst.cmo: cicAst.cmo tacticAst.cmx: cicAst.cmx -box.cmo: box.cmi -box.cmx: box.cmi contentTable.cmo: cicAst.cmo contentTable.cmi contentTable.cmx: cicAst.cmx contentTable.cmi cic2Xml.cmo: cic2Xml.cmi @@ -21,20 +20,22 @@ content_expressions.cmo: content_expressions.cmi content_expressions.cmx: content_expressions.cmi mpresentation.cmo: mpresentation.cmi mpresentation.cmx: mpresentation.cmi +box.cmo: mpresentation.cmi box.cmi +box.cmx: mpresentation.cmx box.cmi cexpr2pres.cmo: content_expressions.cmi mpresentation.cmi cexpr2pres.cmi cexpr2pres.cmx: content_expressions.cmx mpresentation.cmx cexpr2pres.cmi -content2pres.cmo: cexpr2pres.cmi content_expressions.cmi mpresentation.cmi \ - content2pres.cmi -content2pres.cmx: cexpr2pres.cmx content_expressions.cmx mpresentation.cmx \ - content2pres.cmi +content2pres.cmo: box.cmi cexpr2pres.cmi content_expressions.cmi \ + mpresentation.cmi content2pres.cmi +content2pres.cmx: box.cmx cexpr2pres.cmx content_expressions.cmx \ + mpresentation.cmx content2pres.cmi cicAstPp.cmo: cicAst.cmo cicAstPp.cmi cicAstPp.cmx: cicAst.cmx cicAstPp.cmi ast2pres.cmo: box.cmi cicAst.cmo cicAstPp.cmi ast2pres.cmi ast2pres.cmx: box.cmx cicAst.cmx cicAstPp.cmx ast2pres.cmi -sequent2pres.cmo: cexpr2pres.cmi content_expressions.cmi mpresentation.cmi \ - sequent2pres.cmi -sequent2pres.cmx: cexpr2pres.cmx content_expressions.cmx mpresentation.cmx \ - sequent2pres.cmi +sequent2pres.cmo: box.cmi cexpr2pres.cmi content_expressions.cmi \ + mpresentation.cmi sequent2pres.cmi +sequent2pres.cmx: box.cmx cexpr2pres.cmx content_expressions.cmx \ + mpresentation.cmx sequent2pres.cmi cexpr2pres_hashtbl.cmo: cexpr2pres.cmi content_expressions.cmi \ mpresentation.cmi cexpr2pres_hashtbl.cmi cexpr2pres_hashtbl.cmx: cexpr2pres.cmx content_expressions.cmx \ @@ -49,12 +50,12 @@ applyStylesheets.cmo: cic2Xml.cmi misc.cmi sequentPp.cmi xml2Gdome.cmi \ applyStylesheets.cmi applyStylesheets.cmx: cic2Xml.cmx misc.cmx sequentPp.cmx xml2Gdome.cmx \ applyStylesheets.cmi -applyTransformation.cmo: cexpr2pres.cmi cexpr2pres_hashtbl.cmi \ - content2pres.cmi misc.cmi mpresentation.cmi sequent2pres.cmi \ - xml2Gdome.cmi applyTransformation.cmi -applyTransformation.cmx: cexpr2pres.cmx cexpr2pres_hashtbl.cmx \ - content2pres.cmx misc.cmx mpresentation.cmx sequent2pres.cmx \ - xml2Gdome.cmx applyTransformation.cmi +applyTransformation.cmo: box.cmi cexpr2pres.cmi cexpr2pres_hashtbl.cmi \ + content2pres.cmi misc.cmi sequent2pres.cmi xml2Gdome.cmi \ + applyTransformation.cmi +applyTransformation.cmx: box.cmx cexpr2pres.cmx cexpr2pres_hashtbl.cmx \ + content2pres.cmx misc.cmx sequent2pres.cmx xml2Gdome.cmx \ + applyTransformation.cmi acic2Ast.cmo: cicAst.cmo acic2Ast.cmi acic2Ast.cmx: cicAst.cmx acic2Ast.cmi tacticAstPp.cmo: cicAstPp.cmi tacticAst.cmo tacticAstPp.cmi diff --git a/helm/ocaml/cic_transformations/Makefile b/helm/ocaml/cic_transformations/Makefile index 9b16740b3..95d86a7cd 100644 --- a/helm/ocaml/cic_transformations/Makefile +++ b/helm/ocaml/cic_transformations/Makefile @@ -6,9 +6,9 @@ PREDICATES = # modules which have both a .ml and a .mli INTERFACE_FILES = \ - box.mli contentTable.mli \ + contentTable.mli \ cic2Xml.mli content_expressions.mli \ - mpresentation.mli cexpr2pres.mli content2pres.mli \ + mpresentation.mli box.mli cexpr2pres.mli content2pres.mli \ cicAstPp.mli ast2pres.mli \ sequent2pres.mli \ cexpr2pres_hashtbl.mli misc.mli xml2Gdome.mli sequentPp.mli \ diff --git a/helm/ocaml/cic_transformations/applyTransformation.ml b/helm/ocaml/cic_transformations/applyTransformation.ml index be363c50b..ee01f55a9 100644 --- a/helm/ocaml/cic_transformations/applyTransformation.ml +++ b/helm/ocaml/cic_transformations/applyTransformation.ml @@ -43,9 +43,14 @@ let mml_of_cic_sequent metasenv sequent = let content_sequent = Cic2content.map_sequent asequent in let pres_sequent = (Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent) in - let xmlpres = Mpresentation.print_mpres pres_sequent in - Xml2Gdome.document_of_xml Misc.domImpl xmlpres, - (ids_to_terms,ids_to_father_ids,ids_to_hypotheses) + let xmlpres = Box.document_of_box pres_sequent in + (* Xml.pp_to_outchan xmlpres stdout ; *) + try + Xml2Gdome.document_of_xml Misc.domImpl xmlpres, (ids_to_terms,ids_to_father_ids,ids_to_hypotheses) + with + e -> + prerr_endline ("LUCA: eccezione in document_of_xml " ^ (Printexc.to_string e)) ; + raise e ;; let mml_of_cic_object ~explode_all uri acic @@ -60,7 +65,7 @@ let mml_of_cic_object ~explode_all uri acic let pres = Content2pres.content2pres ~ids_to_inner_sorts content in let time2 = Sys.time () in (* prerr_endline ("Fine trasformazione:" ^ (string_of_float (time2 -. time1))); *) - let xmlpres = Mpresentation.print_mpres pres in + let xmlpres = Box.document_of_box pres in let time25 = Sys.time () in (* alternative: printing to file prerr_endline ("FINE printing to stream:" ^ (string_of_float (time25 -. time2))); diff --git a/helm/ocaml/cic_transformations/box.ml b/helm/ocaml/cic_transformations/box.ml index 41b7fb725..764a491eb 100644 --- a/helm/ocaml/cic_transformations/box.ml +++ b/helm/ocaml/cic_transformations/box.ml @@ -36,6 +36,7 @@ type 'expr box = Text of attr * string | Space of attr + | Ink of attr | H of attr * ('expr box) list | V of attr * ('expr box) list | Object of attr * 'expr @@ -43,8 +44,52 @@ type and attr = (string option * string * string) list -let smallskip = Text([]," ");; -let skip = Text([]," ");; +let smallskip = Space([None,"width","0.5em"]);; +let skip = Space([None,"width","1em"]);; let indent t = H([],[skip;t]);; +(* MathML prefix *) +let prefix = "b";; + +let rec print_box = + let module X = Xml in + function + Text (attr,s) -> X.xml_nempty ~prefix "text" attr (X.xml_cdata s) + | Space attr -> X.xml_empty ~prefix "space" attr + | Ink attr -> X.xml_empty ~prefix "ink" attr + | H (attr,l) -> + X.xml_nempty ~prefix "h" attr + [< (List.fold_right (fun x i -> [< (print_box x) ; i >]) l [<>]) + >] + | V (attr,l) -> + X.xml_nempty ~prefix "v" attr + [< (List.fold_right (fun x i -> [< (print_box x) ; i >]) l [<>]) + >] + | Object (attr,m) -> + X.xml_nempty ~prefix "obj" attr [< Mpresentation.print_mpres m >] + | Action (attr,l) -> + X.xml_nempty ~prefix "action" attr + [< (List.fold_right (fun x i -> [< (print_box x) ; i >]) l [<>]) + >] +;; + +let document_of_box pres = + [< Xml.xml_cdata "\n" ; + Xml.xml_cdata "\n"; + Xml.xml_nempty ~prefix "box" + [Some "xmlns","m","http://www.w3.org/1998/Math/MathML" ; + Some "xmlns","b","http://helm.cs.unibo.it/2003/BoxML" ; + Some "xmlns","helm","http://www.cs.unibo.it/helm" ; + Some "xmlns","xlink","http://www.w3.org/1999/xlink" + ] (print_box pres) + >] + +let b_h a b = H(a,b) +let b_v a b = V(a,b) +let b_text a b = Text(a,b) +let b_object b = Object ([],b) +let b_indent = indent +let b_space = Space [None, "width", "0.5em"] +let b_kw = b_text [None, "color", "red"] + diff --git a/helm/ocaml/cic_transformations/box.mli b/helm/ocaml/cic_transformations/box.mli index 2c98b2969..e4d4bbe76 100644 --- a/helm/ocaml/cic_transformations/box.mli +++ b/helm/ocaml/cic_transformations/box.mli @@ -36,6 +36,7 @@ type 'expr box = Text of attr * string | Space of attr + | Ink of attr | H of attr * ('expr box) list | V of attr * ('expr box) list | Object of attr * 'expr @@ -47,5 +48,13 @@ val smallskip : 'expr box val skip: 'expr box val indent : 'expr box -> 'expr box +val document_of_box : Mpresentation.mpres box -> Xml.token Stream.t +val b_h: attr -> 'expr box list -> 'expr box +val b_v: attr -> 'expr box list -> 'expr box +val b_text: attr -> string -> 'expr box +val b_object: 'expr -> 'expr box +val b_indent: 'expr box -> 'expr box +val b_space: 'expr box +val b_kw: string -> 'expr box diff --git a/helm/ocaml/cic_transformations/cexpr2pres.ml b/helm/ocaml/cic_transformations/cexpr2pres.ml index 5210840c8..6f11f561c 100644 --- a/helm/ocaml/cic_transformations/cexpr2pres.ml +++ b/helm/ocaml/cic_transformations/cexpr2pres.ml @@ -98,6 +98,8 @@ let rec make_attributes l1 = (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 @@ -109,7 +111,7 @@ let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t = [Some "helm","xref";Some "xlink","href"] [xref;uri] in if tail = [] then P.Mi (attr,name) - else P.Mrow([],P.Mi (attr,name)::tail) + else P.Mrow([],P.Mi (attr,name)::(make_math_tail tail)) | CE.Symbol (xref,name,Some subst,uri) -> let attr = make_attributes @@ -132,12 +134,12 @@ let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t = P.Mi (attr,name):: P.Mtext([],"["):: (make_subst subst)@ - (P.Mtext([],"]")::tail)) + (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)::tail) + 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' = @@ -151,12 +153,12 @@ let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t = P.Mrow ([],P.Mi (attr,name) :: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")]) else P.Mrow - ([],P.Mi (attr,name):: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")] @ tail) + ([],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)::tail) + 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 @@ -165,11 +167,11 @@ let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t = f tl ~priority ~assoc ~tail aattr sattr) with notfound -> P.Mrow(aattr, - P.Mo([],"(")::P.Mi(sattr,n)::(make_args tl)@(P.Mo([],")")::tail))) + 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([],")")::tail)) + 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 = @@ -187,7 +189,7 @@ let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t = P.Mtext([],n ^ ":"):: (aux s):: P.Mo([],"."):: - (aux body)::tail) + (aux body)::(make_math_tail tail)) | CE.Letin (xref,(n,s),body) -> let attr = make_attributes [Some "helm","xref"] [xref] in P.Mrow (attr, @@ -195,7 +197,7 @@ let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t = P.Mtext([],(n ^ "=")):: (aux s):: P.Mtext([]," in "):: - (aux body)::tail) + (aux body)::(make_math_tail tail)) | CE.Letrec (xref,defs,body) -> let attr = make_attributes [Some "helm","xref"] [xref] in let rec make_defs = @@ -210,7 +212,7 @@ let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t = P.Mtext([],("let rec ")):: (make_defs defs)@ (P.Mtext([]," in "):: - (aux body)::tail)) + (aux body)::(make_math_tail tail))) | CE.Case (xref,a,np) -> let attr = make_attributes [Some "helm","xref"] [xref] in let rec make_patterns = @@ -238,30 +240,31 @@ let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t = (aux a)::P.smallskip:: P.Mtext([],"with")::P.smallskip:: P.Mtext([],"[")::P.smallskip:: - (make_patterns np)@(P.smallskip::P.Mtext([],("]"))::tail)) in + (make_patterns np)@(P.smallskip::P.Mtext([],("]"))::(make_math_tail tail))) in aux t and make_args ?(priority = 0) ?(assoc = false) ?(tail = []) = - let module P = Mpresentation in function - [] -> tail + [] -> 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 = []) = - let module P = Mpresentation in function [] -> [] - | [a] -> - [P.Mtr([],[P.Mtd([],P.indented (cexpr2pres_charcount ~tail:tail a))])] + | [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 - P.Mtr([],[P.Mtd([],P.indented (cexpr2pres_charcount a))]):: + (Box.indent (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)))])] + else + [Box.indent (Box.b_object (P.Mrow ([], (make_args ~tail:tail l))))] (* function @@ -280,7 +283,8 @@ let rec make_args_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) = and cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t = - if not(is_big t) then (cexpr2pres ~priority ~assoc ~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) -> @@ -288,8 +292,9 @@ cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t = 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) + 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 @@ -298,26 +303,27 @@ cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t = (function [] -> assert false | [(uri,a)] -> - [(cexpr2pres a); - P.Mtext([],"/"); - P.Mi([],UriManager.name_of_uri uri)] + [Box.b_object (cexpr2pres a); + Box.b_text [] "/"; + Box.b_object (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:: + 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 - P.Mrow ([], - P.Mi (attr,name):: - P.Mtext([],"["):: + Box.b_h [] ( + Box.b_object (P.Mi (attr,name)):: + Box.b_text [] "[":: (make_subst subst)@ - (P.Mtext([],"]")::tail)) + (Box.b_text [] "]")::(make_box_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)::tail) + 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' = @@ -327,16 +333,13 @@ cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t = | 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) + 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 - P.Mn (attr,value) - else P.Mrow ([],P.Mn (attr,value)::tail) + 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 @@ -344,18 +347,22 @@ cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t = (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)) + 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 - 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)) + 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 = @@ -368,68 +375,75 @@ cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t = 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))])]) + 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 - 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))])]) + 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)] -> - [P.Mtext([],(n ^ "="));(aux body)] + [Box.b_text [] (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)]) + 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 = P.Mtext([],(" with"))::tail in - [P.Mtr ([],[P.Mtd ([],P.Mtext([],("match ")))]); - P.Mtr ([],[P.Mtd ([],aux a ~tail:tail)])] + 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 - [P.Mtr ([],[P.Mtd ([],P.Mrow([],[P.Mtext([],("match"));P.smallskip;aux a ~tail:tail; P.smallskip;P.Mtext([],("with"))]))])] in + [ 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 - [P.Mtr ([], - [P.Mtd ([], - make_pattern sep ~tail 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 - P.Mtr ([], - [P.Mtd ([], - make_pattern sep [] n p)]) - ::(make_patterns false ~tail tl) + [ 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 @@ -443,17 +457,16 @@ cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t = [] -> sep ^ n ^ " -> " | l -> sep ^"(" ^n^" "^(String.concat " " l) ^ ")" ^ " -> " in if (is_big body) then - P.Mtable (P.standard_tbl_attr, - [P.Mtr ([], - [P.Mtd ([],P.Mtext([],lhs))]); - P.Mtr ([], - [P.Mtd ([],P.indented (aux ~tail body ))])]) + Box.b_v [] [ + Box.b_text [] lhs; + Box.indent (aux ~tail body) + ] else - P.Mrow([],[P.Mtext([],lhs);aux ~tail body]) in + Box.b_h [] [ Box.b_text [] lhs; aux ~tail body ] + in let patterns = - make_patterns true np ~tail:(P.Mtext([],"]")::tail) in - P.Mtable (attr@P.standard_tbl_attr, - arg@patterns) + make_patterns true np ~tail:("]"::tail) in + Box.b_v attr (arg@patterns) ;; diff --git a/helm/ocaml/cic_transformations/cexpr2pres.mli b/helm/ocaml/cic_transformations/cexpr2pres.mli index 2bdba9e4d..376d459be 100644 --- a/helm/ocaml/cic_transformations/cexpr2pres.mli +++ b/helm/ocaml/cic_transformations/cexpr2pres.mli @@ -37,7 +37,7 @@ val symbol_table : Content_expressions.cexpr list -> priority:int -> assoc:bool -> - tail:Mpresentation.mpres list -> + tail:string list -> (string option * string * string) list -> (string option * string * string) list -> Mpresentation.mpres @@ -48,10 +48,10 @@ val symbol_table_charcount : Content_expressions.cexpr list -> priority:int -> assoc:bool -> - tail:Mpresentation.mpres list -> + tail:string list -> (string option * string * string) list -> (string option * string * string) list -> - Mpresentation.mpres + Mpresentation.mpres Box.box ) Hashtbl.t val maxsize : int @@ -59,12 +59,12 @@ val countterm : int -> Content_expressions.cexpr -> int val cexpr2pres : ?priority:int -> ?assoc:bool -> - ?tail:Mpresentation.mpres list -> + ?tail:string list -> Content_expressions.cexpr -> Mpresentation.mpres val cexpr2pres_charcount : ?priority:int -> ?assoc:bool -> - ?tail:Mpresentation.mpres list -> + ?tail:string list -> Content_expressions.cexpr -> - Mpresentation.mpres + Mpresentation.mpres Box.box diff --git a/helm/ocaml/cic_transformations/cexpr2pres_hashtbl.ml b/helm/ocaml/cic_transformations/cexpr2pres_hashtbl.ml index 79c9943c9..7cb3ba13c 100644 --- a/helm/ocaml/cic_transformations/cexpr2pres_hashtbl.ml +++ b/helm/ocaml/cic_transformations/cexpr2pres_hashtbl.ml @@ -47,32 +47,60 @@ let unary f = | _ -> assert false ;; +let m_open_fence = P.Mtext([], "(") +let b_open_fence = Box.b_text [] "(" +(* +let m_close_fence = P.Mtext([], ")") +let b_close_fence = Box.b_text [] ")" +*) + +let b_h_with_open_fence attrs a b op = + Box.b_h attrs [ b_open_fence; a; Box.b_object op; b ] +let b_h_without_open_fence attrs a b op = + Box.b_h attrs [ a; Box.b_object op; b ] +let b_v_with_open_fence attrs a b op = + Box.b_v attrs [ + Box.b_h [] [ b_open_fence; a]; + Box.b_indent (Box.b_h [] [ Box.b_object op; b ]) + ] +let b_v_without_open_fence attrs a b op = + Box.b_v attrs [ + a; + Box.b_indent (Box.b_h [] [ Box.b_object op; b ]) + ] + +let m_row_with_open_fence = P.row_with_brackets +let m_row_without_open_fence = P.row_without_brackets + +let m_close_fence = ")" +let b_close_fence = ")" + let init ~(cexpr2pres: ?priority:int -> ?assoc:bool -> - ?tail:Mpresentation.mpres list -> + ?tail:string list -> Content_expressions.cexpr -> Mpresentation.mpres) ~(cexpr2pres_charcount: ?priority:int -> ?assoc:bool -> - ?tail:Mpresentation.mpres list -> + ?tail:string list -> Content_expressions.cexpr -> - Mpresentation.mpres) + Mpresentation.mpres Box.box) = (* arrow *) Hashtbl.add C2P.symbol_table "arrow" (binary (fun a b ~priority ~assoc ~tail aattr sattr -> if (priority > 5) || (priority = 5 && assoc) then - P.row_with_brackets aattr + m_row_with_open_fence aattr (cexpr2pres ~priority:5 ~assoc:false ~tail:[] a) (cexpr2pres ~priority:5 ~assoc:true - ~tail:(P.Mtext([],")")::tail) b) + ~tail:((m_close_fence)::tail) b) (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2192)) else - P.row_without_brackets aattr + m_row_without_open_fence aattr (cexpr2pres ~priority:5 ~assoc:false ~tail:[] a) (cexpr2pres ~priority:5 ~assoc:true ~tail:tail b) (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2192)))); @@ -80,13 +108,13 @@ Hashtbl.add C2P.symbol_table "arrow" (binary Hashtbl.add C2P.symbol_table_charcount "arrow" (binary (fun a b ~priority ~assoc ~tail aattr sattr -> if (priority > 40) || (priority = 40 && assoc) then - P.two_rows_table_with_brackets aattr + b_v_with_open_fence aattr (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:[] a) (cexpr2pres_charcount ~priority:40 ~assoc:true - ~tail:(P.Mtext([],")")::tail) b) + ~tail:(b_close_fence::tail) b) (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2192)) else - P.two_rows_table_without_brackets aattr + b_v_without_open_fence aattr (cexpr2pres_charcount ~priority:5 ~assoc:false ~tail:[] a) (cexpr2pres_charcount ~priority:5 ~assoc:true ~tail:tail b) (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2192)))); @@ -95,13 +123,13 @@ Hashtbl.add C2P.symbol_table_charcount "arrow" (binary Hashtbl.add C2P.symbol_table "eq" (binary (fun a b ~priority ~assoc ~tail aattr sattr -> if (priority > 40) || (priority = 40 && assoc) then - P.row_with_brackets aattr + m_row_with_open_fence aattr (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a) (cexpr2pres ~priority:40 ~assoc:false - ~tail:(P.Mtext([],")")::tail) b) + ~tail:(m_close_fence::tail) b) (P.Mo(sattr,"=")) else - P.row_without_brackets aattr + m_row_without_open_fence aattr (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a) (cexpr2pres ~priority:40 ~assoc:false ~tail:tail b) (P.Mo(sattr,"=")))); @@ -109,13 +137,13 @@ Hashtbl.add C2P.symbol_table "eq" (binary Hashtbl.add C2P.symbol_table_charcount "eq" (binary (fun a b ~priority ~assoc ~tail aattr sattr -> if (priority > 40) || (priority = 40 && assoc) then - P.two_rows_table_with_brackets aattr + b_v_with_open_fence aattr (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a) (cexpr2pres_charcount ~priority:40 ~assoc:false - ~tail:(P.Mtext([],")")::tail) b) + ~tail:(b_close_fence::tail) b) (P.Mo(sattr,"=")) else - P.two_rows_table_without_brackets aattr + b_v_without_open_fence aattr (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a) (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:tail b) (P.Mo(sattr,"=")))); @@ -124,13 +152,13 @@ Hashtbl.add C2P.symbol_table_charcount "eq" (binary Hashtbl.add C2P.symbol_table "and" (binary (fun a b ~priority ~assoc ~tail aattr sattr -> if (priority > 20) || (priority = 20 && assoc) then - P.row_with_brackets aattr + m_row_with_open_fence aattr (cexpr2pres ~priority:20 ~assoc:true ~tail:[] a) (cexpr2pres ~priority:20 ~assoc:false - ~tail:(P.Mtext([],")")::tail) b) + ~tail:(m_close_fence::tail) b) (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2227)) else - P.row_without_brackets aattr + m_row_without_open_fence aattr (cexpr2pres ~priority:20 ~assoc:true ~tail:[] a) (cexpr2pres ~priority:20 ~assoc:false ~tail:tail b) (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2227)))); @@ -138,13 +166,13 @@ Hashtbl.add C2P.symbol_table "and" (binary Hashtbl.add C2P.symbol_table_charcount "and" (binary (fun a b ~priority ~assoc ~tail aattr sattr -> if (priority > 20) || (priority = 20 && assoc) then - P.two_rows_table_with_brackets aattr + b_v_with_open_fence aattr (cexpr2pres_charcount ~priority:20 ~assoc:true ~tail:[] a) (cexpr2pres_charcount ~priority:20 ~assoc:false - ~tail:(P.Mtext([],")")::tail) b) + ~tail:(b_close_fence::tail) b) (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2227)) else - P.two_rows_table_without_brackets aattr + b_v_without_open_fence aattr (cexpr2pres_charcount ~priority:20 ~assoc:true ~tail:[] a) (cexpr2pres_charcount ~priority:20 ~assoc:false ~tail:tail b) (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2227)))); @@ -153,13 +181,13 @@ Hashtbl.add C2P.symbol_table_charcount "and" (binary Hashtbl.add C2P.symbol_table "or" (binary (fun a b ~priority ~assoc ~tail aattr sattr -> if (priority > 10) || (priority = 10 && assoc) then - P.row_with_brackets aattr + m_row_with_open_fence aattr (cexpr2pres ~priority:10 ~assoc:true ~tail:[] a) (cexpr2pres ~priority:10 ~assoc:false - ~tail:(P.Mtext([],")")::tail) b) + ~tail:(m_close_fence::tail) b) (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2228)) else - P.row_without_brackets aattr + m_row_without_open_fence aattr (cexpr2pres ~priority:10 ~assoc:true ~tail:[] a) (cexpr2pres ~priority:10 ~assoc:false ~tail:tail b) (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2228)))); @@ -167,13 +195,13 @@ Hashtbl.add C2P.symbol_table "or" (binary Hashtbl.add C2P.symbol_table_charcount "or" (binary (fun a b ~priority ~assoc ~tail aattr sattr -> if (priority > 10) || (priority = 10 && assoc) then - P.two_rows_table_with_brackets aattr + b_v_with_open_fence aattr (cexpr2pres_charcount ~priority:10 ~assoc:true ~tail:[] a) (cexpr2pres_charcount ~priority:10 ~assoc:false - ~tail:(P.Mtext([],")")::tail) b) + ~tail:(b_close_fence::tail) b) (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2228)) else - P.two_rows_table_without_brackets aattr + b_v_without_open_fence aattr (cexpr2pres_charcount ~priority:10 ~assoc:true ~tail:[] a) (cexpr2pres_charcount ~priority:10 ~assoc:false ~tail:tail b) (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2228)))); @@ -182,13 +210,13 @@ Hashtbl.add C2P.symbol_table_charcount "or" (binary Hashtbl.add C2P.symbol_table "iff" (binary (fun a b ~priority ~assoc ~tail aattr sattr -> if (priority > 5) || (priority = 5 && assoc) then - P.row_with_brackets aattr + m_row_with_open_fence aattr (cexpr2pres ~priority:5 ~assoc:true ~tail:[] a) (cexpr2pres ~priority:5 ~assoc:false - ~tail:(P.Mtext([],")")::tail) b) + ~tail:(m_close_fence::tail) b) (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x21D4)) else - P.row_without_brackets aattr + m_row_without_open_fence aattr (cexpr2pres ~priority:5 ~assoc:true ~tail:[] a) (cexpr2pres ~priority:5 ~assoc:false ~tail:tail b) (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x21D4)))); @@ -196,13 +224,13 @@ Hashtbl.add C2P.symbol_table "iff" (binary Hashtbl.add C2P.symbol_table_charcount "iff" (binary (fun a b ~priority ~assoc ~tail aattr sattr -> if (priority > 5) || (priority = 5 && assoc) then - P.two_rows_table_with_brackets aattr + b_v_with_open_fence aattr (cexpr2pres_charcount ~priority:5 ~assoc:true ~tail:[] a) (cexpr2pres_charcount ~priority:5 ~assoc:false - ~tail:(P.Mtext([],")")::tail) b) + ~tail:(b_close_fence::tail) b) (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x21D4)) else - P.two_rows_table_without_brackets aattr + b_v_without_open_fence aattr (cexpr2pres_charcount ~priority:5 ~assoc:true ~tail:[] a) (cexpr2pres_charcount ~priority:5 ~assoc:false ~tail:tail b) (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x21D4)))); @@ -210,18 +238,18 @@ Hashtbl.add C2P.symbol_table_charcount "iff" (binary (* not *) Hashtbl.add C2P.symbol_table "not" (unary (fun a ~priority ~assoc ~tail attr sattr -> - P.Mrow([],[ - P.Mtext([],"(");P.Mo([],Netconversion.ustring_of_uchar `Enc_utf8 0xAC); - cexpr2pres a;P.Mtext([],")")]))); + (P.Mrow([], [ + m_open_fence; P.Mo([],Netconversion.ustring_of_uchar `Enc_utf8 0xAC); + cexpr2pres a; P.Mtext ([], m_close_fence)])))) ; (* inv *) Hashtbl.add C2P.symbol_table "inv" (unary (fun a ~priority ~assoc ~tail attr sattr -> P.Msup([], P.Mrow([],[ - P.Mtext([],"("); + m_open_fence; cexpr2pres a; - P.Mtext([],")")]), + P.Mtext ([], m_close_fence)]), P.Mrow([],[ P.Mo([],"-"); P.Mn([],"1")])))); @@ -231,21 +259,21 @@ Hashtbl.add C2P.symbol_table "opp" (unary (fun a ~priority ~assoc ~tail attr sattr -> P.Mrow([],[ P.Mo([],"-"); - P.Mtext([],"("); + m_open_fence; cexpr2pres a; - P.Mtext([],")")]))); + P.Mtext ([], m_close_fence)]))); (* leq *) Hashtbl.add C2P.symbol_table "leq" (binary (fun a b ~priority ~assoc ~tail aattr sattr -> if (priority > 40) || (priority = 40 && assoc) then - P.row_with_brackets aattr + m_row_with_open_fence aattr (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a) (cexpr2pres ~priority:40 ~assoc:false - ~tail:(P.Mtext([],")")::tail) b) + ~tail:(m_close_fence::tail) b) (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2264)) else - P.row_without_brackets aattr + m_row_without_open_fence aattr (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a) (cexpr2pres ~priority:40 ~assoc:false ~tail:tail b) (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2264)))); @@ -253,13 +281,13 @@ Hashtbl.add C2P.symbol_table "leq" (binary Hashtbl.add C2P.symbol_table_charcount "leq" (binary (fun a b ~priority ~assoc ~tail aattr sattr -> if (priority > 40) || (priority = 40 && assoc) then - P.two_rows_table_with_brackets aattr + b_v_with_open_fence aattr (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a) (cexpr2pres_charcount ~priority:40 ~assoc:false - ~tail:(P.Mtext([],")")::tail) b) + ~tail:(b_close_fence::tail) b) (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2264)) else - P.two_rows_table_without_brackets aattr + b_v_without_open_fence aattr (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a) (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:tail b) (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2264)))); @@ -268,13 +296,13 @@ Hashtbl.add C2P.symbol_table_charcount "leq" (binary Hashtbl.add C2P.symbol_table "lt" (binary (fun a b ~priority ~assoc ~tail aattr sattr -> if (priority > 40) || (priority = 40 && assoc) then - P.row_with_brackets aattr + m_row_with_open_fence aattr (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a) (cexpr2pres ~priority:40 ~assoc:false - ~tail:(P.Mtext([],")")::tail) b) + ~tail:(m_close_fence::tail) b) (P.Mo(sattr,"<")) else - P.row_without_brackets aattr + m_row_without_open_fence aattr (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a) (cexpr2pres ~priority:40 ~assoc:false ~tail:tail b) (P.Mo(sattr,"<")))); @@ -282,13 +310,13 @@ Hashtbl.add C2P.symbol_table "lt" (binary Hashtbl.add C2P.symbol_table_charcount "lt" (binary (fun a b ~priority ~assoc ~tail aattr sattr -> if (priority > 40) || (priority = 40 && assoc) then - P.two_rows_table_with_brackets aattr + b_v_with_open_fence aattr (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a) (cexpr2pres_charcount ~priority:40 ~assoc:false - ~tail:(P.Mtext([],")")::tail) b) + ~tail:(b_close_fence::tail) b) (P.Mo(sattr,"<")) else - P.two_rows_table_without_brackets aattr + b_v_without_open_fence aattr (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a) (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:tail b) (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2265)))); @@ -297,13 +325,13 @@ Hashtbl.add C2P.symbol_table_charcount "lt" (binary Hashtbl.add C2P.symbol_table "geq" (binary (fun a b ~priority ~assoc ~tail aattr sattr -> if (priority > 40) || (priority = 40 && assoc) then - P.row_with_brackets aattr + m_row_with_open_fence aattr (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a) (cexpr2pres ~priority:40 ~assoc:false - ~tail:(P.Mtext([],")")::tail) b) + ~tail:(m_close_fence::tail) b) (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2265)) else - P.row_without_brackets aattr + m_row_without_open_fence aattr (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a) (cexpr2pres ~priority:40 ~assoc:false ~tail:tail b) (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2265)))); @@ -311,13 +339,13 @@ Hashtbl.add C2P.symbol_table "geq" (binary Hashtbl.add C2P.symbol_table_charcount "geq" (binary (fun a b ~priority ~assoc ~tail aattr sattr -> if (priority > 40) || (priority = 40 && assoc) then - P.two_rows_table_with_brackets aattr + b_v_with_open_fence aattr (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a) (cexpr2pres_charcount ~priority:40 ~assoc:false - ~tail:(P.Mtext([],")")::tail) b) + ~tail:(b_close_fence::tail) b) (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2265)) else - P.two_rows_table_without_brackets aattr + b_v_without_open_fence aattr (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a) (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:tail b) (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2265)))); @@ -326,13 +354,13 @@ Hashtbl.add C2P.symbol_table_charcount "geq" (binary Hashtbl.add C2P.symbol_table "gt" (binary (fun a b ~priority ~assoc ~tail aattr sattr -> if (priority > 40) || (priority = 40 && assoc) then - P.row_with_brackets aattr + m_row_with_open_fence aattr (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a) (cexpr2pres ~priority:40 ~assoc:false - ~tail:(P.Mtext([],")")::tail) b) + ~tail:(m_close_fence::tail) b) (P.Mo(sattr,">")) else - P.row_without_brackets aattr + m_row_without_open_fence aattr (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a) (cexpr2pres ~priority:40 ~assoc:false ~tail:tail b) (P.Mo(sattr,">")))); @@ -340,13 +368,13 @@ Hashtbl.add C2P.symbol_table "gt" (binary Hashtbl.add C2P.symbol_table_charcount "gt" (binary (fun a b ~priority ~assoc ~tail aattr sattr -> if (priority > 40) || (priority = 40 && assoc) then - P.two_rows_table_with_brackets aattr + b_v_with_open_fence aattr (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a) (cexpr2pres_charcount ~priority:40 ~assoc:false - ~tail:(P.Mtext([],")")::tail) b) + ~tail:(b_close_fence::tail) b) (P.Mo(sattr,">")) else - P.two_rows_table_without_brackets aattr + b_v_without_open_fence aattr (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a) (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:tail b) (P.Mo(sattr,">")))); @@ -355,13 +383,13 @@ Hashtbl.add C2P.symbol_table_charcount "gt" (binary Hashtbl.add C2P.symbol_table "plus" (binary (fun a b ~priority ~assoc ~tail aattr sattr -> if (priority > 60) || (priority = 60 && assoc) then - P.row_with_brackets aattr + m_row_with_open_fence aattr (cexpr2pres ~priority:60 ~assoc:true ~tail:[] a) (cexpr2pres ~priority:60 ~assoc:false - ~tail:(P.Mtext([],")")::tail) b) + ~tail:(m_close_fence::tail) b) (P.Mo(sattr,"+")) else - P.row_without_brackets aattr + m_row_without_open_fence aattr (cexpr2pres ~priority:60 ~assoc:true ~tail:[] a) (cexpr2pres ~priority:60 ~assoc:false ~tail:tail b) (P.Mo(sattr,"+")))); @@ -369,13 +397,13 @@ Hashtbl.add C2P.symbol_table "plus" (binary Hashtbl.add C2P.symbol_table_charcount "plus" (binary (fun a b ~priority ~assoc ~tail aattr sattr -> if (priority > 60) || (priority = 60 && assoc) then - P.two_rows_table_with_brackets aattr + b_v_with_open_fence aattr (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a) (cexpr2pres_charcount ~priority:60 ~assoc:false - ~tail:(P.Mtext([],")")::tail) b) + ~tail:(b_close_fence::tail) b) (P.Mo(sattr,"+")) else - P.two_rows_table_without_brackets aattr + b_v_without_open_fence aattr (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a) (cexpr2pres_charcount ~priority:60 ~assoc:false ~tail:tail b) (P.Mo(sattr,"+")))); @@ -384,13 +412,13 @@ Hashtbl.add C2P.symbol_table_charcount "plus" (binary Hashtbl.add C2P.symbol_table "times" (binary (fun a b ~priority ~assoc ~tail aattr sattr -> if (priority > 70) || (priority = 70 && assoc) then - P.row_with_brackets aattr + m_row_with_open_fence aattr (cexpr2pres ~priority:70 ~assoc:true ~tail:[] a) (cexpr2pres ~priority:70 ~assoc:false - ~tail:(P.Mtext([],")")::tail) b) + ~tail:(m_close_fence::tail) b) (P.Mo(sattr,"*")) else - P.row_without_brackets aattr + m_row_without_open_fence aattr (cexpr2pres ~priority:70 ~assoc:true ~tail:[] a) (cexpr2pres ~priority:70 ~assoc:false ~tail:tail b) (P.Mo(sattr,"*")))); @@ -398,13 +426,13 @@ Hashtbl.add C2P.symbol_table "times" (binary Hashtbl.add C2P.symbol_table_charcount "times" (binary (fun a b ~priority ~assoc ~tail aattr sattr -> if (priority > 70) || (priority = 70 && assoc) then - P.two_rows_table_with_brackets aattr + b_v_with_open_fence aattr (cexpr2pres_charcount ~priority:70 ~assoc:true ~tail:[] a) (cexpr2pres_charcount ~priority:70 ~assoc:false - ~tail:(P.Mtext([],")")::tail) b) + ~tail:(b_close_fence::tail) b) (P.Mo(sattr,"*")) else - P.two_rows_table_without_brackets aattr + b_v_without_open_fence aattr (cexpr2pres_charcount ~priority:70 ~assoc:true ~tail:[] a) (cexpr2pres_charcount ~priority:70 ~assoc:false ~tail:tail b) (P.Mo(sattr,"*")))); @@ -413,13 +441,13 @@ Hashtbl.add C2P.symbol_table_charcount "times" (binary Hashtbl.add C2P.symbol_table "minus" (binary (fun a b ~priority ~assoc ~tail aattr sattr -> if (priority > 60) || (priority = 60 && assoc) then - P.row_with_brackets aattr + m_row_with_open_fence aattr (cexpr2pres ~priority:60 ~assoc:true ~tail:[] a) (cexpr2pres ~priority:60 ~assoc:false - ~tail:(P.Mtext([],")")::tail) b) + ~tail:(m_close_fence::tail) b) (P.Mo(sattr,"-")) else - P.row_without_brackets aattr + m_row_without_open_fence aattr (cexpr2pres ~priority:60 ~assoc:true ~tail:[] a) (cexpr2pres ~priority:60 ~assoc:false ~tail:tail b) (P.Mo(sattr,"-")))); @@ -427,13 +455,13 @@ Hashtbl.add C2P.symbol_table "minus" (binary Hashtbl.add C2P.symbol_table_charcount "minus" (binary (fun a b ~priority ~assoc ~tail aattr sattr -> if (priority > 60) || (priority = 60 && assoc) then - P.two_rows_table_with_brackets aattr + b_v_with_open_fence aattr (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a) (cexpr2pres_charcount ~priority:60 ~assoc:false - ~tail:(P.Mtext([],")")::tail) b) + ~tail:(b_close_fence::tail) b) (P.Mo(sattr,"-")) else - P.two_rows_table_without_brackets aattr + b_v_without_open_fence aattr (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a) (cexpr2pres_charcount ~priority:60 ~assoc:false ~tail:tail b) (P.Mo(sattr,"-")))); @@ -442,13 +470,13 @@ Hashtbl.add C2P.symbol_table_charcount "minus" (binary Hashtbl.add C2P.symbol_table "div" (binary (fun a b ~priority ~assoc ~tail aattr sattr -> if (priority > 60) || (priority = 60 && assoc) then - P.row_with_brackets aattr + m_row_with_open_fence aattr (cexpr2pres ~priority:60 ~assoc:true ~tail:[] a) (cexpr2pres ~priority:60 ~assoc:false - ~tail:(P.Mtext([],")")::tail) b) + ~tail:(m_close_fence::tail) b) (P.Mo(sattr,"/")) else - P.row_without_brackets aattr + m_row_without_open_fence aattr (cexpr2pres ~priority:60 ~assoc:true ~tail:[] a) (cexpr2pres ~priority:60 ~assoc:false ~tail:tail b) (P.Mo(sattr,"/")))); @@ -456,13 +484,13 @@ Hashtbl.add C2P.symbol_table "div" (binary Hashtbl.add C2P.symbol_table_charcount "div" (binary (fun a b ~priority ~assoc ~tail aattr sattr -> if (priority > 60) || (priority = 60 && assoc) then - P.two_rows_table_with_brackets aattr + b_v_with_open_fence aattr (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a) (cexpr2pres_charcount ~priority:60 ~assoc:false - ~tail:(P.Mtext([],")")::tail) b) + ~tail:(b_close_fence::tail) b) (P.Mo(sattr,"/")) else - P.two_rows_table_without_brackets aattr + b_v_without_open_fence aattr (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a) (cexpr2pres_charcount ~priority:60 ~assoc:false ~tail:tail b) (P.Mo(sattr,"/")))) diff --git a/helm/ocaml/cic_transformations/cexpr2pres_hashtbl.mli b/helm/ocaml/cic_transformations/cexpr2pres_hashtbl.mli index e6202582e..61c351963 100644 --- a/helm/ocaml/cic_transformations/cexpr2pres_hashtbl.mli +++ b/helm/ocaml/cic_transformations/cexpr2pres_hashtbl.mli @@ -36,14 +36,14 @@ val init: cexpr2pres: (?priority:int -> ?assoc:bool -> - ?tail:Mpresentation.mpres list -> + ?tail:string list -> Content_expressions.cexpr -> Mpresentation.mpres) -> cexpr2pres_charcount: (?priority:int -> ?assoc:bool -> - ?tail:Mpresentation.mpres list -> + ?tail:string list -> Content_expressions.cexpr -> - Mpresentation.mpres) -> + Mpresentation.mpres Box.box) -> unit ;; diff --git a/helm/ocaml/cic_transformations/cicAstPp.ml b/helm/ocaml/cic_transformations/cicAstPp.ml index 2cc83e743..dda70793f 100644 --- a/helm/ocaml/cic_transformations/cicAstPp.ml +++ b/helm/ocaml/cic_transformations/cicAstPp.ml @@ -82,7 +82,7 @@ and pp_subst (name, term) = sprintf "%s \\Assign %s" name (pp_term term) and pp_substs substs = String.concat "; " (List.map pp_subst substs) and pp_pattern ((head, vars), term) = - sprintf "%s \Rightarrow %s" + sprintf "%s \\Rightarrow %s" (match vars with | [] -> head | _ -> diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml index c0cdc5c0f..a2a010f7d 100644 --- a/helm/ocaml/cic_transformations/content2pres.ml +++ b/helm/ocaml/cic_transformations/content2pres.ml @@ -32,6 +32,9 @@ (* *) (***************************************************************************) +module P = Mpresentation +module B = Box + let p_mtr a b = Mpresentation.Mtr(a,b) let p_mtd a b = Mpresentation.Mtd(a,b) let p_mtable a b = Mpresentation.Mtable(a,b) @@ -41,7 +44,6 @@ let p_mo a b = Mpresentation.Mo(a,b) let p_mrow a b = Mpresentation.Mrow(a,b) let p_mphantom a b = Mpresentation.Mphantom(a,b) - let rec split n l = if n = 0 then [],l else let l1,l2 = @@ -138,35 +140,23 @@ let get_xref = ;; let make_row ?(attrs=[]) items concl = - let module P = Mpresentation in - (match concl with - P.Mtable _ -> (* big! *) - P.Mtable (attrs@[None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"], - [P.Mtr([],[P.Mtd ([],P.Mrow([],items))]); - P.Mtr ([],[P.Mtd ([],P.indented concl)])]) - | _ -> (* small *) - P.Mrow(attrs,items@[P.Mspace([None,"width","0.1cm"]);concl])) + match concl with + B.V _ -> (* big! *) + B.b_v attrs [B.b_h [] items; B.b_indent concl] + | _ -> (* small *) + B.b_h attrs (items@[B.b_space; concl]) ;; let make_concl ?(attrs=[]) verb concl = - let module P = Mpresentation in - (match concl with - P.Mtable _ -> (* big! *) - P.Mtable (attrs@[None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"], - [P.Mtr([],[P.Mtd ([],P.Mtext([None,"mathcolor","Red"],verb))]); - P.Mtr ([],[P.Mtd ([],P.indented concl)])]) - | _ -> (* small *) - P.Mrow(attrs, - [P.Mtext([None,"mathcolor","Red"],verb); - P.Mspace([None,"width","0.1cm"]); - concl])) + match concl with + B.V _ -> (* big! *) + B.b_v attrs [ B.b_kw verb; B.b_indent concl] + | _ -> (* small *) + B.b_h attrs [ B.b_kw verb; B.b_space; concl ] ;; let make_args_for_apply term2pres args = let module Con = Content in - let module P = Mpresentation in let make_arg_for_apply is_first arg row = let res = match arg with @@ -176,18 +166,18 @@ let make_args_for_apply term2pres args = (match prem.Con.premise_binder with None -> "previous" | Some s -> s) in - P.Mi([],name)::row + (B.b_object (P.Mi ([], name)))::row | Con.Lemma lemma -> - P.Mi([],lemma.Con.lemma_name)::row + (B.b_object (P.Mi([],lemma.Con.lemma_name)))::row | Con.Term t -> if is_first then (term2pres t)::row - else P.Mi([],"_")::row + else (B.b_object (P.Mi([],"_")))::row | Con.ArgProof _ | Con.ArgMethod _ -> - P.Mi([],"_")::row + (B.b_object (P.Mi([],"_")))::row in - if is_first then res else P.smallskip::res + if is_first then res else B.skip::res in match args with hd::tl -> @@ -205,15 +195,14 @@ let rec justification term2pres p = (p.Con.proof_conclude.Con.conclude_method = "Apply"))) then let pres_args = make_args_for_apply term2pres p.Con.proof_conclude.Con.conclude_args in - P.Mrow([], - P.Mtext([None,"mathcolor","Red"],"by")::P.Mspace([None,"width","0.1cm"]):: - P.Mo([],"(")::pres_args@[P.Mo([],")")]) + B.H([], + (B.b_kw "by")::B.b_space:: + B.Text([],"(")::pres_args@[B.Text([],")")]) else proof2pres term2pres p and proof2pres term2pres p = let rec proof2pres p = let module Con = Content in - let module P = Mpresentation in let indent = let is_decl e = (match e with @@ -238,33 +227,21 @@ and proof2pres term2pres p = let action = match concl with None -> body -(* - P.Maction - ([None,"actiontype","toggle" ; None,"selection","1"], - [P.Mtext [] "proof" ; body]) -*) | Some ac -> - P.Maction - ([None,"actiontype","toggle" ; None,"selection","1"], + B.Action + ([None,"type","toggle"], [(make_concl ~attrs:[Some "helm", "xref", p.Con.proof_id] "proof of" ac); body]) in - P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"], - [P.Mtr ([],[P.Mtd ([],P.Mfenced([],[P.Mtext ([],name)]))]); - P.Mtr ([],[P.Mtd ([], P.indented action)])]) -(* - P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left";Some "helm", "xref", p.Con.proof_id], - [P.Mtr ([],[P.Mtd ([],P.Mfenced([],[P.Mtext ([],name)]))]); - P.Mtr ([],[P.Mtd ([], P.indented action)])]) *) + B.V ([], + [B.Text ([],"(" ^ name ^ ")"); + B.indent action]) and context2pres c continuation = (* we generate a subtable for each context element, for selection purposes The table generated by the head-element does not have an xref; the whole context-proof is already selectable *) - let module P = Mpresentation in match c with [] -> continuation | hd::tl -> @@ -272,30 +249,27 @@ and proof2pres term2pres p = List.fold_right (fun ce continuation -> let xref = get_xref ce in - P.Mtable([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"; Some "helm", "xref", xref ], - [P.Mtr([Some "helm", "xref", "ce_"^xref],[P.Mtd ([],ce2pres ce)]); - P.Mtr([],[P.Mtd ([], continuation)])])) tl continuation in + B.V([Some "helm", "xref", xref ], + [B.H([Some "helm", "xref", "ce_"^xref],[ce2pres ce]); + continuation])) tl continuation in let hd_xref= get_xref hd in - P.Mtable([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"], - [P.Mtr([Some "helm", "xref", "ce_"^hd_xref], - [P.Mtd ([],ce2pres hd)]); - P.Mtr([],[P.Mtd ([], continuation')])]) + B.V([], + [B.H([Some "helm", "xref", "ce_"^hd_xref], + [ce2pres hd]); + continuation']) and ce2pres = - let module P = Mpresentation in let module Con = Content in function `Declaration d -> (match d.Con.dec_name with Some s -> let ty = term2pres d.Con.dec_type in - P.Mrow ([], - [P.Mtext([None,"mathcolor","Red"],"Assume"); - P.Mspace([None,"width","0.1cm"]); - P.Mi([],s); - P.Mtext([],":"); + B.H ([], + [(B.b_kw "Assume"); + B.b_space; + B.Object ([], P.Mi([],s)); + B.Text([],":"); ty]) | None -> prerr_endline "NO NAME!!"; assert false) @@ -303,13 +277,13 @@ and proof2pres term2pres p = (match h.Con.dec_name with Some s -> let ty = term2pres h.Con.dec_type in - P.Mrow ([], - [P.Mtext([None,"mathcolor","Red"],"Suppose"); - P.Mspace([None,"width","0.1cm"]); - P.Mo([],"("); - P.Mi ([],s); - P.Mo([],")"); - P.Mspace([None,"width","0.1cm"]); + B.H ([], + [(B.b_kw "Suppose"); + B.b_space; + B.Text([],"("); + B.Object ([], P.Mi ([],s)); + B.Text([],")"); + B.b_space; ty]) | None -> prerr_endline "NO NAME!!"; assert false) @@ -319,30 +293,28 @@ and proof2pres term2pres p = (match d.Con.def_name with Some s -> let term = term2pres d.Con.def_term in - P.Mrow ([], - [P.Mtext([],"Let "); - P.Mi([],s); - P.Mtext([]," = "); + B.H ([], + [B.Text([],"Let "); + B.Object ([], P.Mi([],s)); + B.Text([]," = "); term]) | None -> prerr_endline "NO NAME!!"; assert false) | `Joint ho -> - P.Mtext ([],"jointdef") + B.Text ([],"jointdef") and acontext2pres ac continuation indent = let module Con = Content in - let module P = Mpresentation in List.fold_right (fun p continuation -> let hd = if indent then - P.indented (proof2pres p) + B.indent (proof2pres p) else proof2pres p in - P.Mtable([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"; Some "helm","xref",p.Con.proof_id], - [P.Mtr([Some "helm","xref","ace_"^p.Con.proof_id],[P.Mtd ([],hd)]); - P.Mtr([],[P.Mtd ([], continuation)])])) ac continuation + B.V([Some "helm","xref",p.Con.proof_id], + [B.H([Some "helm","xref","ace_"^p.Con.proof_id],[hd]); + continuation])) ac continuation and conclude2pres conclude indent omit_conclusion = let module Con = Content in @@ -368,16 +340,13 @@ and proof2pres term2pres p = if conclude.Con.conclude_method = "TD_Conversion" then make_concl "that is equivalent to" concl else make_concl "we conclude" concl in - P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"], - [P.Mtr ([],[P.Mtd ([],conclude_body)]); - P.Mtr ([],[P.Mtd ([],ann_concl)])]) + B.V ([], [conclude_body; ann_concl]) | _ -> conclude_aux conclude in if indent then - P.indented (P.Mrow ([Some "helm", "xref", conclude.Con.conclude_id], + B.indent (B.H ([Some "helm", "xref", conclude.Con.conclude_id], [tconclude_body])) else - P.Mrow ([Some "helm", "xref", conclude.Con.conclude_id],[tconclude_body]) + B.H ([Some "helm", "xref", conclude.Con.conclude_id],[tconclude_body]) and conclude_aux conclude = @@ -386,7 +355,7 @@ and proof2pres term2pres p = if conclude.Con.conclude_method = "TD_Conversion" then let expected = (match conclude.Con.conclude_conclusion with - None -> P.Mtext([],"NO EXPECTED!!!") + None -> B.Text([],"NO EXPECTED!!!") | Some c -> term2pres c) in let subproof = (match conclude.Con.conclude_args with @@ -394,13 +363,13 @@ and proof2pres term2pres p = | _ -> assert false) in let synth = (match subproof.Con.proof_conclude.Con.conclude_conclusion with - None -> P.Mtext([],"NO SYNTH!!!") + None -> B.Text([],"NO SYNTH!!!") | Some c -> (term2pres c)) in - P.Mtable - ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"], - [P.Mtr([],[P.Mtd([],make_concl "we must prove" expected)]); - P.Mtr([],[P.Mtd([],make_concl "or equivalently" synth)]); - P.Mtr([],[P.Mtd([],proof2pres subproof)])]) + B.V + ([], + [make_concl "we must prove" expected; + make_concl "or equivalently" synth; + proof2pres subproof]) else if conclude.Con.conclude_method = "BU_Conversion" then assert false else if conclude.Con.conclude_method = "Exact" then @@ -410,11 +379,10 @@ and proof2pres term2pres p = | _ -> assert false) in (match conclude.Con.conclude_conclusion with None -> - p_mrow [] - [p_mtext [None, "mathcolor", "red"] "Consider" ; P.smallskip; arg] + B.b_h [] [B.b_kw "Consider"; B.b_space; arg] | Some c -> let conclusion = term2pres c in make_row - [arg; P.Mspace([None,"width","0.1cm"]);P.Mtext([],"proves")] + [arg; B.b_space; B.Text([],"proves")] conclusion ) else if conclude.Con.conclude_method = "Intros+LetTac" then @@ -424,15 +392,15 @@ and proof2pres term2pres p = (* OLD CODE let conclusion = (match conclude.Con.conclude_conclusion with - None -> P.Mtext([],"NO Conclusion!!!") + None -> B.Text([],"NO Conclusion!!!") | Some c -> term2pres c) in (match conclude.Con.conclude_args with [Con.ArgProof p] -> - P.Mtable + B.V ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"], - [P.Mtr([],[P.Mtd([],proof2pres p)]); - P.Mtr([],[P.Mtd([], + [B.H([],[B.Object([],proof2pres p)]); + B.H([],[B.Object([], (make_concl "we proved 1" conclusion))])]); | _ -> assert false) *) @@ -459,62 +427,52 @@ and proof2pres term2pres p = (match List.nth conclude.Con.conclude_args 5 with Con.Term t -> term2pres t | _ -> assert false) in - P.Mtable ([None,"align","baseline 1";None,"equalrows","false"; - None,"columnalign","left"], - [P.Mtr ([],[P.Mtd ([],P.Mrow([],[ - P.Mtext([None,"mathcolor","Red"],"rewrite"); - P.Mspace([None,"width","0.1cm"]);term1; - P.Mspace([None,"width","0.1cm"]); - P.Mtext([None,"mathcolor","Red"],"with"); - P.Mspace([None,"width","0.1cm"]);term2]))]); - P.Mtr ([],[P.Mtd ([],P.indented justif)])]); + B.V ([], + [B.H ([],[ + (B.b_kw "rewrite"); + B.b_space; term1; + B.b_space; (B.b_kw "with"); + B.b_space; term2; + B.indent justif])]) else if conclude.Con.conclude_method = "Apply" then let pres_args = make_args_for_apply term2pres conclude.Con.conclude_args in - P.Mrow([], - P.Mtext([None,"mathcolor","Red"],"by"):: - P.Mspace([None,"width","0.1cm"]):: - P.Mo([],"(")::pres_args@[P.Mo([],")")]) + B.H([], + (B.b_kw "by"):: + B.b_space:: + B.Text([],"(")::pres_args@[B.Text([],")")]) else - P.Mtable - ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"], - [P.Mtr ([],[P.Mtd ([],P.Mtext([],"Apply method" ^ conclude.Con.conclude_method ^ " to"))]); - P.Mtr ([], - [P.Mtd ([], - (P.indented - (P.Mtable - ([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"], - args2pres conclude.Con.conclude_args))))])]) + B.V + ([], + [B.Text([],"Apply method" ^ conclude.Con.conclude_method ^ " to"); + (B.indent + (B.V + ([], + args2pres conclude.Con.conclude_args)))]) - and args2pres l = - let module P = Mpresentation in - List.map - (function a -> P.Mtr ([], [P.Mtd ([], arg2pres a)])) l + and args2pres l = List.map arg2pres l and arg2pres = - let module P = Mpresentation in let module Con = Content in function Con.Aux n -> - P.Mtext ([],"aux " ^ n) + B.Text ([],"aux " ^ n) | Con.Premise prem -> - P.Mtext ([],"premise") + B.Text ([],"premise") | Con.Lemma lemma -> - P.Mtext ([],"lemma") + B.Text ([],"lemma") | Con.Term t -> term2pres t | Con.ArgProof p -> proof2pres p | Con.ArgMethod s -> - P.Mtext ([],"method") + B.Text ([],"method") and case conclude = - let module P = Mpresentation in let module Con = Content in let proof_conclusion = (match conclude.Con.conclude_conclusion with - None -> P.Mtext([],"No conclusion???") + None -> B.Text([],"No conclusion???") | Some t -> term2pres t) in let arg,args_for_cases = (match conclude.Con.conclude_args with @@ -525,34 +483,30 @@ and proof2pres term2pres p = let case_arg = (match arg with Con.Aux n -> - P.Mtext ([],"an aux???") + B.Text ([],"an aux???") | Con.Premise prem -> (match prem.Con.premise_binder with - None -> P.Mtext ([],"the previous result") - | Some n -> P.Mi([],n)) - | Con.Lemma lemma -> P.Mi([],lemma.Con.lemma_name) + None -> B.Text ([],"the previous result") + | Some n -> B.Object ([], P.Mi([],n))) + | Con.Lemma lemma -> B.Object ([], P.Mi([],lemma.Con.lemma_name)) | Con.Term t -> term2pres t | Con.ArgProof p -> - P.Mtext ([],"a proof???") + B.Text ([],"a proof???") | Con.ArgMethod s -> - P.Mtext ([],"a method???")) in + B.Text ([],"a method???")) in (make_concl "we proceede by cases on" case_arg) in let to_prove = (make_concl "to prove" proof_conclusion) in - P.Mtable - ([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"], - P.Mtr ([],[P.Mtd ([],case_on)]):: - P.Mtr ([],[P.Mtd ([],to_prove)]):: - (make_cases args_for_cases)) + B.V + ([], + case_on::to_prove::(make_cases args_for_cases)) and byinduction conclude = - let module P = Mpresentation in let module Con = Content in let proof_conclusion = (match conclude.Con.conclude_conclusion with - None -> P.Mtext([],"No conclusion???") + None -> B.Text([],"No conclusion???") | Some t -> term2pres t) in let inductive_arg,args_for_cases = (match conclude.Con.conclude_args with @@ -565,42 +519,36 @@ and proof2pres term2pres p = let arg = (match inductive_arg with Con.Aux n -> - P.Mtext ([],"an aux???") + B.Text ([],"an aux???") | Con.Premise prem -> (match prem.Con.premise_binder with - None -> P.Mtext ([],"the previous result") - | Some n -> P.Mi([],n)) - | Con.Lemma lemma -> P.Mi([],lemma.Con.lemma_name) + None -> B.Text ([],"the previous result") + | Some n -> B.Object ([], P.Mi([],n))) + | Con.Lemma lemma -> B.Object ([], P.Mi([],lemma.Con.lemma_name)) | Con.Term t -> term2pres t | Con.ArgProof p -> - P.Mtext ([],"a proof???") + B.Text ([],"a proof???") | Con.ArgMethod s -> - P.Mtext ([],"a method???")) in + B.Text ([],"a method???")) in (make_concl "we proceede by induction on" arg) in let to_prove = (make_concl "to prove" proof_conclusion) in - P.Mtable - ([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"], - P.Mtr ([],[P.Mtd ([],induction_on)]):: - P.Mtr ([],[P.Mtd ([],to_prove)]):: + B.V + ([], + induction_on::to_prove:: (make_cases args_for_cases)) - and make_cases args_for_cases = - let module P = Mpresentation in - List.map - (fun p -> P.Mtr ([],[P.Mtd ([],make_case p)])) args_for_cases + and make_cases l = List.map make_case l and make_case = - let module P = Mpresentation in let module Con = Content in function Con.ArgProof p -> let name = (match p.Con.proof_name with - None -> P.Mtext([],"no name for case!!") - | Some n -> P.Mi([],n)) in + None -> B.Text([],"no name for case!!") + | Some n -> B.Object ([], P.Mi([],n))) in let indhyps,args = List.partition (function @@ -617,31 +565,28 @@ and proof2pres term2pres p = (match h.Con.dec_name with None -> "NO NAME???" | Some n ->n) in - [P.Mspace([None,"width","0.1cm"]); - P.Mi ([],name); - P.Mtext([],":"); + [B.b_space; + B.Object ([], P.Mi ([],name)); + B.Text([],":"); (term2pres h.Con.dec_type)] - | _ -> [P.Mtext ([],"???")]) in + | _ -> [B.Text ([],"???")]) in dec@p) args [] in let pattern = - P.Mtr ([],[P.Mtd ([],P.Mrow([], - P.Mtext([],"Case")::P.Mspace([None,"width","0.1cm"])::name::pattern_aux@ - [P.Mspace([None,"width","0.1cm"]); - P.Mtext([],"->")]))]) in + B.H ([], + (B.Text([],"Case")::B.b_space::name::pattern_aux)@ + [B.b_space; + B.Text([],"->")]) in let subconcl = (match p.Con.proof_conclude.Con.conclude_conclusion with - None -> P.Mtext([],"No conclusion!!!") + None -> B.Text([],"No conclusion!!!") | Some t -> term2pres t) in - let asubconcl = - P.Mtr([],[P.Mtd([], - P.indented (make_concl "the thesis becomes" subconcl))]) in + let asubconcl = B.indent (make_concl "the thesis becomes" subconcl) in let induction_hypothesis = (match indhyps with [] -> [] | _ -> let text = - P.Mtr([],[P.Mtd([], P.indented - (P.Mtext([],"by induction hypothesis we know:")))]) in + B.indent (B.Text([],"by induction hypothesis we know:")) in let make_hyp = function `Hypothesis h -> @@ -649,17 +594,14 @@ and proof2pres term2pres p = (match h.Con.dec_name with None -> "no name" | Some s -> s) in - P.indented (P.Mrow ([], - [P.Mo([],"("); - P.Mi ([],name); - P.Mo([],")"); - P.Mspace([None,"width","0.1cm"]); + B.indent (B.H ([], + [B.Text([],"("); + B.Object ([], P.Mi ([],name)); + B.Text([],")"); + B.b_space; term2pres h.Con.dec_type])) | _ -> assert false in - let hyps = - List.map - (function ce -> P.Mtr ([], [P.Mtd ([], make_hyp ce)])) - indhyps in + let hyps = List.map make_hyp indhyps in text::hyps) in (* let acontext = acontext2pres_old p.Con.proof_apply_context true in *) @@ -670,16 +612,13 @@ and proof2pres term2pres p = [] -> p.Con.proof_conclude.Con.conclude_id | {Con.proof_id = id}::_ -> id in - P.Maction([None,"actiontype","toggle" ; None,"selection","1"], - [P.indented - (P.Mtext - ([None,"mathcolor","Red" ; + B.Action([None,"type","toggle"], + [B.indent + (B.Text + ([None,"color","red" ; Some "helm", "xref", acontext_id],"Proof")) ; acontext2pres p.Con.proof_apply_context body true]) in - P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"], - pattern::asubconcl::induction_hypothesis@ - [P.Mtr([],[P.Mtd([],presacontext)])]) + B.V ([], pattern::asubconcl::induction_hypothesis@[presacontext]) | _ -> assert false and falseind conclude = @@ -687,7 +626,7 @@ and proof2pres term2pres p = let module Con = Content in let proof_conclusion = (match conclude.Con.conclude_conclusion with - None -> P.Mtext([],"No conclusion???") + None -> B.Text([],"No conclusion???") | Some t -> term2pres t) in let case_arg = (match conclude.Con.conclude_args with @@ -701,11 +640,11 @@ and proof2pres term2pres p = Con.Aux n -> assert false | Con.Premise prem -> (match prem.Con.premise_binder with - None -> [P.Mtext([],"Contradiction, hence")] + None -> [B.Text([],"Contradiction, hence")] | Some n -> - [P.Mi([],n);P.smallskip;P.Mtext([],"is contradictory, hence")]) + [B.Object ([],P.Mi([],n)); B.skip;B.Text([],"is contradictory, hence")]) | Con.Lemma lemma -> - [P.Mi([],lemma.Con.lemma_name);P.smallskip;P.Mtext([],"is contradictory, hence")] + [B.Object ([], P.Mi([],lemma.Con.lemma_name)); B.skip; B.Text([],"is contradictory, hence")] | _ -> assert false) in (* let body = proof2pres {proof with Con.proof_context = tl} in *) make_row arg proof_conclusion @@ -715,7 +654,7 @@ and proof2pres term2pres p = let module Con = Content in let proof_conclusion = (match conclude.Con.conclude_conclusion with - None -> P.Mtext([],"No conclusion???") + None -> B.Text([],"No conclusion???") | Some t -> term2pres t) in let proof,case_arg = (match conclude.Con.conclude_args with @@ -730,9 +669,9 @@ and proof2pres term2pres p = | Con.Premise prem -> (match prem.Con.premise_binder with None -> [] - | Some n -> [P.Mtext([],"by");P.smallskip;P.Mi([],n)]) + | Some n -> [(B.b_kw "by"); B.b_space; B.Object([], P.Mi([],n))]) | Con.Lemma lemma -> - [P.Mtext([],"by");P.smallskip;P.Mi([],lemma.Con.lemma_name)] + [(B.b_kw "by");B.skip; B.Object([], P.Mi([],lemma.Con.lemma_name))] | _ -> assert false) in match proof.Con.proof_context with `Hypothesis hyp1::`Hypothesis hyp2::tl -> @@ -741,32 +680,30 @@ and proof2pres term2pres p = None -> "_" | Some s -> s) in let preshyp1 = - P.Mrow ([], - [P.Mtext([],"("); - P.Mi([],get_name hyp1); - P.Mtext([],")"); - P.smallskip; + B.H ([], + [B.Text([],"("); + B.Object ([], P.Mi([],get_name hyp1)); + B.Text([],")"); + B.skip; term2pres hyp1.Con.dec_type]) in let preshyp2 = - P.Mrow ([], - [P.Mtext([],"("); - P.Mi([],get_name hyp2); - P.Mtext([],")"); - P.smallskip; + B.H ([], + [B.Text([],"("); + B.Object ([], P.Mi([],get_name hyp2)); + B.Text([],")"); + B.skip; term2pres hyp2.Con.dec_type]) in (* let body = proof2pres {proof with Con.proof_context = tl} in *) let body = conclude2pres proof.Con.proof_conclude false true in let presacontext = acontext2pres proof.Con.proof_apply_context body false in - P.Mtable - ([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"], - [P.Mtr ([],[P.Mtd ([], - P.Mrow([],arg@[P.smallskip;P.Mtext([],"we have")]))]); - P.Mtr ([],[P.Mtd ([],preshyp1)]); - P.Mtr ([],[P.Mtd ([],P.Mtext([],"and"))]); - P.Mtr ([],[P.Mtd ([],preshyp2)]); - P.Mtr ([],[P.Mtd ([],presacontext)])]); + B.V + ([], + [B.H ([],arg@[B.skip; B.Text([],"we have")]); + preshyp1; + B.Text([],"and"); + preshyp2; + presacontext]); | _ -> assert false and exists conclude = @@ -774,7 +711,7 @@ and proof2pres term2pres p = let module Con = Content in let proof_conclusion = (match conclude.Con.conclude_conclusion with - None -> P.Mtext([],"No conclusion???") + None -> B.Text([],"No conclusion???") | Some t -> term2pres t) in let proof = (match conclude.Con.conclude_args with @@ -791,30 +728,29 @@ and proof2pres term2pres p = None -> "_" | Some s -> s) in let presdecl = - P.Mrow ([], - [P.Mtext([None,"mathcolor","Red"],"let"); - P.smallskip; - P.Mi([],get_name decl); - P.Mtext([],":"); term2pres decl.Con.dec_type]) in + B.H ([], + [(B.b_kw "let"); + B.skip; + B.Object ([], P.Mi([],get_name decl)); + B.Text([],":"); term2pres decl.Con.dec_type]) in let suchthat = - P.Mrow ([], - [P.Mtext([None,"mathcolor","Red"],"such that"); - P.smallskip; - P.Mtext([],"("); - P.Mi([],get_name hyp); - P.Mtext([],")"); - P.smallskip; + B.H ([], + [(B.b_kw "such that"); + B.skip; + B.Text([],"("); + B.Object ([], P.Mi([],get_name hyp)); + B.Text([],")"); + B.skip; term2pres hyp.Con.dec_type]) in (* let body = proof2pres {proof with Con.proof_context = tl} in *) let body = conclude2pres proof.Con.proof_conclude false true in let presacontext = acontext2pres proof.Con.proof_apply_context body false in - P.Mtable - ([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"], - [P.Mtr ([],[P.Mtd ([],presdecl)]); - P.Mtr ([],[P.Mtd ([],suchthat)]); - P.Mtr ([],[P.Mtd ([],presacontext)])]); + B.V + ([], + [presdecl; + suchthat; + presacontext]); | _ -> assert false in proof2pres p @@ -822,116 +758,86 @@ proof2pres p exception ToDo;; +let aaa = ref 0 + let content2pres term2pres (id,params,metasenv,obj) = - let module K = Content in - let module P = Mpresentation in - match obj with - `Def (K.Const,thesis,`Proof p) -> - p_mtable - [None,"align","baseline 1"; - None,"equalrows","false"; - None,"columnalign","left"; - None,"helm:xref","id"] - ([p_mtr [] - [p_mtd [] - (p_mrow [] - [p_mtext [] - ("UNFINISHED PROOF" ^ id ^"(" ^ - String.concat " ; " (List.map UriManager.string_of_uri params)^ - ")")])] ; - p_mtr [] - [p_mtd [] - (p_mrow [] - [p_mtext [] "THESIS:"])] ; - p_mtr [] - [p_mtd [] - (p_mrow [] - [p_mphantom [] - (p_mtext [] "__") ; - term2pres thesis])]] @ - (match metasenv with - None -> [] - | Some metasenv' -> - [p_mtr [] - [p_mtd [] - (* Conjectures are in their own table to make *) - (* diffing the DOM trees easier. *) - (p_mtable - [None,"align","baseline 1"; - None,"equalrows","false"; - None,"columnalign","left"] - ((p_mtr [] - [p_mtd [] - (p_mrow [] - [p_mtext [] "CONJECTURES:"])]):: - List.map - (function - (id,n,context,ty) -> - p_mtr [] - [p_mtd [] - (p_mrow [Some "helm", "xref", id] - (List.map - (function - None -> - p_mrow [] - [ p_mi [] "_" ; - p_mo [] ":?" ; - p_mi [] "_"] - | Some (`Declaration d) - | Some (`Hypothesis d) -> - let - { K.dec_name = dec_name ; - K.dec_type = ty } = d - in - p_mrow [] - [ p_mi [] - (match dec_name with - None -> "_" - | Some n -> n) ; - p_mo [] ":" ; - term2pres ty] - | Some (`Definition d) -> - let - { K.def_name = def_name ; - K.def_term = bo } = d - in - p_mrow [] - [ p_mi [] - (match def_name with - None -> "_" - | Some n -> n) ; - p_mo [] ":=" ; - term2pres bo] - | Some (`Proof p) -> - let proof_name = p.K.proof_name in - p_mrow [] - [ p_mi [] - (match proof_name with - None -> "_" - | Some n -> n) ; - p_mo [] ":=" ; - proof2pres term2pres p] - ) (List.rev context) @ - [ p_mo [] "|-" ] @ - [ p_mi [] (string_of_int n) ; - p_mo [] ":" ; - term2pres ty ] - )) - ] - ) metasenv' - ))]] - ) @ - [p_mtr [] - [p_mtd [] - (p_mrow [] - [proof2pres term2pres p])]]) - | _ -> raise ToDo + let module K = Content in + match obj with + `Def (K.Const,thesis,`Proof p) -> + B.b_v + [None,"helm:xref","id"] + ([B.b_text [] ("UNFINISHED PROOF " ^ id ^"(" ^ String.concat " ; " (List.map UriManager.string_of_uri params)^ ")") ; + B.b_text [] "THESIS:" ; + B.indent (term2pres thesis)] @ + (match metasenv with + None -> [] + | Some metasenv' -> + (* Conjectures are in their own table to make *) + (* diffing the DOM trees easier. *) + (B.b_v [] + ((B.b_text [] ("CONJECTURES:" ^ (let _ = incr aaa; in (string_of_int !aaa)))):: + (List.map + (function + (id,n,context,ty) -> + (B.b_h [Some "helm", "xref", id] + (((List.map + (function + None -> + B.b_h [] + [ B.b_object (p_mi [] "_") ; + B.b_object (p_mo [] ":?") ; + B.b_object (p_mi [] "_")] + | Some (`Declaration d) + | Some (`Hypothesis d) -> + let + { K.dec_name = dec_name ; + K.dec_type = ty } = d + in + B.b_h [] + [ B.b_object (p_mi [] + (match dec_name with + None -> "_" + | Some n -> n)) ; + B.b_text [] ":" ; + term2pres ty] + | Some (`Definition d) -> + let + { K.def_name = def_name ; + K.def_term = bo } = d + in + B.b_h [] + [ B.b_object (p_mi [] + (match def_name with + None -> "_" + | Some n -> n)) ; + B.b_text [] ":=" ; + term2pres bo] + | Some (`Proof p) -> + let proof_name = p.K.proof_name in + B.b_h [] + [ B.b_object (p_mi [] + (match proof_name with + None -> "_" + | Some n -> n)) ; + B.b_text [] ":=" ; + proof2pres term2pres p] + ) (List.rev context)) @ + [ B.b_text [] "|-" ; + B.b_object (p_mi [] (string_of_int n)) ; + B.b_text [] ":" ; + term2pres ty ]) + )) + ) metasenv')) + )::[proof2pres term2pres p] + ) + ) + | _ -> raise ToDo ;; let content2pres ~ids_to_inner_sorts = content2pres (function p -> - (Cexpr2pres.cexpr2pres_charcount - (Content_expressions.acic2cexpr ids_to_inner_sorts p))) + (Cexpr2pres.cexpr2pres_charcount + (Content_expressions.acic2cexpr ids_to_inner_sorts p))) ;; diff --git a/helm/ocaml/cic_transformations/content2pres.mli b/helm/ocaml/cic_transformations/content2pres.mli index 9b7411685..99a690f7f 100644 --- a/helm/ocaml/cic_transformations/content2pres.mli +++ b/helm/ocaml/cic_transformations/content2pres.mli @@ -34,4 +34,4 @@ val content2pres : ids_to_inner_sorts:(Cic.id, string) Hashtbl.t -> - Cic.annterm Content.cobj -> Mpresentation.mpres + Cic.annterm Content.cobj -> Mpresentation.mpres Box.box diff --git a/helm/ocaml/cic_transformations/mpresentation.ml b/helm/ocaml/cic_transformations/mpresentation.ml index 3c4f92902..a160c7e22 100644 --- a/helm/ocaml/cic_transformations/mpresentation.ml +++ b/helm/ocaml/cic_transformations/mpresentation.ml @@ -210,7 +210,7 @@ and print_mtd = Mtd (attr,m) -> X.xml_nempty ~prefix "mtd" attr [< (print_mpres m) ; X.xml_nempty ~prefix "mphantom" [] (X.xml_nempty ~prefix "mtext" [] (X.xml_cdata "(")) >] ;; -let print_mpres pres = +let document_of_mpres pres = [< Xml.xml_cdata "\n" ; Xml.xml_cdata "\n"; Xml.xml_nempty ~prefix "math" diff --git a/helm/ocaml/cic_transformations/mpresentation.mli b/helm/ocaml/cic_transformations/mpresentation.mli index 53df1fb1d..83f243e6d 100644 --- a/helm/ocaml/cic_transformations/mpresentation.mli +++ b/helm/ocaml/cic_transformations/mpresentation.mli @@ -73,6 +73,6 @@ val two_rows_table_with_brackets : attr -> mpres -> mpres -> mpres -> mpres val two_rows_table_without_brackets : attr -> mpres -> mpres -> mpres -> mpres val row_with_brackets : attr -> mpres -> mpres -> mpres -> mpres val row_without_brackets : attr -> mpres -> mpres -> mpres -> mpres -val print_mpres : - mpres -> Xml.token Stream.t +val print_mpres : mpres -> Xml.token Stream.t +val document_of_mpres : mpres -> Xml.token Stream.t diff --git a/helm/ocaml/cic_transformations/sequent2pres.ml b/helm/ocaml/cic_transformations/sequent2pres.ml index 4c47bc51a..2b159e1c8 100644 --- a/helm/ocaml/cic_transformations/sequent2pres.ml +++ b/helm/ocaml/cic_transformations/sequent2pres.ml @@ -40,12 +40,11 @@ let p_mi a b = Mpresentation.Mi(a,b) let p_mo a b = Mpresentation.Mo(a,b) let p_mrow a b = Mpresentation.Mrow(a,b) let p_mphantom a b = Mpresentation.Mphantom(a,b) +let b_ink a = Box.Ink a let sequent2pres term2pres (_,_,context,ty) = let module K = Content in let module P = Mpresentation in - let make_tr r = - p_mtr [] [p_mtd [] r] in let context2pres context = let rec aux accum = function @@ -57,42 +56,40 @@ let sequent2pres term2pres (_,_,context,ty) = K.dec_id = dec_id ; K.dec_type = ty } = d in let r = - p_mrow [Some "helm", "xref", dec_id] - [ p_mi [] + Box.b_h [Some "helm", "xref", dec_id] + [ Box.b_object (p_mi [] (match dec_name with None -> "_" - | Some n -> n) ; - p_mo [] ":" ; + | Some n -> n)) ; + Box.b_text [] ":" ; term2pres ty] in - aux ((make_tr r)::accum) tl + aux (r::accum) tl | (Some (`Definition d))::tl -> let { K.def_name = def_name ; K.def_id = def_id ; K.def_term = bo } = d in let r = - p_mrow [Some "helm", "xref", def_id] - [ p_mi [] + Box.b_h [Some "helm", "xref", def_id] + [ Box.b_object (p_mi [] (match def_name with None -> "_" - | Some n -> n) ; - p_mo [] ":=" ; + | Some n -> n)) ; + Box.b_text [] ":=" ; term2pres bo] in - aux ((make_tr r)::accum) tl + aux (r::accum) tl | _::_ -> assert false in aux [] context in let pres_context = - make_tr - (p_mtable - [None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"] + (Box.b_v + [] (context2pres context)) in - let pres_goal = - make_tr (term2pres ty) in - (p_mtable - [None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"; None,"rowlines","solid"] - [pres_context;pres_goal]) + let pres_goal = term2pres ty in + (Box.b_v + [] + [pres_context; + b_ink [None,"width","4cm"; None,"height","1px"]; + pres_goal]) ;; let sequent2pres ~ids_to_inner_sorts = diff --git a/helm/ocaml/cic_transformations/sequent2pres.mli b/helm/ocaml/cic_transformations/sequent2pres.mli index 7bb124225..669f4e1c0 100644 --- a/helm/ocaml/cic_transformations/sequent2pres.mli +++ b/helm/ocaml/cic_transformations/sequent2pres.mli @@ -34,6 +34,6 @@ val sequent2pres : ids_to_inner_sorts:(Cic.id, string) Hashtbl.t -> - Cic.annterm Content.conjecture -> Mpresentation.mpres + Cic.annterm Content.conjecture -> Mpresentation.mpres Box.box diff --git a/helm/ocaml/cic_transformations/xml2Gdome.ml b/helm/ocaml/cic_transformations/xml2Gdome.ml index 3d07bf21c..3c77c91b7 100644 --- a/helm/ocaml/cic_transformations/xml2Gdome.ml +++ b/helm/ocaml/cic_transformations/xml2Gdome.ml @@ -24,6 +24,7 @@ *) let document_of_xml (domImplementation : Gdome.domImplementation) strm = +prerr_endline "LUCA: entro nella document_of_xml" ; let module G = Gdome in let module X = Xml in let rec update_namespaces ((defaultns,bindings) as namespaces) = @@ -57,6 +58,7 @@ let document_of_xml (domImplementation : Gdome.domImplementation) strm = | X.NEmpty(p,n,l,c) -> p,n,l,c | _ -> assert false in +prerr_endline "LUCA: entro nella document_of_xml interna" ; let namespaces = update_namespaces (None,[]) root_attributes in let namespaceURI = namespace_of_prefix namespaces root_prefix in let document = @@ -128,6 +130,8 @@ let document_of_xml (domImplementation : Gdome.domImplementation) strm = ~qualifiedName:(get_qualified_name p n) ~value:(Gdome.domString v) ) root_attributes ; +prerr_endline "LUCA: prima di aux" ; aux namespaces (root : Gdome.element :> Gdome.node) root_content ; +prerr_endline "LUCA: dopo di aux" ; document ;; -- 2.39.2