`_` as a valid pattern

45 views
Skip to first unread message

Guillaume Bury

unread,
Mar 25, 2021, 1:36:12 PM3/25/21
to SMT-LIB
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:

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

unread,
Mar 25, 2021, 3:16:17 PM3/25/21
to Guillaume Bury, smt...@googlegroups.com
Hi Guillaume,

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
> <mailto:simon.cru...@m4x.org>>, since this group does not appear
> --
> 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>.

OpenPGP_signature

Martin Nyx Brain

unread,
Mar 25, 2021, 3:16:23 PM3/25/21
to smt...@googlegroups.com, Simon Cruanes, Guillaume Bury
On Thu, 2021-03-25 at 10:36 -0700, Guillaume Bury wrote:
> 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:

<snip>

> 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.

AFAIK the vast majority of people who use this list are not using any
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

unread,
Mar 25, 2021, 3:37:51 PM3/25/21
to SMT-LIB
This is for Simon. I conform that you do not need a gmail account to subscribe to this group. I have just added you with your m4x.org account.

Cesare

Cesare Tinelli

unread,
Mar 25, 2021, 3:48:00 PM3/25/21
to SMT-LIB
The underscore character '_' is unfortunately reserved in SMT-LIB 2.6 for indexed symbols. The example in the reference document is incorrect and needs fixing. 

We do not currently have a wildcard symbol for the match statement although I am surprised this is an annoyance when match has an even more annoying limitation for not allowing nested patterns :) 

The good news is that the upcoming SMT-LIB 3 proposal (which will go out officially this summer) does away with the indexed symbols notation. This would free '_' and allow it to be used as a wildcard in patterns. Stay tuned.

Cesare 

On Thursday, March 25, 2021 at 12:36:12 PM UTC-5 Guillaume Bury wrote:

Simon Cruanes

unread,
Mar 25, 2021, 5:39:31 PM3/25/21
to smt...@googlegroups.com
> We do not currently have a wildcard symbol for the match statement although
> I am surprised this is an annoyance when match has an even more annoying
> limitation for not allowing nested patterns :)

The limitation of not accepting nested patterns is, imho, a reasonable
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
signature.asc

Cesare Tinelli

unread,
May 12, 2021, 5:27:41 PM5/12/21
to smt...@googlegroups.com

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

unread,
May 12, 2021, 6:52:53 PM5/12/21
to smt...@googlegroups.com
Hi Cesare,

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
> `otherwise` or `default`?

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).

I'd argue, for v3 anyway, that `_` should also be allowed as an
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
signature.asc

Cesare Tinelli

unread,
May 17, 2021, 8:06:01 PM5/17/21
to smt...@googlegroups.com

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.

Simon Cruanes

unread,
May 18, 2021, 12:02:58 PM5/18/21
to smt...@googlegroups.com
Hi Cesare,

> I also agree that it would be useful to have a designated symbol,
> ideally `_`, for the "whatever" match inside a constructor pattern.

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
> 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?

I think that sounds very good, both enabling it for SMTLIB v3 and the
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
> (`default`, `otherwise`, ...)

💯. Likewise.

Cheers,

--
Simon Cruanes
signature.asc
Reply all
Reply to author
Forward
0 new messages