(* 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] []