Allow non-reference-type traits #4137
Merged
Conversation
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
fabiomadge
reviewed
Jun 6, 2023
| @@ -177,20 +177,29 @@ class PythonCompiler : SinglePassCompiler { | |||
| var relevantTypeParameters = typeParameters.Where(NeedsTypeDescriptor); | |||
| var args = relevantTypeParameters.Comma(tp => tp.GetCompileName(Options)); | |||
| if (!string.IsNullOrEmpty(args)) { args = $", {args}"; } | |||
| var isNewtypeWithTraits = cls is NewtypeDecl { ParentTraits: { Count: > 0 } }; | |||
There was a problem hiding this comment.
This is always false as of this PR.
There was a problem hiding this comment.
No, with /generalTraits:1, it can be true. Here's an example input:
newtype MyInt extends Trait = int
trait Trait { }
method Main() {
var m: MyInt := 12;
}But without the new type system (engaged with /typeSystemRefresh:1, but not fully supported in this PR), you can't really make use of the parent traits of the newtype.
There was a problem hiding this comment.
I'm fairly certain that this worked for me at the time, but doesn't seem to in this PR's current state.
# Conflicts: # Source/DafnyCore/Resolver/Resolver.cs # Source/DafnyCore/Resolver/TypeInferenceChecker.cs
fabiomadge
reviewed
Jun 8, 2023
# Conflicts: # Source/DafnyCore/AST/Cloner.cs # Source/DafnyCore/AST/Modules/ScopeCloner.cs # Source/DafnyCore/AST/TypeDeclarations/TupleTypeDecl.cs # Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs # Source/DafnyCore/Dafny.atg # Source/DafnyCore/Resolver/Resolver.cs # Source/DafnyCore/Verifier/Translator.ClassMembers.cs # Test/dafny0/DividedConstructors.dfy.expect # Test/dafny0/MiscTypeInferenceTests.dfy.expect
# Conflicts: # Source/DafnyCore/Verifier/Translator.cs
fabiomadge
previously approved these changes
Jul 1, 2023
| @@ -177,20 +177,29 @@ class PythonCompiler : SinglePassCompiler { | |||
| var relevantTypeParameters = typeParameters.Where(NeedsTypeDescriptor); | |||
| var args = relevantTypeParameters.Comma(tp => tp.GetCompileName(Options)); | |||
| if (!string.IsNullOrEmpty(args)) { args = $", {args}"; } | |||
| var isNewtypeWithTraits = cls is NewtypeDecl { ParentTraits: { Count: > 0 } }; | |||
There was a problem hiding this comment.
I'm fairly certain that this worked for me at the time, but doesn't seem to in this PR's current state.
Co-authored-by: Fabio Madge <[email protected]>
Co-authored-by: Fabio Madge <[email protected]>
Co-authored-by: Fabio Madge <[email protected]>
Co-authored-by: Fabio Madge <[email protected]>
Co-authored-by: Fabio Madge <[email protected]>
…esolutionAndTypeInference.cs Co-authored-by: Fabio Madge <[email protected]>
Co-authored-by: Fabio Madge <[email protected]>
…esolutionAndTypeInference.cs Co-authored-by: Fabio Madge <[email protected]>
fabiomadge
approved these changes
Jul 3, 2023
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR allows, under the new command-line switch
--general-traitsor/generalTraits, non-reference types (datatypes, abstract types, and newtypes) to extend traits.Under this option, which with time will become the default, a
traitdeclaration is either a reference type (if it transitively extendsobject, that is, ifobjectis among its parent-type ascendants) or not (ifobjectis not among its parent-type ascendants). A reference-type trait can be used as a parent only for other reference types (that is, other reference-type traits as well as class types). Only reference-type traits can have mutable-field members. Moreover, because only classes offer a way to initialize aconstfield if no RHS is given, a non-reference-type trait must give a RHS for every non-auto-initconstfield.The legacy type system (that is, the current type system) does not understand non-reference-type traits. Therefore, there's not much one can do with these new non-reference-type traits at this time. To make them usable requires
/typeSystemRefresh:1, once full support for it has been supplied in PRs and merged. For the same reason, the new tests included in this PR focus on making sure previous functionality still works, rather than testing that non-reference-type inheritance of traits are verified/compiled correctly.Without the new general traits, it is as if all
traitdeclarations includedextends object. Indeed, for any trait that needs that under/generalTraits:1, it is possible to declare them so already under/generalTraits:0. When running the test suite, I found that only fewtraitdeclarations depend on being reference types. Hence, even under/generalTraits:1, I expect that only fewtraitdeclarations need to be changed to sayextends object.Along the way, this PR fixes a previous bug:
Fixes #4046
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.