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