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