-
Notifications
You must be signed in to change notification settings - Fork 261
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Fix: Ability to cast a datatype to its trait when overriding functions (
#4824) This PR fixes #4823 There were two issues there: - The function override check was casting to ClassLikeDecl, when it should now be TopLevelDeclWithMembers as IndDatatypeDecl can also override trait declarations. - The generated axiom used to rely on types being unboxed, but since now we might compare a trait with a datatype value, we need to ensure correct boxing for Boogie to type-check. I added the corresponding test. <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>
- Loading branch information
1 parent
5babf7c
commit 10b59f5
Showing
6 changed files
with
20 additions
and
4 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Binary file modified
BIN
-247 Bytes
(100%)
Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo
Binary file not shown.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
11 changes: 11 additions & 0 deletions
11
Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4823.dfy
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,11 @@ | ||
// RUN: %baredafny verify %args --type-system-refresh --general-traits=datatype "%s" > "%t" | ||
// RUN: %diff "%s.expect" "%t" | ||
|
||
trait Test<T> { | ||
function Cast(t: T): Test<T> | ||
} | ||
|
||
datatype Impl extends Test<Impl> = ImplConstructor() | ||
{ | ||
function Cast(t: Impl): Test<Impl> { t } | ||
} |
2 changes: 2 additions & 0 deletions
2
Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4823.dfy.expect
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,2 @@ | ||
|
||
Dafny program verifier finished with 1 verified, 0 errors |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
Ability to cast a datatype to its trait when overriding functions |