diff options
Diffstat (limited to 'parsing/search.ml')
| -rw-r--r-- | parsing/search.ml | 224 |
1 files changed, 224 insertions, 0 deletions
diff --git a/parsing/search.ml b/parsing/search.ml new file mode 100644 index 00000000..a3d6e000 --- /dev/null +++ b/parsing/search.ml @@ -0,0 +1,224 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: search.ml,v 1.30.2.1 2004/07/16 19:30:41 herbelin Exp $ *) + +open Pp +open Util +open Names +open Nameops +open Term +open Rawterm +open Declarations +open Libobject +open Declare +open Coqast +open Environ +open Pattern +open Matching +open Printer +open Libnames +open Nametab + +(* The functions print_constructors and crible implement the behavior needed + for the Coq searching commands. + These functions take as first argument the procedure + that will be called to treat each entry. This procedure receives the name + of the object, the assumptions that will make it possible to print its type, + and the constr term that represent its type. *) + +let print_constructors indsp fn env nconstr = + for i = 1 to nconstr do + fn (ConstructRef (indsp,i)) env (Inductive.type_of_constructor env (indsp,i)) + done + +let rec head_const c = match kind_of_term c with + | Prod (_,_,d) -> head_const d + | LetIn (_,_,_,d) -> head_const d + | App (f,_) -> head_const f + | Cast (d,_) -> head_const d + | _ -> c + +(* General search, restricted to head constant if [only_head] *) + +let gen_crible refopt (fn : global_reference -> env -> constr -> unit) = + let env = Global.env () in + let imported = Library.opened_libraries() in + let crible_rec (sp,_) lobj = match object_tag lobj with + | "VARIABLE" -> + (try + let (idc,_,typ) = get_variable (basename sp) in + if refopt = None + || head_const typ = constr_of_reference (out_some refopt) + then + fn (VarRef idc) env typ + with Not_found -> (* we are in a section *) ()) + | "CONSTANT" -> + let kn = locate_constant (qualid_of_sp sp) in + let {const_type=typ} = Global.lookup_constant kn in + if refopt = None + || head_const typ = constr_of_reference (out_some refopt) + then + fn (ConstRef kn) env typ + | "INDUCTIVE" -> + let kn = locate_mind (qualid_of_sp sp) in + let mib = Global.lookup_mind kn in + (match refopt with + | Some (IndRef ((kn',tyi) as ind)) when kn=kn' -> + print_constructors ind fn env + (Array.length (mib.mind_packets.(tyi).mind_user_lc)) + | Some _ -> () + | _ -> + Array.iteri + (fun i mip -> print_constructors (kn,i) fn env + (Array.length mip.mind_user_lc)) mib.mind_packets) + | _ -> () + in + try + Declaremods.iter_all_segments false crible_rec + with Not_found -> + () + +let crible ref = gen_crible (Some ref) + +(* Fine Search. By Yves Bertot. *) + +exception No_section_path + +let rec head c = + let c = strip_outer_cast c in + match kind_of_term c with + | Prod (_,_,c) -> head c + | LetIn (_,_,_,c) -> head c + | _ -> c + +let constr_to_section_path c = match kind_of_term c with + | Const sp -> sp + | _ -> raise No_section_path + +let xor a b = (a or b) & (not (a & b)) + +let plain_display ref a c = + let pc = prterm_env a c in + let pr = pr_global ref in + msg (hov 2 (pr ++ str":" ++ spc () ++ pc) ++ fnl ()) + +let filter_by_module (module_list:dir_path list) (accept:bool) + (ref:global_reference) _ _ = + try + let sp = sp_of_global ref in + let sl = dirpath sp in + let rec filter_aux = function + | m :: tl -> (not (is_dirpath_prefix_of m sl)) && (filter_aux tl) + | [] -> true + in + xor accept (filter_aux module_list) + with No_section_path -> + false + +let gref_eq = + IndRef (Libnames.encode_kn Coqlib.logic_module (id_of_string "eq"), 0) +let gref_eqT = + IndRef (Libnames.encode_kn Coqlib.logic_type_module (id_of_string "eqT"), 0) + +let mk_rewrite_pattern1 eq pattern = + PApp (PRef eq, [| PMeta None; pattern; PMeta None |]) + +let mk_rewrite_pattern2 eq pattern = + PApp (PRef eq, [| PMeta None; PMeta None; pattern |]) + +let pattern_filter pat _ a c = + try + try + is_matching pat (head c) + with _ -> + is_matching + pat (head (Typing.type_of (Global.env()) Evd.empty c)) + with UserError _ -> + false + +let filtered_search filter_function display_function ref = + crible ref + (fun s a c -> if filter_function s a c then display_function s a c) + +let rec id_from_pattern = function + | PRef gr -> gr +(* should be appear as a PRef (VarRef sp) !! + | PVar id -> Nametab.locate (make_qualid [] (string_of_id id)) + *) + | PApp (p,_) -> id_from_pattern p + | _ -> error "the pattern is not simple enough" + +let raw_pattern_search extra_filter display_function pat = + let name = id_from_pattern pat in + filtered_search + (fun s a c -> (pattern_filter pat s a c) & extra_filter s a c) + display_function name + +let raw_search_rewrite extra_filter display_function pattern = + filtered_search + (fun s a c -> + ((pattern_filter (mk_rewrite_pattern1 gref_eq pattern) s a c) || + (pattern_filter (mk_rewrite_pattern2 gref_eq pattern) s a c)) + && extra_filter s a c) + display_function gref_eq +(* + ; + filtered_search + (fun s a c -> + ((pattern_filter (mk_rewrite_pattern1 gref_eqT pattern) s a c) || + (pattern_filter (mk_rewrite_pattern2 gref_eqT pattern) s a c)) + && extra_filter s a c) + display_function gref_eqT +*) + +let text_pattern_search extra_filter = + raw_pattern_search extra_filter plain_display + +let text_search_rewrite extra_filter = + raw_search_rewrite extra_filter plain_display + +let filter_by_module_from_list = function + | [], _ -> (fun _ _ _ -> true) + | l, outside -> filter_by_module l (not outside) + +let search_by_head ref inout = + filtered_search (filter_by_module_from_list inout) plain_display ref + +let search_rewrite pat inout = + text_search_rewrite (filter_by_module_from_list inout) pat + +let search_pattern pat inout = + text_pattern_search (filter_by_module_from_list inout) pat + + +let gen_filtered_search filter_function display_function = + gen_crible None + (fun s a c -> if filter_function s a c then display_function s a c) + +(** SearchAbout *) + +let name_of_reference ref = string_of_id (id_of_global ref) + +type glob_search_about_item = + | GlobSearchRef of global_reference + | GlobSearchString of string + +let search_about_item (itemref,typ) = function + | GlobSearchRef ref -> Termops.occur_term (constr_of_reference ref) typ + | GlobSearchString s -> string_string_contains (name_of_reference itemref) s + +let raw_search_about filter_modules display_function l = + let filter ref' env typ = + filter_modules ref' env typ && + List.for_all (search_about_item (ref',typ)) l + in + gen_filtered_search filter display_function + +let search_about ref inout = + raw_search_about (filter_by_module_from_list inout) plain_display ref |