Making archsat up-to-date with the versions of the dependencies available on opam

opam

@@ -42,12 +42,13 @@ depends: [
   "qcheck"      { with-test & >= "0.8" }
   "dolmen"      { >= "0.4" & < "0.5" }
   "msat"        { >= "0.7" & < "0.8" }
-  "containers"  { >= "2.0" & < "3.0" }
-  "cmdliner"    { >= "0.9.8" }
+  "containers"  { >= "3.6" }
+  "containers-data"  { }
+  "cmdliner"    { >= "0.9.8" & < "2.0.0" }
   "zarith"
   "ocamlgraph"
   "gen"
-  "mtime"
+  "mtime"       { < "2" }
   "iter"        { >= "0.5" }
   "spelll"      { >= "0.3" }
   "uucp"

src/_tags

@@ -37,7 +37,7 @@ true: inline(100), optimize(3), unbox_closures, unbox_closures_factor(20)
 # Package dependencies
 <**/*>: package(unix), package(zarith), package(msat),      \
         package(cmdliner), package(ocamlgraph),             \
-        package(containers), package(containers.data),      \
+        package(containers), package(containers-data),      \
         package(dolmen), package(iter), package(gen),       \
         package(mtime), package(mtime.clock.os),            \
         package(spelll), package(uucp), package(uutf)

src/algos/rewrite.ml

@@ -234,7 +234,7 @@ module Normalize = struct
   let find_term_match rules t =
     let aux pos t' =
       let aux (rule, m, res) = (rule, m, res, pos) in
-      CCOpt.map aux (match_term_head t' rules)
+      CCOption.map aux (match_term_head t' rules)
     in
     Position.Term.find_map aux t
 

src/algos/superposition.ml

@@ -221,7 +221,7 @@ let compare c c' =
     CCOrd.(Expr.Term.compare a a'
            <?> (Expr.Term.compare, b, b')
            <?> (C.compare, c.map, c'.map))
-  | x, y -> Pervasives.compare (_discr x) (_discr y)
+  | x, y -> Stdlib.compare (_discr x) (_discr y)
 
 (* Printing of clauses *)
 let rec pp_id fmt c =
@@ -331,7 +331,7 @@ let map_rewrites m l =
   in
   List.map (fun (f, m') -> (f, apply m m')) l
 
-let rec compute_rewrites = function
+let compute_rewrites = function
   | Hyp (f, m) ->
     if Mapping.is_empty m then [] else
       begin match f with
@@ -963,7 +963,7 @@ let supp_lit c p_set acc =
 let rewrite p active inactive =
   if ((is_eq inactive.clause && p.rules.rp) ||
       (not @@ is_eq inactive.clause && p.rules.rn)) then
-    CCOpt.map (fun x -> p, x) @@ do_rewrite active inactive
+    CCOption.map (fun x -> p, x) @@ do_rewrite active inactive
   else
     None
 
@@ -1141,7 +1141,7 @@ and discount_loop ~merge p_set =
       Util.debug ~section:p_set.section "@{<yellow>Adding clause@} : %a" pp c;
       if c.lit = Empty then begin
         (* Call the callback *)
-        CCOpt.iter (fun f ->
+        CCOption.iter (fun f ->
             Util.debug ~section:p_set.section
               "@{<magenta>Found empty clause reached@}, %d clauses in state" (S.cardinal p_set.clauses);
             f (Lazy.force c.rewrites) (C.elements c.map)) p_set.callback;
@@ -1202,7 +1202,7 @@ let add_neq t ?f a b =
 
 let debug t =
   Util.debug ~section:t.section "@{<White>Precedence@}: @[<hov>%a@]" pp_precedence t;
-  let l = List.sort (fun c c' -> Pervasives.compare c.id c'.id) @@ S.elements t.clauses in
+  let l = List.sort (fun c c' -> Stdlib.compare c.id c'.id) @@ S.elements t.clauses in
   List.iter (fun c -> Util.debug ~section:t.section " |%@ %a" pp c) l
 
 let solve t =

src/algos/synth.ml

@@ -126,10 +126,10 @@ let term_try ty h f =
   Util.debug ~section "Trying: %a" Expr.Print.const_ty f;
   match Match.ty Mapping.empty Expr.(f.id_type.fun_ret) ty with
   | exception Match.Impossible_ty _ ->
-    Util.debug ~section "  \- unif failed";
+    Util.debug ~section "  \\- unif failed";
     None
   | m ->
-    Util.debug ~section "  \- unif found !";
+    Util.debug ~section "  \\- unif found !";
     (* TODO: allow variables in types of terms to synthetize ? *)
     let m' = List.fold_left (fun acc v ->
         if Mapping.Var.mem_ty acc v then acc
@@ -163,10 +163,10 @@ let term_aux h ty =
   (* Since type metas are replaced by Expr.Ty.base, this is sound *)
   (* Interesting case *)
   | { Expr.ty = Expr.TyApp (f, _) } as ty ->
-    let l = CCFun.(
+    let l =
         iter_on_head f
         |> Iter.filter_map (term_try ty h)
-        |> Iter.to_list) in
+        |> Iter.to_list in
     collapse ty l
 
 let rec perform h task =

src/base/builtin.ml

@@ -415,7 +415,7 @@ module Arith = struct
     | r -> fold_apply s r
 
   let apply f l =
-    match CCOpt.sequence_l (List.map classify l) with
+    match CCOption.sequence_l (List.map classify l) with
     | None -> None
     | Some l' ->
       let t = List.fold_left max_type Int l' in

src/base/expr.ml

@@ -415,7 +415,7 @@ module Subst = struct
       Format.fprintf fmt "@[<hov 2>%a ↦@ %a@]" print_key key print_value value
     in
     Format.fprintf fmt "@[<hv>%a@]"
-      CCFormat.(seq ~sep:(return ";@ ") aux) (Mi.values map)
+      CCFormat.(iter ~sep:(return ";@ ") aux) (Mi.values map)
 
   let debug print_key print_value fmt map =
     let aux fmt ((i, j), (key, value)) =
@@ -519,11 +519,11 @@ module Id = struct
     CCVector.push value_vec None;
     { index; id_name; id_type; id_tags; builtin }
 
-  let ttype ?builtin ?tags name = mk_new ?builtin ?tags:(CCOpt.map ref tags) name Type
-  let ty ?builtin ?tags name ty = mk_new ?builtin ?tags:(CCOpt.map ref tags) name ty
+  let ttype ?builtin ?tags name = mk_new ?builtin ?tags:(CCOption.map ref tags) name Type
+  let ty ?builtin ?tags name ty = mk_new ?builtin ?tags:(CCOption.map ref tags) name ty
 
   let const ?builtin ?tags name fun_vars fun_args fun_ret =
-    mk_new ?builtin ?tags:(CCOpt.map ref tags) name { fun_vars; fun_args; fun_ret; }
+    mk_new ?builtin ?tags:(CCOption.map ref tags) name { fun_vars; fun_args; fun_ret; }
 
   let ty_fun ?builtin ?tags name n =
     const ?builtin ?tags name [] (CCList.replicate n Type) Type
@@ -674,7 +674,7 @@ module Meta = struct
   let hash m = CCHash.(combine2 m.meta_id.index (int m.meta_index))
 
   let compare m1 m2 =
-    CCOrd.(compare m1.meta_index m2.meta_index
+    CCOrd.(poly m1.meta_index m2.meta_index
            <?> (Id.compare, m1.meta_id, m2.meta_id))
 
   let equal m1 m2 = compare m1 m2 = 0
@@ -809,14 +809,14 @@ module Ty = struct
 
   let rec compare u v =
     let hu = hash u and hv = hash v in
-    if hu <> hv then Pervasives.compare hu hv
+    if hu <> hv then Stdlib.compare hu hv
     else match u.ty, v.ty with
       | TyVar v1, TyVar v2 -> Id.compare v1 v2
       | TyMeta m1, TyMeta m2 -> Meta.compare m1 m2
       | TyApp (f1, args1), TyApp (f2, args2) ->
         CCOrd.Infix.(Id.compare f1 f2
                      <?> (CCOrd.list compare, args1, args2))
-      | _, _ -> Pervasives.compare (discr u) (discr v)
+      | _, _ -> Stdlib.compare (discr u) (discr v)
 
   let equal u v =
     u == v || (hash u = hash v && compare u v = 0)
@@ -932,15 +932,15 @@ module Term = struct
 
   let rec compare u v =
     let hu = hash u and hv = hash v in
-    if hu <> hv then Pervasives.compare hu hv
+    if hu <> hv then Stdlib.compare hu hv
     else match u.term, v.term with
       | Var v1, Var v2 -> Id.compare v1 v2
       | Meta m1, Meta m2 -> Meta.compare m1 m2
       | App (f1, tys1, args1), App (f2, tys2, args2) ->
         CCOrd.Infix.(Id.compare f1 f2
                      <?> (CCOrd.list Ty.compare, tys1, tys2)
                      <?> (CCOrd.list compare, args1, args2))
-      | _, _ -> Pervasives.compare (discr u) (discr v)
+      | _, _ -> Stdlib.compare (discr u) (discr v)
 
   let equal u v =
     u == v || (hash u = hash v && compare u v = 0)
@@ -1101,7 +1101,7 @@ module Formula = struct
 
   let rec compare f g =
     let hf = hash f and hg = hash g in
-    if hf <> hg then Pervasives.compare hf hg
+    if hf <> hg then Stdlib.compare hf hg
     else match f.formula, g.formula with
       | True, True | False, False -> 0
       | Equal (u1, v1), Equal(u2, v2) ->
@@ -1118,7 +1118,7 @@ module Formula = struct
         CCOrd.Infix.(CCOrd.list Id.compare tys1 tys2
                      <?> (CCOrd.list Id.compare, ts1, ts2)
                      <?> (compare, h1, h2))
-      | _, _ -> Pervasives.compare (discr f) (discr g)
+      | _, _ -> Stdlib.compare (discr f) (discr g)
 
   let equal u v =
     u == v || (hash u = hash v && compare u v = 0)
@@ -1181,10 +1181,10 @@ module Formula = struct
     | True -> f_false
     | False -> f_true
     | Not f' ->
-      let f_status = CCOpt.get_or ~default:f.f_status status in
+      let f_status = CCOption.get_or ~default:f.f_status status in
       { f' with f_status; }
     | _ ->
-      let status = CCOpt.get_or ~default:f.f_status status in
+      let status = CCOption.get_or ~default:f.f_status status in
       mk_formula ~status (Not f)
 
   let check s = function
@@ -1196,7 +1196,7 @@ module Formula = struct
     let rec aux (o, acc) = function
       | [] -> o, acc
       | ({ formula = And l' } as f) :: r ->
-        let t = CCOpt.get_exn @@ get_tag f f_order in
+        let t = CCOption.get_exn_or "CCOption.get_exn_or" @@ get_tag f f_order in
         aux (t :: o, List.rev_append l' acc) r
       | a :: r ->
         aux (F a :: o, a :: acc) r
@@ -1213,7 +1213,7 @@ module Formula = struct
     let rec aux (o, acc) = function
       | [] -> o, acc
       | ({ formula = Or l' } as f) :: r ->
-        let t = CCOpt.get_exn @@ get_tag f f_order in
+        let t = CCOption.get_exn_or "CCOption.get_exn_or" @@ get_tag f f_order in
         aux (t :: o, List.rev_append l' acc) r
       | a :: r ->
         aux (F a :: o, a :: acc) r
@@ -1311,12 +1311,12 @@ module Formula = struct
       if p == new_p then f
       else neg ~status:f.f_status new_p
     | And _ ->
-      let o = CCOpt.get_exn @@ get_tag f f_order in
+      let o = CCOption.get_exn_or "CCOption.get_exn_or" @@ get_tag f f_order in
       let o'= Order.map (subst_aux ~fix ty_vmap ty_mmap t_vmap t_mmap f_vmap f_mmap) o in
       if Order.for_all2 (==) o o' then f
       else Order.build ~status:f.f_status f_and o'
     | Or l ->
-      let o = CCOpt.get_exn @@ get_tag f f_order in
+      let o = CCOption.get_exn_or "CCOption.get_exn_or" @@ get_tag f f_order in
       let o'= Order.map (subst_aux ~fix ty_vmap ty_mmap t_vmap t_mmap f_vmap f_mmap) o in
       if Order.for_all2 (==) o o' then f
       else Order.build ~status:f.f_status f_or o'

src/base/position.ml

@@ -31,7 +31,7 @@ let follow t i = concat t (path [i])
 
 (* Comparison, equality, printing. *)
 let equal = (=)
-let compare = Pervasives.compare
+let compare = Stdlib.compare
 
 let rec print fmt = function
   | Here -> Format.fprintf fmt "."
@@ -73,15 +73,15 @@ module Proof = struct
     match p, t with
     | Here, _ -> Some u
     | Arg (0, p'), { Term.term = Term.App (f, arg) } ->
-      CCOpt.map (fun x -> Term.app x arg) (substitute p' ~by:u f)
+      CCOption.map (fun x -> Term.app x arg) (substitute p' ~by:u f)
     | Arg (1, p'), { Term.term = Term.App (f, arg) } ->
-      CCOpt.map (fun x -> Term.app f x) (substitute p' ~by:u arg)
+      CCOption.map (fun x -> Term.app f x) (substitute p' ~by:u arg)
     | Arg (0, p'), { Term.term = Term.Let (v, e, body) } ->
-      CCOpt.map (fun x -> Term.letin v x body) (substitute p' ~by:u e)
+      CCOption.map (fun x -> Term.letin v x body) (substitute p' ~by:u e)
     | Arg (1, p'), { Term.term = Term.Let (v, e, body) } ->
-      CCOpt.map (fun x -> Term.letin v e x) (substitute p' ~by:u body)
+      CCOption.map (fun x -> Term.letin v e x) (substitute p' ~by:u body)
     | Arg (0, p'), { Term.term = Term.Binder (b, v, body) } ->
-      CCOpt.map (fun x -> Term.bind b v x) (substitute p' ~by:u body)
+      CCOption.map (fun x -> Term.bind b v x) (substitute p' ~by:u body)
     | Arg _, _ -> None
 
   let rec find_aux cur_pos u t =
@@ -90,11 +90,11 @@ module Proof = struct
       | { Term.term = Term.Type }
       | { Term.term = Term.Id _ } -> None
       | { Term.term = Term.App (f, arg) } ->
-        CCOpt.or_lazy
+        CCOption.or_lazy
           (find_aux (fun p -> cur_pos (Arg (0, p))) u f)
           ~else_:(fun () -> find_aux (fun p -> cur_pos (Arg (1, p))) u arg)
       | { Term.term = Term.Let (_, e, body) } ->
-        CCOpt.or_lazy
+        CCOption.or_lazy
           (find_aux (fun p -> cur_pos (Arg (0, p))) u e)
           ~else_:(fun () -> find_aux (fun p -> cur_pos (Arg (1, p))) u body)
       | { Term.term = Term.Binder (_, _, body) } ->
@@ -126,7 +126,7 @@ module Ty = struct
     match p, t with
     | Here, _ -> Some u
     | Arg (k, p'), { Expr.ty = Expr.TyApp(f, l) } ->
-      CCOpt.map (Expr.Ty.apply ~status:t.Expr.ty_status f) @@ CCOpt.sequence_l
+      CCOption.map (Expr.Ty.apply ~status:t.Expr.ty_status f) @@ CCOption.sequence_l
         (List.mapi (fun i v -> if i = k then substitute p' ~by:u v else Some v) l)
     | _ -> None
 
@@ -175,7 +175,7 @@ module Term = struct
     match p, t with
     | Here, _ -> Some u
     | Arg (k, p'), { Expr.term = Expr.App(f, tys, l) } ->
-      CCOpt.map (Expr.Term.apply ~status:t.Expr.t_status f tys) @@ CCOpt.sequence_l
+      CCOption.map (Expr.Term.apply ~status:t.Expr.t_status f tys) @@ CCOption.sequence_l
         (List.mapi (fun i v -> if i = k then substitute p' ~by:u v else Some v) l)
     | _ -> None
 

src/base/tag.ml

@@ -10,7 +10,7 @@
 module M = CCMixmap.Make(struct
     type t = int
     let compare (a: int) (b: int) =
-      Pervasives.compare a b
+      Stdlib.compare a b
   end)
 
 type map = M.t

src/base/type.ml

@@ -13,7 +13,7 @@ module Id = Dolmen.Id
 
 let get_loc =
   let default_loc = Dolmen.ParseLocation.mk "<?>" 0 0 0 0 in
-  (fun t -> CCOpt.get_or ~default:default_loc t.Ast.loc)
+  (fun t -> CCOption.get_or ~default:default_loc t.Ast.loc)
 
 module E = Map.Make(Expr.Id.Ttype)
 module F = Map.Make(Expr.Id.Ty)
@@ -1028,7 +1028,7 @@ let new_decl env t ?attr id =
     Id.print id Ast.print t;
   let aux acc (Any (tag, v)) = Tag.add acc tag v in
   let tags =
-    CCOpt.map (fun a ->
+    CCOption.map (fun a ->
         Util.debug ~section "Typing attribute:@ @[<hov>%a@]" Ast.print a;
         let l = parse_attr_and env a in
         List.fold_left aux Tag.empty l) attr

src/core/dispatcher.ml

@@ -163,11 +163,11 @@ let mk_ext
   Stats.attach section plugin_stats_group;
   {
     section;
-    set_handler = CCOpt.map (profile section) set_handler;
-    set_watcher = CCOpt.map (profile section) set_watcher;
-    assume = CCOpt.map (profile section) assume;
-    eval_pred = CCOpt.map (profile section) eval_pred;
-    preprocess = CCOpt.map (profile section) preprocess;
+    set_handler = CCOption.map (profile section) set_handler;
+    set_watcher = CCOption.map (profile section) set_watcher;
+    assume = CCOption.map (profile section) assume;
+    eval_pred = CCOption.map (profile section) eval_pred;
+    preprocess = CCOption.map (profile section) preprocess;
     handle = match handle with
       | None -> None
       | Some h ->
@@ -492,9 +492,9 @@ let stack_assign_level () =
 
 (** Call/execute a single job *)
 let call_job j =
-  if not CCOpt.(get_or ~default:true (j.job_formula >>= get_truth)) then
+  if not CCOption.(get_or ~default:true (j.job_formula >>= get_truth)) then
     Util.debug ~section:watch_section "Ignoring job %a because of false formula:@ %a"
-      pp_job j Expr.Formula.print (CCOpt.get_exn j.job_formula)
+      pp_job j Expr.Formula.print (CCOption.get_exn_or "CCOption.get_exn_or" j.job_formula)
   else begin
     Util.debug ~section:watch_section "Calling job %a" pp_job j;
     profile j.job_section j.job_callback ()
@@ -535,8 +535,8 @@ let cancel_jobs lvl =
       new_size := !new_size + 1
     end
   done;
-  let () = CCVector.shrink job_trail !new_size in
-  let () = CCVector.shrink job_level lvl in
+  let () = CCVector.truncate job_trail !new_size in
+  let () = CCVector.truncate job_level lvl in
   job_idx := j_lvl
 
 

src/core/ext_arith.ml

@@ -35,11 +35,11 @@ let evaluate_aux t =
   Arith.M.fold (fun e c acc ->
       match Dispatcher.get_assign e with
       | { Expr.term = Expr.App ({ Expr.builtin = B.Val v}, [], []) } ->
-        CCOpt.map (fun acc -> Q.(acc + c * val_to_q v)) acc
+        CCOption.map (fun acc -> Q.(acc + c * val_to_q v)) acc
       | _ -> None
     ) t.Arith.Lit.sum (Some (val_to_q t.Arith.Lit.const))
 
-let evaluate t = CCOpt.map evaluate_aux @@ Arith.Lit.parse_num t
+let evaluate t = CCOption.map evaluate_aux @@ Arith.Lit.parse_num t
 *)
 (* Incomplete extension *)
 (* ************************************************************************ *)

src/core/ext_prop.ml

@@ -32,7 +32,7 @@ let rec sat_eval = function
         None
     end
   | { Expr.formula = Expr.Not f } ->
-    CCOpt.map (fun (b, l) -> (not b, l)) (sat_eval f)
+    CCOption.map (fun (b, l) -> (not b, l)) (sat_eval f)
   | _ -> None
 
 (* Setup watchers *)