V_______________________________________________________________ *)
module B = Brg
+(* module O = Output *)
+
+let rec icm a = function
+ | B.Sort _
+ | B.LRef _
+ | B.GRef _ -> succ a
+ | B.Bind (_, B.Void, t) -> icm (succ a) t
+ | B.Cast (_, u, t) -> icm (icm a u) t
+ | B.Appl (_, u, t)
+ | B.Bind (_, B.Abst u, t)
+ | B.Bind (_, B.Abbr u, t) -> icm (icm (succ a) u) t
let iter map d =
let rec iter_bind d = function
- | B.Void as b -> b
- | B.Abst w -> B.Abst (iter_term d w)
- | B.Abbr v -> B.Abbr (iter_term d v)
+ | B.Void -> B.Void
+ | B.Abst w -> B.Abst (iter_term d w)
+ | B.Abbr v -> B.Abbr (iter_term d v)
and iter_term d = function
| B.Sort _ as t -> t
| B.GRef _ as t -> t
let lift_map h _ a i =
if i + h >= 0 then B.LRef (a, i + h) else assert false
-let lift g h d t =
- if h = 0 then g t else g (iter (lift_map h) d t)
-
-let lift_bind g h d = function
- | B.Void -> g B.Void
- | B.Abst w -> let g w = g (B.Abst w) in lift g h d w
- | B.Abbr v -> let g v = g (B.Abbr v) in lift g h d v
+let lift h d t =
+ if h = 0 then t else begin
+(* O.icm := succ (* icm *) !O.icm (*t*); *) iter (lift_map h) d t
+ end