V_______________________________________________________________ *)
module C = Cps
-module J = Marks
+module P = Marks
module N = Layer
module E = Entity
module D = Crg
(* internal functions: crg to bag term **************************************)
let rec xlate_term st f c = function
- | D.TSort (_, h) -> f (Z.Sort h)
+ | D.TSort k -> f (Z.Sort k)
| D.TGRef (_, s) -> f (Z.GRef s)
- | D.TLRef (a, i) ->
+ | D.TLRef (_, i) ->
let _, l, _ = List.nth c i in f (Z.LRef l)
- | D.TCast (_, u, t) ->
+ | 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
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.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 (n, ws), D.TCast (ac, u, t)) ->
- xlate_term st f c (D.TCast (ac, D.TBind (ab, D.Abst (N.minus st n 1, ws), u), D.TBind (ab, D.Abst (n, ws), t)))
- | D.TBind (a, b, t) ->
+ | D.TBind (y, D.Abst (x, n, ws), D.TCast (u, t)) ->
+ xlate_term st f c (D.TCast (D.TBind (y, D.Abst (x, N.minus st n 1, ws), u), D.TBind (y, D.Abst (x, n, ws), t)))
+ | D.TBind (y, 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
+ xlate_bind st f c y b
-and xlate_bind st f c a = function
- | D.Abst (_, w) ->
- let f ww = Z.push "xlate_bind" f c a (J.new_mark ()) (Z.Abst ww) in
+and xlate_bind st f c y = function
+ | D.Abst (_, _, w) ->
+ let f ww = Z.push "xlate_bind" f c y (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 (J.new_mark ()) (Z.Abbr vv) in
+ | D.Abbr v ->
+ let f vv = Z.push "xlate_bind" f c y (P.new_mark ()) (Z.Abbr vv) in
xlate_term st f c v
- | D.Void ->
- Z.push "xlate_bind" f c a (J.new_mark ()) Z.Void
+ | D.Void ->
+ Z.push "xlate_bind" f c y (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.Sort k -> f (D.TSort k)
| 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 uu = f (D.TCast (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 uu = f (D.TAppl (E.appl_attrs false, 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
+ | Z.Bind (y, l, b, t) ->
+ let f tt bb = f (D.TBind (y, 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
+ let cc = Z.push "xlate_bk_term" C.start c y 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 (N.infinite, tt)) in
+ let f tt = f (D.Abst (false, N.infinity, tt)) in
xlate_bk_term f c t
| Z.Abbr t ->
let f tt = f (D.Abbr tt) in