V_______________________________________________________________ *)
module C = Cps
+module P = Marks
+module N = Layer
module E = Entity
-module J = Marks
-module N = Level
module D = Crg
module Z = Bag
(* internal functions: crg to bag term **************************************)
-let rec shift t = function
- | _, [] -> t
- | (a, l, b) :: c, _ :: ns -> shift (Z.Bind (a, l, b, t)) (c, ns)
- | _ -> assert false
-
-let rec xlate_term xlate_bind f c = function
- | D.TSort (_, h) -> f (Z.Sort h)
- | D.TGRef (_, s) -> f (Z.GRef s)
- | D.TLRef (a, _, _) ->
- let f i =
- let _, l, _ = List.nth c i in
- f (Z.LRef l)
- in
- E.apix C.err f a
- | D.TCast (_, u, t) ->
+let rec xlate_term st f c = function
+ | D.TSort k -> f (Z.Sort k)
+ | D.TGRef (_, s) -> f (Z.GRef s)
+ | D.TLRef (_, 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 xlate_bind (f tt) c u in
- xlate_term xlate_bind f c t
- | D.TAppl (_, vs, t) ->
- let map f v tt = let f vv = f (Z.Appl (vv, tt)) in xlate_term xlate_bind f c v in
- let f tt = C.list_fold_right f map vs tt in
- xlate_term xlate_bind f c t
- | D.TProj (_, e, t) ->
- xlate_term xlate_bind f c (D.tshift e t)
+ 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 (n, ws), D.TCast (ac, u, t)) ->
- xlate_term xlate_bind f c (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 g _ ns = ns in
- let ns = E.get_names g a in
- let cc = xlate_bind C.start c ns b in
- let f tt = f (shift tt (cc, ns)) in
- xlate_term xlate_bind f cc t
-
-let rec xlate_bind f c ns = function
- | D.Abst (_, ws) ->
- let map f n w c =
- let f ww = Z.push "xlate_bind" f c [n] (J.new_location ()) (Z.Abst ww) in
- xlate_term xlate_bind f c w
+ | 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
- C.list_fold_right2 f map ns ws c
- | D.Abbr vs ->
- let map f n v c =
- let f vv = Z.push "xlate_bind" f c [n] (J.new_location ()) (Z.Abbr vv) in
- xlate_term xlate_bind f c v
- in
- C.list_fold_right2 f map ns vs c
- | D.Void _ ->
- let map f n c = Z.push "xlate_bind" f c [n] (J.new_location ()) Z.Void in
- C.list_fold_right f map ns c
+ xlate_bind st f c y b
+
+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 y (P.new_mark ()) (Z.Abbr vv) in
+ xlate_term st f c v
+ | 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 ([], h))
- | Z.GRef s -> f (D.TGRef ([], s))
+ | 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 ([], i, 0)) in
+ 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 ([], 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 ([], [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
+ let f tt = f (D.Abbr tt) in
xlate_bk_term f c t
- | Z.Void -> f (D.Void 1)
+ | Z.Void -> f D.Void
(* interface functions ******************************************************)
-let bag_of_crg f t =
- xlate_term xlate_bind f Z.empty_lenv t
+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