let k, n = resolve_key_with_default st default k in
if n.s then generated st h i else begin
if n <> default then KH.replace st k default;
- if !G.trace >= level then pp_table st; default
+ if !G.ct >= level then pp_table st; default
end
let assert_finite st n j =
- if !G.trace >= level then warn (Printf.sprintf "ASSERT FINITE %u" j);
+ if !G.ct >= level then warn (Printf.sprintf "ASSERT FINITE %u" j);
let rec aux (k, n) j = match n.v with
| Fin i when i = j -> true
| Fin i ->
Printf.printf "binder %s is %u but must be %u\n" (P.string_of_mark k) i j; true (**)
| Inf ->
Printf.printf "binder %s is infinite but must be %u\n" (P.string_of_mark k) j; true (**)
- | Unk -> n.v <- Fin j; if !G.trace >= level then pp_table st; true
+ | Unk -> n.v <- Fin j; if !G.ct >= level then pp_table st; true
| Ref (k, i) -> n.v <- Fin j; aux (resolve_key st k) (i+j)
in
let k, n = resolve_layer st n in
aux (k, n) j
let assert_infinite st n =
- if !G.trace >= level then warn "ASSERT INFINITE";
+ if !G.ct >= level then warn "ASSERT INFINITE";
let rec aux (k, n) = match n.v with
| Inf -> true
| Fin i ->
Printf.printf "binder %s is %u but must be infinite\n" (P.string_of_mark k) i; true (**)
- | Unk -> n.v <- Inf; if !G.trace >= level then pp_table st; true
+ | Unk -> n.v <- Inf; if !G.ct >= level then pp_table st; true
| Ref (k, _) -> n.v <- Inf; aux (resolve_key st k)
in
aux (resolve_layer st n)
let two = finite 2
let rec unknown st =
- if !G.trace >= level then warn "UNKNOWN";
+ if !G.ct >= level then warn "UNKNOWN";
let default = empty () in
let k = P.new_mark () in
let k, n = resolve_key_with_default st default k in
if n.s then match n.v with
| Inf
| Fin _ -> n
- | Unk -> if !G.trace >= level then pp_table st; cell true (Ref (k, 0))
+ | Unk -> if !G.ct >= level then pp_table st; cell true (Ref (k, 0))
| Ref _ -> assert false
else unknown st
let minus st n j =
- if !G.trace >= level then warn (Printf.sprintf "MINUS %u" j);
+ if !G.ct >= level then warn (Printf.sprintf "MINUS %u" j);
let rec aux k n j = match n.v with
| Inf -> cell false n.v
| Fin i when i > j -> cell false (Fin (i - j))
string_of_value k n.v
let assert_not_zero st n =
- if !G.trace >= level then warn "ASSERT NOT ZERO";
+ if !G.ct >= level then warn "ASSERT NOT ZERO";
let k, n = resolve_layer st n in
match n.b, n.v with
| true, _ -> n.b
(* | _ , Fin i when i = 0 ->
Printf.printf "^Pi reduction on binder %s\n" (P.string_of_mark k); false *) (**)
(* if n.s && n.v = Fin 1 then Printf.printf "Pi reduction on binder %s\n" (P.string_of_mark k); *)
- | _ -> n.b <- true; if !G.trace >= level then pp_table st; n.b
+ | _ -> n.b <- true; if !G.ct >= level then pp_table st; n.b
let assert_zero st n = assert_finite st n 0
| Ref _ -> assert false
else false
in begin
- if !G.trace >= level then warn "ASSERT EQUAL";
+ if !G.ct >= level then warn "ASSERT EQUAL";
if b && k1 <> P.null_mark && k2 <> P.null_mark then begin
- n1.v <- Ref (k2, 0); if !G.trace >= level then pp_table st
+ n1.v <- Ref (k2, 0); if !G.ct >= level then pp_table st
end; b end
let is_not_zero st n =