(*
    ||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 X = Library
module D = Drg

(* this is not tail recursive *)
let rec list_iter map l f = match l with
   | []       -> f
   | hd :: tl -> map hd (list_iter map tl f)

let rec lenv_iter map1 map2 l f = match l with
   | D.ESort              -> f
   | D.EBind (lenv, a, b) -> lenv_iter map1 map2 lenv (map1 a b f)
   | D.EProj (lenv, a, e) -> lenv_iter map1 map2 lenv (map2 a e f)

(* these are not tail recursive *)
let rec exp_term t f = match t with
   | D.TSort (a, h)       ->
      let attrs = [X.position h; X.name a] in
      X.tag X.sort attrs f
   | D.TLRef (a, i, j)    ->
      let attrs = [X.position i; X.offset j; X.name a] in
      X.tag X.lref attrs f
   | D.TGRef (a, n)       ->
      let attrs = [X.uri n; X.name a] in
      X.tag X.gref attrs f   
   | D.TCast (a, u, t)    ->
      let attrs = [] in
      X.tag X.cast attrs (exp_term t f) ~contents:(exp_term u)
   | D.TAppl (a, vs, t)   ->
      let attrs = [X.arity (List.length vs)] in
      X.tag X.appl attrs (exp_term t f) ~contents:(list_iter exp_term vs)
   | D.TProj (a, lenv, t) ->
      let attrs = [] in
      X.tag X.proj attrs (exp_term t f) ~contents:(lenv_iter exp_bind exp_eproj lenv)
   | D.TBind (a, b, t) ->
      exp_bind a b (exp_term t f)

and exp_bind a b f = match b with
   | D.Abst ws ->
      let attrs = [X.name a; X.mark a; X.arity (List.length ws)] in
      X.tag X.abst attrs f ~contents:(list_iter exp_term ws)
   | D.Abbr vs ->
      let attrs = [X.name a; X.mark a; X.arity (List.length vs)] in
      X.tag X.abbr attrs f ~contents:(list_iter exp_term vs)
   | D.Void n ->
      let attrs = [X.name a; X.mark a; X.arity n] in
      X.tag X.void attrs f

and exp_eproj a lenv f =
   let attrs = [] in
   X.tag X.proj attrs f ~contents:(lenv_iter exp_bind exp_eproj lenv)

let export_term = exp_term