From d274d65b0027f3833e02080f0cd80f36c9b0b869 Mon Sep 17 00:00:00 2001
From: Martin <martin@derivation.org>
Date: Mon, 30 Oct 2023 10:41:10 +0100
Subject: [PATCH] adapt logtk to mtime 2.0 and oseq 0.5 (raises opam
 requirement accordingly); remove causes of warning 39 (unused rec) and
 warning 6 (label omitted) errors

---
 logtk.opam               | 4 ++--
 src/core/Compute_prec.ml | 2 +-
 src/core/JP_unif.ml      | 4 ++--
 src/core/Ordering.ml     | 2 +-
 src/core/Statement.ml    | 4 ++--
 src/core/Util.ml         | 2 +-
 6 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/logtk.opam b/logtk.opam
index 03d0e25f6..b6c7ae954 100644
--- a/logtk.opam
+++ b/logtk.opam
@@ -14,10 +14,10 @@ depends: [
   "base-bytes"
   "base-unix"
   ("zarith" | "num")
-  "oseq" { >= "0.3" & < "0.5" }
+  "oseq" { >= "0.5" }
   "containers" { >= "3.0" & < "4.0" }
   "containers-data" { >= "3.0" & < "4.0" }
-  "mtime" { >= "1.0"  & < "2.0"}
+  "mtime" { >= "2.0"  & < "3.0"}
   "iter" { >= "1.2" }
   "menhir" {build}
   "dune" { >= "1.11" }
diff --git a/src/core/Compute_prec.ml b/src/core/Compute_prec.ml
index cee2d8a86..21266a9c5 100644
--- a/src/core/Compute_prec.ml
+++ b/src/core/Compute_prec.ml
@@ -83,7 +83,7 @@ let weight_fun_of_prec ?(rank=None) ~symbols ~prec_fun =
   let w_tbl =
     ID.Set.to_list symbols
     (* inverse sorting, we want the number of *larger* symbols *)
-    |> List.sort (fun f g -> Precedence.Constr.compare_by prec_fun g f)
+    |> List.sort (fun f g -> Precedence.Constr.compare_by ~constr:prec_fun g f)
     |> CCList.foldi (fun tbl idx f -> 
         ID.Map.add f (symbol_to_rank idx) tbl) 
        ID.Map.empty in
diff --git a/src/core/JP_unif.ml b/src/core/JP_unif.ml
index 1113f7ef8..cc8199731 100644
--- a/src/core/JP_unif.ml
+++ b/src/core/JP_unif.ml
@@ -197,7 +197,7 @@ let iterate ?(flex_same=false) ~scope ~counter u v l =
       )
   in
   (* The tuple `w` can be of any length. Hence we use the sequence [[alpha], [alpha, beta], [alpha, beta, gamma], ...] *)
-  let types_w_seq = OSeq.iterate [] (fun types_w -> Type.var (H.fresh_cnt ~counter ~ty:Type.tType ()) :: types_w) in
+  let types_w_seq = OSeq.iterate (fun types_w -> Type.var (H.fresh_cnt ~counter ~ty:Type.tType ()) :: types_w) [] in
   if OSeq.is_empty positions 
   then OSeq.empty
   else 
@@ -404,4 +404,4 @@ let unify_scoped (t0, scope0) (t1, scope1) =
 let unify_scoped_nonterminating t s = OSeq.filter_map (fun x -> x) (unify_scoped t s)
 
 (* TODO: operate on inner types like in `Unif`? Test for NO-TYPE terms? *)
-(* TODO: `dont care` unification, i.e. stopping at flex-flex pairs because exact result does not matter? *)
\ No newline at end of file
+(* TODO: `dont care` unification, i.e. stopping at flex-flex pairs because exact result does not matter? *)
diff --git a/src/core/Ordering.ml b/src/core/Ordering.ml
index d4febc72f..56118de34 100644
--- a/src/core/Ordering.ml
+++ b/src/core/Ordering.ml
@@ -300,7 +300,7 @@ module MakeKBO (P : PARAMETERS) : ORD = struct
 
   (** Higher-order KBO *)
   exception UnsupportedTerm
-  let rec kbo ~prec t1 t2 =
+  let kbo ~prec t1 t2 =
     let balance = mk_balance t1 t2 in
     (** Update variable balance, weight balance, and check whether the term contains the fluid term s.
         @param pos stands for positive (is t the left term?)
diff --git a/src/core/Statement.ml b/src/core/Statement.ml
index 00d4ac8a1..cafeab2af 100644
--- a/src/core/Statement.ml
+++ b/src/core/Statement.ml
@@ -631,7 +631,7 @@ let sine_axiom_selector
     map in
 
   let ids_to_defs_compute defs =
-    let rec aux map d = 
+    let aux map d = 
       let update_map map id stm =
         let prev = ID.Map.get_or ~default:InpStmSet.empty id map in
         ID.Map.add id (InpStmSet.add stm prev) map in
@@ -659,7 +659,7 @@ let sine_axiom_selector
 
 
   let categorize_formulas forms =
-    let rec do_categorize (defs, helpers, axioms, conjs) f =
+    let do_categorize (defs, helpers, axioms, conjs) f =
       match view f with 
       | Def _ | Rewrite _ -> (f::defs, helpers, axioms, conjs)
       | Assert _ -> (defs, helpers, f::axioms, conjs)
diff --git a/src/core/Util.ml b/src/core/Util.ml
index 0b1e20c6c..46645d2e1 100644
--- a/src/core/Util.ml
+++ b/src/core/Util.ml
@@ -12,7 +12,7 @@ let start_ = Mtime_clock.now()
 
 let get_time_mon_us () : timestamp =
   let t = Mtime_clock.now() in
-  Mtime.Span.to_us (Mtime.span start_ t)
+  (Mtime.Span.to_float_ns (Mtime.span start_ t)) *. 1e-3
 
 let total_time_s () = get_time_mon_us () *. 1e-6