(*
    ||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 C = Cps
module Y = Entity
module D = Crg
module B = Brg

let rec lenv_fold_left map1 map2 x = function
   | D.ESort            -> x
   | D.EBind (tl, a, b) -> lenv_fold_left map1 map2 (map1 x a b) tl
   | D.EProj (tl, a, e) -> lenv_fold_left map1 map2 (map2 x a e) tl

let rec xlate_term f = function
   | D.TSort (a, l)     -> f (B.Sort (a, l))
   | D.TGRef (a, n)     -> f (B.GRef (a, n))
   | D.TLRef (a, _, _)  -> let f i = f (B.LRef (a, i)) in Y.apix C.err f a
   | D.TCast (a, u, t)  ->
      let f uu tt = f (B.Cast (a, uu, tt)) in
      let f uu = xlate_term (f uu) t in
      xlate_term f u 
   | D.TAppl (a, vs, t) ->
      let map f v tt = let f vv = f (B.Appl (a, vv, tt)) in xlate_term f v in
      let f tt = C.list_fold_right f map vs tt in
      xlate_term f t
   | D.TProj (a, e, t)  ->
      let f tt = f (lenv_fold_left xlate_bind xlate_proj tt e) in
      xlate_term f t
   | D.TBind (ab, D.Abst ws, D.TCast (ac, u, t)) ->
      xlate_term f (D.TCast (ac, D.TBind (ab, D.Abst ws, u), D.TBind (ab, D.Abst ws, t)))
   | D.TBind (a, b, t)  ->
      let f tt = f (xlate_bind tt a b) in xlate_term f t

and xlate_bind x a b =
   let f a ns = a, ns in
   let a, ns = Y.get_names f a in 
   match b with
      | D.Abst ws ->
         let map x n w = 
	    let f ww = B.Bind (n :: a, B.Abst ww, x) in xlate_term f w
	 in
	 List.fold_left2 map x ns ws 
      | D.Abbr vs ->
         let map x n v = 
	    let f vv = B.Bind (n :: a, B.Abbr vv, x) in xlate_term f v
	 in
	 List.fold_left2 map x ns vs
      | D.Void _  ->
         let map x n = B.Bind (n :: a, B.Void, x) in
	 List.fold_left map x ns

and xlate_proj x _ e =
   lenv_fold_left xlate_bind xlate_proj x e

let brg_of_crg f t =
   f (xlate_term C.start t)