(*
    ||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 N = Layer
module E = Entity
module D = Crg
module B = Brg

(* internal functions: crg to brg term **************************************)

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, i)     -> f (B.LRef (a, i))
   | D.TCast (a, u, t)  ->
      let f tt uu = f (B.Cast (a, uu, tt)) in
      let f tt = xlate_term (f tt) u in
      xlate_term f t 
   | D.TAppl (a, v, t) ->
      let f tt vv = f (B.Appl (a, vv, tt)) in
      let f tt = xlate_term (f tt) v in
      xlate_term f t 
   | D.TProj (_, e, t)  -> 
      D.shift (xlate_term f) e t
   | D.TBind (a, b, t)  -> 
      xlate_term (xlate_bind f a b) t

and xlate_bind f a b x = match b with
   | D.Abst (n, w) ->
      let f ww = f (B.Bind (a, B.Abst (n, ww), x)) in 
      xlate_term f w
   | D.Abbr v      ->
      let f vv = f (B.Bind (a, B.Abbr vv, x)) in 
      xlate_term f v
   | D.Void        ->
      f (B.Bind (a, B.Void, x))

(* internal functions: brg to crg term **************************************)

let rec xlate_bk_term f = function
   | B.Sort (a, l)     -> f (D.TSort (a, l))
   | B.GRef (a, n)     -> f (D.TGRef (a, n))
   | B.LRef (a, i)     -> f (D.TLRef (a, i))
   | B.Cast (a, u, t)  ->
      let f tt uu = f (D.TCast (a, uu, tt)) in
      let f tt = xlate_bk_term (f tt) u in
      xlate_bk_term f t 
   | B.Appl (a, u, t)  ->
      let f tt uu = f (D.TAppl (a, uu, tt)) in
      let f tt = xlate_bk_term (f tt) u in
      xlate_bk_term f t 
   | B.Bind (a, b, t)  ->
      let f tt bb = f (D.TBind (a, bb, tt)) in
      let f tt = xlate_bk_bind (f tt) b in
      xlate_bk_term f t 

and xlate_bk_bind f = function
   | B.Abst (n, t) ->
      let f tt = f (D.Abst (n, tt)) in
      xlate_bk_term f t
   | B.Abbr t      ->
      let f tt = f (D.Abbr tt) in
      xlate_bk_term f t
   | B.Void        -> f D.Void
   
(* interface functions ******************************************************)

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

let crg_of_brg = xlate_bk_term