]> matita.cs.unibo.it Git - helm.git/blob - components/content_pres/mpresentation.ml
unified: some theorems on Lift started
[helm.git] / components / content_pres / mpresentation.ml
1 (* Copyright (C) 2000, HELM Team.
2  * 
3  * This file is part of HELM, an Hypertextual, Electronic
4  * Library of Mathematics, developed at the Computer Science
5  * Department, University of Bologna, Italy.
6  * 
7  * HELM is free software; you can redistribute it and/or
8  * modify it under the terms of the GNU General Public License
9  * as published by the Free Software Foundation; either version 2
10  * of the License, or (at your option) any later version.
11  * 
12  * HELM is distributed in the hope that it will be useful,
13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
15  * GNU General Public License for more details.
16  *
17  * You should have received a copy of the GNU General Public License
18  * along with HELM; if not, write to the Free Software
19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 (**************************************************************************)
27 (*                                                                        *)
28 (*                           PROJECT HELM                                 *)
29 (*                                                                        *)
30 (*                Andrea Asperti <asperti@cs.unibo.it>                    *)
31 (*                             16/62003                                   *)
32 (*                                                                        *)
33 (**************************************************************************)
34
35 (* $Id$ *)
36
37 type 'a mpres = 
38     Mi of attr * string
39   | Mn of attr * string
40   | Mo of attr * string
41   | Mtext of attr * string
42   | Mspace of attr
43   | Ms of attr * string
44   | Mgliph of attr * string
45   | Mrow of attr * 'a mpres list
46   | Mfrac of attr * 'a mpres * 'a mpres
47   | Msqrt of attr * 'a mpres
48   | Mroot of attr * 'a mpres * 'a mpres
49   | Mstyle of attr * 'a mpres
50   | Merror of attr * 'a mpres
51   | Mpadded of attr * 'a mpres
52   | Mphantom of attr * 'a mpres
53   | Mfenced of attr * 'a mpres list
54   | Menclose of attr * 'a mpres
55   | Msub of attr * 'a mpres * 'a mpres
56   | Msup of attr * 'a mpres * 'a mpres
57   | Msubsup of attr * 'a mpres * 'a mpres *'a mpres 
58   | Munder of attr * 'a mpres * 'a mpres
59   | Mover of attr * 'a mpres * 'a mpres
60   | Munderover of attr * 'a mpres * 'a mpres *'a mpres 
61 (* | Multiscripts of ???  NOT IMPLEMEMENTED *)
62   | Mtable of attr * 'a row list
63   | Maction of attr * 'a mpres list
64   | Mobject of attr * 'a
65 and 'a row = Mtr of attr * 'a mtd list
66 and 'a mtd = Mtd of attr * 'a mpres
67 and attr = (string option * string * string) list
68 ;;
69
70 let smallskip = Mspace([None,"width","0.5em"]);;
71 let indentation = Mspace([None,"width","1em"]);;
72
73 let indented elem =
74   Mrow([],[indentation;elem]);;
75
76 let standard_tbl_attr = 
77   [None,"align","baseline 1";None,"equalrows","false";None,"columnalign","left"]
78 ;;
79
80 let two_rows_table attr a b =
81   Mtable(attr@standard_tbl_attr,
82     [Mtr([],[Mtd([],a)]);
83      Mtr([],[Mtd([],b)])]);;
84
85 let two_rows_table_with_brackets attr a b op =
86   (* only the open bracket is added; the closed bracket must be in b *)
87   Mtable(attr@standard_tbl_attr,
88     [Mtr([],[Mtd([],Mrow([],[Mtext([],"(");a]))]);
89      Mtr([],[Mtd([],Mrow([],[indentation;op;b]))])]);;
90
91 let two_rows_table_without_brackets attr a b op =
92   Mtable(attr@standard_tbl_attr,
93     [Mtr([],[Mtd([],a)]);
94      Mtr([],[Mtd([],Mrow([],[indentation;op;b]))])]);;
95
96 let row_with_brackets attr a b op =
97   (* by analogy with two_rows_table_with_brackets we only add the
98      open brackets *)
99   Mrow(attr,[Mtext([],"(");a;op;b;Mtext([],")")])
100
101 let row_without_brackets attr a b op =
102   Mrow(attr,[a;op;b])
103
104 (* MathML prefix *)
105 let prefix = "m";;
106  
107 let print_mpres obj_printer mpres =
108  let module X = Xml in
109  let rec aux =
110     function
111       Mi (attr,s) -> X.xml_nempty ~prefix "mi" attr (X.xml_cdata s)
112     | Mn (attr,s) -> X.xml_nempty ~prefix "mn" attr (X.xml_cdata s)
113     | Mo (attr,s) ->
114         let s =
115           let len = String.length s in
116           if len > 1 && s.[0] = '\\'
117           then String.sub s 1 (len - 1)
118           else s
119         in
120         X.xml_nempty ~prefix "mo" attr (X.xml_cdata s)
121     | Mtext (attr,s) -> X.xml_nempty ~prefix "mtext" attr (X.xml_cdata s)
122     | Mspace attr -> X.xml_empty ~prefix "mspace" attr
123     | Ms (attr,s) -> X.xml_nempty ~prefix "ms" attr (X.xml_cdata s)
124     | Mgliph (attr,s) -> X.xml_nempty ~prefix "mgliph" attr (X.xml_cdata s)
125     (* General Layout Schemata *)
126     | Mrow (attr,l) ->
127         X.xml_nempty ~prefix "mrow" attr 
128            [< (List.fold_right (fun x i -> [< (aux x) ; i >]) l [<>])
129             >]
130     | Mfrac (attr,m1,m2) ->
131          X.xml_nempty ~prefix "mfrac" attr [< aux m1; aux m2 >]
132     | Msqrt (attr,m) ->
133          X.xml_nempty ~prefix "msqrt" attr [< aux m >]
134     | Mroot  (attr,m1,m2) ->
135          X.xml_nempty ~prefix "mroot" attr [< aux m1; aux m2 >]
136     | Mstyle (attr,m) -> X.xml_nempty ~prefix "mstyle" attr [< aux m >]
137     | Merror (attr,m) -> X.xml_nempty ~prefix "merror" attr [< aux m >]
138     | Mpadded (attr,m) -> X.xml_nempty ~prefix "mpadded" attr [< aux m >]
139     | Mphantom (attr,m) -> X.xml_nempty ~prefix "mphantom" attr [< aux m >]
140     | Mfenced (attr,l) ->
141         X.xml_nempty ~prefix "mfenced" attr 
142            [< (List.fold_right (fun x i -> [< (aux x) ; i >]) l [<>])
143             >]
144     | Menclose (attr,m) -> X.xml_nempty ~prefix "menclose" attr [< aux m >]
145     (* Script and Limit Schemata *)
146     | Msub (attr,m1,m2) ->
147         X.xml_nempty ~prefix "msub" attr [< aux m1; aux m2 >]
148     | Msup (attr,m1,m2) ->
149         X.xml_nempty ~prefix "msup" attr [< aux m1; aux m2 >]
150     | Msubsup (attr,m1,m2,m3) ->
151         X.xml_nempty ~prefix "msubsup" attr [< aux m1; aux m2; aux m3 >]
152     | Munder (attr,m1,m2) ->
153         X.xml_nempty ~prefix "munder" attr [< aux m1; aux m2 >]
154     | Mover (attr,m1,m2) ->
155         X.xml_nempty ~prefix "mover" attr [< aux m1; aux m2 >]
156     | Munderover (attr,m1,m2,m3) ->
157         X.xml_nempty ~prefix "munderover" attr [< aux m1; aux m2; aux m3 >]
158   (* | Multiscripts of ???  NOT IMPLEMEMENTED *)
159     (* Tables and Matrices *)
160     | Mtable (attr, rl) ->
161         X.xml_nempty ~prefix "mtable" attr 
162            [< (List.fold_right (fun x i -> [< (aux_mrow x) ; i >]) rl [<>]) >]
163     (* Enlivening Expressions *)
164     | Maction (attr, l) ->
165         X.xml_nempty ~prefix "maction" attr 
166           [< (List.fold_right (fun x i -> [< (aux x) ; i >]) l [<>]) >]
167     | Mobject (attr, obj) ->
168         let box_stream = obj_printer obj in
169         X.xml_nempty ~prefix "semantics" attr
170           [< X.xml_nempty ~prefix "annotation-xml" [None, "encoding", "BoxML"]
171               box_stream >]
172           
173   and aux_mrow =
174    let module X = Xml in
175    function 
176       Mtr (attr, l) -> 
177         X.xml_nempty ~prefix "mtr" attr 
178            [< (List.fold_right (fun x i -> [< (aux_mtd x) ; i >]) l [<>])
179             >]
180   and aux_mtd =
181     let module X = Xml in
182     function 
183        Mtd (attr,m) -> X.xml_nempty ~prefix "mtd" attr
184         [< (aux m) ;
185             X.xml_nempty ~prefix "mphantom" []
186               (X.xml_nempty ~prefix "mtext" [] (X.xml_cdata "(")) >]
187   in
188   aux mpres
189 ;;
190
191 let document_of_mpres pres =
192  [< Xml.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
193     Xml.xml_cdata "\n";
194     Xml.xml_nempty ~prefix "math"
195      [Some "xmlns","m","http://www.w3.org/1998/Math/MathML" ;
196       Some "xmlns","helm","http://www.cs.unibo.it/helm" ;
197       Some "xmlns","xlink","http://www.w3.org/1999/xlink"
198      ] (Xml.xml_nempty ~prefix "mstyle" [None, "mathvariant", "normal"; None,
199      "rowspacing", "0.6ex"] (print_mpres (fun _ -> assert false) pres))
200  >]
201
202 let get_attr = function
203   | Maction (attr, _)
204   | Menclose (attr, _)
205   | Merror (attr, _)
206   | Mfenced (attr, _)
207   | Mfrac (attr, _, _)
208   | Mgliph (attr, _)
209   | Mi (attr, _)
210   | Mn (attr, _)
211   | Mo (attr, _)
212   | Mobject (attr, _)
213   | Mover (attr, _, _)
214   | Mpadded (attr, _)
215   | Mphantom (attr, _)
216   | Mroot (attr, _, _)
217   | Mrow (attr, _)
218   | Ms (attr, _)
219   | Mspace attr
220   | Msqrt (attr, _)
221   | Mstyle (attr, _)
222   | Msub (attr, _, _)
223   | Msubsup (attr, _, _, _)
224   | Msup (attr, _, _)
225   | Mtable (attr, _)
226   | Mtext (attr, _)
227   | Munder (attr, _, _)
228   | Munderover (attr, _, _, _) ->
229       attr
230
231 let set_attr attr = function
232   | Maction (_, x) -> Maction (attr, x)
233   | Menclose (_, x) -> Menclose (attr, x)
234   | Merror (_, x) -> Merror (attr, x)
235   | Mfenced (_, x) -> Mfenced (attr, x)
236   | Mfrac (_, x, y) -> Mfrac (attr, x, y)
237   | Mgliph (_, x) -> Mgliph (attr, x)
238   | Mi (_, x) -> Mi (attr, x)
239   | Mn (_, x) -> Mn (attr, x)
240   | Mo (_, x) -> Mo (attr, x)
241   | Mobject (_, x) -> Mobject (attr, x)
242   | Mover (_, x, y) -> Mover (attr, x, y)
243   | Mpadded (_, x) -> Mpadded (attr, x)
244   | Mphantom (_, x) -> Mphantom (attr, x)
245   | Mroot (_, x, y) -> Mroot (attr, x, y)
246   | Mrow (_, x) -> Mrow (attr, x)
247   | Ms (_, x) -> Ms (attr, x)
248   | Mspace _ -> Mspace attr
249   | Msqrt (_, x) -> Msqrt (attr, x)
250   | Mstyle (_, x) -> Mstyle (attr, x)
251   | Msub (_, x, y) -> Msub (attr, x, y)
252   | Msubsup (_, x, y, z) -> Msubsup (attr, x, y, z)
253   | Msup (_, x, y) -> Msup (attr, x, y)
254   | Mtable (_, x) -> Mtable (attr, x)
255   | Mtext (_, x) -> Mtext (attr, x)
256   | Munder (_, x, y) -> Munder (attr, x, y)
257   | Munderover (_, x, y, z) -> Munderover (attr, x, y, z)
258