Commit fa117c16 authored by Sylvain Dailler's avatar Sylvain Dailler

Optional task as label for printing functions

parent 9ab18d32
......@@ -1306,10 +1306,10 @@ let why3tac ?(timelimit=timelimit) s gl =
let command = String.concat " " (cp.command :: cp.extra_options) in
if debug then Format.printf "@[%a@]@\n---@." Pretty.print_task !task;
if debug then Format.printf "@[%a@]@\n---@."
(fun fmt -> Driver.print_task drv fmt None) !task;
(fun fmt -> Driver.print_task drv fmt) !task;
let limit =
{ Call_provers.empty_limit with Call_provers.limit_time = timelimit } in
let call = Driver.prove_task ~command ~limit drv None !task in
let call = Driver.prove_task ~command ~limit drv !task in
wait_on_call call
with
| NotFO ->
......
......@@ -298,13 +298,13 @@ let prepare_task ~cntexample drv task =
let task = update_task drv task in
List.fold_left apply task transl
let print_task_prepared ?old drv fmt tables task =
let print_task_prepared ?old ?name_table drv fmt task =
let p = match drv.drv_printer with
| None -> raise NoPrinter
| Some p -> p
in
let printer_args = { Printer.env = drv.drv_env;
name_table = tables;
name_table = name_table;
prelude = drv.drv_prelude;
th_prelude = drv.drv_thprelude;
blacklist = drv.drv_blacklist;
......@@ -314,14 +314,14 @@ let print_task_prepared ?old drv fmt tables task =
fprintf fmt "@[%a@]@?" (printer ?old) task;
printer_args.printer_mapping
let print_task ?old ?(cntexample=false) drv fmt tables task =
let print_task ?old ?(cntexample=false) ?name_table drv fmt task =
let task = prepare_task ~cntexample drv task in
let _ = print_task_prepared ?old drv fmt tables task in
let _ = print_task_prepared ?old ?name_table drv fmt task in
()
let print_theory ?old drv fmt tables th =
let print_theory ?old ?name_table drv fmt th =
let task = Task.use_export None th in
print_task ?old drv fmt tables task
print_task ?old ?name_table drv fmt task
let file_name_of_task ?old ?inplace drv task =
match old, inplace with
......@@ -334,12 +334,12 @@ let file_name_of_task ?old ?inplace drv task =
let fn = try Filename.chop_extension fn with Invalid_argument _ -> fn in
get_filename drv fn "T" pr.pr_name.id_string
let prove_task_prepared ~command ~limit ?old ?inplace drv tables task =
let prove_task_prepared ~command ~limit ?old ?inplace ?name_table drv task =
let buf = Buffer.create 1024 in
let fmt = formatter_of_buffer buf in
let old_channel = Opt.map open_in old in
let filename = file_name_of_task ?old ?inplace drv task in
let printer_mapping = print_task_prepared ?old:old_channel drv fmt tables task in
let printer_mapping = print_task_prepared ?old:old_channel ?name_table drv fmt task in
pp_print_flush fmt ();
Opt.iter close_in old_channel;
let res =
......@@ -349,9 +349,9 @@ let prove_task_prepared ~command ~limit ?old ?inplace drv tables task =
res
let prove_task ~command ~limit ?(cntexample=false) ?old
?inplace drv tables task =
?inplace ?name_table drv task =
let task = prepare_task ~cntexample drv task in
prove_task_prepared ~command ~limit ?old ?inplace drv tables task
prove_task_prepared ~command ~limit ?old ?inplace ?name_table drv task
(* exception report *)
......
......@@ -46,11 +46,13 @@ val call_on_buffer :
val print_task :
?old : in_channel ->
?cntexample : bool ->
driver -> Format.formatter -> Task.name_tables option -> Task.task -> unit
?name_table: Task.name_tables ->
driver -> Format.formatter -> Task.task -> unit
val print_theory :
?old : in_channel ->
driver -> Format.formatter -> Task.name_tables option -> Theory.theory -> unit
?name_table: Task.name_tables ->
driver -> Format.formatter -> Theory.theory -> unit
(** produce a realization of the given theory using the given driver *)
val prove_task :
......@@ -59,21 +61,24 @@ val prove_task :
?cntexample : bool ->
?old : string ->
?inplace : bool ->
driver -> Task.name_tables option -> Task.task -> Call_provers.prover_call
?name_table : Task.name_tables ->
driver -> Task.task -> Call_provers.prover_call
(** Split the previous function in two simpler functions *)
val prepare_task : cntexample:bool -> driver -> Task.task -> Task.task
val print_task_prepared :
?old : in_channel ->
driver -> Format.formatter -> Task.name_tables option -> Task.task -> Printer.printer_mapping
?name_table: Task.name_tables ->
driver -> Format.formatter -> Task.task -> Printer.printer_mapping
val prove_task_prepared :
command : string ->
limit : Call_provers.resource_limit ->
?old : string ->
?inplace : bool ->
driver -> Task.name_tables option -> Task.task -> Call_provers.prover_call
?name_table : Task.name_tables ->
driver -> Task.task -> Call_provers.prover_call
(** Traverse all metas from a driver *)
......
......@@ -407,7 +407,7 @@ let build_prover_call c id pr limit callback =
let tables = Session_itp.get_tables c.controller_session id in
let call =
Driver.prove_task ?old:None ~cntexample:true ~inplace:false ~command
~limit driver tables task
~limit ?name_table:tables driver task
in
let pa = (c.controller_session,id,pr,callback,false,call) in
Queue.push pa prover_tasks_in_progress
......
......@@ -722,7 +722,7 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
let task = get_task cont.controller_session id in
let tables = get_tables cont.controller_session id in
let s = Pp.string_of
(fun fmt -> Driver.print_task ~cntexample:false task_driver fmt tables)
(fun fmt -> Driver.print_task ~cntexample:false ?name_table:tables task_driver fmt)
task in
P.notify (Task (nid,s))
| _ ->
......
......@@ -1975,7 +1975,7 @@ let copy_external_proof
let ch = open_out dst_file in
let fmt = formatter_of_out_channel ch in
(* Do not need tables because not a case in itp *)
Driver.print_task ~old driver fmt None task;
Driver.print_task ~old driver fmt task;
close_in old;
close_out ch;
let dst_file = Sysutil.relativize_filename dir dst_file in
......@@ -2024,7 +2024,7 @@ let update_edit_external_proof ~cntexample env_session a =
let ch = open_out file in
let fmt = formatter_of_out_channel ch in
(* Name table is only used in ITP printing *)
Driver.print_task ~cntexample ?old driver fmt None goal;
Driver.print_task ~cntexample ?old driver fmt goal;
Opt.iter close_in old;
close_out ch;
file
......
......@@ -195,7 +195,7 @@ let idle_handler t =
(* Name table are not used outside ITP *)
let call =
Driver.prove_task ?old ~cntexample ~inplace ~command
~limit driver None goal
~limit driver goal
in
let pa = Check_prover (callback,false,call) in
Queue.push pa t.proof_attempts_queue;
......
......@@ -245,7 +245,7 @@ let output_task drv fname _tname th task dir =
let ext = String.sub dest i (String.length dest - i) in
let cout = open_out (Filename.concat dir (name ^ ext)) in
(* Name tables not necessary outside of ITP *)
Driver.print_task drv (formatter_of_out_channel cout) None task;
Driver.print_task drv (formatter_of_out_channel cout) task;
close_out cout
let output_task_prepared drv fname _tname th task dir =
......@@ -261,7 +261,7 @@ let output_task_prepared drv fname _tname th task dir =
let cout = open_out (Filename.concat dir (name ^ ext)) in
(* TODO print the counterexample *)
(* Name tables not necessary outside ITP *)
let _counterexample = Driver.print_task_prepared drv (formatter_of_out_channel cout) None task in
let _counterexample = Driver.print_task_prepared drv (formatter_of_out_channel cout) task in
close_out cout
let output_theory drv fname _tname th task dir =
......@@ -278,7 +278,7 @@ let output_theory drv fname _tname th task dir =
end else None in
let cout = open_out file in
(* Name table is not necessary outside ITP *)
Driver.print_task ?old drv (formatter_of_out_channel cout) None task;
Driver.print_task ?old drv (formatter_of_out_channel cout) task;
close_out cout
let do_task drv fname tname (th : Theory.theory) (task : Task.task) =
......@@ -290,14 +290,14 @@ let do_task drv fname tname (th : Theory.theory) (task : Task.task) =
| None, Some command ->
(* Name tables not necessary outside ITP *)
let call =
Driver.prove_task ~command ~limit ~cntexample:!opt_cntexmp drv None task in
Driver.prove_task ~command ~limit ~cntexample:!opt_cntexmp drv task in
let res = Call_provers.wait_on_call call in
printf "%s %s %s : %a@." fname tname
(task_goal task).Decl.pr_name.Ident.id_string
Call_provers.print_prover_result res
| None, None ->
(* Name tables not necessary outside ITP *)
Driver.print_task ~cntexample:!opt_cntexmp drv std_formatter None task
Driver.print_task ~cntexample:!opt_cntexmp drv std_formatter task
| Some dir, _ -> output_task drv fname tname th task dir
let do_tasks env drv fname tname th task =
......
......@@ -101,7 +101,7 @@ let do_global_theory (_tname,p,t) =
end else None in
let cout = open_out file in
(* Name tables not necessary outside of ITP *)
Driver.print_task ?old opt_driver (formatter_of_out_channel cout) None task;
Driver.print_task ?old opt_driver (formatter_of_out_channel cout) task;
close_out cout
let () =
......
......@@ -80,7 +80,7 @@ let run_one env config filters dir fname =
let cout = open_out (Filename.concat dir (name ^ ext)) in
(* Name table not necessary outside of ITP *)
Driver.print_task lp.prover_driver
(formatter_of_out_channel cout) None task;
(formatter_of_out_channel cout) task;
close_out cout
) th
) file
......
......@@ -3,7 +3,7 @@
- obsolete
- update proof attempt
*)
(*
open Why3
open Unix_scheduler
open Format
......@@ -347,3 +347,4 @@ let () =
(fun () -> List.iter
(fun n -> treat_notification fmt n) (get_notified ()); true);
Unix_scheduler.main_loop (interp chout fmt)
*)
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