Commit d1bbf7ca authored by MARCHE Claude's avatar MARCHE Claude
Browse files

ITP server: commands can now call a function of the controller

parent 56ac1980
......@@ -210,15 +210,6 @@ val run_strategy_on_goal :
[schedule_transformation]). [callback] is called on each step of
execution of the strategy. *)
type report =
| Result of Call_provers.prover_result * Call_provers.prover_result
(** Result(new_result,old_result) *)
| CallFailed of exn
| Prover_not_installed
| Edited_file_absent of string
| No_former_result of Call_provers.prover_result
(** Type for the reporting of a replayed call *)
(* [copy_paste c a b] try to copy subtree originating at node a to node b *)
val copy_paste:
notification:(any -> bool -> unit) ->
......@@ -230,6 +221,15 @@ val copy_detached:
copy:(parent:any -> any -> unit) ->
controller -> any -> unit
type report =
| Result of Call_provers.prover_result * Call_provers.prover_result
(** Result(new_result,old_result) *)
| CallFailed of exn
| Prover_not_installed
| Edited_file_absent of string
| No_former_result of Call_provers.prover_result
(** Type for the reporting of a replayed call *)
(* 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:
......
......@@ -60,38 +60,6 @@ let unproven_goals_below_id cont id =
| ATh th ->
List.rev (unproven_goals_below_th cont [] th)
(****************)
(* Command list *)
(****************)
let commands =
[
"list-transforms", "list available transformations", Qnotask list_transforms_query;
"list-provers", "list available provers", Qnotask list_provers;
(*
"list-strategies", "list available strategies", list_strategies;
*)
"print", "<s> print the declaration where s was defined", Qtask print_id;
"search", "<s> print some declarations where s appear", Qtask search_id;
(*
"r", "reload the session (test only)", test_reload;
"rp", "replay", test_replay;
"s", "save the current session", test_save_session;
"ng", "go to the next goal", then_print (move_to_goal_ret_p next_node);
"pg", "go to the prev goal", then_print (move_to_goal_ret_p prev_node);
"gu", "go to the goal up", then_print (move_to_goal_ret_p zipper_up);
"gd", "go to the goal down", then_print (move_to_goal_ret_p zipper_down);
"gr", "go to the goal right", then_print (move_to_goal_ret_p zipper_right);
"gl", "go to the goal left", then_print (move_to_goal_ret_p zipper_left)
*)
]
let commands_table = Stdlib.Hstr.create 17
let () =
List.iter
(fun (c,_,f) -> Stdlib.Hstr.add commands_table c f)
commands
(*******************)
(* Strategies list *)
(*******************)
......@@ -342,6 +310,42 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
let debug = Debug.register_flag "itp_server" ~desc:"ITP server"
(****************)
(* Command list *)
(****************)
let interrupt_query _cont _args = C.interrupt (); "interrupted"
let commands =
[
"list-transforms", "list available transformations", Qnotask list_transforms_query;
"list-provers", "list available provers", Qnotask list_provers;
(*
"list-strategies", "list available strategies", list_strategies;
*)
"print", "<s> print the declaration where s was defined", Qtask print_id;
"search", "<s> print some declarations where s appear", Qtask search_id;
"interrupt", "interrupt all scheduled or running proof tasks", Qnotask interrupt_query;
(*
"r", "reload the session (test only)", test_reload;
"rp", "replay", test_replay;
"s", "save the current session", test_save_session;
"ng", "go to the next goal", then_print (move_to_goal_ret_p next_node);
"pg", "go to the prev goal", then_print (move_to_goal_ret_p prev_node);
"gu", "go to the goal up", then_print (move_to_goal_ret_p zipper_up);
"gd", "go to the goal down", then_print (move_to_goal_ret_p zipper_down);
"gr", "go to the goal right", then_print (move_to_goal_ret_p zipper_right);
"gl", "go to the goal left", then_print (move_to_goal_ret_p zipper_left)
*)
]
let commands_table = Stdlib.Hstr.create 17
let () =
List.iter
(fun (c,_,f) -> Stdlib.Hstr.add commands_table c f)
commands
type server_data =
{ config : Whyconf.config;
task_driver : Driver.driver;
......@@ -1057,7 +1061,6 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
| Query s -> P.notify (Message (Query_Info (nid, s)))
| Prove (p, limit) -> schedule_proof_attempt nid p limit
| Strategies st -> run_strategy_on_task nid st
| Interrupt -> C.interrupt ()
| Help_message s -> P.notify (Message (Help s))
| QError s -> P.notify (Message (Query_Error (nid, s)))
| Other (s, _args) ->
......
......@@ -232,7 +232,6 @@ type command =
| Transform of string * Trans.gentrans * string list
| Prove of Whyconf.config_prover * Call_provers.resource_limit
| Strategies of string
| Interrupt
| Help_message of string
| Query of string
| QError of string
......@@ -251,7 +250,6 @@ let interp_others commands config cmd args =
| _ -> "1"
in
Strategies s
| "interrupt" -> Interrupt
| "help" ->
let text = Pp.sprintf
"Please type a command among the following (automatic completion available)@\n\
......
......@@ -43,7 +43,6 @@ type command =
| Transform of string * Trans.gentrans * string list
| Prove of Whyconf.config_prover * Call_provers.resource_limit
| Strategies of string
| Interrupt
| Help_message of string
| Query of string
| QError of 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