(*
    ||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 H = Hierarchy
module C = Cps
module Y = Entity
module T = Txt
module D = Crg

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

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

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

(* Internal functions *******************************************************)

let initial_status mk_uri = {
   path = []; line = 1; sort = 0; mk_uri = mk_uri
}

let name_of_id id = Y.Name (id, true)

let mk_lref f i j k = f (D.TLRef ([Y.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.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 (b, t)       ->
      let map1 (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 map2 (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 []) in
	    let lenv, aa, wws = List.fold_left map1 (lenv, [], []) xws in
	    lenv, aa, D.Abst wws
         | T.Abbr xvs ->
	    let lenv = D.push_bind C.start lenv [] (D.Abbr []) in
	    let lenv, aa, vvs = List.fold_left map1 (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 map2 (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 mk_contents tt = function
   | T.Decl -> [], Y.Abst tt
   | T.Ax   -> [], Y.Abst tt
   | T.Def  -> [], Y.Abbr tt
   | T.Th   -> [], Y.Abbr tt

let xlate_entity err f st = function
   | 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 (kind, id, meta, 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, b = mk_contents tt kind in 
      let a = if meta <> "" then Y.Meta meta :: a else a in
      let entity = Y.Mark st.line :: a, uri, b in
      f {st with line = succ st.line} entity

(* Interface functions ******************************************************)

let initial_status mk_uri =
   initial_status mk_uri

let crg_of_txt = xlate_entity