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

new implementation of bisect using at each step eliminate_definition

parent 6d29a830
......@@ -370,103 +370,3 @@ let () = Exn_printer.register (fun fmt exn -> match exn with
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
type bisect_step =
| BSdone of task
| BSstep of task * (bool -> bisect_step)
(*
Simple version
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
*)
let rec bisect_aux cont task lt i lk =
if i < 2 then
let res0 b =
if b then cont [] else
(assert (List.length lt = 1); cont lt) in
try BSstep (merge task lk, res0) with UnknownIdent _ -> res0 false
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 *)
let res1 b =
if b
then bisect_aux cont task lt1 i1 lk
else
let res2 b =
if b
then bisect_aux cont task lt2 i2 lk
else
let c1 lt2 =
let lk2 = List.append lt2 lk in
let c2 lt1 = cont (List.append lt1 lt2) in
bisect_aux c2 task lt1 i1 lk2 in
bisect_aux c1 task1 lt2 i2 lk in
try BSstep (merge (merge task lt2) lk, res2)
with UnknownIdent _ -> res2 false in
try BSstep (merge task1 lk,res1) with UnknownIdent _ -> res1 false
let bisect_step 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 c1 lt =
BSdone (add_tdecl (merge task lt) goal) in
bisect_aux c1 task lt i [goal]
let bisect f task =
let rec run = function
| BSdone r -> r
| BSstep (t,c) -> run (c (f t)) in
run (bisect_step task)
......@@ -93,19 +93,6 @@ val split_theory : theory -> Spr.t option -> task -> task list
that end by one of [s]. They are in the opposite order than
in the theory *)
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 *)
type bisect_step =
| BSdone of task
| BSstep of task * (bool -> bisect_step)
val bisect_step : task -> bisect_step
(** Same as before but doing it step by step *)
(** {2 realization utilities} *)
val used_theories : task -> theory Mid.t
......
......@@ -27,6 +27,17 @@ let debug = Debug.register_info_flag "ide_info"
~desc:"About why3ide."
let () = Debug.set_flag debug
(** set the exception call back handler to the Exn_printer of why3 *)
let () = (***** TODO TODO make that work, it seems not called!!! *)
let why3_handler exn =
Format.eprintf "@[Why3ide callback raised an exception:@\n%a@]@.@."
Exn_printer.exn_printer exn;
(** print the stack trace if asked to (can't be done by the usual way) *)
if Debug.test_flag Debug.stack_trace then
Printf.eprintf "Backtrace:\n%t\n%!" Printexc.print_backtrace
in
GtkSignal.user_handler := why3_handler
(* config file *)
(* type altern_provers = prover option Mprover.t *)
......
......@@ -970,20 +970,15 @@ let bisect_proof_attempt pa =
if b then set_timelimit res;
let r = c b in
match r with
| Task.BSdone t2 ->
| Eliminate_definition.BSdone [] ->
dprintf debug "Bisecting doesn't reduced the task.@."
| Eliminate_definition.BSdone reml ->
dprintf debug "Bisecting done.@.";
let t1 = S.goal_task pa.S.proof_parent in
if Task.task_equal t2 t1 then
dprintf debug "But doesn't reduced the task.@."
else
begin try
let keygen = MA.keygen in
let notify = MA.notify in
let diff =
Trans.apply (Trans.apply Eliminate_definition.compute_diff t1) t2 in
(* we know that this metas are registered *)
let diff = List.map (fun (m,l) -> m.Theory.meta_name,l) diff in
let metas = S.add_registered_metas ~keygen eS diff pa.S.proof_parent in
let reml = List.map (fun (m,l) -> m.Theory.meta_name,l) reml in
let metas = S.add_registered_metas ~keygen eS reml pa.S.proof_parent in
let trans = S.add_registered_transformation ~keygen
eS "eliminate_builtin" metas.S.metas_goal in
let goal = List.hd trans.S.transf_goals in (* only one *)
......@@ -994,11 +989,13 @@ let bisect_proof_attempt pa =
with e ->
dprintf debug "Bisecting error:@\n%a@."
Exn_printer.exn_printer e end
| Task.BSstep (t,c) ->
| Eliminate_definition.BSstep (t,c) ->
assert (not lp.S.prover_config.C.in_place); (* TODO do this case *)
M.schedule_proof_attempt
~timelimit:!timelimit
~memlimit:pa.S.proof_memlimit
?old:(S.get_edited_as_abs eS.S.session pa)
(** It is dangerous, isn't it? to be in place for bisecting? *)
~inplace:lp.S.prover_config.C.in_place
~command:(C.get_complete_command lp.S.prover_config)
~driver:lp.S.prover_driver
......@@ -1020,12 +1017,12 @@ let bisect_proof_attempt pa =
then dprintf debug "Initial task can't be proved.@."
else
let t = S.goal_task pa.S.proof_parent in
let r = Task.bisect_step t in
let r = Eliminate_definition.bisect_step t in
match r with
| Task.BSdone res ->
assert (Task.task_equal res t);
| Eliminate_definition.BSdone res ->
assert (res = []);
dprintf debug "Task can't be reduced.@."
| Task.BSstep (t,c) ->
| Eliminate_definition.BSstep (t,c) ->
set_timelimit res;
match S.load_prover eS pa.S.proof_prover with
| None -> (* No prover so we do nothing *)
......
......@@ -433,19 +433,25 @@ let do_task drv fname tname (th : Theory.theory) (task : Task.task) =
exit 1
| Some dir, Some command when !opt_bisect ->
let test task =
let call = Driver.prove_task_prepared
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;
res.Call_provers.pr_answer = Call_provers.Valid in
let prepared_task = Driver.prepare_task drv task in
if not (test prepared_task)
if not (test task)
then printf "I can't bisect %s %s %s which is not valid@." fname tname
(task_goal task).Decl.pr_name.Ident.id_string
else
let prepared_task = Task.bisect test prepared_task in
let rem = Eliminate_definition.bisect test task in
let goal,task = Task.task_separate_goal task in
let task = List.fold_left
(fun task (m,ml) -> Task.add_meta task m ml) task rem in
let task = add_tdecl task goal in
(** We suppose here that the first transformation in the driver
is remove_builtin *)
let prepared_task = Driver.prepare_task drv 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
......
......@@ -840,6 +840,7 @@ let print_decls ~old info fmt dl =
fprintf fmt "@\n@[<hov>%a@\n@]" (print_list nothing (print_decl ~old info)) dl
let print_task env pr thpr _blacklist realize ?old fmt task =
(* eprintf "Task:%a@.@." Pretty.print_task task; *)
forget_all ();
print_prelude fmt pr;
print_th_prelude task fmt thpr;
......@@ -866,6 +867,7 @@ let print_task env pr thpr _blacklist realize ?old fmt task =
Mid.map (fun (th,s) -> fprintf fmt "Require %s.@\n" s; th) realized_theories in
let realized_symbols = Task.used_symbols realized_theories' in
let local_decls = Task.local_decls task realized_symbols in
eprintf "local_decls:%i@." (List.length local_decls);
(* associate a special printer to each symbol in a realized theory *)
let symbol_printers =
let printers =
......
......@@ -34,7 +34,7 @@ let add_id undef_ls rem_ls (ls,ld) (abst,defn) =
(** TODO: go further? such as constructor that are removed? *)
let elim undef_ls rem_pr rem_ls rem_ts d = match d.d_node with
let elim_abstract undef_ls rem_pr rem_ls rem_ts d = match d.d_node with
| Dlogic l ->
let ld, id = List.fold_right (add_id undef_ls rem_ls) l ([],[]) in
ld @ (if id = [] then [] else [create_logic_decl id])
......@@ -54,7 +54,7 @@ let eliminate_builtin =
Trans.on_tagged_pr Printer.meta_remove_prop (fun rem_pr ->
Trans.on_tagged_ls Printer.meta_remove_logic (fun rem_ls ->
Trans.on_tagged_ts Printer.meta_remove_type_symbol (fun rem_ts ->
Trans.decl (elim undef_ls rem_pr rem_ls rem_ts) None))))
Trans.decl (elim_abstract undef_ls rem_pr rem_ls rem_ts) None))))
let () = Trans.register_transform "eliminate_builtin" eliminate_builtin
~desc_metas:[Printer.meta_syntax_logic,
......@@ -181,3 +181,140 @@ let () =
recursive@ definition (at@ least@ two@ functions@ or@ \
predicates@ defined@ at@ the@ same@ time)";
(** Bisect *)
open Task
open Theory
type bisect_step =
| BSdone of (Theory.meta * Theory.meta_arg list) list
| BSstep of task * (bool -> bisect_step)
type rem = { rem_pr : Spr.t; rem_ls : Sls.t; rem_ts : Sts.t }
let print_rem fmt rem = Format.fprintf fmt
"@[rem_pr:@[%a@]@\nrem_ls:@[%a@]@\nrem_ts:@[%a@]@\n"
(Pp.print_iter1 Spr.iter Pp.comma Pretty.print_pr) rem.rem_pr
(Pp.print_iter1 Sls.iter Pp.comma Pretty.print_ls) rem.rem_ls
(Pp.print_iter1 Sts.iter Pp.comma Pretty.print_ts) rem.rem_ts
let rec elim_task task rem =
match task with
| Some ({task_decl = {td_node = Decl decl}} as task) ->
let task = elim_task task.task_prev rem in
let l = elim_abstract Sls.empty
rem.rem_pr rem.rem_ls rem.rem_ts decl in
List.fold_left Task.add_decl task l
| Some task ->
Task.add_tdecl (elim_task task.task_prev rem) task.task_decl
| None -> None
let add_rem rem decl =
let remove_ts rem ts =
{ rem with rem_ts = Sts.add ts rem.rem_ts} in
let remove_ls rem ls =
{ rem with rem_ls = Sls.add ls rem.rem_ls} in
let remove_pr rem pr =
{ rem with rem_pr = Spr.add pr rem.rem_pr} in
match decl.d_node with
| Dtype ts -> remove_ts rem ts
| Ddata l -> List.fold_left (fun rem (ts,_) -> remove_ts rem ts) rem l
| Dparam ls -> remove_ls rem ls
| Dlogic l -> List.fold_left (fun rem (ls,_) -> remove_ls rem ls) rem l
| Dind (_,l) -> List.fold_left (fun rem (ls,_) -> remove_ls rem ls) rem l
| Dprop (_,pr,_) -> remove_pr rem pr
let union_rem rem1 rem2 =
{ rem_ts = Sts.union rem1.rem_ts rem2.rem_ts;
rem_ls = Sls.union rem1.rem_ls rem2.rem_ls;
rem_pr = Spr.union rem1.rem_pr rem2.rem_pr;
}
let create_meta_rem_list rem =
let remove_ts acc ts =
(Printer.meta_remove_type_symbol, [Theory.MAts ts])::acc in
let remove_ls acc ls =
(Printer.meta_remove_logic, [Theory.MAls ls])::acc in
let remove_pr acc pr =
(Printer.meta_remove_prop, [Theory.MApr pr])::acc in
let acc = Sts.fold_left remove_ts [] rem.rem_ts in
let acc = Sls.fold_left remove_ls acc rem.rem_ls in
let acc = Spr.fold_left remove_pr acc rem.rem_pr in
acc
let fold_sub f acc a i1 i2 =
let acc = ref acc in
for i=i1 to i2-1 do
acc := f !acc a.(i)
done;
!acc
let rec bisect_aux task a i1 i2 rem cont (* lt i lk *) =
(* Format.eprintf "i1: %i, i2: %i@\nrem:%a@." i1 i2 *)
(* print_rem rem; *)
let call rem valid invalid =
try BSstep (elim_task task rem,
fun b -> if b then valid () else invalid ())
with UnknownIdent _ -> invalid ()
in
if i2 - i1 < 2 then
let rem1 = add_rem rem a.(i1) in
call rem1
(fun () -> assert (i2 - i1 = 1); cont rem1)
(fun () -> cont rem)
else
let m = (i1+i2)/2 in
let rem1 = fold_sub add_rem rem a m i2 in
call rem1
(fun () -> bisect_aux task a i1 m rem1 cont)
(fun () ->
bisect_aux task a m i2 rem
(fun rem1 -> (* rem c rem1 c \old(rem1) *)
let rem2 = fold_sub add_rem rem1 a i1 m in
call rem2
(fun () -> cont rem2)
(fun () -> bisect_aux task a i1 m rem1 cont)))
let bisect_step task0 =
let task= match task0 with
| Some {task_decl = {td_node = Decl {d_node = Dprop (Pgoal,_,_)}};
task_prev = task} -> task
| _ -> raise GoalNotFound in
let rec length acc = function
| Some {task_decl = {td_node = Decl _};
task_prev = t} -> length (acc + 1) t
| Some {task_prev = t} -> length acc t
| None -> acc in
let n = length 0 task in
let a = Array.create n (Obj.magic 0) in
let rec init acc = function
| Some {task_decl = {td_node = Decl d}; task_prev = t} ->
a.(acc) <- d; init (acc - 1) t
| Some { task_prev = t} -> init acc t
| None -> assert (acc = -1) in
init (n-1) task;
let empty_rem = {rem_ts = Sts.empty; rem_ls = Sls.empty;
rem_pr = Spr.empty} in
bisect_aux task0 a 0 n empty_rem
(fun rem -> BSdone (create_meta_rem_list rem))
let bisect f task =
let rec run = function
| BSdone r -> r
| BSstep (t,c) -> run (c (f t)) in
run (bisect_step task)
(** catch exception for debug *)
(* let bisect_step task0 = *)
(* let res = try bisect_step task0 with exn -> *)
(* Format.eprintf "bisect_step fail: %a@." Exn_printer.exn_printer exn; *)
(* raise exn in *)
(* match res with *)
(* | BSdone _ as d -> d *)
(* | BSstep (t,f) -> BSstep (t,fun b -> try f b with exn -> *)
(* Format.eprintf "bisect_step fail: %a@." Exn_printer.exn_printer exn; *)
(* raise exn) *)
......@@ -31,3 +31,18 @@ val eliminate_definition_pred : Task.task Trans.trans
val eliminate_definition : Task.task Trans.trans
val eliminate_mutual_recursion: Task.task Trans.trans
(** bisection *)
val bisect : (Task.task -> bool) ->
Task.task -> (Theory.meta * Theory.meta_arg list) list
(** [bisect test task] return metas that specify the symbols that
can be removed without making the task invalid for
the function test. *)
type bisect_step =
| BSdone of (Theory.meta * Theory.meta_arg list) list
| BSstep of Task.task * (bool -> bisect_step)
val bisect_step : Task.task -> bisect_step
(** Same as before but doing it step by step *)
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