Add !is/!has syntax as shorthand for negated is/has

[matthias-brun]

Negation is annoying to use with the is syntax, since it requires wrapping in parentheses: !(x is Variant). This PR adds isnt syntax, which expands to !(x is Variant).

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[Chris-Hawblitzel]

I like the idea of having a more compact syntax for !(x is Variant), as this PR proposes. Dafny has something similar to this already, with its in and !in infix operators. Since we have is and has infix operators, I'd propose !is and !has to avoid introducing extra words and for consistency with ==/!=.

[matthias-brun]

Thanks for the suggestion, I like it! I'll change the syntax accordingly and add it for !has as well.

[jaybosamiya-ms]

Surely, for consistency with == => !=, we should be doing this⸮

[jaybosamiya-ms]

I do like the !is and !has infix operators, fwiw :)

[parno]

We'll need to update both verusfmt and verus-analyzer to recognize the new syntax.

[tjhance]

jay is objectively correct. !s and !as are the only sensible choices

[matthias-brun]

@Chris-Hawblitzel It looks like getting !is to parse right isn't quite as straightforward. I think you have a better understanding of syn, so maybe you can give me a pointer on what the best way to implement this is.

I tried the naive thing of just replacing the isnt token in my current code by !is but that fails as it seems to try and parse the ! as negation instead. The result is error: expected delimiter (with is underlined). The token stream has the two tokens ! and is rather than a single !is token. So I suppose the first question is: Am I interpreting correctly that making !is a token is the wrong approach? We don't seem to reject Verus keywords as identifiers (e.g. let is: nat = 1;) so unambiguous tokenization wouldn't be possible anymore.

[utaal]

There is some functionality to merge tokens to handle these cases - I can't look now but I should be able to take a look next week.

[Chris-Hawblitzel]

I would recommend parsing ! and is as two separate, consecutive tokens. For example, where the regular is is parsed with:

input.peek(Token![is])

the ! + is tokens could be parsed with something like:

input.peek(Token![!]) && input.peek2(Token![is])

This is a pretty common approach in syn.

[utaal]

I pushed a commit that treats !is as a single token (so it disallows ! is) and is consistent with how we handle other compound tokens. I needed to rename it internally to isnt, because proc_macro doesn't accept tokens that are a mix of a character and an identifier. @Chris-Hawblitzel does that make sense to you?

However, I think the main issue with !is is this case Matthias spotted:
https://github.com/verus-lang/verus/pull/1435/files#diff-38b1650a5373a031c934060b5a2588c88feb0c515b81307f121b982ea5bb02b8R1152-R1157

        proof fn let_with_is_ident() {
            let is = false;
            assert(!is);
        }

which now fails to parse (before and after my commit), and I think making it contextual would be a non-trivial endeavor. That said, we've already decided that is is a keyword (for the existing a is X syntax).

[utaal]

@Chris-Hawblitzel is looking into parsing !is contextually as two tokens (the same way we handle is).
@parno and @jaybosamiya-ms as additional reviewers because this changes syntax that needs to be reflected in verusfmt and VScode.

[parno]

I took a quick look at verus analyzer. It turns out that it currently only supports is but not has. Apparently the latter doesn't show up in vstd.

One existing annoyance is that due to the existing design of rust-analyzer's parser, back when I added support for is, I had to make is a first-class keyword to get it to parse correctly. That means you can't use is as a variable name, for instance. The only other Verus keywords that I have to do that for are "ghost", "tracked", "forall", "exists", and "matches". All of the others are conditional keywords, which means they're still valid for, e.g., identifiers.

For this PR in particular, it looks doable to support !is, I would just have to work around the fact that rust-analyzer currently appears to allow macro calls with a space between the macro name and the exclamation mark (i.e., print !("hello") is okay).

[jaybosamiya-ms]

Verusfmt now supports !is (I added it to its main branch a couple of weeks ago; I have triggered a new release, which should be live in a few minutes once CI is done verus-lang/verusfmt@214299b; EDIT: live on v0.5.3 onwards).

Regarding contextual vs not: I think having is as a non-contextual keyword is perfectly fine. I don't see anyone using is as the name of a variable or a struct field or such. There may be users who have a method named is (~a.is(b)), but I don't see that as being common with standard Rust conventions (eq or similar would be the conventional name instead). Also, if someone really needs to interface with external code with is used as an identifier, there is always the raw-identifier syntax r#is, so we are not even restricting interfacing with unchangeable external code). Generally speaking, I very much prefer non-contextual keywords, rather than contextual ones, since non-contextual keywords are easier to understand and deal with (e.g., writing a syntax highlighter is easier).

Re macro calls: I had to handle something similar for verusfmt too :) At least for versufmt it was easy to fix by making macro calls look-ahead for an opening brace/bracket/paren immediately after the ! and otherwise back out.

[parno]

Re macro calls: I had to handle something similar for verusfmt too :) At least for versufmt it was easy to fix by making macro calls look-ahead for an opening brace/bracket/paren immediately after the ! and otherwise back out.

Interesting. In rust-analyzer, it appears they have a look ahead for != and back out in that case, so I added another one for is, and that seems to work.

[parno]

FWIW, I have a branch of verus-analyzer where !is, and !has appear to be working.