diff options
Diffstat (limited to 'plugins/micromega/mutils.ml')
| -rw-r--r-- | plugins/micromega/mutils.ml | 76 |
1 files changed, 45 insertions, 31 deletions
diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml index 7f0dce04..a07cbec6 100644 --- a/plugins/micromega/mutils.ml +++ b/plugins/micromega/mutils.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -31,7 +31,7 @@ let finally f rst = rst () ; res with reraise -> (try rst () - with any -> raise reraise + with any -> raise reraise ); raise reraise let map_option f x = @@ -72,15 +72,15 @@ let rec map3 f l1 l2 l3 = match l1 , l2 ,l3 with | [] , [] , [] -> [] | e1::l1 , e2::l2 , e3::l3 -> (f e1 e2 e3)::(map3 f l1 l2 l3) - | _ -> raise (Invalid_argument "map3") + | _ -> invalid_arg "map3" -let rec is_sublist l1 l2 = +let rec is_sublist f l1 l2 = match l1 ,l2 with | [] ,_ -> true | e::l1', [] -> false | e::l1' , e'::l2' -> - if e = e' then is_sublist l1' l2' - else is_sublist l1 l2' + if f e e' then is_sublist f l1' l2' + else is_sublist f l1 l2' let list_try_find f = let rec try_find_f = function @@ -89,7 +89,7 @@ let list_try_find f = in try_find_f -let rec list_fold_right_elements f l = +let list_fold_right_elements f l = let rec aux = function | [] -> invalid_arg "list_fold_right_elements" | [x] -> x @@ -142,9 +142,9 @@ let rec rec_gcd_list c l = | [] -> c | e::l -> rec_gcd_list (gcd_big_int c (numerator e)) l -let rec gcd_list l = +let gcd_list l = let res = rec_gcd_list zero_big_int l in - if compare_big_int res zero_big_int = 0 + if Int.equal (compare_big_int res zero_big_int) 0 then unit_big_int else res let rats_to_ints l = @@ -192,7 +192,7 @@ let select_pos lpos l = match l with | [] -> failwith "select_pos" | e::l -> - if i = j + if Int.equal i j then e:: (xselect (i+1) rpos l) else xselect (i+1) lpos l in xselect 0 lpos l @@ -269,19 +269,19 @@ struct let rec positive n = - if n=1 then XH - else if n land 1 = 1 then XI (positive (n lsr 1)) + if Int.equal n 1 then XH + else if Int.equal (n land 1) 1 then XI (positive (n lsr 1)) else XO (positive (n lsr 1)) let n nt = if nt < 0 then assert false - else if nt = 0 then N0 + else if Int.equal nt 0 then N0 else Npos (positive nt) let rec index n = - if n=1 then XH - else if n land 1 = 1 then XI (index (n lsr 1)) + if Int.equal n 1 then XH + else if Int.equal (n land 1) 1 then XI (index (n lsr 1)) else XO (index (n lsr 1)) @@ -289,8 +289,8 @@ struct (*a.k.a path_of_int *) (* returns the list of digits of n in reverse order with initial 1 removed *) let rec digits_of_int n = - if n=1 then [] - else (n mod 2 = 1)::(digits_of_int (n lsr 1)) + if Int.equal n 1 then [] + else (Int.equal (n mod 2) 1)::(digits_of_int (n lsr 1)) in List.fold_right (fun b c -> (if b then XI c else XO c)) @@ -342,7 +342,7 @@ struct | [] -> 0 (* Equal *) | f::l -> let cmp = f () in - if cmp = 0 then compare_lexical l else cmp + if Int.equal cmp 0 then compare_lexical l else cmp let rec compare_list cmp l1 l2 = match l1 , l2 with @@ -351,7 +351,7 @@ struct | _ , [] -> 1 | e1::l1 , e2::l2 -> let c = cmp e1 e2 in - if c = 0 then compare_list cmp l1 l2 else c + if Int.equal c 0 then compare_list cmp l1 l2 else c (** * hash_list takes a hash function and a list, and computes an integer which @@ -393,7 +393,7 @@ struct let from i = i let next i = i + 1 let pp o i = output_string o (string_of_int i) - let compare : int -> int -> int = Pervasives.compare + let compare : int -> int -> int = Int.compare end @@ -403,6 +403,12 @@ end module TagSet = Set.Make(Tag) +(** As for Unix.close_process, our Unix.waipid will ignore all EINTR *) + +let rec waitpid_non_intr pid = + try snd (Unix.waitpid [] pid) + with Unix.Unix_error (Unix.EINTR, _, _) -> waitpid_non_intr pid + (** * Forking routine, plumbing the appropriate pipes where needed. *) @@ -422,25 +428,33 @@ let command exe_path args vl = flush outch ; (* Wait for its completion *) - let _pid,status = Unix.waitpid [] pid in + let status = waitpid_non_intr pid in finally (* Recover the result *) (fun () -> match status with | Unix.WEXITED 0 -> - let inch = Unix.in_channel_of_descr stdout_read in - begin try Marshal.from_channel inch - with x when x <> Sys.Break -> - failwith (Printf.sprintf "command \"%s\" exited %s" exe_path (Printexc.to_string x)) - end - | Unix.WEXITED i -> failwith (Printf.sprintf "command \"%s\" exited %i" exe_path i) - | Unix.WSIGNALED i -> failwith (Printf.sprintf "command \"%s\" killed %i" exe_path i) - | Unix.WSTOPPED i -> failwith (Printf.sprintf "command \"%s\" stopped %i" exe_path i)) + let inch = Unix.in_channel_of_descr stdout_read in + begin + try Marshal.from_channel inch + with any -> + failwith + (Printf.sprintf "command \"%s\" exited %s" exe_path + (Printexc.to_string any)) + end + | Unix.WEXITED i -> + failwith (Printf.sprintf "command \"%s\" exited %i" exe_path i) + | Unix.WSIGNALED i -> + failwith (Printf.sprintf "command \"%s\" killed %i" exe_path i) + | Unix.WSTOPPED i -> + failwith (Printf.sprintf "command \"%s\" stopped %i" exe_path i)) (* Cleanup *) (fun () -> - List.iter (fun x -> try Unix.close x with e when e <> Sys.Break -> ()) - [stdin_read; stdin_write; stdout_read; stdout_write; stderr_read; stderr_write]) + List.iter (fun x -> try Unix.close x with any -> ()) + [stdin_read; stdin_write; + stdout_read; stdout_write; + stderr_read; stderr_write]) (* Local Variables: *) (* coding: utf-8 *) |