]> matita.cs.unibo.it Git - helm.git/blob - components/grafite_parser/print_grammar.ml
snapshot
[helm.git] / components / grafite_parser / print_grammar.ml
1 (* Copyright (C) 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 (* $Id$ *)
27
28 open Gramext 
29
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
38       Some s -> s
39     | None -> s
40
41 let needs_brackets t =
42   let rec count_brothers = function 
43     | Node {brother = brother} -> 1 + count_brothers brother
44     | _ -> 0
45   in
46   count_brothers t > 1
47
48 let visit_description desc fmt self = 
49   let skip s = List.mem s [ ] in
50   let inline s = List.mem s [ "int" ] in
51   
52   let rec visit_entry e todo is_son nesting =
53     let { ename = ename; edesc = desc } = e in 
54     if inline ename then 
55       visit_desc desc todo is_son nesting
56     else
57       begin
58         Format.fprintf fmt "%s " ename;
59         if skip ename then
60           todo
61         else
62           todo @ [e]
63       end
64       
65   and visit_desc d todo is_son nesting =
66     match d with
67     | Dlevels [] -> todo
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
71         List.fold_left  
72           (fun acc l -> 
73             Format.fprintf fmt "@ | ";
74             visit_level l acc is_son nesting) 
75           todo levels;
76     | _ -> todo
77     
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
82     
83   and visit_tree t todo is_son nesting =
84     match t with
85     | Node node -> visit_node node todo is_son nesting
86     | _ -> todo
87     
88   and visit_node n todo is_son nesting =
89     let is_tree_printable t =
90       match t with
91       | Node _ -> true
92       | _ -> false
93     in
94     let { node = symbol; son = son ; brother = brother } = n in 
95     let todo = visit_symbol symbol todo is_son nesting in
96     let todo =
97       if is_tree_printable son then
98         begin
99           let need_b = needs_brackets son in
100           if not is_son then
101             Format.fprintf fmt "@[<hov2>";
102           if need_b then
103              Format.fprintf fmt "( ";
104           let todo = visit_tree son todo true nesting in
105           if need_b then
106              Format.fprintf fmt ")";
107           if not is_son then
108               Format.fprintf fmt "@]";
109           todo
110         end
111       else
112         todo
113     in
114     if is_tree_printable brother then
115       begin
116         Format.fprintf fmt "@ | ";
117         visit_tree brother todo is_son nesting
118       end
119     else
120       todo
121     
122   and visit_symbol s todo is_son nesting =
123     match s with
124     | Smeta (name, sl, _) -> 
125         Format.fprintf fmt "%s " name;
126         List.fold_left (
127           fun acc s -> 
128             let todo = visit_symbol s acc is_son nesting in
129             if is_son then
130               Format.fprintf fmt "@ ";
131             todo) 
132         todo sl
133     | Snterm entry -> visit_entry entry todo is_son nesting 
134     | Snterml (entry,_) -> visit_entry entry todo is_son nesting
135     | Slist0 symbol -> 
136         Format.fprintf fmt "{@[<hov2> ";
137         let todo = visit_symbol symbol todo is_son (nesting+1) in
138         Format.fprintf fmt "@]} @ ";
139         todo
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 "@]} @]] @ ";
148         todo
149     | Slist1 symbol -> 
150         Format.fprintf fmt "{@[<hov2> ";
151         let todo = visit_symbol symbol todo is_son (nesting + 1) in
152         Format.fprintf fmt "@]}+ @ ";
153         todo 
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 "@]} @ ";
160         todo
161     | Sopt symbol -> 
162         Format.fprintf fmt "[@[<hov2> ";
163         let todo = visit_symbol symbol todo is_son (nesting + 1) in
164         Format.fprintf fmt "@]] @ ";
165         todo
166     | Sself -> Format.fprintf fmt "%s " self; todo
167     | Snext -> Format.fprintf fmt "next "; todo
168     | Stoken pattern -> 
169         let constructor, keyword = pattern in
170         if keyword = "" then
171           Format.fprintf fmt "`%s' " constructor
172         else
173           Format.fprintf fmt "\"%s\" " (tex_of_unicode keyword);
174         todo
175     | Stree tree ->
176         if needs_brackets tree then
177           begin
178             Format.fprintf fmt "@[<hov2>( ";
179             let todo = visit_tree tree todo is_son (nesting + 1) in
180             Format.fprintf fmt ")@] @ ";
181             todo
182           end
183         else
184           visit_tree tree todo is_son (nesting + 1)
185   in
186   visit_desc desc [] false 0
187 ;;
188
189 let rec clean_dummy_desc = function
190   | Dlevels l -> Dlevels (clean_levels l)
191   | x -> x
192
193 and clean_levels = function
194   | [] -> []
195   | l :: tl -> clean_level l @ clean_levels tl
196   
197 and clean_level = function
198   | x -> 
199       let pref = clean_tree x.lprefix in
200       let suff = clean_tree x.lsuffix in
201       match pref,suff with
202       | DeadEnd, DeadEnd -> []
203       | _ -> [{x with lprefix = pref; lsuffix = suff}]
204   
205 and clean_tree = function
206   | Node n -> clean_node n
207   | x -> x
208   
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
217         DeadEnd
218       else 
219         if bn then 
220           Node {node=Sself;son=son;brother=brother}
221         else
222           Node {node=node;son=son;brother=brother}
223
224 and is_level_dummy = function
225   | {lsuffix=lsuffix;lprefix=lprefix} -> 
226       is_tree_dummy lsuffix && is_tree_dummy lprefix
227   
228 and is_desc_dummy = function
229   | Dlevels l -> List.for_all is_level_dummy l
230   | Dparser _ -> true
231   
232 and is_entry_dummy = function
233   | {edesc=edesc} -> is_desc_dummy edesc
234   
235 and is_symbol_dummy = function
236   | Stoken ("DUMMY", _) -> true
237   | Stoken _ -> false
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
245   
246 and is_tree_dummy = function
247   | Node {node=node} -> is_symbol_dummy node 
248   | _ -> true
249 ;;
250   
251
252 let rec visit_entries todo pped =
253   let fmt = Format.std_formatter in
254   match todo with
255   | [] -> ()
256   | hd :: tl -> 
257       let todo =
258         if not (List.memq hd pped) then
259           begin
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 ();
267             todo 
268           end
269         else
270           todo
271       in
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
277         HExtlib.list_uniq 
278           ~eq:(fun e1 e2 -> (name_of_entry e1) = (name_of_entry e2))
279           (List.sort 
280             (fun e1 e2 -> 
281               Pervasives.compare (name_of_entry e1) (name_of_entry e2))
282             todo),
283         pped
284       in
285       let todo,pped = clean_todo todo in
286       visit_entries todo pped
287 ;;
288
289 let _ =
290   let g_entry = Grammar.Entry.obj GrafiteParser.statement in
291   visit_entries [g_entry] []