From 993acb64bcfd9a250f7a46220defe9481533e750 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Fri, 10 Nov 2023 16:38:07 +0100 Subject: [PATCH] Fix Search is:Scheme Fix #18298 --- .../18537-fix-search-scheme.rst | 8 +++++++ tactics/declareScheme.ml | 2 +- tactics/declareScheme.mli | 8 ++++--- test-suite/output/SearchScheme.out | 22 +++++++++++++++++++ test-suite/output/SearchScheme.v | 2 ++ vernac/comSearch.ml | 10 ++++++++- 6 files changed, 47 insertions(+), 5 deletions(-) create mode 100644 doc/changelog/08-vernac-commands-and-options/18537-fix-search-scheme.rst create mode 100644 test-suite/output/SearchScheme.out create mode 100644 test-suite/output/SearchScheme.v diff --git a/doc/changelog/08-vernac-commands-and-options/18537-fix-search-scheme.rst b/doc/changelog/08-vernac-commands-and-options/18537-fix-search-scheme.rst new file mode 100644 index 0000000000000..352d9478e0dc9 --- /dev/null +++ b/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 `_, + fixes `#18298 `_, + by Gaëtan Gilbert). diff --git a/tactics/declareScheme.ml b/tactics/declareScheme.ml index 1249ff8058d6d..8807847c8ca70 100644 --- a/tactics/declareScheme.ml +++ b/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 diff --git a/tactics/declareScheme.mli b/tactics/declareScheme.mli index d10cb4ef1584f..cc9c97170a5c9 100644 --- a/tactics/declareScheme.mli +++ b/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 diff --git a/test-suite/output/SearchScheme.out b/test-suite/output/SearchScheme.out new file mode 100644 index 0000000000000..b437edf9c7003 --- /dev/null +++ b/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 diff --git a/test-suite/output/SearchScheme.v b/test-suite/output/SearchScheme.v new file mode 100644 index 0000000000000..bcc3d86e9ceb8 --- /dev/null +++ b/test-suite/output/SearchScheme.v @@ -0,0 +1,2 @@ +Search nat is:Scheme. +(* was "le : nat -> nat -> Prop" *) diff --git a/vernac/comSearch.ml b/vernac/comSearch.ml index b0e3a114eae8c..b16154be2f85e 100644 --- a/vernac/comSearch.ml +++ b/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))