Commit 97ce495f authored by Andrei Paskevich's avatar Andrei Paskevich

rename 'regexptime' to 'timeregexp' and add comments

parent c64c50c6
......@@ -27,12 +27,12 @@ type timeunit =
| Sec
| Msec
type regexptime = {
re : Str.regexp;
group : timeunit array; (*ieme corresponds to the group i + 1*)
type timeregexp = {
re : Str.regexp;
group : timeunit array; (* i-th corresponds to the group i+1 *)
}
let regexptime s =
let timeregexp s =
let cmd_regexp = Str.regexp "%\\(.\\)" in
let nb = ref 0 in
let l = ref [] in
......@@ -132,7 +132,7 @@ type post_prover_call = unit -> prover_result
type bare_prover_call = unit -> post_prover_call
let call_on_buffer ~command ?(timelimit=0) ?(memlimit=0)
~regexps ~regexpstime ~exitcodes ~filename buffer =
~regexps ~timeregexps ~exitcodes ~filename buffer =
let on_stdin = ref true in
let on_timelimit = ref false in
let cmd_regexp = Str.regexp "%\\(.\\)" in
......@@ -169,7 +169,7 @@ let call_on_buffer ~command ?(timelimit=0) ?(memlimit=0)
Debug.dprintf debug "Call_provers: exited with status %d@." n;
(try List.assoc n exitcodes with Not_found -> grep out regexps)
in
let time = Util.default_option time (grep_time out regexpstime) in
let time = Util.default_option time (grep_time out timeregexps) in
let ans = match ans with
| HighFailure when !on_timelimit && timelimit > 0
&& time >= (0.9 *. float timelimit) -> Timeout
......
......@@ -56,10 +56,12 @@ val debug : Debug.flag
If set [call_on_buffer] prints on stderr the commandline called
and the output of the prover. *)
(** time parser *)
type regexptime
val regexptime : string -> regexptime
(** *)
type timeregexp
(** The type of precompiled regular expressions for time parsing *)
val timeregexp : string -> timeregexp
(** Converts a regular expression with special markers '%h','%m',
'%s','%i' (for milliseconds) into a value of type [timeregexp] *)
type post_prover_call = unit -> prover_result
(** Thread-unsafe closure that processes a prover's output
......@@ -75,7 +77,7 @@ val call_on_buffer :
?timelimit : int ->
?memlimit : int ->
regexps : (Str.regexp * prover_answer) list ->
regexpstime : regexptime list ->
timeregexps : timeregexp list ->
exitcodes : (int * prover_answer) list ->
filename : string ->
Buffer.t -> bare_prover_call
......@@ -89,10 +91,11 @@ val call_on_buffer :
the first field are substituted in the second field (\0,\1,...).
The regexps are tested in the order of the list.
@param regexpstime : if the first field matches the prover output,
the second field is the time in the format "%f:%f:%f" (h:m:s)
after substitution of matching groups. Otherwise wallclock is
used. The regexps are tested in the order of the list.
@param timeregexps : a list of regular expressions with special
markers '%h','%m','%s','%i' (for milliseconds), constructed with
[timeregexp] function, and used to extract the time usage from
the prover's output. If the list is empty, wallclock is used.
The regexps are tested in the order of the list.
@param exitcodes : if the first field is the exit code, then
the second field is the answer. Exit codes are tested in the order
......
......@@ -42,7 +42,7 @@ type driver = {
drv_meta : (theory * Stdecl.t) Mid.t;
drv_meta_cl : (theory * Stdecl.t) Mid.t;
drv_regexps : (Str.regexp * prover_answer) list;
drv_regexpstime : Call_provers.regexptime list;
drv_timeregexps : Call_provers.timeregexp list;
drv_exitcodes : (int * prover_answer) list;
}
......@@ -72,11 +72,11 @@ exception UnknownProp of (string list * string list)
let load_driver = let driver_tag = ref (-1) in fun env file ->
let prelude = ref [] in
let regexps = ref [] in
let regexpstime = ref [] in
let exitcodes = ref [] in
let filename = ref None in
let printer = ref None in
let transform = ref [] in
let timeregexps = ref [] in
let set_or_raise loc r v error = match !r with
| Some _ -> raise (Loc.Located (loc, Duplicate error))
......@@ -90,7 +90,7 @@ let load_driver = let driver_tag = ref (-1) in fun env file ->
| RegexpTimeout s -> add_to_list regexps (Str.regexp s, Timeout)
| RegexpUnknown (s,t) -> add_to_list regexps (Str.regexp s, Unknown t)
| RegexpFailure (s,t) -> add_to_list regexps (Str.regexp s, Failure t)
| RegexpTime r -> add_to_list regexpstime (Call_provers.regexptime r)
| TimeRegexp r -> add_to_list timeregexps (Call_provers.timeregexp r)
| ExitCodeValid s -> add_to_list exitcodes (s, Valid)
| ExitCodeInvalid s -> add_to_list exitcodes (s, Invalid)
| ExitCodeTimeout s -> add_to_list exitcodes (s, Timeout)
......@@ -171,7 +171,7 @@ let load_driver = let driver_tag = ref (-1) in fun env file ->
drv_meta = !meta;
drv_meta_cl = !meta_cl;
drv_regexps = List.rev !regexps;
drv_regexpstime = List.rev !regexpstime;
drv_timeregexps = List.rev !timeregexps;
drv_exitcodes = List.rev !exitcodes;
}
......@@ -200,11 +200,11 @@ let file_of_task drv input_file theory_name task =
let call_on_buffer ~command ?timelimit ?memlimit drv buffer =
let regexps = drv.drv_regexps in
let regexpstime = drv.drv_regexpstime in
let timeregexps = drv.drv_timeregexps in
let exitcodes = drv.drv_exitcodes in
let filename = get_filename drv "" "" "" in
Call_provers.call_on_buffer
~command ?timelimit ?memlimit ~regexps ~regexpstime
~command ?timelimit ?memlimit ~regexps ~timeregexps
~exitcodes ~filename buffer
(** print'n'prove *)
......
......@@ -50,7 +50,7 @@ type global =
| RegexpTimeout of string
| RegexpUnknown of string * string
| RegexpFailure of string * string
| RegexpTime of string
| TimeRegexp of string
| ExitCodeValid of int
| ExitCodeInvalid of int
| ExitCodeTimeout of int
......
......@@ -57,7 +57,7 @@ global:
| VALID STRING { RegexpValid $2 }
| INVALID STRING { RegexpInvalid $2 }
| TIMEOUT STRING { RegexpTimeout $2 }
| TIME STRING { RegexpTime ($2) }
| TIME STRING { TimeRegexp $2 }
| UNKNOWN STRING STRING { RegexpUnknown ($2, $3) }
| FAIL STRING STRING { RegexpFailure ($2, $3) }
| VALID INTEGER { ExitCodeValid $2 }
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment