chore: fix compiler warnings

Author: hargoniX

src/backends/CVC4.ml

@@ -121,7 +121,7 @@ type t = {
   decode: decode_state;
   print_model: bool;
   options: string;
-  mutable sexp : DSexp.t;
+  sexp : DSexp.t;
   mutable closed : bool;
   mutable res : (T.t, Ty.t) Problem.Res.t option;
 }
@@ -919,7 +919,7 @@ let pipes
       let n = List.length options in
       assert (n > 0);
       (* each process' slice is only [1/n] of the global CVC4 slice *)
-      CCOpt.map (fun s -> s /. float n) slice
+      CCOption.map (fun s -> s /. float n) slice
     ) else slice
   in
   let encode pb =

src/backends/Smbc.ml

@@ -642,7 +642,7 @@ let dt_of_term (t:term): (term,ty) Model.DT.t =
       | TI.Builtin (`Ite (_,_,_)), v :: vars_tail ->
         let tests, else_ = T.ite_unfold t in
         let tests_v, other_tests =
-          CCList.partition_map
+          CCList.partition_filter_map
             (fun (a, b) ->
                match get_eqn_exn v vars_tail a with
                  | Some t ->

src/core/AnalyzeType.ml

@@ -176,7 +176,7 @@ module Make(T : TI.S) = struct
             | Stmt.Attr_infinite -> Some Card.infinite
             | _ -> None)
           attrs
-        |> CCOpt.get_or ~default
+        |> CCOption.get_or ~default
       | Env.Cstor _
       | Env.Fun_def (_,_,_)
       | Env.Fun_spec (_,_)

src/core/Env.ml

@@ -254,7 +254,7 @@ let mem ~env ~id = ID.PerTbl.mem env.infos id
 
 let find_ty_exn ~env id = (find_exn ~env id).ty
 
-let find_ty ~env id = CCOpt.map (fun x -> x.ty) (find ~env id)
+let find_ty ~env id = CCOption.map (fun x -> x.ty) (find ~env id)
 
 module type PRINT_TERM = sig
   type t

src/core/MetaVar.ml

@@ -36,7 +36,7 @@ let rebind ~var x =
   if can_bind var then invalid_arg "MetaVar.rebind" else var.deref <- Some x
 
 let update ~f v =
-  {v with deref=CCOpt.map f v.deref; }
+  {v with deref=CCOption.map f v.deref; }
 
 let pp oc v = Format.fprintf oc "?%a" ID.pp_full v.id
 let to_string v = "?" ^ ID.to_string v.id

src/core/Model.ml

@@ -76,7 +76,7 @@ module DT = struct
       Cases {
         var=Var.update_ty ~f:ty cases.var;
         tests;
-        default=CCOpt.map (map ~term ~ty) cases.default;
+        default=CCOption.map (map ~term ~ty) cases.default;
       }
 
   let rec filter_map ~test:ft ~yield:fy dt = match dt with
@@ -97,7 +97,7 @@ module DT = struct
             l
           |> tests_
       and default =
-        CCOpt.map (filter_map ~test:ft ~yield:fy) default
+        CCOption.map (filter_map ~test:ft ~yield:fy) default
       in
       mk_cases var tests ~default
 
@@ -245,7 +245,7 @@ module DT = struct
           | Tests l -> List.iter (fun (_,rhs) -> check_vars vars' rhs) l
           | Match (m,_) -> ID.Map.iter (fun _ (_,_,rhs) -> check_vars vars' rhs) m
         end;
-        CCOpt.iter (check_vars vars') default;
+        CCOption.iter (check_vars vars') default;
     in
     check_vars (vars t) t
 
@@ -400,7 +400,7 @@ module DT_util = struct
                tys, vars, eval_subst ~subst rhs)
           |> DT.match_ ~missing
       in
-      let default = CCOpt.map (eval_subst ~subst) default in
+      let default = CCOption.map (eval_subst ~subst) default in
       DT.mk_cases var' tests ~default
 
   let rec map_vars ~subst = function
@@ -422,7 +422,7 @@ module DT_util = struct
                tys,vars, map_vars ~subst rhs)
           |> DT.match_ ~missing
       in
-      let default = CCOpt.map (map_vars ~subst) default in
+      let default = CCOption.map (map_vars ~subst) default in
       DT.mk_cases var tests ~default
 
   let rename_vars dt = eval_subst ~subst:Subst.empty dt
@@ -491,7 +491,7 @@ module DT_util = struct
         DT.map_tests_or_match tests
           ~f:(fun sub -> join sub b) ~ty:CCFun.id ~term:CCFun.id
       and default =
-        CCOpt.map (fun d -> join d b) default
+        CCOption.map (fun d -> join d b) default
       in
       DT.mk_cases var tests ~default
 
@@ -534,7 +534,7 @@ module DT_util = struct
       CCList.filter_map
         (fun (c,subst) -> match c with
            | DT.Yield _ -> assert false
-           | DT.Cases {DT.default; _} -> CCOpt.map (fun x->x,subst) default)
+           | DT.Cases {DT.default; _} -> CCOption.map (fun x->x,subst) default)
         l
     in
     begin match l with
@@ -672,7 +672,7 @@ module DT_util = struct
           in
           (* add the default case, if needed *)
           let l =
-            let default = CCOpt.map (aux subst vars') default in
+            let default = CCOption.map (aux subst vars') default in
             CCList.cons_maybe default l
           in
           assert (l<>[]);
@@ -684,7 +684,7 @@ module DT_util = struct
                  T.eval ~subst lhs, aux subst vars rhs)
               l
           and default =
-            CCOpt.map (aux subst vars) default
+            CCOption.map (aux subst vars) default
           in
           DT.mk_tests v ~tests:l ~default
         )

src/core/Statement.ml

@@ -311,7 +311,7 @@ let map_clause_bind ~bind ~term acc c =
   let acc, vars = Utils.fold_map bind acc c.clause_vars in
   {
     clause_vars=vars;
-    clause_guard=CCOpt.map (term acc Polarity.Neg) c.clause_guard;
+    clause_guard=CCOption.map (term acc Polarity.Neg) c.clause_guard;
     clause_concl=term acc Polarity.Pos c.clause_concl;
   }
 
@@ -417,7 +417,7 @@ let fold_clause_bind ~bind ~term ~ty k b_acc acc (c:(_,_) pred_clause) =
   let pol = match k with `Pred -> Polarity.Pos | `Copred -> Polarity.Neg in
   let b_acc = List.fold_left bind b_acc c.clause_vars in
   let acc = term b_acc pol acc c.clause_concl in
-  CCOpt.fold (term b_acc (Polarity.inv pol)) acc c.clause_guard
+  CCOption.fold (term b_acc (Polarity.inv pol)) acc c.clause_guard
 
 let fold_pred_bind ~bind ~term ~ty k b_acc acc (def:(_,_) pred_def) =
   let acc = ty b_acc acc def.pred_defined.defined_ty in

src/core/Traversal.ml

@@ -212,7 +212,7 @@ module Make(T : TermInner.S)(Arg : ARG)(State : sig type t end) = struct
           List.iter
             (fun c ->
                yield_vars c.Stmt.clause_vars;
-               CCOpt.iter yield_term c.Stmt.clause_guard;
+               CCOption.iter yield_term c.Stmt.clause_guard;
                yield_term c.Stmt.clause_concl)
             p.Stmt.pred_clauses
         | PS_spec s ->

src/core/TypeCheck.ml

@@ -264,7 +264,7 @@ module Make(T : TI.S) = struct
     let check_top env bound _pol () t = ignore (check ~env bound t) in
     let check_ty env bound () t = ignore (check ~env bound t) in
     (* check cardinalities *)
-    CCOpt.iter
+    CCOption.iter
       (fun cache -> TyCard.check_non_zero ~cache env st)
       t.cache;
     (* basic check *)

src/parsers/TPTP_preprocess.ml

@@ -119,7 +119,7 @@ let close_forall t =
     | `Wildcard :: l' -> enter_bvars l' f
     | `Var v :: l' -> enter_bvar v (fun () -> enter_bvars l' f)
   and enter_ty_bvar (v, tyopt) f =
-    CCOpt.iter compute_fvars tyopt;
+    CCOption.iter compute_fvars tyopt;
     enter_bvar v f
   in
   compute_fvars t;
@@ -196,7 +196,7 @@ let rec declare_missing ~ctx ~state t =
                (fun () -> c, vars, declare_missing ~ctx ~state rhs))
           l
       and def =
-        CCOpt.map (declare_missing ~ctx ~state) def
+        CCOption.map (declare_missing ~ctx ~state) def
       in
       A.match_with ~loc ?default:def t l
     | A.Ite (a,b,c) ->

src/random/Term_random.ml

@@ -323,7 +323,7 @@ let mk_rand() = Random.State.make_self_init ()
 let generate ?(rand=mk_rand()) g = g rand
 
 let generate_l ?n ?(rand=mk_rand()) g =
-  let n = CCOpt.get_lazy (fun () -> G.(1 -- 50) rand) n in
+  let n = CCOption.get_lazy (fun () -> G.(1 -- 50) rand) n in
   G.list_repeat n g rand
 
 let pp_rules() =

src/transformations/Cstor_as_fun.ml

@@ -76,7 +76,7 @@ let cstor_as_fun (state:state) (id:ID.t) ~ty : ID.t * def option =
 type glob_state = {
   state: state;
   mutable env: env;
-  mutable new_stmts : (term, ty) Stmt.t CCVector.vector;
+  new_stmts : (term, ty) Stmt.t CCVector.vector;
   (* used for new declarations. [id, type, attribute list] *)
 }
 
@@ -151,7 +151,7 @@ let decode_model state m : (_,_) Model.t =
 
 (** {2 Pipe} *)
 
-let pipe_with ?on_decoded ~decode ~print ~check =
+let pipe_with ?on_decoded ~decode ~print ~check () =
   let on_encoded =
     Utils.singleton_if print () ~f:(fun () ->
       let module PPb = Problem.P in
@@ -181,4 +181,4 @@ let pipe ~print ~check =
     else []
   in
   let decode state = Problem.Res.map_m ~f:(decode_model state) in
-  pipe_with ~on_decoded ~print ~decode ~check
+  pipe_with ~on_decoded ~print ~decode ~check ()

src/transformations/Cstor_as_fun.mli

@@ -54,6 +54,7 @@ val pipe_with :
   decode:(state -> 'c -> 'd) ->
   print:bool ->
   check:bool ->
+  unit ->
   ((term, term) Problem.t,
    (term, term) Problem.t,
    'c, 'd

src/transformations/ElimCopy.ml

@@ -92,7 +92,7 @@ let has_small_exact_card card_concrete = match card_concrete with
   | Cardinality.Exact n ->
     (* if [n >= threshold] we approximate *)
     if Cardinality.Z.(compare n (of_int approx_threshold_) <= 0)
-    then Some (Cardinality.Z.to_int n |> CCOpt.get_exn)
+    then Some (Cardinality.Z.to_int n |> CCOption.get_exn_or "Cardinality was too large")
     else None
 
 let attrs_of_ty state (ty:ty): Stmt.decl_attr list =

src/transformations/ElimData.ml

@@ -51,6 +51,7 @@ module type S = sig
     decode:(decode_state -> 'c -> 'd) ->
     print:bool ->
     check:bool ->
+    unit ->
     ((T.t,T.t) Problem.t,
      (T.t,T.t) Problem.t, 'c, 'd
     ) Transform.t
@@ -164,7 +165,7 @@ module Make(M : sig val mode : mode end) = struct
     | None -> errorf "could not find encoding of `is-%a`" ID.pp id
 
   let ty_id ~state (id:ID.t) : T.t option =
-    let open CCOpt in
+    let open CCOption in
     Env.find_ty ~env:state.env id
     <+> Env.find_ty ~env:state.new_env id
 
@@ -887,7 +888,7 @@ module Make(M : sig val mode : mode end) = struct
            let cs =
              List.map
                (fun {Stmt.clause_guard=g; clause_concl=t; clause_vars} ->
-                  let g = CCOpt.map (tr_term state Pol.Neg) g in
+                  let g = CCOption.map (tr_term state Pol.Neg) g in
                   (* only process under the predicate itself *)
                   let t =
                     T.map () t ~bind:(fun _ _ -> assert false)
@@ -1156,7 +1157,7 @@ module Make(M : sig val mode : mode end) = struct
     | M_codata ->
       F.(update_l [Codata, Absent; Data, Present; Ind_preds, Present])
 
-  let pipe_with ?on_decoded ~decode ~print ~check =
+  let pipe_with ?on_decoded ~decode ~print ~check () =
     let on_encoded =
       Utils.singleton_if check ()
         ~f:(fun () ->
@@ -1186,7 +1187,7 @@ module Make(M : sig val mode : mode end) = struct
       else []
     in
     let decode state = Problem.Res.map_m ~f:(decode_model state) in
-    pipe_with ~on_decoded ~check ~decode ~print
+    pipe_with ~on_decoded ~check ~decode ~print ()
 end
 
 module Data = Make(struct let mode = M_data end)

src/transformations/ElimData.mli

@@ -44,6 +44,7 @@ module type S = sig
     decode:(decode_state -> 'c -> 'd) ->
     print:bool ->
     check:bool ->
+    unit ->
     ((term,term) Problem.t,
      (term,term) Problem.t, 'c, 'd
     ) Transform.t

src/transformations/ElimPatternMatch.ml

@@ -44,7 +44,7 @@ let elim_match ~mode ~env t =
   in
   let rec elim_match_ ~subst t = match T.repr t with
     | TI.Var v ->
-      CCOpt.get_or ~default:t (Subst.find ~subst v)
+      CCOption.get_or ~default:t (Subst.find ~subst v)
     | TI.Const _ -> t
     | TI.App (f,l) -> T.app (elim_match_ ~subst f) (elim_match_l_ ~subst l)
     | TI.Builtin b -> T.builtin (Builtin.map b ~f:(elim_match_ ~subst))

src/transformations/ElimRecursion.ml

@@ -740,7 +740,7 @@ let decode_model ~state m =
 
 (** {6 Pipe} *)
 
-let pipe_with ?on_decoded ~decode ~print ~check =
+let pipe_with ?on_decoded ~decode ~print ~check () =
   let on_encoded =
     Utils.singleton_if print () ~f:(fun () ->
       let module PPb = Problem.P in
@@ -770,4 +770,4 @@ let pipe ~print ~check =
     else []
   in
   let decode state = Problem.Res.map_m ~f:(decode_model ~state) in
-  pipe_with ~on_decoded ~print ~decode ~check
+  pipe_with ~on_decoded ~print ~decode ~check ()

src/transformations/ElimRecursion.mli

@@ -40,6 +40,7 @@ val pipe_with :
   decode:(decode_state -> 'c -> 'd) ->
   print:bool ->
   check:bool ->
+  unit ->
   ((term, term) Problem.t,
    (term, term) Problem.t,
    'c, 'd

src/transformations/ElimTypes.ml

@@ -448,7 +448,7 @@ let decode_term ?(subst=Var.Subst.empty) state rety t ty =
         | Some map ->
           (* if [id] is a unitype domain constant, replace it *)
           ID.Map.get id map
-          |> CCOpt.map_or ~default:t T.const
+          |> CCOption.map_or ~default:t T.const
       end
     | _ ->
       T.map () t
@@ -541,7 +541,7 @@ let decode_model ~state m =
 
 (** {2 Pipe} *)
 
-let pipe_with ?on_decoded ~decode ~print ~check =
+let pipe_with ?on_decoded ~decode ~print ~check () =
   let on_encoded =
     Utils.singleton_if print ()
       ~f:(fun () ->
@@ -571,5 +571,5 @@ let pipe ~print ~check =
          name (Problem.Res.pp T.pp' T.pp)]
     else []
   in
-  pipe_with ~check ~print ~on_decoded
+  pipe_with ~check ~print ~on_decoded ()
     ~decode:(fun state -> Problem.Res.map_m ~f:(decode_model ~state))

src/transformations/ElimTypes.mli

@@ -30,6 +30,7 @@ val pipe_with :
   decode:(state -> 'c -> 'd) ->
   print:bool ->
   check:bool ->
+  unit ->
   ((term,term) Problem.t,
    (term,term) Problem.t, 'c, 'd
   ) Transform.t

src/transformations/Elim_HOF.ml

@@ -337,13 +337,13 @@ type decode_state = {
 }
 
 type state = {
-  mutable env: (term, ty) Env.t;
+  env: (term, ty) Env.t;
   (* environment (to get signatures, etc.) *)
   arities: arity_set FunMap.t;
   (* set of arities for partially applied symbols/variables *)
   mutable app_count: int;
   (* used for generating new names *)
-  mutable new_stmts : (term, ty) Stmt.t CCVector.vector;
+  new_stmts : (term, ty) Stmt.t CCVector.vector;
   (* used for new declarations. [id, type, attribute list] *)
   mutable unsat_means_unknown: bool;
   (* did we have to do some approximation? *)
@@ -1001,7 +1001,7 @@ let as_handle_ ~state ty : handle option =
     | [], _ -> None
     | args,ret -> Some (handle_arrow_l args (H_leaf ret))
 
-let is_handle_ ~state ty : bool = CCOpt.is_some (as_handle_ ~state ty)
+let is_handle_ ~state ty : bool = CCOption.is_some (as_handle_ ~state ty)
 
 (* all domain constants whose type is a handle *)
 let all_fun_consts_ ~state m : (ty * handle) ID.Map.t =
@@ -1185,7 +1185,7 @@ let decode_model ~state m =
 
 (** {2 Pipe} *)
 
-let pipe_with ?on_decoded ~decode ~print ~check =
+let pipe_with ?on_decoded ~decode ~print ~check () =
   let on_encoded =
     Utils.singleton_if print () ~f:(fun () ->
       let module PPb = Problem.P in
@@ -1218,4 +1218,4 @@ let pipe ~print ~check =
     else []
   in
   let decode state = Problem.Res.map_m ~f:(decode_model ~state) in
-  pipe_with ~on_decoded ~print ~decode ~check
+  pipe_with ~on_decoded ~print ~decode ~check ()