(*
    ||M||  This file is part of HELM, an Hypertextual, Electronic        
    ||A||  Library of Mathematics, developed at the Computer Science     
    ||T||  Department, University of Bologna, Italy.                     
    ||I||                                                                
    ||T||  HELM is free software; you can redistribute it and/or         
    ||A||  modify it under the terms of the GNU General Public License   
    \   /  version 2 or (at your option) any later version.              
     \ /   This software is distributed as is, NO WARRANTY.              
      V_______________________________________________________________ *)

module F = Format
module U = NUri
module M = Meta

type counters = {
   eabsts: int;
   eabbrs: int;
   pabsts: int;    
   tsorts: int;
   tlrefs: int;
   tgrefs: int;
   pappls: int;
   tappls: int;
   tabsts: int;
}

let initial_counters = {
   eabsts = 0; eabbrs = 0; pabsts = 0; pappls = 0;
   tsorts = 0; tlrefs = 0; tgrefs = 0; tappls = 0; tabsts = 0
}

let rec count_term f c = function
   | M.Sort _          -> 
      f {c with tsorts = succ c.tsorts}
   | M.LRef _          -> 
      f {c with tlrefs = succ c.tlrefs}
   | M.GRef (_, _, ts) -> 
      let c = {c with tgrefs = succ c.tgrefs} in
      let c = {c with pappls = c.pappls + List.length ts} in
      Cps.list_fold_left f count_term c ts
   | M.Appl (v, t)     -> 
      let c = {c with tappls = succ c.tappls} in
      let f c = count_term f c t in
      count_term f c v
   | M.Abst (_, w, t)  -> 
      let c = {c with tabsts = succ c.tabsts} in
      let f c = count_term f c t in
      count_term f c w

let count_par f c (_, w) = count_term f c w

let count_entry f c = function
   | _, pars, _, w, None        ->
      let c = {c with eabsts = succ c.eabsts} in
      let c = {c with pabsts = c.pabsts + List.length pars} in
      let f c = count_term f c w in
      Cps.list_fold_left f count_par c pars   
   | _, pars, _, w, Some (_, v) ->
      let c = {c with eabbrs = succ c.eabbrs} in
      let c = {c with pabsts = c.pabsts + List.length pars} in
      let f c = count_term f c v in
      let f c = count_term f c w in
      Cps.list_fold_left f count_par c pars

let count_item f c = function
   | Some e -> count_entry f c e
   | None   -> f c

let print_counters f c =
   let terms = c.tsorts + c.tgrefs + c.tgrefs + c.tappls + c.tabsts in
   let pars = c.pabsts + c.pappls in
   let items = c.eabsts + c.eabbrs in
   Printf.printf "  Intermediate representation summary\n";
   Printf.printf "    Total entry items:        %6u\n" items;
   Printf.printf "      Declaration items:      %6u\n" c.eabsts;
   Printf.printf "      Definition items:       %6u\n" c.eabbrs;
   Printf.printf "    Total parameter items:    %6u\n" pars;
   Printf.printf "      Application items:      %6u\n" c.pappls;
   Printf.printf "      Abstraction items:      %6u\n" c.pabsts;
   Printf.printf "    Total term items:         %6u\n" terms;
   Printf.printf "      Sort items:             %6u\n" c.tsorts;
   Printf.printf "      Local reference items:  %6u\n" c.tlrefs;
   Printf.printf "      Global reference items: %6u\n" c.tgrefs;
   Printf.printf "      Application items:      %6u\n" c.tappls;
   Printf.printf "      Abstraction items:      %6u\n" c.tabsts;
   flush stdout; f ()

let string_of_sort = function
   | true -> "Type"
   | false -> "Prop"

let string_of_transparent = function
   | true  -> "="
   | false -> "~"

let pp_list pp opend sep closed frm l =
   let rec aux frm = function
      | []       -> ()
      | [hd]     -> pp frm hd
      | hd :: tl -> F.fprintf frm "%a%s%a" pp hd sep aux tl 
   in
   if l = [] then () else F.fprintf frm "%s%a%s" opend aux l closed

let rec pp_args frm args = pp_list pp_term "(" "," ")" frm args

and pp_term frm = function
   | M.Sort s            -> 
      F.fprintf frm "@[*%s@]" (string_of_sort s)
   | M.LRef (l, i)       ->
      F.fprintf frm "@[%u@@#%u@]" l i
   | M.GRef (l, uri, ts) ->
      F.fprintf frm "@[%u@@$%s%a@]" l (U.string_of_uri uri) pp_args ts
   | M.Appl (v, t)       ->
      F.fprintf frm "@[(%a).%a@]" pp_term v pp_term t
   | M.Abst (id, w, t)   ->
      F.fprintf frm "@[[%s:%a].%a@]" id pp_term w pp_term t

let pp_par frm (id, w) =
    F.fprintf frm "%s:%a" id pp_term w

let pp_pars = pp_list pp_par "[" "," "]"

let pp_body frm = function
   | None            -> ()
   | Some (trans, t) ->
      F.fprintf frm "%s%a" (string_of_transparent trans) pp_term t

let pp_entry frm (l, pars, uri, u, body) =
   F.fprintf frm "@[%u@@%s%a%a:%a@]@\n%!" 
      l (U.string_of_uri uri) pp_pars pars pp_body body pp_term u

let pp_item f frm = function 
   | Some entry -> pp_entry frm entry; f ()
   | None       -> f ()