Search: Adding support for an "is:kind" clause.

library/kindops.ml

@@ -35,3 +35,13 @@ let string_of_definition_object_kind = function
   | Let -> "Let"
   | (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) ->
     CErrors.anomaly (Pp.str "Internal definition kind.")
+
+let string_of_assumption_kind = function
+  | Definitional -> "Parameter"
+  | Logical -> "Axiom"
+  | Conjectural -> "Conjecture"
+
+let string_of_logical_kind = function
+  | IsAssumption k -> string_of_assumption_kind k
+  | IsDefinition k -> string_of_definition_object_kind k
+  | IsProof k -> string_of_theorem_kind k

library/kindops.mli

@@ -15,3 +15,4 @@ open Decl_kinds
 val logical_kind_of_goal_kind : goal_object_kind -> logical_kind
 val string_of_theorem_kind : theorem_kind -> string
 val string_of_definition_object_kind : definition_object_kind -> string
+val string_of_logical_kind : logical_kind -> string

plugins/ssr/ssrvernac.mlg

@@ -403,9 +403,9 @@ let all_true _ = true
 let rec interp_search_about args accu = match args with
 | [] -> accu
 | (flag, arg) :: rem ->
-  fun gr env typ ->
-    let ans = Search.search_about_filter arg gr env typ in
-    (if flag then ans else not ans) && interp_search_about rem accu gr env typ
+  fun gr kind env typ ->
+    let ans = Search.search_about_filter arg gr kind env typ in
+    (if flag then ans else not ans) && interp_search_about rem accu gr kind env typ
 
 let interp_search_arg arg =
   let arg = List.map (fun (x,arg) -> x, match arg with
@@ -428,7 +428,7 @@ let interp_search_arg arg =
   let is_string =
     function (_, Search.GlobSearchString _) -> true | _ -> false in
   let a2, a3 = List.partition is_string a1 in
-  interp_search_about (a2 @ a3) (fun gr env typ -> hpat typ)
+  interp_search_about (a2 @ a3) (fun gr kind env typ -> hpat typ)
 
 (* Module path postfilter *)
 
@@ -459,10 +459,10 @@ let interp_modloc mr =
     CErrors.user_err ?loc:qid.CAst.loc (str "No Module " ++ pr_qualid qid) in
   let mr_out, mr_in = List.partition fst mr in
   let interp_bmod b = function
-  | [] -> fun _ _ _ -> true
+  | [] -> fun _ _ _ _ -> true
   | rmods -> Search.module_filter (List.map interp_mod rmods, b) in
   let is_in = interp_bmod false mr_in and is_out = interp_bmod true mr_out in
-  fun gr env typ -> is_in gr env typ && is_out gr env typ
+  fun gr kind env typ -> is_in gr kind env typ && is_out gr kind env typ
 
 (* The unified, extended vernacular "Search" command *)
 
@@ -476,9 +476,9 @@ VERNAC COMMAND EXTEND SsrSearchPattern CLASSIFIED AS QUERY
 | [ "Search" ssr_search_arg(a) ssr_modlocs(mr) ] ->
   { let hpat = interp_search_arg a in
     let in_mod = interp_modloc mr in
-    let post_filter gr env typ = in_mod gr env typ && hpat gr env typ in
-    let display gr env typ =
-      if post_filter gr env typ then ssrdisplaysearch gr env typ
+    let post_filter gr kind env typ = in_mod gr kind env typ && hpat gr kind env typ in
+    let display gr kind env typ =
+      if post_filter gr kind env typ then ssrdisplaysearch gr env typ
     in
     Search.generic_search None display }
 END

vernac/g_vernac.mlg

@@ -43,6 +43,8 @@ let subprf = Entry.create "vernac:subprf"
 
 let class_rawexpr = Entry.create "vernac:class_rawexpr"
 let thm_token = Entry.create "vernac:thm_token"
+let def_token = Entry.create "vernac:def_token"
+let assumption_token = Entry.create "vernac:assumption_token"
 let def_body = Entry.create "vernac:def_body"
 let decl_notation = Entry.create "vernac:decl_notation"
 let record_field = Entry.create "vernac:record_field"
@@ -184,7 +186,7 @@ let name_of_ident_decl : ident_decl -> name_decl =
 
 (* Gallina declarations *)
 GRAMMAR EXTEND Gram
-  GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion
+  GLOBAL: gallina gallina_ext thm_token def_token assumption_token def_body of_type_with_opt_coercion
     record_field decl_notation rec_definition ident_decl univ_decl;
 
   gallina:
@@ -1058,6 +1060,8 @@ GRAMMAR EXTEND Gram
     [ [ b = positive_search_mark; test_id_colon;
         where = search_where; ":"; s = ne_string; sc = OPT scope ->
             { (b, SearchString (where,s,sc)) }
+      | b = positive_search_mark; IDENT "is"; ":"; kl = logical_kinds ->
+            { (b, SearchKind kl) }
       | b = positive_search_mark; s = ne_string; sc = OPT scope ->
             { (b, SearchString (Search.Anywhere,s,sc)) }
       | b = positive_search_mark; test_id_colon;
@@ -1067,6 +1071,21 @@ GRAMMAR EXTEND Gram
             { (b, SearchSubPattern (Search.Anywhere,p)) }
       ] ]
   ;
+  logical_kinds:
+    [ [ "[" ; l = LIST1 logical_kind; "]" -> { l }
+      | k = logical_kind -> { [k] } ] ]
+  ;
+  logical_kind:
+    [ [ k = thm_token -> { IsProof k }
+      | k = assumption_token -> { IsAssumption (snd k) }
+      | k = extended_def_token -> { IsDefinition k } ] ]
+  ;
+  extended_def_token:
+    [ [ k = def_token -> { snd k }
+      | IDENT "Coercion" -> { Coercion }
+      | IDENT "Instance" -> { Instance }
+      | IDENT "Scheme" -> { Scheme } ] ]
+  ;
   search_where:
     [ [ IDENT "hyp" -> { Search.InHyp } | IDENT "concl" -> { Search.InConcl } ] ]
   ;

vernac/lemmas.ml

@@ -221,9 +221,9 @@ let check_name_freshness locality {CAst.loc;v=id} : unit =
 
 let save_remaining_recthms (locality,p,kind) norm univs body opaq i (id,(t_i,(_,imps))) =
   let t_i = norm t_i in
-  let k = IsAssumption Conjectural in
   match body with
   | None ->
+      let k = IsAssumption Conjectural in
       (match locality with
       | Discharge ->
           let impl = false in (* copy values from Vernacentries *)

vernac/ppvernac.ml

@@ -149,6 +149,7 @@ open Pputils
       match c with
         | SearchSubPattern (where,p) -> pr_search_where where ++ pr_constr_pattern_expr p
         | SearchString (where,s,sc) -> pr_search_where where ++ qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
+        | SearchKind kind -> str "is:" ++ str (String.concat "," (List.map Kindops.string_of_logical_kind kind))
 
   let pr_search a gopt b pr_p =
     pr_opt (fun g -> Goal_select.pr_goal_selector g ++ str ":"++ spc()) gopt

vernac/search.ml

@@ -21,8 +21,10 @@ open Globnames
 
 module NamedDecl = Context.Named.Declaration
 
-type filter_function = GlobRef.t -> env -> constr -> bool
-type display_function = GlobRef.t -> env -> constr -> unit
+type filter_function =
+  GlobRef.t -> Decl_kinds.logical_kind option -> env -> constr -> bool
+type display_function =
+  GlobRef.t -> Decl_kinds.logical_kind option -> env -> constr -> unit
 
 (* This option restricts the output of [SearchPattern ...],
 [SearchAbout ...], etc. to the names of the symbols matching the
@@ -35,6 +37,7 @@ type glob_search_where = InHyp | InConcl | Anywhere
 type glob_search_about_item =
   | GlobSearchSubPattern of glob_search_where * constr_pattern
   | GlobSearchString of string
+  | GlobSearchKind of Decl_kinds.logical_kind list
 
 module SearchBlacklist =
   Goptions.MakeStringTable
@@ -55,34 +58,35 @@ module SearchBlacklist =
 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
+    fn (ConstructRef (indsp, i)) None env typ
   done
 
 let iter_named_context_name_type f =
   List.iter (fun decl -> f (NamedDecl.get_id decl) (NamedDecl.get_type decl))
 
 (* General search over hypothesis of a goal *)
-let iter_hypothesis glnum (fn : GlobRef.t -> env -> constr -> unit) =
+let iter_hypothesis glnum (fn : GlobRef.t -> Decl_kinds.logical_kind option -> env -> constr -> unit) =
   let env = Global.env () in
-  let iter_hyp idh typ = fn (VarRef idh) env typ in
+  let iter_hyp idh typ = fn (VarRef idh) None 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 : GlobRef.t -> env -> constr -> unit) =
+let iter_declarations (fn : GlobRef.t -> Decl_kinds.logical_kind option -> env -> constr -> unit) =
   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 (NamedDecl.get_id decl)) env (NamedDecl.get_type decl)
+      fn (VarRef (NamedDecl.get_id decl)) None env (NamedDecl.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, _) = Typeops.type_of_global_in_context (Global.env ()) gr in
-      fn gr env typ
+    let kind = Decls.constant_kind cst in
+      fn gr (Some kind) env typ
   | "INDUCTIVE" ->
     let mind = Global.mind_of_delta_kn kn in
     let mib = Global.lookup_mind mind in
@@ -91,7 +95,7 @@ let iter_declarations (fn : GlobRef.t -> env -> constr -> unit) =
       let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in
       let i = (ind, u) in
       let typ = Inductiveops.type_of_inductive env i in
-      let () = fn (IndRef ind) env typ in
+      let () = fn (IndRef ind) None env typ in
       let len = Array.length mip.mind_user_lc in
       iter_constructors ind u fn env len
     in
@@ -118,7 +122,7 @@ module ConstrPriority = struct
 
   (* The priority is memoised here. Because of the very localised use
      of this module, it is not worth it making a convenient interface. *)
-  type t = GlobRef.t * Environ.env * Constr.t * priority
+  type t = GlobRef.t * Decl_kinds.logical_kind option * Environ.env * Constr.t * priority
   and priority = int
 
   module ConstrSet = CSet.Make(Constr)
@@ -143,7 +147,7 @@ module ConstrPriority = struct
   let priority t : priority =
     -(3*(num_symbols t) + size t)
 
-  let compare (_,_,_,p1) (_,_,_,p2) =
+  let compare (_,_,_,_,p1) (_,_,_,_,p2) =
     Pervasives.compare p1 p2
 end
 
@@ -158,16 +162,16 @@ let rec iter_priority_queue q fn =
       with Heap.EmptyHeap -> None
   end in
   match next with
-  | Some (gref,env,t,_) ->
-    fn gref env t;
+  | Some (gref,kind,env,t,_) ->
+    fn gref kind env t;
     iter_priority_queue (PriorityQueue.remove q) fn
   | None -> ()
 
 let prioritize_search seq fn =
   let acc = ref PriorityQueue.empty in
-  let iter gref env t =
+  let iter gref kind env t =
     let p = ConstrPriority.priority t in
-    acc := PriorityQueue.add (gref,env,t,p) !acc
+    acc := PriorityQueue.add (gref,kind,env,t,p) !acc
   in
   let () = seq iter in
   iter_priority_queue !acc fn
@@ -199,12 +203,12 @@ let full_name_of_reference ref =
 (** Whether a reference is blacklisted *)
 let blacklist_filter_aux () =
   let l = SearchBlacklist.elements () in
-  fun ref env typ ->
+  fun ref kind 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 module_filter (mods, outside) ref kind env typ =
   let sp = Nametab.path_of_global ref in
   let sl = dirpath sp in
   let is_outside md = not (is_dirpath_prefix_of md sl) in
@@ -214,7 +218,7 @@ let module_filter (mods, outside) ref env typ =
 
 let name_of_reference ref = Id.to_string (Nametab.basename_of_global ref)
 
-let search_about_filter query gr env typ = match query with
+let search_about_filter query gr kind env typ = match query with
 | GlobSearchSubPattern (where,pat) ->
   let open Context.Rel.Declaration in
   let typl = match where with
@@ -230,19 +234,21 @@ let search_about_filter query gr env typ = match query with
   List.exists (fun typ -> Constr_matching.is_matching_appsubterm ~closed:false env (Evd.from_env env) pat (EConstr.of_constr typ)) typl
 | GlobSearchString s ->
   String.string_contains ~where:(name_of_reference gr) ~what:s
+| GlobSearchKind l ->
+  match kind with None -> false | Some k -> List.mem k l
 
 
 (** 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 &&
+  let filter ref kind env typ =
+    module_filter mods ref kind env typ &&
     pattern_filter pat ref env (Evd.from_env env) (* FIXME *) (EConstr.of_constr typ) &&
-    blacklist_filter ref env typ
+    blacklist_filter ref kind env typ
   in
-  let iter ref env typ =
-    if filter ref env typ then pr_search ref env typ
+  let iter ref kind env typ =
+    if filter ref kind env typ then pr_search ref kind env typ
   in
   generic_search gopt iter
 
@@ -260,44 +266,44 @@ 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 &&
+  let filter ref kind env typ =
+    module_filter mods ref kind env typ &&
     (pattern_filter pat1 ref env (Evd.from_env env) (* FIXME *) (EConstr.of_constr typ) ||
        pattern_filter pat2 ref env (Evd.from_env env) (EConstr.of_constr typ)) &&
-    blacklist_filter ref env typ
+    blacklist_filter ref kind env typ
   in
-  let iter ref env typ =
-    if filter ref env typ then pr_search ref env typ
+  let iter ref kind env typ =
+    if filter ref kind env typ then pr_search ref kind 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 &&
+  let filter ref kind env typ =
+    module_filter mods ref kind env typ &&
     head_filter pat ref env (Evd.from_env env) (* FIXME *) (EConstr.of_constr typ) &&
-    blacklist_filter ref env typ
+    blacklist_filter ref kind env typ
   in
-  let iter ref env typ =
-    if filter ref env typ then pr_search ref env typ
+  let iter ref kind env typ =
+    if filter ref kind env typ then pr_search ref kind 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 filter ref kind env typ =
     let eqb b1 b2 = if b1 then b2 else not b2 in
-    module_filter mods ref env typ &&
+    module_filter mods ref kind env typ &&
     List.for_all
-      (fun (b,i) -> eqb b (search_about_filter i ref env typ)) items &&
-    blacklist_filter ref env typ
+      (fun (b,i) -> eqb b (search_about_filter i ref kind env typ)) items &&
+    blacklist_filter ref kind env typ
   in
-  let iter ref env typ =
-    if filter ref env typ then pr_search ref env typ
+  let iter ref kind env typ =
+    if filter ref kind env typ then pr_search ref kind env typ
   in
   generic_search gopt iter
 
@@ -355,7 +361,7 @@ let interface_search =
     List.for_all match_type tpe &&
     List.for_all match_subtype subtpe &&
     List.for_all match_module mods &&
-    (blacklist || blacklist_filter ref env constr)
+    (blacklist || blacklist_filter ref kind env constr)
   in
   let ans = ref [] in
   let print_function ref env constr =
@@ -381,7 +387,7 @@ let interface_search =
     } in
     ans := answer :: !ans;
   in
-  let iter ref env typ =
+  let iter ref kind env typ =
     if filter_function ref env typ then print_function ref env typ
   in
   let () = generic_search glnum iter in

vernac/search.mli

@@ -20,9 +20,12 @@ type glob_search_where = InHyp | InConcl | Anywhere
 type glob_search_about_item =
   | GlobSearchSubPattern of glob_search_where * constr_pattern
   | GlobSearchString of string
+  | GlobSearchKind of Decl_kinds.logical_kind list
 
-type filter_function = GlobRef.t -> env -> constr -> bool
-type display_function = GlobRef.t -> env -> constr -> unit
+type filter_function =
+  GlobRef.t -> Decl_kinds.logical_kind option -> env -> constr -> bool
+type display_function =
+  GlobRef.t -> Decl_kinds.logical_kind option -> env -> constr -> unit
 
 (** {6 Generic filter functions} *)