Jason Gross (Jan 26 2022 at 19:19): Jason Gross (Jan 26 2022 at 19:19):Is there a complete list of terms x such that match x with _ => idtac end succeeds but match x with x => idtac end fails? (I just discovered that any term containing unfolded primitive projections makes the cut, c.f. https://github.com/coq/coq/issues/15554)
Gaëtan Gilbert (Jan 26 2022 at 19:37):how would we know if a list of bugs is complete?
Jason Gross (Jan 26 2022 at 19:54):I guess that's a good point, and I should have instead asked "does anyone know any other such terms?"
Ali Caglayan (Jan 26 2022 at 20:17):Well looking at the code, _ successes before x since it is obviously a wildcard. The later gets checked with
(** [pattern_match_term pat term lhs] returns the possible
matchings of [term] with the pattern [pat => lhs]. *)
let pattern_match_term pat term lhs =
match pat with
| Term p ->
begin
try
put_subst (Constr_matching.extended_matches E.env E.sigma p term) <*>
return lhs
with Constr_matching.PatternMatchingFailure -> fail
end
| Subterm (id_ctxt,p) ->
let rec map s (e, info) =
{ stream = fun k ctx -> match IStream.peek s with
| IStream.Nil -> Proofview.tclZERO ~info e
| IStream.Cons ({ Constr_matching.m_sub ; m_ctx }, s) ->
let subst = adjust m_sub in
let context = id_map_try_add id_ctxt m_ctx Id.Map.empty in
let terms = empty_term_subst in
let nctx = { subst ; context ; terms ; lhs = () } in
match merge ctx nctx with
| None -> (map s (e, info)).stream k ctx
| Some nctx -> Proofview.tclOR (k lhs nctx) (fun e -> (map s e).stream k ctx)
}
in
map (Constr_matching.match_subterm E.env E.sigma p term) imatching_error
Which is probably handling primitive records incorrectly.
Paolo Giarrusso (Jan 26 2022 at 20:44):@Jason Gross has anybody attempted to use something QuickCheck-like to test the relevant equality is reflexive?
Jason Gross (Jan 26 2022 at 20:45):@Paolo Giarrusso Not that I know of. Would it be hard to set up?
Paolo Giarrusso (Jan 26 2022 at 20:45):no idea, and I'm half-expecting there's too much mutable state in Coq terms for this
Pierre-Marie Pédrot (Jan 26 2022 at 21:10):can x be an Ltac-bound variable, or are you requiring it to be a copy-paste?
Pierre-Marie Pédrot (Jan 26 2022 at 21:11):with evars you can probably do weird things courtesy of pattern_of_constr
Jason Gross (Jan 26 2022 at 23:47):@Pierre-Marie Pédrot I'd be interested in Ltac-bound variables too. I thought that pattern_of_constr sometimes turned specific evars into general holes, but for this to happen you need to get more restrictive.
Last updated: May 31 2023 at 17:01 UTC