Merge PR coq#18537: Fix Search is:Scheme

Reviewed-by: ppedrot
Reviewed-by: herbelin
Ack-by: Villetaneuse
Co-authored-by: ppedrot <[email protected]>

doc/changelog/08-vernac-commands-and-options/18537-fix-search-scheme.rst

@@ -0,0 +1,8 @@
+- **Fixed:**
+  :cmd:`Search` with modifier `is:Scheme` restricted the search to inductive types
+  which have schemes instead of the schemes themselves.
+  For instance `Search nat is:Scheme` with just the prelude loaded would return `le`
+  i.e. the only inductive type whose type mentions `nat`
+  (`#18537 <https://github.com/coq/coq/pull/18537>`_,
+  fixes `#18298 <https://github.com/coq/coq/issues/18298>`_,
+  by Gaëtan Gilbert).

tactics/declareScheme.ml

@@ -41,4 +41,4 @@ let declare_scheme kind indcl =
 
 let lookup_scheme kind ind = CString.Map.find kind (Indmap.find ind !scheme_map)
 
-let all_schemes () = Indmap.domain !scheme_map
+let all_schemes () = !scheme_map

tactics/declareScheme.mli

@@ -8,6 +8,8 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-val declare_scheme : string -> (Names.inductive * Names.Constant.t) array -> unit
-val lookup_scheme : string -> Names.inductive -> Names.Constant.t
-val all_schemes : unit -> Names.Indset.t
+open Names
+
+val declare_scheme : string -> (inductive * Constant.t) array -> unit
+val lookup_scheme : string -> inductive -> Constant.t
+val all_schemes : unit -> Constant.t CString.Map.t Indmap.t

test-suite/output/SearchScheme.out

@@ -0,0 +1,22 @@
+nat_sind:
+  forall P : nat -> SProp,
+  P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n
+nat_rec:
+  forall P : nat -> Set,
+  P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n
+nat_ind:
+  forall P : nat -> Prop,
+  P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n
+nat_rect:
+  forall P : nat -> Type,
+  P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n
+le_ind:
+  forall (n : nat) (P : nat -> Prop),
+  P n ->
+  (forall m : nat, n <= m -> P m -> P (S m)) ->
+  forall n0 : nat, n <= n0 -> P n0
+le_sind:
+  forall (n : nat) (P : nat -> SProp),
+  P n ->
+  (forall m : nat, n <= m -> P m -> P (S m)) ->
+  forall n0 : nat, n <= n0 -> P n0

test-suite/output/SearchScheme.v

@@ -0,0 +1,2 @@
+Search nat is:Scheme.
+(* was "le : nat -> nat -> Prop" *)

vernac/comSearch.ml

@@ -45,7 +45,15 @@ let kind_searcher = Decls.(function
     Inr (fun gr -> List.exists (fun c -> GlobRef.CanOrd.equal c.Structures.CSTable.solution gr) canonproj)
   | IsDefinition Scheme ->
     let schemes = DeclareScheme.all_schemes () in
-    Inr (fun gr -> Indset.exists (fun c -> GlobRef.CanOrd.equal (GlobRef.IndRef c) gr) schemes)
+    let schemes = lazy begin
+      Indmap.fold (fun _ schemes acc ->
+          CString.Map.fold (fun _ c acc -> Cset.add c acc) schemes acc)
+        schemes Cset.empty
+    end
+    in
+    Inr (function
+        | ConstRef c -> Cset.mem c (Lazy.force schemes)
+        | _ -> false)
   | IsDefinition Instance ->
     let instances = Typeclasses.all_instances () in
     Inr (fun gr -> List.exists (fun c -> GlobRef.CanOrd.equal c.Typeclasses.is_impl gr) instances))