-
Notifications
You must be signed in to change notification settings - Fork 8
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Andrew Banchich
committed
May 2, 2024
1 parent
8e74ac2
commit a89d9fb
Showing
24 changed files
with
2,164 additions
and
1 deletion.
There are no files selected for viewing
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
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
803 changes: 803 additions & 0 deletions
803
TestModels/SimpleTypes/SimpleBoolean/codegen-patches/rust/dafny-4.4.0.patch
Large diffs are not rendered by default.
Oops, something went wrong.
23 changes: 23 additions & 0 deletions
23
TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/Cargo.toml
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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,23 @@ | ||
[package] | ||
name = "simple_boolean" | ||
version = "0.1.0" | ||
edition = "2021" | ||
|
||
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html | ||
|
||
[dependencies] | ||
dafny_runtime = { path = "../../../../dafny-dependencies/dafny_runtime_rust"} | ||
dafny_standard_library = { path = "../../../../dafny-dependencies/StandardLibrary/runtimes/rust"} | ||
simple_boolean_dafny = { path = "./dafny_impl"} | ||
|
||
[dependencies.aws-smithy-runtime] | ||
features = ["client"] | ||
|
||
[dependencies.aws-smithy-runtime-api] | ||
features = ["client"] | ||
|
||
[dependencies.aws-smithy-types] | ||
|
||
[dev-dependencies.tokio] | ||
version = "1.26.0" | ||
features = ["full"] |
30 changes: 30 additions & 0 deletions
30
TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/README.md
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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,30 @@ | ||
This directory is the code generation target for the SimpleBoolean model when targetting Rust. | ||
|
||
Like the other targets, the crate is a combination of the output of three different components: | ||
|
||
1. The output of Dafny code generation for Rust (`src/implementation_from_dafny.rs`) | ||
2. The output of `smithy-dafny` shim/conversion generation for Rust (the `conversions` module) | ||
3. The output of `smithy-rs` (all other files) | ||
|
||
Most of the `smithy-rs` output is not modified, | ||
only trimmed down to cut out components that aren't relevant for Polymorph libraries. | ||
The main exception is `client.rs` and the operation builders such as `operation/get_boolean.rs`, | ||
which instantiate the underlying Dafny client implementation and invoke operations on it, respectively, | ||
instead of sending the operation value through an orchestrated plugin stack | ||
that eventually serializes it and sends it to a remote service endpoint. | ||
|
||
This crate also includes manually-written Rust tests demonstrating what it's like | ||
to work with the Rust API we're exposing. | ||
Although we need to also get the Dafny-generated tests working, | ||
the manually-written ones are also valuable. | ||
|
||
It looks likely that `smithy-rs` is pluggable enough that we can plug our conversion code generation | ||
into it without having to fork its implementation. | ||
This means we should be able to get 2. and 3. above out of a single call to `smithy-rs`. | ||
Hence I've optimistically left the "// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT." | ||
header on both kinds of files. | ||
|
||
Note that even 1. is hand-modified, as the Dafny Rust code generator is not yet complete, | ||
and rejects some features such as the type paramter variance specifier on `Option<+T>`. | ||
We are trusting that Dafny will soon generate exactly the content of `implementation_from_dafny.rs` | ||
and it is a priority to set up CI to assert that ASAP. |
13 changes: 13 additions & 0 deletions
13
TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/dafny_impl/Cargo.toml
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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,13 @@ | ||
[package] | ||
name = "simple_boolean_dafny" | ||
version = "0.1.0" | ||
edition = "2021" | ||
|
||
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html | ||
|
||
[dependencies] | ||
dafny_runtime = { path = "../../../../../dafny-dependencies/dafny_runtime_rust"} | ||
dafny_standard_library = { path = "../../../../../dafny-dependencies/StandardLibrary/runtimes/rust"} | ||
|
||
[lib] | ||
path = "src/implementation_from_dafny.rs" |
Oops, something went wrong.