X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fmpresentation.ml;h=6943d9cafeecdca729a82a6247f8c899a6fd4632;hb=12cc5b2b8e7f7bb0b5e315094b008a293a4df6b1;hp=116b845b5f358f830acecd741b369ec229f771a5;hpb=f7b2e35a7bdadb4fdf0e640428e694703ddf67a5;p=helm.git diff --git a/helm/ocaml/cic_transformations/mpresentation.ml b/helm/ocaml/cic_transformations/mpresentation.ml index 116b845b5..6943d9caf 100644 --- a/helm/ocaml/cic_transformations/mpresentation.ml +++ b/helm/ocaml/cic_transformations/mpresentation.ml @@ -32,9 +32,7 @@ (* *) (**************************************************************************) -type - mpres = - (* token elements *) +type 'a mpres = Mi of attr * string | Mn of attr * string | Mo of attr * string @@ -42,52 +40,40 @@ type | Mspace of attr | Ms of attr * string | Mgliph of attr * string - (* General Layout Schemata *) - | Mrow of attr * mpres list - | Mfrac of attr * mpres * mpres - | Msqrt of attr * mpres - | Mroot of attr * mpres * mpres - | Mstyle of attr * mpres - | Merror of attr * mpres - | Mpadded of attr * mpres - | Mphantom of attr * mpres - | Mfenced of attr * mpres list - | Menclose of attr * mpres - (* Script and Limit Schemata *) - | Msub of attr * mpres * mpres - | Msup of attr * mpres * mpres - | Msubsup of attr * mpres * mpres *mpres - | Munder of attr * mpres * mpres - | Mover of attr * mpres * mpres - | Munderover of attr * mpres * mpres *mpres + | Mrow of attr * 'a mpres list + | Mfrac of attr * 'a mpres * 'a mpres + | Msqrt of attr * 'a mpres + | Mroot of attr * 'a mpres * 'a mpres + | Mstyle of attr * 'a mpres + | Merror of attr * 'a mpres + | Mpadded of attr * 'a mpres + | Mphantom of attr * 'a mpres + | Mfenced of attr * 'a mpres list + | Menclose of attr * 'a mpres + | Msub of attr * 'a mpres * 'a mpres + | Msup of attr * 'a mpres * 'a mpres + | Msubsup of attr * 'a mpres * 'a mpres *'a mpres + | Munder of attr * 'a mpres * 'a mpres + | Mover of attr * 'a mpres * 'a mpres + | Munderover of attr * 'a mpres * 'a mpres *'a mpres (* | Multiscripts of ??? NOT IMPLEMEMENTED *) - (* Tables and Matrices *) - | Mtable of attr * row list - (* Enlivening Expressions *) - | Maction of attr * mpres list - -and - - row = Mtr of attr * mtd list - -and - - mtd = Mtd of attr * mpres - -and - - attr = (string * string) list - + | Mtable of attr * 'a row list + | Maction of attr * 'a mpres list + | Mobject of attr * 'a +and 'a row = Mtr of attr * 'a mtd list +and 'a mtd = Mtd of attr * 'a mpres +and attr = (string option * string * string) list ;; -let smallskip = Mspace([("width","0.1cm")]);; -let indentation = Mspace([("width","0.3cm")]);; +let smallskip = Mspace([None,"width","0.5em"]);; +let indentation = Mspace([None,"width","1em"]);; let indented elem = Mrow([],[indentation;elem]);; let standard_tbl_attr = - [("align","baseline 1");("equalrows","false");("columnalign","left")];; + [None,"align","baseline 1";None,"equalrows","false";None,"columnalign","left"] +;; let two_rows_table attr a b = Mtable(attr@standard_tbl_attr, @@ -98,121 +84,105 @@ let two_rows_table_with_brackets attr a b op = (* only the open bracket is added; the closed bracket must be in b *) Mtable(attr@standard_tbl_attr, [Mtr([],[Mtd([],Mrow([],[Mtext([],"(");a]))]); - Mtr([],[Mtd([],Mrow([],[indentation;op;smallskip;b]))])]);; + Mtr([],[Mtd([],Mrow([],[indentation;op;b]))])]);; let two_rows_table_without_brackets attr a b op = Mtable(attr@standard_tbl_attr, [Mtr([],[Mtd([],a)]); - Mtr([],[Mtd([],Mrow([],[indentation;op;smallskip;b]))])]);; + Mtr([],[Mtd([],Mrow([],[indentation;op;b]))])]);; let row_with_brackets attr a b op = (* by analogy with two_rows_table_with_brackets we only add the open brackets *) - Mrow(attr,[Mtext([],"(");a;smallskip;op;smallskip;b]) + Mrow(attr,[Mtext([],"(");a;op;b;Mtext([],")")]) let row_without_brackets attr a b op = - Mrow(attr,[a;smallskip;op;smallskip;b]) + Mrow(attr,[a;op;b]) + +(* MathML prefix *) +let prefix = "m";; -let rec print_mpres = +let print_mpres obj_printer mpres = let module X = Xml in + let rec aux = function - Mi (attr,s) -> X.xml_nempty "mi" attr (X.xml_cdata s) - | Mn (attr,s) -> X.xml_nempty "mn" attr (X.xml_cdata s) - | Mo (attr,s) -> X.xml_nempty "mo" attr (X.xml_cdata s) - | Mtext (attr,s) -> X.xml_nempty "mtext" attr (X.xml_cdata s) - | Mspace attr -> X.xml_empty "mspace" attr - | Ms (attr,s) -> X.xml_nempty "ms" attr (X.xml_cdata s) - | Mgliph (attr,s) -> X.xml_nempty "mgliph" attr (X.xml_cdata s) - (* General Layout Schemata *) - | Mrow (attr,l) -> - X.xml_nempty "mrow" attr - [< (List.fold_right (fun x i -> [< (print_mpres x) ; i >]) l [<>]) - >] - | Mfrac (attr,m1,m2) -> - X.xml_nempty "mfrac" attr - [< print_mpres m1; - print_mpres m2 - >] - | Msqrt (attr,m) -> - X.xml_nempty "msqrt" attr [< print_mpres m >] - | Mroot (attr,m1,m2) -> - X.xml_nempty "mroot" attr - [< print_mpres m1; - print_mpres m2 - >] - | Mstyle (attr,m) -> - X.xml_nempty "mstyle" attr [< print_mpres m >] - | Merror (attr,m) -> - X.xml_nempty "merror" attr [< print_mpres m >] - | Mpadded (attr,m) -> - X.xml_nempty "mpadded" attr [< print_mpres m >] - | Mphantom (attr,m) -> - X.xml_nempty "mphantom" attr [< print_mpres m >] - | Mfenced (attr,l) -> - X.xml_nempty "mfenced" attr - [< (List.fold_right (fun x i -> [< (print_mpres x) ; i >]) l [<>]) - >] - | Menclose (attr,m) -> - X.xml_nempty "menclose" attr [< print_mpres m >] - (* Script and Limit Schemata *) - | Msub (attr,m1,m2) -> - X.xml_nempty "msub" attr - [< print_mpres m1; - print_mpres m2 - >] - | Msup (attr,m1,m2) -> - X.xml_nempty "msup" attr - [< print_mpres m1; - print_mpres m2 - >] - | Msubsup (attr,m1,m2,m3) -> - X.xml_nempty "msubsup" attr - [< print_mpres m1; - print_mpres m2; - print_mpres m3 - >] - | Munder (attr,m1,m2) -> - X.xml_nempty "munder" attr - [< print_mpres m1; - print_mpres m2 - >] - | Mover (attr,m1,m2) -> - X.xml_nempty "mover" attr - [< print_mpres m1; - print_mpres m2 - >] - | Munderover (attr,m1,m2,m3) -> - X.xml_nempty "munderover" attr - [< print_mpres m1; - print_mpres m2; - print_mpres m3 - >] -(* | Multiscripts of ??? NOT IMPLEMEMENTED *) - (* Tables and Matrices *) - | Mtable (attr, rl) -> - X.xml_nempty "mtable" attr - [< (List.fold_right (fun x i -> [< (print_mrow x) ; i >]) rl [<>]) - >] - (* Enlivening Expressions *) - | Maction (attr, l) -> - X.xml_nempty "maction" attr - [< (List.fold_right (fun x i -> [< (print_mpres x) ; i >]) l [<>]) - >] - -and print_mrow = - let module X = Xml in - function - Mtr (attr, l) -> - X.xml_nempty "mtr" attr - [< (List.fold_right (fun x i -> [< (print_mtd x) ; i >]) l [<>]) - >] - -and print_mtd = - let module X = Xml in - function - Mtd (attr,m) -> X.xml_nempty "mtd" attr (print_mpres m) + Mi (attr,s) -> X.xml_nempty ~prefix "mi" attr (X.xml_cdata s) + | Mn (attr,s) -> X.xml_nempty ~prefix "mn" attr (X.xml_cdata s) + | Mo (attr,s) -> X.xml_nempty ~prefix "mo" attr (X.xml_cdata s) + | Mtext (attr,s) -> X.xml_nempty ~prefix "mtext" attr (X.xml_cdata s) + | Mspace attr -> X.xml_empty ~prefix "mspace" attr + | Ms (attr,s) -> X.xml_nempty ~prefix "ms" attr (X.xml_cdata s) + | Mgliph (attr,s) -> X.xml_nempty ~prefix "mgliph" attr (X.xml_cdata s) + (* General Layout Schemata *) + | Mrow (attr,l) -> + X.xml_nempty ~prefix "mrow" attr + [< (List.fold_right (fun x i -> [< (aux x) ; i >]) l [<>]) + >] + | Mfrac (attr,m1,m2) -> + X.xml_nempty ~prefix "mfrac" attr [< aux m1; aux m2 >] + | Msqrt (attr,m) -> + X.xml_nempty ~prefix "msqrt" attr [< aux m >] + | Mroot (attr,m1,m2) -> + X.xml_nempty ~prefix "mroot" attr [< aux m1; aux m2 >] + | Mstyle (attr,m) -> X.xml_nempty ~prefix "mstyle" attr [< aux m >] + | Merror (attr,m) -> X.xml_nempty ~prefix "merror" attr [< aux m >] + | Mpadded (attr,m) -> X.xml_nempty ~prefix "mpadded" attr [< aux m >] + | Mphantom (attr,m) -> X.xml_nempty ~prefix "mphantom" attr [< aux m >] + | Mfenced (attr,l) -> + X.xml_nempty ~prefix "mfenced" attr + [< (List.fold_right (fun x i -> [< (aux x) ; i >]) l [<>]) + >] + | Menclose (attr,m) -> X.xml_nempty ~prefix "menclose" attr [< aux m >] + (* Script and Limit Schemata *) + | Msub (attr,m1,m2) -> + X.xml_nempty ~prefix "msub" attr [< aux m1; aux m2 >] + | Msup (attr,m1,m2) -> + X.xml_nempty ~prefix "msup" attr [< aux m1; aux m2 >] + | Msubsup (attr,m1,m2,m3) -> + X.xml_nempty ~prefix "msubsup" attr [< aux m1; aux m2; aux m3 >] + | Munder (attr,m1,m2) -> + X.xml_nempty ~prefix "munder" attr [< aux m1; aux m2 >] + | Mover (attr,m1,m2) -> + X.xml_nempty ~prefix "mover" attr [< aux m1; aux m2 >] + | Munderover (attr,m1,m2,m3) -> + X.xml_nempty ~prefix "munderover" attr [< aux m1; aux m2; aux m3 >] + (* | Multiscripts of ??? NOT IMPLEMEMENTED *) + (* Tables and Matrices *) + | Mtable (attr, rl) -> + X.xml_nempty ~prefix "mtable" attr + [< (List.fold_right (fun x i -> [< (aux_mrow x) ; i >]) rl [<>]) >] + (* Enlivening Expressions *) + | Maction (attr, l) -> + X.xml_nempty ~prefix "maction" attr + [< (List.fold_right (fun x i -> [< (aux x) ; i >]) l [<>]) >] + | Mobject (attr, obj) -> + X.xml_nempty ~prefix "semantics" attr (obj_printer obj) + and aux_mrow = + let module X = Xml in + function + Mtr (attr, l) -> + X.xml_nempty ~prefix "mtr" attr + [< (List.fold_right (fun x i -> [< (aux_mtd x) ; i >]) l [<>]) + >] + and aux_mtd = + let module X = Xml in + function + Mtd (attr,m) -> X.xml_nempty ~prefix "mtd" attr + [< (aux m) ; + X.xml_nempty ~prefix "mphantom" [] + (X.xml_nempty ~prefix "mtext" [] (X.xml_cdata "(")) >] + in + aux mpres ;; - - +let document_of_mpres pres = + [< Xml.xml_cdata "\n" ; + Xml.xml_cdata "\n"; + Xml.xml_nempty ~prefix "math" + [Some "xmlns","m","http://www.w3.org/1998/Math/MathML" ; + Some "xmlns","helm","http://www.cs.unibo.it/helm" ; + Some "xmlns","xlink","http://www.w3.org/1999/xlink" + ] (Xml.xml_nempty ~prefix "mstyle" [None, "mathvariant", "normal"; None, + "rowspacing", "0.6ex"] (print_mpres (fun _ -> assert false) pres)) + >]