Commit 9b299112 authored by Sylvain Dailler's avatar Sylvain Dailler

Modified server as discussed and adaptation to support former commans.

replay_print now takes a formatter.
Added messages and message_notification.
Added New_node.
Changing name of command request for disambiguation.
Changed parsing of IDE command line. (function interp).
parent 7ea0162a
......@@ -905,7 +905,7 @@ let clear_command_entry () = command_entry#set_text ""
let current_node_ID () = !current_selected_index
(*
(* TODO now split as notifications and inside session_user_interface
let interp cmd =
let id =
match !current_selected_index with
......
......@@ -559,12 +559,12 @@ let print_report fmt (r: report) =
Call_provers.print_prover_result new_r
(* TODO to be removed when we have a better way to print *)
let replay_print (lr: (proofNodeID * Whyconf.prover * Call_provers.resource_limit * report) list) =
let replay_print fmt (lr: (proofNodeID * Whyconf.prover * Call_provers.resource_limit * report) list) =
let pp_elem fmt (id, pr, rl, report) =
fprintf fmt "ProofNodeID: %d, Prover: %a, Timelimit?: %d, Result: %a@."
(Obj.magic id) Whyconf.print_prover pr rl.Call_provers.limit_time print_report report
in
Format.printf "%a@." (Pp.print_list Pp.newline pp_elem) lr
Format.fprintf fmt "%a@." (Pp.print_list Pp.newline pp_elem) lr
let replay ~remove_obsolete ~use_steps c ~callback =
......
......@@ -203,7 +203,9 @@ type report =
(* Callback for the report printing of replay
TODO to be removed when we have a better way to print the result of replay *)
val replay_print:
(proofNodeID * Whyconf.prover * Call_provers.resource_limit * report) list -> unit
Format.formatter ->
(proofNodeID * Whyconf.prover * Call_provers.resource_limit * report) list ->
unit
(* TODO replay for manual proofs ? *)
val replay:
......
This diff is collapsed.
......@@ -3,68 +3,68 @@ open Call_provers
type prover = string
type transformation = string
type strategy = string
type infos =
{hidden_provers : string list;
session_time_limit : int;
session_mem_limit : int;
session_nb_processes : int;
session_cntexample : bool;
main_dir : string}
(* TODO:
Size of the name can be proportionnal to the size of the tree.
Maybe, we should find an other solution *)
type node_ID = string
type pos_ID = string
type node_ID = int
val root_node : node_ID
(* --------------------------- types to be expanded if needed --------------------------------- *)
type node_type = Root | File | Theory | Transformation | Goal | ProofAttempt of bool
type node_type = NRoot | NFile | NTheory | NTransformation | NGoal | NProofAttempt of bool
type node_info = { proved : bool; (* TODO: add more *)
name : string }
(* todo, separate what's updatable from the rest in types *)
(* pos_ID is the suffix of node_ID: its position in its brothers list *)
type session_tree =
| Node of node_ID * pos_ID * node_type * node_info * session_tree list
type error_notification =
(* Global information known when server process has started and that can be
shared with the IDE through communication *)
type global_information =
{
provers : prover list;
transformations : transformation list;
strategies : strategy list;
(* hidden_provers : string list; *)
(* session_time_limit : int; *)
(* session_mem_limit : int; *)
(* session_nb_processes : int; *)
(* session_cntexample : bool; *)
(* main_dir : string *)
}
type message_notification =
| Proof_error of node_ID * string
| Transf_error of node_ID * string
| Strat_error of node_ID * string
| Replay_Info of string
| Query_Info of node_ID * string
| Query_Error of node_ID * string
| Help of string
| Information of string
type notification =
| Node_change of node_ID * node_info
(* inform that the data of the given node changed *)
| New_subtree of node_ID * session_tree
(* the given node has a new child whose contents is the given tree *)
| New_node of node_ID * node_ID * node_type * node_info
(* Notification of creation of new_node:
New_node (new_node, parent_node, new_node_type, new_node_content). *)
| Remove of node_ID
(* the given node was removed *)
| Initialized of infos * prover list * transformation list * strategy list
| Initialized of global_information
(* initial global data *)
| Saved
(* the session was saved on disk *)
| Session_Tree of session_tree
(* the full session tree is sent *)
| Error of error_notification
(* an error occured *)
| Message of string
(* an informative message *)
| Message of message_notification
(* an informative message, can be an error message *)
type request_type =
| Command of string
| Prove of prover * resource_limit
| Transform of transformation * string list
| Strategy of strategy
| Open of string
| Get_Session_Tree
| Save
| Reload
| Replay
| Exit
| Command_req of string
| Prove_req of prover * resource_limit
| Transform_req of transformation * string list
| Strategy_req of strategy
| Open_req of string
| Get_Session_Tree_req
| Save_req
| Reload_req
| Replay_req
| Exit_req
type ide_request = request_type * node_ID
......
......@@ -245,17 +245,18 @@ let strategies env config =
let sort_pair (x,_) (y,_) = String.compare x y
let list_transforms _cont _args =
let l =
let list_transforms () =
List.rev_append
(List.rev_append (Trans.list_transforms ()) (Trans.list_transforms_l ()))
(List.rev_append (Trans.list_transforms_with_args ()) (Trans.list_transforms_with_args_l ()))
in
(List.rev_append (Trans.list_transforms ()) (Trans.list_transforms_l ()))
(List.rev_append (Trans.list_transforms_with_args ()) (Trans.list_transforms_with_args_l ()))
let list_transforms_query _cont _args =
let l = list_transforms () in
let print_trans_desc fmt (x,r) =
fprintf fmt "@[<hov 2>%s@\n@[<hov>%a@]@]" x Pp.formatted r
in
Pp.string_of (Pp.print_list Pp.newline2 print_trans_desc)
(List.sort sort_pair l)
(List.sort sort_pair l)
let list_provers cont _args =
let l =
......@@ -316,7 +317,7 @@ type query =
let commands =
[
"list-transforms", "list available transformations", Qnotask list_transforms;
"list-transforms", "list available transformations", Qnotask list_transforms_query;
"list-provers", "list available provers", Qnotask list_provers;
(*
"list-strategies", "list available strategies", list_strategies;
......@@ -382,31 +383,162 @@ let split_args s =
| [] -> "",[]
type command =
| Transform of string * Trans.gentrans * string list
| Query of string
| Other of string * string list
| Transform of string * Trans.gentrans * string list
| Prove of Whyconf.config_prover * Call_provers.resource_limit
| Strategies of string
| Help_message of string
| Query of string
| QError of string
| Other of string * string list
(********* 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})
| _ -> None
end
let interp cont id s =
let interp_others config cmd args =
match parse_prover_name config cmd args with
| Some (prover_config, limit) ->
Prove (prover_config, limit)
| None ->
match cmd with
| "auto" ->
let s =
match args with
| "2"::_ -> "2"
| _ -> "1"
in
Strategies s
| "help" ->
let text = Pp.sprintf
"Please type a command among the following (automatic completion available)@\n\
@\n\
@ <transformation name> [arguments]@\n\
@ <prover name> [<time limit> [<mem limit>]]@\n\
@ <query> [arguments]@\n\
@ auto [auto level]@\n\
@\n\
Available queries are:@\n@[%a@]" help_on_queries ()
in
Help_message text
| _ ->
Other (cmd, args)
let interp config cont id s =
let cmd,args = split_args s in
try
let f = Stdlib.Hstr.find commands_table cmd in
match f,id with
| Qnotask f, _ -> Query (f cont args)
| Qtask _, None -> Query "please select a goal first"
| Qtask _, None -> QError "please select a goal first"
| Qtask f, Some id ->
let tables = match Session_itp.get_tables cont.Controller_itp.controller_session id with
| None -> raise (Task.Bad_name_table "interp")
| Some tables -> tables in
let s = try Query (f cont tables args) with
| Undefined_id s -> Query ("No existing id corresponding to " ^ s)
| Number_of_arguments -> Query "Bad number of arguments"
| Undefined_id s -> QError ("No existing id corresponding to " ^ s)
| Number_of_arguments -> QError "Bad number of arguments"
in s
with Not_found ->
try
let t = Trans.lookup_trans cont.Controller_itp.controller_env cmd in
Transform (cmd,t,args)
with Trans.UnknownTrans _ ->
Other(cmd,args)
interp_others config cmd args
(*
let interp cont id cmd =
try
match interp cont id cmd with
| Transform(s,_t,args) ->
clear_command_entry ();
apply_transform cont s args
| Query s ->
clear_command_entry ();
message_zone#buffer#set_text s
| Other(s,args) ->
begin
match parse_prover_name gconfig.config s args with
| Some (prover_config, limit) ->
clear_command_entry ();
Prove test_schedule_proof_attempt cont prover_config limit
| None ->
match s with
Strategies
| "auto" ->
let s =
match args with
| "2"::_ -> "2"
| _ -> "1"
in
clear_command_entry ();
run_strategy_on_task s
| "help" ->
clear_command_entry ();
let text = Pp.sprintf
"Please type a command among the following (automatic completion available)@\n\
@\n\
@ <transformation name> [arguments]@\n\
@ <prover name> [<time limit> [<mem limit>]]@\n\
@ <query> [arguments]@\n\
@ auto [auto level]@\n\
@\n\
Available queries are:@\n@[%a@]" help_on_queries ()
in
message_zone#buffer#set_text text
| _ ->
message_zone#buffer#set_text ("unknown command '"^s^"'")
end
with e when not (Debug.test_flag Debug.stack_trace) ->
message_zone#buffer#set_text (Pp.sprintf "anomaly: %a" Exn_printer.exn_printer e)
*)
(********* Callbacks tools *******)
......
module Unix_Scheduler : sig
module Unix_scheduler : sig
val timeout: ms:int -> (unit -> bool) -> unit
(** [timeout ~ms f] registers the function [f] as a function to be
......
open Ident
open Task
exception Arg_parse_error of string * string
......
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