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 E.apix C.err f a
+ | 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, 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.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) ->
- xlate_term f (D.tshift e t)
- | D.TBind (a, b, t) ->
- let f tt = f (xlate_bind tt a b) in xlate_term f t
+ D.shift (xlate_term f) e t
+ | D.TBind (a, b, t) ->
+ xlate_term (xlate_bind f a b) 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 = B.Bind (n :: J.new_mark () :: a, B.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 = 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_bind f a b x = match b with
+ | D.Abst (n, w) ->
+ let f ww = f (B.Bind (J.new_mark () :: 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, 0))
+ | 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 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) ->
and xlate_bk_bind f = function
| B.Abst (n, t) ->
- let f tt = f (D.Abst (n, [tt])) in
+ 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
+ let f tt = f (D.Abbr tt) in
xlate_bk_term f t
- | B.Void -> f (D.Void 1)
+ | B.Void -> f D.Void
(* interface functions ******************************************************)