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 (*CSC: ??????? What's the meaning of this function?
32 let contractions = ("\\Longrightarrow","=>") :: [] in
33 if String.length s <= 1 then s
34 else (* probably an extended unicode symbol *)
35 let s = Utf8Macro.tex_of_unicode s in
36 try List.assoc s contractions with Not_found -> s
37 *) match Utf8Macro.tex_of_unicode s with
41 let needs_brackets t =
42 let rec count_brothers = function
43 | Node {brother = brother} -> 1 + count_brothers brother
48 let visit_description desc fmt self =
49 let skip s = List.mem s [ ] in
50 let inline s = List.mem s [ "int" ] in
52 let rec visit_entry e todo is_son nesting =
53 let { ename = ename; edesc = desc } = e in
55 visit_desc desc todo is_son nesting
58 Format.fprintf fmt "%s " ename;
65 and visit_desc d todo is_son nesting =
68 | Dlevels [lev] -> visit_level lev todo is_son nesting
69 | Dlevels (lev::levels) ->
70 let todo = visit_level lev todo is_son nesting in
73 Format.fprintf fmt "@ | ";
74 visit_level l acc is_son nesting)
78 and visit_level l todo is_son nesting =
79 let { lsuffix = suff ; lprefix = pref } = l in
80 let todo = visit_tree suff todo is_son nesting in
81 visit_tree pref todo is_son nesting
83 and visit_tree t todo is_son nesting =
85 | Node node -> visit_node node todo is_son nesting
88 and visit_node n todo is_son nesting =
89 let is_tree_printable t =
94 let { node = symbol; son = son ; brother = brother } = n in
95 let todo = visit_symbol symbol todo is_son nesting in
97 if is_tree_printable son then
99 let need_b = needs_brackets son in
101 Format.fprintf fmt "@[<hov2>";
103 Format.fprintf fmt "( ";
104 let todo = visit_tree son todo true nesting in
106 Format.fprintf fmt ")";
108 Format.fprintf fmt "@]";
114 if is_tree_printable brother then
116 Format.fprintf fmt "@ | ";
117 visit_tree brother todo is_son nesting
122 and visit_symbol s todo is_son nesting =
124 | Smeta (name, sl, _) ->
125 Format.fprintf fmt "%s " name;
128 let todo = visit_symbol s acc is_son nesting in
130 Format.fprintf fmt "@ ";
133 | Snterm entry -> visit_entry entry todo is_son nesting
134 | Snterml (entry,_) -> visit_entry entry todo is_son nesting
136 Format.fprintf fmt "{@[<hov2> ";
137 let todo = visit_symbol symbol todo is_son (nesting+1) in
138 Format.fprintf fmt "@]} @ ";
140 | Slist0sep (symbol,sep) ->
141 Format.fprintf fmt "[@[<hov2> ";
142 let todo = visit_symbol symbol todo is_son (nesting + 1) in
143 Format.fprintf fmt "{@[<hov2> ";
144 let todo = visit_symbol sep todo is_son (nesting + 2) in
145 Format.fprintf fmt " ";
146 let todo = visit_symbol symbol todo is_son (nesting + 2) in
147 Format.fprintf fmt "@]} @]] @ ";
150 Format.fprintf fmt "{@[<hov2> ";
151 let todo = visit_symbol symbol todo is_son (nesting + 1) in
152 Format.fprintf fmt "@]}+ @ ";
154 | Slist1sep (symbol,sep) ->
155 let todo = visit_symbol symbol todo is_son nesting in
156 Format.fprintf fmt "{@[<hov2> ";
157 let todo = visit_symbol sep todo is_son (nesting + 1) in
158 let todo = visit_symbol symbol todo is_son (nesting + 1) in
159 Format.fprintf fmt "@]} @ ";
162 Format.fprintf fmt "[@[<hov2> ";
163 let todo = visit_symbol symbol todo is_son (nesting + 1) in
164 Format.fprintf fmt "@]] @ ";
166 | Sself -> Format.fprintf fmt "%s " self; todo
167 | Snext -> Format.fprintf fmt "next "; todo
169 let constructor, keyword = pattern in
171 Format.fprintf fmt "`%s' " constructor
173 Format.fprintf fmt "\"%s\" " (tex_of_unicode keyword);
176 if needs_brackets tree then
178 Format.fprintf fmt "@[<hov2>( ";
179 let todo = visit_tree tree todo is_son (nesting + 1) in
180 Format.fprintf fmt ")@] @ ";
184 visit_tree tree todo is_son (nesting + 1)
186 visit_desc desc [] false 0
189 let rec clean_dummy_desc = function
190 | Dlevels l -> Dlevels (clean_levels l)
193 and clean_levels = function
195 | l :: tl -> clean_level l @ clean_levels tl
197 and clean_level = function
199 let pref = clean_tree x.lprefix in
200 let suff = clean_tree x.lsuffix in
202 | DeadEnd, DeadEnd -> []
203 | _ -> [{x with lprefix = pref; lsuffix = suff}]
205 and clean_tree = function
206 | Node n -> clean_node n
209 and clean_node = function
210 | {node=node;son=son;brother=brother} ->
211 let bn = is_symbol_dummy node in
212 let bs = is_tree_dummy son in
213 let bb = is_tree_dummy brother in
214 let son = if bs then DeadEnd else son in
215 let brother = if bb then DeadEnd else brother in
216 if bb && bs && bn then
220 Node {node=Sself;son=son;brother=brother}
222 Node {node=node;son=son;brother=brother}
224 and is_level_dummy = function
225 | {lsuffix=lsuffix;lprefix=lprefix} ->
226 is_tree_dummy lsuffix && is_tree_dummy lprefix
228 and is_desc_dummy = function
229 | Dlevels l -> List.for_all is_level_dummy l
232 and is_entry_dummy = function
233 | {edesc=edesc} -> is_desc_dummy edesc
235 and is_symbol_dummy = function
236 | Stoken ("DUMMY", _) -> true
238 | Smeta (_, lt, _) -> List.for_all is_symbol_dummy lt
239 | Snterm e | Snterml (e, _) -> is_entry_dummy e
240 | Slist1 x | Slist0 x -> is_symbol_dummy x
241 | Slist1sep (x,y) | Slist0sep (x,y) -> is_symbol_dummy x && is_symbol_dummy y
242 | Sopt x -> is_symbol_dummy x
243 | Sself | Snext -> false
244 | Stree t -> is_tree_dummy t
246 and is_tree_dummy = function
247 | Node {node=node} -> is_symbol_dummy node
252 let rec visit_entries todo pped =
253 let fmt = Format.std_formatter in
258 if not (List.memq hd pped) then
260 let { ename = ename; edesc = desc } = hd in
261 Format.fprintf fmt "@[<hv2>%s ::=@ " ename;
262 let desc = clean_dummy_desc desc in
263 let todo = visit_description desc fmt ename @ todo in
264 Format.fprintf fmt "@]";
265 Format.pp_print_newline fmt ();
266 Format.pp_print_newline fmt ();
272 let clean_todo todo =
273 let name_of_entry e = e.ename in
274 let pped = hd :: pped in
275 let todo = tl @ todo in
276 let todo = List.filter (fun e -> not(List.memq e pped)) todo in
278 ~eq:(fun e1 e2 -> (name_of_entry e1) = (name_of_entry e2))
281 Pervasives.compare (name_of_entry e1) (name_of_entry e2))
285 let todo,pped = clean_todo todo in
286 visit_entries todo pped
290 let g_entry = Grammar.Entry.obj GrafiteParser.statement in
291 visit_entries [g_entry] []