Skip to content
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

Support members for the new newtypes #5311

Merged
merged 62 commits into from
Apr 16, 2024
Merged
Changes from 1 commit
Commits
Show all changes
62 commits
Select commit Hold shift + click to select a range
60b5d0d
chore: Remove unused method
RustanLeino Mar 4, 2024
be3e917
Improve lookup of refined declarations
RustanLeino Mar 4, 2024
dc4af00
Make CheckCharacteristics available outside of class
RustanLeino Mar 5, 2024
433f654
Use local variable for refinedModuleTopLevelDecls, after all
RustanLeino Mar 5, 2024
0c18f5a
Add uniform checking of type characteristics in refinement modules
RustanLeino Mar 5, 2024
42d25fa
Add release notes
RustanLeino Mar 5, 2024
3fd27a0
Remove comment that made more sense in bug report
RustanLeino Mar 11, 2024
e572224
Improve error messages
RustanLeino Mar 11, 2024
9b8b0f4
Fix whitespace
RustanLeino Mar 11, 2024
8e56b6e
Merge branch 'master' into issue-2064
RustanLeino Mar 11, 2024
fa04f0b
Implement newtype-(i)map
RustanLeino Mar 12, 2024
4658600
Add release notes
RustanLeino Mar 12, 2024
2929542
Merge branch 'master' into newtype-map
RustanLeino Mar 12, 2024
5313370
Update FAQ error documentation
RustanLeino Mar 12, 2024
f2d2bce
Include Refinement Errors in the HowToFAQ documentation
RustanLeino Mar 12, 2024
0a4fdfc
Merge branch 'master' into newtype-map
RustanLeino Mar 12, 2024
238362d
Merge branch 'master' into newtype-map
RustanLeino Mar 19, 2024
b9647e0
Continue trying bounds after applying defaults
RustanLeino Mar 19, 2024
156fb0a
Merge branch 'master' into newtype-map
RustanLeino Mar 20, 2024
b7d9950
Merge branch 'master' into newtype-map
RustanLeino Mar 27, 2024
6206c5e
Add various .html files to ignore file
RustanLeino Mar 28, 2024
aba618b
Add type advice to RHS of map-domain subtraction
RustanLeino Mar 28, 2024
fc49e91
Merge branch 'master' into newtype-map
RustanLeino Mar 28, 2024
c396b5c
Merge branch 'master' into newtype-map
RustanLeino Mar 28, 2024
0f518c2
Merge branch 'master' into newtype-map
RustanLeino Mar 29, 2024
d70baf6
Fix typo in comment
RustanLeino Apr 2, 2024
8f1e145
chore: Improve code with newer C# construct
RustanLeino Apr 2, 2024
ce5d044
Add members WhatKindAndName to simplify printing
RustanLeino Apr 2, 2024
7f7d9a4
Add parent information also from newtype base types
RustanLeino Apr 2, 2024
fbc6e9d
Add remaining collection types, so that type parameters are defined
RustanLeino Apr 2, 2024
472fb66
Merge branch 'master' into newtype-members
RustanLeino Apr 3, 2024
6aa5825
Account for added ValuetypeDecl’s in resolved-print output
RustanLeino Apr 4, 2024
6a4424f
Use _bv “type family” only in legacy resolver
RustanLeino Apr 6, 2024
3eef290
chore: Improve C#
RustanLeino Apr 6, 2024
58bdaa9
chore: Improve formatting and comments
RustanLeino Apr 6, 2024
3b5c9c9
chore: Clean up comment
RustanLeino Apr 7, 2024
f544ac7
Improve error messages
RustanLeino Apr 7, 2024
eabc2d0
Add “char” to the valuetypeDecl list
RustanLeino Apr 7, 2024
f693f8f
Improve error messages
RustanLeino Apr 7, 2024
008e94c
Add tests for general-newtype + full-traits
RustanLeino Apr 7, 2024
9f37513
Update test files
RustanLeino Apr 7, 2024
26ea24a
Move InheritMembers machinery from registration to resolution
RustanLeino Apr 7, 2024
29c4d75
Remove old, unused code
RustanLeino Apr 8, 2024
66f67cd
Clarify behavior of traits extending traits
RustanLeino Apr 9, 2024
fbd9a40
Add tests
RustanLeino Apr 9, 2024
82e3007
Add tests
RustanLeino Apr 9, 2024
7b4619e
Add tests for compilation
RustanLeino Apr 9, 2024
8be947a
Support general newtype conversions in Go
RustanLeino Apr 9, 2024
56a4657
Merge branch 'master' into newtype-members
RustanLeino Apr 9, 2024
204b4e2
Merge branch 'master' into newtype-members
RustanLeino Apr 9, 2024
faae090
Fix Go coersions for newtypes
RustanLeino Apr 9, 2024
0597f77
Remove extraneous line in test file
RustanLeino Apr 9, 2024
89f8704
Merge branch 'master' into newtype-members
RustanLeino Apr 9, 2024
57c047a
Fix whitespace
RustanLeino Apr 9, 2024
557415e
Update Source/DafnyCore/Resolver/ModuleResolver.cs
RustanLeino Apr 16, 2024
2823169
Update Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs
RustanLeino Apr 16, 2024
64e48ae
Regress assignment syntax from good-ol’ Dafny to C# :)
RustanLeino Apr 16, 2024
290606a
Print immutable special fields as “const”
RustanLeino Apr 16, 2024
431d51a
Merge branch 'master' into newtype-members
RustanLeino Apr 16, 2024
43cf2d7
Adjust expect file to new error order
RustanLeino Apr 16, 2024
809f708
Update generated code (order of declarations)
RustanLeino Apr 16, 2024
9d1a09e
Merge branch 'master' into newtype-members
RustanLeino Apr 16, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Make CheckCharacteristics available outside of class
  • Loading branch information
RustanLeino committed Mar 5, 2024
commit dc4af00a0ff87dde6a6b7258c5a889de648a081d
4 changes: 2 additions & 2 deletions Source/DafnyCore/Resolver/CheckTypeCharacteristics_Visitor.cs
Original file line number Diff line number Diff line change
Expand Up @@ -342,7 +342,7 @@ void CheckTypeInstantiation(IToken tok, string what, string className, List<Type
}
}

bool CheckCharacteristics(TypeParameter.TypeParameterCharacteristics formal, Type actual, bool inGhostContext, out string whatIsWrong, out string hint) {
public static bool CheckCharacteristics(TypeParameter.TypeParameterCharacteristics formal, Type actual, bool inGhostContext, out string whatIsWrong, out string hint) {
Contract.Ensures(Contract.Result<bool>() || (Contract.ValueAtReturn(out whatIsWrong) != null && Contract.ValueAtReturn(out hint) != null));
if (!inGhostContext && formal.EqualitySupport != TypeParameter.EqualitySupportValue.Unspecified && !actual.SupportsEquality) {
whatIsWrong = "equality";
Expand Down Expand Up @@ -374,7 +374,7 @@ bool CheckCharacteristics(TypeParameter.TypeParameterCharacteristics formal, Typ
return true;
}

string TypeEqualityErrorMessageHint(Type argType) {
static string TypeEqualityErrorMessageHint(Type argType) {
Contract.Requires(argType != null);
var cl = (argType.Normalize() as UserDefinedType)?.ResolvedClass;
var tp = (TopLevelDecl)(cl as TypeParameter) ?? cl as AbstractTypeDecl;
Expand Down