Commit ebd28e68 authored by MARCHE Claude's avatar MARCHE Claude

strategies: run them on all selection, recursively

parent 96addbf6
......@@ -929,8 +929,7 @@ let apply_trans_on_selection tr =
let a = get_any_from_row_reference r in
M.transform (env_session()) sched
~context_unproved_goals_only:!context_unproved_goals_only
tr
a)
tr a)
(get_selected_row_references ())
......@@ -938,11 +937,9 @@ let apply_strategy_on_selection str =
List.iter
(fun r ->
let a = get_any_from_row_reference r in
match a with
| S.Goal g ->
M.run_strategy_on_goal (env_session()) sched
str g
| _ -> ())
M.run_strategy (env_session()) sched
~context_unproved_goals_only:!context_unproved_goals_only
str a)
(get_selected_row_references ())
......@@ -1460,7 +1457,7 @@ let strategies () :
]
*)
let loaded_strategies = ref []
let loaded_strategies = ref []
let strategies () =
match !loaded_strategies with
......
......@@ -938,7 +938,7 @@ let convert_unknown_prover =
(SyntaxError
("unable to parse goto argument '" ^ n ^ "' as an integer"))
in
if g < 0 || g > max then
if g < 0 || g > max then
raise
(SyntaxError ("goto index " ^ n ^ " is invalid"));
Igoto g
......@@ -961,7 +961,7 @@ let convert_unknown_prover =
(SyntaxError
("unable to parse timelimit argument '" ^ t ^ "'"))
in
if timelimit <= 0 then
if timelimit <= 0 then
raise
(SyntaxError ("timelimit " ^ t ^ " is invalid"));
let memlimit =
......@@ -971,7 +971,7 @@ let convert_unknown_prover =
(SyntaxError
("unable to parse memlimit argument '" ^ m ^ "'"))
in
if memlimit <= 0 then
if memlimit <= 0 then
raise
(SyntaxError ("memlimit " ^ m ^ " is invalid"));
Icall_prover(p.Whyconf.prover,timelimit,memlimit)
......@@ -979,11 +979,11 @@ let convert_unknown_prover =
raise (SyntaxError "'c' expects exactly three arguments")
| ["t";t;n] ->
let () =
try
try
let _ = Trans.lookup_transform t env.env in
()
with Trans.UnknownTrans _ ->
try
try
let _ = Trans.lookup_transform_l t env.env in
()
with Trans.UnknownTrans _->
......@@ -996,7 +996,7 @@ let convert_unknown_prover =
(SyntaxError
("unable to parse argument '" ^ n ^ "' as an integer"))
in
if g < 0 || g > max then
if g < 0 || g > max then
raise
(SyntaxError ("index " ^ n ^ " is invalid"));
Itransform(t,g)
......@@ -1056,6 +1056,21 @@ let convert_unknown_prover =
let callback () = exec_strategy es sched 0 strat g in
schedule_delayed_action sched callback
let run_strategy_on_goal_or_children ~context_unproved_goals_only
eS sched strat g =
goal_iter_leaf_goal ~unproved_only:context_unproved_goals_only
(run_strategy_on_goal eS sched strat) g
let rec run_strategy eS sched ~context_unproved_goals_only strat a =
match a with
| Goal g | Proof_attempt {proof_parent = g} ->
run_strategy_on_goal_or_children ~context_unproved_goals_only
eS sched strat g
| _ ->
iter (run_strategy ~context_unproved_goals_only eS sched strat) a
end
......
......@@ -327,6 +327,11 @@ module Make(O: OBSERVER) : sig
O.key Session.env_session -> t ->
strategy -> O.key Session.goal -> unit
val run_strategy:
O.key Session.env_session -> t ->
context_unproved_goals_only:bool ->
strategy -> O.key Session.any -> unit
end
......
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