(*
    ||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 P = Marks
module N = Layer
module E = Entity
module D = Crg
module Z = Bag

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

let rec xlate_term st f c = function
   | D.TSort (_, h)    -> f (Z.Sort h)
   | D.TGRef (_, s)    -> f (Z.GRef s)
   | D.TLRef (a, i)    ->
      let _, l, _ = List.nth c i in f (Z.LRef l)
   | D.TCast (_, u, t) ->
      let f tt uu = f (Z.Cast (uu, tt)) in
      let f tt = xlate_term st (f tt) c u in
      xlate_term st f c t
   | D.TAppl (_, v, t) ->
      let f tt vv = f (Z.Appl (vv, tt)) in
      let f tt = xlate_term st (f tt) c v in
      xlate_term st f c t
   | D.TProj (_, e, t) ->
      D.shift (xlate_term st f c) e t
(* this case should be removed by improving alpha-conversion *)
   | D.TBind (ab, D.Abst (x, n, ws), D.TCast (ac, u, t)) ->
      xlate_term st f c (D.TCast (ac, D.TBind (ab, D.Abst (x, N.minus st n 1, ws), u), D.TBind (ab, D.Abst (x, n, ws), t)))
   | D.TBind (a, b, t) ->
      let f cc =
         let a, l, b = List.hd cc in
         let f tt = f (Z.Bind (a, l, b, tt)) in
         xlate_term st f cc t
      in
      xlate_bind st f c a b

and xlate_bind st f c a = function
   | D.Abst (_, _, w) ->
      let f ww = Z.push "xlate_bind" f c a (P.new_mark ()) (Z.Abst ww) in 
      xlate_term st f c w
   | D.Abbr v         -> 
      let f vv = Z.push "xlate_bind" f c a (P.new_mark ()) (Z.Abbr vv) in
      xlate_term st f c v
   | D.Void           ->
      Z.push "xlate_bind" f c a (P.new_mark ()) Z.Void

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

let rec xlate_bk_term f c = function
   | Z.Sort h            -> f (D.TSort (E.empty_node, h))
   | Z.GRef s            -> f (D.TGRef (E.empty_node, s))
   | Z.LRef l            -> 
       let f i = f (D.TLRef (E.empty_node, i)) in
       Z.nth C.err f l c
   | Z.Cast (u, t)  ->
      let f tt uu = f (D.TCast (E.empty_node, uu, tt)) in
      let f tt = xlate_bk_term (f tt) c u in
      xlate_bk_term f c t 
   | Z.Appl (u, t)       ->
      let f tt uu = f (D.TAppl (E.empty_node, uu, tt)) in
      let f tt = xlate_bk_term (f tt) c u in
      xlate_bk_term f c t 
   | Z.Bind (a, l, b, t) ->
      let f tt bb = f (D.TBind (a, bb, tt)) in      
      let f tt = xlate_bk_bind (f tt) c b in
      let cc = Z.push "xlate_bk_term" C.start c a l b in
      xlate_bk_term f cc t

and xlate_bk_bind f c = function
   | Z.Abst t ->
      let f tt = f (D.Abst (false, N.infinite, tt)) in
      xlate_bk_term f c t
   | Z.Abbr t ->
      let f tt = f (D.Abbr tt) in
      xlate_bk_term f c t
   | Z.Void   -> f D.Void

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

let bag_of_crg st f t =
   xlate_term st f Z.empty_lenv t

let crg_of_bag f t = xlate_bk_term f Z.empty_lenv t