V_______________________________________________________________ *)
module C = Cps
+module N = Layer
module E = Entity
-module N = Level
module D = Crg
module B = Brg
(* internal functions: crg to brg term **************************************)
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, i) -> f (B.LRef (a, i))
- | D.TCast (a, u, t) ->
- let f tt uu = f (B.Cast (a, uu, tt)) in
+ | D.TSort k -> f (B.Sort k)
+ | D.TGRef (a, n) -> f (B.GRef (a, n))
+ | D.TLRef (a, i) -> f (B.LRef (a, i))
+ | D.TCast (u, t) ->
+ let f tt uu = f (B.Cast (uu, tt)) in
let f tt = xlate_term (f tt) u in
- xlate_term f t
+ 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) ->
+ | D.TProj (e, t) ->
D.shift (xlate_term f) e t
- | D.TBind (a, b, t) ->
- xlate_term (xlate_bind f a b) t
+ | D.TBind (y, b, t) ->
+ xlate_term (xlate_bind f y b) t
-and xlate_bind f a b x = match b with
- | D.Abst (n, w) ->
- let f ww = f (B.Bind (a, B.Abst (n, ww), x)) in
+and xlate_bind f y b t = match b with
+ | D.Abst (r, n, w) ->
+ let f ww = f (B.Bind (y, B.Abst (r, n, ww), t)) in
xlate_term f w
- | D.Abbr v ->
- let f vv = f (B.Bind (a, B.Abbr vv, x)) in
+ | D.Abbr v ->
+ let f vv = f (B.Bind (y, B.Abbr vv, t)) in
xlate_term f v
- | D.Void ->
- f (B.Bind (a, B.Void, x))
+ | D.Void ->
+ f (B.Bind (y, B.Void, t))
(* 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))
- | B.Cast (a, u, t) ->
- let f tt uu = f (D.TCast (a, uu, tt)) in
+ | B.Sort k -> f (D.TSort k)
+ | B.GRef (a, n) -> f (D.TGRef (a, n))
+ | B.LRef (a, i) -> f (D.TLRef (a, i))
+ | B.Cast (u, t) ->
+ let f tt uu = f (D.TCast (uu, tt)) in
let f tt = xlate_bk_term (f tt) u in
xlate_bk_term f t
- | B.Appl (a, u, t) ->
+ | B.Appl (a, u, t) ->
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) ->
- let f tt bb = f (D.TBind (a, bb, tt)) in
+ | B.Bind (y, b, t) ->
+ let f tt bb = f (D.TBind (y, bb, tt)) in
let f tt = xlate_bk_bind (f tt) b in
xlate_bk_term f t
and xlate_bk_bind f = function
- | B.Abst (n, t) ->
- let f tt = f (D.Abst (n, tt)) in
+ | B.Abst (r, n, t) ->
+ let f tt = f (D.Abst (r, n, tt)) in
xlate_bk_term f t
- | B.Abbr t ->
+ | B.Abbr t ->
let f tt = f (D.Abbr tt) in
xlate_bk_term f t
- | B.Void -> f D.Void
+ | B.Void -> f D.Void
(* interface functions ******************************************************)