Commit 50dbba85 authored by Andrei Paskevich's avatar Andrei Paskevich

- accept non-splitting transformations only in driver files

- apply transformations in Driver at print_task/prove_task
parent cd770632
......@@ -11,7 +11,7 @@ unknown "\\bunknown\\b\\|\\bsat\\b" "Unknown"
(* À discuter *)
transformation "simplify_recursive_definition"
transformation (*"split_goal_pos_neg_goal"*) "split_goal_pos_neg_all"
(* transformation (*"split_goal_pos_neg_goal"*) "split_goal_pos_neg_all"*)
transformation "inline_trivial"
transformation "remove_logic_definition"
transformation "encoding_decorate"
......
......@@ -2,7 +2,7 @@ printer "why3"
filename "%f-%t-%g.why"
(* À discuter *)
transformation "split_goal_pos_neg_all"
(* transformation "split_goal_pos_neg_all" *)
theory BuiltIn
syntax type int "int"
......
......@@ -11,7 +11,7 @@ unknown "unknown\\|sat\\|Fail" "Unknown"
(* À discuter *)
transformation "simplify_recursive_definition"
transformation (*"split_goal_pos_neg_goal"*) "split_goal_pos_neg_all"
(*transformation (*"split_goal_pos_neg_goal"*) "split_goal_pos_neg_all"*)
transformation "inline_trivial"
transformation "remove_logic_definition"
transformation "encoding_decorate"
......
......@@ -34,17 +34,10 @@ val store_use : (unit -> env -> use -> 'a trans) -> 'a trans_reg
val store_both : (unit -> env -> use -> clone -> 'a trans) -> 'a trans_reg
val store_task : (unit -> env -> task -> 'a trans) -> 'a trans_reg
(*
val store_clone : (unit -> env -> clone -> 'a trans) -> 'a trans_reg
*)
exception ArgumentNeeded
(*
val apply_clone : 'a trans_reg -> env -> clone -> task -> 'a
*)
val apply_env : 'a trans_reg -> env -> task -> 'a
val apply : 'a trans_reg -> task -> 'a
val apply_env : 'a trans_reg -> env -> task -> 'a
val apply : 'a trans_reg -> task -> 'a
val compose : task trans_reg -> 'a trans_reg -> 'a trans_reg
val compose_l : task tlist_reg -> 'a tlist_reg -> 'a tlist_reg
......
......@@ -107,28 +107,14 @@ let call_on_buffer ?(debug=false) ~command ~timelimit ~memlimit
(try List.assoc n exitcodes with Not_found -> grep out regexps)
in
let ans = match ans with
| HighFailure when time >= (0.9 *. float timelimit) -> Timeout
| HighFailure
when timelimit > 0 && time >= (0.9 *. float timelimit) -> Timeout
| _ -> ans
in
{ pr_answer = ans;
pr_output = out;
pr_time = time }
(*
let call_on_formatter ?debug ?filename
~command ~timelimit ~memlimit ~regexps formatter =
let buffer = Buffer.create 1024 in
let fmt = formatter_of_buffer buffer in
formatter fmt; pp_print_flush fmt ();
call_on_buffer ?debug ?filename ~command ~timelimit ~memlimit ~regexps buffer
let call_on_file ?debug ?filename
~command ~timelimit ~memlimit ~regexps filename =
let buffer = file_contents_buf filename in
call_on_buffer ?debug ?filename ~command ~timelimit ~memlimit ~regexps buffer
*)
(*
let is_true_cygwin = Sys.os_type = "Cygwin"
......
......@@ -129,26 +129,27 @@ type driver = {
drv_printer : printer option;
drv_prelude : string list;
drv_filename : string option;
drv_transform : task tlist_reg;
drv_transform : task trans_reg;
drv_thprelude : string list Mid.t;
drv_translations : (translation * translation) Mid.t;
drv_regexps : (Str.regexp * Call_provers.prover_answer) list;
drv_exitcodes : (int * Call_provers.prover_answer) list;
}
(** register transformations *)
(** register printers and transformations *)
let (transforms : (string, task tlist_reg) Hashtbl.t) = Hashtbl.create 17
let register_transform_l name trans = Hashtbl.replace transforms name trans
let register_transform name t = register_transform_l name (singleton t)
let list_transforms () = Hashtbl.fold (fun k _ acc -> k::acc) transforms []
(** register printers *)
let (printers : (string, printer) Hashtbl.t) = Hashtbl.create 17
let printers : (string, printer) Hashtbl.t = Hashtbl.create 17
let register_printer name printer = Hashtbl.replace printers name printer
let list_printers () = Hashtbl.fold (fun k _ acc -> k::acc) printers []
let transforms : (string, task trans_reg) Hashtbl.t = Hashtbl.create 17
let register_transform name trans = Hashtbl.replace transforms name trans
let list_transforms () = Hashtbl.fold (fun k _ acc -> k::acc) transforms []
let transforms_l : (string, task tlist_reg) Hashtbl.t = Hashtbl.create 17
let register_transform_l name trans = Hashtbl.replace transforms_l name trans
let list_transforms_l () = Hashtbl.fold (fun k _ ac -> k::ac) transforms_l []
(** parse a driver file *)
let load_plugin dir (byte,nat) =
......@@ -224,7 +225,7 @@ let load_driver env file =
let exitcodes = ref [] in
let filename = ref None in
let printer = ref None in
let transform = ref identity_l in
let transform = ref identity in
let set_or_raise loc r v error = match !r with
| Some _ -> errorm ~loc "duplicate %s" error
| None -> r := Some v
......@@ -247,7 +248,7 @@ let load_driver env file =
try set_or_raise loc printer (Hashtbl.find printers s) "printer"
with Not_found -> errorm ~loc "unknown printer %s" s end
| Transform s -> begin
try transform := compose_l (Hashtbl.find transforms s) !transform
try transform := compose (Hashtbl.find transforms s) !transform
with Not_found -> errorm ~loc "unknown transformation %s" s end
| Plugin files -> load_plugin (Filename.dirname file) files
in
......@@ -290,10 +291,6 @@ let query_ident drv clone =
(** using drivers *)
let apply_transforms drv =
(* apply_clone drv.drv_raw.drv_transforms drv.drv_env drv.drv_clone *)
apply_env drv.drv_transform drv.drv_env
let print_prelude drv used fmt =
let pr_pr s () = Format.fprintf fmt "%s@\n" s in
List.fold_right pr_pr drv.drv_prelude ();
......@@ -313,6 +310,7 @@ let print_prelude drv used fmt =
Format.fprintf fmt "@."
let print_task drv fmt task =
let task = apply_env drv.drv_transform drv.drv_env task in
let printer = match drv.drv_printer with
| None -> errorm "no printer specified in the driver file"
| Some p -> p (query_ident drv (task_clone task))
......
......@@ -56,20 +56,18 @@ val register_printer : string -> printer -> unit
val register_transform : string -> task Register.trans_reg -> unit
val register_transform_l : string -> task Register.tlist_reg -> unit
val list_printers : unit -> string list
val list_transforms : unit -> string list
val list_printers : unit -> string list
val list_transforms : unit -> string list
val list_transforms_l : unit -> string list
(** {2 use a driver} *)
val apply_transforms : driver -> task -> task list
(** transform task *)
val file_of_task : driver -> string -> string -> task -> string
(** file_of_task input_file theory_name task *)
val print_task : driver -> formatter -> task -> unit
(** print a task *)
val file_of_task : driver -> string -> string -> task -> string
(** file_of_task input_file theory_name task *)
val prove_task :
?debug : bool ->
command : string ->
......
......@@ -285,10 +285,6 @@ let do_task _env drv fname tname (th : Why.Theory.theory) (task : Task.task) =
Driver.print_task drv (formatter_of_out_channel cout) task;
close_out cout
let do_task env drv fname tname th task =
let tasks = Driver.apply_transforms drv task in
List.iter (do_task env drv fname tname th) tasks
let do_theory env drv fname tname th glist =
if !opt_print_theory then
printf "%a@." Pretty.print_theory th
......
......@@ -1466,22 +1466,19 @@ let try_prover ~debug ~timelimit ~memlimit ~prover ~command ~driver
if debug then Format.printf "setting attempt status to Scheduled@.";
External_proof.set_status db attempt Scheduled;
if debug then Format.eprintf "Task : %a@." Why.Pretty.print_task g.task;
let task =
try
match Why.Driver.apply_transforms driver g.task with
| [t] -> t
| _ -> assert false
with Why.Driver.Error e ->
Format.eprintf "Db.try_prover: apply_transforms reports %a@." Why.Driver.report e;
raise Exit
| e ->
try
Printexc.print (fun () -> raise e) ()
with _ -> raise Exit
in
if debug then Format.eprintf "Task for prover: %a@." (Why.Driver.print_task driver) task;
if debug then Format.eprintf "Task for prover: %a@." (Why.Driver.print_task driver) g.task;
let callback =
Why.Driver.prove_task ~debug ~command ~timelimit ~memlimit driver task
try
Why.Driver.prove_task ~debug ~command ~timelimit ~memlimit driver g.task
with
| Why.Driver.Error e ->
Format.eprintf "Db.try_prover: prove_task reports %a@."
Why.Driver.report e;
raise Exit
| e ->
try
Printexc.print (fun () -> raise e) ()
with _ -> raise Exit
in
fun () ->
if debug then Format.printf "setting attempt status to Running@.";
......
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