(* Copyright (C) 2000, 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://cs.unibo.it/helm/.
 *)

(**************************************************************************)
(*                                                                        *)
(*                           PROJECT HELM                                 *)
(*                                                                        *)
(*                Andrea Asperti <asperti@cs.unibo.it>                    *)
(*                             28/6/2003                                   *)
(*                                                                        *)
(**************************************************************************)

module P = Mpresentation;;
module A = CicAst;;

let symbol_table = Hashtbl.create 503;;
let symbol_table_charcount = Hashtbl.create 503;;

let maxsize = 25;;

let rec countvar current_size = function
    (Cic.Anonymous, None) -> current_size + 1 (* underscore *)
  | (Cic.Anonymous, Some ty) -> countterm current_size ty
  | (Cic.Name s, None) -> current_size + String.length s
  | (Cic.Name s, Some ty) -> current_size + countterm current_size ty

and countterm current_size t =
  if current_size > maxsize then current_size 
  else match t with
      A.AttributedTerm (_,t) -> countterm current_size t
    | A.Appl l -> 
        List.fold_left countterm current_size l
    | A.Binder (_,var,body) -> 
        let varsize = countvar current_size var in
        countterm (varsize + 1) body (* binder *)
    | A.Case (arg, _, ty, pl) ->
        let size1 = countterm (current_size+10) arg in (* match with *)
        let size2 =
          match ty with
              None -> size1
            | Some ty -> countterm size1 ty in
        List.fold_left 
          (fun c ((constr,vars),action) ->
             let size3 =
               List.fold_left countvar (c+String.length constr) vars in
             countterm size3 action) size2 pl 
    | A.LetIn (var,s,t) ->
        let size1 = countvar current_size var in
        let size2 = countterm size1 s in
        countterm size2 t
    | A.LetRec (_,l,t) ->
        let size1 =
          List.fold_left
            (fun c (var,s,_) -> 
               let size1 = countvar c var in
               countterm size1 s) current_size l in
	  countterm size1 t
    | A.Ident(s,l) ->
        List.fold_left 
	  (fun c (v,t) -> countterm (c + (String.length v)) t) 
          (current_size + (String.length s)) l
    | A.Implicit -> current_size + 1 (* underscore *)
    | A.Meta (_,l) ->
	List.fold_left 
	  (fun c t -> 
             match t with
		 None -> c + 1 (* underscore *)
	       | Some t -> countterm c t)
          (current_size + 1) l (* num *)
    | A.Num (s, _) -> current_size + String.length s
    | A.Sort _ -> current_size + 4 (* sort name *)
    | A.Symbol (s,_) -> current_size + String.length s
;;

let is_big t = 
  ((countterm 0 t) > maxsize)
;;

let map_attribute =
  function
      `Loc (n,m) -> 
        (Some "helm","loc",(string_of_int n)^" "^(string_of_int m))
    | `IdRef s -> 
	(Some "helm","xref",s)
;;

let map_attributes = List.map map_attribute
;;
let resolve_binder = function
    `Lambda -> Box.Text([],"\\lambda")
  | `Pi -> Box.Text([],"\\Pi")
  | `Exists -> Box.Text([],"\\exists")
  | `Forall -> Box.Text([],"\\forall")

let rec ast2box ?(priority = 0) ?(assoc = false) ?(attr = []) t =
  if is_big t then 
    bigast2box ~priority ~assoc ~attr t 
  else Box.Object (map_attributes attr, t)
and bigast2box ?(priority = 0) ?(assoc = false) ?(attr = []) =
  function
      A.AttributedTerm (attr1, t) -> 
        (* attr should be empty, since AtrtributedTerm are not
           supposed to be directly nested *)
	bigast2box ~priority ~assoc ~attr:(attr1::~attr) t 
    | A.Appl l ->
	Box.H 
          (map_attributes attr, 
	   [Box.Text([],"(");
            Box.V([],List.map ast2box l);
            Box.Text([],")")])
    | A.Binder(kind, var, body) ->
	Box.V(map_attributes attr,
	      [Box.H([],[resolve_binder kind;
			 Box.smallskip;
			 make_var var;
			 Box.Text([],".")]);
	       Box.indent (ast2box body)])
    | A.Case(arg, _, ty, pl) ->
	let make_rule sep ((constr,vars),rhs) =
	  if (is_big rhs) then
	    Box.V([],[Box.H([],[Box.Text([],sep);
			        Box.smallskip; 
		 		make_pattern constr vars;
				Box.smallskip; 
				Box.Text([],"->")]);
		      Box.indent (bigast2box rhs)])
	  else
	    Box.H([],[Box.Text([],sep);
		      Box.smallskip; 
		      make_pattern constr vars;
		      Box.smallskip; 
		      Box.Text([],"->");
		      Box.smallskip; 
		      Box.Object([],rhs)]) in
	let plbox = match pl with
	    [] -> Box.Text([],"[]")
	  | r::tl -> 
	      Box.H([],
		    [Box.V([], 
			   (make_rule "[" r)::(List.map (make_rule "|") tl));
		     Box.Text([],"]")]) in
	if is_big arg then
	  Box.V(map_attributes attr,
		[Box.Text([],"match");
		 Box.H([],[Box.skip;
			   bigast2box arg;
			   Box.smallskip;
			   Box.Text([],"with")]);
		 plbox])
	else
	  Box.V(map_attributes attr,
		[Box.H(map_attributes attr,
		       [Box.Text([],"match");
			Box.smallskip;
			ast2box arg;
			Box.smallskip;
			Box.Text([],"with")]);
		 plbox])
    | A.LetIn (var, s, t) ->
	Box.V(map_attributes attr,
	      (make_def "let" var s "in")@[ast2box t])
    | A.LetRec (_, vars, body) ->
	let definitions =
	  let rec make_defs let_txt = function
	      [] -> []
	    | [(var,s,_)] -> 
		make_def let_txt var s "in"
	    | (var,s,_)::tl ->
		(make_def let_txt var s "")@(make_defs "and" tl) in
	  make_defs "let rec" vars in
	Box.V(map_attributes attr,
	      definitions@[ast2box body])
    | A.Ident (s, subst) ->
	let subst =
	  let rec make_substs start_txt = 
	    function
	      [] -> []
	    | [(s,t)] -> 
		make_subst start_txt s t "]"
	    | (s,t)::tl ->
		(make_subst start_txt s t ";")@(make_substs " " tl) in
	  make_substs "[" subst in
	Box.V([], (* attr here or on Vbox? *)
	      [Box.Text(map_attributes attr,s);
	       Box.indent(Box.V([],subst))])
    | A.Implicit -> 
	Box.Text([],"_") (* big? *)
    | A.Meta (n, l) ->
	let local_context =
	  List.map 
	    (function t -> 
	       Box.H([],[aux_option t; Box.Text([],";")])) 
	    l in
	Box.V(map_attributes attr,
	      [Box.Text([],"?"^(string_of_int n));
	       Box.H([],[Box.Text([],"[");
			 Box.V([],local_context);
			 Box.Text([],"]")])])
    | A.Num (s, _) -> 
	 Box.Text([],s)
    | A.Sort kind ->
	(match kind with 
	     `Prop -> Box.Text([],"Prop")
	   | `Set -> Box.Text([],"Set")
	   | `Type -> Box.Text([],"Type")   
	   | `CProp -> Box.Text([],"CProp"))    
    | A.Symbol (s, _) -> 
	Box.Text([],s)

and aux_option = function
    None  -> Box.Text([],"_")
  | Some ast -> ast2box ast 

and make_var = function
    (Cic.Anonymous, None) -> Box.Text([],"_:_")
  | (Cic.Anonymous, Some t) -> 
      Box.H([],[Box.Text([],"_:");ast2box t])
  | (Cic.Name s, None) -> Box.Text([],s)
  | (Cic.Name s, Some t) ->
      if is_big t then
	Box.V([],[Box.Text([],s^":");
		  Box.indent(bigast2box t)])
      else
	Box.H([],[Box.Text([],s^":");Box.Object([],t)])

and make_pattern constr = 
  function
      [] -> Box.Text([],constr)
    | vars -> 
	let bvars =
	  List.fold_right 
	    (fun var acc -> 
	       let bv = 
		 match var with
		     (* ignoring the type *)
		     (Cic.Anonymous, _) -> Box.Text([],"_")
		   | (Cic.Name s, _) -> Box.Text([],s) in
		 Box.Text([]," ")::bv::acc) vars [Box.Text([],")")] in
	  Box.H([],Box.Text([],"(")::Box.Text([],constr)::bvars)
    

and make_def let_txt var def end_txt =
  let name = 
    (match var with
         (* ignoring the type *)
	 (Cic.Anonymous, _) -> Box.Text([],"_") 
       | (Cic.Name s, _) -> Box.Text([],s)) in
  pretty_append 
    [Box.Text([],let_txt);
     Box.smallskip;
     name;
     Box.smallskip;
     Box.Text([],"=")
    ]
    def 
    [Box.smallskip;Box.Text([],end_txt)] 

and make_subst start_txt varname body end_txt =
  pretty_append 
    [Box.Text([],start_txt);
     Box.Text([],varname);
     Box.smallskip;
     Box.Text([],":=")
    ]
    body
    [Box.Text([],end_txt)] 
	  
and pretty_append l ast tail =
  if is_big ast then
    [Box.H([],l);
     Box.H([],Box.skip::(bigast2box ast)::tail)]
  else
    [Box.H([],l@(Box.smallskip::(ast2box ast)::tail))]

;;