(*
    ||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

(* 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, b) -> 
         let e = aux e in
(* NOTE: the inner binders are alpha-converted first *)
         let a = R.alpha D.mem e a in
         map_bind st e a b out tab; D.EBind (e, a, b)
      | D.EAppl (e, a, v) ->
         let e = aux e in
         map_appl st e a v out tab; D.EAppl (e, a, v)
      | D.EProj (e, a, d) ->
         let e = aux e in
         map_proj st e a d out tab; D.EProj (e, a, d)
   in
   ignore (aux lenv)

let rec exp_term st e t out tab = match t with
   | D.TSort (a, l)       ->
      let a =
         let err _ = a in
         let f s = {a with E.n_name = Some (s, true)} in
	 H.string_of_sort err f l
      in
      let attrs = [XL.position l; XL.name a] in
      XL.tag XL.sort attrs out tab
   | D.TLRef (a, i)       ->
      let a = 
         let err _ = a in
	 let f n r = {a with E.n_name = Some (n, r)} in
         D.get_name err f i e
      in
      let attrs = [XL.position i; XL.name a] in
      XL.tag XL.lref attrs out tab
   | D.TGRef (a, n)       ->
      let a = {a with E.n_name = Some (U.name_of_uri n, true)} in
      let attrs = [XL.uri n; XL.name a; XL.apix a] in
      XL.tag XL.gref attrs out tab
   | D.TCast (a, 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 (a, v, t)    ->
      let attrs = [] in
      XL.tag XL.appl attrs ~contents:(exp_term st e v) out tab;
      exp_term st e t out tab
   | D.TProj (a, 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 a lenv e) t out tab
   | D.TBind (a, b, t) ->
(* NOTE: the inner binders are alpha-converted first *)
      let a = R.alpha D.mem e a in
      exp_bind st e a b out tab; 
      exp_term st (D.push_bind C.start a b e) t out tab 

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

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

and exp_proj st e a 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