Commit 4e26f72b authored by MARCHE Claude's avatar MARCHE Claude

add strategies in tools menu and in commands

parent e66b0a96
......@@ -446,6 +446,11 @@ let tools_menu = factory#add_submenu "_Tools"
let tools_factory = new GMenu.factory tools_menu ~accel_group
let strategies_factory =
let tools_submenu_strategies = tools_factory#add_submenu "Strategies" in
let ( _ : GMenu.menu_item) = tools_factory#add_separator () in
new GMenu.factory tools_submenu_strategies
let provers_factory =
let tools_submenu_provers = tools_factory#add_submenu "Provers" in
let ( _ : GMenu.menu_item) = tools_factory#add_separator () in
......@@ -1511,7 +1516,7 @@ let new_node ?parent (* ?(collapse=false) *) id name typ detached =
(**************************************************)
(* tools submenus for provers and transformations *)
(* tools submenus for strategies, provers and transformations *)
(**************************************************)
let sanitize_markup x =
......@@ -1527,6 +1532,18 @@ let string_of_desc desc =
let add_submenu_strategy (shortcut,strategy) =
let i = create_menu_item
strategies_factory
strategy
("run strategy " ^ strategy ^ " on selected goal (shortcut: " ^ shortcut ^ ")")
in
let callback () =
Debug.dprintf debug "[IDE INFO] interp command '%s'@." shortcut;
interp shortcut
in
connect_menu_item i ~callback
let add_submenu_prover (shortcut,prover) =
let i = create_menu_item
provers_factory
......@@ -1541,7 +1558,7 @@ let add_submenu_prover (shortcut,prover) =
let init_completion provers transformations commands =
let init_completion provers transformations strategies commands =
(* add the names of all the the transformations *)
List.iter add_completion_entry transformations;
(* add the name of the commands *)
......@@ -1560,8 +1577,7 @@ let init_completion provers transformations commands =
in
List.iter add_submenu_prover provers_sorted;
add_completion_entry "auto";
add_completion_entry "auto 2";
List.iter add_submenu_strategy strategies;
command_entry_completion#set_text_column completion_col;
command_entry_completion#set_match_func match_function;
......@@ -1578,9 +1594,9 @@ let () =
let callback () = interp name in
let i = create_menu_item submenu (sanitize_markup name) (string_of_desc desc) in
connect_menu_item i ~callback
in
let trans = List.filter filter transformations in
List.iter iter trans
in
let trans = List.filter filter transformations in
List.iter iter trans
in
add_submenu_transform
"transformations (a-e)"
......@@ -1743,7 +1759,7 @@ let treat_notification n =
Hint.remove node_id_pa id
| Initialized g_info ->
(* TODO: treat other *)
init_completion g_info.provers g_info.transformations g_info.commands;
init_completion g_info.provers g_info.transformations g_info.strategies g_info.commands;
| Saved ->
session_needs_saving := false;
print_message "Session saved.";
......
......@@ -78,6 +78,7 @@ type controller =
controller_env: Env.env;
controller_provers:
(Whyconf.config_prover * Driver.driver) Whyconf.Hprover.t;
controller_strategies : (string * string * Strategy.instruction array) Stdlib.Hstr.t;
}
......@@ -88,6 +89,7 @@ let create_controller config env ses =
controller_config = config;
controller_env = env;
controller_provers = Whyconf.Hprover.create 7;
controller_strategies = Stdlib.Hstr.create 7;
}
in
let provers = Whyconf.get_provers config in
......
......@@ -83,6 +83,7 @@ type controller = private
controller_config : Whyconf.config;
controller_env : Env.env;
controller_provers : (Whyconf.config_prover * Driver.driver) Whyconf.Hprover.t;
controller_strategies : (string * string * Strategy.instruction array) Stdlib.Hstr.t;
}
val create_controller: Whyconf.config -> Env.env -> Session_itp.session -> controller
......
......@@ -23,7 +23,7 @@ type global_information =
{
provers : (string * prover) list;
transformations : transformation list;
strategies : strategy list;
strategies : (string * strategy) list;
commands : string list;
(* hidden_provers : string list; *)
(* session_time_limit : int; *)
......
......@@ -24,7 +24,7 @@ type global_information =
{
provers : (string * prover) list;
transformations : transformation list;
strategies : strategy list;
strategies : (string * strategy) list;
commands : string list
(* hidden_provers : string list; *)
(* session_time_limit : int; *)
......
......@@ -75,10 +75,6 @@ let unproven_goals_below_id cont id =
| ATh th ->
List.rev (unproven_goals_below_th cont [] th)
(*******************)
(* Strategies list *)
(*******************)
let loaded_strategies = ref []
(****** Exception handling *********)
......@@ -982,11 +978,9 @@ end
let n = Pp.sprintf "%a" Whyconf.print_prover p in
(x,n) :: acc) (Whyconf.get_prover_shortcuts config) []
in
load_strategies c;
let transformation_list = List.map fst (list_transforms ()) in
let strategies_list =
let l = strategies d.cont.controller_env config loaded_strategies in
List.map (fun (a,_,_,_) -> a) l
in
let strategies_list = list_strategies c in
let infos =
{
provers = prover_list;
......@@ -1128,21 +1122,21 @@ end
let run_strategy_on_task ~counterexmp nid s =
let d = get_server_data () in
let unproven_goals = unproven_goals_below_id d.cont (any_from_node_ID nid) in
let l = strategies d.cont.controller_env d.cont.controller_config loaded_strategies in
let st = List.filter (fun (_,c,_,_) -> c=s) l in
match st with
| [(n,_,_,st)] ->
Debug.dprintf debug_strat "[strategy_exec] running strategy '%s'@." n;
let callback sts =
Debug.dprintf debug_strat "[strategy_exec] strategy status: %a@." print_strategy_status sts
in
let callback_pa = callback_update_tree_proof d.cont in
let callback_tr tr args st = callback_update_tree_transform tr args st in
List.iter (fun id ->
C.run_strategy_on_goal d.cont id st ~counterexmp
try
let (n,_,st) = Hstr.find d.cont.controller_strategies s in
Debug.dprintf debug_strat "[strategy_exec] running strategy '%s'@." n;
let callback sts =
Debug.dprintf debug_strat "[strategy_exec] strategy status: %a@." print_strategy_status sts
in
let callback_pa = callback_update_tree_proof d.cont in
let callback_tr tr args st = callback_update_tree_transform tr args st in
List.iter (fun id ->
C.run_strategy_on_goal d.cont id st ~counterexmp
~callback_pa ~callback_tr ~callback ~notification:(notify_change_proved d.cont))
unproven_goals
| _ -> Debug.dprintf debug_strat "[strategy_exec] strategy '%s' not found@." s
unproven_goals
with
Not_found ->
Debug.dprintf debug_strat "[strategy_exec] strategy '%s' not found@." s
(* ----------------- Clean session -------------------- *)
......@@ -1332,7 +1326,7 @@ end
| Command_req (nid, cmd) ->
begin
let snid = get_proof_node_id nid in
match (interp commands_table d.cont.controller_config d.cont snid cmd) with
match interp commands_table d.cont snid cmd with
| Transform (s, _t, args) -> treat_request (Transform_req (nid, s, args))
| Query s -> P.notify (Message (Query_Info (nid, s)))
| Prove (p, limit) ->
......
......@@ -27,10 +27,14 @@ let convert_infos (i: global_information) =
Record (convert_record ["prover_shorcut", String s;
"prover_name", String p])
in
let convert_strategy (s,p) =
Record (convert_record ["strategy_shorcut", String s;
"strategy_name", String p])
in
Record (convert_record
["provers", List (List.map convert_prover i.provers);
"transformations", List (List.map (fun x -> String x) i.transformations);
"strategies", List (List.map (fun x -> String x) i.strategies);
"strategies", List (List.map convert_strategy i.strategies);
"commands", List (List.map (fun x -> String x) i.commands)])
let convert_prover_answer (pa: prover_answer) =
......@@ -653,7 +657,10 @@ let parse_infos j =
get_string (get_field j "prover_name"))
with Not_found -> raise NotInfos) pr;
transformations = List.map (fun j -> match j with | String x -> x | _ -> raise NotInfos) tr;
strategies = List.map (fun j -> match j with | String x -> x | _ -> raise NotInfos) str;
strategies = List.map (fun j -> try
(get_string (get_field j "strategy_shortcut"),
get_string (get_field j "strategy_name"))
with Not_found -> raise NotInfos) str;
commands = List.map (fun j -> match j with | String x -> x | _ -> raise NotInfos) com}
with _ -> raise NotInfos
......
......@@ -137,6 +137,28 @@ let list_provers cont _args =
let l = List.sort String.compare l in
Pp.sprintf "%a" (Pp.print_list Pp.newline Pp.string) l
let load_strategies cont =
let config = cont.Controller_itp.controller_config in
let env = cont.Controller_itp.controller_env in
let strategies = Whyconf.get_strategies config in
Stdlib.Mstr.iter
(fun _ st ->
let name = st.Whyconf.strategy_name in
try
let code = st.Whyconf.strategy_code in
let code = Strategy_parser.parse env config code in
let shortcut = st.Whyconf.strategy_shortcut in
Debug.dprintf debug "[session server info] Strategy '%s' loaded.@." name;
Stdlib.Hstr.add cont.Controller_itp.controller_strategies shortcut
(name, st.Whyconf.strategy_desc, code)
with Strategy_parser.SyntaxError msg ->
Debug.dprintf debug
"[session server warning] Loading strategy '%s' failed: %s@." name msg)
strategies
let list_strategies cont =
Stdlib.Hstr.fold (fun s (a,_,_) acc -> (s,a)::acc) cont.Controller_itp.controller_strategies []
let symbol_name s =
match s with
......@@ -244,33 +266,6 @@ let help_on_queries fmt commands =
let p fmt (c,help) = Format.fprintf fmt "%20s : %s" c help in
Format.fprintf fmt "%a" (Pp.print_list Pp.newline p) l
let strategies env config loaded_strategies =
match !loaded_strategies with
| [] ->
let strategies = Whyconf.get_strategies config in
let strategies =
Stdlib.Mstr.fold_left
(fun acc _ st ->
let name = st.Whyconf.strategy_name in
try
let code = st.Whyconf.strategy_code in
let code = Strategy_parser.parse env config code in
let shortcut = st.Whyconf.strategy_shortcut in
Debug.dprintf debug "[session server info] Strategy '%s' loaded.@." name;
(name, shortcut, st.Whyconf.strategy_desc, code) :: acc
with Strategy_parser.SyntaxError msg ->
Debug.dprintf debug
"[session server warning] Loading strategy '%s' failed: %s@." name msg;
acc)
[]
strategies
in
let strategies = List.rev strategies in
loaded_strategies := strategies;
strategies
| l -> l
(* Return the prover corresponding to given name. name is of the form
| name
| name, version
......@@ -358,22 +353,18 @@ type command =
| QError of string
| Other of string * string list
let interp_others commands_table config cmd args =
match parse_prover_name config cmd args with
let interp_others commands_table cont cmd args =
match parse_prover_name cont.Controller_itp.controller_config cmd args with
| Some (prover_config, limit) ->
if prover_config.Whyconf.interactive then
Edit (prover_config)
else
Prove (prover_config, limit)
| None ->
if Stdlib.Hstr.mem cont.Controller_itp.controller_strategies cmd then
Strategies cmd
else
match cmd, args with
| "auto", _ ->
let s =
match args with
| "2"::_ -> "2"
| _ -> "1"
in
Strategies s
| "help", [trans] ->
let print_trans_desc fmt r =
Format.fprintf fmt "@[%s:\n%a@]" trans Pp.formatted r
......@@ -388,10 +379,10 @@ let interp_others commands_table config cmd args =
"Please type a command among the following (automatic completion available)@\n\
@\n\
@ <transformation name> [arguments]@\n\
@ <prover name> [<time limit> [<mem limit>]]@\n\
@ <prover shortcut> [<time limit> [<mem limit>]]@\n\
@ <query> [arguments]@\n\
@ <help transformation_name> @\n\
@ auto [auto level]@\n\
@ <strategy shortcut>@\n\
@ help <transformation_name> @\n\
@\n\
Available queries are:@\n@[%a@]" help_on_queries commands_table
in
......@@ -399,7 +390,7 @@ let interp_others commands_table config cmd args =
| _ ->
Other (cmd, args)
let interp commands_table config cont id s =
let interp commands_table cont id s =
let cmd,args = split_args s in
try
let (_,f) = Stdlib.Hstr.find commands_table cmd in
......@@ -424,7 +415,7 @@ let interp commands_table config cont id s =
else
Transform (cmd,t,args)
| None ->
interp_others commands_table config cmd args
interp_others commands_table cont cmd args
(***********************)
(* First Unproven goal *)
......
......@@ -40,13 +40,13 @@ type query =
val print_id: 'a -> Trans.naming_table -> string list -> string
val search_id: 'a -> Trans.naming_table -> string list -> string
val list_strategies : Controller_itp.controller -> (string * string) list
val list_provers: Controller_itp.controller -> _ -> string
val list_transforms: unit -> (string * Pp.formatted) list
val list_transforms_query: _ -> _ -> string
(* val help_on_queries: Format.formatter -> (string * string * 'a) list -> unit *)
val strategies: Env.env -> Whyconf.config ->
(string * string * string * Strategy.instruction array) list ref ->
(string * string * string * Strategy.instruction array) list
val load_strategies: Controller_itp.controller -> unit
(** Command line parsing tools *)
......@@ -64,9 +64,8 @@ type command =
val interp:
(string * query) Stdlib.Hstr.t ->
Whyconf.config ->
Controller_itp.controller ->
Session_itp.proofNodeID option -> string -> command
Controller_itp.controller ->
Session_itp.proofNodeID option -> string -> command
val get_first_unproven_goal_around:
......
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