Type test for char

[RustanLeino]

Summary

For an integer u, the expression u is char is currently not supported.

Many variations of of types are supported for is, but testing whether an int is a char is currently missing.

Background and Motivation

Stating u is char as an integer range is awkward and error prone.

Also, for code that is migrating from before-Unicode support to full Unicode support, it would be nicer to have an expression that takes on different meanings depending on what Unicode mode Dafny is invoked in.

Proposed Feature

With --unicode-char:false, u is char (where u has type int`) should be equivalent to

0 <= u < 0x1_0000

With --unicode-char:true, u is char (where u has type int`) should be equivalent to

0 <= u < 0xD800 || 0xE000 <= u < 0x10_0000

Alternatives

No response

[robin-aws]

I'm not sure I love this idea, as much as I agree with the motivation. Currently is will allow the RHS to be a subset type but not a newtype, so something similar like x is uint8 is rejected (type test for type 'uint8' must be from an expression assignable to it (got 'int')).

I usually think of is as a test of "is this value already in fact of this type", which lines up well with the semantics of subset types w.r.t. their base types, and classes w.r.t. their traits, for example. char behaves like a newtype rather than a subset type, so I feel like using is to mean "is convertable to" would be inconsistent.

[mattmccutchen-amazon]

With --unicode-char:true, u is char (where u has type int`) should be equivalent to

0 <= u < 0xD800 || 0xE000 <= u < 0x10_0000

This should be:

0 <= u < 0xD800 || 0xE000 <= u <= 0x10_FFFF

Valid Unicode scalar values go up to 0x10FFFF. It looks like Dafny implements this correctly and only the comment above was wrong. Of course, the <= 0x10_FFFF can be replaced with < 0x11_0000 at the taste of the user. I personally find it easier to remember that 0x10FFFF is the largest valid value.