[cmdline] Simplify code for handling time and memory limits.

src/main.ml

@@ -87,59 +87,42 @@ let config detect () =
              Whyconf.print_prover Pp.nothing)
           provers))
 
-(* conversion string -> int for memlimit and timeout *)
-(* auxiliary functions, TODO move to a better place *)
-(* first, find the first non-numerical character, and return a couple of
-   substrings *)
-let rec find_first_non_num (s : string) (i : int) (m : int) =
-  (* MUST be called with m = String.length s*)
-  if i >= m
-  then i
-  else
-    match s.[i] with
-    | '0' | '1' | '2' | '3' | '4' | '5' | '6' | '7' | '8' | '9' ->
-      find_first_non_num s (i + 1) m
-    | _ -> i
-
-let split_non_num (s : string) =
-  let m = String.length s in
-  let x = find_first_non_num s 0 m in
-  if x = m
-  then (s, "")
-  else (String.sub s ~pos:0 ~len:x, String.sub s ~pos:x ~len:(m - x))
-
-let find_mult_memlimit = function
-  | "" -> 1
-  | "M" | "MB" | "mega" | "megabytes" -> 1
-  | "G" | "GB" | "giga" | "gigabytes" -> 1000
-  | "T" | "TB" | "tera" | "terabytes" -> 1000000
-  | _ -> failwith "Unknown unit for memory limit"
-
-let find_mult_timeout = function
-  | "" -> 1
-  | "s" | "seconds" -> 1
-  | "min" | "minutes" -> 60
-  | "h" | "hours" -> 3600
-  | _ -> failwith "Unknown unit for timeout"
-
-let convert_memlimit (s : string option) : int option =
-  match s with
-  | None -> None
-  | Some s ->
-    let mem1, mem2 = split_non_num (String.strip s) in
-    Some (Int.of_string mem1 * find_mult_memlimit mem2)
+let memlimit_of_string s =
+  let s = String.strip s in
+  let value =
+    let re = Re__Pcre.regexp "[0-9]+" in
+    Re__Core.matches re s
+  in
+  let unit =
+    let re = Re__Pcre.regexp "MB?|GB?|TB?" in
+    Re__Core.matches re s
+  in
+  match (value, unit) with
+  | [ v ], ([] | [ "M" ] | [ "MB" ]) -> Int.of_string v
+  | [ v ], ([ "G" ] | [ "GB" ]) -> Int.of_string v * 1000
+  | [ v ], ([ "T" ] | [ "TB" ]) -> Int.of_string v * 1000000
+  | _ -> failwith "Unrecognized memory limit"
 
-let convert_timelimit s =
-  match s with
-  | None -> None
-  | Some s ->
-    let time1, time2 = split_non_num (String.strip s) in
-    Some (Int.of_string time1 * find_mult_timeout time2)
+let timelimit_of_string s =
+  let s = String.strip s in
+  let value =
+    let re = Re__Pcre.regexp "[0-9]+" in
+    Re__Core.matches re s
+  in
+  let unit =
+    let re = Re__Pcre.regexp "[a-z]" in
+    Re__Core.matches re s
+  in
+  match (value, unit) with
+  | [ v ], ([] | [ "s" ]) -> Int.of_string v
+  | [ v ], [ "m" ] -> Int.of_string v * 60
+  | [ v ], [ "h" ] -> Int.of_string v * 3600
+  | _ -> failwith "Unrecognized time limit"
 
-let verify format loadpath memlimit timeout prover dataset_csv files =
+let verify format loadpath memlimit timelimit prover dataset_csv files =
   let debug = log_level_is_debug () in
-  let memlimit = convert_memlimit memlimit in
-  let timelimit = convert_timelimit timeout in
+  let memlimit = Option.map memlimit ~f:memlimit_of_string in
+  let timelimit = Option.map timelimit ~f:timelimit_of_string in
   List.iter
     ~f:
       (Verification.verify ~debug format loadpath ?memlimit ?timelimit prover