`_` as a valid pattern
Guillaume Bury
Howdy y'all,
In https://github.com/CVC4/CVC4/issues/5128 it came to light that the smtlib v2.6 standard is slightly inconsistent when it comes to patterns in the `match` expression construct. The example uses `_` but it's a reserved identifier which cannot be used as a variable.
Personally, I think it's annoying that `match` does not have a catch-all/wildcard case. Many languages allow `_` as a special "ignore" pattern in destructuring or pattern matching. Using a dummy variable means you need to be careful to not capture it later, and it's also vulnerable to typos (if you type `Nil` instead of `nil`, for example, in a list
`nil|cons`, it silently matches anything).
I think it would be cleaner to allow `_` explicitely, adding a case for patterns: `cstor | (cstor args) | variable | _`.
Best,
PS: I'm not writing this to google groups, I don't have nor want a
google account, which seems to be required to post there. Emails are simpler.
Aina Niemetz
this is not an answer to your question but regarding posting to this
group. Everybody can post to the group even without a Google account.
You just send an email to the group, and one of the moderators has to
give you the right to post, and that's it. You won't be able to post to
the group using the web interface, but that's it.
Cheers,
Aina
On 3/25/21 10:36 AM, Guillaume Bury wrote:
> Posting on behalf of Simon Cruanes <simon.cru...@m4x.org
> You received this message because you are subscribed to the Google
> Groups "SMT-LIB" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to smt-lib+u...@googlegroups.com
> <mailto:smt-lib+u...@googlegroups.com>.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/smt-lib/deee654b-ec3b-41f4-bdb1-0205ab1b73f7n%40googlegroups.com
> <https://groups.google.com/d/msgid/smt-lib/deee654b-ec3b-41f4-bdb1-0205ab1b73f7n%40googlegroups.com?utm_medium=email&utm_source=footer>.
Martin Nyx Brain
> Posting on behalf of Simon Cruanes <simon.cru...@m4x.org>,
> since this
> group does not appear to be accessible for those who don't have (or
> want to
> have/use) a google account:
> PS: I'm not writing this to google groups, I don't have nor want a
> google account, which seems to be required to post there. Emails are
> simpler.
kind of google account and are using e-mail. If there is not an easy
way of signing up and e-mail address and using it without the
permission of the Googly Overlords then that is A Problem and we should
move the list.
Cheers,
- Martin
Cesare Tinelli
Cesare Tinelli
Simon Cruanes
> I am surprised this is an annoyance when match has an even more annoying
> limitation for not allowing nested patterns :)
one. It makes solvers easier to implement and gives a very clear
semantics to `match` (compiling nested patterns requires heuristics
to pick what to destruct first, etc. so better let frontends handle it).
On the other hand, a default case is necessary to keep match expressions small.
Would a keyword (like `else` or `otherwise` or `default`) be a suitable
alternative?
Cheers,
--
Simon Cruanes
Cesare Tinelli
Hi Simon,
On the other hand, a default case is necessary to keep match expressions small.
Would a keyword (like `else` or `otherwise` or `default`) be a suitable
alternative?
An alternative to what, though? What's the problem with just using a variable a pattern for the last case? Isn't that even more compact than otherwise or default? Or is the problem the burden of choosing the right name for the variable to avoid name clashes? (You have the same problem for any variable in a pattern anyway).
Could you clarify?
Thanks,
Cesare
--
You received this message because you are subscribed to a topic in the Google Groups "SMT-LIB" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/smt-lib/ohNBx84mq9s/unsubscribe.
To unsubscribe from this group and all its topics, send an email to smt-lib+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/YFzrx%2BDxTs%2BoD/NV%40church.
Simon Cruanes
a variable is not a good alternative to a default case, imho.
> An alternative to what, though? What's the problem with just using a
> variable a pattern for the last case? Isn't that even more compact than
Not having either means you duplicate some big terms, but here the
difference is just a few characters (so it's not worse than verbose
keywords). The main issue, to me, between variables and "default"
is not compactness but robustness. A mere typo and a constant
constructor (one with no argument) might be turned into a variable
pattern; there is also, as you point out, the risk of capture.
On the other hand, why is it useful to be able to use a variable as a
pattern? That seems rarely useful and it is redundant with `let`. I know
it's available in more expressive languages (like OCaml) but these would
typically compile down to SMT and could introduce a let for this kind of
patterns.
> Or is the problem the burden of choosing the right
> name for the variable to avoid name clashes? (You have the same problem for
> any variable in a pattern anyway).
immediate argument to a constructor in a pattern, for this exact reason,
as the trivial pattern that ignores what it's matched against.
Cheers,
--
Simon Cruanes
Cesare Tinelli
Hi Simon,
Thanks for the clarification. I see now that your are not actually just proposing to introduce a keyword for the catch-all case; you are proposing the elimination of variables altogether as individual patterns. It is the latter that would make the match construct more robust.
I think you make a very good point. I also agree that it would be useful to have a designated symbol, ideally _, for the "whatever" match inside a constructor pattern.
Since this change would not be backward compatible and we are close to releasing a first proposal for Version 3 of the language, I would be inclined to introduce the change in full in that version (especially the restriction on the patterns and the use of _).
As an intermediate step, we could for now add a default keyword for the catchall case and deprecate (but not disallow yet) the use of variables as a pattern.
How does that sound?
It'd be good to hear from others as well, especially on whether introducing a new keyword in Version 2.6 is worth the trouble and also on how to name it (default, otherwise, ...)
Best,
Cesare
--
You received this message because you are subscribed to a topic in the Google Groups "SMT-LIB" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/smt-lib/ohNBx84mq9s/unsubscribe.
To unsubscribe from this group and all its topics, send an email to smt-lib+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/YJxTPj%2BY18NdZeGf%40church.
Simon Cruanes
> I also agree that it would be useful to have a designated symbol,
Yes, to summarize, I think match arms would be one of:
- `(<symbol> <expr>)` for constant patterns
- `((<symbol> <var-or-wildcard>+) <expr>)` where <var-or-wildcard> is either a
symbol (a variable) or `_` (a wildcard, discarding the matchee's
value)
- `(:default <expr>)` or something like that for the default case, which
is optional when all constructors have been covered by previous
patterns.
(deprecated:)
- `(<symbol> <expr>)` for variable patterns, when `<symbol>` is not a
known constructor.
I think dolmen could flag the later with a warning to help migrate
benchmarks that make use of it.
> Since this change would not be backward compatible and we are close to
> releasing a first proposal for Version 3 of the language, I would be
> inclined to introduce the change in full in that version (especially the
> As an intermediate step, we could for now add a `default` keyword for the
> catchall case and deprecate (but not disallow yet) the use of variables as a
> pattern.
>
> How does that sound?
deprecation of `default` (at least for constructors as it would be
entirely incompatible).
> It'd be good to hear from others as well, especially on whether introducing
> a new keyword in Version 2.6 is worth the trouble and also on how to name it
💯. Likewise.
Cheers,
--
Simon Cruanes