module ZE = BagEnvironment
module ZR = BagReduction
+IFDEF TYPE THEN
+
(* Internal functions *******************************************************)
let level = 4
let rec b_type_of err f st c x =
(* L.warn "Entering T.b_type_of"; *)
- if !G.ct >= level then log1 st "Now checking" c x;
+IFDEF TRACE THEN
+ if !G.ct >= level then log1 st "Now checking" c x
+ELSE () END;
match x with
| Z.Sort h ->
let h = H.apply h in f x (Z.Sort h)
Z.get err0 f c i
| Z.GRef uri ->
let f = function
- | _, _, _, E.Abst w -> f x w
- | _, _, _, E.Abbr (Z.Cast (w, v)) -> f x w
- | _, _, _, E.Abbr _ -> assert false
- | _, _, _, E.Void -> assert false
+ | _, _, _, E.Abst (_, w) -> f x w
+ | _, _, _, E.Abbr (_, Z.Cast (w, v)) -> f x w
+ | _, _, _, E.Abbr _ -> assert false
+ | _, _, _, E.Void -> assert false
in
ZE.get_entity f uri
| Z.Bind (y, l, Z.Abbr v, t) ->
| Z.Appl (v, t) ->
let f xv vv xt tt = function
| ZR.Abst w ->
- if !G.ct > level then L.log st ZO.specs level (L.t_items1 "Just scanned" c w);
+IFDEF TRACE THEN
+ if !G.ct > level then L.log st ZO.specs level (L.t_items1 "Just scanned" c w)
+ELSE () END;
let f a =
(* L.warn (Printf.sprintf "Convertible: %b" a); *)
if a then f (S.sh2 v xv t xt x Z.appl) (Z.appl xv tt)
(* Interface functions ******************************************************)
and type_of err f st c x = b_type_of err f st c x
+
+END