Coq SearchAny Patch

coq-searchany.patch

From 8fa45911905da8fd1732f79ec95b0c9733c07d6c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment=20Pit--Claudel?= <clement.pitclaudel@live.com>
Date: Mon, 16 Feb 2015 08:34:20 -0500
Subject: [PATCH 1/3] vernac: Add a SearchAny command to print all identifiers

"SearchAny" does the same as "SearchPattern _", but it doesn't print
definition bodies, yielding an about 10x reduction in the size of the
answer. This is useful for tools that need to list all identifiers in
context at a given point in a proof (for en example of such a tool see
https://github.com/cpitclaudel/company-coq/)
---
 parsing/g_vernac.ml4      | 2 ++
 toplevel/libtypes.ml      | 1 +
 toplevel/libtypes.mli     | 1 +
 toplevel/search.ml        | 7 +++++++
 toplevel/search.mli       | 1 +
 toplevel/vernacentries.ml | 1 +
 toplevel/vernacexpr.ml    | 1 +
 7 files changed, 14 insertions(+)

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 301370e..de59cfa 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -767,6 +767,8 @@ GEXTEND Gram
 	  VernacSearch (SearchHead c, l)
       | IDENT "SearchPattern"; c = constr_pattern; l = in_or_out_modules ->
 	  VernacSearch (SearchPattern c, l)
+      | IDENT "SearchAny"; l = in_or_out_modules ->
+      VernacSearch (SearchAny, l)
       | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules ->
 	  VernacSearch (SearchRewrite c, l)
       | IDENT "SearchAbout"; s = searchabout_query; l = searchabout_queries ->
diff --git a/toplevel/libtypes.ml b/toplevel/libtypes.ml
index 5977591..0e289ef 100644
--- a/toplevel/libtypes.ml
+++ b/toplevel/libtypes.ml
@@ -89,6 +89,7 @@ let search_pattern pat = TypeDnet.search_pattern !all_types pat
 let search_concl pat = TypeDnet.search_concl !all_types pat
 let search_head_concl pat = TypeDnet.search_head_concl !all_types pat
 let search_eq_concl eq pat = TypeDnet.search_eq_concl !all_types eq pat
+let find_all () = TypeDnet.find_all !all_types
 
 let add typ gr =
   defined_types := TypeDnet.add typ gr !defined_types;
diff --git a/toplevel/libtypes.mli b/toplevel/libtypes.mli
index cec3597..27021ac 100644
--- a/toplevel/libtypes.mli
+++ b/toplevel/libtypes.mli
@@ -24,3 +24,4 @@ val search_pattern : types -> result list
 val search_concl : types -> result list
 val search_head_concl : types -> result list
 val search_eq_concl : constr -> types -> result list
+val find_all : unit -> Libnames.global_reference list
diff --git a/toplevel/search.ml b/toplevel/search.ml
index 19d696a..03126b3 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -110,6 +110,10 @@ let plain_display ref a c =
   let pr = pr_global ref in
   msg (hov 2 (pr ++ str":" ++ spc () ++ pc) ++ fnl ())
 
+let minimal_display ref = (* See plain_display *)
+  let pr = pr_global ref in
+  msg (pr ++ fnl ())
+
 let filter_by_module (module_list:dir_path list) (accept:bool)
   (ref:global_reference) _ _ =
   try
@@ -211,6 +215,9 @@ let filter_blacklist gr _ _ =
 
 let (&&&&&) f g x y z = f x y z && g x y z
 
+let search_any inout = (* See raw_search. Add inout? *)
+  List.iter minimal_display (Libtypes.find_all ())
+
 let search_by_head pat inout =
   text_search_by_head (filter_by_module_from_list inout &&&&& filter_blacklist) pat
 
diff --git a/toplevel/search.mli b/toplevel/search.mli
index 76821e6..675662c 100644
--- a/toplevel/search.mli
+++ b/toplevel/search.mli
@@ -20,6 +20,7 @@ type glob_search_about_item =
   | GlobSearchSubPattern of constr_pattern
   | GlobSearchString of string
 
+val search_any     : dir_path list * bool  -> unit
 val search_by_head : constr -> dir_path list * bool -> unit
 val search_rewrite : constr -> dir_path list * bool -> unit
 val search_pattern : constr -> dir_path list * bool -> unit
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 75efe13..3f2601a 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1369,6 +1369,7 @@ let vernac_search s r =
   | SearchPattern c ->
       let (_,c) = interp_open_constr_patvar Evd.empty (Global.env()) c in
       Search.search_pattern c r
+  | SearchAny -> Search.search_any r
   | SearchRewrite c ->
       let _,pat = interp_open_constr_patvar Evd.empty (Global.env()) c in
       Search.search_rewrite pat r
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 3106e86..358cace 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -77,6 +77,7 @@ type search_about_item =
   | SearchString of string * scope_name option
 
 type searchable =
+  | SearchAny
   | SearchPattern of constr_pattern_expr
   | SearchRewrite of constr_pattern_expr
   | SearchHead of constr_pattern_expr
-- 
2.3.1


From 4c620c7522c8c71c6aaa8386ad829d513b30c870 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment=20Pit--Claudel?= <clement.pitclaudel@live.com>
Date: Mon, 16 Feb 2015 12:19:42 -0500
Subject: [PATCH 2/3] vernac: Fix an incomplete pattern match

---
 parsing/ppvernac.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index f249129..aaaf889 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -136,6 +136,7 @@ let pr_search_about (b,c) =
 
 let pr_search a b pr_p = match a with
   | SearchHead c -> str"Search" ++ spc() ++ pr_p c ++ pr_in_out_modules b
+  | SearchAny -> str"SearchAny" ++ spc() ++ pr_in_out_modules b
   | SearchPattern c -> str"SearchPattern" ++ spc() ++ pr_p c ++ pr_in_out_modules b
   | SearchRewrite c -> str"SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b
   | SearchAbout sl -> str"SearchAbout" ++ spc() ++ str "[" ++ prlist_with_sep spc pr_search_about sl ++ str "]" ++ pr_in_out_modules b
-- 
2.3.1


From 198b9c47dedf4fa3b2a95ab7102b2d2d4ada392f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment=20Pit--Claudel?= <clement.pitclaudel@live.com>
Date: Mon, 16 Feb 2015 12:20:56 -0500
Subject: [PATCH 3/3] search: Add a minimal search option

When set, search results only display symbol names, instead of
displaying full terms. This is useful when the list of symbols is needed
by an external program
---
 interp/constrextern.ml    |  3 +++
 interp/constrextern.mli   |  1 +
 toplevel/search.ml        | 33 ++++++++++++++++++++-------------
 toplevel/vernacentries.ml |  9 +++++++++
 4 files changed, 33 insertions(+), 13 deletions(-)

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index ee529fe..2269ec3 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -40,6 +40,9 @@ let print_arguments = ref false
 (* If true, prints local context of evars, whatever print_arguments *)
 let print_evar_arguments = ref false
 
+(* If true, search results only include symbol names *)
+let search_minimal = ref false
+
 (* This governs printing of implicit arguments.  When
    [print_implicits] is on then [print_implicits_explicit_args] tells
    how implicit args are printed. If on, implicit args are printed
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 55fabab..ea71127 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -41,6 +41,7 @@ val extern_rel_context : constr option -> env ->
   rel_context -> local_binder list
 
 (** Printing options *)
+val search_minimal : bool ref
 val print_implicits : bool ref
 val print_implicits_defensive : bool ref
 val print_arguments : bool ref
diff --git a/toplevel/search.ml b/toplevel/search.ml
index 03126b3..a3e0fe5 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -106,13 +106,12 @@ let rec head c =
 let xor a b = (a or b) & (not (a & b))
 
 let plain_display ref a c =
-  let pc = pr_lconstr_env a c in
   let pr = pr_global ref in
-  msg (hov 2 (pr ++ str":" ++ spc () ++ pc) ++ fnl ())
-
-let minimal_display ref = (* See plain_display *)
-  let pr = pr_global ref in
-  msg (pr ++ fnl ())
+  if !Constrextern.search_minimal then
+    msg (pr ++ fnl ())
+  else
+    let pc = pr_lconstr_env a c in
+    msg (hov 2 (pr ++ str":" ++ spc () ++ pc) ++ fnl ())
 
 let filter_by_module (module_list:dir_path list) (accept:bool)
   (ref:global_reference) _ _ =
@@ -186,14 +185,19 @@ let full_name_of_reference ref =
  * functions to use the new Libtypes facility
  *)
 
+let raw_search_iter env extra_filter display_function gr =
+  let typ = Global.type_of_global gr in
+  if extra_filter gr env typ then
+    display_function gr env typ
+
 let raw_search search_function extra_filter display_function pat =
   let env = Global.env() in
-  List.iter
-    (fun (gr,_,_) ->
-       let typ = Global.type_of_global gr in
-       if extra_filter gr env typ then
-	 display_function gr env typ
-    ) (search_function pat)
+  let it = raw_search_iter env extra_filter display_function in
+  List.iter (fun (gr,_,_) -> it gr) (search_function pat)
+
+let raw_search_identonly search_function extra_filter display_function pat =
+  let env = Global.env() in
+  List.iter (raw_search_iter env extra_filter display_function) (search_function pat)
 
 let text_pattern_search extra_filter =
   raw_search Libtypes.search_concl extra_filter plain_display
@@ -204,6 +208,9 @@ let text_search_rewrite extra_filter =
 let text_search_by_head extra_filter =
   raw_search Libtypes.search_head_concl extra_filter plain_display
 
+let text_search_any extra_filter =
+   raw_search_identonly Libtypes.find_all extra_filter plain_display
+
 let filter_by_module_from_list = function
   | [], _ -> (fun _ _ _ -> true)
   | l, outside -> filter_by_module l (not outside)
@@ -216,7 +223,7 @@ let filter_blacklist gr _ _ =
 let (&&&&&) f g x y z = f x y z && g x y z
 
 let search_any inout = (* See raw_search. Add inout? *)
-  List.iter minimal_display (Libtypes.find_all ())
+  text_search_any (filter_by_module_from_list inout &&&&& filter_blacklist) ()
 
 let search_by_head pat inout =
   text_search_by_head (filter_by_module_from_list inout &&&&& filter_blacklist) pat
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 3f2601a..22e7dfa 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -953,6 +953,15 @@ let make_silent_if_not_pcoq b =
 
 let _ =
   declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "minimal search output";
+      optkey   = ["Search";"Minimal"];
+      optread  = (fun () -> !Constrextern.search_minimal);
+      optwrite = (:=) Constrextern.search_minimal }
+
+let _ =
+  declare_bool_option
     { optsync  = false;
       optdepr  = false;
       optname  = "silent";
-- 
2.3.1