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 rec flatten_tree = function
33 | Node {node = n; brother = b; son = s} ->
34 List.map (fun l -> n :: l) (flatten_tree s) @ flatten_tree b
36 let tex_of_unicode s = s
38 let rec clean_dummy_desc = function
39 | Dlevels l -> Dlevels (clean_levels l)
42 and clean_levels = function
44 | l :: tl -> clean_level l @ clean_levels tl
46 and clean_level = function
48 let pref = clean_tree x.lprefix in
49 let suff = clean_tree x.lsuffix in
51 | DeadEnd, DeadEnd -> []
52 | _ -> [{x with lprefix = pref; lsuffix = suff}]
54 and clean_tree = function
55 | Node n -> clean_node n
58 and clean_node = function
59 | {node=node;son=son;brother=brother} ->
60 let bn = is_symbol_dummy node in
61 let bs = is_tree_dummy son in
62 let bb = is_tree_dummy brother in
63 let son = if bs then DeadEnd else son in
64 let brother = if bb then DeadEnd else brother in
65 if bb && bs && bn then
69 Node {node=Sself;son=son;brother=brother}
71 Node {node=node;son=son;brother=brother}
73 and is_level_dummy = function
74 | {lsuffix=lsuffix;lprefix=lprefix} ->
75 is_tree_dummy lsuffix && is_tree_dummy lprefix
77 and is_desc_dummy = function
78 | Dlevels l -> List.for_all is_level_dummy l
81 and is_entry_dummy = function
82 | {edesc=edesc} -> is_desc_dummy edesc
84 and is_symbol_dummy = function
85 | Stoken ("DUMMY", _) -> true
87 | Snterm e | Snterml (e, _) -> is_entry_dummy e
88 | Slist1 x | Slist0 x -> is_symbol_dummy x
89 | Slist1sep (x,y,false) | Slist0sep (x,y,false) -> is_symbol_dummy x && is_symbol_dummy y
90 | Sopt x -> is_symbol_dummy x
91 | Sself | Snext -> false
92 | Stree t -> is_tree_dummy t
95 and is_tree_dummy = function
96 | Node {node=node} -> is_symbol_dummy node
99 let needs_brackets t =
100 let rec count_brothers = function
101 | Node {brother = brother} -> 1 + count_brothers brother
106 let visit_description desc fmt self =
107 let skip _s = true in
108 let inline s = List.mem s [ "int" ] in
110 let rec visit_entry e ?level todo is_son =
111 let { ename = ename; edesc = desc } = e in
113 visit_desc desc todo is_son
117 | None -> Format.fprintf fmt "%s " ename;
118 | Some _ -> Format.fprintf fmt "%s " ename;);
125 and visit_desc d todo is_son =
130 Format.fprintf fmt "@ ";
131 visit_level l acc is_son )
135 and visit_level l todo is_son =
136 let { lname = name ; lsuffix = suff ; lprefix = pref } = l in
139 (fun x -> Sself :: x) (flatten_tree suff) @ flatten_tree pref)
142 and visit_tree name t todo _is_son =
143 if List.for_all (List.for_all is_symbol_dummy) t then todo else (
144 Format.fprintf fmt "@[<v>";
146 |Some name -> Format.fprintf fmt "Precedence %s:@ " name
148 Format.fprintf fmt "@[<v>";
152 if List.for_all is_symbol_dummy x then todo else (
153 Format.fprintf fmt "@[<h> | ";
157 let todo = visit_symbol x acc true in
158 Format.fprintf fmt "@ ";
162 Format.fprintf fmt "@]@ ";
166 Format.fprintf fmt "@]";
167 Format.fprintf fmt "@]";
170 and visit_symbol s todo is_son =
172 | Snterm entry -> visit_entry entry todo is_son
173 | Snterml (entry,level) -> visit_entry entry ~level todo is_son
175 Format.fprintf fmt "{@[<hov2> ";
176 let todo = visit_symbol symbol todo is_son in
177 Format.fprintf fmt "@]} @ ";
179 | Slist0sep (symbol,sep,false) ->
180 Format.fprintf fmt "[@[<hov2> ";
181 let todo = visit_symbol symbol todo is_son in
182 Format.fprintf fmt "{@[<hov2> ";
183 let todo = visit_symbol sep todo is_son in
184 Format.fprintf fmt " ";
185 let todo = visit_symbol symbol todo is_son in
186 Format.fprintf fmt "@]} @]] @ ";
189 Format.fprintf fmt "{@[<hov2> ";
190 let todo = visit_symbol symbol todo is_son in
191 Format.fprintf fmt "@]}+ @ ";
193 | Slist1sep (symbol,sep,false) ->
194 let todo = visit_symbol symbol todo is_son in
195 Format.fprintf fmt "{@[<hov2> ";
196 let todo = visit_symbol sep todo is_son in
197 let todo = visit_symbol symbol todo is_son in
198 Format.fprintf fmt "@]} @ ";
201 Format.fprintf fmt "[@[<hov2> ";
202 let todo = visit_symbol symbol todo is_son in
203 Format.fprintf fmt "@]] @ ";
205 | Sself -> Format.fprintf fmt "%s " self; todo
206 | Snext -> Format.fprintf fmt "next "; todo
208 let constructor, keyword = pattern in
210 (if constructor <> "DUMMY" then
211 Format.fprintf fmt "`%s' " constructor)
213 Format.fprintf fmt "%s " (tex_of_unicode keyword);
216 visit_tree None (flatten_tree tree) todo is_son
219 visit_desc desc [] false
223 let rec visit_entries fmt todo pped =
228 if not (List.memq hd pped) then
230 let { ename = ename; edesc = desc } = hd in
231 Format.fprintf fmt "@[<hv 2>%s ::= " ename;
232 let desc = clean_dummy_desc desc in
233 let todo = visit_description desc fmt ename @ todo in
234 Format.fprintf fmt "@]\n\n";
240 let clean_todo todo =
241 let name_of_entry e = e.ename in
242 let pped = hd :: pped in
243 let todo = tl @ todo in
244 let todo = List.filter (fun e -> not(List.memq e pped)) todo in
246 ~eq:(fun e1 e2 -> (name_of_entry e1) = (name_of_entry e2))
249 Stdlib.compare (name_of_entry e1) (name_of_entry e2))
253 let todo,pped = clean_todo todo in
254 visit_entries fmt todo pped
257 let ebnf_of_term status =
258 let g_entry = Grammar.Entry.obj (CicNotationParser.term status) in
259 let buff = Buffer.create 100 in
260 let fmt = Format.formatter_of_buffer buff in
261 visit_entries fmt [g_entry] [];
262 Format.fprintf fmt "@?";
263 let s = Buffer.contents buff in