1 (* Copyright (C) 2005, HELM Team.
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.
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.
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.
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,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
30 let tex_of_unicode s =
31 let contractions = ("\\Longrightarrow","=>") :: [] in
32 if String.length s <= 1 then s
33 else (* probably an extended unicode symbol *)
34 let s = Utf8Macro.tex_of_unicode s in
35 try List.assoc s contractions with Not_found -> s
37 let needs_brackets t =
38 let rec count_brothers = function
39 | Node {brother = brother} -> 1 + count_brothers brother
44 let visit_description desc fmt self =
45 let skip s = List.mem s [ ] in
46 let inline s = List.mem s [ "int" ] in
48 let rec visit_entry e todo is_son nesting =
49 let { ename = ename; edesc = desc } = e in
51 visit_desc desc todo is_son nesting
54 Format.fprintf fmt "%s " ename;
61 and visit_desc d todo is_son nesting =
64 | Dlevels [lev] -> visit_level lev todo is_son nesting
65 | Dlevels (lev::levels) ->
66 let todo = visit_level lev todo is_son nesting in
69 Format.fprintf fmt "@ | ";
70 visit_level l acc is_son nesting)
74 and visit_level l todo is_son nesting =
75 let { lsuffix = suff ; lprefix = pref } = l in
76 let todo = visit_tree suff todo is_son nesting in
77 visit_tree pref todo is_son nesting
79 and visit_tree t todo is_son nesting =
81 | Node node -> visit_node node todo is_son nesting
84 and visit_node n todo is_son nesting =
85 let is_tree_printable t =
90 let { node = symbol; son = son ; brother = brother } = n in
91 let todo = visit_symbol symbol todo is_son nesting in
93 if is_tree_printable son then
95 let need_b = needs_brackets son in
97 Format.fprintf fmt "@[<hov2>";
99 Format.fprintf fmt "( ";
100 let todo = visit_tree son todo true nesting in
102 Format.fprintf fmt ")";
104 Format.fprintf fmt "@]";
110 if is_tree_printable brother then
112 Format.fprintf fmt "@ | ";
113 visit_tree brother todo is_son nesting
118 and visit_symbol s todo is_son nesting =
120 | Smeta (name, sl, _) ->
121 Format.fprintf fmt "%s " name;
124 let todo = visit_symbol s acc is_son nesting in
126 Format.fprintf fmt "@ ";
129 | Snterm entry -> visit_entry entry todo is_son nesting
130 | Snterml (entry,_) -> visit_entry entry todo is_son nesting
132 Format.fprintf fmt "{@[<hov2> ";
133 let todo = visit_symbol symbol todo is_son (nesting+1) in
134 Format.fprintf fmt "@]} @ ";
136 | Slist0sep (symbol,sep) ->
137 Format.fprintf fmt "[@[<hov2> ";
138 let todo = visit_symbol symbol todo is_son (nesting + 1) in
139 Format.fprintf fmt "{@[<hov2> ";
140 let todo = visit_symbol sep todo is_son (nesting + 2) in
141 Format.fprintf fmt " ";
142 let todo = visit_symbol symbol todo is_son (nesting + 2) in
143 Format.fprintf fmt "@]} @]] @ ";
146 Format.fprintf fmt "{@[<hov2> ";
147 let todo = visit_symbol symbol todo is_son (nesting + 1) in
148 Format.fprintf fmt "@]}+ @ ";
150 | Slist1sep (symbol,sep) ->
151 let todo = visit_symbol symbol todo is_son nesting in
152 Format.fprintf fmt "{@[<hov2> ";
153 let todo = visit_symbol sep todo is_son (nesting + 1) in
154 let todo = visit_symbol symbol todo is_son (nesting + 1) in
155 Format.fprintf fmt "@]} @ ";
158 Format.fprintf fmt "[@[<hov2> ";
159 let todo = visit_symbol symbol todo is_son (nesting + 1) in
160 Format.fprintf fmt "@]] @ ";
162 | Sself -> Format.fprintf fmt "%s " self; todo
163 | Snext -> Format.fprintf fmt "next "; todo
165 let constructor, keyword = pattern in
167 Format.fprintf fmt "`%s' " constructor
169 Format.fprintf fmt "\"%s\" " (tex_of_unicode keyword);
172 if needs_brackets tree then
174 Format.fprintf fmt "@[<hov2>( ";
175 let todo = visit_tree tree todo is_son (nesting + 1) in
176 Format.fprintf fmt ")@] @ ";
180 visit_tree tree todo is_son (nesting + 1)
182 visit_desc desc [] false 0
185 let rec clean_dummy_desc = function
186 | Dlevels l -> Dlevels (clean_levels l)
189 and clean_levels = function
191 | l :: tl -> clean_level l @ clean_levels tl
193 and clean_level = function
195 let pref = clean_tree x.lprefix in
196 let suff = clean_tree x.lsuffix in
198 | DeadEnd, DeadEnd -> []
199 | _ -> [{x with lprefix = pref; lsuffix = suff}]
201 and clean_tree = function
202 | Node n -> clean_node n
205 and clean_node = function
206 | {node=node;son=son;brother=brother} ->
207 let bn = is_symbol_dummy node in
208 let bs = is_tree_dummy son in
209 let bb = is_tree_dummy brother in
210 let son = if bs then DeadEnd else son in
211 let brother = if bb then DeadEnd else brother in
212 if bb && bs && bn then
216 Node {node=Sself;son=son;brother=brother}
218 Node {node=node;son=son;brother=brother}
220 and is_level_dummy = function
221 | {lsuffix=lsuffix;lprefix=lprefix} ->
222 is_tree_dummy lsuffix && is_tree_dummy lprefix
224 and is_desc_dummy = function
225 | Dlevels l -> List.for_all is_level_dummy l
228 and is_entry_dummy = function
229 | {edesc=edesc} -> is_desc_dummy edesc
231 and is_symbol_dummy = function
232 | Stoken ("DUMMY", _) -> true
234 | Smeta (_, lt, _) -> List.for_all is_symbol_dummy lt
235 | Snterm e | Snterml (e, _) -> is_entry_dummy e
236 | Slist1 x | Slist0 x -> is_symbol_dummy x
237 | Slist1sep (x,y) | Slist0sep (x,y) -> is_symbol_dummy x && is_symbol_dummy y
238 | Sopt x -> is_symbol_dummy x
239 | Sself | Snext -> false
240 | Stree t -> is_tree_dummy t
242 and is_tree_dummy = function
243 | Node {node=node} -> is_symbol_dummy node
248 let rec visit_entries todo pped =
249 let fmt = Format.std_formatter in
254 if not (List.memq hd pped) then
256 let { ename = ename; edesc = desc } = hd in
257 Format.fprintf fmt "@[<hv2>%s ::=@ " ename;
258 let desc = clean_dummy_desc desc in
259 let todo = visit_description desc fmt ename @ todo in
260 Format.fprintf fmt "@]";
261 Format.pp_print_newline fmt ();
262 Format.pp_print_newline fmt ();
268 let clean_todo todo =
269 let name_of_entry e = e.ename in
270 let pped = hd :: pped in
271 let todo = tl @ todo in
272 let todo = List.filter (fun e -> not(List.memq e pped)) todo in
274 ~eq:(fun e1 e2 -> (name_of_entry e1) = (name_of_entry e2))
277 Pervasives.compare (name_of_entry e1) (name_of_entry e2))
281 let todo,pped = clean_todo todo in
282 visit_entries todo pped
286 let g_entry = Grammar.Entry.obj GrafiteParser.statement in
287 visit_entries [g_entry] []