[cmdline] Move time and memory limit conversion functions into main module.

src/main.ml

@@ -87,11 +87,62 @@ 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 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 verify format loadpath memlimit timeout prover dataset_csv files =
   let debug = log_level_is_debug () in
+  let memlimit = convert_memlimit memlimit in
+  let timelimit = convert_timelimit timeout in
   List.iter
     ~f:
-      (Verification.verify ~debug format loadpath ?memlimit ?timeout prover
+      (Verification.verify ~debug format loadpath ?memlimit ?timelimit prover
          ?dataset_csv)
     files
 
@@ -164,7 +215,7 @@ let verify_cmd =
         & opt (some string) None
         & info [ "m"; "memlimit" ] ~doc ~docv:"MEM")
     in
-    let timeout =
+    let timelimit =
       let doc =
         "Time limit. $(docv) is intended in seconds (s) by default, but \
          minutes (m) and hours (h) may also be specified instead."
@@ -196,12 +247,13 @@ let verify_cmd =
     Term.(
       ret
         (const
-           (fun format loadpath memlimit timeout prover dataset_csv files _ ->
+           (fun format loadpath memlimit timelimit prover dataset_csv files _ ->
            `Ok
              (exec_cmd cmdname (fun () ->
-                verify format loadpath memlimit timeout prover dataset_csv files)))
-        $ format $ loadpath $ memlimit $ timeout $ prover $ dataset_csv $ files
-        $ setup_logs))
+                verify format loadpath memlimit timelimit prover dataset_csv
+                  files)))
+        $ format $ loadpath $ memlimit $ timelimit $ prover $ dataset_csv
+        $ files $ setup_logs))
   in
   Cmd.v info term
 

src/verification.ml

@@ -136,69 +136,14 @@ let call_prover ~limit config env prover config_prover driver dataset_csv task =
       Fmt.(option ~none:nop (any " " ++ string))
       additional_info)
 
-
-(* 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
-    begin
-      match s.[i] with
-      | '0' | '1' | '2' | '3' | '4' | '5' | '6' | '7' | '8' | '9' -> find_first_non_num s (i+1) m
-      | _ -> i
-    end
-
-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 "Unkown unit for memory limit"
-
-let find_mult_timeout = function
-        "" -> 1
-      | "s" | "seconds" -> 1
-      | "min" | "minutes" -> 60
-      | "h" | "hours" -> 3600
-      | _ -> failwith "Unkown unit for timeout"
-
-let convert_memlimit (s:string option) : int option =
-  match s with
-    None -> None
-  | Some s -> 
-    let (mem1,mem2) = split_non_num s in (*(String.trim s) in*)
-  Some ((Int.of_string mem1) * (find_mult_memlimit mem2))
-
-let convert_timeout (s:string option) : int option=
-    match s with
-    None -> None
-  | Some s -> 
-  let (time1,time2) = split_non_num s in
-  Some ((Int.of_string time1) * (find_mult_timeout time2))
-
-
-let verify ?(debug = false) format loadpath ?memlimit ?timeout prover
+let verify ?(debug = false) format loadpath ?memlimit ?timelimit prover
   ?dataset_csv file =
   if debug then Debug.set_flag (Debug.lookup_flag "call_prover");
-
-  let memlimit = convert_memlimit memlimit in
-  let timeout = convert_timeout timeout in
-  
   let env, config = create_env ~debug loadpath in
   let limit =
     let main = Whyconf.get_main config in
     let memlimit = Option.value memlimit ~default:(Whyconf.memlimit main) in
-    let timelimit = Option.value timeout ~default:(Whyconf.timelimit main) in
+    let timelimit = Option.value timelimit ~default:(Whyconf.timelimit main) in
     let def = Call_provers.empty_limit in
     {
       Call_provers.limit_time = timelimit;

src/verification.mli

@@ -31,8 +31,8 @@ val verify :
   ?debug:bool ->
   string option ->
   string list ->
-  ?memlimit:string ->
-  ?timeout:string ->
+  ?memlimit:int ->
+  ?timelimit:int ->
   Prover.t ->
   ?dataset_csv:string ->
   File.t ->