Commit 790abd8b authored by Andrei Paskevich's avatar Andrei Paskevich

optional parameter 'old' for printers

parent 72f9215b
......@@ -33,7 +33,7 @@ type prelude_map = prelude Mid.t
type 'a pp = formatter -> 'a -> unit
type printer = prelude -> prelude_map -> task pp
type printer = prelude -> prelude_map -> ?old:in_channel -> task pp
let printers : (string, printer) Hashtbl.t = Hashtbl.create 17
......
......@@ -31,7 +31,7 @@ type prelude_map = prelude Mid.t
type 'a pp = Format.formatter -> 'a -> unit
type printer = prelude -> prelude_map -> task pp
type printer = prelude -> prelude_map -> ?old:in_channel -> task pp
val register_printer : string -> printer -> unit
......
......@@ -233,7 +233,7 @@ let update_task drv task =
in
add_tdecl task goal
let print_task drv fmt task =
let print_task ?old drv fmt task =
let p = match drv.drv_printer with
| None -> raise NoPrinter
| Some p -> p
......@@ -248,12 +248,12 @@ let print_task drv fmt task =
(*Format.printf "@\n@\nTASK";*)
let task = update_task drv task in
let task = List.fold_left apply task transl in
fprintf fmt "@[%a@]@?" printer task
fprintf fmt "@[%a@]@?" (printer ?old) task
let prove_task ~command ?timelimit ?memlimit drv task =
let prove_task ~command ?timelimit ?memlimit ?old drv task =
let buf = Buffer.create 1024 in
let fmt = formatter_of_buffer buf in
print_task drv fmt task; pp_print_flush fmt ();
print_task ?old drv fmt task; pp_print_flush fmt ();
call_on_buffer ~command ?timelimit ?memlimit drv buf
(* exception report *)
......
......@@ -41,11 +41,13 @@ val call_on_buffer :
driver -> Buffer.t -> unit -> Call_provers.prover_result
val print_task :
?old : in_channel ->
driver -> Format.formatter -> Task.task -> unit
val prove_task :
command : string ->
?timelimit : int ->
?memlimit : int ->
driver -> Task.task -> unit -> Call_provers.prover_result
?old : in_channel ->
driver -> Task.task -> (unit -> Call_provers.prover_result)
......@@ -227,7 +227,8 @@ let print_task pr thpr fmt task =
ignore (print_list_opt (add_flush newline2) (print_decl info) fmt decls)
let () = register_printer "alt-ergo"
(fun pr thpr fmt task ->
(fun pr thpr ?old fmt task ->
ignore old;
forget_all ident_printer;
print_task pr thpr fmt task)
......
......@@ -337,7 +337,8 @@ let print_decl info fmt d = match d.d_node with
let print_decls info fmt dl =
fprintf fmt "@[<hov>%a@\n@]" (print_list nothing (print_decl info)) dl
let print_task pr thpr fmt task =
let print_task pr thpr ?old fmt task =
ignore old;
forget_all ();
print_prelude fmt pr;
print_th_prelude task fmt thpr;
......
......@@ -189,7 +189,8 @@ let print_task pr thpr fmt task =
ignore (print_list_opt (add_flush newline2) (print_decl info) fmt decls)
let () = register_printer "simplify"
(fun pr thpr fmt task ->
(fun pr thpr ?old fmt task ->
ignore old;
forget_all ident_printer;
print_task pr thpr fmt task)
......@@ -218,6 +218,7 @@ let print_task pr thpr fmt task =
fprintf fmt "@\n)@."
let () = register_printer "smtv1"
(fun pr thpr fmt task ->
(fun pr thpr ?old fmt task ->
ignore old;
forget_all ident_printer;
print_task pr thpr fmt task)
......@@ -162,7 +162,8 @@ let print_task pr thpr fmt task =
ignore (print_list_opt (add_flush newline2) (print_decl info) fmt decls)
let () = register_printer "tptp"
(fun pr thpr fmt task ->
(fun pr thpr ?old fmt task ->
ignore old;
forget_all ident_printer;
print_task pr thpr fmt task)
......@@ -391,7 +391,8 @@ let print_tdecl fmt td = match td.td_node with
fprintf fmt "@[<hov 2>(* meta %s %a *)@]@\n@\n"
m.meta_name (print_list comma print_meta_arg) al
let print_task pr thpr fmt task =
let print_task pr thpr ?old fmt task =
ignore old;
forget_all ();
print_prelude fmt pr;
print_th_prelude task fmt thpr;
......
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