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/
28 let tex_of_unicode s =
29 let contractions = ("\\Longrightarrow","=>") :: [] in
30 if String.length s <= 1 then s
31 else (* probably an extended unicode symbol *)
32 let s = Utf8Macro.tex_of_unicode s in
33 try List.assoc s contractions with Not_found -> s
35 let needs_brackets t =
36 let rec count_brothers = function
37 | Node {brother = brother} -> 1 + count_brothers brother
42 let visit_description desc fmt self =
43 let skip s = List.mem s [ ] in
44 let inline s = List.mem s [ "int" ] in
46 let rec visit_entry e todo is_son nesting =
47 let { ename = ename; edesc = desc } = e in
49 visit_desc desc todo is_son nesting
52 Format.fprintf fmt "%s " ename;
59 and visit_desc d todo is_son nesting =
62 | Dlevels [lev] -> visit_level lev todo is_son nesting
63 | Dlevels (lev::levels) ->
64 let todo = visit_level lev todo is_son nesting in
67 Format.fprintf fmt "@ | ";
68 visit_level l acc is_son nesting)
72 and visit_level l todo is_son nesting =
73 let { lsuffix = suff ; lprefix = pref } = l in
74 let todo = visit_tree suff todo is_son nesting in
75 visit_tree pref todo is_son nesting
77 and visit_tree t todo is_son nesting =
79 | Node node -> visit_node node todo is_son nesting
82 and visit_node n todo is_son nesting =
83 let is_tree_printable t =
88 let { node = symbol; son = son ; brother = brother } = n in
89 let todo = visit_symbol symbol todo is_son nesting in
91 if is_tree_printable son then
93 let need_b = needs_brackets son in
95 Format.fprintf fmt "@[<hov2>";
97 Format.fprintf fmt "( ";
98 let todo = visit_tree son todo true nesting in
100 Format.fprintf fmt ")";
102 Format.fprintf fmt "@]";
108 if is_tree_printable brother then
110 Format.fprintf fmt "@ | ";
111 visit_tree brother todo is_son nesting
116 and visit_symbol s todo is_son nesting =
118 | Smeta (name, sl, _) ->
119 Format.fprintf fmt "%s " name;
122 let todo = visit_symbol s acc is_son nesting in
124 Format.fprintf fmt "@ ";
127 | Snterm entry -> visit_entry entry todo is_son nesting
128 | Snterml (entry,_) -> visit_entry entry todo is_son nesting
130 Format.fprintf fmt "{@[<hov2> ";
131 let todo = visit_symbol symbol todo is_son (nesting+1) in
132 Format.fprintf fmt "@]} @ ";
134 | Slist0sep (symbol,sep) ->
135 Format.fprintf fmt "[@[<hov2> ";
136 let todo = visit_symbol symbol todo is_son (nesting + 1) in
137 Format.fprintf fmt "{@[<hov2> ";
138 let todo = visit_symbol sep todo is_son (nesting + 2) in
139 Format.fprintf fmt " ";
140 let todo = visit_symbol symbol todo is_son (nesting + 2) in
141 Format.fprintf fmt "@]} @]] @ ";
144 Format.fprintf fmt "{@[<hov2> ";
145 let todo = visit_symbol symbol todo is_son (nesting + 1) in
146 Format.fprintf fmt "@]}+ @ ";
148 | Slist1sep (symbol,sep) ->
149 let todo = visit_symbol symbol todo is_son nesting in
150 Format.fprintf fmt "{@[<hov2> ";
151 let todo = visit_symbol sep todo is_son (nesting + 1) in
152 let todo = visit_symbol symbol todo is_son (nesting + 1) in
153 Format.fprintf fmt "@]} @ ";
156 Format.fprintf fmt "[@[<hov2> ";
157 let todo = visit_symbol symbol todo is_son (nesting + 1) in
158 Format.fprintf fmt "@]] @ ";
160 | Sself -> Format.fprintf fmt "%s " self; todo
161 | Snext -> Format.fprintf fmt "next "; todo
163 let constructor, keyword = pattern in
165 Format.fprintf fmt "`%s' " constructor
167 Format.fprintf fmt "\"%s\" " (tex_of_unicode keyword);
170 if needs_brackets tree then
172 Format.fprintf fmt "@[<hov2>( ";
173 let todo = visit_tree tree todo is_son (nesting + 1) in
174 Format.fprintf fmt ")@] @ ";
178 visit_tree tree todo is_son (nesting + 1)
180 visit_desc desc [] false 0
183 let rec clean_dummy_desc = function
184 | Dlevels l -> Dlevels (clean_levels l)
187 and clean_levels = function
189 | l :: tl -> clean_level l @ clean_levels tl
191 and clean_level = function
193 let pref = clean_tree x.lprefix in
194 let suff = clean_tree x.lsuffix in
196 | DeadEnd, DeadEnd -> []
197 | _ -> [{x with lprefix = pref; lsuffix = suff}]
199 and clean_tree = function
200 | Node n -> clean_node n
203 and clean_node = function
204 | {node=node;son=son;brother=brother} ->
205 let bn = is_symbol_dummy node in
206 let bs = is_tree_dummy son in
207 let bb = is_tree_dummy brother in
208 let son = if bs then DeadEnd else son in
209 let brother = if bb then DeadEnd else brother in
210 if bb && bs && bn then
214 Node {node=Sself;son=son;brother=brother}
216 Node {node=node;son=son;brother=brother}
218 and is_level_dummy = function
219 | {lsuffix=lsuffix;lprefix=lprefix} ->
220 is_tree_dummy lsuffix && is_tree_dummy lprefix
222 and is_desc_dummy = function
223 | Dlevels l -> List.for_all is_level_dummy l
226 and is_entry_dummy = function
227 | {edesc=edesc} -> is_desc_dummy edesc
229 and is_symbol_dummy = function
230 | Stoken ("DUMMY", _) -> true
232 | Smeta (_, lt, _) -> List.for_all is_symbol_dummy lt
233 | Snterm e | Snterml (e, _) -> is_entry_dummy e
234 | Slist1 x | Slist0 x -> is_symbol_dummy x
235 | Slist1sep (x,y) | Slist0sep (x,y) -> is_symbol_dummy x && is_symbol_dummy y
236 | Sopt x -> is_symbol_dummy x
237 | Sself | Snext -> false
238 | Stree t -> is_tree_dummy t
240 and is_tree_dummy = function
241 | Node {node=node} -> is_symbol_dummy node
246 let rec visit_entries todo pped =
247 let fmt = Format.std_formatter in
252 if not (List.memq hd pped) then
254 let { ename = ename; edesc = desc } = hd in
255 Format.fprintf fmt "@[<hv2>%s ::=@ " ename;
256 let desc = clean_dummy_desc desc in
257 let todo = visit_description desc fmt ename @ todo in
258 Format.fprintf fmt "@]";
259 Format.pp_print_newline fmt ();
260 Format.pp_print_newline fmt ();
266 let clean_todo todo =
267 let name_of_entry e = e.ename in
268 let pped = hd :: pped in
269 let todo = tl @ todo in
270 let todo = List.filter (fun e -> not(List.memq e pped)) todo in
272 ~eq:(fun e1 e2 -> (name_of_entry e1) = (name_of_entry e2))
275 Pervasives.compare (name_of_entry e1) (name_of_entry e2))
279 let todo,pped = clean_todo todo in
280 visit_entries todo pped
284 let g_entry = Grammar.Entry.obj GrafiteParser.statement in
285 visit_entries [g_entry] []