(* 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 shift t = function
+ | _, [] -> t
+ | (a, l, b) :: c, _ :: ns -> shift (Z.Bind (a, l, b, t)) (c, ns)
+ | _ -> assert false
-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 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 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 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
+ xlate_term xlate_bind f c t
+ | D.TProj (_, e, t) ->
+ xlate_term xlate_bind f c (D.tshift e 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)))
+ 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 f tt = f (xlate_bind tt a b) in xlate_term f 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
-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
+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
+ 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
(* 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
+let rec xlate_bk_term f c = function
+ | Z.Sort h -> f (D.TSort ([], h))
+ | Z.GRef s -> f (D.TGRef ([], s))
+ | Z.LRef l ->
+ let f i = f (D.TLRef ([], i, 0)) 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 = 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 = 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
+ 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
+ xlate_bk_term f cc t
-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 ->
+and xlate_bk_bind f c = function
+ | Z.Abst t ->
+ let f tt = f (D.Abst (N.infinite, [tt])) in
+ xlate_bk_term f c t
+ | Z.Abbr t ->
let f tt = f (D.Abbr [tt]) in
- xlate_bk_term f t
- | Z.Void -> f (D.Void 1)
-
+ xlate_bk_term f c t
+ | Z.Void -> f (D.Void 1)
+
(* interface functions ******************************************************)
let bag_of_crg f t =
- f (xlate_term C.start t)
+ xlate_term xlate_bind f Z.empty_lenv t
-let crg_of_bag = xlate_bk_term
+let crg_of_bag f t = xlate_bk_term f Z.empty_lenv t
projects / helm.git / blobdiff