]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/grafite_parser/print_grammar.ml
Added a new section on automation
[helm.git] / helm / ocaml / 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   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
36
37 let needs_brackets t =
38   let rec count_brothers = function 
39     | Node {brother = brother} -> 1 + count_brothers brother
40     | _ -> 0
41   in
42   count_brothers t > 1
43
44 let visit_description desc fmt self = 
45   let skip s = List.mem s [ ] in
46   let inline s = List.mem s [ "int" ] in
47   
48   let rec visit_entry e todo is_son nesting =
49     let { ename = ename; edesc = desc } = e in 
50     if inline ename then 
51       visit_desc desc todo is_son nesting
52     else
53       begin
54         Format.fprintf fmt "%s " ename;
55         if skip ename then
56           todo
57         else
58           todo @ [e]
59       end
60       
61   and visit_desc d todo is_son nesting =
62     match d with
63     | Dlevels [] -> todo
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
67         List.fold_left  
68           (fun acc l -> 
69             Format.fprintf fmt "@ | ";
70             visit_level l acc is_son nesting) 
71           todo levels;
72     | _ -> todo
73     
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
78     
79   and visit_tree t todo is_son nesting =
80     match t with
81     | Node node -> visit_node node todo is_son nesting
82     | _ -> todo
83     
84   and visit_node n todo is_son nesting =
85     let is_tree_printable t =
86       match t with
87       | Node _ -> true
88       | _ -> false
89     in
90     let { node = symbol; son = son ; brother = brother } = n in 
91     let todo = visit_symbol symbol todo is_son nesting in
92     let todo =
93       if is_tree_printable son then
94         begin
95           let need_b = needs_brackets son in
96           if not is_son then
97             Format.fprintf fmt "@[<hov2>";
98           if need_b then
99              Format.fprintf fmt "( ";
100           let todo = visit_tree son todo true nesting in
101           if need_b then
102              Format.fprintf fmt ")";
103           if not is_son then
104               Format.fprintf fmt "@]";
105           todo
106         end
107       else
108         todo
109     in
110     if is_tree_printable brother then
111       begin
112         Format.fprintf fmt "@ | ";
113         visit_tree brother todo is_son nesting
114       end
115     else
116       todo
117     
118   and visit_symbol s todo is_son nesting =
119     match s with
120     | Smeta (name, sl, _) -> 
121         Format.fprintf fmt "%s " name;
122         List.fold_left (
123           fun acc s -> 
124             let todo = visit_symbol s acc is_son nesting in
125             if is_son then
126               Format.fprintf fmt "@ ";
127             todo) 
128         todo sl
129     | Snterm entry -> visit_entry entry todo is_son nesting 
130     | Snterml (entry,_) -> visit_entry entry todo is_son nesting
131     | Slist0 symbol -> 
132         Format.fprintf fmt "{@[<hov2> ";
133         let todo = visit_symbol symbol todo is_son (nesting+1) in
134         Format.fprintf fmt "@]} @ ";
135         todo
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 "@]} @]] @ ";
144         todo
145     | Slist1 symbol -> 
146         Format.fprintf fmt "{@[<hov2> ";
147         let todo = visit_symbol symbol todo is_son (nesting + 1) in
148         Format.fprintf fmt "@]}+ @ ";
149         todo 
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 "@]} @ ";
156         todo
157     | Sopt symbol -> 
158         Format.fprintf fmt "[@[<hov2> ";
159         let todo = visit_symbol symbol todo is_son (nesting + 1) in
160         Format.fprintf fmt "@]] @ ";
161         todo
162     | Sself -> Format.fprintf fmt "%s " self; todo
163     | Snext -> Format.fprintf fmt "next "; todo
164     | Stoken pattern -> 
165         let constructor, keyword = pattern in
166         if keyword = "" then
167           Format.fprintf fmt "`%s' " constructor
168         else
169           Format.fprintf fmt "\"%s\" " (tex_of_unicode keyword);
170         todo
171     | Stree tree ->
172         if needs_brackets tree then
173           begin
174             Format.fprintf fmt "@[<hov2>( ";
175             let todo = visit_tree tree todo is_son (nesting + 1) in
176             Format.fprintf fmt ")@] @ ";
177             todo
178           end
179         else
180           visit_tree tree todo is_son (nesting + 1)
181   in
182   visit_desc desc [] false 0
183 ;;
184
185 let rec clean_dummy_desc = function
186   | Dlevels l -> Dlevels (clean_levels l)
187   | x -> x
188
189 and clean_levels = function
190   | [] -> []
191   | l :: tl -> clean_level l @ clean_levels tl
192   
193 and clean_level = function
194   | x -> 
195       let pref = clean_tree x.lprefix in
196       let suff = clean_tree x.lsuffix in
197       match pref,suff with
198       | DeadEnd, DeadEnd -> []
199       | _ -> [{x with lprefix = pref; lsuffix = suff}]
200   
201 and clean_tree = function
202   | Node n -> clean_node n
203   | x -> x
204   
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
213         DeadEnd
214       else 
215         if bn then 
216           Node {node=Sself;son=son;brother=brother}
217         else
218           Node {node=node;son=son;brother=brother}
219
220 and is_level_dummy = function
221   | {lsuffix=lsuffix;lprefix=lprefix} -> 
222       is_tree_dummy lsuffix && is_tree_dummy lprefix
223   
224 and is_desc_dummy = function
225   | Dlevels l -> List.for_all is_level_dummy l
226   | Dparser _ -> true
227   
228 and is_entry_dummy = function
229   | {edesc=edesc} -> is_desc_dummy edesc
230   
231 and is_symbol_dummy = function
232   | Stoken ("DUMMY", _) -> true
233   | Stoken _ -> false
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
241   
242 and is_tree_dummy = function
243   | Node {node=node} -> is_symbol_dummy node 
244   | _ -> true
245 ;;
246   
247
248 let rec visit_entries todo pped =
249   let fmt = Format.std_formatter in
250   match todo with
251   | [] -> ()
252   | hd :: tl -> 
253       let todo =
254         if not (List.memq hd pped) then
255           begin
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 ();
263             todo 
264           end
265         else
266           todo
267       in
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
273         HExtlib.list_uniq 
274           ~eq:(fun e1 e2 -> (name_of_entry e1) = (name_of_entry e2))
275           (List.sort 
276             (fun e1 e2 -> 
277               Pervasives.compare (name_of_entry e1) (name_of_entry e2))
278             todo),
279         pped
280       in
281       let todo,pped = clean_todo todo in
282       visit_entries todo pped
283 ;;
284
285 let _ =
286   let g_entry = Grammar.Entry.obj GrafiteParser.statement in
287   visit_entries [g_entry] []