]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/print_grammar.ml
Reshaped structure of ocaml/ libraries.
[helm.git] / helm / ocaml / cic_notation / print_grammar.ml
diff --git a/helm/ocaml/cic_notation/print_grammar.ml b/helm/ocaml/cic_notation/print_grammar.ml
deleted file mode 100644 (file)
index d7d6f3c..0000000
+++ /dev/null
@@ -1,285 +0,0 @@
-(* 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/
- *)
-
-open Gramext 
-
-let tex_of_unicode s =
-  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
-
-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] []