From 011de69dab3afcd265f6e38aab05548654a606c8 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 22 Oct 2020 19:41:15 +0200 Subject: Adding a typed interpretation of patterns. --- interp/constrintern.ml | 9 +++++++++ interp/constrintern.mli | 6 ++++++ 2 files changed, 15 insertions(+) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 959b61a3d7..7dbc6c86a6 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -2471,6 +2471,15 @@ let intern_constr_pattern env sigma ?(as_type=false) ?(ltacvars=empty_ltac_sign) ~pattern_mode:true ~ltacvars env sigma c in pattern_of_glob_constr c +let interp_constr_pattern env sigma ?(expected_type=WithoutTypeConstraint) c = + let kind_for_intern = match expected_type with OfType _ -> WithoutTypeConstraint | _ -> expected_type in + let c = intern_gen kind_for_intern ~pattern_mode:true env sigma c in + let flags = { Pretyping.no_classes_no_fail_inference_flags with expand_evars = false } in + let sigma, c = understand_tcc ~flags env sigma ~expected_type c in + (* FIXME: it is necessary to be unsafe here because of the way we handle + evars in the pretyper. Sometimes they get solved eagerly. *) + pattern_of_constr env sigma (EConstr.Unsafe.to_constr c) + let intern_core kind env sigma ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign) { Genintern.intern_ids = ids; Genintern.notation_variable_status = vl } c = let tmp_scope = scope_of_type_kind env sigma kind in diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 898a3e09c8..11d756803f 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -136,10 +136,16 @@ val interp_type_evars_impls : ?flags:inference_flags -> env -> evar_map -> (** Interprets constr patterns *) +(** Without typing *) val intern_constr_pattern : env -> evar_map -> ?as_type:bool -> ?ltacvars:ltac_sign -> constr_pattern_expr -> patvar list * constr_pattern +(** With typing *) +val interp_constr_pattern : + env -> evar_map -> ?expected_type:typing_constraint -> + constr_pattern_expr -> constr_pattern + (** Raise Not_found if syndef not bound to a name and error if unexisting ref *) val intern_reference : qualid -> GlobRef.t -- cgit v1.2.3 From 2355b3ed9a9af853b67f406d61404c4c05f8c8e5 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 22 Oct 2020 19:41:47 +0200 Subject: Typing patterns and using type constraints in Search. We accept patterns that we failed to type as a fallback. --- interp/constrintern.ml | 3 +-- test-suite/output/Search.out | 4 ++++ test-suite/output/Search.v | 7 +++++++ test-suite/output/bug_13244.out | 9 +++++++++ test-suite/output/bug_13244.v | 3 +++ vernac/comSearch.ml | 11 ++++++++++- 6 files changed, 34 insertions(+), 3 deletions(-) create mode 100644 test-suite/output/bug_13244.out create mode 100644 test-suite/output/bug_13244.v diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 7dbc6c86a6..efab586f8a 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -2472,8 +2472,7 @@ let intern_constr_pattern env sigma ?(as_type=false) ?(ltacvars=empty_ltac_sign) pattern_of_glob_constr c let interp_constr_pattern env sigma ?(expected_type=WithoutTypeConstraint) c = - let kind_for_intern = match expected_type with OfType _ -> WithoutTypeConstraint | _ -> expected_type in - let c = intern_gen kind_for_intern ~pattern_mode:true env sigma c in + let c = intern_gen expected_type ~pattern_mode:true env sigma c in let flags = { Pretyping.no_classes_no_fail_inference_flags with expand_evars = false } in let sigma, c = understand_tcc ~flags env sigma ~expected_type c in (* FIXME: it is necessary to be unsafe here because of the way we handle diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out index 09feca71e7..503cfa2732 100644 --- a/test-suite/output/Search.out +++ b/test-suite/output/Search.out @@ -458,3 +458,7 @@ reflexive_eq_dom_reflexive: B.b: B.a A.b: A.a F.L: F.P 0 +inr: forall {A B : Type}, B -> A + B +inl: forall {A B : Type}, A -> A + B +(use "About" for full details on the implicit arguments of inl and inr) +f: None = 0 diff --git a/test-suite/output/Search.v b/test-suite/output/Search.v index a5ac2cb511..2f29e1aff1 100644 --- a/test-suite/output/Search.v +++ b/test-suite/output/Search.v @@ -89,3 +89,10 @@ Module Bug12647. Search F.P. End Bar. End Bug12647. + +Module WithCoercions. + Search headconcl:(_ + _) inside Datatypes. + Coercion Some_nat := @Some nat. + Axiom f : None = 0. + Search (None = 0). +End WithCoercions. diff --git a/test-suite/output/bug_13244.out b/test-suite/output/bug_13244.out new file mode 100644 index 0000000000..8c7d4ac776 --- /dev/null +++ b/test-suite/output/bug_13244.out @@ -0,0 +1,9 @@ +negbT: forall [b : bool], b = false -> ~~ b +contra_notN: forall [P : Prop] [b : bool], (b -> P) -> ~ P -> ~~ b +contraPN: forall [P : Prop] [b : bool], (b -> ~ P) -> P -> ~~ b +contraNN: forall [c b : bool], (c -> b) -> ~~ b -> ~~ c +contraL: forall [c b : bool], (c -> ~~ b) -> b -> ~~ c +contraTN: forall [c b : bool], (c -> ~~ b) -> b -> ~~ c +contra: forall [c b : bool], (c -> b) -> ~~ b -> ~~ c +introN: forall [P : Prop] [b : bool], reflect P b -> ~ P -> ~~ b +contraFN: forall [c b : bool], (c -> b) -> b = false -> ~~ c diff --git a/test-suite/output/bug_13244.v b/test-suite/output/bug_13244.v new file mode 100644 index 0000000000..83eaac1a35 --- /dev/null +++ b/test-suite/output/bug_13244.v @@ -0,0 +1,3 @@ +Require Import ssr.ssrbool. +Set Warnings "-ssr-search-moved". +Search headconcl:(~~ _). diff --git a/vernac/comSearch.ml b/vernac/comSearch.ml index 9de8d6fbc3..f3b21eb813 100644 --- a/vernac/comSearch.ml +++ b/vernac/comSearch.ml @@ -53,7 +53,16 @@ let kind_searcher = Decls.(function let interp_search_item env sigma = function | SearchSubPattern ((where,head),pat) -> - let _,pat = Constrintern.intern_constr_pattern env sigma pat in + let expected_type = Pretyping.(if head then IsType else WithoutTypeConstraint) in + let pat = + try Constrintern.interp_constr_pattern env sigma ~expected_type pat + with e when CErrors.noncritical e -> + (* We cannot ensure (yet?) that a typable pattern will + actually be typed, consider e.g. (forall A, A -> A /\ A) + which fails, not seeing that A can be Prop; so we use an + untyped pattern as a fallback (i.e w/o no insertion of + coercions, no compilation of pattern-matching) *) + snd (Constrintern.intern_constr_pattern env sigma ~as_type:head pat) in GlobSearchSubPattern (where,head,pat) | SearchString ((Anywhere,false),s,None) when Id.is_valid s -> GlobSearchString s -- cgit v1.2.3 From 3515988d1b9f792bf6f4e921f4776c5fe574b3ed Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 22 Oct 2020 20:18:03 +0200 Subject: Adding change log for #13255. --- .../13255-master+fix13244-use-coercions-in-search.rst | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 doc/changelog/07-commands-and-options/13255-master+fix13244-use-coercions-in-search.rst diff --git a/doc/changelog/07-commands-and-options/13255-master+fix13244-use-coercions-in-search.rst b/doc/changelog/07-commands-and-options/13255-master+fix13244-use-coercions-in-search.rst new file mode 100644 index 0000000000..03be92f897 --- /dev/null +++ b/doc/changelog/07-commands-and-options/13255-master+fix13244-use-coercions-in-search.rst @@ -0,0 +1,7 @@ +- **Added:** + Added support for automatic insertion of coercions in :cmd:`Search` + patterns. Additionally, head patterns are now automatically + interpreted as types + (`#13255 `_, + fixes `#13244 `_, + by Hugo Herbelin). -- cgit v1.2.3