Commit dd2493a7 authored by Sylvain Dailler's avatar Sylvain Dailler

fixes #68

Adding a search query "search_all" which search the declarations that
contains at least one of the identifiers provided by the user.
parent 50317a3a
......@@ -363,7 +363,9 @@ let () =
"print", "<id> print the declaration where <id> was defined",
Qtask print_id;
"search", "<ids> print the declarations where all <ids> appears",
Qtask search_id;
Qtask (search_id ~search_both:false);
"search_all", "<ids> print the declarations where one of <ids> appears",
Qtask (search_id ~search_both:true);
(*
"r", "reload the session (test only)", test_reload;
"s", "save the current session", test_save_session;
......
......@@ -224,19 +224,24 @@ let occurs_in_decl d id =
| Dprop ((Paxiom|Plemma), pr, t) -> Ident.id_equal pr.pr_name id || occurs_in_term id t
| Dprop _ -> false)
let do_search km idl =
let do_search ~search_both km idl =
Ident.Mid.fold
(fun _ d acc ->
if List.for_all (occurs_in_decl d) idl then Decl.Sdecl.add d acc else acc) km Decl.Sdecl.empty
if search_both then
(if List.exists (occurs_in_decl d) idl then Decl.Sdecl.add d acc else acc)
else
(if List.for_all (occurs_in_decl d) idl then Decl.Sdecl.add d acc else acc)) km Decl.Sdecl.empty
let search s tables =
let search ~search_both s tables =
let ids = List.rev_map
(fun s -> try symbol_name (Args_wrapper.find_symbol s tables)
with Args_wrapper.Arg_parse_type_error _ |
Args_wrapper.Arg_qid_not_found _ -> raise (Undefined_id s)) s
in
let l = do_search tables.Trans.known_map ids in
let l = do_search ~search_both tables.Trans.known_map ids in
if Decl.Sdecl.is_empty l then
(* In case where search_both is true, this error cannot appear because there
is at least one declaration: the definition of the ident. *)
Pp.sprintf
"No declaration contain all the %d identifiers @[%a@]"
(List.length ids)
......@@ -253,10 +258,10 @@ let print_id _cont task args =
| [s] -> print_id s task
| _ -> raise Number_of_arguments
let search_id _cont task args =
let search_id ~search_both _cont task args =
match args with
| [] -> raise Number_of_arguments
| _ -> search args task
| _ -> search ~search_both args task
type query =
| Qnotask of (Controller_itp.controller -> string list -> string)
......
......@@ -46,7 +46,7 @@ type query =
(* The first argument is not used: these functions are supposed to be given to a
Qtask. *)
val print_id: 'a -> Trans.naming_table -> string list -> string
val search_id: 'a -> Trans.naming_table -> string list -> string
val search_id: search_both:bool -> 'a -> Trans.naming_table -> string list -> string
val list_strategies : Controller_itp.controller -> (string * string) list
val list_provers: Controller_itp.controller -> _ -> 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