Skip to content

Commit

Permalink
feat: add Positional Rust TestModel (#497)
Browse files Browse the repository at this point in the history
  • Loading branch information
andrewbanchich authored Sep 11, 2024
1 parent e6c895c commit a9039bb
Show file tree
Hide file tree
Showing 47 changed files with 2,136 additions and 1 deletion.
1 change: 1 addition & 0 deletions SmithyDafnyMakefile.mk
Original file line number Diff line number Diff line change
Expand Up @@ -582,6 +582,7 @@ _mv_implementation_rust:
# rustfmt has a recurring bug where it leaves behind trailing spaces and then complains about it.
# Pre-process the Dafny-generated Rust code to remove them.
sed -i -e 's/[[:space:]]*$$//' runtimes/rust/src/implementation_from_dafny.rs

rustfmt runtimes/rust/src/implementation_from_dafny.rs
rm -rf implementation_from_dafny-rust

Expand Down
1 change: 1 addition & 0 deletions TestModels/Positional/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@
CORES=2

ENABLE_EXTERN_PROCESSING=1
RUST_BENERATED=1

include ../SharedMakefile.mk

Expand Down
25 changes: 25 additions & 0 deletions TestModels/Positional/runtimes/rust/Cargo.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
[package]
name = "positional"
version = "0.1.0"
edition = "2021"

# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html

[features]
wrapped-client = []

[dependencies]
aws-smithy-runtime = {version = "1.6.0", features = ["client"] }
aws-smithy-runtime-api = {version = "1.7.0", features = ["client"] }
aws-smithy-types = "1.2.0"
dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust"}

[dev-dependencies]
positional = { path = ".", features = ["wrapped-client"] }

[dependencies.tokio]
version = "1.26.0"
features = ["full"]

[lib]
path = "src/implementation_from_dafny.rs"
30 changes: 30 additions & 0 deletions TestModels/Positional/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 Positional 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_positional.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.
38 changes: 38 additions & 0 deletions TestModels/Positional/runtimes/rust/src/client.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,38 @@
// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT.

use aws_smithy_types::error::operation::BuildError;

#[derive(::std::clone::Clone, ::std::fmt::Debug)]
pub struct Client {
pub(crate) dafny_client: ::dafny_runtime::Object<dyn crate::simple::positional::internaldafny::types::ISimplePositionalClient>
}

impl Client {
/// Creates a new client from the service [`Config`](crate::Config).
#[track_caller]
pub fn from_conf(
conf: crate::types::simple_positional_config::SimplePositionalConfig,
) -> Result<Self, BuildError> {
let inner =
crate::simple::positional::internaldafny::_default::SimplePositional(
&crate::conversions::simple_positional_config::_simple_positional_config::to_dafny(conf),
);
if matches!(
inner.as_ref(),
crate::_Wrappers_Compile::Result::Failure { .. }
) {
// TODO: convert error - the potential types are not modeled!
return Err(BuildError::other(
::aws_smithy_types::error::metadata::ErrorMetadata::builder()
.message("Invalid client config")
.build(),
));
}
Ok(Self {
dafny_client: ::dafny_runtime::upcast_object()(inner.Extract()),
})
}
}

mod get_resource;
mod get_resource_positional;
15 changes: 15 additions & 0 deletions TestModels/Positional/runtimes/rust/src/client/get_resource.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT.
impl super::Client {
/// Constructs a fluent builder for the [`GetResource`](crate::operation::get_resource::builders::GetResourceFluentBuilder) operation.
///
/// - The fluent builder is configurable:
/// - [`name(impl Into<String>)`](crate::operation::get_resource::builders::GetResourceFluentBuilder::name) / [`set_name(Option<String>)`](crate::operation::get_resource::builders::GetResourceFluentBuilder::set_name):<br>required: **true**<br>(undocumented)<br>
/// - On success, responds with [`GetResourceOutput`](crate::operation::get_resource::GetResourceOutput) with field(s):
/// - [`output(SimpleResourceReference)`](crate::operation::get_resource::GetResourceOutput::output): (undocumented)
/// - On failure, responds with [`SdkError<GetResourceError>`](crate::operation::get_resource::GetResourceError)
pub fn get_resource(
&self,
) -> crate::operation::get_resource::builders::GetResourceFluentBuilder {
crate::operation::get_resource::builders::GetResourceFluentBuilder::new(self.clone())
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT.
impl super::Client {
/// Constructs a fluent builder for the [`GetResourcePositional`](crate::operation::get_resource_positional::builders::GetResourcePositionalFluentBuilder) operation.
///
/// - The fluent builder is configurable:
/// - [`name(impl Into<String>)`](crate::operation::get_resource_positional::builders::GetResourcePositionalFluentBuilder::name) / [`set_name(Option<String>)`](crate::operation::get_resource_positional::builders::GetResourcePositionalFluentBuilder::set_name):<br>required: **true**<br>(undocumented)<br>
/// - On success, responds with [`GetResourcePositionalOutput`](crate::operation::get_resource_positional::GetResourcePositionalOutput) with field(s):
/// - [`output(SimpleResourceReference)`](crate::operation::get_resource_positional::GetResourcePositionalOutput::output): (undocumented)
/// - On failure, responds with [`SdkError<GetResourcePositionalError>`](crate::operation::get_resource_positional::GetResourcePositionalError)
pub fn get_resource_positional(
&self
) -> crate::operation::get_resource_positional::builders::GetResourcePositionalFluentBuilder
{
crate::operation::get_resource_positional::builders::GetResourcePositionalFluentBuilder::new(
self.clone(),
)
}
}
10 changes: 10 additions & 0 deletions TestModels/Positional/runtimes/rust/src/conversions.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT.
pub mod get_resource;
pub mod get_resource_positional;
pub mod get_name;

pub mod simple_positional_config;

pub mod simple_resource;

pub(crate) mod error;
32 changes: 32 additions & 0 deletions TestModels/Positional/runtimes/rust/src/conversions/error.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@
/// Wraps up an arbitrary Rust Error value as a Dafny Error
pub fn to_opaque_error<E: std::error::Error + 'static>(
value: E,
) -> ::std::rc::Rc<crate::simple::positional::internaldafny::types::Error>
{
let error_obj: ::dafny_runtime::Object<dyn ::std::any::Any> = ::dafny_runtime::Object(Some(
::std::rc::Rc::new(::std::cell::UnsafeCell::new(value)),
));
::std::rc::Rc::new(
crate::simple::positional::internaldafny::types::Error::Opaque {
obj: error_obj,
},
)
}

/// Wraps up an arbitrary Rust Error value as a Dafny Result<T, Error>.Failure
pub fn to_opaque_error_result<T: dafny_runtime::DafnyType, E: std::error::Error + 'static>(
value: E,
) -> ::std::rc::Rc<
crate::_Wrappers_Compile::Result<
T,
::std::rc::Rc<
crate::simple::positional::internaldafny::types::Error,
>,
>,
> {
::std::rc::Rc::new(
crate::_Wrappers_Compile::Result::Failure {
error: to_opaque_error(value),
},
)
}
34 changes: 34 additions & 0 deletions TestModels/Positional/runtimes/rust/src/conversions/get_name.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,34 @@
// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT.

use std::any::Any;

#[allow(dead_code)]
pub fn to_dafny_error(
value: crate::operation::get_name::GetNameError,
) -> ::std::rc::Rc<
crate::r#simple::positional::internaldafny::types::Error,
> {
match value {
crate::operation::get_name::GetNameError::Unhandled(unhandled) =>
::std::rc::Rc::new(crate::r#simple::positional::internaldafny::types::Error::Opaque { obj: ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(unhandled)) })
}
}

#[allow(dead_code)]
pub fn from_dafny_error(
dafny_value: ::std::rc::Rc<
crate::r#simple::positional::internaldafny::types::Error,
>,
) -> crate::operation::get_name::GetNameError {
// TODO: Losing information here, but we have to figure out how to wrap an arbitrary Dafny value as std::error::Error
if matches!(&dafny_value.as_ref(), crate::r#simple::positional::internaldafny::types::Error::CollectionOfErrors { .. }) {
let error_message = "TODO: can't get message yet";
crate::operation::get_name::GetNameError::generic(::aws_smithy_types::error::metadata::ErrorMetadata::builder().message(error_message).build())
} else {
crate::operation::get_name::GetNameError::generic(::aws_smithy_types::error::metadata::ErrorMetadata::builder().message("Opaque error").build())
}
}

pub mod _get_name_input;

pub mod _get_name_output;
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0
// Do not modify this file. This file is machine generated, and any changes to it will be overwritten.
#[allow(dead_code)]
pub fn to_dafny(
value: crate::operation::get_name::GetNameInput,
) -> ::std::rc::Rc<
crate::r#simple::positional::internaldafny::types::GetNameInput,
>{
::std::rc::Rc::new(crate::r#simple::positional::internaldafny::types::GetNameInput::GetNameInput {
})
}
#[allow(dead_code)]
pub fn from_dafny(
dafny_value: ::std::rc::Rc<
crate::r#simple::positional::internaldafny::types::GetNameInput,
>,
) -> crate::operation::get_name::GetNameInput {
crate::operation::get_name::GetNameInput::builder()
.build()
.unwrap()
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0
// Do not modify this file. This file is machine generated, and any changes to it will be overwritten.
#[allow(dead_code)]
pub fn to_dafny(
value: crate::operation::get_name::GetNameOutput,
) -> ::std::rc::Rc<
crate::r#simple::positional::internaldafny::types::GetNameOutput,
>{
::std::rc::Rc::new(crate::r#simple::positional::internaldafny::types::GetNameOutput::GetNameOutput {
name: dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&value.name.unwrap()),
})
}
#[allow(dead_code)]
pub fn from_dafny(
dafny_value: ::std::rc::Rc<
crate::r#simple::positional::internaldafny::types::GetNameOutput,
>,
) -> crate::operation::get_name::GetNameOutput {
crate::operation::get_name::GetNameOutput::builder()
.set_name(Some(dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(dafny_value.name())))
.build()
.unwrap()
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,34 @@
// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT.

use std::any::Any;

#[allow(dead_code)]
pub fn to_dafny_error(
value: crate::operation::get_resource::GetResourceError,
) -> ::std::rc::Rc<
crate::r#simple::positional::internaldafny::types::Error,
> {
match value {
crate::operation::get_resource::GetResourceError::Unhandled(unhandled) =>
::std::rc::Rc::new(crate::r#simple::positional::internaldafny::types::Error::Opaque { obj: ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(unhandled)) })
}
}

#[allow(dead_code)]
pub fn from_dafny_error(
dafny_value: ::std::rc::Rc<
crate::r#simple::positional::internaldafny::types::Error,
>,
) -> crate::operation::get_resource::GetResourceError {
// TODO: Losing information here, but we have to figure out how to wrap an arbitrary Dafny value as std::error::Error
if matches!(&dafny_value.as_ref(), crate::r#simple::positional::internaldafny::types::Error::CollectionOfErrors { .. }) {
let error_message = "TODO: can't get message yet";
crate::operation::get_resource::GetResourceError::generic(::aws_smithy_types::error::metadata::ErrorMetadata::builder().message(error_message).build())
} else {
crate::operation::get_resource::GetResourceError::generic(::aws_smithy_types::error::metadata::ErrorMetadata::builder().message("Opaque error").build())
}
}

pub mod _get_resource_input;

pub mod _get_resource_output;
Original file line number Diff line number Diff line change
@@ -0,0 +1,29 @@
// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT.
#[allow(dead_code)]
pub fn to_dafny(
value: crate::operation::get_resource::GetResourceInput,
) -> ::std::rc::Rc<
crate::r#simple::positional::internaldafny::types::GetResourceInput,
> {
let name = value.name().unwrap();
let name =
dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(name);

::std::rc::Rc::new(crate::r#simple::positional::internaldafny::types::GetResourceInput::GetResourceInput {
name,
})
}

#[allow(dead_code)]
pub fn from_dafny(
dafny_value: ::std::rc::Rc<
crate::r#simple::positional::internaldafny::types::GetResourceInput,
>,
) -> crate::operation::get_resource::GetResourceInput {
let name =
dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(
dafny_value.name(),
);

crate::operation::get_resource::GetResourceInput { name: Some(name) }
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0
// Do not modify this file. This file is machine generated, and any changes to it will be overwritten.
#[allow(dead_code)]
pub fn to_dafny(
value: crate::operation::get_resource::GetResourceOutput,
) -> ::std::rc::Rc<
crate::r#simple::positional::internaldafny::types::GetResourceOutput,
>{
::std::rc::Rc::new(crate::r#simple::positional::internaldafny::types::GetResourceOutput::GetResourceOutput {
output: crate::conversions::simple_resource::to_dafny(value.output.clone().unwrap())
,
})
}
#[allow(dead_code)]
pub fn from_dafny(
dafny_value: ::std::rc::Rc<
crate::r#simple::positional::internaldafny::types::GetResourceOutput,
>,
) -> crate::operation::get_resource::GetResourceOutput {
crate::operation::get_resource::GetResourceOutput::builder()
.set_output(Some( crate::conversions::simple_resource::from_dafny(dafny_value.output().clone())
))
.build()
.unwrap()
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT.

use std::any::Any;

#[allow(dead_code)]
pub fn to_dafny_error(
value: crate::operation::get_resource_positional::GetResourcePositionalError,
) -> ::std::rc::Rc<crate::simple::positional::internaldafny::types::Error>
{
match value {
crate::operation::get_resource_positional::GetResourcePositionalError::Unhandled(unhandled) =>
::std::rc::Rc::new(crate::simple::positional::internaldafny::types::Error::Opaque { obj: ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(unhandled)) })
}
}

#[allow(dead_code)]
pub fn from_dafny_error(
dafny_value: ::std::rc::Rc<
crate::simple::positional::internaldafny::types::Error,
>,
) -> crate::operation::get_resource_positional::GetResourcePositionalError {
// TODO: Losing information here, but we have to figure out how to wrap an arbitrary Dafny value as std::error::Error
if matches!(&dafny_value.as_ref(), crate::simple::positional::internaldafny::types::Error::CollectionOfErrors { .. }) {
let error_message = "TODO: can't get message yet";
crate::operation::get_resource_positional::GetResourcePositionalError::generic(::aws_smithy_types::error::metadata::ErrorMetadata::builder().message(error_message).build())
} else {
crate::operation::get_resource_positional::GetResourcePositionalError::generic(::aws_smithy_types::error::metadata::ErrorMetadata::builder().message("Opaque error").build())
}
}

pub mod _get_resource_positional_input;
Loading

0 comments on commit a9039bb

Please sign in to comment.