+++ /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 contractions = ("\\Longrightarrow","=>") :: [] in
- if String.length s <= 1 then s
- else (* probably an extended unicode symbol *)
- let s = Utf8Macro.tex_of_unicode s in
- try List.assoc s contractions with Not_found -> s
-
-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 = 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 { 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 "%s " 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 ->
- if needs_brackets tree then
- begin
- Format.fprintf fmt "@[<hov2>( ";
- let todo = visit_tree tree todo is_son (nesting + 1) in
- Format.fprintf fmt ")@] @ ";
- todo
- end
- else
- visit_tree tree todo is_son (nesting + 1)
- 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} ->
- 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
-
-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 ename @ 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 GrafiteParser.statement in
- visit_entries [g_entry] []