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.

Sign up for GitHub

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

Jump to bottom

fix: Compilation of subset types constrained by type parameter #3893

Merged
merged 15 commits into from
May 4, 2023
Merged

fix: Compilation of subset types constrained by type parameter #3893

Changes from 1 commit
Commits
Show all changes
15 commits
Select commit Hold shift + click to select a range
162a95e
Add test cases
RustanLeino Apr 20, 2023
d2dca99
fix: Improve Subrange verification to reduce a completeness issue
RustanLeino Apr 20, 2023
1035bed
fix: Crash in resolver
RustanLeino Apr 20, 2023
4bd9803
fix: For Java
RustanLeino Apr 21, 2023
079dde2
fix: For C#
RustanLeino Apr 21, 2023
34a2db0
fix: For Go
RustanLeino Apr 21, 2023
59e1a32
fix: Add cast required by Java for functions
RustanLeino Apr 21, 2023
0b6ecd4
Add tests
RustanLeino Apr 21, 2023
8973cd7
Remove apparently unreachable code
RustanLeino Apr 21, 2023
f65ec61
Update tests
RustanLeino Apr 21, 2023
aa15dc9
Add release notes
RustanLeino Apr 21, 2023
2bd8e7e
Merge branch 'master' into issue-3883
RustanLeino Apr 21, 2023
dc7fb51
Update 3892-fix to cover additional bugs
RustanLeino Apr 22, 2023
539c006
Merge branch 'master' into issue-3883
RustanLeino Apr 26, 2023
d65ad03
Merge branch 'master' into issue-3883
RustanLeino May 4, 2023
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
fix: Add cast required by Java for functions 
Fixes #3892
  • Loading branch information
@RustanLeino
RustanLeino committed Apr 21, 2023
commit 59e1a3221cd650085da0f9ab778bc0e691a02041
6 changes: 5 additions & 1 deletion Source/DafnyCore/Compilers/Java/Compiler-java.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -999,7 +999,7 @@ protected class ClassWriter : IClassWriter {
// we're looking for).
var tp = targetTypeIgnoringConstraints.AsTypeParameter;
if (tp == null) {
typeDescriptorExpr = $"{DafnyTypeDescriptor}.referenceWithInitializer({StripTypeParameters(targetTypeName)}.class, () -> {d})";
typeDescriptorExpr = $"{DafnyTypeDescriptor}.referenceWithInitializer({StripTypeParameters(targetTypeName)}.class, () -> ({targetTypeName}){d})";
} else {
var td = FormatTypeDescriptorVariable(tp.GetCompileName(Options));
typeDescriptorExpr = $"{DafnyTypeDescriptor}.referenceWithInitializerAndTypeDescriptor({td}, () -> {d})";
Expand Down Expand Up @@ -3128,6 +3128,10 @@ protected class ClassWriter : IClassWriter {
return $"({BoxedTypeName(xType, wr, udt.tok)}) null";
}
} else if (cl is DatatypeDecl dt) {
if (DatatypeWrapperEraser.GetInnerTypeOfErasableDatatypeWrapper(Options, dt, out var innerType)) {
var typeSubstMap = TypeParameter.SubstitutionMap(dt.TypeArgs, udt.TypeArgs);
return TypeInitializationValue(innerType.Subst(typeSubstMap), wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors);
}
var s = FullTypeName(udt);
var typeargs = "";
var nonGhostTypeArgs = SelectNonGhost(cl, udt.TypeArgs);
Expand Down