From dda7d129dba6c90d642cd99cd989e5f13c0eb4b4 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 3 Jul 2019 12:54:37 +0200 Subject: [core] [api] Support OCaml 4.08 The changes are large due to `Pervasives` deprecation: - the `Pervasives` module has been deprecated in favor of `Stdlib`, we have opted for introducing a few wrapping functions in `Util` and just unqualified the rest of occurrences. We avoid the shims as in the previous attempt. - a bug regarding partial application have been fixed. - some formatting functions have been deprecated, but previous versions don't include a replacement, thus the warning has been disabled. We may want to clean up things a bit more, in particular w.r.t. modules once we can move to OCaml 4.07 as the minimum required version. Note that there is a clash between 4.08.0 modules `Option` and `Int` and Coq's ones. It is not clear if we should resolve that clash or not, see PR #10469 for more discussion. On the good side, OCaml 4.08.0 does provide a few interesting functionalities, including nice new warnings useful for devs. --- plugins/extraction/common.ml | 2 +- plugins/ltac/profile_ltac.ml | 2 +- plugins/ltac/tactic_debug.ml | 2 +- plugins/micromega/certificate.ml | 2 +- plugins/micromega/coq_micromega.ml | 4 ++-- plugins/micromega/csdpcert.ml | 2 +- plugins/micromega/mfourier.ml | 4 ++-- plugins/micromega/mutils.ml | 4 ++-- plugins/micromega/polynomial.ml | 16 ++++++++-------- plugins/micromega/simplex.ml | 4 ++-- plugins/micromega/sos_lib.ml | 10 +++++----- plugins/micromega/vect.ml | 4 ++-- plugins/omega/coq_omega.ml | 6 +++--- plugins/omega/omega.ml | 2 +- plugins/ssr/ssrview.ml | 2 +- 15 files changed, 33 insertions(+), 33 deletions(-) (limited to 'plugins') diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 9abf212443..109125702c 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -125,7 +125,7 @@ module KOrd = struct type t = kind * string let compare (k1, s1) (k2, s2) = - let c = Pervasives.compare k1 k2 (* OK *) in + let c = pervasives_compare k1 k2 (* OK *) in if c = 0 then String.compare s1 s2 else c end diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 243e0e945c..9d46bbc74e 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -376,7 +376,7 @@ let get_local_profiling_results () = List.hd Local.(!stack) own. *) module DData = struct type t = Feedback.doc_id * Stateid.t - let compare x y = Pervasives.compare x y + let compare x y = compare x y end module SM = Map.Make(DData) diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 9e735e0680..539536911c 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -156,7 +156,7 @@ let rec prompt level = begin let open Proofview.NonLogical in Proofview.NonLogical.print_notice (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >> - if Pervasives.(!batch) then return (DebugOn (level+1)) else + if Util.(!batch) then return (DebugOn (level+1)) else let exit = (skip:=0) >> (skipped:=0) >> raise Sys.Break in Proofview.NonLogical.catch Proofview.NonLogical.read_line begin function (e, info) -> match e with diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index 2e32b00c25..24039c93c6 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -93,7 +93,7 @@ let dev_form n_spec p = let rec fixpoint f x = let y' = f x in - if Pervasives.(=) y' x then y' + if (=) y' x then y' else fixpoint f y' let rec_simpl_cone n_spec e = diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index f0435126aa..5cc2c2e061 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1585,7 +1585,7 @@ let compact_proofs (cnf_ff: 'cst cnf) res (cnf_ff': 'cst cnf) = let is_proof_compatible (old_cl:'cst clause) (prf,prover) (new_cl:'cst clause) = let hyps_idx = prover.hyps prf in let hyps = selecti hyps_idx old_cl in - is_sublist Pervasives.(=) hyps new_cl in + is_sublist (=) hyps new_cl in @@ -1953,7 +1953,7 @@ open Persistent_cache module Cache = PHashtable(struct type t = (provername * micromega_polys) - let equal = Pervasives.(=) + let equal = (=) let hash = Hashtbl.hash end) diff --git a/plugins/micromega/csdpcert.ml b/plugins/micromega/csdpcert.ml index d8f71cda0c..cf5f60fb55 100644 --- a/plugins/micromega/csdpcert.ml +++ b/plugins/micromega/csdpcert.ml @@ -136,7 +136,7 @@ let pure_sos l = I should nonetheless be able to try something - over Z > is equivalent to -1 >= *) try let l = List.combine l (CList.interval 0 (List.length l -1)) in - let (lt,i) = try (List.find (fun (x,_) -> Pervasives.(=) (snd x) Mc.Strict) l) + let (lt,i) = try (List.find (fun (x,_) -> (=) (snd x) Mc.Strict) l) with Not_found -> List.hd l in let plt = poly_neg (poly_of_term (expr_to_term (fst lt))) in let (n,polys) = sumofsquares plt in (* n * (ci * pi^2) *) diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml index 34fb32c270..943bcb384b 100644 --- a/plugins/micromega/mfourier.ml +++ b/plugins/micromega/mfourier.ml @@ -15,7 +15,7 @@ open Vect let debug = false -let compare_float (p : float) q = Pervasives.compare p q +let compare_float (p : float) q = pervasives_compare p q (** Implementation of intervals *) open Itv @@ -587,7 +587,7 @@ struct let optimise vect l = (* We add a dummy (fresh) variable for vector *) let fresh = - List.fold_left (fun fr c -> Pervasives.max fr (Vect.fresh c.coeffs)) 0 l in + List.fold_left (fun fr c -> max fr (Vect.fresh c.coeffs)) 0 l in let cstr = { coeffs = Vect.set fresh (Int (-1)) vect ; op = Eq ; diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml index 97cf23ac1f..537b6175b4 100644 --- a/plugins/micromega/mutils.ml +++ b/plugins/micromega/mutils.ml @@ -21,7 +21,7 @@ module Int = struct type t = int - let compare : int -> int -> int = Pervasives.compare + let compare : int -> int -> int = compare let equal : int -> int -> bool = (=) end @@ -354,7 +354,7 @@ struct let from i = i let next i = i + 1 - let max : int -> int -> int = Pervasives.max + let max : int -> int -> int = max let pp o i = output_string o (string_of_int i) let compare : int -> int -> int = Int.compare let to_int x = x diff --git a/plugins/micromega/polynomial.ml b/plugins/micromega/polynomial.ml index f909b4ecda..1a31a36732 100644 --- a/plugins/micromega/polynomial.ml +++ b/plugins/micromega/polynomial.ml @@ -278,7 +278,7 @@ and op = |Eq | Ge | Gt exception Strict -let is_strict c = Pervasives.(=) c.op Gt +let is_strict c = (=) c.op Gt let eval_op = function | Eq -> (=/) @@ -422,7 +422,7 @@ module LinPoly = struct let min_list (l:int list) = match l with | [] -> None - | e::l -> Some (List.fold_left Pervasives.min e l) + | e::l -> Some (List.fold_left min e l) let search_linear p l = min_list (search_all_linear p l) @@ -656,9 +656,9 @@ module ProofFormat = struct let rec compare p1 p2 = match p1, p2 with | Annot(s1,p1) , Annot(s2,p2) -> if s1 = s2 then compare p1 p2 - else Pervasives.compare s1 s2 - | Hyp i , Hyp j -> Pervasives.compare i j - | Def i , Def j -> Pervasives.compare i j + else Util.pervasives_compare s1 s2 + | Hyp i , Hyp j -> Util.pervasives_compare i j + | Def i , Def j -> Util.pervasives_compare i j | Cst n , Cst m -> Num.compare_num n m | Zero , Zero -> 0 | Square v1 , Square v2 -> Vect.compare v1 v2 @@ -667,7 +667,7 @@ module ProofFormat = struct | MulPrf(p1,q1) , MulPrf(p2,q2) -> cmp_pair compare compare (p1,q1) (p2,q2) | AddPrf(p1,q1) , MulPrf(p2,q2) -> cmp_pair compare compare (p1,q1) (p2,q2) | CutPrf p , CutPrf p' -> compare p p' - | _ , _ -> Pervasives.compare (id_of_constr p1) (id_of_constr p2) + | _ , _ -> Util.pervasives_compare (id_of_constr p1) (id_of_constr p2) end @@ -785,7 +785,7 @@ module ProofFormat = struct let rec xid_of_hyp i l' = match l' with | [] -> failwith (Printf.sprintf "id_of_hyp %i %s" hyp (string_of_int_list l)) - | hyp'::l' -> if Pervasives.(=) hyp hyp' then i else xid_of_hyp (i+1) l' in + | hyp'::l' -> if (=) hyp hyp' then i else xid_of_hyp (i+1) l' in xid_of_hyp 0 l end @@ -873,7 +873,7 @@ module ProofFormat = struct let (p,o) = eval_prf_rule (fun i -> IMap.find i env) prf in if is_unsat (p,o) then true else - if Pervasives.(=) rst Done + if (=) rst Done then begin Printf.fprintf stdout "Last inference %a %s\n" LinPoly.pp p (string_of_op o); diff --git a/plugins/micromega/simplex.ml b/plugins/micromega/simplex.ml index 15fb55c007..4c95e6da75 100644 --- a/plugins/micromega/simplex.ml +++ b/plugins/micromega/simplex.ml @@ -587,7 +587,7 @@ let cut env rmin sol vm (rst:Restricted.t) tbl (x,v) = Printf.printf "This is a cutting plane for %a:" LinPoly.pp_var x; Printf.printf " %a\n" WithProof.output (v,prf); end; - if Pervasives.(=) (snd v) Eq + if (=) (snd v) Eq then (* Unsat *) Some (x,(v,prf)) else let vl = (Vect.dotproduct (fst v) (Vect.set 0 (Int 1) sol)) in @@ -651,7 +651,7 @@ let integer_solver lp = match find_cut (!nb mod 2) env cr (*x*) sol vm rst tbl with | None -> None | Some(cr,((v,op),cut)) -> - if Pervasives.(=) op Eq + if (=) op Eq then (* This is a contradiction *) Some(Step(vr,CutPrf cut, Done)) else diff --git a/plugins/micromega/sos_lib.ml b/plugins/micromega/sos_lib.ml index e3a9f6f60f..58d5d7ecf1 100644 --- a/plugins/micromega/sos_lib.ml +++ b/plugins/micromega/sos_lib.ml @@ -13,7 +13,7 @@ open Num (* Comparisons that are reflexive on NaN and also short-circuiting. *) (* ------------------------------------------------------------------------- *) -let cmp = Pervasives.compare (** FIXME *) +let cmp = compare (** FIXME *) let (=?) = fun x y -> cmp x y = 0;; let ( cmp x y < 0;; @@ -491,21 +491,21 @@ let temp_path = Filename.get_temp_dir_name ();; (* ------------------------------------------------------------------------- *) let strings_of_file filename = - let fd = try Pervasives.open_in filename + let fd = try open_in filename with Sys_error _ -> failwith("strings_of_file: can't open "^filename) in let rec suck_lines acc = - try let l = Pervasives.input_line fd in + try let l = input_line fd in suck_lines (l::acc) with End_of_file -> List.rev acc in let data = suck_lines [] in - (Pervasives.close_in fd; data);; + (close_in fd; data);; let string_of_file filename = String.concat "\n" (strings_of_file filename);; let file_of_string filename s = - let fd = Pervasives.open_out filename in + let fd = open_out filename in output_string fd s; close_out fd;; diff --git a/plugins/micromega/vect.ml b/plugins/micromega/vect.ml index 4b2bc66eb7..a5f3b83c48 100644 --- a/plugins/micromega/vect.ml +++ b/plugins/micromega/vect.ml @@ -148,7 +148,7 @@ let rec add (ve1:t) (ve2:t) = match ve1 , ve2 with | [] , v | v , [] -> v | (v1,c1)::l1 , (v2,c2)::l2 -> - let cmp = Pervasives.compare v1 v2 in + let cmp = Util.pervasives_compare v1 v2 in if cmp == 0 then let s = add_num c1 c2 in if eq_num (Int 0) s @@ -163,7 +163,7 @@ let rec xmul_add (n1:num) (ve1:t) (n2:num) (ve2:t) = | [] , _ -> mul n2 ve2 | _ , [] -> mul n1 ve1 | (v1,c1)::l1 , (v2,c2)::l2 -> - let cmp = Pervasives.compare v1 v2 in + let cmp = Util.pervasives_compare v1 v2 in if cmp == 0 then let s = ( n1 */ c1) +/ (n2 */ c2) in if eq_num (Int 0) s diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 6aec83318c..776bd0a829 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -500,7 +500,7 @@ let context sigma operation path (t : constr) = | (p, Fix ((_,n as ln),(tys,lna,v))) -> let l = Array.length v in let v' = Array.copy v in - v'.(n)<- loop (Pervasives.(+) i l) p v.(n); (mkFix (ln,(tys,lna,v'))) + v'.(n)<- loop (Util.(+) i l) p v.(n); (mkFix (ln,(tys,lna,v'))) | ((P_TYPE :: p), Prod (n,t,c)) -> (mkProd (n,loop i p t,c)) | ((P_TYPE :: p), Lambda (n,t,c)) -> @@ -684,7 +684,7 @@ let simpl_coeffs path_init path_k = | _ -> assert false) | _ -> assert false in - let n = Pervasives.(-) (List.length path_k) (List.length path_init) in + let n = Util.(-) (List.length path_k) (List.length path_init) in let newc = context sigma (fun _ t -> loop n t) (List.rev path_init) (pf_concl gl) in convert_concl ~check:false newc DEFAULTcast @@ -1000,7 +1000,7 @@ let shrink_pair p f1 f2 = | t1,t2 -> begin oprint t1; print_newline (); oprint t2; print_newline (); - flush Pervasives.stdout; CErrors.user_err Pp.(str "shrink.1") + flush stdout; CErrors.user_err Pp.(str "shrink.1") end let reduce_factor p = function diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml index cec87221f0..05c31062fc 100644 --- a/plugins/omega/omega.ml +++ b/plugins/omega/omega.ml @@ -242,7 +242,7 @@ let add_event, history, clear_history = (fun () -> !accu), (fun () -> accu := []) -let nf_linear = List.sort (fun x y -> Pervasives.(-) y.v x.v) +let nf_linear = List.sort (fun x y -> Util.(-) y.v x.v) let nf ((b : bool),(e,(x : int))) = (b,(nf_linear e,x)) diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index 34f13b1096..f91b5e7aa2 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -26,7 +26,7 @@ module AdaptorDb = struct module AdaptorKind = struct type t = kind - let compare = Pervasives.compare + let compare = pervasives_compare end module AdaptorMap = Map.Make(AdaptorKind) -- cgit v1.2.3