X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Fgrafite_parser%2Fprint_grammar.ml;fp=components%2Fgrafite_parser%2Fprint_grammar.ml;h=f05b77a11b029fa75d60ea5d920793ebca2767fa;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hp=0000000000000000000000000000000000000000;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1;p=helm.git

diff --git a/components/grafite_parser/print_grammar.ml b/components/grafite_parser/print_grammar.ml
new file mode 100644
index 000000000..f05b77a11
--- /dev/null
+++ b/components/grafite_parser/print_grammar.ml
@@ -0,0 +1,291 @@
+(* Copyright (C) 2005, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+(* $Id$ *)
+
+open Gramext 
+
+let tex_of_unicode s =
+(*CSC: ??????? What's the meaning of this function?
+  let contractions = ("\\Longrightarrow","=>") :: [] in
+  if String.length s <= 1 then s
+  else  (* probably an extended unicode symbol *)
+    let s = Utf8Macro.tex_of_unicode s in
+    try List.assoc s contractions with Not_found -> s
+*) match Utf8Macro.tex_of_unicode s with
+      Some s -> s
+    | None -> s
+
+let needs_brackets t =
+  let rec count_brothers = function 
+    | Node {brother = brother} -> 1 + count_brothers brother
+    | _ -> 0
+  in
+  count_brothers t > 1
+
+let visit_description desc fmt self = 
+  let skip s = List.mem s [ ] in
+  let inline s = List.mem s [ "int" ] in
+  
+  let rec visit_entry e todo is_son nesting =
+    let { ename = ename; edesc = desc } = e in 
+    if inline ename then 
+      visit_desc desc todo is_son nesting
+    else
+      begin
+        Format.fprintf fmt "%s " ename;
+        if skip ename then
+          todo
+        else
+          todo @ [e]
+      end
+      
+  and visit_desc d todo is_son nesting =
+    match d with
+    | Dlevels [] -> todo
+    | Dlevels [lev] -> visit_level lev todo is_son nesting
+    | Dlevels (lev::levels) -> 
+        let todo = visit_level lev todo is_son nesting in
+        List.fold_left  
+          (fun acc l -> 
+            Format.fprintf fmt "@ | ";
+            visit_level l acc is_son nesting) 
+          todo levels;
+    | _ -> todo
+    
+  and visit_level l todo is_son nesting =
+    let { lsuffix = suff ; lprefix = pref } = l in
+    let todo = visit_tree suff todo is_son nesting in
+    visit_tree pref todo is_son nesting
+    
+  and visit_tree t todo is_son nesting =
+    match t with
+    | Node node -> visit_node node todo is_son nesting
+    | _ -> todo
+    
+  and visit_node n todo is_son nesting =
+    let is_tree_printable t =
+      match t with
+      | Node _ -> true
+      | _ -> false
+    in
+    let { node = symbol; son = son ; brother = brother } = n in 
+    let todo = visit_symbol symbol todo is_son nesting in
+    let todo =
+      if is_tree_printable son then
+        begin
+          let need_b = needs_brackets son in
+          if not is_son then
+            Format.fprintf fmt "@[<hov2>";
+          if need_b then
+             Format.fprintf fmt "( ";
+          let todo = visit_tree son todo true nesting in
+          if need_b then
+             Format.fprintf fmt ")";
+          if not is_son then
+              Format.fprintf fmt "@]";
+          todo
+        end
+      else
+        todo
+    in
+    if is_tree_printable brother then
+      begin
+        Format.fprintf fmt "@ | ";
+        visit_tree brother todo is_son nesting
+      end
+    else
+      todo
+    
+  and visit_symbol s todo is_son nesting =
+    match s with
+    | Smeta (name, sl, _) -> 
+        Format.fprintf fmt "%s " name;
+        List.fold_left (
+          fun acc s -> 
+            let todo = visit_symbol s acc is_son nesting in
+            if is_son then
+              Format.fprintf fmt "@ ";
+            todo) 
+        todo sl
+    | Snterm entry -> visit_entry entry todo is_son nesting 
+    | Snterml (entry,_) -> visit_entry entry todo is_son nesting
+    | Slist0 symbol -> 
+        Format.fprintf fmt "{@[<hov2> ";
+        let todo = visit_symbol symbol todo is_son (nesting+1) in
+        Format.fprintf fmt "@]} @ ";
+        todo
+    | Slist0sep (symbol,sep) ->
+        Format.fprintf fmt "[@[<hov2> ";
+        let todo = visit_symbol symbol todo is_son (nesting + 1) in
+        Format.fprintf fmt "{@[<hov2> ";
+        let todo = visit_symbol sep todo is_son (nesting + 2) in
+        Format.fprintf fmt " ";
+        let todo = visit_symbol symbol todo is_son (nesting + 2) in
+        Format.fprintf fmt "@]} @]] @ ";
+        todo
+    | Slist1 symbol -> 
+        Format.fprintf fmt "{@[<hov2> ";
+        let todo = visit_symbol symbol todo is_son (nesting + 1) in
+        Format.fprintf fmt "@]}+ @ ";
+        todo 
+    | Slist1sep (symbol,sep) ->
+        let todo = visit_symbol symbol todo is_son nesting in
+        Format.fprintf fmt "{@[<hov2> ";
+        let todo = visit_symbol sep todo is_son (nesting + 1) in
+        let todo = visit_symbol symbol todo is_son (nesting + 1) in
+        Format.fprintf fmt "@]} @ ";
+        todo
+    | Sopt symbol -> 
+        Format.fprintf fmt "[@[<hov2> ";
+        let todo = visit_symbol symbol todo is_son (nesting + 1) in
+        Format.fprintf fmt "@]] @ ";
+        todo
+    | Sself -> Format.fprintf fmt "%s " self; todo
+    | Snext -> Format.fprintf fmt "next "; todo
+    | Stoken pattern -> 
+        let constructor, keyword = pattern in
+        if keyword = "" then
+          Format.fprintf fmt "`%s' " constructor
+        else
+          Format.fprintf fmt "\"%s\" " (tex_of_unicode keyword);
+        todo
+    | Stree tree ->
+        if needs_brackets tree then
+          begin
+            Format.fprintf fmt "@[<hov2>( ";
+            let todo = visit_tree tree todo is_son (nesting + 1) in
+            Format.fprintf fmt ")@] @ ";
+            todo
+          end
+        else
+          visit_tree tree todo is_son (nesting + 1)
+  in
+  visit_desc desc [] false 0
+;;
+
+let rec clean_dummy_desc = function
+  | Dlevels l -> Dlevels (clean_levels l)
+  | x -> x
+
+and clean_levels = function
+  | [] -> []
+  | l :: tl -> clean_level l @ clean_levels tl
+  
+and clean_level = function
+  | x -> 
+      let pref = clean_tree x.lprefix in
+      let suff = clean_tree x.lsuffix in
+      match pref,suff with
+      | DeadEnd, DeadEnd -> []
+      | _ -> [{x with lprefix = pref; lsuffix = suff}]
+  
+and clean_tree = function
+  | Node n -> clean_node n
+  | x -> x
+  
+and clean_node = function
+  | {node=node;son=son;brother=brother} ->
+      let bn = is_symbol_dummy node in
+      let bs = is_tree_dummy son in
+      let bb = is_tree_dummy brother in
+      let son = if bs then DeadEnd else son in
+      let brother = if bb then DeadEnd else brother in
+      if bb && bs && bn then
+        DeadEnd
+      else 
+        if bn then 
+          Node {node=Sself;son=son;brother=brother}
+        else
+          Node {node=node;son=son;brother=brother}
+
+and is_level_dummy = function
+  | {lsuffix=lsuffix;lprefix=lprefix} -> 
+      is_tree_dummy lsuffix && is_tree_dummy lprefix
+  
+and is_desc_dummy = function
+  | Dlevels l -> List.for_all is_level_dummy l
+  | Dparser _ -> true
+  
+and is_entry_dummy = function
+  | {edesc=edesc} -> is_desc_dummy edesc
+  
+and is_symbol_dummy = function
+  | Stoken ("DUMMY", _) -> true
+  | Stoken _ -> false
+  | Smeta (_, lt, _) -> List.for_all is_symbol_dummy lt
+  | Snterm e | Snterml (e, _) -> is_entry_dummy e
+  | Slist1 x | Slist0 x -> is_symbol_dummy x
+  | Slist1sep (x,y) | Slist0sep (x,y) -> is_symbol_dummy x && is_symbol_dummy y
+  | Sopt x -> is_symbol_dummy x
+  | Sself | Snext -> false
+  | Stree t -> is_tree_dummy t
+  
+and is_tree_dummy = function
+  | Node {node=node} -> is_symbol_dummy node 
+  | _ -> true
+;;
+  
+
+let rec visit_entries todo pped =
+  let fmt = Format.std_formatter in
+  match todo with
+  | [] -> ()
+  | hd :: tl -> 
+      let todo =
+        if not (List.memq hd pped) then
+          begin
+            let { ename = ename; edesc = desc } = hd in 
+            Format.fprintf fmt "@[<hv2>%s ::=@ " ename;
+            let desc = clean_dummy_desc desc in 
+            let todo = visit_description desc fmt ename @ todo in
+            Format.fprintf fmt "@]";
+            Format.pp_print_newline fmt ();
+            Format.pp_print_newline fmt ();
+            todo 
+          end
+        else
+          todo
+      in
+      let clean_todo todo =
+        let name_of_entry e = e.ename in
+        let pped = hd :: pped in
+        let todo = tl @ todo in
+        let todo = List.filter (fun e -> not(List.memq e pped)) todo in
+        HExtlib.list_uniq 
+          ~eq:(fun e1 e2 -> (name_of_entry e1) = (name_of_entry e2))
+          (List.sort 
+            (fun e1 e2 -> 
+              Pervasives.compare (name_of_entry e1) (name_of_entry e2))
+            todo),
+        pped
+      in
+      let todo,pped = clean_todo todo in
+      visit_entries todo pped
+;;
+
+let _ =
+  let g_entry = Grammar.Entry.obj GrafiteParser.statement in
+  visit_entries [g_entry] []