(* 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/.
 *)

module H = Hashtbl
module M = Meta
module A = Aut

type context_node = M.qid option (* context node: None = root *)

type context = (M.qid, context_node) H.t (* context: son, parent *)

type status = {
   genv: M.environment; (* global environment *)
   path: M.id list;     (* current section path *) 
   cnt: context;        (* context *)
   node: context_node;  (* current context node *)
   explicit: bool       (* need explicit context root? *)
}

type resolver = Local of int
              | Global of M.pars
	      | Unresolved

let initial_status = {
   genv = []; path = []; cnt = H.create 11; node = None; explicit = true
}

let complete_qid f st (id, is_local, qs) =
   let f qs = f (id, qs) in
   if is_local then Cps.list_rev_append f st.path ~tail:qs else f qs

let resolve_gref f st lenv gref =
  let rec get_local f i = function
     | []                              -> f None
     | (name, _) :: _ when name = gref -> f (Some i)
     | _ :: tl                         -> get_local f (succ i) tl
  in
  let rec get_global f = function
     | []                                       -> None
     | (args, name, _, _) :: _ when name = gref -> f (Some args)
     | _ :: tl                                  -> get_global f tl
  in
  let g = function
      | Some args -> f (Global args)
      | None      -> f Unresolved
  in
  let f = function
      | Some i -> f (Local i)
      | None   -> get_global g st.genv
  in
  get_local f 0 lenv

let rec xlate_term f st lenv = function
   | A.Sort sort         -> f (M.Sort sort)
   | A.Appl (v, t)       ->
      let f vv tt = f (M.Appl (vv, tt)) in
      let f vv = xlate_term (f vv) st lenv t in
      xlate_term f st lenv v
   | A.Abst (name, w, t) ->
      let add name w lenv = 
         let f name = (name, w) :: lenv in
         complete_qid f st (name, true, []) 
      in
      let f ww tt = f (M.Abst (name, ww, tt)) in
      let f ww = xlate_term (f ww) st (add name ww lenv) t in
      xlate_term f st lenv w
   | A.GRef (name, args) ->
      let f name = function
	 | Local i     -> f (M.LRef i)
         | Global defs -> 
            let map1 f = xlate_term f st lenv in
	    let map2 f (name, _) = f (M.GRef (name, [])) in
            let f tail =  	   
	       let f args = f (M.GRef (name, args)) in
               let f defs = Cps.list_rev_map_append f map2 defs ~tail in
	       Cps.list_sub_strict f defs args
	    in
	    Cps.list_map f map1 args
	 | Unresolved  -> assert false
      in
      let f name = resolve_gref (f name) st lenv name in
      complete_qid f st name