Commit 343f4048 authored by Sylvain Dailler's avatar Sylvain Dailler

Added calls to prover in IDE.

parent 5ac21137
......@@ -366,12 +366,6 @@ let remove_children iter =
ignore (goals_model#remove (goals_model#iter_children (Some iter)))
else ()
(*
match (goals_model#iter_children row_reference) with
| None -> ()
| iter -> goals_model#remove iter
*)
(* Callback of a proof_attempt *)
let callback_update_tree_proof _ses row_ref _id name =
fun panid pa_status ->
......@@ -394,55 +388,17 @@ let callback_update_tree_proof _ses row_ref _id name =
| Running -> () (* TODO: set icon to 'play' *)
| _ -> () (* TODO ? *)
(* TODO to be replaced *)
(* Return the prover corresponding to given name. name is of the form
| name
| name, version
| name, altern
| name, version, altern *)
let return_prover fmt name =
let fp = Whyconf.parse_filter_prover name in
(** all provers that have the name/version/altern name *)
let provers = Whyconf.filter_provers gconfig.config fp in
if Whyconf.Mprover.is_empty provers then begin
fprintf fmt "Prover corresponding to %s has not been found@." name;
None
end else
Some (snd (Whyconf.Mprover.choose provers))
let test_schedule_proof_attempt ses =
let test_schedule_proof_attempt ses (p: Whyconf.config_prover) limit =
match !current_selected_index with
| IproofNode id ->
let row_ref = Hpn.find pn_id_to_gtree id in
(* TODO put this somewhere else *)
let name, limit = match ["Alt-Ergo,1.01"; "10"] with
(* TODO recover this
| [name] ->
let default_limit = Call_provers.{limit_time = Whyconf.timelimit main;
limit_mem = Whyconf.memlimit main;
limit_steps = 0} in
name, default_limit*)
| [name; timeout] -> name, Call_provers.{empty_limit with
limit_time = int_of_string timeout}
| [name; timeout; oom ] ->
name, Call_provers.{limit_time = int_of_string timeout;
limit_mem = int_of_string oom;
limit_steps = 0}
| _ -> printf "Bad arguments prover_name, version timeout memlimit@.";
"", Call_provers.empty_limit
in
let np = return_prover Format.std_formatter name in (* TODO std_formatter dummy argument *)
(match np with
| None -> ()
| Some p ->
let np = Pp.string_of Whyconf.print_prover p.Whyconf.prover in
let callback = callback_update_tree_proof ses row_ref id np in
let prover = p.Whyconf.prover in
let printing = prover.Whyconf.prover_name ^ "(" ^ prover.Whyconf.prover_version ^ ")" in
let callback = callback_update_tree_proof ses row_ref id printing in
C.schedule_proof_attempt
cont id p.Whyconf.prover
~limit ~callback)
| _ -> () (* TODO *)
(* | _ -> printf "Give the prover name@."*)
cont id prover
~limit ~callback
| _ -> message_zone#buffer#set_text ("Must be on a proof node to use a prover.")
let clear_command_entry () = command_entry#set_text ""
......@@ -455,13 +411,18 @@ let interp cmd =
apply_transform cont.controller_session s args
| Query s ->
message_zone#buffer#set_text s
| Other(s,_args) ->
| Other(s,args) ->
begin
match parse_prover_name gconfig.config s args with
| Some (prover_config, limit) ->
clear_command_entry ();
test_schedule_proof_attempt cont.controller_session prover_config limit
| None ->
match s with
| "s" -> clear_command_entry ();
run_strategy_on_task "1"
| "c" -> clear_command_entry ();
test_schedule_proof_attempt cont.controller_session
| _ -> message_zone#buffer#set_text ("unknown command '"^s^"'")
end
let (_ : GtkSignal.id) =
command_entry#connect#activate
......
......@@ -171,3 +171,47 @@ let interp env s =
Transform (cmd,t,args)
with Trans.UnknownTrans _ ->
Other(cmd,args)
(********* Callbacks tools *******)
(* Return the prover corresponding to given name. name is of the form
| name
| name, version
| name, altern
| name, version, altern *)
let return_prover name config =
let fp = Whyconf.parse_filter_prover name in
(** all provers that have the name/version/altern name *)
let provers = Whyconf.filter_provers config fp in
if Whyconf.Mprover.is_empty provers then begin
Format.eprintf "Prover corresponding to %s has not been found@." name;
None
end else
Some (snd (Whyconf.Mprover.choose provers))
(* Parses the Other command. If it fails to parse it, it answers None otherwise
it returns the config of the prover together with the ressource_limit *)
let parse_prover_name config name args :
(Whyconf.config_prover * Call_provers.resource_limit) option =
let main = Whyconf.get_main config in
match (return_prover name config) with
| None -> None
| Some prover_config ->
begin
if (List.length args > 2) then None else
match args with
| [] ->
let default_limit = Call_provers.{limit_time = Whyconf.timelimit main;
limit_mem = Whyconf.memlimit main;
limit_steps = 0} in
Some (prover_config, default_limit)
| [timeout] -> Some (prover_config,
Call_provers.{empty_limit with
limit_time = int_of_string timeout})
| [timeout; oom ] ->
Some (prover_config, Call_provers.{limit_time = int_of_string timeout;
limit_mem = int_of_string oom;
limit_steps = 0})
| _ -> Format.eprintf "Parse_prover_name. Should not happen. Please report@."; None
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