-
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.
feat: Rust codegen for Constraints (#582)
*Issue #, if available:* #533 *Description of changes:* This PR implements Rust library codegen for input validation of supported constraint traits (`@required`, `@length`, `@range`). Notes: * Unlike in Java and C#, library users may directly construct the generated operation input structures in Rust (in order to aid in idiomatic usage, especially w.r.t. pattern matching, like the AWS SDK for Rust does) and are not restricted to using the builder pattern. Therefore, the builder can't take sole responsibility for validation; instead, validation happens whenever an operation is called. * Unlike other target languages, Rust is limited in its ability to propagate arbitrary errors up the call stack unless the API is designed for doing so. Our models don't define a specific error shape for validation, so in order to represent validation errors in the generated `Error` enum, we generate a `ValidationError` variant that only exists on the Rust side. When converting to Dafny, we upcast the error into the `Opaque` variant; when converting from Dafny, we downcast it back after checking that doing so is safe using `dafny_runtime::is_object!`. * By Polymorph's design, values crossing the boundary from Dafny-compiled code are assumed to be "valid", but the `WrappedSimpleConstraintsTest` intentionally breaks this assumption in order to test the constraint validation logic, forcing invalid values across the boundary by (ab)using `{:axiom}`. This would be okay except that the Dafny tests in the Constraints test model *also* pass across malformed UTF-8 for `@DafnyUtf8Bytes` strings (which is not a constraint trait). The Rust type conversion process does not allow for failure when converting values from Dafny (doing so would be a major refactor and probably some performance impact), so I've isolated the malformed UTF-8 test assertions and used a bit of `sed` to simply disable them for Rust specifically, while allowing the other languages to continue testing them.
- Loading branch information
Showing
40 changed files
with
3,162 additions
and
50 deletions.
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
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -5,6 +5,8 @@ CORES=2 | |
|
||
ENABLE_EXTERN_PROCESSING=1 | ||
|
||
TRANSPILE_TESTS_IN_RUST=1 | ||
|
||
include ../SharedMakefile.mk | ||
|
||
PROJECT_SERVICES := \ | ||
|
@@ -19,13 +21,19 @@ SMITHY_DEPS=dafny-dependencies/Model/traits.smithy | |
# This project has no dependencies | ||
# DEPENDENT-MODELS:= | ||
|
||
# First, export DAFNY_VERSION=4.2 | ||
# Three separate items, because 'make polymorph_code_gen' doesn't quite work | ||
polymorph: | ||
npm i --no-save prettier@3 [email protected] | ||
make polymorph_dafny | ||
make polymorph_java | ||
make polymorph_dotnet | ||
clean: _clean | ||
rm -rf $(LIBRARY_ROOT)/runtimes/java/src/main/dafny-generated | ||
rm -rf $(LIBRARY_ROOT)/runtimes/java/src/main/smithy-generated | ||
rm -rf $(LIBRARY_ROOT)/runtimes/java/src/test/dafny-generated | ||
|
||
# Patch out tests that Rust codegen doesn't support | ||
transpile_rust: | transpile_implementation_rust transpile_dependencies_rust remove_unsupported_rust_tests | ||
|
||
remove_unsupported_rust_tests: | ||
$(MAKE) _sed_file \ | ||
SED_FILE_PATH=$(LIBRARY_ROOT)/runtimes/rust/src/implementation_from_dafny.rs \ | ||
SED_BEFORE_STRING='let mut allowBadUtf8BytesFromDafny: bool = true' \ | ||
SED_AFTER_STRING='let mut allowBadUtf8BytesFromDafny: bool = false' | ||
|
||
# Python | ||
|
||
|
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,25 @@ | ||
[package] | ||
name = "simple_constraints" | ||
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.7.1", features=["client"]} | ||
aws-smithy-runtime-api = {version = "1.7.2", features=["client"]} | ||
aws-smithy-types = "1.2.4" | ||
dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust"} | ||
|
||
[dependencies.tokio] | ||
version = "1.26.0" | ||
features = ["full"] | ||
|
||
[dev-dependencies] | ||
simple_constraints = { path = ".", features = ["wrapped-client"] } | ||
|
||
[lib] | ||
path = "src/implementation_from_dafny.rs" |
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,38 @@ | ||
// 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. | ||
use aws_smithy_types::error::operation::BuildError; | ||
|
||
#[derive(::std::clone::Clone, ::std::fmt::Debug, ::std::cmp::PartialEq)] | ||
pub struct Client { | ||
pub(crate) dafny_client: ::dafny_runtime::Object<dyn crate::r#simple::constraints::internaldafny::types::ISimpleConstraintsClient> | ||
} | ||
|
||
impl Client { | ||
/// Creates a new client from the service [`Config`](crate::Config). | ||
#[track_caller] | ||
pub fn from_conf( | ||
conf: crate::types::simple_constraints_config::SimpleConstraintsConfig, | ||
) -> Result<Self, BuildError> { | ||
let inner = | ||
crate::simple::constraints::internaldafny::_default::SimpleConstraints( | ||
&crate::conversions::simple_constraints_config::_simple_constraints_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_constraints; |
49 changes: 49 additions & 0 deletions
49
TestModels/Constraints/runtimes/rust/src/client/get_constraints.rs
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,49 @@ | ||
// 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. | ||
impl crate::client::Client { | ||
/// Constructs a fluent builder for the [`GetConstraints`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder) operation. | ||
/// | ||
/// - The fluent builder is configurable: | ||
/// - [`blob_less_than_or_equal_to_ten(impl Into<Option<::aws_smithy_types::Blob>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::blob_less_than_or_equal_to_ten) / [`set_blob_less_than_or_equal_to_ten(Option<::aws_smithy_types::Blob>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::set_blob_less_than_or_equal_to_ten): (undocumented)<br> | ||
/// - [`greater_than_one(impl Into<Option<::std::primitive::i32>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::greater_than_one) / [`set_greater_than_one(Option<::std::primitive::i32>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::set_greater_than_one): (undocumented)<br> | ||
/// - [`less_than_ten(impl Into<Option<::std::primitive::i32>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::less_than_ten) / [`set_less_than_ten(Option<::std::primitive::i32>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::set_less_than_ten): (undocumented)<br> | ||
/// - [`list_less_than_or_equal_to_ten(impl Into<Option<::std::vec::Vec<::std::string::String>>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::list_less_than_or_equal_to_ten) / [`set_list_less_than_or_equal_to_ten(Option<::std::vec::Vec<::std::string::String>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::set_list_less_than_or_equal_to_ten): (undocumented)<br> | ||
/// - [`map_less_than_or_equal_to_ten(impl Into<Option<::std::collections::HashMap<::std::string::String, ::std::string::String>>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::map_less_than_or_equal_to_ten) / [`set_map_less_than_or_equal_to_ten(Option<::std::collections::HashMap<::std::string::String, ::std::string::String>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::set_map_less_than_or_equal_to_ten): (undocumented)<br> | ||
/// - [`my_blob(impl Into<Option<::aws_smithy_types::Blob>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::my_blob) / [`set_my_blob(Option<::aws_smithy_types::Blob>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::set_my_blob): (undocumented)<br> | ||
/// - [`my_list(impl Into<Option<::std::vec::Vec<::std::string::String>>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::my_list) / [`set_my_list(Option<::std::vec::Vec<::std::string::String>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::set_my_list): (undocumented)<br> | ||
/// - [`my_list_of_utf8_bytes(impl Into<Option<::std::vec::Vec<::std::string::String>>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::my_list_of_utf8_bytes) / [`set_my_list_of_utf8_bytes(Option<::std::vec::Vec<::std::string::String>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::set_my_list_of_utf8_bytes): (undocumented)<br> | ||
/// - [`my_map(impl Into<Option<::std::collections::HashMap<::std::string::String, ::std::string::String>>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::my_map) / [`set_my_map(Option<::std::collections::HashMap<::std::string::String, ::std::string::String>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::set_my_map): (undocumented)<br> | ||
/// - [`my_string(impl Into<Option<::std::string::String>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::my_string) / [`set_my_string(Option<::std::string::String>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::set_my_string): (undocumented)<br> | ||
/// - [`my_utf8_bytes(impl Into<Option<::std::string::String>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::my_utf8_bytes) / [`set_my_utf8_bytes(Option<::std::string::String>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::set_my_utf8_bytes): (undocumented)<br> | ||
/// - [`non_empty_blob(impl Into<Option<::aws_smithy_types::Blob>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::non_empty_blob) / [`set_non_empty_blob(Option<::aws_smithy_types::Blob>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::set_non_empty_blob): (undocumented)<br> | ||
/// - [`non_empty_list(impl Into<Option<::std::vec::Vec<::std::string::String>>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::non_empty_list) / [`set_non_empty_list(Option<::std::vec::Vec<::std::string::String>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::set_non_empty_list): (undocumented)<br> | ||
/// - [`non_empty_map(impl Into<Option<::std::collections::HashMap<::std::string::String, ::std::string::String>>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::non_empty_map) / [`set_non_empty_map(Option<::std::collections::HashMap<::std::string::String, ::std::string::String>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::set_non_empty_map): (undocumented)<br> | ||
/// - [`non_empty_string(impl Into<Option<::std::string::String>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::non_empty_string) / [`set_non_empty_string(Option<::std::string::String>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::set_non_empty_string): (undocumented)<br> | ||
/// - [`one_to_ten(impl Into<Option<::std::primitive::i32>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::one_to_ten) / [`set_one_to_ten(Option<::std::primitive::i32>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::set_one_to_ten): (undocumented)<br> | ||
/// - [`string_less_than_or_equal_to_ten(impl Into<Option<::std::string::String>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::string_less_than_or_equal_to_ten) / [`set_string_less_than_or_equal_to_ten(Option<::std::string::String>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::set_string_less_than_or_equal_to_ten): (undocumented)<br> | ||
/// - [`my_ten_to_ten(impl Into<Option<::std::primitive::i64>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::my_ten_to_ten) / [`set_my_ten_to_ten(Option<::std::primitive::i64>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::set_my_ten_to_ten): (undocumented)<br> | ||
/// - On success, responds with [`GetConstraintsOutput`](crate::operation::get_constraints::GetConstraintsOutput) with field(s): | ||
/// - [`blob_less_than_or_equal_to_ten(Option<::aws_smithy_types::Blob>)`](crate::operation::get_constraints::GetConstraintsOutput::blob_less_than_or_equal_to_ten): (undocumented) | ||
/// - [`greater_than_one(Option<::std::primitive::i32>)`](crate::operation::get_constraints::GetConstraintsOutput::greater_than_one): (undocumented) | ||
/// - [`less_than_ten(Option<::std::primitive::i32>)`](crate::operation::get_constraints::GetConstraintsOutput::less_than_ten): (undocumented) | ||
/// - [`list_less_than_or_equal_to_ten(Option<::std::vec::Vec<::std::string::String>>)`](crate::operation::get_constraints::GetConstraintsOutput::list_less_than_or_equal_to_ten): (undocumented) | ||
/// - [`map_less_than_or_equal_to_ten(Option<::std::collections::HashMap<::std::string::String, ::std::string::String>>)`](crate::operation::get_constraints::GetConstraintsOutput::map_less_than_or_equal_to_ten): (undocumented) | ||
/// - [`my_blob(Option<::aws_smithy_types::Blob>)`](crate::operation::get_constraints::GetConstraintsOutput::my_blob): (undocumented) | ||
/// - [`my_list(Option<::std::vec::Vec<::std::string::String>>)`](crate::operation::get_constraints::GetConstraintsOutput::my_list): (undocumented) | ||
/// - [`my_list_of_utf8_bytes(Option<::std::vec::Vec<::std::string::String>>)`](crate::operation::get_constraints::GetConstraintsOutput::my_list_of_utf8_bytes): (undocumented) | ||
/// - [`my_map(Option<::std::collections::HashMap<::std::string::String, ::std::string::String>>)`](crate::operation::get_constraints::GetConstraintsOutput::my_map): (undocumented) | ||
/// - [`my_string(Option<::std::string::String>)`](crate::operation::get_constraints::GetConstraintsOutput::my_string): (undocumented) | ||
/// - [`my_utf8_bytes(Option<::std::string::String>)`](crate::operation::get_constraints::GetConstraintsOutput::my_utf8_bytes): (undocumented) | ||
/// - [`non_empty_blob(Option<::aws_smithy_types::Blob>)`](crate::operation::get_constraints::GetConstraintsOutput::non_empty_blob): (undocumented) | ||
/// - [`non_empty_list(Option<::std::vec::Vec<::std::string::String>>)`](crate::operation::get_constraints::GetConstraintsOutput::non_empty_list): (undocumented) | ||
/// - [`non_empty_map(Option<::std::collections::HashMap<::std::string::String, ::std::string::String>>)`](crate::operation::get_constraints::GetConstraintsOutput::non_empty_map): (undocumented) | ||
/// - [`non_empty_string(Option<::std::string::String>)`](crate::operation::get_constraints::GetConstraintsOutput::non_empty_string): (undocumented) | ||
/// - [`one_to_ten(Option<::std::primitive::i32>)`](crate::operation::get_constraints::GetConstraintsOutput::one_to_ten): (undocumented) | ||
/// - [`string_less_than_or_equal_to_ten(Option<::std::string::String>)`](crate::operation::get_constraints::GetConstraintsOutput::string_less_than_or_equal_to_ten): (undocumented) | ||
/// - [`that_ten_to_ten(Option<::std::primitive::i64>)`](crate::operation::get_constraints::GetConstraintsOutput::that_ten_to_ten): (undocumented) | ||
/// - On failure, responds with [`SdkError<GetConstraintsError>`](crate::operation::get_constraints::GetConstraintsError) | ||
pub fn get_constraints(&self) -> crate::operation::get_constraints::builders::GetConstraintsFluentBuilder { | ||
crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::new(self.clone()) | ||
} | ||
} |
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,10 @@ | ||
// 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. | ||
pub mod client; | ||
|
||
pub mod error; | ||
|
||
pub mod get_constraints; | ||
|
||
pub mod simple_constraints_config; |
24 changes: 24 additions & 0 deletions
24
TestModels/Constraints/runtimes/rust/src/conversions/client.rs
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,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. | ||
// 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::client::Client, | ||
) -> | ||
::dafny_runtime::Object<dyn crate::r#simple::constraints::internaldafny::types::ISimpleConstraintsClient> | ||
{ | ||
value.dafny_client.clone() | ||
} | ||
|
||
#[allow(dead_code)] | ||
pub fn from_dafny( | ||
dafny_value: ::dafny_runtime::Object< | ||
dyn crate::r#simple::constraints::internaldafny::types::ISimpleConstraintsClient | ||
>, | ||
) -> crate::client::Client { | ||
crate::client::Client { dafny_client: dafny_value } | ||
} |
99 changes: 99 additions & 0 deletions
99
TestModels/Constraints/runtimes/rust/src/conversions/error.rs
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,99 @@ | ||
// 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. | ||
/// Wraps up an arbitrary Rust Error value as a Dafny Error | ||
pub fn to_opaque_error<E: 'static>(value: E) -> | ||
::std::rc::Rc<crate::r#simple::constraints::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#simple::constraints::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: 'static>(value: E) -> | ||
::std::rc::Rc< | ||
crate::_Wrappers_Compile::Result< | ||
T, | ||
::std::rc::Rc<crate::r#simple::constraints::internaldafny::types::Error> | ||
> | ||
> | ||
{ | ||
::std::rc::Rc::new(crate::_Wrappers_Compile::Result::Failure { | ||
error: to_opaque_error(value), | ||
}) | ||
} | ||
pub fn to_dafny( | ||
value: crate::types::error::Error, | ||
) -> ::std::rc::Rc<crate::r#simple::constraints::internaldafny::types::Error> { | ||
::std::rc::Rc::new(match value { | ||
crate::types::error::Error::SimpleConstraintsException { message } => | ||
crate::r#simple::constraints::internaldafny::types::Error::SimpleConstraintsException { | ||
message: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&message), | ||
}, | ||
crate::types::error::Error::CollectionOfErrors { list, message } => | ||
crate::r#simple::constraints::internaldafny::types::Error::CollectionOfErrors { | ||
message: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&message), | ||
list: ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(&list, |e| to_dafny(e.clone())) | ||
}, | ||
crate::types::error::Error::ValidationError(inner) => | ||
crate::r#simple::constraints::internaldafny::types::Error::Opaque { | ||
obj: { | ||
let rc = ::std::rc::Rc::new(inner) as ::std::rc::Rc<dyn ::std::any::Any>; | ||
// safety: `rc` is new, ensuring it has refcount 1 and is uniquely owned. | ||
// we should use `dafny_runtime_conversions::rc_struct_to_dafny_class` once it | ||
// accepts unsized types (https://github.com/dafny-lang/dafny/pull/5769) | ||
unsafe { ::dafny_runtime::Object::from_rc(rc) } | ||
}, | ||
}, | ||
crate::types::error::Error::Opaque { obj } => | ||
crate::r#simple::constraints::internaldafny::types::Error::Opaque { | ||
obj: ::dafny_runtime::Object(obj.0) | ||
}, | ||
}) | ||
} | ||
|
||
#[allow(dead_code)] | ||
pub fn from_dafny( | ||
dafny_value: ::std::rc::Rc< | ||
crate::r#simple::constraints::internaldafny::types::Error, | ||
>, | ||
) -> crate::types::error::Error { | ||
match ::std::borrow::Borrow::borrow(&dafny_value) { | ||
crate::r#simple::constraints::internaldafny::types::Error::SimpleConstraintsException { message } => | ||
crate::types::error::Error::SimpleConstraintsException { | ||
message: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(&message), | ||
}, | ||
crate::r#simple::constraints::internaldafny::types::Error::CollectionOfErrors { list, message } => | ||
crate::types::error::Error::CollectionOfErrors { | ||
message: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(&message), | ||
list: ::dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(&list, |e| from_dafny(e.clone())) | ||
}, | ||
crate::r#simple::constraints::internaldafny::types::Error::Opaque { obj } => | ||
crate::types::error::Error::Opaque { | ||
obj: obj.clone() | ||
}, | ||
crate::r#simple::constraints::internaldafny::types::Error::Opaque { obj } => | ||
{ | ||
use ::std::any::Any; | ||
if ::dafny_runtime::is_object!(obj, crate::types::error::ValidationError) { | ||
let typed = ::dafny_runtime::cast_object!(obj.clone(), crate::types::error::ValidationError); | ||
crate::types::error::Error::ValidationError( | ||
// safety: dafny_class_to_struct will increment ValidationError's Rc | ||
unsafe { | ||
::dafny_runtime::dafny_runtime_conversions::object::dafny_class_to_struct(typed) | ||
} | ||
) | ||
} else { | ||
crate::types::error::Error::Opaque { | ||
obj: obj.clone() | ||
} | ||
} | ||
}, | ||
} | ||
} |
Oops, something went wrong.