diff --git a/TestModels/LanguageSpecificLogic/Makefile b/TestModels/LanguageSpecificLogic/Makefile index b32098635..3eabbac60 100644 --- a/TestModels/LanguageSpecificLogic/Makefile +++ b/TestModels/LanguageSpecificLogic/Makefile @@ -3,6 +3,8 @@ CORES=2 +RUST_BENERATED=1 + include ../SharedMakefile.mk PROJECT_SERVICES := \ @@ -17,6 +19,10 @@ SMITHY_DEPS=dafny-dependencies/Model/traits.smithy # Projects using replaceable modules must explicitly define these values. NET_SRC_INDEX=src/replaces/net NET_TEST_INDEX=test/replaces/net +RUST_SRC_INDEX=src/replaces/rust +RUST_TEST_INDEX=test/replaces/rust + +RUST_OTHER_FILES=runtimes/rust/src/externs.rs # This project has no dependencies # DEPENDENT-MODELS:= diff --git a/TestModels/LanguageSpecificLogic/runtimes/net/Extern/ExternOperations.cs b/TestModels/LanguageSpecificLogic/runtimes/net/Extern/ExternOperations.cs index 5efcd3f6e..5a6dbfa08 100644 --- a/TestModels/LanguageSpecificLogic/runtimes/net/Extern/ExternOperations.cs +++ b/TestModels/LanguageSpecificLogic/runtimes/net/Extern/ExternOperations.cs @@ -8,24 +8,25 @@ namespace NetLanguageSpecificLogicImpl_Compile { - public partial class __default - { - public static - Wrappers_Compile._IResult< - Dafny.ISequence, - language.specific.logic.internaldafny.types._IError - > - GetNetRuntimeVersion ( - NetLanguageSpecificLogicImpl_Compile._IConfig config - ) { - return Wrappers_Compile.Result< - Dafny.ISequence, - language.specific.logic.internaldafny.types._IError - >.create_Success( - Dafny.Sequence.FromString( - System.Environment.Version.ToString() + public partial class __default + { + public static + Wrappers_Compile._IResult< + Dafny.ISequence, + language.specific.logic.internaldafny.types._IError + > + GetNetRuntimeVersion( + NetLanguageSpecificLogicImpl_Compile._IConfig config ) - ); - } - } + { + return Wrappers_Compile.Result< + Dafny.ISequence, + language.specific.logic.internaldafny.types._IError + >.create_Success( + Dafny.Sequence.FromString( + System.Environment.Version.ToString() + ) + ); + } + } } diff --git a/TestModels/LanguageSpecificLogic/runtimes/rust/Cargo.toml b/TestModels/LanguageSpecificLogic/runtimes/rust/Cargo.toml new file mode 100644 index 000000000..5c89c5cc4 --- /dev/null +++ b/TestModels/LanguageSpecificLogic/runtimes/rust/Cargo.toml @@ -0,0 +1,25 @@ +[package] +name = "language_specific_logic" +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] +language_specific_logic = { path = ".", features = ["wrapped-client"] } + +[dependencies.tokio] +version = "1.26.0" +features = ["full"] + +[lib] +path = "src/implementation_from_dafny.rs" diff --git a/TestModels/LanguageSpecificLogic/runtimes/rust/src/client.rs b/TestModels/LanguageSpecificLogic/runtimes/rust/src/client.rs new file mode 100644 index 000000000..1436ffda5 --- /dev/null +++ b/TestModels/LanguageSpecificLogic/runtimes/rust/src/client.rs @@ -0,0 +1,39 @@ +// 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 +} + +impl Client { + /// Creates a new client from the service [`Config`](crate::Config). + #[track_caller] + pub fn from_conf( + conf: crate::types::language_specific_logic_config::LanguageSpecificLogicConfig, + ) -> Result { + // If this service had any configuration properties, + // they would need converting here too. + let inner = + crate::language::specific::logic::internaldafny::_default::LanguageSpecificLogic( + &crate::conversions::language_specific_logic_config::_language_specific_logic_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_runtime_information; diff --git a/TestModels/LanguageSpecificLogic/runtimes/rust/src/client/get_runtime_information.rs b/TestModels/LanguageSpecificLogic/runtimes/rust/src/client/get_runtime_information.rs new file mode 100644 index 000000000..d8791bd44 --- /dev/null +++ b/TestModels/LanguageSpecificLogic/runtimes/rust/src/client/get_runtime_information.rs @@ -0,0 +1,12 @@ +// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. +impl super::Client { + /// Constructs a fluent builder for the [`GetRuntimeInformation`](crate::operation::get_runtime_information::builders::GetRuntimeInformationFluentBuilder) operation. + /// + /// - On success, responds with [`GetRuntimeInformationOutput`](crate::operation::get_runtime_information::GetRuntimeInformationOutput) with field(s): + /// - [`language(String)`](crate::operation::get_runtime_information::GetRuntimeInformationOutput::language): (undocumented) + /// - [`runtime(String)`](crate::operation::get_runtime_information::GetRuntimeInformationOutput::runtime): (undocumented) + /// - On failure, responds with [`SdkError`](crate::operation::get_runtime_information::GetRuntimeInformationError) + pub fn get_runtime_information(&self) -> crate::operation::get_runtime_information::builders::GetRuntimeInformationFluentBuilder { + crate::operation::get_runtime_information::builders::GetRuntimeInformationFluentBuilder::new(self.clone()) + } +} diff --git a/TestModels/LanguageSpecificLogic/runtimes/rust/src/conversions.rs b/TestModels/LanguageSpecificLogic/runtimes/rust/src/conversions.rs new file mode 100644 index 000000000..1f370a9b9 --- /dev/null +++ b/TestModels/LanguageSpecificLogic/runtimes/rust/src/conversions.rs @@ -0,0 +1,6 @@ +// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. +pub mod get_runtime_information; + +pub mod language_specific_logic_config; + +pub(crate) mod error; diff --git a/TestModels/LanguageSpecificLogic/runtimes/rust/src/conversions/error.rs b/TestModels/LanguageSpecificLogic/runtimes/rust/src/conversions/error.rs new file mode 100644 index 000000000..c5d1f5831 --- /dev/null +++ b/TestModels/LanguageSpecificLogic/runtimes/rust/src/conversions/error.rs @@ -0,0 +1,30 @@ +/// Wraps up an arbitrary Rust Error value as a Dafny Error +pub fn to_opaque_error(value: E) -> + ::std::rc::Rc +{ + let error_obj: ::dafny_runtime::Object = + ::dafny_runtime::Object(Some(::std::rc::Rc::new( + ::std::cell::UnsafeCell::new(value), + ))); + ::std::rc::Rc::new( + crate::r#language::specific::logic::internaldafny::types::Error::Opaque { + obj: error_obj, + }, + ) +} + +/// Wraps up an arbitrary Rust Error value as a Dafny Result.Failure +pub fn to_opaque_error_result(value: E) -> + ::std::rc::Rc< + crate::_Wrappers_Compile::Result< + T, + ::std::rc::Rc + > + > +{ + ::std::rc::Rc::new( + crate::_Wrappers_Compile::Result::Failure { + error: to_opaque_error(value) + } + ) +} diff --git a/TestModels/LanguageSpecificLogic/runtimes/rust/src/conversions/get_runtime_information.rs b/TestModels/LanguageSpecificLogic/runtimes/rust/src/conversions/get_runtime_information.rs new file mode 100644 index 000000000..9539a2bdc --- /dev/null +++ b/TestModels/LanguageSpecificLogic/runtimes/rust/src/conversions/get_runtime_information.rs @@ -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_runtime_information::GetRuntimeInformationError, +) -> ::std::rc::Rc +{ + match value { + crate::operation::get_runtime_information::GetRuntimeInformationError::Unhandled(unhandled) => + ::std::rc::Rc::new(crate::r#language::specific::logic::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#language::specific::logic::internaldafny::types::Error, + >, +) -> crate::operation::get_runtime_information::GetRuntimeInformationError { + // 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#language::specific::logic::internaldafny::types::Error::CollectionOfErrors { .. }) { + let error_message = "TODO: can't get message yet"; + crate::operation::get_runtime_information::GetRuntimeInformationError::generic(::aws_smithy_types::error::metadata::ErrorMetadata::builder().message(error_message).build()) + } else { + crate::operation::get_runtime_information::GetRuntimeInformationError::generic(::aws_smithy_types::error::metadata::ErrorMetadata::builder().message("Opaque error").build()) + } +} + +pub mod _get_runtime_information_output; diff --git a/TestModels/LanguageSpecificLogic/runtimes/rust/src/conversions/get_runtime_information/_get_runtime_information_output.rs b/TestModels/LanguageSpecificLogic/runtimes/rust/src/conversions/get_runtime_information/_get_runtime_information_output.rs new file mode 100644 index 000000000..dd3a1ccbe --- /dev/null +++ b/TestModels/LanguageSpecificLogic/runtimes/rust/src/conversions/get_runtime_information/_get_runtime_information_output.rs @@ -0,0 +1,49 @@ +// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. +#[allow(dead_code)] +pub fn to_dafny( + value: crate::operation::get_runtime_information::GetRuntimeInformationOutput, +) -> ::std::rc::Rc< + crate::r#language::specific::logic::internaldafny::types::GetRuntimeInformationOutput, +> { + let crate::operation::get_runtime_information::GetRuntimeInformationOutput { + language, + runtime, + } = value; + + let language = + dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string( + &language, + ); + + let runtime = + dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string( + &runtime, + ); + + ::std::rc::Rc::new(crate::r#language::specific::logic::internaldafny::types::GetRuntimeInformationOutput::GetRuntimeInformationOutput { + language: language, + runtime: runtime, + }) +} + +#[allow(dead_code)] +pub fn from_dafny( + dafny_value: ::std::rc::Rc, +) -> crate::operation::get_runtime_information::GetRuntimeInformationOutput { + let crate::r#language::specific::logic::internaldafny::types::GetRuntimeInformationOutput::GetRuntimeInformationOutput { language, runtime } = dafny_value.as_ref(); + + let language = + dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string( + &language, + ); + + let runtime = + dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string( + &runtime, + ); + + crate::operation::get_runtime_information::GetRuntimeInformationOutput { + language, + runtime, + } +} diff --git a/TestModels/LanguageSpecificLogic/runtimes/rust/src/conversions/language_specific_logic_config.rs b/TestModels/LanguageSpecificLogic/runtimes/rust/src/conversions/language_specific_logic_config.rs new file mode 100644 index 000000000..8516fd7d6 --- /dev/null +++ b/TestModels/LanguageSpecificLogic/runtimes/rust/src/conversions/language_specific_logic_config.rs @@ -0,0 +1,3 @@ +// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. + +pub mod _language_specific_logic_config; diff --git a/TestModels/LanguageSpecificLogic/runtimes/rust/src/conversions/language_specific_logic_config/_language_specific_logic_config.rs b/TestModels/LanguageSpecificLogic/runtimes/rust/src/conversions/language_specific_logic_config/_language_specific_logic_config.rs new file mode 100644 index 000000000..f43a415a2 --- /dev/null +++ b/TestModels/LanguageSpecificLogic/runtimes/rust/src/conversions/language_specific_logic_config/_language_specific_logic_config.rs @@ -0,0 +1,19 @@ +// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. +#[allow(dead_code)] + +pub fn to_dafny( + value: crate::types::language_specific_logic_config::LanguageSpecificLogicConfig, +) -> ::std::rc::Rc< + crate::language::specific::logic::internaldafny::types::LanguageSpecificLogicConfig, +> { + ::std::rc::Rc::new(crate::r#language::specific::logic::internaldafny::types::LanguageSpecificLogicConfig::LanguageSpecificLogicConfig {}) +} + +#[allow(dead_code)] +pub fn from_dafny( + dafny_value: ::std::rc::Rc< + crate::r#language::specific::logic::internaldafny::types::LanguageSpecificLogicConfig, + >, +) -> crate::types::language_specific_logic_config::LanguageSpecificLogicConfig { + crate::types::language_specific_logic_config::LanguageSpecificLogicConfig {} +} diff --git a/TestModels/LanguageSpecificLogic/runtimes/rust/src/error.rs b/TestModels/LanguageSpecificLogic/runtimes/rust/src/error.rs new file mode 100644 index 000000000..ec89cbecc --- /dev/null +++ b/TestModels/LanguageSpecificLogic/runtimes/rust/src/error.rs @@ -0,0 +1,14 @@ +// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. +pub use ::aws_smithy_runtime_api::box_error::BoxError; + +/// Error type returned by the client. +pub type SdkError = + ::aws_smithy_runtime_api::client::result::SdkError; +pub use ::aws_smithy_runtime_api::client::result::ConnectorError; +pub use ::aws_smithy_types::error::operation::BuildError; + +pub use ::aws_smithy_types::error::display::DisplayErrorContext; +pub use ::aws_smithy_types::error::metadata::ErrorMetadata; +pub use ::aws_smithy_types::error::metadata::ProvideErrorMetadata; + +pub(crate) mod sealed_unhandled; diff --git a/TestModels/LanguageSpecificLogic/runtimes/rust/src/error/sealed_unhandled.rs b/TestModels/LanguageSpecificLogic/runtimes/rust/src/error/sealed_unhandled.rs new file mode 100644 index 000000000..cce22d1cf --- /dev/null +++ b/TestModels/LanguageSpecificLogic/runtimes/rust/src/error/sealed_unhandled.rs @@ -0,0 +1,26 @@ +// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. +/// This struct is not intended to be used. +/// +/// This struct holds information about an unhandled error, +/// but that information should be obtained by using the +/// [`ProvideErrorMetadata`](::aws_smithy_types::error::metadata::ProvideErrorMetadata) trait +/// on the error type. +/// +/// This struct intentionally doesn't yield any useful information itself. +#[deprecated( + note = "Matching `Unhandled` directly is not forwards compatible. Instead, match using a \ +variable wildcard pattern and check `.code()`: + \ +   `err if err.code() == Some(\"SpecificExceptionCode\") => { /* handle the error */ }` + \ +See [`ProvideErrorMetadata`](::aws_smithy_types::error::metadata::ProvideErrorMetadata) for what information is available for the error." +)] +#[derive(Debug)] +pub struct Unhandled { + pub(crate) source: ::aws_smithy_runtime_api::box_error::BoxError, + pub(crate) meta: ::aws_smithy_types::error::metadata::ErrorMetadata, +} + +impl ::dafny_runtime::UpcastObject for Unhandled { + ::dafny_runtime::UpcastObjectFn!(dyn ::std::any::Any); +} diff --git a/TestModels/LanguageSpecificLogic/runtimes/rust/src/externs.rs b/TestModels/LanguageSpecificLogic/runtimes/rust/src/externs.rs new file mode 100644 index 000000000..0d275900d --- /dev/null +++ b/TestModels/LanguageSpecificLogic/runtimes/rust/src/externs.rs @@ -0,0 +1,24 @@ +#![allow(warnings, unconditional_panic)] +#![allow(nonstandard_style)] + +impl crate::r#_LanguageSpecificLogicImpl_Compile::_default { + pub fn GetRustRuntimeVersion( + config: &::std::rc::Rc, + ) -> ::std::rc::Rc< + crate::r#_Wrappers_Compile::Result< + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + ::std::rc::Rc, + >, + > { + let os = ::std::env::consts::OS; + let arch = ::std::env::consts::ARCH; + let runtime = ::std::format!("{} {}", os, arch); + + let runtime_str = + dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string( + &runtime, + ); + let result = crate::r#_Wrappers_Compile::Result::Success { value: runtime_str }; + ::std::rc::Rc::new(result) + } +} diff --git a/TestModels/LanguageSpecificLogic/runtimes/rust/src/lib.rs b/TestModels/LanguageSpecificLogic/runtimes/rust/src/lib.rs new file mode 100644 index 000000000..7d3f2bb59 --- /dev/null +++ b/TestModels/LanguageSpecificLogic/runtimes/rust/src/lib.rs @@ -0,0 +1,24 @@ +#![allow(deprecated)] + +// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. + +pub mod client; +pub mod types; + +/// Common errors and error handling utilities. +pub mod error; + +/// All operations that this crate can perform. +pub mod operation; + +mod conversions; + +pub mod implementation_from_dafny; + +mod externs; + +#[cfg(feature = "wrapped-client")] +pub mod wrapped; + +pub use client::Client; +pub use types::language_specific_logic_config::LanguageSpecificLogicConfig; diff --git a/TestModels/LanguageSpecificLogic/runtimes/rust/src/operation.rs b/TestModels/LanguageSpecificLogic/runtimes/rust/src/operation.rs new file mode 100644 index 000000000..236168ae0 --- /dev/null +++ b/TestModels/LanguageSpecificLogic/runtimes/rust/src/operation.rs @@ -0,0 +1,4 @@ +// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. + +/// Types for the `GetRuntimeInformation` operation. +pub mod get_runtime_information; diff --git a/TestModels/LanguageSpecificLogic/runtimes/rust/src/operation/get_runtime_information.rs b/TestModels/LanguageSpecificLogic/runtimes/rust/src/operation/get_runtime_information.rs new file mode 100644 index 000000000..d3015b8d6 --- /dev/null +++ b/TestModels/LanguageSpecificLogic/runtimes/rust/src/operation/get_runtime_information.rs @@ -0,0 +1,139 @@ +// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. +/// Orchestration and serialization glue logic for `GetRuntimeInformation`. +#[derive(::std::clone::Clone, ::std::default::Default, ::std::fmt::Debug)] +#[non_exhaustive] +pub struct GetRuntimeInformation; +impl GetRuntimeInformation { + /// Creates a new `GetRuntimeInformation` + pub fn new() -> Self { + Self + } + pub(crate) async fn send( + client: &crate::client::Client, + ) -> ::std::result::Result< + crate::operation::get_runtime_information::GetRuntimeInformationOutput, + crate::operation::get_runtime_information::GetRuntimeInformationError, + > { + let inner_result = + ::dafny_runtime::md!(client.dafny_client.clone()).GetRuntimeInformation(); + if matches!( + inner_result.as_ref(), + crate::r#_Wrappers_Compile::Result::Success { .. } + ) { + Ok( + crate::conversions::get_runtime_information::_get_runtime_information_output::from_dafny( + inner_result.value().clone(), + ), + ) + } else { + Err(crate::conversions::get_runtime_information::from_dafny_error( + inner_result.error().clone(), + )) + } + } +} + +/// Error type for the `GetRuntimeInformation` operation. +#[non_exhaustive] +#[derive(::std::fmt::Debug)] +pub enum GetRuntimeInformationError { + /// An unexpected error occurred (e.g., invalid JSON returned by the service or an unknown error code). + #[deprecated( + note = "Matching `Unhandled` directly is not forwards compatible. Instead, match using a \ + variable wildcard pattern and check `.code()`: + \ +    `err if err.code() == Some(\"SpecificExceptionCode\") => { /* handle the error */ }` + \ + See [`ProvideErrorMetadata`](#impl-ProvideErrorMetadata-for-GetRuntimeInformationError) for what information is available for the error." + )] + Unhandled(crate::error::sealed_unhandled::Unhandled), +} +impl GetRuntimeInformationError { + /// Creates the `GetRuntimeInformationError::Unhandled` variant from any error type. + pub fn unhandled( + err: impl ::std::convert::Into< + ::std::boxed::Box< + dyn ::std::error::Error + ::std::marker::Send + ::std::marker::Sync + 'static, + >, + >, + ) -> Self { + Self::Unhandled(crate::error::sealed_unhandled::Unhandled { + source: err.into(), + meta: ::std::default::Default::default(), + }) + } + + /// Creates the `GetRuntimeInformationError::Unhandled` variant from an [`ErrorMetadata`](::aws_smithy_types::error::ErrorMetadata). + pub fn generic(err: ::aws_smithy_types::error::ErrorMetadata) -> Self { + Self::Unhandled(crate::error::sealed_unhandled::Unhandled { + source: err.clone().into(), + meta: err, + }) + } + /// + /// Returns error metadata, which includes the error code, message, + /// request ID, and potentially additional information. + /// + pub fn meta(&self) -> &::aws_smithy_types::error::ErrorMetadata { + match self { + Self::Unhandled(e) => &e.meta, + } + } +} +impl ::std::error::Error for GetRuntimeInformationError { + fn source(&self) -> ::std::option::Option<&(dyn ::std::error::Error + 'static)> { + match self { + Self::Unhandled(_inner) => ::std::option::Option::Some(&*_inner.source), + } + } +} +impl ::std::fmt::Display for GetRuntimeInformationError { + fn fmt(&self, f: &mut ::std::fmt::Formatter<'_>) -> ::std::fmt::Result { + match self { + Self::Unhandled(_inner) => { + if let ::std::option::Option::Some(code) = + ::aws_smithy_types::error::metadata::ProvideErrorMetadata::code(self) + { + write!(f, "unhandled error ({code})") + } else { + f.write_str("unhandled error") + } + } + } + } +} +impl ::aws_smithy_types::retry::ProvideErrorKind for GetRuntimeInformationError { + fn code(&self) -> ::std::option::Option<&str> { + ::aws_smithy_types::error::metadata::ProvideErrorMetadata::code(self) + } + fn retryable_error_kind(&self) -> ::std::option::Option<::aws_smithy_types::retry::ErrorKind> { + ::std::option::Option::None + } +} +impl ::aws_smithy_types::error::metadata::ProvideErrorMetadata for GetRuntimeInformationError { + fn meta(&self) -> &::aws_smithy_types::error::ErrorMetadata { + match self { + Self::Unhandled(_inner) => &_inner.meta, + } + } +} +impl ::aws_smithy_runtime_api::client::result::CreateUnhandledError for GetRuntimeInformationError { + fn create_unhandled_error( + source: ::std::boxed::Box< + dyn ::std::error::Error + ::std::marker::Send + ::std::marker::Sync + 'static, + >, + meta: ::std::option::Option<::aws_smithy_types::error::ErrorMetadata>, + ) -> Self { + Self::Unhandled(crate::error::sealed_unhandled::Unhandled { + source, + meta: meta.unwrap_or_default(), + }) + } +} + +pub use crate::operation::get_runtime_information::_get_runtime_information_output::GetRuntimeInformationOutput; + +mod _get_runtime_information_output; + +/// Builders +pub mod builders; diff --git a/TestModels/LanguageSpecificLogic/runtimes/rust/src/operation/get_runtime_information/_get_runtime_information_output.rs b/TestModels/LanguageSpecificLogic/runtimes/rust/src/operation/get_runtime_information/_get_runtime_information_output.rs new file mode 100644 index 000000000..f63eb9804 --- /dev/null +++ b/TestModels/LanguageSpecificLogic/runtimes/rust/src/operation/get_runtime_information/_get_runtime_information_output.rs @@ -0,0 +1,78 @@ +// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. +#[allow(missing_docs)] // documentation missing in model +#[non_exhaustive] +#[derive(::std::clone::Clone, ::std::cmp::PartialEq, ::std::fmt::Debug)] +pub struct GetRuntimeInformationOutput { + #[allow(missing_docs)] // documentation missing in model + pub language: ::std::string::String, + #[allow(missing_docs)] // documentation missing in model + pub runtime: ::std::string::String, +} +impl GetRuntimeInformationOutput { + #[allow(missing_docs)] // documentation missing in model + pub fn language(&self) -> &str { + &self.language + } + #[allow(missing_docs)] // documentation missing in model + pub fn runtime(&self) -> &str { + &self.runtime + } +} +impl GetRuntimeInformationOutput { + /// Creates a new builder-style object to manufacture [`GetRuntimeInformationOutput`](crate::operation::operation::GetRuntimeInformationOutput). + pub fn builder() -> crate::operation::get_runtime_information::builders::GetRuntimeInformationOutputBuilder { + crate::operation::get_runtime_information::builders::GetRuntimeInformationOutputBuilder::default() + } +} + +/// A builder for [`GetRuntimeInformationOutput`](crate::operation::operation::GetRuntimeInformationOutput). +#[non_exhaustive] +#[derive( + ::std::clone::Clone, ::std::cmp::PartialEq, ::std::default::Default, ::std::fmt::Debug, +)] +pub struct GetRuntimeInformationOutputBuilder { + pub(crate) language: ::std::string::String, + pub(crate) runtime: ::std::string::String, +} +impl GetRuntimeInformationOutputBuilder { + #[allow(missing_docs)] // documentation missing in model + pub fn language(mut self, input: impl ::std::convert::Into<::std::string::String>) -> Self { + self.language = input.into(); + self + } + #[allow(missing_docs)] // documentation missing in model + pub fn set_language(mut self, input: ::std::string::String) -> Self { + self.language = input; + self + } + #[allow(missing_docs)] // documentation missing in model + pub fn get_language(&self) -> &::std::string::String { + &self.language + } + #[allow(missing_docs)] // documentation missing in model + pub fn runtime(mut self, input: impl ::std::convert::Into<::std::string::String>) -> Self { + self.runtime = input.into(); + self + } + #[allow(missing_docs)] // documentation missing in model + pub fn set_runtime(mut self, input: ::std::string::String) -> Self { + self.runtime = input; + self + } + #[allow(missing_docs)] // documentation missing in model + pub fn get_runtime(&self) -> &::std::string::String { + &self.runtime + } + /// Consumes the builder and constructs a [`GetRuntimeInformationOutput`](crate::operation::operation::GetRuntimeInformationOutput). + pub fn build( + self, + ) -> ::std::result::Result< + crate::operation::get_runtime_information::GetRuntimeInformationOutput, + ::aws_smithy_types::error::operation::BuildError, + > { + ::std::result::Result::Ok(crate::operation::get_runtime_information::GetRuntimeInformationOutput { + language: self.language, + runtime: self.runtime, + }) + } +} diff --git a/TestModels/LanguageSpecificLogic/runtimes/rust/src/operation/get_runtime_information/builders.rs b/TestModels/LanguageSpecificLogic/runtimes/rust/src/operation/get_runtime_information/builders.rs new file mode 100644 index 000000000..7f134241f --- /dev/null +++ b/TestModels/LanguageSpecificLogic/runtimes/rust/src/operation/get_runtime_information/builders.rs @@ -0,0 +1,26 @@ +// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. +pub use crate::operation::get_runtime_information::_get_runtime_information_output::GetRuntimeInformationOutputBuilder; + +/// Fluent builder constructing a request to `GetRuntimeInformation`. +/// +#[derive(::std::clone::Clone, ::std::fmt::Debug)] +pub struct GetRuntimeInformationFluentBuilder { + client: crate::Client, +} +impl GetRuntimeInformationFluentBuilder { + /// Creates a new `GetRuntimeInformation`. + pub(crate) fn new(client: crate::Client) -> Self { + Self { + client, + } + } + /// Sends the request and returns the response. + pub async fn send( + self, + ) -> ::std::result::Result< + crate::operation::get_runtime_information::GetRuntimeInformationOutput, + crate::operation::get_runtime_information::GetRuntimeInformationError, + > { + crate::operation::get_runtime_information::GetRuntimeInformation::send(&self.client).await + } +} diff --git a/TestModels/LanguageSpecificLogic/runtimes/rust/src/standard_library_conversions.rs b/TestModels/LanguageSpecificLogic/runtimes/rust/src/standard_library_conversions.rs new file mode 100644 index 000000000..3a51134c6 --- /dev/null +++ b/TestModels/LanguageSpecificLogic/runtimes/rust/src/standard_library_conversions.rs @@ -0,0 +1,246 @@ +pub fn ostring_to_dafny( + input: &Option, +) -> ::std::rc::Rc< + crate::_Wrappers_Compile::Option<::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>>, +> { + let dafny_value = match input { + Some(b) => crate::_Wrappers_Compile::Option::Some { value: + dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&b) + }, + None => crate::_Wrappers_Compile::Option::None {}, +}; + ::std::rc::Rc::new(dafny_value) +} + +pub fn ostring_from_dafny( + input: ::std::rc::Rc< + crate::_Wrappers_Compile::Option<::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>>, + >, +) -> Option { + if matches!(input.as_ref(), crate::_Wrappers_Compile::Option::Some { .. }) { + Some( + dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string( + &input.Extract(), + ), + ) + } else { + None + } +} + +pub fn obool_to_dafny(input: Option) -> ::std::rc::Rc> { + let dafny_value = match input { + Some(b) => crate::_Wrappers_Compile::Option::Some { value: b }, + None => crate::_Wrappers_Compile::Option::None {}, + }; + ::std::rc::Rc::new(dafny_value) +} + +pub fn obool_from_dafny(input: ::std::rc::Rc>) -> Option { + if matches!(input.as_ref(), crate::_Wrappers_Compile::Option::Some { .. }) { + Some(input.Extract()) + } else { + None + } +} + +pub fn oint_to_dafny(input: Option) -> ::std::rc::Rc> { + let dafny_value = match input { + Some(b) => crate::_Wrappers_Compile::Option::Some { value: b }, + None => crate::_Wrappers_Compile::Option::None {}, + }; + ::std::rc::Rc::new(dafny_value) +} + +pub fn oint_from_dafny(input: ::std::rc::Rc>) -> Option { + if matches!(input.as_ref(), crate::_Wrappers_Compile::Option::Some { .. }) { + Some(input.Extract()) + } else { + None + } +} + +pub fn olong_to_dafny(input: Option) -> ::std::rc::Rc> { + let dafny_value = match input { + Some(b) => crate::_Wrappers_Compile::Option::Some { value: b }, + None => crate::_Wrappers_Compile::Option::None {}, + }; + ::std::rc::Rc::new(dafny_value) +} + +pub fn olong_from_dafny(input: ::std::rc::Rc>) -> Option { + if matches!(input.as_ref(), crate::_Wrappers_Compile::Option::Some { .. }) { + Some(input.Extract()) + } else { + None + } +} + +pub fn blob_to_dafny( + input: &::aws_smithy_types::Blob, +) -> ::dafny_runtime::Sequence { + ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(&input.clone().into_inner(), |x| *x) +} + +pub fn oblob_to_dafny( + input: &Option<::aws_smithy_types::Blob>, +) -> ::std::rc::Rc>> { + let dafny_value = match input { + Some(b) => crate::_Wrappers_Compile::Option::Some { + value: blob_to_dafny(&b), + }, + None => crate::_Wrappers_Compile::Option::None {}, + }; + ::std::rc::Rc::new(dafny_value) +} + +pub fn blob_from_dafny( + input: ::dafny_runtime::Sequence, +) -> ::aws_smithy_types::Blob { + + ::aws_smithy_types::Blob::new( + ::std::rc::Rc::try_unwrap(input.to_array()) + .unwrap_or_else(|rc| (*rc).clone()), + ) +} + +pub fn oblob_from_dafny( + input: ::std::rc::Rc>>, +) -> Option<::aws_smithy_types::Blob> { + if matches!(input.as_ref(), crate::_Wrappers_Compile::Option::Some { .. }) { + Some(blob_from_dafny(input.Extract())) + } else { + None + } +} + +pub fn double_to_dafny( + input: f64, +) -> ::dafny_runtime::Sequence { + ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence( + &f64::to_be_bytes(input).to_vec(), + |x| *x) +} + +pub fn odouble_to_dafny( + input: &Option, +) -> ::std::rc::Rc>> { + let dafny_value = match input { + Some(f) => crate::_Wrappers_Compile::Option::Some { + value: double_to_dafny(*f), + }, + None => crate::_Wrappers_Compile::Option::None {}, + }; + ::std::rc::Rc::new(dafny_value) +} + +pub fn double_from_dafny( + input: &::dafny_runtime::Sequence, +) -> f64 { + let v = ::dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(input, |x| *x); + f64::from_be_bytes(v.try_into().expect("Error converting Sequence to f64")) +} + +pub fn odouble_from_dafny( + input: ::std::rc::Rc>>, +) -> Option { + if matches!(input.as_ref(), crate::_Wrappers_Compile::Option::Some { .. }) { + Some(double_from_dafny(&input.Extract())) + } else { + None + } +} + +pub fn timestamp_to_dafny( + input: ::aws_smithy_types::DateTime, +) -> ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16> { + ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&input.to_string()) +} + +pub fn otimestamp_to_dafny( + input: &Option<::aws_smithy_types::DateTime>, +) -> ::std::rc::Rc>> { + let dafny_value = match input { + Some(f) => crate::_Wrappers_Compile::Option::Some { + value: timestamp_to_dafny(*f), + }, + None => crate::_Wrappers_Compile::Option::None {}, + }; + ::std::rc::Rc::new(dafny_value) +} + +pub fn timestamp_from_dafny( + input: ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, +) -> ::aws_smithy_types::DateTime { + let s = dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(&input); + ::aws_smithy_types::DateTime::from_str( + &s, + aws_smithy_types::date_time::Format::DateTime, + ).unwrap() +} + +pub fn otimestamp_from_dafny( + input: ::std::rc::Rc>>, +) -> Option<::aws_smithy_types::DateTime> { + if matches!(input.as_ref(), crate::_Wrappers_Compile::Option::Some { .. }) { + Some(timestamp_from_dafny(input.Extract())) + } else { + None + } +} + +pub fn option_from_dafny( + input: ::std::rc::Rc>, + converter: fn(&T) -> TR, +) -> Option { + match &*input { + crate::_Wrappers_Compile::Option::Some { value } => Some(converter(value)), + crate::_Wrappers_Compile::Option::None { } => None, + } +} + +pub fn option_to_dafny( + input: &Option, + converter: fn(&TR) -> T, +) -> ::std::rc::Rc> { + match input { + Some(value) => ::std::rc::Rc::new( + crate::_Wrappers_Compile::Option::Some { + value: converter(&value) + } + ), + None => ::std::rc::Rc::new( + crate::_Wrappers_Compile::Option::None {} + ), + } +} + +pub fn result_from_dafny( + input: ::std::rc::Rc>, + converter_t: fn(&T) -> TR, + converter_e: fn(&E) -> ER, +) -> Result { + match &*input { + crate::_Wrappers_Compile::Result::Success { value } => Ok(converter_t(value)), + crate::_Wrappers_Compile::Result::Failure { error } => Err(converter_e(error)), + } +} + +pub fn result_to_dafny( + input: &Result, + converter_t: fn(&TR) -> T, + converter_e: fn(&ER) -> E, +) -> ::std::rc::Rc> { + match input { + Ok(value) => ::std::rc::Rc::new( + crate::_Wrappers_Compile::Result::Success { + value: converter_t(&value) + } + ), + Err(error) => ::std::rc::Rc::new( + crate::_Wrappers_Compile::Result::Failure { + error: converter_e(&error) + } + ), + } +} \ No newline at end of file diff --git a/TestModels/LanguageSpecificLogic/runtimes/rust/src/types.rs b/TestModels/LanguageSpecificLogic/runtimes/rust/src/types.rs new file mode 100644 index 000000000..6a0613663 --- /dev/null +++ b/TestModels/LanguageSpecificLogic/runtimes/rust/src/types.rs @@ -0,0 +1,4 @@ +// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. + +/// Types for the `LanguageSpecificLogicConfig` +pub mod language_specific_logic_config; diff --git a/TestModels/LanguageSpecificLogic/runtimes/rust/src/types/language_specific_logic_config.rs b/TestModels/LanguageSpecificLogic/runtimes/rust/src/types/language_specific_logic_config.rs new file mode 100644 index 000000000..4ace3ff26 --- /dev/null +++ b/TestModels/LanguageSpecificLogic/runtimes/rust/src/types/language_specific_logic_config.rs @@ -0,0 +1,26 @@ +// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. + +#[derive(::std::clone::Clone, ::std::fmt::Debug)] +pub struct LanguageSpecificLogicConfig {} + +impl LanguageSpecificLogicConfig { + pub fn builder() -> LanguageSpecificLogicConfigBuilder { + LanguageSpecificLogicConfigBuilder::new() + } +} + +#[derive(::std::clone::Clone, ::std::fmt::Debug)] +pub struct LanguageSpecificLogicConfigBuilder {} + +impl LanguageSpecificLogicConfigBuilder { + /// Creates a new `LanguageSpecificLogicConfigBuilder`. + pub(crate) fn new() -> Self { + Self {} + } + pub fn build( + self, + ) -> ::std::result::Result + { + ::std::result::Result::Ok(LanguageSpecificLogicConfig {}) + } +} diff --git a/TestModels/LanguageSpecificLogic/runtimes/rust/src/wrapped.rs b/TestModels/LanguageSpecificLogic/runtimes/rust/src/wrapped.rs new file mode 100644 index 000000000..b9babe5bc --- /dev/null +++ b/TestModels/LanguageSpecificLogic/runtimes/rust/src/wrapped.rs @@ -0,0 +1 @@ +pub mod client; diff --git a/TestModels/LanguageSpecificLogic/runtimes/rust/src/wrapped/client.rs b/TestModels/LanguageSpecificLogic/runtimes/rust/src/wrapped/client.rs new file mode 100644 index 000000000..139f0a97a --- /dev/null +++ b/TestModels/LanguageSpecificLogic/runtimes/rust/src/wrapped/client.rs @@ -0,0 +1,83 @@ +use tokio::runtime::Runtime; + +pub struct Client { + wrapped: crate::client::Client, + + /// A `current_thread` runtime for executing operations on the + /// asynchronous client in a blocking manner. + rt: Runtime +} + +impl dafny_runtime::UpcastObject for Client { + ::dafny_runtime::UpcastObjectFn!(dyn crate::r#language::specific::logic::internaldafny::types::ILanguageSpecificLogicClient); +} + +impl dafny_runtime::UpcastObject for Client { + ::dafny_runtime::UpcastObjectFn!(dyn ::std::any::Any); +} + +impl Client { + pub fn from_conf(config: &::std::rc::Rc< + crate::r#language::specific::logic::internaldafny::types::LanguageSpecificLogicConfig, + >) -> +::std::rc::Rc, + ::std::rc::Rc +>> { + let rt_result = tokio::runtime::Builder::new_current_thread() + .enable_all() + .build(); + let rt = match rt_result { + Ok(x) => x, + Err(error) => return crate::conversions::error::to_opaque_error_result(error), + }; + let result = crate::client::Client::from_conf( + crate::conversions::language_specific_logic_config::_language_specific_logic_config::from_dafny( + config.clone(), + ), + ); + match result { + Ok(client) => { + let wrap = crate::wrapped::client::Client { + wrapped: client, + rt + }; + std::rc::Rc::new( + crate::_Wrappers_Compile::Result::Success { + value: ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(wrap)) + } + ) + }, + Err(error) => crate::conversions::error::to_opaque_error_result(error) + } + } +} + +impl crate::r#language::specific::logic::internaldafny::types::ILanguageSpecificLogicClient + for Client +{ + fn GetRuntimeInformation( + &mut self, + ) -> std::rc::Rc< + crate::r#_Wrappers_Compile::Result< + std::rc::Rc< + crate::r#language::specific::logic::internaldafny::types::GetRuntimeInformationOutput, + >, + std::rc::Rc, + >, + >{ + let result = self.rt.block_on(crate::operation::get_runtime_information::GetRuntimeInformation::send(&self.wrapped)); + match result { + Err(error) => ::std::rc::Rc::new( + crate::_Wrappers_Compile::Result::Failure { + error: crate::conversions::get_runtime_information::to_dafny_error(error), + }, + ), + Ok(client) => ::std::rc::Rc::new( + crate::_Wrappers_Compile::Result::Success { + value: crate::conversions::get_runtime_information::_get_runtime_information_output::to_dafny(client), + }, + ), + } + } +} diff --git a/TestModels/LanguageSpecificLogic/runtimes/rust/tests/language_specific_logic_test.rs b/TestModels/LanguageSpecificLogic/runtimes/rust/tests/language_specific_logic_test.rs new file mode 100644 index 000000000..03cd5a30f --- /dev/null +++ b/TestModels/LanguageSpecificLogic/runtimes/rust/tests/language_specific_logic_test.rs @@ -0,0 +1,19 @@ +use language_specific_logic::*; + + +#[tokio::test] +async fn test_get_runtime_information() { + let result = client() + .get_runtime_information() + .send() + .await; + let output = result.unwrap(); + assert_eq!(output.language(), "Rust"); + assert!(output.runtime().contains(std::env::consts::OS)); + assert!(output.runtime().contains(std::env::consts::ARCH)); +} + +pub fn client() -> Client { + let config = LanguageSpecificLogicConfig::builder().build().unwrap(); + Client::from_conf(config).unwrap() +} diff --git a/TestModels/LanguageSpecificLogic/src/replaces/rust/Index.dfy b/TestModels/LanguageSpecificLogic/src/replaces/rust/Index.dfy new file mode 100644 index 000000000..0c454c4bf --- /dev/null +++ b/TestModels/LanguageSpecificLogic/src/replaces/rust/Index.dfy @@ -0,0 +1,8 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 + +// Include generic Index, which is the root of generic Dafny code +include "../../Index.dfy" + +// Include Rust-specific replacements +include "LanguageSpecificLogicImpl.dfy" diff --git a/TestModels/LanguageSpecificLogic/src/replaces/rust/LanguageSpecificLogicImpl.dfy b/TestModels/LanguageSpecificLogic/src/replaces/rust/LanguageSpecificLogicImpl.dfy new file mode 100644 index 000000000..1402f4464 --- /dev/null +++ b/TestModels/LanguageSpecificLogic/src/replaces/rust/LanguageSpecificLogicImpl.dfy @@ -0,0 +1,32 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +include "../../LanguageSpecificLogicImpl.dfy" + +module RustLanguageSpecificLogicImpl replaces LanguageSpecificLogicImpl { + // This method is listed as an operation on the service in the Smithy model. + // Smithy-Dafny will write code to call this operation. + // Internally, the generated Dafny will call the extern. + // This provides a consistent interface for users. + method GetRuntimeInformation(config: InternalConfig) + returns (output: Result) + ensures output.Success? ==> + && output.value.language == "Rust" + && output.value.runtime != "" + { + var runtimeInfo :- expect GetRuntimeInformationRustExternMethod(config); + var getRuntimeInformationOutput := GetRuntimeInformationOutput( + language := "Rust", + runtime := runtimeInfo + ); + return Success(getRuntimeInformationOutput); + } + + // This method is NOT listed as an operation on the service in the Smithy model. + // Since this is an extern method with a different name per language, we can't define + // the interface for this method on the Smithy model. + // Instead, we define the `AllRuntimesMethod` which IS a Smithy operation + // and call this method from there. + method {:extern "GetRustRuntimeVersion"} GetRuntimeInformationRustExternMethod(config: InternalConfig) + returns (output: Result) + ensures output.Success? ==> output.value != "" +} diff --git a/TestModels/LanguageSpecificLogic/test/replaces/rust/Index.dfy b/TestModels/LanguageSpecificLogic/test/replaces/rust/Index.dfy new file mode 100644 index 000000000..b7059076a --- /dev/null +++ b/TestModels/LanguageSpecificLogic/test/replaces/rust/Index.dfy @@ -0,0 +1,9 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 + +// No generic test Index to include + +// Include Rust-specific replacements +include "../../../src/WrappedLanguageSpecificLogicImpl.dfy" +include "LanguageSpecificLogicImplTest.dfy" +include "WrappedLanguageSpecificLogicImplTest.dfy" diff --git a/TestModels/LanguageSpecificLogic/test/replaces/rust/LanguageSpecificLogicImplTest.dfy b/TestModels/LanguageSpecificLogic/test/replaces/rust/LanguageSpecificLogicImplTest.dfy new file mode 100644 index 000000000..7aa3655b6 --- /dev/null +++ b/TestModels/LanguageSpecificLogic/test/replaces/rust/LanguageSpecificLogicImplTest.dfy @@ -0,0 +1,28 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +include "Index.dfy" + +// Note that by replacing a `replaceable` module, this file will also run tests from that module. +module RustLanguageSpecificLogicImplTest replaces LanguageSpecificLogicImplTest { + + method {:test} RustSpecificTests() { + var client :- expect LanguageSpecificLogic.LanguageSpecificLogic(); + TestRustClient(client); + } + + method TestRustClient(client: ILanguageSpecificLogicClient) + requires client.ValidState() + modifies client.Modifies + ensures client.ValidState() + { + var output := client.GetRuntimeInformation(); + expect output.Success?; + // For Rust-only tests, we can assert the output language is Rust + expect output.value.language == "Rust"; + // We could also assert some result on the extern's result (i.e. runtime version), but won't + + // We should ONLY see printed values like "Rust language: Rust". + // We should ALSO see printed values like "Generic language: Rust" from the `replaceable` tests. + print "Rust language: ", output.value.language, "; Rust runtime: ", output.value.runtime, "\n"; + } +} diff --git a/TestModels/LanguageSpecificLogic/test/replaces/rust/WrappedLanguageSpecificLogicImplTest.dfy b/TestModels/LanguageSpecificLogic/test/replaces/rust/WrappedLanguageSpecificLogicImplTest.dfy new file mode 100644 index 000000000..b642b881c --- /dev/null +++ b/TestModels/LanguageSpecificLogic/test/replaces/rust/WrappedLanguageSpecificLogicImplTest.dfy @@ -0,0 +1,15 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +include "../../../src/WrappedLanguageSpecificLogicImpl.dfy" +include "../../WrappedLanguageSpecificLogicImplTest.dfy" +include "LanguageSpecificLogicImplTest.dfy" + +// Note that by replacing a `replaceable` module, this file will also run tests from that module. +module RustLanguageSpecificLogicTest replaces WrappedLanguageSpecificLogicTest { + import RustLanguageSpecificLogicImplTest + + method{:test} WrappedRustOnlyTests() { + var client :- expect WrappedLanguageSpecificLogicService.WrappedLanguageSpecificLogic(); + RustLanguageSpecificLogicImplTest.TestRustClient(client); + } +} diff --git a/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithyrust/RustTestModels.java b/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithyrust/RustTestModels.java index dde434c00..8e07e1b8f 100644 --- a/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithyrust/RustTestModels.java +++ b/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithyrust/RustTestModels.java @@ -24,7 +24,6 @@ class RustTestModels extends TestModelTest { DISABLED_TESTS.add("Errors"); DISABLED_TESTS.add("Extendable"); DISABLED_TESTS.add("Extern"); - DISABLED_TESTS.add("LanguageSpecificLogic"); DISABLED_TESTS.add("LocalService"); DISABLED_TESTS.add("MultipleModels"); DISABLED_TESTS.add("Positional");