(*
    ||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 U  = NUri
module C  = Cps
module G  = Options
module H  = Hierarchy
module E  = Entity
module T  = Txt
module TT = TxtTxt
module D  = Crg

type status = {
   path  : T.id list;      (* current section path *)
   line  : int;            (* line number *)
   sort  : int;            (* first default sort index *)
   mk_uri: G.uri_generator (* uri generator *) 
}

let henv_size = 7000 (* hash tables initial size *)

let henv = Hashtbl.create henv_size (* optimized global environment *)

(* Internal functions *******************************************************)
(*
let name_of_id ?(r=true) id = E.Name (id, r)

let mk_lref f i j k = f (D.TLRef ([E.Apix k], i, j))

let mk_gref f uri = f (D.TGRef ([], uri))

let uri_of_id st id path =
   let str = String.concat "/" path in
   let str = Filename.concat str id in 
   let str = st.mk_uri str in
   U.uri_of_string str

let resolve_gref err f st id =
   try f (Hashtbl.find henv id)
   with Not_found -> err ()

let rec xlate_term f st lenv = function
   | T.Inst _
   | T.Impl _         -> assert false
   | T.Sort h         -> 
      f (D.TSort ([], h))
   | T.NSrt id        -> 
      let f h = f (D.TSort ([], h)) in
      H.sort_of_string C.err f id
   | T.LRef (i, j)    ->    
      D.get_index C.err (mk_lref f i j) i j lenv
   | T.NRef id        ->
      let err () = resolve_gref C.err (mk_gref f) st id in
      D.resolve_lref err (mk_lref f) id lenv
   | T.Cast (u, t)    ->
      let f uu tt = f (D.TCast ([], uu, tt)) in
      let f uu = xlate_term (f uu) st lenv t in
      xlate_term f st lenv u
   | T.Appl (vs, t)   ->
      let map f = xlate_term f st lenv in
      let f vvs tt = f (D.TAppl ([], vvs, tt)) in
      let f vvs = xlate_term (f vvs) st lenv t in
      C.list_map f map vs
   | T.Bind (n, b, t) ->
      let abst_map (lenv, a, wws) (id, r, w) = 
         let attr = name_of_id ~r id in
	 let ww = xlate_term C.start st lenv w in
	 D.push2 C.err C.start lenv ~attr ~t:ww (), attr :: a, ww :: wws
      in
      let abbr_map (lenv, a, wws) (id, w) = 
         let attr = name_of_id id in
	 let ww = xlate_term C.start st lenv w in
	 D.push2 C.err C.start lenv ~attr ~t:ww (), attr :: a, ww :: wws
      in
      let void_map (lenv, a, n) id = 
	 let attr = name_of_id id in
	 D.push2 C.err C.start lenv ~attr (), attr :: a, succ n
      in
      let lenv, aa, bb = match b with
         | T.Abst xws ->
	    let lenv = D.push_bind C.start lenv [] (D.Abst (n, [])) in
	    let lenv, aa, wws = List.fold_left abst_map (lenv, [], []) xws in
	    lenv, aa, D.Abst (n, wws)
         | T.Abbr xvs ->
	    let lenv = D.push_bind C.start lenv [] (D.Abbr []) in
	    let lenv, aa, vvs = List.fold_left abbr_map (lenv, [], []) xvs in
	    lenv, aa, D.Abbr vvs
         | T.Void ids ->
	    let lenv = D.push_bind C.start lenv [] (D.Void 0) in
	    let lenv, aa, n = List.fold_left void_map (lenv, [], 0) ids in
	    lenv, aa, D.Void n
      in
      let f tt = f (D.TBind (aa, bb, tt)) in
      xlate_term f st lenv t

let xlate_term f st lenv t =
   TT.contract (xlate_term f st lenv) t

let mk_contents n tt = function
   | T.Decl -> []                    , E.Abst (n, tt)
   | T.Ax   -> [E.InProp]            , E.Abst (n, tt)
   | T.Cong -> [E.InProp; E.Progress], E.Abst (n, tt)   
   | T.Def  -> []                    , E.Abbr tt
   | T.Th   -> [E.InProp]            , E.Abbr tt

let xlate_entity err f gen st = function
   | T.Require _                           ->
      err st
   | T.Section (Some name)                 ->
      err {st with path = name :: st.path}
   | T.Section None                        ->
      begin match st.path with
	 | _ :: ptl -> 
	    err {st with path = ptl}
         | _        -> assert false
      end
   | T.Sorts sorts                         ->
      let map st (xix, s) =
         let ix = match xix with 
	    | None    -> st.sort
	    | Some ix -> ix
	 in
         {st with sort = H.set_sorts ix [s]}
      in
      err (List.fold_left map st sorts)
   | T.Graph id                            ->
      assert (H.set_graph id); err st
   | T.Entity (main, kind, n, id, info, t) ->
      let uri = uri_of_id st id st.path in
      Hashtbl.add henv id uri;
      let tt = xlate_term C.start st D.empty_lenv t in
(*
      print_newline (); CrgOutput.pp_term print_string tt;
*)
      let a = [] in
      let ms, b = mk_contents n tt kind in 
      let ms = if main then E.Main :: ms else ms in 
      let a = if ms <> [] then E.Meta ms :: a else a in
      let a = if info <> ("", "") then E.Info info :: a else a in
      let entity = E.Mark st.line :: a, uri, b in
      f {st with line = succ st.line} entity
   | T.Generate _                          ->
      err st

(* Interface functions ******************************************************)
*)
let initial_status () =
   Hashtbl.clear henv; {
   path = []; line = 1; sort = 0; mk_uri = G.get_mk_uri ()
}

let refresh_status st = {st with
   mk_uri = G.get_mk_uri ()
}

let crg_of_txt _ _ = assert false (* xlate_entity *)