Commit 7d1d2570 authored by MARCHE Claude's avatar MARCHE Claude

commands can be registered at any time.

adding the replay command in command line
parent 78c34cf3
......@@ -317,21 +317,30 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
(* Command list *)
(****************)
let interrupt_query _cont _args = C.interrupt (); "interrupted"
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;
let commands_table = Stdlib.Hstr.create 17
let register_command c d f = Stdlib.Hstr.add commands_table c (d,f)
let () =
List.iter (fun (c,d,f) -> register_command c d f)
[
"interrupt", "interrupt all scheduled or running proof tasks",
Qnotask interrupt_query;
"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;
"print", "<id> print the declaration where <id> was defined",
Qtask print_id;
"search", "<is> print declarations where <id> appears",
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);
......@@ -342,12 +351,6 @@ let commands =
*)
]
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;
......@@ -784,7 +787,7 @@ let () =
transformations = transformation_list;
strategies = strategies_list;
commands =
List.map (fun (c,_,_) -> c) commands
Hstr.fold (fun c _ acc -> c :: acc) commands_table []
}
in
match cont_from_session ~notify:P.notify d.cont f with
......@@ -941,6 +944,9 @@ let () =
C.replay ~use_steps:false ~obsolete_only:true d.cont
~callback ~notification:notify_change_proved ~final_callback
let () = register_command "replay" "replay obsolete proofs"
(Qnotask (fun _cont _args -> replay_session (); "replay in progress, be patient"))
(* ---------------- Mark obsolete ------------------ *)
let mark_obsolete n =
let d = get_server_data () in
......@@ -1043,7 +1049,7 @@ let () =
| Command_req (nid, cmd) ->
begin
let snid = get_proof_node_id nid in
match (interp commands commands_table d.config d.cont snid cmd) with
match (interp commands_table d.config 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) -> schedule_proof_attempt nid p limit
......
......@@ -140,7 +140,7 @@ type query =
| Qtask of (Controller_itp.controller -> Task.name_tables -> string list -> string)
let help_on_queries fmt commands =
let l = List.rev_map (fun (c,h,_) -> (c,h)) commands in
let l = Stdlib.Hstr.fold (fun c (h,_) acc -> (c,h)::acc) commands [] in
let l = List.sort sort_pair l in
let p fmt (c,help) = Format.fprintf fmt "%20s : %s" c help in
Format.fprintf fmt "%a" (Pp.print_list Pp.newline p) l
......@@ -258,7 +258,7 @@ type command =
| QError of string
| Other of string * string list
let interp_others commands config cmd args =
let interp_others commands_table config cmd args =
match parse_prover_name config cmd args with
| Some (prover_config, limit) ->
Prove (prover_config, limit)
......@@ -280,16 +280,16 @@ let interp_others commands config cmd args =
@ <query> [arguments]@\n\
@ auto [auto level]@\n\
@\n\
Available queries are:@\n@[%a@]" help_on_queries commands
Available queries are:@\n@[%a@]" help_on_queries commands_table
in
Help_message text
| _ ->
Other (cmd, args)
let interp commands commands_table config cont id s =
let interp commands_table config cont id s =
let cmd,args = split_args s in
try
let f = Stdlib.Hstr.find commands_table cmd in
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"
......@@ -306,7 +306,7 @@ let interp commands commands_table config cont id s =
let t = Trans.lookup_trans cont.Controller_itp.controller_env cmd in
Transform (cmd,t,args)
with Trans.UnknownTrans _ ->
interp_others commands config cmd args
interp_others commands_table config cmd args
(***********************)
......
......@@ -26,7 +26,7 @@ val search_id: 'a -> Task.name_tables -> string list -> string
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 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
......@@ -44,8 +44,8 @@ type command =
| QError of string
| Other of string * string list
val interp: (string * string * 'a) list ->
query Stdlib.Hstr.t ->
val interp:
(string * query) Stdlib.Hstr.t ->
Whyconf.config ->
Controller_itp.controller ->
Session_itp.proofNodeID option -> string -> command
......
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