(*
    ||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 KF = Filename
module KH = Hashtbl
module KL = List

module U  = NUri
module C  = Cps
module G  = Options
module H  = Hierarchy
module E  = 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 *)
   rest  : bool;           (* restricted applications *) 
   mk_uri: G.uri_generator (* uri generator *) 
}

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

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

let xerr s () = 
   Printf.printf "%s\n%!" s; C.err ()

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

let mk_lref f a y i = f y (D.TLRef (a, i))

let mk_gref f y uri = f y (D.TGRef (E.empty_node, uri))

let get err f e i = match D.get e i with
   | _, _, _, D.Void -> err ()
   | _, a, y, _      -> mk_lref f a y i

let resolve_gref err f st id =
   try 
      let y, uri = KH.find henv id in f y uri
   with Not_found -> err ()

let name_of_id ?(r=true) id =
   if id = "" then None else Some (id, r)

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

let rec xlate_term f st lenv = function
(*
   CrgOutput.pp_lenv print_string (Layer.initial_status ()) lenv;
   Printf.printf "\n";
*)
   | T.Sort k         ->
      let y = E.bind_attrs ~main:(k, 0) () in 
      f y (D.TSort k)
   | T.NSrt id        ->
      let f h = xlate_term f st lenv (T.Sort h) in
      H.sort_of_string (xerr "sort not found") f id
   | T.LRef i         ->
      get (xerr "index out of bounds") f lenv i
   | T.NRef id        ->
      let err () = resolve_gref (xerr "global constant not found") (mk_gref f) st id in
      D.resolve_lref err (mk_lref f) id lenv
   | T.Cast (u, t)    ->
      let f uu y tt = f y (D.TCast (uu, tt)) in
      let f _ uu = xlate_term (f uu) st lenv t in
      xlate_term f st lenv u
   | T.Appl (v, t)    ->
      let f vv y tt = f y (D.TAppl (E.appl_attrs st.rest, vv, tt)) in
      let f _ vv = xlate_term (f vv) st lenv t in
      xlate_term f st lenv v
   | T.Proj (bs, t)   ->
      let f e y tt = f y (D.TProj (e, tt)) in
      let f (lenv, e) = xlate_term (f e) st lenv t in
      C.list_fold_left f (xlate_bind st) (lenv, D.empty_lenv) bs
   | T.Inst (t, vs)   ->
      let map f v e =
         let f _ vv = D.push_appl f (E.appl_attrs st.rest) vv e in
         xlate_term f st lenv v
      in
      let f e y tt = f y (D.TProj (e, tt)) in
      let f e = xlate_term (f e) st lenv t in
      C.list_fold_right f map vs D.empty_lenv

and xlate_bind st f (lenv, e) b =
   let f lenv e = f (lenv, e) in
   let f y b lenv = D.push_bind (f lenv) E.empty_node y b e in
   let f y b = D.push_bind (f y b) E.empty_node y b lenv in
   match b with
      | T.Abst (n, id, r, w) ->
         let f y ww =
            let y = E.bind_attrs ?name:(name_of_id id) () in
            f y (D.Abst (false, n, ww))
         in
         xlate_term f st lenv w
      | T.Abbr (id, v)       ->
         let f y vv =
            let y = E.bind_attrs ?name:(name_of_id id) () in
            f y (D.Abbr vv)
         in
         xlate_term f st lenv v
      | T.Void id           ->
         let y = E.bind_attrs ?name:(name_of_id id) ~main:(st.sort, 0) () in
         f y D.Void

let mk_contents main kind tt =
   let ms, b = match kind with
      | T.Decl -> []                    , E.abst E.empty_env tt
      | T.Ax   -> [E.InProp]            , E.abst E.empty_env tt
      | T.Cong -> [E.InProp; E.Progress], E.abst E.empty_env tt   
      | T.Def  -> []                    , E.abbr E.empty_env tt
      | T.Th   -> [E.InProp]            , E.abbr E.empty_env tt
   in
   if main then E.Main :: ms, b else ms, b

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 (KL.fold_left map st sorts)
   | T.Graph id                           ->
      assert (H.set_graph id); err st
   | T.Constant (main, kind, id, info, t) ->
      let uri = uri_of_id st id st.path in
      let g ya tt =
         KH.add henv id (ya, uri);
(*
         print_newline (); CrgOutput.pp_term print_string tt;
*)   
         let meta, b = mk_contents main kind tt in 
         let na = E.node_attrs ~apix:st.line () in
         let ra = E.root_attrs ~meta ~info () in
         let entity = ra, na, uri, b in
         f {st with line = succ st.line} entity
      in
      xlate_term g st D.empty_lenv t
   | T.Generate _                         ->
      err st

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

let initial_status () =
   KH.clear henv; {
   path = []; line = 1; sort = 0; rest = true; mk_uri = G.get_mk_uri ()
}

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

let crg_of_txt = xlate_entity