Support members for the new newtypes #5311
Conversation
# Conflicts: # Source/DafnyCore/Resolver/CheckTypeCharacteristics_Visitor.cs # Source/DafnyCore/Rewriters/RefinementErrors.cs # Source/DafnyCore/Rewriters/RefinementTransformer.cs # docs/HowToFAQ/Errors-Refinement.md
| } | ||
| } | ||
| } | ||
| if (prevErrorCount == reporter.Count(ErrorLevel.Error)) { |
There was a problem hiding this comment.
This If statement has not been moved, just deleted. Could you please confirm why?
There was a problem hiding this comment.
Thanks for noticing. Yes, this is as intended. The RegisterInheritedMembers and InheritedTraitMembers methods had been responsible for bringing in the members from a type's trait parents. With the more general newtypes, a newtype can now inherit members also from its base type. However, the base type is, in general, not known this early in the resolution pipeline. Therefore, the functionality of RegisterInheritedMembers and InheritedTraitMembers was moved into "pass 0" of the resolver.
| @@ -1,4 +1,4 @@ | |||
| git-issue-2303.dfy(5,10): Error: newtype's base type is not fully determined; add an explicit type for bound variable 'x' | |||
| git-issue-2303.dfy(5,10): Error: base type of newtype 'int0' is not fully determined; add an explicit type for bound variable 'x' | |||
There was a problem hiding this comment.
Good job making the message a bit more explicit
| type seq<+T> { } | ||
|
|
||
| type multiset<+T> { } | ||
|
|
||
| type map<+T, +U> { | ||
| var Keys: set<T> // immutable |
There was a problem hiding this comment.
Immutable with var? Shouldn't it be const?
There was a problem hiding this comment.
Good call. I changed the printing code to output these SpecialFields as const.
Co-authored-by: Mikaël Mayer <[email protected]>
Co-authored-by: Mikaël Mayer <[email protected]>
No new cases needed to be checked. Unlike members inherited from a parent trait, the members that are inherited from the base type already have a body and cannot be overridden. |
This PR adds support for members of the recently expanded newtypes. In particular, inheritance of user-defined members and built-in members (such as
.RotateLeftfor bitvector types) are handled. Under--general-trait=full, inheritance from bothnewtypebase types and parent traits are handled.A
newtype's inherited members can only be figured out once thenewtype's base type is known. Since the base type is in general inferred, this means that member registration cannot happen until resolution has started. So, this PR moves that process fromRegister...toResolve....As part of this PR, other built-in types (
char,set, ...) were added to thevaluetypeDeclsarray. This has an effect on the--rprintoutput.The PR also improves some error messages (e.g., making them more consistent by using the format
type 'T') and removes some unused code that was left in abandoned#if ...directives during the resolver refresh.By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.