Work with embedding of terms & polynomials. No shift simplification q…

…uick-fix.

.ocamlinit

@@ -2,8 +2,6 @@
 #use "topfind";;
 (* ## end of OPAM user-setup addition for ocamltop / base ## keep this line *)
 
-let cmaPath = "/home/vnn490/Documents/Zipo/zipperposition/_build/default/src/";;
-
 (* Steps to fix “Error: unbound module An_example” in Ocaml interpreter:
 1. Find .ml file defining An_example (e.g. F12 opens definition in VSCode+Merlin).
 2. #require an external dependency, or proceed to step 3 for Zipperposition specific An_example.
@@ -13,56 +11,60 @@ let cmaPath = "/home/vnn490/Documents/Zipo/zipperposition/_build/default/src/";;
 6. Restart.
 
 Other notes:
-#mod_use "path/to/a_file.ml";;  Wraps inside module A_file like the compiler.
+#mod_use "path/to/a_file.ml";;  wraps inside module A_file like the compiler.
 Program ocamlobjinfo or objinfo prints info about given .cma file.
 $OCAML_TOPLEVEL_PATH/autoload  might be an alternative to this file.
 This file makes the toplevel slow to start. *)
 
 
 (* Zipperposition files: .cmi *)
 
-#directory "/home/vnn490/Documents/Zipo/zipperposition/_build/install/default/lib/logtk";;
-#directory "/home/vnn490/Documents/Zipo/zipperposition/_build/install/default/lib/logtk/proofs";;
-#directory "/home/vnn490/Documents/Zipo/zipperposition/_build/install/default/lib/logtk/parsers";;
-#directory "/home/vnn490/Documents/Zipo/zipperposition/_build/install/default/lib/logtk/solving";;
-#directory "/home/vnn490/Documents/Zipo/zipperposition/_build/install/default/lib/logtk/arbitrary";;
+#directory "./_build/install/default/lib/logtk";;
+#directory "./_build/install/default/lib/logtk/proofs";;
+#directory "./_build/install/default/lib/logtk/parsers";;
+#directory "./_build/install/default/lib/logtk/solving";;
+#directory "./_build/install/default/lib/logtk/arbitrary";;
 
-#directory "/home/vnn490/Documents/Zipo/zipperposition/_build/install/default/lib/libzipperposition";;
-#directory "/home/vnn490/Documents/Zipo/zipperposition/_build/install/default/lib/libzipperposition/avatar";;
-#directory "/home/vnn490/Documents/Zipo/zipperposition/_build/install/default/lib/libzipperposition/arith";;
-#directory "/home/vnn490/Documents/Zipo/zipperposition/_build/install/default/lib/libzipperposition/calculi";;
-#directory "/home/vnn490/Documents/Zipo/zipperposition/_build/install/default/lib/libzipperposition/phases";;
-#directory "/home/vnn490/Documents/Zipo/zipperposition/_build/install/default/lib/libzipperposition/induction";;
+#directory "./_build/install/default/lib/libzipperposition";;
+#directory "./_build/install/default/lib/libzipperposition/avatar";;
+#directory "./_build/install/default/lib/libzipperposition/arith";;
+#directory "./_build/install/default/lib/libzipperposition/calculi";;
+#directory "./_build/install/default/lib/libzipperposition/phases";;
+#directory "./_build/install/default/lib/libzipperposition/induction";;
 
 #directory ".";; (* Source .ml files may be duplicated in the .../_build/install/... directories so put the working directory into the search path as the last one to give it the precedence. *)
 
 
-(* External dependencies *)
+(* External dependencies—missing optional ones just print warnings and continue *)
 
-#require "batteries";; (* If ∄ Batteries, this just prints warning and continues. *)
-(* from src/{core,prover,solving}/dune files, (libraries ...) rows *)
+#require "batteries";;
+(* from src/{core,prover,...}/dune files, (libraries ...) rows *)
 #require "containers";;
 #require "containers-data";;
 #require "iter";;
 #require "oseq";;
 #require "zarith";;
 #require "unix";;
-#require "str";;
+#require "str";;
+#require "mtime.clock.os";;
 #require "msat";;
 #require "msat.tseitin";;
-#require "qcheck";;
+#require "qcheck";;
+#require "logtk.arith";;
 
 
 (* Zipperposition files: .cma *)
-
-let workingDirectory = Unix.getcwd();;
-let inZipperpositionDirectory p = Unix.chdir(cmaPath^p);;
+
+let workingDirectory = Sys.getcwd();;
+let cmaPath = "/_build/default/src/";;
+let inZipperpositionDirectory p = try Sys.chdir(workingDirectory^cmaPath^p)
+with Sys_error e -> print_string(e^" and so ");;
 
 inZipperpositionDirectory "core";;
 #load "logtk.cma";; (* dlllogtk.so is found from the set working directory *)
-
+
 inZipperpositionDirectory "proofs";;
-#load "logtk_proofs.cma";;
+#load "logtk_proofs.cma";;
 
 inZipperpositionDirectory "parsers";;
 #load "logtk_parsers.cma";;
@@ -79,9 +81,6 @@ inZipperpositionDirectory "prover";;
 inZipperpositionDirectory "prover_calculi/avatar";;
 #load "libzipperposition_avatar.cma";;
 
-inZipperpositionDirectory "prover_calculi/arith";;
-#load "libzipperposition_arith.cma";;
-
 inZipperpositionDirectory "prover_calculi/induction";;
 #load "libzipperposition_induction.cma";;
 
@@ -194,5 +193,5 @@ open RecurrencePolynomial;;
 #mod_use "summation_equality.ml";;
 open Summation_equality;;
 
-Unix.chdir workingDirectory;; (* restore original working directory *)
+Sys.chdir workingDirectory;; (* restore original working directory *)
 open Batteries (* If ∄ Batteries, this crashes, so make it the last command. *)

src/core/Util.ml

@@ -203,14 +203,13 @@ module UntypedPrint = struct
   let string_printers: ((any -> bool) * (any -> string)) list ref = ref[]
 
   let add_pp type_test to_string = string_printers := (type_test, to_string % magic) :: !string_printers
+
+  let registered_types() = magic List.map fst !string_printers
 
   let str x =
-    let rec loop = function [] -> raise(Failure "Printers from TypeTests.ml are uninitialized!")
-    | (type_test, to_string)::printers ->
-      if is_int(repr x) then string_of_int(magic x) (* prioritize int's *)
-      else if type_test x then to_string x
-      else loop printers
-    in loop(magic !string_printers)
+    let _, to_string = try magic List.find (CCFun.flip fst x) !string_printers
+      with Not_found -> failwith "Printers from TypeTests.ml are uninitialized!"
+    in to_string x
 
   (* Print message msg preceded by FILE line LINE ≣̲̇CALL-DEPTH of the caller's caller. *)
   let print_with_caller msg =

src/core/Util.mli

@@ -114,7 +114,10 @@ module UntypedPrint : sig
   val (~<) : 'a -> 'a
   val (|<) : string -> 'a -> 'a
   (** 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 registered_types : unit -> ('a -> bool) list
+  (** Retrieve the type tests used for polymorphic printing in order of priority. *)
+
   val str : 'a -> string
   (** Adhoc polymorphic to_string *)