(* 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) ->
+ | 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) ->
+ | 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) ->
+ | 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
(* 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) ->
+ | 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
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.empty_node, true, 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) ->