(*
    ||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 H  = Hierarchy
module E  = Entity
module R  = Alpha
module XL = XmlLibrary
module D  = Crg

IFDEF OBJECTS THEN

(* internal functions *******************************************************)

let lenv_iter map_bind map_appl map_proj st e lenv out tab = 
   let rec aux = function
      | D.ESort              -> e
      | D.EBind (e, a, y, b) ->
         let e = aux e in
(* NOTE: the inner binders are alpha-converted first *)
         let y = R.alpha D.mem e y in
         map_bind st e a y b out tab; D.EBind (e, a, y, b)
      | D.EAppl (e, x, v)    ->
         let e = aux e in
         map_appl st e x v out tab; D.EAppl (e, x, v)
      | D.EProj (e, d)       ->
         let e = aux e in
         map_proj st e d out tab; D.EProj (e, d)
   in
   ignore (aux lenv)

let rec exp_term st e t out tab = match t with
   | D.TSort k         ->
      let y =
         let err _ = E.empty_bind in
         let f s = E.bind_attrs ~name:(s, true) () in
	 H.string_of_sort err f k
      in
      let attrs = [XL.position k; XL.name y] in
      XL.tag XL.sort attrs out tab
   | D.TLRef (_, i)    ->
      let y = 
         let err _ = E.empty_bind in
	 let f s r = E.bind_attrs ~name:(s, r) () in
         D.get_name err f i e
      in
      let attrs = [XL.depth i; XL.name y] in
      XL.tag XL.lref attrs out tab
   | D.TGRef (_, n)    ->
      let y = E.bind_attrs ~name:(U.name_of_uri n, true) () in
      let attrs = [XL.uri n; XL.name y] in
      XL.tag XL.gref attrs out tab
   | D.TCast (u, t)    ->
      let attrs = [] in
      XL.tag XL.cast attrs ~contents:(exp_term st e u) out tab;
      exp_term st e t out tab
   | D.TAppl (x, v, t) ->
      let attrs = [] in
      XL.tag (XL.appl x) attrs ~contents:(exp_term st e v) out tab;
      exp_term st e t out tab
   | D.TProj (lenv, t) ->
      let attrs = [] in
      XL.tag XL.proj attrs ~contents:(lenv_iter exp_bind exp_appl exp_proj st e lenv) out tab;
      exp_term st (D.push_proj C.start lenv e) t out tab
   | D.TBind (y, b, t) ->
(* NOTE: the inner binders are alpha-converted first *)
      let y = R.alpha D.mem e y in
      exp_bind st e E.empty_node y b out tab; 
      exp_term st (D.push_bind C.start E.empty_node y b e) t out tab 

and exp_appl st e x v out tab =
   let attrs = [] in
   XL.tag (XL.appl x) attrs ~contents:(exp_term st e v) out tab;

and exp_bind st e a y b out tab = match b with
   | D.Abst (_, n, w) ->
      let attrs = XL.layer st n :: XL.name y :: XL.side y @ XL.main y in
      XL.tag XL.abst attrs ~contents:(exp_term st e w) out tab
   | D.Abbr v         ->
      let attrs = [XL.name y] in
      XL.tag XL.abbr attrs ~contents:(exp_term st e v) out tab
   | D.Void           ->
      let attrs = [XL.name y] in
      XL.tag XL.void attrs out tab

and exp_proj st e lenv out tab =
   let attrs = [] in
   XL.tag XL.proj attrs ~contents:(lenv_iter exp_bind exp_appl exp_proj st e lenv) out tab

(* interface functions ******************************************************)

let export_term st = exp_term st D.empty_lenv

END