adapt logtk to mtime 2.0 and oseq 0.5 (raises opam requirement accord…

…ingly); remove causes of warning 39 (unused rec) and warning 6 (label omitted) errors

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" }

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

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? *)
+(* TODO: `dont care` unification, i.e. stopping at flex-flex pairs because exact result does not matter? *)

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?)

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)

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