Fix dynamic debug type tests.

src/core/Util.ml

@@ -212,9 +212,9 @@ module UntypedPrint = struct
       else loop printers
     in loop(magic !string_printers)
 
-  (* Print message msg preceded by FILE line LINE ⛓️CALL-DEPTH of the caller's caller. *)
+  (* Print message msg preceded by FILE line LINE ≣̲̇CALL-DEPTH of the caller's caller. *)
   let print_with_caller msg =
-    print_string(caller_file_line 2 ^" ⛓️"^ str Printexc.(raw_backtrace_length(get_callstack 9999)) ^"\t");
+    print_string(caller_file_line 2 ^" ≣̲̇"^ str Printexc.(raw_backtrace_length(get_callstack 9999)) ^"\t");
     flush_all(); (* Show at least location if printing triggers segmentation fault. *)
     let msg = msg() in print_endline(msg ^ if String.length msg < 55(*arbitrary*) then "" else "\n")
 

src/core/Util.mli

@@ -112,10 +112,8 @@ module UntypedPrint : sig
   (** type for values of forgotten type *)
 
   val (~<) : 'a -> 'a
-  (** Prefix an expression with ~< to trace it together with its location and call chain length. Output can contain oddities due to inlining and lack of runtime types. *)
-
   val (|<) : string -> 'a -> 'a
-  (** Prefix an expression with [message|<] to trace it together with [message], location and call chain length. Output can contain oddities due to inlining and lack of runtime types. *)
+  (** Prefix an expression with [~<] or [message|<] to trace it together with its location and call stack depth. Output can contain oddities due to inlining and lack of runtime types. *)
 
   val str : 'a -> string
   (** Adhoc polymorphic to_string *)

src/prover_phases/RecurrencePolynomial.ml

@@ -312,11 +312,11 @@ let var_name = string_part_at "y x v u t s r p o n m l k j i h e a"
  Currently I annotate at the embedding. This has the trade-off of making all polynomials in terms/clauses “ugly” but an embedded polynomial in a term in a polynomial does not need nested annotation. *)
 let term_name t = Term.to_string t
 
-(* E.g. ["-2x";"3y";"-4z"] becomes "-2x﹢3y﹣4z". (On Ubuntu command line “﹢” has width 2 which seems nice balance between 1 of “+” and 3 of “ + ”, some times.) *)
+(* E.g. ["-2x";"3y";"-4z"] becomes "-2x＋3y－4z". (On Ubuntu command line “＋” has width 2 which seems nice balance between 1 of “+” and 3 of “ + ”, some times.) *)
 let concat_plus_minus view = function
 | [] -> "0"
 | m::p -> map view p
-  |> flat_map String.(fun s -> if rcontains_from s 0 '-' then ["﹣"; sub s 1 (length s -1)] else ["﹢"; s])
+  |> flat_map String.(fun s -> if rcontains_from s 0 '-' then ["－"; sub s 1 (length s -1)] else ["＋"; s])
   |> cons(view m)
   |> String.concat ""
 
@@ -331,7 +331,7 @@ and mono_to_string m = group_succ ~eq:indet_eq m
   |> function ""->"1" | "-"->"-1" | "͘"->"1͘" | s->s
 
 and indet_to_string = function
-| C a -> (match Z.to_string a with "-1"->"-" | s->s) (* The trivial a=1 does not occur. *)
+| C a -> (match Z.to_string a with "1"->assert false | "-1"->"-" | s->s)
 | A I -> "͘"
 | A(V i) -> var_name i
 | A(T t) -> term_name t
@@ -351,7 +351,7 @@ let pp_poly = to_formatter poly_to_string
 (* List of terms that the given recurrence relates, without duplicates. *)
 let terms_in = sort_uniq ~cmp:Term.compare % flat_map(fun m -> match rev m with A(T t)::_->[t] | _->[])
 
-let term0 = Term.const ~ty:term (ID.make "𝟬")
+let term0 = Term.const ~ty:term (ID.make "⬮")
 exception RepresentingPolynomial of poly * Precedence.Weight.t * (simple_indeterminate -> int list)
 
 (* Given polynomial P<>0, embed P into a fresh ID idP, that idP into a Term termP, and it into a literal term0≈termP. Return all three.
@@ -362,7 +362,7 @@ let poly_as_lit_term_id ?name ?(weight=omega) p =
     (* Compute default name only if none is given. *)
     let replace = fold_left (%) id % map(fun(old,by) -> global_replace (regexp old) by) in
     let _name = poly_to_string p
-    |> replace ["﹢","˖"(*ᚐ*); "﹣","−"; "-","−"] (* avoid ' ' around name *)
+    |> replace ["＋","˖"; "－","−"; "-","−"] (* avoid ' ' around name *)
     |> flip String.iter
     (* |> Iter.filter(fun c -> not(mem c [' ';'(';')'])) *)
     (* |> Iter.take 20 *)

src/prover_phases/TypeTests.ml

@@ -26,13 +26,13 @@ let debug_root x b = Printexc.(if not b then match !debug_typing_fail with
 ); b
 
 (* When you see garbage output from str, ~< or |< instead of registered pretty printer's output, then the corresponding type test has an error. Use this function to narrow which subexpression is causing the problem. So replace, say ~<x, by debug_has_type t x where t is the type test that should pass for x. *)
-let debug_has_type t x =
+let debug_has_type ?(msg="") t x =
   debug_typing_fail := `On;
   let x_is_t = t x in
   let recorded = !debug_typing_fail in
   debug_typing_fail := `Off;
   if x_is_t then (print_endline("Valid typing in " ^ caller_file_line 1); x) else(
-    print_endline("Invalid typing for value:\n" ^ str x ^ (match recorded with
+    print_endline(msg ^ "\nInvalid typing for value:\n" ^ str x ^ (match recorded with
       | `At(sub_x, trace) ->
         "\n\nTyping the following subexpression failed:\n" ^ str sub_x ^
         "\n\nStack trace of the last corresponding test:\n" ^ Printexc.raw_backtrace_to_string trace
@@ -91,14 +91,15 @@ let exception' x = object0 x or test_tag 0 (function y::_-> object0 y |_->false)
 let rec ccmap key t x = union 1 [[ccmap key t; key; t; ccmap key t; int]] x
 (* Test for the default Set of OCaml which as a type is also the same as CCSet. *)
 let rec ccset t x = union 1 [[ccset t; t; ccset t; int]] x
-let ccbv x = tuple[array int; int] x
+let ccbv x = tuple[string(*array int*); int] x
 let ccvector t = tuple[int; array t] ~st:(fun(s,a)-> size a >= s & s >= 0)
 let rec bucketlist k v x = union 1 [[k; v; bucketlist k v]] x
 let hashtbl k v = tuple[int; array(bucketlist k v); int; int] ~st:(fun(s,a,_,_) -> size a >= s/2 & s >= 0)
 
 (* arbitrary precision types—unsafe! *)
-let integer x = int x or custom x
-let rational x = tuple[integer; integer] x
+let using_zarith = int Logtk_arith.Z.one
+let integer x = if using_zarith then int x or custom x else tuple[int;custom] x
+let rational x = tuple(integer::integer::(if using_zarith then [] else [bool])) x
 
 (* Types specific to Zipperposition *)
 
@@ -164,7 +165,7 @@ let rec position x = union 1 [[position]; [position]; [position]; [position]; [i
 let cut_form x = tuple[ccset tvar; list literals] x
 let payload x = union 1 [[literals]; [cut_form]; [list inductive_case]] x
 let trail x = ccset(tuple[int; payload; any(*TODO What should this be? See bool_lit.ml line 20*)]) x
-let sclause x = tuple[int; literals; trail; int] x
+let sclause x = tuple[int; literals; trail; int] x
 let clause x = tuple[
   sclause;
   int; 
@@ -181,14 +182,6 @@ let exn_pair x = tuple[tuple[object0;int]; exception'] x
 let flex_state x = ccmap int exn_pair x
 let run's_result x = or_error(tuple[flex_state; szs_status]) x
 
-(* let powers x = array int x
-let shifts x = union 1 [
-  [powers; term];
-  [powers; term; powers; term];
-  [int; int; powers; term]] x
-let monomial x = tuple[integer; powers; shifts] x
-let polynomial x = list monomial x *)
-
 let rec polynomial x = list monomial x
 and monomial x = list indeterminate x
 and indeterminate x = union 0 [
@@ -215,9 +208,9 @@ let clever_view sep view l = String.(
   indent := sub !indent 0 (length !indent - 1);
   s')
 (* optional helper to print integers, symbolic numbers, ring elements etc. differently *)
-let serif, double, sans, bold, thin = 94,104,114,124,134
+let wide, serif, double, sans, bold, thin = 96,94,104,114,124,134
 let digits_in style = String.(to_seq %> List.of_seq %> concat_view "" (function
-  | '0'..'9' as d -> "\xF0\x9D\x9F" ^ make 1 Char.(chr(style + code d))
+  | '0'..'9' as d -> (if style=wide then "\xEF\xBC" else "\xF0\x9D\x9F") ^ make 1 Char.(chr(style + code d))
   | c -> make 1 c))
 
 let extension = {Extensions.default with
@@ -232,7 +225,7 @@ add_pp clause (CCFormat.to_string Env.C.pp_tstp);
 add_pp any (fun x -> (match tag x with
   | t when t=final_tag -> "final" 
   | t when t=out_of_heap_tag -> "code"
-  | t when t=unaligned_tag -> "unaligned" (* e.g. 1ˢᵗ closure field unless its the above *)
+  | t when t=unaligned_tag -> "unaligned" (* e.g. 1ˢᵗ closure field unless it is the above *)
   | _ -> "tag="^str(tag x)
 )^":size="^str(size x));
 
@@ -295,8 +288,5 @@ add_pp term Term.to_string;
 add_pp literal Literal.to_string;
 add_pp proof (CCFormat.to_string Proof.S.pp_normal);
 
-add_pp monomial (digits_in serif % RecurrencePolynomial.mono_to_string);
-add_pp polynomial (digits_in serif % RecurrencePolynomial.poly_to_string);
-(* open Summation_equality.RecurrencePolynomial;;
-add_pp monomial mono_to_string;
-add_pp polynomial poly_to_string; *)
+add_pp monomial (digits_in wide % RecurrencePolynomial.mono_to_string);
+add_pp polynomial (digits_in wide % RecurrencePolynomial.poly_to_string);

src/prover_phases/summation_equality.ml

@@ -414,7 +414,7 @@ let sum_equality_inference clause =
   propagate_recurrences_to !"{ᵐm-n}b"; (* OK *)
   propagate_recurrences_to !"∑ⁿ{ᵐm-n}b"; (* missing M-rule *)
   (* propagate_recurrences_to !"{ⁿm}∑ⁿ{ᵐm-n}b"; (* errors: {ᵐm-n} vs {ᵐ-n+m}; rec. with N is very wrong *)
-  *)
+  *)
   ~<recurrence_table;
   exit 1;
   let seeSatur pp = ((~<) % Iter.to_list % saturate_with_order~=[1] % Iter.of_list % map eq0) pp in