Commit e07b4d55 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Remove unused code.

parent 5173ec5b
......@@ -240,37 +240,6 @@ let output_task drv fname _tname th task dir =
Driver.print_task drv (formatter_of_out_channel cout) task;
close_out cout
let output_task_prepared drv fname _tname th task dir =
let fname = Filename.basename fname in
let fname =
try Filename.chop_extension fname with _ -> fname in
let tname = th.th_name.Ident.id_string in
let dest = Driver.file_of_task drv fname tname task in
(* Uniquify the filename before the extension if it exists*)
let i = try String.rindex dest '.' with _ -> String.length dest in
let name = Ident.string_unique !fname_printer (String.sub dest 0 i) in
let ext = String.sub dest i (String.length dest - i) in
let cout = open_out (Filename.concat dir (name ^ ext)) in
(* TODO print the counterexample *)
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 =
let fname = Filename.basename fname in
let fname =
try Filename.chop_extension fname with _ -> fname in
let dest = Driver.file_of_theory drv fname th in
let file = Filename.concat dir dest in
let old =
if Sys.file_exists file then begin
let backup = file ^ ".bak" in
Sys.rename file backup;
Some (open_in backup)
end else None in
let cout = open_out file in
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) =
let limit =
{ Call_provers.empty_limit with
......
......@@ -17,8 +17,6 @@
open Lexing
open Why3
let output_comments = ref true
let newline lexbuf =
let pos = lexbuf.lex_curr_p in
lexbuf.lex_curr_p <-
......
......@@ -153,9 +153,6 @@ let run_normal dir filter_provers =
(** By time *)
let print_float_list =
Pp.print_list_delim ~start:Pp.lsquare ~stop:Pp.rsquare ~sep:Pp.semi Pp.float
let grab_valid_time provers_time provers pa =
let prover = pa.Session.proof_prover in
if Whyconf.Sprover.mem prover provers then
......
......@@ -48,8 +48,6 @@ let rec interactive to_remove =
| "n" -> false
| _ -> interactive to_remove
let keygen ?parent:_ _ = ()
let fname_printer = Ident.create_ident_printer []
let run_one env config filters dir fname =
......
......@@ -145,13 +145,6 @@ end
module M = Session_scheduler.Make(O)
let print_res fname pa ps old_ps =
dprintf verbose
"@[<hov 2>From file %s:@\nResult@ for@ the@ proof@ attempt@ %a:\
@ %a@\nPreviously@ it@ was@ %a@]@."
fname print_external_proof pa print_attempt_status ps
print_attempt_status old_ps
let print_proof_goal fmt pa =
pp_print_string fmt (goal_name pa.proof_parent).Ident.id_string
......@@ -167,13 +160,6 @@ let same_result r1 r2 =
| Call_provers.Failure f1, Call_provers.Failure f2 -> f1 = f2
| _ -> false
let same_status old_res new_res =
match old_res, new_res with
| InternalFailure old_exn, InternalFailure new_exn ->
(Printexc.to_string old_exn) = (Printexc.to_string new_exn)
| Done(old_res), Done(new_res) -> same_result old_res new_res
| _ -> false
let is_valid pr =
match pr.Call_provers.pr_answer with
| Call_provers.Valid -> true
......
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