Stream: Coq devs & plugin devs

Topic: bugs in `match`

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

https://github.com/coq/coq/blob/e64a92e6c5b74ca5631f2bbddcad1172f7325446/plugins/ltac/tactic_matching.ml#L236-L262

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: Dec 06 2023 at 15:01 UTC