+(* 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/
+ *)
+
+(* $Id$ *)
+
+open Gramext
+
+let rec flatten_tree = function
+ | DeadEnd -> []
+ | LocAct _ -> [[]]
+ | Node {node = n; brother = b; son = s} ->
+ List.map (fun l -> n :: l) (flatten_tree s) @ flatten_tree b
+
+let tex_of_unicode s = s
+
+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
+ | _ -> assert false
+
+and is_tree_dummy = function
+ | Node {node=node} -> is_symbol_dummy node
+ | _ -> true
+
+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 = true in
+ let inline s = List.mem s [ "int" ] in
+
+ let rec visit_entry e ?level todo is_son =
+ let { ename = ename; edesc = desc } = e in
+ if inline ename then
+ visit_desc desc todo is_son
+ else
+ begin
+ (match level with
+ | None -> Format.fprintf fmt "%s " ename;
+ | Some _ -> Format.fprintf fmt "%s " ename;);
+ if skip ename then
+ todo
+ else
+ todo @ [e]
+ end
+
+ and visit_desc d todo is_son =
+ match d with
+ | Dlevels l ->
+ List.fold_left
+ (fun acc l ->
+ Format.fprintf fmt "@ ";
+ visit_level l acc is_son )
+ todo l;
+ | Dparser _ -> todo
+
+ and visit_level l todo is_son =
+ let { lname = name ; lsuffix = suff ; lprefix = pref } = l in
+ visit_tree name
+ (List.map
+ (fun x -> Sself :: x) (flatten_tree suff) @ flatten_tree pref)
+ todo is_son
+
+ and visit_tree name t todo is_son =
+ if List.for_all (List.for_all is_symbol_dummy) t then todo else (
+ Format.fprintf fmt "@[<v>";
+ (match name with
+ |Some name -> Format.fprintf fmt "Precedence %s:@ " name
+ | None -> ());
+ Format.fprintf fmt "@[<v>";
+ let todo =
+ List.fold_left
+ (fun acc x ->
+ if List.for_all is_symbol_dummy x then todo else (
+ Format.fprintf fmt "@[<h> | ";
+ let todo =
+ List.fold_left
+ (fun acc x ->
+ let todo = visit_symbol x acc true in
+ Format.fprintf fmt "@ ";
+ todo)
+ acc x
+ in
+ Format.fprintf fmt "@]@ ";
+ todo))
+ todo t
+ in
+ Format.fprintf fmt "@]";
+ Format.fprintf fmt "@]";
+ todo)
+
+ and visit_symbol s todo is_son =
+ 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 in
+ if is_son then
+ Format.fprintf fmt "@ ";
+ todo)
+ todo sl
+ | Snterm entry -> visit_entry entry todo is_son
+ | Snterml (entry,level) -> visit_entry entry ~level todo is_son
+ | Slist0 symbol ->
+ Format.fprintf fmt "{@[<hov2> ";
+ let todo = visit_symbol symbol todo is_son in
+ Format.fprintf fmt "@]} @ ";
+ todo
+ | Slist0sep (symbol,sep) ->
+ Format.fprintf fmt "[@[<hov2> ";
+ let todo = visit_symbol symbol todo is_son in
+ Format.fprintf fmt "{@[<hov2> ";
+ let todo = visit_symbol sep todo is_son in
+ Format.fprintf fmt " ";
+ let todo = visit_symbol symbol todo is_son in
+ Format.fprintf fmt "@]} @]] @ ";
+ todo
+ | Slist1 symbol ->
+ Format.fprintf fmt "{@[<hov2> ";
+ let todo = visit_symbol symbol todo is_son in
+ Format.fprintf fmt "@]}+ @ ";
+ todo
+ | Slist1sep (symbol,sep) ->
+ let todo = visit_symbol symbol todo is_son in
+ Format.fprintf fmt "{@[<hov2> ";
+ let todo = visit_symbol sep todo is_son in
+ let todo = visit_symbol symbol todo is_son in
+ Format.fprintf fmt "@]} @ ";
+ todo
+ | Sopt symbol ->
+ Format.fprintf fmt "[@[<hov2> ";
+ let todo = visit_symbol symbol todo is_son 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
+ (if constructor <> "DUMMY" then
+ Format.fprintf fmt "`%s' " constructor)
+ else
+ Format.fprintf fmt "%s " (tex_of_unicode keyword);
+ todo
+ | Stree tree ->
+ visit_tree None (flatten_tree tree) todo is_son
+ | _ -> assert false
+ in
+ visit_desc desc [] false
+;;
+
+
+let rec visit_entries fmt todo pped =
+ 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 "@[<hv 2>%s ::= " ename;
+ let desc = clean_dummy_desc desc in
+ let todo = visit_description desc fmt ename @ todo in
+ Format.fprintf fmt "@]\n\n";
+ 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 fmt todo pped
+;;
+
+let ebnf_of_term () =
+ let g_entry = Grammar.Entry.obj (CicNotationParser.term ()) in
+ let buff = Buffer.create 100 in
+ let fmt = Format.formatter_of_buffer buff in
+ visit_entries fmt [g_entry] [];
+ Format.fprintf fmt "@?";
+ let s = Buffer.contents buff in
+ s
+;;