module ZE = BagEnvironment
module ZS = BagSubstitution
+IFDEF TYPE THEN
+
type machine = {
i: int;
c: Z.lenv;
let rec ho_whd f c m x =
(* L.warn "entering R.ho_whd"; *)
let aux m = function
- | Sort_ h -> f (Sort h)
- | Bind_ (_, _, w, _) ->
+ | Sort_ h -> f (Sort h)
+ | Bind_ (_, _, w, _) ->
let f w = f (Abst w) in unwind_to_term f m w
- | LRef_ (_, Some w) -> ho_whd f c m w
- | GRef_ (_, _, _, E.Abst w) -> ho_whd f c m w
- | GRef_ (_, _, _, E.Abbr v) -> ho_whd f c m v
- | LRef_ (_, None) -> assert false
- | GRef_ (_, _, _, E.Void) -> assert false
+ | LRef_ (_, Some w) -> ho_whd f c m w
+ | GRef_ (_, _, _, E.Abst (_, w)) -> ho_whd f c m w
+ | GRef_ (_, _, _, E.Abbr (_, v)) -> ho_whd f c m v
+ | LRef_ (_, None) -> assert false
+ | GRef_ (_, _, _, E.Void) -> assert false
in
whd aux c m x
let ho_whd f st c t =
- if !G.ct >= level then log1 st "Now scanning" c t;
+IFDEF TRACE THEN
+ if !G.ct >= level then log1 st "Now scanning" c t
+ELSE () END;
ho_whd f c empty_machine t
let rec are_convertible f st a c m1 t1 m2 t2 =
(* L.warn "entering R.are_convertible"; *)
let rec aux m1 r1 m2 r2 =
(* L.warn "entering R.are_convertible_aux"; *)
+IFDEF TRACE THEN
let u, t = term_of_whdr r1, term_of_whdr r2 in
- if !G.ct >= level then log2 st "Now really converting" c u c t;
+ if !G.ct >= level then log2 st "Now really converting" c u c t
+ELSE () END;
match r1, r2 with
| Sort_ k1, Sort_ k2 ->
if k1 = k2 then f a else f false
| GRef_ (_, {E.n_apix = a1}, _, E.Abst _),
GRef_ (_, {E.n_apix = a2}, _, E.Abst _) ->
if a1 = a2 then are_convertible_stacks f st a c m1 m2 else f false
- | GRef_ (_, {E.n_apix = a1}, _, E.Abbr v1),
- GRef_ (_, {E.n_apix = a2}, _, E.Abbr v2) ->
+ | GRef_ (_, {E.n_apix = a1}, _, E.Abbr (_, v1)),
+ GRef_ (_, {E.n_apix = a2}, _, E.Abbr (_, v2)) ->
if a1 = a2 then
let f a =
if a then f a else are_convertible f st true c m1 v1 m2 v2
else
if a1 < a2 then whd (aux m1 r1) c m2 v2 else
whd (aux_rev m2 r2) c m1 v1
- | _, GRef_ (_, _, _, E.Abbr v2) ->
+ | _, GRef_ (_, _, _, E.Abbr (_, v2)) ->
whd (aux m1 r1) c m2 v2
- | GRef_ (_, _, _, E.Abbr v1), _ ->
+ | GRef_ (_, _, _, E.Abbr (_, v1)), _ ->
whd (aux_rev m2 r2) c m1 v1
| Bind_ (y1, l1, w1, t1), Bind_ (_, l2, w2, t2) ->
let l = P.new_mark () in
else
C.list_fold_left2 f map a m1.s m2.s
-let are_convertible f st c u t =
- if !G.ct >= level then log2 st "Now converting" c u c t;
+let are_convertible f st c u t =
+IFDEF TRACE THEN
+ if !G.ct >= level then log2 st "Now converting" c u c t
+ELSE () END;
are_convertible f st true c empty_machine u empty_machine t
+
+END