--- /dev/null
+(* 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/
+ *)
+
+open Gramext
+
+let tex_of_unicode s =
+ let no_expansion = ["|";",";"(";")";"[";"]";":";"_";".";"=";";";"{";"}"] in
+ let contractions =
+ ("\\Longrightarrow","=>") :: []
+ in
+ if List.exists ((=) s) no_expansion then s
+ else
+ let s = Utf8Macro.tex_of_unicode s in
+ try List.assoc s contractions with Not_found -> s
+
+let visit_description desc fmt =
+ let skip s = List.mem s [ ] in
+ let inline s = List.mem s [ "int" ] in
+
+ let rec visit_entry e todo is_son nesting =
+ let { ename = ename; edesc = desc } = e in
+ if inline ename then
+ visit_desc desc todo is_son nesting
+ else
+ begin
+ Format.fprintf fmt "%s " ename;
+ if skip ename then
+ todo
+ else
+ todo @ [e]
+ end
+
+ and visit_desc d todo is_son nesting =
+ match d with
+ | Dlevels [] -> todo
+ | Dlevels [lev] -> visit_level lev todo is_son nesting
+ | Dlevels (lev::levels) ->
+ let todo = visit_level lev todo is_son nesting in
+ List.fold_left
+ (fun acc l ->
+ Format.fprintf fmt "@ | ";
+ visit_level l acc is_son nesting)
+ todo levels;
+ | _ -> todo
+
+ and visit_level l todo is_son nesting =
+ let { lsuffix = suff ; lprefix = pref } = l in
+ let todo = visit_tree suff todo is_son nesting in
+ visit_tree pref todo is_son nesting
+
+ and visit_tree t todo is_son nesting =
+ match t with
+ | Node node -> visit_node node todo is_son nesting
+ | _ -> todo
+
+ and visit_node n todo is_son nesting =
+ let is_tree_printable t =
+ match t with
+ | Node _ -> true
+ | _ -> false
+ in
+ let needs_brackets t =
+ let rec count_brothers = function
+ | Node {brother = brother} -> 1 + count_brothers brother
+ | _ -> 0
+ in
+ count_brothers t > 1
+ in
+ let { node = symbol; son = son ; brother = brother } = n in
+ let todo = visit_symbol symbol todo is_son nesting in
+ let todo =
+ if is_tree_printable son then
+ begin
+ let need_b = needs_brackets son in
+ if not is_son then
+ Format.fprintf fmt "@[<hov2>";
+ if need_b then
+ Format.fprintf fmt "( ";
+ let todo = visit_tree son todo true nesting in
+ if need_b then
+ Format.fprintf fmt ")";
+ if not is_son then
+ Format.fprintf fmt "@]";
+ todo
+ end
+ else
+ todo
+ in
+ if is_tree_printable brother then
+ begin
+ Format.fprintf fmt "@ | ";
+ visit_tree brother todo is_son nesting
+ end
+ else
+ todo
+
+ and visit_symbol s todo is_son nesting =
+ 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 nesting in
+ if is_son then
+ Format.fprintf fmt "@ ";
+ todo)
+ todo sl
+ | Snterm entry -> visit_entry entry todo is_son nesting
+ | Snterml (entry,_) -> visit_entry entry todo is_son nesting
+ | Slist0 symbol ->
+ Format.fprintf fmt "@[<hov2>{ ";
+ let todo = visit_symbol symbol todo is_son (nesting+1) in
+ Format.fprintf fmt "}@] @ ";
+ todo
+ | Slist0sep (symbol,sep) ->
+ Format.fprintf fmt "@[<hov2>[ ";
+ let todo = visit_symbol symbol todo is_son (nesting + 1) in
+ Format.fprintf fmt "@[<hov2>{ ";
+ let todo = visit_symbol sep todo is_son (nesting + 2) in
+ Format.fprintf fmt " ";
+ let todo = visit_symbol symbol todo is_son (nesting + 2) in
+ Format.fprintf fmt "}@] @ ]@] @ ";
+ todo
+ | Slist1 symbol ->
+ Format.fprintf fmt "@[<hov2>{ ";
+ let todo = visit_symbol symbol todo is_son (nesting + 1) in
+ Format.fprintf fmt "}+@] @ ";
+ todo
+ | Slist1sep (symbol,sep) ->
+ let todo = visit_symbol symbol todo is_son nesting in
+ Format.fprintf fmt " @[<hov2>{ ";
+ let todo = visit_symbol sep todo is_son (nesting + 1) in
+ let todo = visit_symbol symbol todo is_son (nesting + 1) in
+ Format.fprintf fmt "}@] @ ";
+ todo
+ | Sopt symbol ->
+ Format.fprintf fmt "@[<hov2>[ ";
+ let todo = visit_symbol symbol todo is_son (nesting + 1) in
+ Format.fprintf fmt "]@] @ ";
+ todo
+ | Sself -> Format.fprintf fmt "self "; todo
+ | Snext -> Format.fprintf fmt "next "; todo
+ | Stoken pattern ->
+ let constructor, keyword = pattern in
+ if keyword = "" then
+ Format.fprintf fmt "'%s' " constructor
+ else
+ Format.fprintf fmt "\"%s\" " (tex_of_unicode keyword);
+ todo
+ | Stree tree -> visit_tree tree todo is_son nesting
+ in
+ visit_desc desc [] false 0
+;;
+
+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} when
+ is_symbol_dummy node &&
+ is_tree_dummy son &&
+ is_tree_dummy brother -> DeadEnd
+ | x -> Node x
+
+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 -> false
+ | Snext -> true
+ | Stree t -> is_tree_dummy t
+
+and is_tree_dummy = function
+ | Node {node=node} -> is_symbol_dummy node
+ | _ -> true
+;;
+
+
+let rec visit_entries todo pped =
+ let fmt = Format.std_formatter in
+ 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 "@[<hv2>%s ::=@ " ename;
+ let desc = clean_dummy_desc desc in
+ let todo = visit_description desc fmt @ todo in
+ Format.fprintf fmt "@]";
+ Format.pp_print_newline fmt ();
+ Format.pp_print_newline fmt ();
+ 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 todo pped
+;;
+
+let _ =
+(* let g_entry = Grammar.Entry.obj CicNotationParser.term in*)
+ let g_entry = Grammar.Entry.obj GrafiteParser.statement in
+ visit_entries [g_entry] []
projects / helm.git / commitdiff