Commit f259ae47 authored by François Bobot's avatar François Bobot

--bisect : (with -o dir and -P prover) instead of creating a file

with the task pretty printed, it reduce the set of axioms to a minimal
 set of declaration which still prove the goal and pretty print it.

Currently it does the bisection on the goal already prepared for the prover
parent 9013fabd
......@@ -316,3 +316,49 @@ let () = Exn_printer.register (fun fmt exn -> match exn with
Format.fprintf fmt "Metaproperty '%s' is not exclusive" m.meta_name
| _ -> raise exn)
(* task1 : prefix
lt : to reduce
lk : suffix (reverse order)
i : length of lt
*)
let rec split i l acc = match i,l with
| 0, l -> List.rev acc, l
| _, [] -> assert false
| n, a::l -> split (pred n) l (a::acc)
let merge task l = List.fold_left add_tdecl task l
let rec bisect_aux f task lt i lk =
if i < 2 then
if try f (merge task lk) with UnknownIdent _ -> false then [] else
(assert (List.length lt = 1); lt)
else
let i1 = i/2 in
let i2 = i/2 + i mod 2 in
let lt1,lt2 = split i1 lt [] in
let task1 = merge task lt1 in (** Can't fail *)
(** These "if then else" allow to remove big chunck with one call to f *)
if try f (merge task1 lk) with UnknownIdent _ -> false
then bisect_aux f task lt1 i1 lk
else
if try f (merge (merge task lt2) lk) with UnknownIdent _ -> false
then bisect_aux f task lt2 i2 lk
else
let lt2 = bisect_aux f task1 lt2 i2 lk in
let lk2 = List.append lt2 lk in
let lt1 = bisect_aux f task lt1 i1 lk2 in
List.append lt1 lt2
let bisect f task =
let task,goal = match task with
| Some {task_decl = {td_node = Decl {d_node = Dprop (Pgoal,_,_)}} as td;
task_prev = task} -> task,td
| _ -> raise GoalNotFound in
let lt,i,tacc = task_fold (fun (acc,i,tacc) td ->
match td.td_node with
| Decl _ -> (td::acc,succ i,tacc)
| _ -> (acc,i,td::tacc)) ([],0,[]) task in
let task = merge None tacc in
let lt = bisect_aux f task lt i [goal] in
add_tdecl (merge task lt) goal
......@@ -120,3 +120,8 @@ exception GoalFound
exception SkipFound
exception LemmaFound
val bisect : (task -> bool) -> task -> task
(** [bisect test task] return a task included in [task] which is at
the limit of truthness of the function test. The returned task is
included in [task] and if any declarations are removed from it the
task doesn't verify test anymore *)
......@@ -236,14 +236,7 @@ let update_task drv task =
in
add_tdecl task goal
let print_task ?old drv fmt task =
let p = match drv.drv_printer with
| None -> raise NoPrinter
| Some p -> p
in
let printer =
lookup_printer p drv.drv_env drv.drv_prelude drv.drv_thprelude
in
let prepare_task drv task =
let lookup_transform t = t, lookup_transform t drv.drv_env in
let transl = List.map lookup_transform drv.drv_transform in
let apply task (_t, tr) =
......@@ -253,16 +246,37 @@ let print_task ?old drv fmt task =
(*Format.printf "@\n@\nTASK";*)
let task = update_task drv task in
let task = List.fold_left apply task transl in
task
let print_task_prepared ?old drv fmt task =
let p = match drv.drv_printer with
| None -> raise NoPrinter
| Some p -> p
in
let printer =
lookup_printer p drv.drv_env drv.drv_prelude drv.drv_thprelude
in
fprintf fmt "@[%a@]@?" (printer ?old) task
let prove_task ~command ?timelimit ?memlimit ?old drv task =
let print_task ?old drv fmt task =
let task = prepare_task drv task in
print_task_prepared ?old drv fmt task
let prove_task_prepared ~command ?timelimit ?memlimit ?old drv task =
let buf = Buffer.create 1024 in
let fmt = formatter_of_buffer buf in
print_task ?old drv fmt task; pp_print_flush fmt ();
print_task_prepared ?old drv fmt task; pp_print_flush fmt ();
let res = call_on_buffer ~command ?timelimit ?memlimit drv buf in
Buffer.reset buf;
res
let prove_task ~command ?timelimit ?memlimit ?old drv task =
let task = prepare_task drv task in
prove_task_prepared ~command ?timelimit ?memlimit ?old drv task
(* exception report *)
let string_of_qualid thl idl =
......
......@@ -43,6 +43,7 @@ val call_on_buffer :
?memlimit : int ->
driver -> Buffer.t -> Call_provers.pre_prover_call
val print_task :
?old : in_channel ->
driver -> Format.formatter -> Task.task -> unit
......@@ -54,3 +55,18 @@ val prove_task :
?old : in_channel ->
driver -> Task.task -> Call_provers.pre_prover_call
(** Split the previous function in two simpler function *)
val prepare_task : driver -> Task.task -> Task.task
val print_task_prepared :
?old : in_channel ->
driver -> Format.formatter -> Task.task -> unit
val prove_task_prepared :
command : string ->
?timelimit : int ->
?memlimit : int ->
?old : in_channel ->
driver -> Task.task -> Call_provers.pre_prover_call
(***)
......@@ -100,6 +100,7 @@ let opt_timelimit = ref None
let opt_memlimit = ref None
let opt_command = ref None
let opt_task = ref None
let opt_bisect = ref false
let opt_print_theory = ref false
let opt_print_namespace = ref false
......@@ -141,7 +142,8 @@ let option_list = Arg.align [
"--prover", Arg.String (fun s -> opt_prover := Some s),
" same as -P";
"--coq-realize", Arg.String (fun s -> opt_coq_realization := Some s),
" produce, in given file, a Coq realization of the theory given using -T";
" produce, in given file, a Coq realization of the theory given \
using -T";
"-F", Arg.String (fun s -> opt_parser := Some s),
"<format> Select input format (default: \"why\")";
"--format", Arg.String (fun s -> opt_parser := Some s),
......@@ -170,6 +172,9 @@ let option_list = Arg.align [
"<dir> Print the selected goals to separate files in <dir>";
"--output", Arg.String (fun s -> opt_output := Some s),
" same as -o";
"--bisect", Arg.Set opt_bisect,
" Reduce the set of needed axioms which prove a goal, \
and output the resulting task";
"--print-theory", Arg.Set opt_print_theory,
" Print selected theories";
"--print-namespace", Arg.Set opt_print_namespace,
......@@ -304,10 +309,20 @@ let () =
eprintf "Option '-m'/'--memlimit' requires a prover.@.";
exit 1
end;
if !opt_bisect then begin
eprintf "Option '--bisect' requires a prover.@.";
exit 1
end;
if !opt_driver = None && not !opt_print_namespace then
opt_print_theory := true
end;
if !opt_bisect && !opt_output = None then begin
eprintf "Option '--bisect' require a directory to output the result.@.";
exit 1
end;
opt_loadpath := List.rev_append !opt_loadpath (Whyconf.loadpath main);
if !opt_timelimit = None then opt_timelimit := Some (Whyconf.timelimit main);
if !opt_memlimit = None then opt_memlimit := Some (Whyconf.memlimit main);
......@@ -345,17 +360,7 @@ let print_th_namespace fmt th =
let fname_printer = ref (Ident.create_ident_printer [])
let do_task drv fname tname (th : Why.Theory.theory) (task : Task.task) =
match !opt_output, !opt_command with
| None, Some command ->
let call = Driver.prove_task ~command ~timelimit ~memlimit 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 ->
Driver.print_task drv std_formatter task
| Some dir, _ ->
let output_task drv fname _tname th task dir =
let fname = Filename.basename fname in
let fname =
try Filename.chop_extension fname with _ -> fname
......@@ -370,6 +375,48 @@ let do_task drv fname tname (th : Why.Theory.theory) (task : Task.task) =
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
Driver.print_task_prepared drv (formatter_of_out_channel cout) task;
close_out cout
let do_task drv fname tname (th : Why.Theory.theory) (task : Task.task) =
match !opt_output, !opt_command with
| Some dir, Some command when !opt_bisect ->
(* Should we test that the full task in proved? *)
let test task =
let call = Driver.prove_task_prepared
~command ~timelimit ~memlimit 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;
res.Call_provers.pr_answer = Call_provers.Valid in
let prepared_task = Driver.prepare_task drv task in
let prepared_task = Task.bisect test prepared_task in
output_task_prepared drv fname tname th prepared_task dir
| None, Some command ->
let call = Driver.prove_task ~command ~timelimit ~memlimit 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 ->
Driver.print_task drv std_formatter task
| Some dir, _ -> output_task drv fname tname th task dir
let do_tasks env drv fname tname th task =
let lookup acc t =
(try Trans.singleton (Trans.lookup_transform t env) with
......
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