helm/ocaml/cic_notation/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] []