Merge PR #8855: More search options

Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Ack-by: kyoDralliam

3 files changed, 112 insertions, 88 deletions

diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 62cc8ea86b..a9a243868f 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -59,6 +59,8 @@ DELETE: [
 | lookup_at_as_comma
 | test_only_starredidentrefs
 | test_bracket_ident
+| test_hash_ident
+| test_id_colon
 | test_lpar_id_colon
 | test_lpar_id_coloneq  (* todo: grammar seems incorrect, repeats the "(" IDENT ":=" *)
 | test_lpar_id_rpar
@@ -1231,8 +1233,8 @@ query_command: [
 | WITH "SearchPattern" constr_pattern in_or_out_modules
 | REPLACE "SearchRewrite" constr_pattern in_or_out_modules "."
 | WITH "SearchRewrite" constr_pattern in_or_out_modules
-| REPLACE "Search" searchabout_query searchabout_queries "."
-| WITH "Search" searchabout_queries
+| REPLACE "Search" search_query search_queries "."
+| WITH "Search" search_queries
 ]
 
 vernac_toplevel: [
@@ -1457,17 +1459,10 @@ ne_in_or_out_modules: [
 | DELETE "outside" LIST1 global
 ]
 
-searchabout_query: [
-| REPLACE positive_search_mark ne_string OPT scope_delimiter
-| WITH ne_string OPT scope_delimiter
-| REPLACE positive_search_mark constr_pattern
-| WITH constr_pattern
-]
-
-searchabout_queries: [
+search_queries: [
 | DELETE ne_in_or_out_modules
-| REPLACE searchabout_query searchabout_queries
-| WITH LIST1 ( positive_search_mark searchabout_query ) OPT ne_in_or_out_modules
+| REPLACE search_query search_queries
+| WITH LIST1 ( search_query ) OPT ne_in_or_out_modules
 | DELETE (* empty *)
 ]
 
@@ -1475,6 +1470,27 @@ positive_search_mark: [
 | OPTINREF
 ]
 
+SPLICE: [
+| positive_search_mark
+]
+
+search_query: [
+| REPLACE OPT "-" search_item
+| WITH search_item
+| "-" search_query
+| REPLACE OPT "-" "[" LIST1 ( LIST1 search_query ) SEP "|" "]"
+| WITH "[" LIST1 ( LIST1 search_query ) SEP "|" "]"
+]
+
+search_item: [
+| REPLACE search_where ":" ne_string OPT scope_delimiter
+| WITH OPT ( search_where ":" ) ne_string OPT scope_delimiter
+| DELETE ne_string OPT scope_delimiter
+| REPLACE search_where ":" constr_pattern
+| WITH OPT ( search_where ":" ) constr_pattern
+| DELETE constr_pattern
+]
+
 by_notation: [
 | REPLACE ne_string OPT [ "%" IDENT ]
 | WITH ne_string OPT [ "%" scope_key ]
@@ -1485,14 +1501,6 @@ scope_delimiter: [
 | WITH "%" scope_key
 ]
 
-(* Don't show these details *)
-DELETE: [
-| register_token
-| register_prim_token
-| register_type_token
-]
-
-
 decl_notation: [
 | REPLACE ne_lstring ":=" constr only_parsing OPT [ ":" IDENT ]
 | WITH ne_lstring ":=" constr only_parsing OPT [ ":" scope_name ]
@@ -1638,7 +1646,6 @@ SPLICE: [
 | record_binder
 | at_level_opt
 | table_value
-| positive_search_mark
 | in_or_out_modules
 | option_setting
 | orient
@@ -1672,11 +1679,14 @@ SPLICE: [
 | intropatterns
 | instance_name
 | ne_in_or_out_modules
-| searchabout_queries
+| search_queries
 | locatable
 | scope_delimiter
 | bignat
 | one_import_filter_name
+| register_token
+| search_where
+| extended_def_token
 ] (* end SPLICE *)
 
 RENAME: [
@@ -1725,7 +1735,9 @@ RENAME: [
 | record_binder_body field_body
 | class_rawexpr class
 | smart_global smart_qualid
+(*
 | searchabout_query search_item
+*)
 | option_table setting_name
 | argument_spec_block arg_specs
 | more_implicits_block implicits_alt
@@ -1735,8 +1747,6 @@ RENAME: [
 | numnotoption numeral_modifier
 ]
 
-(* todo: positive_search_mark is a lousy name for OPT "-" *)
-
 (* todo: doesn't work if up above... maybe because 'clause' doesn't exist? *)
 clause_dft_concl: [
 | OPTINREF
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 92e9df51d5..1b0a5c28ee 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -798,58 +798,7 @@ gallina: [
 ]
 
 register_token: [
-| register_prim_token
-| register_type_token
-]
-
-register_type_token: [
-| "#int63_type"
-| "#float64_type"
-]
-
-register_prim_token: [
-| "#int63_head0"
-| "#int63_tail0"
-| "#int63_add"
-| "#int63_sub"
-| "#int63_mul"
-| "#int63_div"
-| "#int63_mod"
-| "#int63_lsr"
-| "#int63_lsl"
-| "#int63_land"
-| "#int63_lor"
-| "#int63_lxor"
-| "#int63_addc"
-| "#int63_subc"
-| "#int63_addcarryc"
-| "#int63_subcarryc"
-| "#int63_mulc"
-| "#int63_diveucl"
-| "#int63_div21"
-| "#int63_addmuldiv"
-| "#int63_eq"
-| "#int63_lt"
-| "#int63_le"
-| "#int63_compare"
-| "#float64_opp"
-| "#float64_abs"
-| "#float64_eq"
-| "#float64_lt"
-| "#float64_le"
-| "#float64_compare"
-| "#float64_classify"
-| "#float64_add"
-| "#float64_sub"
-| "#float64_mul"
-| "#float64_div"
-| "#float64_sqrt"
-| "#float64_of_int63"
-| "#float64_normfr_mantissa"
-| "#float64_frshiftexp"
-| "#float64_ldshiftexp"
-| "#float64_next_up"
-| "#float64_next_down"
+| test_hash_ident "#" IDENT
 ]
 
 thm_token: [
@@ -1252,7 +1201,7 @@ query_command: [
 | "SearchHead" constr_pattern in_or_out_modules "."
 | "SearchPattern" constr_pattern in_or_out_modules "."
 | "SearchRewrite" constr_pattern in_or_out_modules "."
-| "Search" searchabout_query searchabout_queries "."
+| "Search" search_query search_queries "."
 ]
 
 printable: [
@@ -1349,14 +1298,48 @@ positive_search_mark: [
 |
 ]
 
-searchabout_query: [
-| positive_search_mark ne_string OPT scope_delimiter
-| positive_search_mark constr_pattern
+search_query: [
+| positive_search_mark search_item
+| positive_search_mark "[" LIST1 ( LIST1 search_query ) SEP "|" "]"
 ]
 
-searchabout_queries: [
+search_item: [
+| test_id_colon search_where ":" ne_string OPT scope_delimiter
+| "is" ":" logical_kind
+| ne_string OPT scope_delimiter
+| test_id_colon search_where ":" constr_pattern
+| constr_pattern
+]
+
+logical_kind: [
+| thm_token
+| assumption_token
+| "Context"
+| extended_def_token
+| "Primitive"
+]
+
+extended_def_token: [
+| def_token
+| "Coercion"
+| "Instance"
+| "Scheme"
+| "Canonical"
+| "Field"
+| "Method"
+]
+
+search_where: [
+| "head"
+| "hyp"
+| "concl"
+| "headhyp"
+| "headconcl"
+]
+
+search_queries: [
 | ne_in_or_out_modules
-| searchabout_query searchabout_queries
+| search_query search_queries
 |
 ]
 
@@ -1910,9 +1893,13 @@ debug: [
 |
 ]
 
+eauto_search_strategy_name: [
+| "bfs"
+| "dfs"
+]
+
 eauto_search_strategy: [
-| "(bfs)"
-| "(dfs)"
+| "(" eauto_search_strategy_name ")"
 |
 ]
 
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 11f06b7b8a..3a327fc748 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -823,7 +823,7 @@ command: [
 | "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident )
 | "Typeclasses" "Transparent" LIST0 qualid
 | "Typeclasses" "Opaque" LIST0 qualid
-| "Typeclasses" "eauto" ":=" OPT "debug" OPT [ "(bfs)" | "(dfs)" ] OPT int
+| "Typeclasses" "eauto" ":=" OPT "debug" OPT ( "(" eauto_search_strategy_name ")" ) OPT int
 | "Proof" "with" ltac_expr OPT [ "using" section_subset_expr ]
 | "Proof" "using" section_subset_expr OPT [ "with" ltac_expr ]
 | "Tactic" "Notation" OPT ( "(" "at" "level" num ")" ) LIST1 ltac_production_item ":=" ltac_expr
@@ -940,7 +940,7 @@ command: [
 | "SearchHead" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
 | "SearchPattern" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
 | "SearchRewrite" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
-| "Search" LIST1 ( OPT "-" search_item ) OPT ( [ "inside" | "outside" ] LIST1 qualid )
+| "Search" LIST1 ( search_query ) OPT ( [ "inside" | "outside" ] LIST1 qualid )
 | "Time" sentence
 | "Redirect" string sentence
 | "Timeout" num sentence
@@ -996,9 +996,31 @@ comment: [
 | num
 ]
 
+search_query: [
+| search_item
+| "-" search_query
+| "[" LIST1 ( LIST1 search_query ) SEP "|" "]"
+]
+
 search_item: [
-| one_term
-| string OPT ( "%" scope_key )
+| OPT ( [ "head" | "hyp" | "concl" | "headhyp" | "headconcl" ] ":" ) string OPT ( "%" scope_key )
+| OPT ( [ "head" | "hyp" | "concl" | "headhyp" | "headconcl" ] ":" ) one_term
+| "is" ":" logical_kind
+]
+
+logical_kind: [
+| thm_token
+| assumption_token
+| "Context"
+| "Definition"
+| "Example"
+| "Coercion"
+| "Instance"
+| "Scheme"
+| "Canonical"
+| "Field"
+| "Method"
+| "Primitive"
 ]
 
 univ_name_list: [
@@ -1085,6 +1107,11 @@ hints_path: [
 | hints_path hints_path
 ]
 
+eauto_search_strategy_name: [
+| "bfs"
+| "dfs"
+]
+
 class: [
 | "Funclass"
 | "Sortclass"