-
Notifications
You must be signed in to change notification settings - Fork 260
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Include subtypes in case patterns #1715
Comments
Lovely! But surprising for subset types, at least until #1680 is solved: what's the desugared version of |
There is currently no surface syntax like |
It would be nice to additionally expose this capability to the programmer in a more generic way by allowing a guard in a |
I agree that this would be a very useful extension to Dafny. Similarly to @fabiomadge I was wondering whether implementing this would allow us to relatively easily add support for guards in case expressions. Given that the proposal can report redundant checks, I assume that it would also report errors on non-exhaustive pattern matches, is that correct? E.g. if I write
would it report that And, similarly, if I have the following assertion:
would it then accept the pattern match and not report the above case as missing?
Did this intend to say "not always possible at compile time"?
This was probably meant for explanation purposes, to contrast the proposal with the current semantics, but I believe that Dafny wouldn't allow me to pattern match on two case patterns that differ only in the type ascriptions, because it currently doesn't them as type checks. |
I keep this in mind while working on #1604 |
Dafny insists that the given The "redundant case" message is just a warning. It works accurately today, because we can syntactically distinguish the cases. Under the proposed extension, it becomes more difficult to determine if a case a redundant, since case selection can depend on the types of values. Hence, I suggested that Dafny will use the declared base-type hierarchy of subset types (rather than the constraints given in subset-type declarations) to determine whether or not to give a "redundant case" warning (see the If we take yet another step and let the |
There are type tests that cannot be performed at run time (and hence the compiler cannot emit code for doing it). For example, consider datatype Flavor = Strawberry | Licorice | Vanilla
datatype IceCream = IceCream(flavor: Flavor, ghost popular: bool)
type PopularIceCream = c: IceCream | c.popular witness *
method Example(c: IceCream) {
if c is PopularIceCream { // cannot be tested at run time
}
} It is not possible to test |
(There was a typo in my example, where I had written The |
An alternative to this approach is to some form of path-sensitive typing. We already have something like this in Dafny with |
Dafny does have the effect of path-sensitive typing, like in the example you gave. But it's not the type system that does this. Instead, the type is usually the base type (like method M(b: bool, x: T?)
requires b ==> x != null
{
if b {
// here, you can use x as if it had the non-null type T
}
} Note that |
I'm actually quite concerned that interpreting I think I prefer the alternative of only supporting guard expressions instead, for clarify and consistency. Something like:
Exhaustiveness just implies another proof obligation. If the desugared guards on a match statement/expression (assuming we can express a pattern like |
I'm curious what kind of cases you have in mind, could you give an example of other Dafny features/patterns that would have a different flavour? If the verifier provides exhaustiveness errors and redundant-case warnings, would the users not immediately understand what's going on? |
But the proposal is to interpret it as a type constraint: the branch is only taken if the constraint is satisfied. No? Using Besides the syntax is going to be pretty heavy:
|
I meant a "constraint" as in type checking - pretend I said "assertion" instead :) |
This PR makes various changes and improvements to resolution. The need for these changes was driven by the upcoming new type inference. The PR also fixes several issues related to the desugaring of `match` constructs. Fixes #3908 Fixes #3915 Fixes #3918 Fixes #3921 Fixes #3922 Fixes #3923 Changes related to `match`: * Eliminate `ReplaceTypesWithBoundVariables`. This troublesome method was changing the AST before desugarings were taking place. This made the up-and-coming pre-type inference more difficult. And as I was fixing these other bugs related to `match`, I found that I repeatedly had to counteract what `ReplaceTypesWithBoundVariables` had done. This because increasingly more complicated, so I decided to address the real problem and remove `ReplaceTypesWithBoundVariables`. Amazingly, doing so cause almost no problems by itself. My conclusion is that this method was here only for historical purposes, no longer for anything useful. * Print attributes and types of case patterns * **fix:** Fix issues with temporary variables introduced during resolution of case patterns (#3908) * Introduce `VisitExtendedPattern` method * Visit patterns during visitation of `NestedMatchStmt` * Include literal expressions in the `.SubExpressions` of cases * Don't generate (unused) local/bound variable for literal patterns * Memoize value computed by `OptimisticallyDesugaredLit` * Print the RHS literal of symbolic literals in case patterns * **fix:** Mark ghost status of case variables correctly (#3918) * **fix:** (**breaking change**) Don't allow downcasts from traits in case patterns (#3922). These cases previously caused the C# and Java compiler to emit malformed code. Rather than changing those compilers, I took the opportunity to disallow such downcasts during resolution. In the future, we plan to introduce some kind of type-case statement, which is a better solution for these things, anyway (see also #1715). But, technically, this is a breaking change for anyone who was using the old behavior with the JavaScript, Go, or Python compilers. * **fix:** Fix crash that occurred due to malformed desugaring when encountering `_: int` in pattern (#3923) Other changes: * Make working method `CreateResolvedCall` more general to support parameters and type parameters * Include `ObjectToDiscard` in the `.SubExpressions` of `StaticReceiverExpr` * Generate proper scaffolding around `MemberSelectExpr` and `FunctionCallExpr` when desugaring iterators * Refactor some code in the resolution of `AssignOrReturnStmt` to make routines reusable by pre-resolution * Move the computation of loop-body surrogate away from the early name-resolution/type-inference pass. (A consequence of this is that the warning messages for body-less loops appear in a later phase of resolution than before.) * (**breaking change**) Move assumption-variable checks away from the early name-resolution/type-inference pass. A breaking-change consequence of this is that type-less assumption variables are no longer inferred to have type `bool`. (This breaking change is justified as follows: Assumption variables are rarely, if ever, used. The inference that was removed only affects assumptions variables that weren't used for anything, because any other proper use would cause them to be inferred to be of type `bool`. The breaking-change fix is, at worst, to manually add the type `: bool` to the declaration of each assumption variable.) * Make introduction of members of built-in types (like `.Floor` and `.IsLimit`) more uniform * **fix:** Fix `:autoReq` to include type parameters of function calls * **fix:** Re-include the `examples/induction-principle-code/` tests, which had been "temporarily" excluded for a while. (A recent restriction that affects those test cases is fixed in this PR.) * (**breaking change**) Use of `this` when dereferencing static members is now disallowed in the first phase of object constructors. This makes the treatment of `this` in that first phase more uniform. * Change a couple of test cases to no longer rely on cast-free conversions from a trait to a class. This is in preparation for the new type inference, which will insist on having such casts explicitly. * Fix: Perform size checks of bitvector literals in case patterns (#3915). (At some point in the past, the `git-issue-889b.expect` file of these tests had been changed, which caused the introduction of this bug to go unnoticed sooner.) * **fix:** Check for underspecified type arguments of subset types (#3921) <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small> --------- Co-authored-by: Remy Willems <[email protected]>
This is a proposal to extend how Dafny handles explicitly typed bound variables in case patterns. In particular, the proposal is to make such types part of the pattern, rather than being an assertion about what holds about such a pattern. In other words, the proposal is to change the meaning of
x: X
in a case pattern from a type assertion (assert ... x is X
) to a type test (if ... x is X
).Background
Case patterns can introduce bound variables. Most often, these variables are just named and their types are inferred. For example, given the usual
and given
xs: List<int>
, the statementinfers
x
to have typeint
andrest
to have typeList<int>
.The bound variables are allowed to be given a type explicitly. For example,
x
can be declared explicitly to have typeint
as follows:The semantics of giving such a type explicitly is that the program text asserts that any value that fits in the structural pattern given has the indicated type. For example,
is saying that if
xs
has the formCons(_, _)
, thenxs.head
is anat
. If thismatch
statement is executed withxs
beingCons(2, Cons(-3, Nil))
, then it will bindx
as2
. As another example, the program is in error if thismatch
is reached withxs
beingCons(-1, Nil)
(as usual, the verifier will generate proof obligations to show that a program does not exhibit such errors).Proposed new semantics
The proposal is to change the semantics of an explicitly given type to make the
case
apply only if the corresponding value has the given type. Under the proposed semantics, a case likecase Cons(x: nat, rest) =>
would be taken only ifxs
is of theCons
variant and the head of theCons
is anat
. For anxs
value likeCons(-1, Nil)
, thecase
would not be taken; instead, the nextcase
in order will be considered (and, in the usual manner, the program is in error if nocase
applies).Use case
Under the proposed semantics, one can write the following:
Another use case
As another use case, consider the following types:
and suppose
trs
has typeList<Tr>
. Then, the followingmatch
statement gives separate cases for the head of the list being anA
or aB
:Under the proposed semantics, this
match
statement is semantically equivalent toIn contrast, under the current semantics, it is semantically equivalent to
where the second
trs.Cons?
case will never be taken.Some details
Type tests
The proposed semantics involves a type test, rather than a type assertion. Such a type test is not always possible at run time, because the test may involve a ghost expression (in the constraint of a subset type) or may involve non-injective type parameters of reference types. Dafny already restricts such run-time tests elsewhere (for example, in comprehensions where a type test is needed, and in
is
expressions for reference types). Thus, if thematch
occurs in a compiled context, then these same restrictions apply to explicitly typed bound variables.(The last case for a given structure does not require run-time type tests, since anything of that structure is verified to have that type. Nevertheless, I propose we don't treat this special case any differently.)
Redundant cases
The proposal affects the redundant-case checks. In particular, a warning about a redundant case should be generated only if there's a previous case whose types are supertypes. This should be done nominally (that is, without involving the verifier).
For example, given
and
xs: List<int>
, we haveAs another example, given
and again
xs: List<int>
, we haveThe text was updated successfully, but these errors were encountered: