diff --git a/src/core/Util.ml b/src/core/Util.ml index bcfa0fc6f..ad497f1df 100755 --- a/src/core/Util.ml +++ b/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") diff --git a/src/core/Util.mli b/src/core/Util.mli index c5c78c0f8..21494d5fb 100755 --- a/src/core/Util.mli +++ b/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 *) diff --git a/src/prover_phases/RecurrencePolynomial.ml b/src/prover_phases/RecurrencePolynomial.ml index c1a515405..b0bee25ab 100644 --- a/src/prover_phases/RecurrencePolynomial.ml +++ b/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 *) diff --git a/src/prover_phases/TypeTests.ml b/src/prover_phases/TypeTests.ml index 26602e855..2c97448fd 100755 --- a/src/prover_phases/TypeTests.ml +++ b/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 ~ "\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; *) \ No newline at end of file +add_pp monomial (digits_in wide % RecurrencePolynomial.mono_to_string); +add_pp polynomial (digits_in wide % RecurrencePolynomial.poly_to_string); \ No newline at end of file diff --git a/src/prover_phases/summation_equality.ml b/src/prover_phases/summation_equality.ml index 0ad037b20..8168df2ed 100755 --- a/src/prover_phases/summation_equality.ml +++ b/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 *) - *) + *) ~