Imported Upstream version 8.8.2upstream/8.8.2

1 files changed, 0 insertions, 315 deletions

diff --git a/toplevel/search.ml b/toplevel/search.ml
deleted file mode 100644
index ff3c7a4f..00000000
--- a/toplevel/search.ml
+++ /dev/null
@@ -1,315 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Pp
-open Util
-open Names
-open Term
-open Declarations
-open Libobject
-open Environ
-open Pattern
-open Printer
-open Libnames
-open Globnames
-open Nametab
-open Goptions
-
-type filter_function = global_reference -> env -> constr -> bool
-type display_function = global_reference -> env -> constr -> unit
-
-(* This option restricts the output of [SearchPattern ...],
-[SearchAbout ...], etc. to the names of the symbols matching the
-query, separated by a newline. This type of output is useful for
-editors (like emacs), to generate a list of completion candidates
-without having to parse thorugh the types of all symbols. *)
-
-type glob_search_about_item =
-  | GlobSearchSubPattern of constr_pattern
-  | GlobSearchString of string
-
-module SearchBlacklist =
-  Goptions.MakeStringTable
-    (struct
-      let key = ["Search";"Blacklist"]
-      let title = "Current search blacklist : "
-      let member_message s b =
-	str "Search blacklist does " ++ (if b then mt () else str "not ") ++ str "include " ++ str s
-      let synchronous = true
-     end)
-
-(* The functions iter_constructors and iter_declarations 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 iter_constructors indsp u fn env nconstr =
-  for i = 1 to nconstr do
-    let typ = Inductiveops.type_of_constructor env ((indsp, i), u) in
-    fn (ConstructRef (indsp, i)) env typ
-  done
-
-let iter_named_context_name_type f =
-  let open Context.Named.Declaration in
-  List.iter (fun decl -> f (get_id decl) (get_type decl))
-
-(* General search over hypothesis of a goal *)
-let iter_hypothesis glnum (fn : global_reference -> env -> constr -> unit) =
-  let env = Global.env () in
-  let iter_hyp idh typ = fn (VarRef idh) env typ in
-  let evmap,e = Pfedit.get_goal_context glnum in
-  let pfctxt = named_context e in
-  iter_named_context_name_type iter_hyp pfctxt
-
-(* General search over declarations *)
-let iter_declarations (fn : global_reference -> env -> constr -> unit) =
-  let open Context.Named.Declaration in
-  let env = Global.env () in
-  let iter_obj (sp, kn) lobj = match object_tag lobj with
-  | "VARIABLE" ->
-    begin try
-      let decl = Global.lookup_named (basename sp) in
-      fn (VarRef (get_id decl)) env (get_type decl)
-    with Not_found -> (* we are in a section *) () end
-  | "CONSTANT" ->
-    let cst = Global.constant_of_delta_kn kn in
-    let gr = ConstRef cst in
-    let typ = Global.type_of_global_unsafe gr in
-      fn gr env typ
-  | "INDUCTIVE" ->
-    let mind = Global.mind_of_delta_kn kn in
-    let mib = Global.lookup_mind mind in
-    let iter_packet i mip =
-      let ind = (mind, i) in
-      let u = Declareops.inductive_instance mib in
-      let i = (ind, u) in
-      let typ = Inductiveops.type_of_inductive env i in
-      let () = fn (IndRef ind) env typ in
-      let len = Array.length mip.mind_user_lc in
-      iter_constructors ind u fn env len
-    in
-    Array.iteri iter_packet mib.mind_packets
-  | _ -> ()
-  in
-  try Declaremods.iter_all_segments iter_obj
-  with Not_found -> ()
-
-let generic_search glnumopt fn =
-  (match glnumopt with
-  | None -> ()
-  | Some glnum ->  iter_hypothesis glnum fn);
-  iter_declarations fn
-
-(** Filters *)
-
-(** This function tries to see whether the conclusion matches a pattern. *)
-(** FIXME: this is quite dummy, we may find a more efficient algorithm. *)
-let rec pattern_filter pat ref env typ =
-  let typ = strip_outer_cast typ in
-  if Constr_matching.is_matching env Evd.empty pat typ then true
-  else match kind_of_term typ with
-  | Prod (_, _, typ)
-  | LetIn (_, _, _, typ) -> pattern_filter pat ref env typ
-  | _ -> false
-
-let rec head_filter pat ref env typ =
-  let typ = strip_outer_cast typ in
-  if Constr_matching.is_matching_head env Evd.empty pat typ then true
-  else match kind_of_term typ with
-  | Prod (_, _, typ)
-  | LetIn (_, _, _, typ) -> head_filter pat ref env typ
-  | _ -> false
-
-let full_name_of_reference ref =
-  let (dir,id) = repr_path (path_of_global ref) in
-  DirPath.to_string dir ^ "." ^ Id.to_string id
-
-(** Whether a reference is blacklisted *)
-let blacklist_filter_aux () =
-  let l = SearchBlacklist.elements () in
-  fun ref env typ ->
-  let name = full_name_of_reference ref in
-  let is_not_bl str = not (String.string_contains ~where:name ~what:str) in
-  List.for_all is_not_bl l
-
-let module_filter (mods, outside) ref env typ =
-  let sp = path_of_global ref in
-  let sl = dirpath sp in
-  let is_outside md = not (is_dirpath_prefix_of md sl) in
-  let is_inside md = is_dirpath_prefix_of md sl in
-  if outside then List.for_all is_outside mods
-  else List.is_empty mods || List.exists is_inside mods
-
-let name_of_reference ref = Id.to_string (basename_of_global ref)
-
-let search_about_filter query gr env typ = match query with
-| GlobSearchSubPattern pat ->
-  Constr_matching.is_matching_appsubterm ~closed:false env Evd.empty pat typ
-| GlobSearchString s ->
-  String.string_contains ~where:(name_of_reference gr) ~what:s
-
-
-(** SearchPattern *)
-
-let search_pattern gopt pat mods pr_search =
-  let blacklist_filter = blacklist_filter_aux () in
-  let filter ref env typ =
-    module_filter mods ref env typ &&
-    pattern_filter pat ref env typ &&
-    blacklist_filter ref env typ
-  in
-  let iter ref env typ =
-    if filter ref env typ then pr_search ref env typ
-  in
-  generic_search gopt iter
-
-(** SearchRewrite *)
-
-let eq = Coqlib.glob_eq
-
-let rewrite_pat1 pat =
-  PApp (PRef eq, [| PMeta None; pat; PMeta None |])
-
-let rewrite_pat2 pat =
-  PApp (PRef eq, [| PMeta None; PMeta None; pat |])
-
-let search_rewrite gopt pat mods pr_search =
-  let pat1 = rewrite_pat1 pat in
-  let pat2 = rewrite_pat2 pat in
-  let blacklist_filter = blacklist_filter_aux () in
-  let filter ref env typ =
-    module_filter mods ref env typ &&
-    (pattern_filter pat1 ref env typ ||
-       pattern_filter pat2 ref env typ) &&
-    blacklist_filter ref env typ
-  in
-  let iter ref env typ =
-    if filter ref env typ then pr_search ref env typ
-  in
-  generic_search gopt iter
-
-(** Search *)
-
-let search_by_head gopt pat mods pr_search =
-  let blacklist_filter = blacklist_filter_aux () in
-  let filter ref env typ =
-    module_filter mods ref env typ &&
-    head_filter pat ref env typ &&
-    blacklist_filter ref env typ
-  in
-  let iter ref env typ =
-    if filter ref env typ then pr_search ref env typ
-  in
-  generic_search gopt iter
-
-(** SearchAbout *)
-
-let search_about gopt items mods pr_search =
-  let blacklist_filter = blacklist_filter_aux () in
-  let filter ref env typ =
-    let eqb b1 b2 = if b1 then b2 else not b2 in
-    module_filter mods ref env typ &&
-    List.for_all
-      (fun (b,i) -> eqb b (search_about_filter i ref env typ)) items &&
-    blacklist_filter ref env typ
-  in
-  let iter ref env typ =
-    if filter ref env typ then pr_search ref env typ
-  in
-  generic_search gopt iter
-
-type search_constraint =
-  | Name_Pattern of Str.regexp
-  | Type_Pattern of Pattern.constr_pattern
-  | SubType_Pattern of Pattern.constr_pattern
-  | In_Module of Names.DirPath.t
-  | Include_Blacklist
-
-type 'a coq_object = {
-  coq_object_prefix : string list;
-  coq_object_qualid : string list;
-  coq_object_object : 'a;
-}
-
-let interface_search =
-  let rec extract_flags name tpe subtpe mods blacklist = function
-  | [] -> (name, tpe, subtpe, mods, blacklist)
-  | (Name_Pattern regexp, b) :: l ->
-    extract_flags ((regexp, b) :: name) tpe subtpe mods blacklist l
-  | (Type_Pattern pat, b) :: l ->
-    extract_flags name ((pat, b) :: tpe) subtpe mods blacklist l
-  | (SubType_Pattern pat, b) :: l ->
-    extract_flags name tpe ((pat, b) :: subtpe) mods blacklist l
-  | (In_Module id, b) :: l ->
-    extract_flags name tpe subtpe ((id, b) :: mods) blacklist l
-  | (Include_Blacklist, b) :: l ->
-    extract_flags name tpe subtpe mods b l
-  in
-  fun ?glnum flags ->
-  let (name, tpe, subtpe, mods, blacklist) =
-    extract_flags [] [] [] [] false flags
-  in
-  let blacklist_filter = blacklist_filter_aux () in
-  let filter_function ref env constr =
-    let id = Names.Id.to_string (Nametab.basename_of_global ref) in
-    let path = Libnames.dirpath (Nametab.path_of_global ref) in
-    let toggle x b = if x then b else not b in
-    let match_name (regexp, flag) =
-      toggle (Str.string_match regexp id 0) flag
-    in
-    let match_type (pat, flag) =
-      toggle (Constr_matching.is_matching env Evd.empty pat constr) flag
-    in
-    let match_subtype (pat, flag) =
-      toggle
-        (Constr_matching.is_matching_appsubterm ~closed:false 
-	   env Evd.empty pat constr) flag
-    in
-    let match_module (mdl, flag) =
-      toggle (Libnames.is_dirpath_prefix_of mdl path) flag
-    in
-    List.for_all match_name name &&
-    List.for_all match_type tpe &&
-    List.for_all match_subtype subtpe &&
-    List.for_all match_module mods &&
-    (blacklist || blacklist_filter ref env constr)
-  in
-  let ans = ref [] in
-  let print_function ref env constr =
-    let fullpath = DirPath.repr (Nametab.dirpath_of_global ref) in
-    let qualid = Nametab.shortest_qualid_of_global Id.Set.empty ref in
-    let (shortpath, basename) = Libnames.repr_qualid qualid in
-    let shortpath = DirPath.repr shortpath in
-    (* [shortpath] is a suffix of [fullpath] and we're looking for the missing
-       prefix *)
-    let rec prefix full short accu = match full, short with
-    | _, [] ->
-      let full = List.rev_map Id.to_string full in
-      (full, accu)
-    | _ :: full, m :: short ->
-      prefix full short (Id.to_string m :: accu)
-    | _ -> assert false
-    in
-    let (prefix, qualid) = prefix fullpath shortpath [Id.to_string basename] in
-    let answer = {
-      coq_object_prefix = prefix;
-      coq_object_qualid = qualid;
-      coq_object_object = string_of_ppcmds (pr_lconstr_env env Evd.empty constr);
-    } in
-    ans := answer :: !ans;
-  in
-  let iter ref env typ =
-    if filter_function ref env typ then print_function ref env typ
-  in
-  let () = generic_search glnum iter in
-  !ans
-
-let blacklist_filter ref env typ =
-  blacklist_filter_aux () ref env typ