Commit 0cd33156 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

Added print and search.

parent 6fdc56a9
......@@ -516,10 +516,14 @@ let run_strategy_on_task s =
let clear_command_entry () = command_entry#set_text ""
open Session_user_interface
let current_id id =
match id with
| IproofNode id -> id
| _ -> assert (false) (* TODO *)
let interp cmd =
match interp cont.controller_env cmd with
let id = current_id !current_selected_index in
match interp cont.controller_env id cont.controller_session cmd with
| Transform(s,_t,args) ->
clear_command_entry ();
apply_transform cont.controller_session s args
......
open Format
open Session_itp
(* TODO: raise exceptions instead of using explicit eprintf/exit *)
let cont_from_files spec usage_str env files provers =
......@@ -30,7 +31,7 @@ let cont_from_files spec usage_str env files provers =
Unix.mkdir dir 0o777
end;
(* we load the session *)
let ses,use_shapes = Session_itp.load_session dir in
let ses,use_shapes = load_session dir in
eprintf "using shapes: %a@." pp_print_bool use_shapes;
(* create the controller *)
let c = Controller_itp.create_controller env ses in
......@@ -181,15 +182,58 @@ let list_transforms _args =
Pp.string_of (Pp.print_list Pp.newline2 print_trans_desc)
(List.sort sort_pair l)
let find_any_id nt s =
try (Stdlib.Mstr.find s nt.Theory.ns_pr).Decl.pr_name with
| Not_found -> try (Stdlib.Mstr.find s nt.Theory.ns_ls).Term.ls_name with
| Not_found -> (Stdlib.Mstr.find s nt.Theory.ns_ts).Ty.ts_name
(* The id you are trying to use is undefined *)
exception Undefined_id
(* Bad number of arguments *)
exception Number_of_arguments
let print_id s task =
let tables = Args_wrapper.build_name_tables task in
let km = tables.Args_wrapper.known_map in
let id = try find_any_id tables.Args_wrapper.namespace s with
| Not_found -> raise Undefined_id in
let d =
try Ident.Mid.find id km with
| Not_found -> raise Not_found (* Should not happen *)
in
Pp.string_of (Why3printer.print_decl tables) d
let print_id task args =
match args with
| [s] -> print_id s task
| _ -> raise Number_of_arguments
let search s task =
let tables = Args_wrapper.build_name_tables task in
let id_decl = tables.Args_wrapper.id_decl in
let id = try find_any_id tables.Args_wrapper.namespace s with
| Not_found -> raise Undefined_id in
let l =
try Ident.Mid.find id id_decl with
| Not_found -> raise Not_found (* Should not happen *)
in
Pp.string_of (Pp.print_list Pp.newline2 (Why3printer.print_decl tables)) l
let search_id task args =
match args with
| [s] -> search s task
| _ -> raise Number_of_arguments
let commands =
[
"list-transforms", "list available transformations", list_transforms;
"list-transforms", "list available transformations", (fun _ -> list_transforms);
(*
"list-provers", "list available provers", list_provers;
"list-strategies", "list available strategies", list_strategies;
"print", "<s> print the declaration where s was defined", test_print_id;
"search", "<s> print some declarations where s appear", test_search_id;
*)
"print", "<s> print the declaration where s was defined", print_id;
"search", "<s> print some declarations where s appear", search_id;
(*
"r", "reload the session (test only)", test_reload;
"rp", "replay", test_replay;
"s", "save the current session", test_save_session;
......@@ -240,11 +284,12 @@ type command =
| Query of string
| Other of string * string list
let interp env s =
let interp env id ses s =
let task = Session_itp.get_task ses id in
let cmd,args = split_args s in
try
let f = Stdlib.Hstr.find commands_table cmd in
Query (f args)
Query (f task args)
with Not_found ->
try
let t = Trans.lookup_trans env cmd in
......
......@@ -111,6 +111,7 @@ end
(************************)
open Why3
open Session_user_interface
open Format
(* files of the current task *)
......@@ -568,52 +569,15 @@ let print_known_map _fmt _args =
printf "known: %s@." id.Ident.id_string)
km
let find_any_id nt s =
try (Stdlib.Mstr.find s nt.Theory.ns_pr).Decl.pr_name with
| Not_found -> try (Stdlib.Mstr.find s nt.Theory.ns_ls).Term.ls_name with
| Not_found -> (Stdlib.Mstr.find s nt.Theory.ns_ts).Ty.ts_name
let print_id s task fmt =
let tables = Args_wrapper.build_name_tables task in
let km = tables.Args_wrapper.known_map in
let id = try Some (find_any_id tables.Args_wrapper.namespace s) with
| Not_found -> Format.fprintf fmt "Does not exists @."; None in
if id = None then () else
let id = Opt.get id in
let d =
try Some (Ident.Mid.find id km) with
| Not_found -> None in
if d = None then () else Format.fprintf fmt "%a @." (Why3printer.print_decl tables) (Opt.get d)
let test_print_id fmt args =
let test_print_id _fmt args =
let id = nearest_goal () in
let task = get_task cont.controller_session id in
match args with
| [s] -> print_id s task fmt
| _ -> Format.fprintf fmt "Wrong number of arguments"
Format.printf "%s@." (print_id task args)
let search s fmt task =
let tables = Args_wrapper.build_name_tables task in
let id_decl = tables.Args_wrapper.id_decl in
let id = try Some (find_any_id tables.Args_wrapper.namespace s) with
| Not_found -> Format.fprintf fmt "Does not exists @."; None in
if id = None then () else
let id = Opt.get id in
let l =
try Some (Ident.Mid.find id id_decl) with
| Not_found -> None in
if l = None then () else
Format.fprintf fmt "%a @."
(Pp.print_list (fun fmt _ -> Format.fprintf fmt "\n")
(Why3printer.print_decl tables)) (Opt.get l)
let test_search_id fmt args =
let test_search_id _fmt args =
let id = nearest_goal () in
let task = get_task cont.controller_session id in
match args with
| [s] -> search s fmt task
| _ -> Format.fprintf fmt "Wrong number of arguments"
Format.printf "%s@." (search_id task args)
(****)
......
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