Commit ec5ae5c3 authored by MARCHE Claude's avatar MARCHE Claude

replaced Edit_req request with Edit command.

edit is now possible for non-interactive provers
parent b22d53e5
......@@ -568,7 +568,20 @@ let prepare_edition c ?file pn pr ~notification =
let proof_attempts_id = get_proof_attempt_ids session pn in
let panid =
try
Hprover.find proof_attempts_id pr
let panid = Hprover.find proof_attempts_id pr in
(* if no proof script yet, we need to add one
it happens e.g when editing a file for an automatic prover
*)
let pa = get_proof_attempt_node session panid in
match pa.proof_script with
| None ->
let file = match file with
| Some f -> f
| None -> create_file_rel_path c pr pn
in
set_proof_script pa file;
panid
| Some _ -> panid
with Not_found ->
let file = match file with
| Some f -> f
......
......@@ -100,10 +100,6 @@ type notification =
type ide_request =
| Command_req of node_ID * string
| Edit_req of node_ID * prover
(*
| Open_session_req of string
*)
| Add_file_req of string
| Set_max_tasks_req of int
| Get_file_contents of string
......@@ -127,11 +123,8 @@ type ide_request =
(* Return true if the request modify the session *)
let modify_session (r: ide_request) =
match r with
| Command_req _
| Add_file_req _ | Remove_subtree _ | Copy_paste _ | Copy_detached _
| Replay_req | Clean_req | Mark_obsolete_req _ | Edit_req _ -> true
(*| Open_session_req _ *)
| Command_req _ | Add_file_req _ | Remove_subtree _ | Copy_paste _
| Copy_detached _ | Replay_req | Clean_req | Mark_obsolete_req _ -> true
| Set_max_tasks_req _ | Get_file_contents _
| Get_task _ | Save_file_req _ | Get_first_unproven_node _
| Get_Session_Tree_req | Save_req | Reload_req | Exit_req
......
......@@ -109,11 +109,6 @@ type ide_request =
(* executes the given command on the given node. command is
interpreted by Server_utils.interp. This includes calling
provers, applying transformations, stategies. *)
| Edit_req of node_ID * prover
(** Request for edition of the proof script of the proof attempt
associated to the given node id. Works also for non-interactive
provers, it simply opens an editeor on the file sent to the
prover. *)
| Add_file_req of string
| Set_max_tasks_req of int
| Get_file_contents of string
......
......@@ -16,8 +16,6 @@ open Controller_itp
open Server_utils
open Itp_communication
exception Bad_prover_name of string
(**********************************)
(* list unproven goal and related *)
(**********************************)
......@@ -254,10 +252,6 @@ let get_exception_message ses id e =
let print_request fmt r =
match r with
| Command_req (_nid, s) -> fprintf fmt "command \"%s\"" s
| Edit_req (_nid, prover) -> fprintf fmt "edit with %s" prover
(*
| Open_session_req f -> fprintf fmt "open session file %s" f
*)
| Add_file_req f -> fprintf fmt "open file %s" f
| Set_max_tasks_req i -> fprintf fmt "set max tasks %i" i
| Get_file_contents _f -> fprintf fmt "get file contents"
......@@ -456,12 +450,6 @@ let () =
Hint.remove model_any nid;
Hpan.remove pan_to_node_ID pa
let get_prover p =
let d = get_server_data () in
match return_prover p d.cont.controller_config with
| None -> raise (Bad_prover_name p)
| Some c -> c
let add_node_to_table node new_id =
match node with
| AFile file -> Hstr.add file_to_node_ID (file_name file) new_id
......@@ -1258,19 +1246,13 @@ end
(* ----------------- treat_request -------------------- *)
let get_proof_node_id nid =
try
match any_from_node_ID nid with
| APn pn_id -> Some pn_id
| _ -> None
with
Not_found -> None
let treat_request r =
let d = get_server_data () in
let config = d.cont.controller_config in
try (
match r with
(*
| Edit_req (nid, p) ->
let p = try Some (get_prover p) with
| Bad_prover_name p -> P.notify (Message (Proof_error (nid, "Bad prover name" ^ p))); None
......@@ -1280,6 +1262,7 @@ end
| Some p ->
schedule_edition nid p
end
*)
| Clean_req -> clean_session ()
| Save_req -> save_session ()
| Reload_req -> reload_session ()
......@@ -1322,7 +1305,7 @@ end
| Interrupt_req -> C.interrupt ()
| Command_req (nid, cmd) ->
begin
let snid = get_proof_node_id nid in
let snid = try Some(any_from_node_ID nid) with Not_found -> None in
match interp commands_table d.cont snid cmd with
| Transform (s, _t, args) -> apply_transform nid s args
| Query s -> P.notify (Message (Query_Info (nid, s)))
......
......@@ -138,10 +138,6 @@ let convert_node_type nt =
let convert_request_constructor (r: ide_request) =
match r with
| Command_req _ -> String "Command_req"
| Edit_req _ -> String "Edit_req"
(*
| Open_session_req _ -> String "Open_session_req"
*)
| Add_file_req _ -> String "Add_file_req"
| Save_file_req _ -> String "Save_file_req"
| Set_max_tasks_req _ -> String "Set_max_tasks_req"
......@@ -170,15 +166,6 @@ let print_request_to_json (r: ide_request): Json_base.json =
convert_record ["ide_request", cc r;
"node_ID", Int nid;
"command", String s]
| Edit_req (nid, prover) ->
convert_record ["ide_request", cc r;
"node_ID", Int nid;
"prover", String prover]
(*
| Open_session_req f ->
convert_record ["ide_request", cc r;
"file", String f]
*)
| Add_file_req f ->
convert_record ["ide_request", cc r;
"file", String f]
......@@ -436,15 +423,6 @@ let parse_request (constr: string) j =
let nid = get_int (get_field j "node_ID") in
let s = get_string (get_field j "command") in
Command_req (nid, s)
| "Edit_req" ->
let nid = get_int (get_field j "node_ID") in
let p = get_string (get_field j "prover") in
Edit_req (nid, p)
(*
| "Open_session_req" ->
let f = get_string (get_field j "file") in
Open_session_req f
*)
| "Focus_req" ->
let nid = get_int (get_field j "node_ID") in
Focus_req nid
......
......@@ -353,69 +353,79 @@ type command =
| QError of string
| Other of string * string list
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
| "help", [trans] ->
let print_trans_desc fmt r =
Format.fprintf fmt "@[%s:\n%a@]" trans Pp.formatted r
in
(try
let desc = Trans.lookup_trans_desc trans in
Help_message (Pp.string_of print_trans_desc desc)
with
| Not_found -> QError (Pp.sprintf "Transformation %s does not exists" trans))
| "help", _ ->
let text = Pp.sprintf
"Please type a command among the following (automatic completion available)@\n\
@\n\
@ <transformation name> [arguments]@\n\
@ <prover shortcut> [<time limit> [<mem limit>]]@\n\
@ <query> [arguments]@\n\
@ <strategy shortcut>@\n\
@ help <transformation_name> @\n\
@\n\
Available queries are:@\n@[%a@]" help_on_queries commands_table
in
Help_message text
| _ ->
Other (cmd, args)
let interp commands_table 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 -> QError "please select a goal first"
| Qtask f, Some id ->
| Qtask f, Some (Session_itp.APn id) ->
let _,table = Session_itp.get_task cont.Controller_itp.controller_session id in
let s = try Query (f cont table args) with
| Undefined_id s -> QError ("No existing id corresponding to " ^ s)
| Number_of_arguments -> QError "Bad number of arguments"
in s
| Qtask _, _ -> QError "please select a goal first"
with Not_found ->
let t =
try Some (Trans.lookup_trans cont.Controller_itp.controller_env cmd) with
| Trans.UnknownTrans _ -> None
in
match t with
| Some t ->
if id = None then
QError ("Please select a valid node id")
else
Transform (cmd,t,args)
| None ->
interp_others commands_table cont cmd args
try
let t = Trans.lookup_trans cont.Controller_itp.controller_env cmd in
match id with
| Some (Session_itp.APn _id) -> Transform (cmd,t,args)
| _ -> QError ("Please select a goal node in the task tree")
with
| Trans.UnknownTrans _ ->
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
| "edit", _ ->
begin
match id with
| Some (Session_itp.APa id) ->
let pa =
Session_itp.get_proof_attempt_node
cont.Controller_itp.controller_session id in
begin try
let p,_ = Whyconf.Hprover.find
cont.Controller_itp.controller_provers
pa.Session_itp.prover in
Edit p
with Not_found ->
QError "prover not found"
end
| _ -> QError ("Please select a proof node in the task tree")
end
| "help", [trans] ->
let print_trans_desc fmt r =
Format.fprintf fmt "@[%s:\n%a@]" trans Pp.formatted r
in
(try
let desc = Trans.lookup_trans_desc trans in
Help_message (Pp.string_of print_trans_desc desc)
with
| Not_found -> QError (Pp.sprintf "Transformation %s does not exists" trans))
| "help", _ ->
let text = Pp.sprintf
"Please type a command among the following (automatic completion available)@\n\
@\n\
@ <transformation name> [arguments]@\n\
@ <prover shortcut> [<time limit> [<mem limit>]]@\n\
@ <query> [arguments]@\n\
@ <strategy shortcut>@\n\
@ help <transformation_name> @\n\
@\n\
Available queries are:@\n@[%a@]" help_on_queries commands_table
in
Help_message text
| _ ->
Other (cmd, args)
(***********************)
(* First Unproven goal *)
......
......@@ -65,7 +65,7 @@ type command =
val interp:
(string * query) Stdlib.Hstr.t ->
Controller_itp.controller ->
Session_itp.proofNodeID option -> string -> command
Session_itp.any option -> string -> command
val get_first_unproven_goal_around:
......
......@@ -57,9 +57,13 @@ type proof_attempt_node = {
mutable proof_state : Call_provers.prover_result option;
(* None means that the call was not done or never returned *)
mutable proof_obsolete : bool;
proof_script : string option; (* non empty for external ITP *)
mutable proof_script : string option; (* non empty for external ITP *)
}
let set_proof_script pa file =
assert (pa.proof_script = None);
pa.proof_script <- Some file
type proof_node = {
proofn_name : Ident.ident;
proofn_expl : string;
......
......@@ -76,8 +76,10 @@ type proof_attempt_node = private {
mutable proof_state : Call_provers.prover_result option;
(* None means that there is a prover call in progress *)
mutable proof_obsolete : bool;
proof_script : string option; (* non empty for external ITP *)
}
mutable proof_script : string option; (* non empty for external ITP *)
}
val set_proof_script : proof_attempt_node -> string -> unit
(* [is_below s a b] true if a is below b in the session tree *)
val is_below: session -> any -> any -> bool
......
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