Commit da374ddf authored by MARCHE Claude's avatar MARCHE Claude

itp: ability to run strategies

parent 465f57f3
......@@ -204,8 +204,8 @@ LIB_WHYML = mlw_ty mlw_expr mlw_decl mlw_pretty mlw_wp mlw_module \
mlw_main mlw_interp
LIB_SESSION = compress xml termcode session session_itp \
controller_itp session_tools strategy strategy_parser \
session_scheduler
session_tools strategy strategy_parser \
controller_itp session_scheduler
LIBMODULES = $(addprefix src/util/, $(LIB_UTIL)) \
$(addprefix src/core/, $(LIB_CORE)) \
......
......@@ -30,9 +30,17 @@ type transformation_status =
let print_trans_status fmt st =
match st with
| TSscheduled -> fprintf fmt "TScheduled"
| TSdone tid -> fprintf fmt "TSdone" (* TODO print tid *)
| TSdone _tid -> fprintf fmt "TSdone" (* TODO print tid *)
| TSfailed -> fprintf fmt "TSfailed"
type strategy_status = STSgoto of proofNodeID * int | STShalt
let print_strategy_status fmt st =
match st with
| STSgoto(id,n) -> fprintf fmt "goto step %d in proofNode %a" n print_proofNodeID id
| STShalt -> fprintf fmt "halt"
open Ident
type proof_state = {
......@@ -41,7 +49,7 @@ type proof_state = {
pn_state : bool Hpn.t;
}
let init_proof_state ses =
let init_proof_state _ses =
{th_state = Hid.create 7;
tn_state = Htn.create 42;
pn_state = Hpn.create 42}
......@@ -214,27 +222,97 @@ let schedule_proof_attempt c id pr ~limit ~callback =
let schedule_transformation_r c id name args ~callback =
let apply_trans () =
let task = get_task c.controller_session id in
try
let subtasks = Trans.apply_transform_args name c.controller_env args task in
let tid = graft_transf c.controller_session id name args subtasks in
callback (TSdone tid);
false
with e when not (Debug.test_flag Debug.stack_trace) ->
Format.eprintf
"@[Exception raised in Trans.apply_transform %s:@ %a@.@]"
begin
try
let subtasks = Trans.apply_transform_args name c.controller_env args task in
(* if result is same as input task, consider it as a failure *)
begin
match subtasks with
| [t'] when Task.task_equal t' task ->
callback TSfailed
| _ ->
let tid = graft_transf c.controller_session id name args subtasks in
callback (TSdone tid)
end
with e when not (Debug.test_flag Debug.stack_trace) ->
Format.eprintf
"@[Exception raised in Trans.apply_transform %s:@ %a@.@]"
name Exn_printer.exn_printer e;
callback TSfailed;
false
callback TSfailed
end;
false
in
S.idle ~prio:0 apply_trans;
callback TSscheduled
let schedule_transformation c id name args ~callback =
let callback s = (match s with
| TSdone tid -> update_trans_node c tid false (*(get_sub_tasks c.controller_session tid = [])*) (* TODO need to change schedule transformation to get the id ? *)
| TSdone tid -> update_trans_node c tid false
(*(get_sub_tasks c.controller_session tid = [])*)
(* TODO need to change schedule transformation to get the id ? *)
| TSfailed -> ()
| _ -> ()); callback s in
schedule_transformation_r c id name args ~callback:callback
schedule_transformation_r c id name args ~callback
open Strategy
let run_strategy_on_goal c id strat ~callback =
let rec exec_strategy pc strat g =
if pc < 0 || pc >= Array.length strat then
callback STShalt
else
match Array.get strat pc with
| Icall_prover(p,timelimit,memlimit) ->
let callback res =
match res with
| Scheduled | Running -> (* nothing to do yet *) ()
| Done { Call_provers.pr_answer = Call_provers.Valid } ->
(* proof succeeded, nothing more to do *)
callback STShalt
| Interrupted | InternalFailure _
| Done _ ->
(* proof did not succeed, goto to next step *)
callback (STSgoto (g,pc+1));
let run_next () = exec_strategy (pc+1) strat g; false in
S.idle ~prio:0 run_next
| Unedited | JustEdited ->
(* should not happen *)
assert false
in
let limit = { Call_provers.empty_limit with
Call_provers.limit_time = timelimit;
limit_mem = memlimit} in
schedule_proof_attempt c g p ~limit ~callback
| Itransform(trname,pcsuccess) ->
let callback ntr =
match ntr with
| TSfailed -> (* transformation failed *)
callback (STSgoto (g,pc+1));
let run_next () = exec_strategy (pc+1) strat g; false in
S.idle ~prio:0 run_next
| TSscheduled -> ()
| TSdone tid ->
List.iter
(fun g ->
callback (STSgoto (g,pcsuccess));
let run_next () =
exec_strategy pcsuccess strat g; false
in
S.idle ~prio:0 run_next)
(get_sub_tasks c.controller_session tid);
(*Todo._done todo*) ()
in
schedule_transformation c g trname [] ~callback
| Igoto pc ->
callback (STSgoto (g,pc));
exec_strategy pc strat g
in
exec_strategy 0 strat id
let read_file env ?format fn =
let theories = Env.read_file Env.base_language env ?format fn in
......@@ -264,7 +342,7 @@ let add_file c ?format fname =
find a corresponding new theory resp. old goal are kept, with
tasks associated to them *)
let merge_file (old_ses : session) (c : controller) _ file =
let _merge_file (old_ses : session) (c : controller) _ file =
let format = file.file_format in
let old_theories = file.file_theories in
let new_theories =
......
......@@ -27,6 +27,10 @@ type transformation_status = TSscheduled | TSdone of transID | TSfailed
val print_trans_status : Format.formatter -> transformation_status -> unit
type strategy_status = STSgoto of proofNodeID * int | STShalt
val print_strategy_status : Format.formatter -> strategy_status -> unit
module type Scheduler = sig
(** Any module of this signature should implement a scheduler,
......@@ -109,6 +113,16 @@ val schedule_transformation :
the transformation status changes. Typically at Scheduled, then
Done tid.*)
val run_strategy_on_goal :
controller ->
proofNodeID ->
Strategy.t ->
callback:(strategy_status -> unit) -> unit
(** [run_strategy_on_goal c id strat] executes asynchronously the
strategy [strat] on the goal [id]. TODO: add callback to get
inform of the progress *)
val add_file : controller -> ?format:Env.fformat -> string -> unit
(** [add_file_to_session cont ?fmt fname] parses the source file
[fname] and add the resulting theories to the session of [cont] *)
......
......@@ -9,6 +9,9 @@ let debug = Debug.register_info_flag "session_itp"
type transID = int
type proofNodeID = int
let print_proofNodeID fmt id =
Format.fprintf fmt "%d" id
type theory = {
theory_name : Ident.ident;
theory_goals : proofNodeID list;
......@@ -236,7 +239,7 @@ let rec print_proof_node s (fmt: Format.formatter) p =
| Trans id -> (get_transfNode s id).transf_name
in
fprintf fmt
"@[<hv 2> Goal %s;@ parent %s;@ sum %s;@ @[<hov 2>[%a]@]@ @[<hov 2>[%a]@]@]"
"@[<hv 1> Goal %s;@ parent %s;@ sum %s;@ @[<hv 1>[%a]@]@ @[<hv 1>[%a]@]@]"
pn.proofn_name.id_string parent
(Opt.fold (fun _ a -> Termcode.string_of_checksum a) "None" pn.proofn_checksum)
(Pp.print_list Pp.semi print_proof_attempt)
......@@ -249,7 +252,7 @@ and print_trans_node s fmt id =
let name = tn.transf_name in
let l = tn.transf_subtasks in
let parent = (get_proofNode s tn.transf_parent).proofn_name.id_string in
fprintf fmt "@[<hv 2> Trans %s; args %a; parent %s;@ [%a]@]" name (Pp.print_list Pp.colon pp_print_string) args parent
fprintf fmt "@[<hv 1> Trans %s;@ args %a;@ parent %s;@ [%a]@]" name (Pp.print_list Pp.colon pp_print_string) args parent
(Pp.print_list Pp.semi (print_proof_node s)) l
......
......@@ -17,6 +17,8 @@ unique identifiers of type [proofNodeId]
type session
type proofNodeID
val print_proofNodeID : Format.formatter -> proofNodeID -> unit
type transID
module Hpn: Exthtbl.S with type key = proofNodeID
......
......@@ -392,7 +392,7 @@ let rec print_proof_node s (fmt: Format.formatter) p =
fprintf fmt "P";
fprintf fmt
"@[<hv 2> Goal %s; parent %s;@ @[<hov 2>[%a]@]@ @[<hov 2>[%a]@]@]"
"@[<hv 2>{ Goal=%s;@ parent=%s;@ @[<hv 1>[%a]@]@ @[<hv 1>[%a]@] }@]"
(get_proof_name s p).Ident.id_string parent
(Pp.print_list Pp.semi print_proof_attempt)
(get_proof_attempts s p)
......@@ -408,17 +408,17 @@ and print_trans_node s fmt id =
let parent = (get_proof_name s (get_trans_parent s id)).Ident.id_string in
if Controller_itp.tn_proved cont id then
fprintf fmt "P";
fprintf fmt "@[<hv 2> Trans %s; args %a; parent %s;@ [%a]@]" name (Pp.print_list Pp.semi pp_print_string) args parent
fprintf fmt "@[<hv 2>{ Trans=%s;@ args=%a;@ parent=%s;@ [%a] }@]" name (Pp.print_list Pp.semi pp_print_string) args parent
(Pp.print_list Pp.semi (print_proof_node s)) l
let print_theory s fmt th : unit =
if Controller_itp.th_proved cont (theory_name th) then
fprintf fmt "P";
fprintf fmt "@[<hv 2> Theory %s;@ [%a]@]" (theory_name th).Ident.id_string
fprintf fmt "@[<hv 1> Theory %s;@ [%a]@]" (theory_name th).Ident.id_string
(Pp.print_list Pp.semi (fun fmt a -> print_proof_node s fmt a)) (theory_goals th)
let print_file s fmt (file, thl) =
fprintf fmt "@[<hv 2> File %s;@ [%a]@]" file.file_name
fprintf fmt "@[<hv 1> File %s;@ [%a]@]" file.file_name
(Pp.print_list Pp.semi (print_theory s)) thl
let print_s s fmt =
......@@ -574,10 +574,28 @@ let strategies () =
let list_strategies _fmt _args =
let l = strategies () in
let pp_strat fmt (n,s,_,_) = fprintf fmt "%s: %s" s n in
let pp_strat fmt (n,s,desc,_) = fprintf fmt "%s (%s): %s" s n desc in
printf "@[<hov 2>== Known strategies ==@\n%a@]@."
(Pp.print_list Pp.newline pp_strat) l
let run_strategy _fmt args =
match args with
| [s] ->
let l = strategies () in
let st = List.filter (fun (_,c,_,_) -> c=s) l in
begin
match st with
| [(n,_,_,st)] ->
printf "running strategy '%s'@." n;
let id = nearest_goal () in
let callback sts =
printf "Strategy status: %a@." print_strategy_status sts
in
C.run_strategy_on_goal cont id st ~callback
| _ -> printf "Strategy '%s' not found@." s
end
| _ -> printf "Please give the strategy shortcut as argument@."
(*******)
......@@ -600,18 +618,19 @@ let commands =
"list-transforms", "list available transformations", list_transforms;
"list-strategies", "list available strategies", list_strategies;
"a", "<transname> <args>: apply the transformation <transname> with arguments <args>", apply_transform;
"t", "<transname> <args>: behave like a but add function to display into the callback", test_transform_and_display;
"t", "<transname> <args>: behave like 'a' but add function to display into the callback", test_transform_and_display;
"p", "print the session in raw form", dump_session_raw;
"c", "test schedule_proof_attempt with alt-ergo on the first goal", test_schedule_proof_attempt;
"g", "prints the first goal", test_print_goal;
"c", "<provername> [timelimit [memlimit]] run a prover on the current goal", test_schedule_proof_attempt;
"st", "<c> apply the strategy whose shortcut is 'c'", run_strategy;
"g", "prints the current goal", test_print_goal;
"r", "reload the session (test only)", test_reload;
"s", "[s my_session] save the current session in my_session.xml", test_save_session;
"ng", "get to the next goal", then_print (move_to_goal_ret_p next_node);
"pg", "get to the prev goal", then_print (move_to_goal_ret_p prev_node);
"gu", "get to the goal up", then_print (move_to_goal_ret_p zipper_up);
"gd", "get to the goal down", then_print (move_to_goal_ret_p zipper_down);
"gr", "get to the goal right", then_print (move_to_goal_ret_p zipper_right);
"gl", "get to the goal left", then_print (move_to_goal_ret_p zipper_left);
"s", "<file> save the current session in <file>.xml", test_save_session;
"ng", "go to the next goal", then_print (move_to_goal_ret_p next_node);
"pg", "go to the prev goal", then_print (move_to_goal_ret_p prev_node);
"gu", "go to the goal up", then_print (move_to_goal_ret_p zipper_up);
"gd", "go to the goal down", then_print (move_to_goal_ret_p zipper_down);
"gr", "go to the goal right", then_print (move_to_goal_ret_p zipper_right);
"gl", "go to the goal left", then_print (move_to_goal_ret_p zipper_left);
"pcur", "print tree rooted at current position", (print_position_p cont.controller_session zipper);
"test", "test register known_map",
(fun _ _ ->
......
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