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