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 no_expansion = ["|";",";"(";")";"[";"]";":";"_";".";"=";";";"{";"}"] in
  30   let contractions =
  31     ("\\Longrightarrow","=>") :: []
  32   in
  33   if List.exists ((=) s) no_expansion then s
  34   else
  35     let s = Utf8Macro.tex_of_unicode s in
  36     try List.assoc s contractions with Not_found -> s
  37
  38 let visit_description desc fmt =
  39   let skip s = List.mem s [ ] in
  40   let inline s = List.mem s [ "int" ] in
  41
  42   let rec visit_entry e todo is_son nesting =
  43     let { ename = ename; edesc = desc } = e in
  44     if inline ename then
  45       visit_desc desc todo is_son nesting
  46     else
  47       begin
  48         Format.fprintf fmt "%s " ename;
  49         if skip ename then
  50           todo
  51         else
  52           todo @ [e]
  53       end
  54
  55   and visit_desc d todo is_son nesting =
  56     match d with
  57     | Dlevels [] -> todo
  58     | Dlevels [lev] -> visit_level lev todo is_son nesting
  59     | Dlevels (lev::levels) ->
  60         let todo = visit_level lev todo is_son nesting in
  61         List.fold_left
  62           (fun acc l ->
  63             Format.fprintf fmt "@ | ";
  64             visit_level l acc is_son nesting)
  65           todo levels;
  66     | _ -> todo
  67
  68   and visit_level l todo is_son nesting =
  69     let { lsuffix = suff ; lprefix = pref } = l in
  70     let todo = visit_tree suff todo is_son nesting in
  71     visit_tree pref todo is_son nesting
  72
  73   and visit_tree t todo is_son nesting =
  74     match t with
  75     | Node node -> visit_node node todo is_son nesting
  76     | _ -> todo
  77
  78   and visit_node n todo is_son nesting =
  79     let is_tree_printable t =
  80       match t with
  81       | Node _ -> true
  82       | _ -> false
  83     in
  84     let needs_brackets t =
  85       let rec count_brothers = function
  86         | Node {brother = brother} -> 1 + count_brothers brother
  87         | _ -> 0
  88       in
  89       count_brothers t > 1
  90     in
  91     let { node = symbol; son = son ; brother = brother } = n in
  92     let todo = visit_symbol symbol todo is_son nesting in
  93     let todo =
  94       if is_tree_printable son then
  95         begin
  96           let need_b = needs_brackets son in
  97           if not is_son then
  98             Format.fprintf fmt "@[<hov2>";
  99           if need_b then
 100              Format.fprintf fmt "( ";
 101           let todo = visit_tree son todo true nesting in
 102           if need_b then
 103              Format.fprintf fmt ")";
 104           if not is_son then
 105               Format.fprintf fmt "@]";
 106           todo
 107         end
 108       else
 109         todo
 110     in
 111     if is_tree_printable brother then
 112       begin
 113         Format.fprintf fmt "@ | ";
 114         visit_tree brother todo is_son nesting
 115       end
 116     else
 117       todo
 118
 119   and visit_symbol s todo is_son nesting =
 120     match s with
 121     | Smeta (name, sl, _) ->
 122         Format.fprintf fmt "%s " name;
 123         List.fold_left (
 124           fun acc s ->
 125             let todo = visit_symbol s acc is_son nesting in
 126             if is_son then
 127               Format.fprintf fmt "@ ";
 128             todo)
 129         todo sl
 130     | Snterm entry -> visit_entry entry todo is_son nesting
 131     | Snterml (entry,_) -> visit_entry entry todo is_son nesting
 132     | Slist0 symbol ->
 133         Format.fprintf fmt "@[<hov2>{ ";
 134         let todo = visit_symbol symbol todo is_son (nesting+1) in
 135         Format.fprintf fmt "}@] @ ";
 136         todo
 137     | Slist0sep (symbol,sep) ->
 138         Format.fprintf fmt "@[<hov2>[ ";
 139         let todo = visit_symbol symbol todo is_son (nesting + 1) in
 140         Format.fprintf fmt "@[<hov2>{ ";
 141         let todo = visit_symbol sep todo is_son (nesting + 2) in
 142         Format.fprintf fmt " ";
 143         let todo = visit_symbol symbol todo is_son (nesting + 2) in
 144         Format.fprintf fmt "}@] @ ]@] @ ";
 145         todo
 146     | Slist1 symbol ->
 147         Format.fprintf fmt "@[<hov2>{ ";
 148         let todo = visit_symbol symbol todo is_son (nesting + 1) in
 149         Format.fprintf fmt "}+@] @ ";
 150         todo
 151     | Slist1sep (symbol,sep) ->
 152         let todo = visit_symbol symbol todo is_son nesting in
 153         Format.fprintf fmt " @[<hov2>{ ";
 154         let todo = visit_symbol sep todo is_son (nesting + 1) in
 155         let todo = visit_symbol symbol todo is_son (nesting + 1) in
 156         Format.fprintf fmt "}@] @ ";
 157         todo
 158     | Sopt symbol ->
 159         Format.fprintf fmt "@[<hov2>[ ";
 160         let todo = visit_symbol symbol todo is_son (nesting + 1) in
 161         Format.fprintf fmt "]@] @ ";
 162         todo
 163     | Sself -> Format.fprintf fmt "self "; todo
 164     | Snext -> Format.fprintf fmt "next "; todo
 165     | Stoken pattern ->
 166         let constructor, keyword = pattern in
 167         if keyword = "" then
 168           Format.fprintf fmt "'%s' " constructor
 169         else
 170           Format.fprintf fmt "\"%s\" " (tex_of_unicode keyword);
 171         todo
 172     | Stree tree -> visit_tree tree todo is_son nesting
 173   in
 174   visit_desc desc [] false 0
 175 ;;
 176
 177 let rec clean_dummy_desc = function
 178   | Dlevels l -> Dlevels (clean_levels l)
 179   | x -> x
 180
 181 and clean_levels = function
 182   | [] -> []
 183   | l :: tl -> clean_level l @ clean_levels tl
 184
 185 and clean_level = function
 186   | x ->
 187       let pref = clean_tree x.lprefix in
 188       let suff = clean_tree x.lsuffix in
 189       match pref,suff with
 190       | DeadEnd, DeadEnd -> []
 191       | _ -> [{x with lprefix = pref; lsuffix = suff}]
 192
 193 and clean_tree = function
 194   | Node n -> clean_node n
 195   | x -> x
 196
 197 and clean_node = function
 198   | {node=node;son=son;brother=brother} when
 199       is_symbol_dummy node &&
 200       is_tree_dummy son &&
 201       is_tree_dummy brother -> DeadEnd
 202   | x -> Node x
 203
 204 and is_level_dummy = function
 205   | {lsuffix=lsuffix;lprefix=lprefix} ->
 206       is_tree_dummy lsuffix && is_tree_dummy lprefix
 207
 208 and is_desc_dummy = function
 209   | Dlevels l -> List.for_all is_level_dummy l
 210   | Dparser _ -> true
 211
 212 and is_entry_dummy = function
 213   | {edesc=edesc} -> is_desc_dummy edesc
 214
 215 and is_symbol_dummy = function
 216   | Stoken ("DUMMY", _) -> true
 217   | Stoken _ -> false
 218   | Smeta (_, lt, _) -> List.for_all is_symbol_dummy lt
 219   | Snterm e | Snterml (e, _) -> is_entry_dummy e
 220   | Slist1 x | Slist0 x -> is_symbol_dummy x
 221   | Slist1sep (x,y) | Slist0sep (x,y) -> is_symbol_dummy x && is_symbol_dummy y
 222   | Sopt x -> is_symbol_dummy x
 223   | Sself -> false
 224   | Snext -> true
 225   | Stree t -> is_tree_dummy t
 226
 227 and is_tree_dummy = function
 228   | Node {node=node} -> is_symbol_dummy node
 229   | _ -> true
 230 ;;
 231
 232
 233 let rec visit_entries todo pped =
 234   let fmt = Format.std_formatter in
 235   match todo with
 236   | [] -> ()
 237   | hd :: tl ->
 238       let todo =
 239         if not (List.memq hd pped) then
 240           begin
 241             let { ename = ename; edesc = desc } = hd in
 242             Format.fprintf fmt "@[<hv2>%s ::=@ " ename;
 243             let desc = clean_dummy_desc desc in
 244             let todo = visit_description desc fmt @ todo in
 245             Format.fprintf fmt "@]";
 246             Format.pp_print_newline fmt ();
 247             Format.pp_print_newline fmt ();
 248             todo
 249           end
 250         else
 251           todo
 252       in
 253       let clean_todo todo =
 254         let name_of_entry e = e.ename in
 255         let pped = hd :: pped in
 256         let todo = tl @ todo in
 257         let todo = List.filter (fun e -> not(List.memq e pped)) todo in
 258         HExtlib.list_uniq
 259           ~eq:(fun e1 e2 -> (name_of_entry e1) = (name_of_entry e2))
 260           (List.sort
 261             (fun e1 e2 ->
 262               Pervasives.compare (name_of_entry e1) (name_of_entry e2))
 263             todo),
 264         pped
 265       in
 266       let todo,pped = clean_todo todo in
 267       visit_entries todo pped
 268 ;;
 269
 270 let _ =
 271 (*  let g_entry = Grammar.Entry.obj CicNotationParser.term in*)
 272   let g_entry = Grammar.Entry.obj GrafiteParser.statement in
 273   visit_entries [g_entry] []