]> matita.cs.unibo.it Git - helm.git/blob - matitaB/components/content_pres/cicNotationPres.ml
Matitaweb: TeX-like macro handling.
[helm.git] / matitaB / components / content_pres / cicNotationPres.ml
1 (* Copyright (C) 2004-2005, 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://helm.cs.unibo.it/
24  *)
25
26 open Printf
27
28 module A = NotationPt
29
30 type markup = string Box.box
31
32 let to_unicode = Utf8Macro.unicode_of_tex
33
34 let small_skip    = Box.Text ([], " ")
35 let open_paren    = Box.Text ([], "(")
36 let closed_paren  = Box.Text ([], ")")
37 let semicolon     = Box.Text ([], ";")
38
39 let toggle_action children =
40   Box.Action ([None, "actiontype", "toggle"], children)
41
42 type child_pos = [ `Left | `Right | `Inner ]
43
44 let pp_assoc =
45   function
46   | Gramext.LeftA -> "LeftA"
47   | Gramext.RightA -> "RightA"
48   | Gramext.NonA -> "NonA"
49
50 let rec is_atomic = function
51   | Box.Space _
52   | Box.Ink _
53   | Box.Text _ 
54   | Box.Object _ -> true
55   | Box.H (_, [box])
56   | Box.V (_, [box])
57   | Box.HV (_, [box])
58   | Box.HOV (_, [box])
59   | Box.Action (_, [box]) -> is_atomic box
60   | _ -> false
61
62 let add_parens child_prec curr_prec t =
63   if is_atomic t then 
64     ((*prerr_endline ("NOT adding parens around ATOMIC: "^
65       BoxPp.render_to_string (function x::_->x|_->assert false)
66         ~map_unicode_to_tex:false 80 t);*)t)
67   else if child_prec >= 0 && child_prec < curr_prec then 
68     begin 
69     (*prerr_endline ("adding parens around: "^
70       BoxPp.render_to_string (function x::_->x|_->assert false)
71         ~map_unicode_to_tex:false 80 t);*)
72       Box.H ([], [ open_paren; t; closed_paren ])
73   end else
74     ((*prerr_endline ("NOT adding parens around: "^
75       BoxPp.render_to_string (function x::_->x|_->assert false)
76         ~map_unicode_to_tex:false 80 t);*)t)
77
78 let box_of spec attrs children =
79   match children with
80     | [t] -> t
81     | _ ->
82         let kind, spacing, indent = spec in
83         let dress children =
84           if spacing then
85             NotationUtil.dress small_skip children
86           else
87             children
88         in
89         let attrs' =
90           (if spacing then [None, "spacing", "0.5em"] else [])
91           @ (if indent then [None, "indent", "0.5em"] else []) 
92           @ attrs
93         in
94           match kind with
95             | A.H -> Box.H (attrs',children)
96             | A.V -> Box.V (attrs',children)
97             | A.HV -> Box.HV (attrs',children)
98             | A.HOV -> Box.HOV (attrs',children)
99
100 let render status ?(prec=(-1)) =
101   let rec aux prec t =
102     match t with
103     | A.AttributedTerm _ ->
104         aux_attributes [] ""  prec t
105     | A.Num (literal, _) -> Box.Text ([], literal)
106     | A.Symbol (literal, Some (None,desc)) ->
107         let literal = to_unicode literal in
108         let attr = [ None, "title", desc ] in
109           Box.Text (attr, literal)
110     | A.Symbol (literal, Some (Some u,desc)) -> 
111         let literal = to_unicode literal in
112         let attr = [ None, "title", desc; None, "href", u ] in
113         Box.Text (attr, literal)
114     | A.Symbol (literal, _) -> Box.Text ([], to_unicode literal)
115     | A.Ident (literal, `Uri u) ->
116         let attr = [ None, "href", u ] in
117         let literal = to_unicode literal in
118         Box.Text (attr,literal)
119     | A.Ident (literal, _) -> Box.Text ([], to_unicode literal)
120     | A.Meta(n, l) ->
121         let local_context =
122           Box.Text ([], "["):: 
123             (NotationUtil.dress (Box.Text ([],  ";"))
124               (List.map 
125                 (function 
126                 | None -> Box.Text ([],  "_")
127                 | Some t -> aux prec t) l)) @
128             [Box.Text ([], "]")]
129         in
130         Box.H ([],
131           (Box.Text ([], "?"^string_of_int n)::
132             (if (l <> []) then [Box.H ([],local_context)] else [])))
133     | A.Literal (`Symbol (s,x))
134     | A.Literal (`Keyword (s,x))
135     | A.Literal (`Number (s,x)) ->
136        let attr = 
137          match x with
138          | None, None -> []
139          | Some u, None -> [ None, "href", u ]
140          | None, Some d -> [ None, "title", d ]
141          | Some u, Some d -> [ None, "href", u; None, "title", d ]
142        in        
143        Box.Text (attr, to_unicode s)
144     | A.UserInput -> Box.Text ([], "%")
145     | A.Layout l -> aux_layout prec l
146     | A.Magic _
147     | A.Variable _ -> assert false  (* should have been instantiated *)
148     | t ->
149         prerr_endline ("unexpected ast: " ^ NotationPp.pp_term status t);
150         assert false
151
152   and aux_attributes xmlattrs xref  prec t =
153     let reset = ref false in
154     let inferred_level = ref None in
155     let expected_level = ref None in
156     let new_xref = ref [] in
157     let new_xmlattrs = ref [] in
158     let rec aux_attribute =
159       function
160       | A.AttributedTerm (attr, t) ->
161           (match attr with
162           | `Loc _
163           | `Raw _ -> ()
164           | `Level (-1) -> reset := true
165           | `Level child_prec ->
166 (*               assert (!expected_level = None); *)
167               expected_level := !inferred_level;
168               inferred_level := Some child_prec
169           | `IdRef xref -> new_xref := xref :: !new_xref
170           | `XmlAttrs attrs -> new_xmlattrs := attrs @ !new_xmlattrs);
171           aux_attribute t
172       | t ->
173           let prec = 
174             match !expected_level with
175             | None -> prec
176             | Some prec -> prec
177           in
178           (match !inferred_level with
179           | None -> aux prec t
180           | Some child_prec ->
181               let t' = aux child_prec t in
182               (*prerr_endline 
183                 ("inferred: "^string_of_int child_prec^ 
184                  " exp: "^string_of_int prec ^ 
185                  " term: "^BoxPp.render_to_string ~map_unicode_to_tex:false
186                     (function x::_->x|_->assert false) 80 t');*)
187               if !reset
188               then ((*prerr_endline "reset";*)t')
189               else add_parens child_prec prec t')
190     in
191 (*     prerr_endline (NotationPp.pp_term t); *)
192     aux_attribute t
193
194   and aux_layout prec l =
195     let attrs = [] in
196     let invoke' t = aux prec t in
197       (* use the one below to reset precedence and associativity *)
198     let invoke_reinit t = aux ~-1 t in
199     match l with
200     | A.Sup (A.Layout (A.Sub (t1,t2)), t3)
201     | A.Sup (A.AttributedTerm (_,A.Layout (A.Sub (t1,t2))), t3)
202       -> assert false
203     | A.Sub (t1, t2) -> Box.H ([],[aux prec t1;Box.Text ([],"_");aux prec t2])
204     | A.Sup (t1, t2) -> Box.H ([],[aux prec t1;Box.Text ([],"^");aux prec t2])
205     | A.Below (t1, t2) -> assert false 
206     | A.Above (t1, t2) -> assert false
207     | A.Frac (t1, t2)
208     | A.Over (t1, t2) -> assert false
209     | A.Atop (t1, t2) -> assert false
210     | A.InfRule (t1, t2, t3) -> assert false
211     | A.Sqrt t -> assert false
212     | A.Root (t1, t2) -> assert false
213     | A.Box ((_,spacing,_) as kind, terms) ->
214         let children =
215           aux_children spacing prec
216             (NotationUtil.ungroup terms)
217         in
218         box_of kind attrs children
219     | A.Mstyle (l,terms) -> assert false
220     | A.Mpadded (l,terms) -> assert false
221     | A.Maction alternatives -> 
222          toggle_action (List.map invoke_reinit alternatives)
223     | A.Group terms -> assert false 
224     | A.Break -> Box.Space []
225   and aux_children spacing prec terms =
226     let find_clusters =
227       let rec aux_list first clusters acc =
228         function
229             [] when acc = [] -> List.rev clusters
230           | [] -> aux_list first (List.rev acc :: clusters) [] []
231           | (A.Layout A.Break) :: tl when acc = [] ->
232               aux_list first clusters [] tl
233           | (A.Layout A.Break) :: tl ->
234               aux_list first (List.rev acc :: clusters) [] tl
235           | [hd] ->
236                 aux_list false clusters
237                   (aux prec hd :: acc) []
238           | hd :: tl ->
239                 aux_list false clusters
240                   (aux prec hd :: acc) tl
241       in
242         aux_list true [] []
243     in
244     let boxify_pres =
245       function
246           [t] -> t
247         | tl -> box_of (A.H, spacing, false) [] tl
248     in
249       List.map boxify_pres (find_clusters terms) 
250   in
251   (fun t ->
252    (* prerr_endline ("ast:\n" ^ (NotationPp.pp_term status t));*)
253   aux prec t)
254
255 (* let render_to_boxml id_to_uri t =
256   let xml_stream = print_box (box_of_mpres (render id_to_uri t)) in
257   Xml.add_xml_declaration xml_stream *)
258
259 let render_context_entry status name = function
260   | A.Decl t -> 
261       Box.H ([],
262              [Box.Text([],name); Box.Text([],":"); 
263               render status (TermContentPres.pp_ast status t)])
264   | A.Def (t,ty) -> 
265       Box.H ([],
266               [Box.Text([],name); Box.Text([],Utf8Macro.unicode_of_tex"\\def");
267                render status (TermContentPres.pp_ast status t)])
268
269 let render_context status context =
270   Box.V ([], 
271          Box.Space [None, "width", "0.5em"]:: 
272          List.map 
273            (fun (name,entry) -> 
274               render_context_entry status (to_unicode name) entry) context)
275
276 let render_sequent status (i,context,ty) =
277   Box.V ([],
278          [render_context status (List.rev context);
279           Box.Ink [None,"width","4cm"; None,"height","2px"];
280           render status (TermContentPres.pp_ast status ty)])
281           
282