Skip to content

Commit

Permalink
feat: add SimpleBoolean for Rust
Browse files Browse the repository at this point in the history
  • Loading branch information
Andrew Banchich committed Apr 30, 2024
1 parent 8e74ac2 commit fe0bdc7
Show file tree
Hide file tree
Showing 22 changed files with 2,378 additions and 0 deletions.
903 changes: 903 additions & 0 deletions TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/Cargo.lock

Large diffs are not rendered by default.

23 changes: 23 additions & 0 deletions TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/Cargo.toml
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 TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/README.md
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.

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

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"
Loading

0 comments on commit fe0bdc7

Please sign in to comment.