Skip to content

Commit

Permalink
feat: benerate LanguageSpecificLogic for Rust (#507)
Browse files Browse the repository at this point in the history
  • Loading branch information
alex-chew authored Aug 22, 2024
1 parent 80df331 commit 91e1a94
Show file tree
Hide file tree
Showing 31 changed files with 1,046 additions and 20 deletions.
6 changes: 6 additions & 0 deletions TestModels/LanguageSpecificLogic/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,8 @@

CORES=2

RUST_BENERATED=1

include ../SharedMakefile.mk

PROJECT_SERVICES := \
Expand All @@ -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:=
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -8,24 +8,25 @@

namespace NetLanguageSpecificLogicImpl_Compile
{
public partial class __default
{
public static
Wrappers_Compile._IResult<
Dafny.ISequence<char>,
language.specific.logic.internaldafny.types._IError
>
GetNetRuntimeVersion (
NetLanguageSpecificLogicImpl_Compile._IConfig config
) {
return Wrappers_Compile.Result<
Dafny.ISequence<char>,
language.specific.logic.internaldafny.types._IError
>.create_Success(
Dafny.Sequence<char>.FromString(
System.Environment.Version.ToString()
public partial class __default
{
public static
Wrappers_Compile._IResult<
Dafny.ISequence<char>,
language.specific.logic.internaldafny.types._IError
>
GetNetRuntimeVersion(
NetLanguageSpecificLogicImpl_Compile._IConfig config
)
);
}
}
{
return Wrappers_Compile.Result<
Dafny.ISequence<char>,
language.specific.logic.internaldafny.types._IError
>.create_Success(
Dafny.Sequence<char>.FromString(
System.Environment.Version.ToString()
)
);
}
}
}
25 changes: 25 additions & 0 deletions TestModels/LanguageSpecificLogic/runtimes/rust/Cargo.toml
Original file line number Diff line number Diff line change
@@ -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"
39 changes: 39 additions & 0 deletions TestModels/LanguageSpecificLogic/runtimes/rust/src/client.rs
Original file line number Diff line number Diff line change
@@ -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<dyn crate::r#language::specific::logic::internaldafny::types::ILanguageSpecificLogicClient>
}

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<Self, BuildError> {
// 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;
Original file line number Diff line number Diff line change
@@ -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<GetRuntimeInformationError>`](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())
}
}
Original file line number Diff line number Diff line change
@@ -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;
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
/// 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::r#language::specific::logic::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::r#language::specific::logic::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::r#language::specific::logic::internaldafny::types::Error>
>
>
{
::std::rc::Rc::new(
crate::_Wrappers_Compile::Result::Failure {
error: to_opaque_error(value)
}
)
}
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_runtime_information::GetRuntimeInformationError,
) -> ::std::rc::Rc<crate::r#language::specific::logic::internaldafny::types::Error>
{
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;
Original file line number Diff line number Diff line change
@@ -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::r#language::specific::logic::internaldafny::types::GetRuntimeInformationOutput>,
) -> 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,
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT.

pub mod _language_specific_logic_config;
Original file line number Diff line number Diff line change
@@ -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 {}
}
14 changes: 14 additions & 0 deletions TestModels/LanguageSpecificLogic/runtimes/rust/src/error.rs
Original file line number Diff line number Diff line change
@@ -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<E, R = ::aws_smithy_runtime_api::client::orchestrator::HttpResponse> =
::aws_smithy_runtime_api::client::result::SdkError<E, R>;
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;
Original file line number Diff line number Diff line change
@@ -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()`:
\
&nbsp;&nbsp;&nbsp;`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<dyn ::std::any::Any> for Unhandled {
::dafny_runtime::UpcastObjectFn!(dyn ::std::any::Any);
}
24 changes: 24 additions & 0 deletions TestModels/LanguageSpecificLogic/runtimes/rust/src/externs.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
#![allow(warnings, unconditional_panic)]
#![allow(nonstandard_style)]

impl crate::r#_LanguageSpecificLogicImpl_Compile::_default {
pub fn GetRustRuntimeVersion(
config: &::std::rc::Rc<crate::r#_LanguageSpecificLogicImpl_Compile::Config>,
) -> ::std::rc::Rc<
crate::r#_Wrappers_Compile::Result<
::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>,
::std::rc::Rc<crate::r#language::specific::logic::internaldafny::types::Error>,
>,
> {
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)
}
}
24 changes: 24 additions & 0 deletions TestModels/LanguageSpecificLogic/runtimes/rust/src/lib.rs
Original file line number Diff line number Diff line change
@@ -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;
Original file line number Diff line number Diff line change
@@ -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;
Loading

0 comments on commit 91e1a94

Please sign in to comment.