Commit d962aa69 authored by MARCHE Claude's avatar MARCHE Claude

searching multiple idents simultaneously, available in IDE

parent bcd79af4
......@@ -73,49 +73,49 @@ let loaded_strategies = ref []
let print_term s id fmt t =
let tables = match (Session_itp.get_table s id) with
| None -> Args_wrapper.build_name_tables (Session_itp.get_task s id)
| None -> Args_wrapper.build_naming_tables (Session_itp.get_task s id)
| Some tables -> tables in
Why3printer.print_term tables fmt t
let print_type s id fmt t =
let tables = match (Session_itp.get_table s id) with
| None -> Args_wrapper.build_name_tables (Session_itp.get_task s id)
| None -> Args_wrapper.build_naming_tables (Session_itp.get_task s id)
| Some tables -> tables in
Why3printer.print_ty tables fmt t
let print_ts s id fmt t =
let tables = match (Session_itp.get_table s id) with
| None -> Args_wrapper.build_name_tables (Session_itp.get_task s id)
| None -> Args_wrapper.build_naming_tables (Session_itp.get_task s id)
| Some tables -> tables in
Why3printer.print_ts tables fmt t
let print_ls s id fmt t =
let tables = match (Session_itp.get_table s id) with
| None -> Args_wrapper.build_name_tables (Session_itp.get_task s id)
| None -> Args_wrapper.build_naming_tables (Session_itp.get_task s id)
| Some tables -> tables in
Why3printer.print_ls tables fmt t
let print_tv s id fmt t =
let tables = match (Session_itp.get_table s id) with
| None -> Args_wrapper.build_name_tables (Session_itp.get_task s id)
| None -> Args_wrapper.build_naming_tables (Session_itp.get_task s id)
| Some tables -> tables in
Why3printer.print_tv tables fmt t
let print_vsty s id fmt t =
let tables = match (Session_itp.get_table s id) with
| None -> Args_wrapper.build_name_tables (Session_itp.get_task s id)
| None -> Args_wrapper.build_naming_tables (Session_itp.get_task s id)
| Some tables -> tables in
Why3printer.print_forget_vsty tables fmt t
let print_pr s id fmt t =
let tables = match (Session_itp.get_table s id) with
| None -> Args_wrapper.build_name_tables (Session_itp.get_task s id)
| None -> Args_wrapper.build_naming_tables (Session_itp.get_task s id)
| Some tables -> tables in
Why3printer.print_pr tables fmt t
let print_pat s id fmt t =
let tables = match (Session_itp.get_table s id) with
| None -> Args_wrapper.build_name_tables (Session_itp.get_task s id)
| None -> Args_wrapper.build_naming_tables (Session_itp.get_task s id)
| Some tables -> tables in
Why3printer.print_pat tables fmt t
......@@ -368,7 +368,7 @@ let () =
*)
"print", "<id> print the declaration where <id> was defined",
Qtask print_id;
"search", "<is> print declarations where <id> appears",
"search", "<ids> print the declarations where all <ids> appears",
Qtask search_id;
(*
"r", "reload the session (test only)", test_reload;
......
......@@ -147,13 +147,59 @@ let print_id s tables =
in
Pp.string_of (Why3printer.print_decl tables) d
(* searching ids in declarations *)
let occurs_in_type id = Ty.ty_s_any (fun ts -> Ident.id_equal ts.Ty.ts_name id)
let occurs_in_term id =
Term.t_s_any (occurs_in_type id) (fun ls -> Ident.id_equal id ls.Term.ls_name)
let occurs_in_constructor id (cs,projs) =
Ident.id_equal cs.Term.ls_name id ||
List.exists (function Some ls -> Ident.id_equal ls.Term.ls_name id | None -> false) projs
let occurs_in_defn id (ls,def) =
Ident.id_equal ls.Term.ls_name id ||
let (_vl,t) = Decl.open_ls_defn def in occurs_in_term id t
let occurs_in_ind_decl id (_,clauses) =
List.exists (fun (_,t) -> occurs_in_term id t) clauses
let occurs_in_decl d id =
Decl.(match d.d_node with
| Decl.Dtype ts -> Ident.id_equal ts.Ty.ts_name id (* look through ts.ys_def *)
| Decl.Ddata dl ->
List.exists
(fun ((ts,c): data_decl) ->
Ident.id_equal ts.Ty.ts_name id || List.exists (occurs_in_constructor id) c)
dl
| Decl.Dparam ls -> Ident.id_equal ls.Term.ls_name id
| Decl.Dlogic dl -> List.exists (occurs_in_defn id) dl
| Decl.Dind (_, il) -> List.exists (occurs_in_ind_decl id) il
| Dprop ((Paxiom|Plemma), pr, t) -> Ident.id_equal pr.pr_name id || occurs_in_term id t
| Dprop _ -> false)
let do_search 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
let search s tables =
(*let tables = Args_wrapper.build_name_tables task in*)
let id = try find_any_id tables.Trans.namespace s with
| Not_found -> raise (Undefined_id s) in
let l = Args_wrapper.search tables.Trans.known_map [id] in
let s_id = print_id s tables in
s_id ^ (Pp.string_of (Pp.print_list Pp.newline2 (Why3printer.print_decl tables)) l)
let ids = List.rev_map
(fun s -> try find_any_id tables.Trans.namespace s
with Not_found -> raise (Undefined_id s)) s
in
let l = do_search tables.Trans.known_map ids in
if Decl.Sdecl.is_empty l then
Pp.sprintf
"No declaration contain all the %d identifiers @[%a@]"
(List.length ids)
(Pp.print_list Pp.space (fun fmt id -> Pp.string fmt id.Ident.id_string))
ids
else let l = Decl.Sdecl.elements l in
Pp.string_of (Pp.print_list Pp.newline2 (Why3printer.print_decl tables)) l
let print_id _cont task args =
match args with
......@@ -162,8 +208,8 @@ let print_id _cont task args =
let search_id _cont task args =
match args with
| [s] -> search s task
| _ -> raise Number_of_arguments
| [] -> raise Number_of_arguments
| _ -> search args task
type query =
| Qnotask of (Controller_itp.controller -> string list -> string)
......
......@@ -531,7 +531,7 @@ let graft_proof_attempt ?file (s : session) (id : proofNodeID) (pr : Whyconf.pro
of proofNodeID [id] of parent [p] of task [t] *)
let mk_proof_node ~version ~expl (s : session) (n : Ident.ident) (t : Task.task)
(parent : proof_parent) (node_id : proofNodeID) =
let tables = Args_wrapper.build_name_tables t in
let tables = Args_wrapper.build_naming_tables t in
let sum = Some (Termcode.task_checksum ~version t) in
let shape = Termcode.t_shape_task ~version ~expl t in
let pn = { proofn_name = n;
......
......@@ -143,7 +143,7 @@ let add (d: decl) (tables: naming_table): naming_table =
let s = id_unique tables.printer id in
add_unsafe s (Pr pr) tables
let build_name_tables task : naming_table =
let build_naming_tables task : naming_table =
let pr = fresh_printer () in
let km = Task.task_known task in
let tables = {
......@@ -159,39 +159,6 @@ let build_name_tables task : naming_table =
let l = Mid.fold (fun _id d acc -> d :: acc) km [] in
List.fold_left (fun tables d -> add d tables) tables l
(* searching ids in declarations *)
let occurs_in_type id = ty_s_any (fun ts -> Ident.id_equal ts.Ty.ts_name id)
let occurs_in_term id =
t_s_any (occurs_in_type id) (fun ls -> Ident.id_equal id ls.ls_name)
let occurs_in_constructor _id _c = false
let occurs_in_defn id (_,def) =
let (_vl,t) = open_ls_defn def in occurs_in_term id t
let occurs_in_ind_decl id (_,clauses) =
List.exists (fun (_,t) -> occurs_in_term id t) clauses
let occurs_in_decl d id =
match d.d_node with
| Dtype ts -> Ident.id_equal ts.Ty.ts_name id
| Ddata dl ->
List.exists
(fun ((_,c): data_decl) -> List.exists (occurs_in_constructor id) c)
dl
| Dparam _ls -> false
| Dlogic dl -> List.exists (occurs_in_defn id) dl
| Dind (_is, il) -> List.exists (occurs_in_ind_decl id) il
| Dprop (k, _, t) -> k = Paxiom && occurs_in_term id t
let search km idl =
Mid.fold
(fun _id d acc ->
if List.for_all (occurs_in_decl d) idl then d :: acc else acc) km []
(************* wrapper *************)
type symbol =
......@@ -238,7 +205,6 @@ let find_symbol s tables =
let type_ptree ~as_fmla t tables =
(*let tables = build_name_tables task in*)
let km = tables.known_map in
let ns = tables.namespace in
if as_fmla
......
......@@ -11,11 +11,7 @@ exception Arg_hyp_not_found of string
(** Pre-processing of tasks, to build unique names for all declared
identifiers of a task.*)
val build_name_tables : Task.task -> Trans.naming_table
val search : Decl.known_map -> Ident.ident list -> Decl.decl list
(** [search km ids] returns the set of declarations from [km] that
contain all the identifiers [ids] *)
val build_naming_tables : Task.task -> Trans.naming_table
type symbol =
| Tstysymbol of Ty.tysymbol
......
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