Commit 214b1af1 authored by Andrei Paskevich's avatar Andrei Paskevich

driver: memoize the updated task

otherwise we lose the beginning of the transformation chain
parent ffa0aa01
......@@ -44,6 +44,7 @@ type driver = {
drv_regexps : (Str.regexp * prover_answer) list;
drv_timeregexps : Call_provers.timeregexp list;
drv_exitcodes : (int * prover_answer) list;
drv_tag : int
}
(** parse a driver file *)
......@@ -195,6 +196,7 @@ let load_driver = let driver_tag = ref (-1) in fun env file ->
drv_regexps = List.rev !regexps;
drv_timeregexps = List.rev !timeregexps;
drv_exitcodes = List.rev !exitcodes;
drv_tag = !driver_tag
}
(** apply drivers *)
......@@ -260,6 +262,17 @@ let update_task drv task =
in
add_tdecl task goal
let update_task =
let h = Hashtbl.create 5 in
fun drv ->
let update = try Hashtbl.find h drv.drv_tag with
| Not_found ->
let upd = Trans.store (update_task drv) in
Hashtbl.add h drv.drv_tag upd;
upd
in
Trans.apply update
let prepare_task drv task =
let lookup_transform t = lookup_transform t drv.drv_env in
let transl = List.map lookup_transform drv.drv_transform in
......
......@@ -55,9 +55,9 @@ val prove_task :
?old : in_channel ->
driver -> Task.task -> Call_provers.pre_prover_call
(** Split the previous function in two simpler function *)
(** Split the previous function in two simpler functions *)
val prepare_task : driver -> Task.task -> Task.task
val print_task_prepared :
?old : in_channel ->
driver -> Format.formatter -> Task.task -> unit
......
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