(* 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 CE = Content_expressions;;

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

let maxsize = 25;;

let rec countterm current_size t =
  if current_size > maxsize then current_size 
  else match t with
    CE.Symbol (_,name,None,_) -> current_size + (String.length name)
  | CE.Symbol (_,name,Some subst,_) -> 
      let c1 = current_size + (String.length name) in 
      countsubst subst c1
  | CE.LocalVar (_,name) -> current_size + (String.length name)
  | CE.Meta (_,name,l) ->
     List.fold_left
      (fun i t ->
        match t with
           None -> i
         | Some t' -> countterm i t'
      ) (current_size + String.length name) l
  | CE.Num (_,value) -> current_size + (String.length value)
  | CE.Appl (_,l) -> 
      List.fold_left countterm current_size l
  | CE.Binder (_, _,(n,s),body) -> 
      let cs = countterm (current_size + 2 + (String.length n)) s in
      countterm cs body
  | CE.Letin (_,(n,s),body) ->
      let cs = countterm (current_size + 3 + (String.length n)) s in
      countterm cs body
  | CE.Letrec (_,defs,body) ->
      let cs = 
        List.fold_left 
          (fun c (n,bo) -> countterm (c+(String.length n)) bo) current_size defs in
      countterm cs body
  | CE.Case (_,a,np) ->
      let cs = countterm (current_size + 4) a in
      List.fold_left 
        (fun c (n,bo) -> countterm (c+(String.length n)) bo) current_size np

and
countsubst subst current_size =
    List.fold_left 
      (fun current_size (uri,expr) ->
         if (current_size > maxsize) then current_size
         else 
           let c1 = 
             (current_size + (String.length (UriManager.name_of_uri uri))) in
           (countterm c1 expr)) current_size subst
;;

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

let rec make_attributes l1 =
  function
      [] -> []
    | None::tl -> make_attributes (List.tl l1) tl
    | (Some s)::tl ->
       let p,n = List.hd l1 in
        (p,n,s)::(make_attributes (List.tl l1) tl)
;;

let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t =
  let module CE = Content_expressions in
  let module P = Mpresentation in
  let rec aux =
  function
      CE.Symbol (xref,name,None,uri) -> 
        let attr = 
         make_attributes 
          [Some "helm","xref";Some "xlink","href"] [xref;uri] in
        if tail = [] then
          P.Mi (attr,name)
        else P.Mrow([],P.Mi (attr,name)::tail)
    | CE.Symbol (xref,name,Some subst,uri) ->
        let attr = 
         make_attributes 
          [Some "helm","xref";Some "xlink","href"] [xref;uri] in
        let rec make_subst =
          (function 
               [] -> assert false
             | [(uri,a)] -> 
                 [(aux a);
                  P.Mtext([],"/");
                  P.Mi([],UriManager.name_of_uri uri)]
             | (uri,a)::tl -> 
                 (aux a)::
                 P.Mtext([],"/")::
                 P.Mi([],UriManager.name_of_uri uri)::
                 P.Mtext([],"; ")::
                 P.smallskip::
                 (make_subst tl)) in
        P.Mrow ([],
          P.Mi (attr,name)::
          P.Mtext([],"[")::
          (make_subst subst)@
          (P.Mtext([],"]")::tail))
    | CE.LocalVar (xref,name) -> 
        let attr = make_attributes [Some "helm","xref"] [xref] in
        if tail = [] then
          P.Mi (attr,name)
        else P.Mrow([],P.Mi (attr,name)::tail)
    | CE.Meta (xref,name,l) ->
        let attr = make_attributes [Some "helm","xref"] [xref] in
        let l' =
         List.map
          (function
              None -> P.Mo([],"_")
            | Some t -> cexpr2pres t
          ) l
        in
         if tail = [] then
           P.Mrow ([],P.Mi (attr,name) :: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")])
         else
           P.Mrow
            ([],P.Mi (attr,name):: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")] @ tail)
    | CE.Num (xref,value) -> 
        let attr = make_attributes [Some "helm","xref"] [xref] in
        if tail = [] then
          P.Mn (attr,value)
        else P.Mrow([],P.Mn (attr,value)::tail)
    | CE.Appl (axref,CE.Symbol(sxref,n,subst,uri)::tl) ->
        let aattr = make_attributes [Some "helm","xref"] [axref] in
        let sattr = make_attributes [Some "helm","xref";Some "xlink","href"] [sxref;uri] in
        (try 
          (let f = Hashtbl.find symbol_table n in
           f tl ~priority ~assoc ~tail aattr sattr)
        with notfound ->
           P.Mrow(aattr,
           P.Mo([],"(")::P.Mi(sattr,n)::(make_args tl)@(P.Mo([],")")::tail)))
    | CE.Appl (xref,l) as t ->
        let attr = make_attributes [Some"helm","xref"] [xref] in
        P.Mrow(attr,
           P.Mo([],"(")::(make_args l)@(P.Mo([],")")::tail))
    | CE.Binder (xref, kind,(n,s),body) ->
        let attr = make_attributes [Some "helm","xref"] [xref] in
        let binder = 
          if kind = "Lambda" then 
             Netconversion.ustring_of_uchar `Enc_utf8 0x03bb
          else if kind = "Prod" then
             Netconversion.ustring_of_uchar `Enc_utf8 0x03a0
          else if kind = "Forall" then
             Netconversion.ustring_of_uchar `Enc_utf8 0x2200
          else if kind = "Exists" then
             Netconversion.ustring_of_uchar `Enc_utf8 0x2203
          else "unknown" in
        P.Mrow (attr, 
           P.Mtext([None,"mathcolor","Blue"],binder)::
           P.Mtext([],n ^ ":")::
           (aux s)::
           P.Mo([],".")::
           (aux body)::tail)
    | CE.Letin (xref,(n,s),body) ->
        let attr = make_attributes [Some "helm","xref"] [xref] in
        P.Mrow (attr, 
           P.Mtext([],("let "))::
           P.Mtext([],(n ^ "="))::
           (aux s)::
           P.Mtext([]," in ")::
           (aux body)::tail)
    | CE.Letrec (xref,defs,body) ->
        let attr = make_attributes [Some "helm","xref"] [xref] in
        let rec make_defs =
          (function 
               [] -> assert false
             | [(n,bo)] -> 
                 [P.Mtext([],(n ^ "="));(aux body)]
             | (n,bo)::tl -> 
                 P.Mtext([],(n ^ "="))::
                 (aux body)::P.Mtext([]," and")::(make_defs tl)) in
        P.Mrow (attr,  
          P.Mtext([],("let rec "))::
          (make_defs defs)@
           (P.Mtext([]," in ")::
           (aux body)::tail))
    | CE.Case (xref,a,np) ->
        let attr = make_attributes [Some "helm","xref"] [xref] in
        let rec make_patterns =
          (function 
               [] -> []
             | [(n,p)] -> make_pattern n p
             | (n,p)::tl -> 
                 (make_pattern n p)@(P.smallskip::
                 P.Mtext([],"|")::P.smallskip::(make_patterns tl)))
        and make_pattern n p =           
          let rec get_vars_and_body = 
            (function
                CE.Binder (_, "Lambda",(n,_),body) ->
                  let v,b = get_vars_and_body body in
                  n::v,b 
              | t -> [],t) in
          let vars,body = get_vars_and_body p in
          let lhs = 
            match vars with 
	        [] -> n ^ " -> "
              | l -> "(" ^ n ^" "^(String.concat " " l) ^ ")" ^ " -> " in
          [P.Mtext([],lhs);P.smallskip;aux body] in
        P.Mrow (attr,  
          P.Mtext([],"match")::P.smallskip::
          (aux a)::P.smallskip::
          P.Mtext([],"with")::P.smallskip::
          P.Mtext([],"[")::P.smallskip::
          (make_patterns np)@(P.smallskip::P.Mtext([],("]"))::tail))  in
  aux t

and

make_args ?(priority = 0) ?(assoc = false) ?(tail = []) =
  let module P = Mpresentation in
  function
      [] -> tail
    | a::tl -> P.smallskip::(cexpr2pres a)::(make_args ~tail:tail tl)
;;

let rec make_args_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) =
  let module P = Mpresentation in 
  function
    [] -> []
  | [a] -> 
      [P.Mtr([],[P.Mtd([],P.indented (cexpr2pres_charcount ~tail:tail a))])]
  | (a::tl) as l ->
      let c = List.fold_left countterm 0 l in
      if c > maxsize then
        P.Mtr([],[P.Mtd([],P.indented (cexpr2pres_charcount a))])::
        (make_args_charcount ~tail:tail tl)
      else [P.Mtr([],[P.Mtd([],P.Mrow([],(P.Mspace([None,"width","0.2cm"]))::(make_args ~tail:tail l)))])]

(* 
  function 
      [] -> []
    | a::tl -> 
        let tlpres = 
          let c = List.fold_left countterm 0 tl in
          if c > maxsize then
            P.Mtable ([("align","baseline 1");("equalrows","false");
             ("columnalign","left")],
              (make_args_charcount tl))
          else 
            P.Mrow([], make_args tl) in
        [P.Mtr([],[P.Mtd([],(cexpr2pres_charcount a))]);
         P.Mtr([],[P.Mtd([],P.indented tlpres)])] *)
and  

cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t =
  if not(is_big t) then (cexpr2pres ~priority ~assoc ~tail t) 
  else let aux = cexpr2pres_charcount in
  match t with
      CE.Symbol (xref,name,None,uri) -> 
        let attr = 
         make_attributes 
          [Some "helm","xref";Some "xlink","href"] [xref;uri] in
        if tail = [] then
          P.Mi (attr,name)
        else P.Mrow ([],P.Mi (attr,name)::tail)
    | CE.Symbol (xref,name,Some subst,uri) ->
        let attr = 
         make_attributes 
          [Some "helm","xref";Some "xlink","href"] [xref;uri] in
        let rec make_subst =
          (function 
               [] -> assert false
             | [(uri,a)] -> 
                 [(cexpr2pres a);
                  P.Mtext([],"/");
                  P.Mi([],UriManager.name_of_uri uri)]
             | (uri,a)::tl -> 
                 (cexpr2pres a)::
                 P.Mtext([],"/")::
                 P.Mi([],UriManager.name_of_uri uri)::
                 P.Mtext([],"; ")::
                 P.smallskip::
                 (make_subst tl)) in
        P.Mrow ([],
          P.Mi (attr,name)::
          P.Mtext([],"[")::
          (make_subst subst)@
          (P.Mtext([],"]")::tail))
    | CE.LocalVar (xref,name) -> 
        let attr = make_attributes [Some "helm","xref"] [xref] in
        if tail = [] then
          P.Mi (attr,name)
        else P.Mrow ([],P.Mi (attr,name)::tail)
    | CE.Meta (xref,name,l) ->
        let attr = make_attributes [Some "helm","xref"] [xref] in
        let l' =
         List.map
          (function
              None -> P.Mo([],"_")
            | Some t -> cexpr2pres t
          ) l
        in
         if tail = [] then
           P.Mrow ([],P.Mi (attr,name) :: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")])
         else
           P.Mrow
            ([],P.Mi (attr,name):: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")] @ tail)
    | CE.Num (xref,value) -> 
        let attr = make_attributes [Some "helm","xref"] [xref] in
        if tail = [] then
          P.Mn (attr,value)
        else P.Mrow ([],P.Mn (attr,value)::tail)
    | CE.Appl (axref,CE.Symbol(sxref,n,subst,uri)::tl) ->
        let aattr = make_attributes [Some "helm","xref"] [axref] in
        let sattr = make_attributes [Some "helm","xref";Some "xlink","href"] [sxref;uri] in
        (try 
          (let f = Hashtbl.find symbol_table_charcount n in
           f tl ~priority ~assoc ~tail aattr sattr)
         with notfound ->
          P.Mtable (aattr@P.standard_tbl_attr,
            P.Mtr([],[P.Mtd([],P.Mrow([],
              [P.Mtext([],"(");
               cexpr2pres (CE.Symbol(sxref,n,subst,uri))]))])::
            make_args_charcount ~tail:(P.Mtext([],")")::tail) tl))
    | CE.Appl (xref,l) as t ->
        let attr = make_attributes [Some "helm","xref"] [xref] in
        P.Mtable (attr@P.standard_tbl_attr,
          P.Mtr([],[P.Mtd([],P.Mrow([],
            [P.Mtext([],"(");
             cexpr2pres_charcount (List.hd l)]))])::
          make_args_charcount ~tail:(P.Mtext([],")")::tail) (List.tl l))
    | CE.Binder (xref, kind,(n,s),body) as t ->
        let attr = make_attributes [Some "helm","xref"] [xref] in
        let binder = 
          if kind = "Lambda" then 
            Netconversion.ustring_of_uchar `Enc_utf8 0x03bb  
          else if kind = "Prod" then
            Netconversion.ustring_of_uchar `Enc_utf8 0x03a0
          else if kind = "Forall" then
            Netconversion.ustring_of_uchar `Enc_utf8 0x2200
          else if kind = "Exists" then
            Netconversion.ustring_of_uchar `Enc_utf8 0x2203
          else "unknown" in  
        P.Mtable (attr@P.standard_tbl_attr,
           [P.Mtr ([],[P.Mtd ([],
             P.Mrow([],
              [P.Mtext([None,"mathcolor","Blue"],binder);
               P.Mtext([],n ^ ":");
               cexpr2pres_charcount s ~tail:[P.Mtext([],".")]]))]);
            P.Mtr ([],[P.Mtd ([],
             P.indented (cexpr2pres_charcount body ~tail:tail))])]) 
    | CE.Letin (xref,(n,s),body) as t ->
        let attr = make_attributes [Some "helm","xref"] [xref] in
        P.Mtable (attr@P.standard_tbl_attr,
           [P.Mtr ([],[P.Mtd ([],
             P.Mrow([],
              [P.Mtext([None,"mathcolor","Blue"],"let");
               P.smallskip;
               P.Mtext([],n ^ "=");
               cexpr2pres_charcount s;
               P.smallskip;
               P.Mtext([],"in");
              ]))]);
            P.Mtr ([],[P.Mtd ([],
             P.indented (cexpr2pres_charcount body))])])
    | CE.Letrec (xref,defs,body) ->
        let attr = make_attributes [Some "helm","xref"] [xref] in
        let rec make_defs =
          (function 
               [] -> assert false
             | [(n,bo)] -> 
                 [P.Mtext([],(n ^ "="));(aux body)]
             | (n,bo)::tl -> 
                 P.Mtext([],(n ^ "="))::
                 (aux body)::P.Mtext([]," and")::(make_defs tl)) in
        P.Mrow (attr,  
          P.Mtext([],("let rec "))::
          (make_defs defs)@
          [P.Mtext([]," in ");
           (aux body)])
    | CE.Case (xref,a,np) ->
        let attr = make_attributes [Some "helm","xref"] [xref] in
        let arg = 
          if (is_big a) then
            let tail = P.Mtext([],(" with"))::tail in
            [P.Mtr ([],[P.Mtd ([],P.Mtext([],("match ")))]);
             P.Mtr ([],[P.Mtd ([],aux a ~tail:tail)])]
          else 
            [P.Mtr ([],[P.Mtd ([],P.Mrow([],[P.Mtext([],("match"));P.smallskip;aux a ~tail:tail; P.smallskip;P.Mtext([],("with"))]))])] in
        let rec make_patterns is_first ~tail =
          function 
              [] -> []
            | [(n,p)] ->
                let sep = 
                  if is_first then "[ " else "| " in
                [P.Mtr ([],
                  [P.Mtd ([],
                     make_pattern sep ~tail n p)])]
            | (n,p)::tl -> 
                let sep = 
                  if is_first then "[ " else "| " in
                P.Mtr ([],
                  [P.Mtd ([],
                    make_pattern sep [] n p)])
                ::(make_patterns false ~tail  tl)
        and make_pattern sep ~tail n p =
          let rec get_vars_and_body = 
            function
                CE.Binder (_, "Lambda",(n,_),body) ->
                  let v,b = get_vars_and_body body in
                  n::v,b 
              | t -> [],t in
          let vars,body = get_vars_and_body p in
          let lhs = 
            match vars with 
	        [] -> sep ^ n ^ " -> "
              | l -> sep ^"(" ^n^" "^(String.concat " " l) ^ ")" ^ " -> " in
          if (is_big body) then
            P.Mtable (P.standard_tbl_attr,
              [P.Mtr ([],
                [P.Mtd ([],P.Mtext([],lhs))]);
               P.Mtr ([],
                [P.Mtd ([],P.indented (aux ~tail body ))])])
          else
            P.Mrow([],[P.Mtext([],lhs);aux ~tail body]) in
        let patterns =
          make_patterns true np ~tail:(P.Mtext([],"]")::tail) in 
        P.Mtable (attr@P.standard_tbl_attr,
          arg@patterns)
;;