feat!: Support seq<trait> in C# #557

robin-aws · 2020-03-04T22:10:00Z

Addresses #406 for C# only.

See comments in Test/dafny0/RuntimeTypeTests0.dfy for details.

BREAKING CHANGE: Sequences are now represented by a Dafny.ISequence<T> interface, which will break external code.

robin-aws · 2020-03-04T22:20:58Z

AWS CodeBuild CI Report

CodeBuild project: Dafny
Commit ID: 2ece678
Result: FAILED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

robin-aws · 2020-03-05T00:38:29Z

AWS CodeBuild CI Report

CodeBuild project: Dafny
Commit ID: ec8405e
Result: SUCCEEDED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

RustanLeino

What's with DafnyRuntimeTests that makes them difficult to include at this time?

Some more tests of some compile code would be good. Also, it would be good to include that example (which I think sits somewhere in the test suite) that has the comment that says "this would be expensive to support at run time", to make sure it compiles correctly (to efficient code).

RustanLeino · 2020-03-05T04:50:51Z

Binaries/DafnyRuntime.cs

+ Type ty = typeof(G);
+ // TODO-RS: How to generalize this?
+ if (ty.Name.Equals("ISequence`1")) {
+ Type classType = Type.GetType("Dafny.Sequence`1");


Is the type Dafny.Sequence`1 always in the run time? If so, can its type be looked up with a typeof instead of by name? Also, is the `1 suffix unavoidable?

Yes this is super-sloppy and needs to be cleaned up. ISequence`1 is shorthand for "The ISequence type that takes one type parameter" (since C# allows overloading by number of type parameters). It's just a little tricky because I need to map from Dafny.ISequence<x> to Dafny.Sequence<x>, where x is a concrete type rather than the generic type parameter T, and I'm still learning the C# reflection model. I know how to do it in Java! :)

robin-aws · 2020-03-05T16:09:20Z

I hadn't intended this to be ready for review yet, I wanted to check that all tests passed on CodeBuild before I added a lot of new ones. Perhaps I should have put (draft PR don't review yet) in the title. :) Appreciate the eyes on it all the same though!

What's with DafnyRuntimeTests that makes them difficult to include at this time?

Nothing fundamental, it'll just be extra work to have the build process run C# tests as well as the lit tests. I initially created this just to validate my assumptions about the out type parameter qualifier, but plan to achieve adequate coverage through lit tests as usual. I definitely want to start adding C# tests but I didn't feel like this change was the right timing. I'm planning on returning to this in a later PR, but feel free to vote for getting the new project working now instead!

Some more tests of some compile code would be good. Also, it would be good to include that example (which I think sits somewhere in the test suite) that has the comment that says "this would be expensive to support at run time", to make sure it compiles correctly (to efficient code).

Agreed, working on the explicit tests now. You're referring to Test/dafny0/RuntimeTypeTests0.dfy I believe, which still doesn't work because it uses seq<object> which appears to be a special case. I'll check if it's easy to support that too.

robin-aws · 2020-03-05T16:18:17Z

Some more tests of some compile code would be good. Also, it would be good to include that example (which I think sits somewhere in the test suite) that has the comment that says "this would be expensive to support at run time", to make sure it compiles correctly (to efficient code).

Agreed, working on the explicit tests now. You're referring to Test/dafny0/RuntimeTypeTests0.dfy I believe, which still doesn't work because it uses seq<object> which appears to be a special case. I'll check if it's easy to support that too.

My mistake, that test happens to only cover set<trait> and (user-defined datatype)<trait>, which can be addressed with the same technique but requires about the same amount of compiler changes each, so I'm not going to address them in this PR. I will move my additional tests on seq<trait> to that file though.

robin-aws · 2020-03-05T17:44:49Z

AWS CodeBuild CI Report

CodeBuild project: Dafny
Commit ID: 8d66c02
Result: FAILED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

robin-aws · 2020-03-05T19:03:17Z

AWS CodeBuild CI Report

CodeBuild project: Dafny
Commit ID: 2a97770
Result: FAILED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

robin-aws · 2020-03-05T21:43:41Z

AWS CodeBuild CI Report

CodeBuild project: Dafny
Commit ID: e55eebc
Result: FAILED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

robin-aws · 2020-03-05T22:13:29Z

AWS CodeBuild CI Report

CodeBuild project: Dafny
Commit ID: a2b3639
Result: SUCCEEDED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

robin-aws · 2020-03-05T22:16:01Z

Ready for review now - interested in feedback on whether existing regression tests and the added case in Test/dafny0/RuntimeTypeTests0.dfy are adequate.

RustanLeino · 2020-03-06T23:41:41Z

Things look good. I think the one test in RuntimeTypeTests0.dfy is fine, since it mostly serves as a comparison with Datatype and set, which don't yet have this support. However, I do think that adding a run-time checked example would be appropriate, since the PR changes the run-time representation of sequences. (Note that, despite the /compile:3 flag and the Main method in this example, nothing gets executed because of the compiler errors.) Such tests would go well in Test/comp, where they could test the seq functionality for all target compilers.

robin-aws · 2020-03-09T16:49:44Z

AWS CodeBuild CI Report

CodeBuild project: Dafny
Commit ID: 97319ee
Result: SUCCEEDED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

…-of-trait-in-csharp

robin-aws · 2020-03-09T21:22:25Z

AWS CodeBuild CI Report

CodeBuild project: Dafny
Commit ID: bfea981
Result: SUCCEEDED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

robin-aws added 4 commits March 2, 2020 16:02

Partial work

e2e06ae

Better naming convention

8392e5a

More refactoring

f60634f

Fix Default<G>()

2ece678

Fix test, remove DafnyRuntimeTests (for now)

ec8405e

RustanLeino reviewed Mar 5, 2020

View reviewed changes

Moved tests into RuntimeTypeTests0.dfy, updated comments

8d66c02

More accurate compiler error comments

2a97770

Improve use of Type reflection, fix expected error line numbers

e55eebc

Handle non-generic types

a2b3639

robin-aws changed the title ~~Support seq<trait> in csharp (draft PR)~~ Support seq<trait> in C# Mar 5, 2020

robin-aws changed the title ~~Support seq<trait> in C#~~ Support seq<trait> in C# Mar 5, 2020

robin-aws marked this pull request as ready for review March 5, 2020 22:16

Add runtime tests for covariant sequences

97319ee

robin-aws changed the title ~~Support seq<trait> in C#~~ feat!: Support seq<trait> in C# Mar 9, 2020

RustanLeino approved these changes Mar 9, 2020

View reviewed changes

Merge branch 'master' of github.com:dafny-lang/dafny into compile-seq…

bfea981

…-of-trait-in-csharp

robin-aws merged commit 9d79b3c into dafny-lang:master Mar 9, 2020

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat!: Support seq<trait> in C# #557

feat!: Support seq<trait> in C# #557

robin-aws commented Mar 4, 2020 •

edited

Loading

robin-aws commented Mar 4, 2020

robin-aws commented Mar 5, 2020

RustanLeino left a comment

RustanLeino Mar 5, 2020

robin-aws Mar 5, 2020

robin-aws commented Mar 5, 2020

robin-aws commented Mar 5, 2020 •

edited

Loading

robin-aws commented Mar 5, 2020

robin-aws commented Mar 5, 2020

robin-aws commented Mar 5, 2020

robin-aws commented Mar 5, 2020

robin-aws commented Mar 5, 2020

RustanLeino commented Mar 6, 2020

robin-aws commented Mar 9, 2020

robin-aws commented Mar 9, 2020

feat!: Support seq<trait> in C# #557

feat!: Support seq<trait> in C# #557

Conversation

robin-aws commented Mar 4, 2020 • edited Loading

robin-aws commented Mar 4, 2020

AWS CodeBuild CI Report

robin-aws commented Mar 5, 2020

AWS CodeBuild CI Report

RustanLeino left a comment

Choose a reason for hiding this comment

RustanLeino Mar 5, 2020

Choose a reason for hiding this comment

robin-aws Mar 5, 2020

Choose a reason for hiding this comment

robin-aws commented Mar 5, 2020

robin-aws commented Mar 5, 2020 • edited Loading

robin-aws commented Mar 5, 2020

AWS CodeBuild CI Report

robin-aws commented Mar 5, 2020

AWS CodeBuild CI Report

robin-aws commented Mar 5, 2020

AWS CodeBuild CI Report

robin-aws commented Mar 5, 2020

AWS CodeBuild CI Report

robin-aws commented Mar 5, 2020

RustanLeino commented Mar 6, 2020

robin-aws commented Mar 9, 2020

AWS CodeBuild CI Report

robin-aws commented Mar 9, 2020

AWS CodeBuild CI Report

robin-aws commented Mar 4, 2020 •

edited

Loading

robin-aws commented Mar 5, 2020 •

edited

Loading