Commit f0ebb813 authored by MARCHE Claude's avatar MARCHE Claude

ebauche de bisect

parent 8ab1a7ed
......@@ -821,6 +821,17 @@ let copy_detached ~copy c from_any =
(* Only goal can be detached *)
| _ -> raise (BadCopyDetached "copy_detached. Can only copy goal")
(***************** {2 replay} ****************)
type report =
| Result of Call_provers.prover_result * Call_provers.prover_result
(** Result(new_result,old_result) *)
......@@ -881,7 +892,6 @@ let replay ?(obsolete_only=true) ?(use_steps=false)
r := (id, pr, limits, Prover_not_installed) :: !r;
in
(* === replay === *)
let session = c.controller_session in
let count = ref 0 in
let report = ref [] in
......@@ -920,4 +930,112 @@ let replay ?(obsolete_only=true) ?(use_steps=false)
(* Calling replay on all the proof_attempts of the session *)
Session_itp.session_iter_proof_attempt replay_pa session
(*************** bisect **********)
let debug = Debug.register_flag ~desc:"Task bisection" "bisect"
let bisect_proof_attempt ~notification c pa_id =
let ses = c.controller_session in
let pa = get_proof_attempt_node ses pa_id in
let goal_id = pa.parent in
let prover = pa.prover in
let limit = { pa.limit with
Call_provers.limit_steps =
Call_provers.empty_limit.Call_provers.limit_steps }
in
let timelimit = ref (-1) in
let set_timelimit res =
timelimit := 1 + (int_of_float (floor res.Call_provers.pr_time)) in
let rec callback kont _pa_id = function
| Running | Scheduled -> ()
| Interrupted ->
Debug.dprintf debug "Bisecting interrupted.@."
| Unedited | JustEdited -> assert false
| Uninstalled _ -> assert false
| InternalFailure exn ->
(* Perhaps the test can be considered false in this case? *)
Debug.dprintf debug "Bisecting interrupted by an error %a.@."
Exn_printer.exn_printer exn
| Done res ->
let b = res.Call_provers.pr_answer = Call_provers.Valid in
Debug.dprintf debug "Bisecting: %a.@."
Call_provers.print_prover_result res;
if b then set_timelimit res;
match kont b with
| Eliminate_definition.BSdone rem ->
if Decl.Spr.is_empty rem.Eliminate_definition.rem_pr &&
Term.Sls.is_empty rem.Eliminate_definition.rem_ls &&
Ty.Sts.is_empty rem.Eliminate_definition.rem_ts
then
Debug.dprintf debug "Bisecting doesn't reduced the task.@."
else
begin
Debug.dprintf debug "Bisecting done.@.";
()
(*
begin try
let keygen = MA.keygen in
let notify = MA.notify in
let reml = List.map (fun (m,l) -> m.Theory.meta_name,l) reml in
let metas = S.add_registered_metas ~keygen ses reml pa.S.proof_parent in
let trans = S.add_registered_transformation ~keygen
ses "eliminate_builtin" metas.S.metas_goal in
let goal = List.hd trans.S.transf_goals in (* only one *)
let npa = S.copy_external_proof ~notify ~keygen ~obsolete:true
~goal ~env_session:ses pa in
MA.init_any (S.Metas metas);
M.run_external_proof ses sched ~cntexample npa
with e ->
dprintf debug "Bisecting error:@\n%a@."
Exn_printer.exn_printer e end
*)
end
| Eliminate_definition.BSstep (rem,kont) ->
schedule_proof_attempt
c goal_id prover
~counterexmp:false
~limit:{ limit with Call_provers.limit_time = !timelimit; }
~callback:(callback kont)
~notification
in
(* Run once the complete goal in order to verify its validity and
update the proof attempt *)
let first_callback pa_id = function
(* this pa_id can be different from the first pa_id *)
| Running | Scheduled -> ()
| Interrupted ->
Debug.dprintf debug "Bisecting interrupted.@."
| Unedited | JustEdited | Uninstalled _ -> assert false
| InternalFailure exn ->
Debug.dprintf debug "proof of the initial task interrupted by an error %a.@."
Exn_printer.exn_printer exn
| Done res ->
if res.Call_provers.pr_answer <> Call_provers.Valid
then Debug.dprintf debug "Initial task can't be proved.@."
else
let t = get_raw_task ses goal_id in
let r = Eliminate_definition.bisect_step t in
match r with
| Eliminate_definition.BSdone res ->
Debug.dprintf debug "Task can't be reduced.@."
| Eliminate_definition.BSstep (rem,kont) ->
set_timelimit res;
schedule_proof_attempt
c goal_id prover
~counterexmp:false
~limit:{ limit with Call_provers.limit_time = !timelimit}
~callback:(callback kont)
~notification
in
Debug.dprintf debug "Bisecting with %a started.@."
Whyconf.print_prover prover;
schedule_proof_attempt
c goal_id prover ~counterexmp:false ~limit ~callback:first_callback ~notification
end
......@@ -306,4 +306,7 @@ a list of 4-uples [(goalID, prover, limits, report)]
*)
val bisect_proof_attempt:
notification:notifier -> controller -> proofAttemptID -> unit
end
......@@ -195,16 +195,25 @@ let () =
eliminate_definition_if_poly
~desc:"Same@ as@ eliminate_definition@ but@ only@ if@ polymorphism@ appear."
(** Bisect *)
(***** {2 Bisection} ********)
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 }
type bisect_step =
| BSdone of rem
| BSstep of rem * (bool -> bisect_step)
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
......@@ -244,6 +253,7 @@ let _union_rem rem1 rem2 =
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, [Theory.MAts ts])::acc in
......@@ -255,6 +265,7 @@ let create_meta_rem_list rem =
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
......@@ -267,7 +278,7 @@ 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,
try BSstep (rem,
fun b -> if b then valid () else invalid ())
with UnknownIdent _ -> invalid ()
in
......@@ -310,12 +321,12 @@ let bisect_step task0 =
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))
(fun rem -> BSdone rem)
let bisect f task =
let rec run = function
| BSdone r -> r
| BSstep (t,c) -> run (c (f t)) in
| BSstep (rem,c) -> let t = elim_task task rem in run (c (f t)) in
run (bisect_step task)
(** catch exception for debug *)
......
......@@ -25,15 +25,16 @@ val eliminate_mutual_recursion: Task.task Trans.trans
(** bisection *)
val bisect : (Task.task -> bool) ->
Task.task -> (Theory.meta * Theory.meta_arg list) list
type rem = { rem_pr : Decl.Spr.t; rem_ls : Term.Sls.t; rem_ts : Ty.Sts.t }
val bisect : (Task.task -> bool) -> Task.task -> rem
(** [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)
| BSdone of rem
| BSstep of rem * (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