--- /dev/null
+(*
+ ||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 E = Entity
+module J = Marks
+module N = Level
+module D = Crg
+module Z = Bag
+
+(* internal functions: crg to bag term **************************************)
+
+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 (Z.Sort (a, l))
+ | D.TGRef (a, n) -> f (Z.GRef (a, n))
+ | D.TLRef (a, _, _) -> let f i = f (Z.LRef (a, i)) in E.apix C.err f a
+ | D.TCast (a, u, t) ->
+ let f uu tt = f (Z.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 (Z.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 (n, ws), D.TCast (ac, u, t)) ->
+ xlate_term f (D.TCast (ac, D.TBind (ab, D.Abst (N.pred n, ws), u), D.TBind (ab, D.Abst (n, 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 = E.get_names f a in
+ match b with
+ | D.Abst (m, ws) ->
+ let map x n w =
+ let f ww = Z.Bind (n :: J.new_mark () :: a, Z.Abst (m, 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 = Z.Bind (n :: a, Z.Abbr vv, x) in
+ xlate_term f v
+ in
+ List.fold_left2 map x ns vs
+ | D.Void _ ->
+ let map x n = Z.Bind (n :: a, Z.Void, x) in
+ List.fold_left map x ns
+
+and xlate_proj x _ e =
+ lenv_fold_left xlate_bind xlate_proj x e
+
+(* internal functions: bag to crg term **************************************)
+
+let rec xlate_bk_term f = function
+ | Z.Sort (a, l) -> f (D.TSort (a, l))
+ | Z.GRef (a, n) -> f (D.TGRef (a, n))
+ | Z.LRef (a, i) -> f (D.TLRef (a, i, 0))
+ | Z.Cast (a, u, t) ->
+ let f uu tt = f (D.TCast (a, uu, tt)) in
+ let f uu = xlate_bk_term (f uu) t in
+ xlate_bk_term f u
+ | Z.Appl (a, u, t) ->
+ let f uu tt = f (D.TAppl (a, [uu], tt)) in
+ let f uu = xlate_bk_term (f uu) t in
+ xlate_bk_term f u
+ | Z.Bind (a, b, t) ->
+ let f bb tt = f (D.TBind (a, bb, tt)) in
+ let f bb = xlate_bk_term (f bb) t in
+ xlate_bk_bind f b
+
+and xlate_bk_bind f = function
+ | Z.Abst (n, t) ->
+ let f tt = f (D.Abst (n, [tt])) in
+ xlate_bk_term f t
+ | Z.Abbr t ->
+ let f tt = f (D.Abbr [tt]) in
+ xlate_bk_term f t
+ | Z.Void -> f (D.Void 1)
+
+(* interface functions ******************************************************)
+
+let bag_of_crg f t =
+ f (xlate_term C.start t)
+
+let crg_of_bag = xlate_bk_term