diff --git a/.github/workflows/pull.yml b/.github/workflows/pull.yml index cb26671d21..168a2d1e80 100644 --- a/.github/workflows/pull.yml +++ b/.github/workflows/pull.yml @@ -53,7 +53,7 @@ jobs: # Rust code generation is under development and depends on pending changes to the # Dafny Rust code generation, so we test on a specific unreleased commit instead. dafny-version: - - 5f2330113320f2af0476473fd267b5b547f94cba + - d07403b6d6606257e1b5aada4d0156901f4a17de uses: ./.github/workflows/test_models_rust_tests.yml with: dafny: ${{ matrix.dafny-version }} diff --git a/SmithyDafnyMakefile.mk b/SmithyDafnyMakefile.mk index 8027e465fa..eb8a0d0315 100644 --- a/SmithyDafnyMakefile.mk +++ b/SmithyDafnyMakefile.mk @@ -193,6 +193,7 @@ transpile_implementation: SRC_INDEX_TRANSPILE=$(if $(SRC_INDEX),$(SRC_INDEX),src # Also the expectation is that verification happens in the `verify` target # `find` looks for `Index.dfy` files in either V1 or V2-styled project directories (single vs. multiple model files). transpile_implementation: + dafny --version find ./dafny/**/$(SRC_INDEX_TRANSPILE)/ ./$(SRC_INDEX_TRANSPILE)/ -name 'Index.dfy' | sed -e 's/^/include "/' -e 's/$$/"/' | dafny \ translate $(TARGET) \ --stdin \ @@ -231,6 +232,7 @@ _transpile_test_all: TRANSPILE_DEPENDENCIES=$(if ${DIR_STRUCTURE_V2}, $(patsubst _transpile_test_all: transpile_test transpile_test: + dafny --version find ./dafny/**/$(TEST_INDEX_TRANSPILE) ./$(TEST_INDEX_TRANSPILE) -name "*.dfy" -name '*.dfy' | sed -e 's/^/include "/' -e 's/$$/"/' | dafny \ translate $(TARGET) \ --stdin \ @@ -609,7 +611,7 @@ transpile_implementation_rust: SRC_INDEX=$(RUST_SRC_INDEX) transpile_implementation_rust: TEST_INDEX=$(RUST_TEST_INDEX) # The Dafny Rust code generator is not complete yet, # so we want to emit code even if there are unsupported features in the input. -transpile_implementation_rust: DAFNY_OPTIONS=--emit-uncompilable-code --allow-warnings --compile-suffix --rust-module-name implementation_from_dafny +transpile_implementation_rust: DAFNY_OPTIONS=--emit-uncompilable-code --allow-warnings --compile-suffix --rust-module-name implementation_from_dafny --rust-sync # The Dafny Rust code generator only supports a single crate for everything, # so we inline all dependencies by not passing `-library` to Dafny. transpile_implementation_rust: TRANSPILE_DEPENDENCIES= @@ -629,7 +631,7 @@ _mv_implementation_rust: # Pre-process the Dafny-generated Rust code to remove them. sed -i -e 's/[[:space:]]*$$//' runtimes/rust/src/implementation_from_dafny.rs rm -f runtimes/rust/src/implementation_from_dafny.rs-e - rustfmt --edition 2021 runtimes/rust/src/implementation_from_dafny.rs +# rustfmt --edition 2021 runtimes/rust/src/implementation_from_dafny.rs rm -rf implementation_from_dafny-rust build_rust: @@ -637,6 +639,7 @@ build_rust: cargo build test_rust: + rustc --version cd runtimes/rust; \ cargo test --release -- --nocapture @@ -776,7 +779,7 @@ local_transpile_impl_rust_single: TARGET=rs local_transpile_impl_rust_single: OUT=implementation_from_dafny local_transpile_impl_rust_single: SRC_INDEX=$(RUST_SRC_INDEX) local_transpile_impl_rust_single: TEST_INDEX=$(RUST_TEST_INDEX) -local_transpile_impl_rust_single: DAFNY_OPTIONS=--emit-uncompilable-code --allow-warnings --compile-suffix +local_transpile_impl_rust_single: DAFNY_OPTIONS=--emit-uncompilable-code --allow-warnings --compile-suffix --rust-sync local_transpile_impl_rust_single: TRANSPILE_DEPENDENCIES= local_transpile_impl_rust_single: STD_LIBRARY= local_transpile_impl_rust_single: SRC_INDEX_TRANSPILE=$(if $(SRC_INDEX),$(SRC_INDEX),src) diff --git a/TestModels/.gitignore b/TestModels/.gitignore index 8815c7af98..b666081343 100644 --- a/TestModels/.gitignore +++ b/TestModels/.gitignore @@ -50,6 +50,9 @@ **/src/types.rs **/src/types **/target +**/src/validation.rs +**/src/wrapped +**/src/wrapped.rs # .NET Artifacts **/bin diff --git a/TestModels/Aggregate/runtimes/rust/Cargo.toml b/TestModels/Aggregate/runtimes/rust/Cargo.toml index 0f684f389e..cb99d3e296 100644 --- a/TestModels/Aggregate/runtimes/rust/Cargo.toml +++ b/TestModels/Aggregate/runtimes/rust/Cargo.toml @@ -12,7 +12,7 @@ wrapped-client = [] 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"} +dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]} [dev-dependencies] simple_aggregate = { path = ".", features = ["wrapped-client"] } diff --git a/TestModels/CallingAWSSDKFromLocalService/runtimes/rust/Cargo.toml b/TestModels/CallingAWSSDKFromLocalService/runtimes/rust/Cargo.toml index cfa67e9cdf..97fe552841 100644 --- a/TestModels/CallingAWSSDKFromLocalService/runtimes/rust/Cargo.toml +++ b/TestModels/CallingAWSSDKFromLocalService/runtimes/rust/Cargo.toml @@ -13,7 +13,7 @@ aws-config = "1.5.8" 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"} +dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]} aws-sdk-dynamodb = "1.50.0" aws-sdk-kms = "1.47.0" diff --git a/TestModels/CallingAWSSDKFromLocalService/runtimes/rust/src/ddb.rs b/TestModels/CallingAWSSDKFromLocalService/runtimes/rust/src/ddb.rs index bb9d259b09..d1cd3cc07d 100644 --- a/TestModels/CallingAWSSDKFromLocalService/runtimes/rust/src/ddb.rs +++ b/TestModels/CallingAWSSDKFromLocalService/runtimes/rust/src/ddb.rs @@ -17,10 +17,10 @@ static DAFNY_TOKIO_RUNTIME: LazyLock = LazyLock::new(|| #[allow(non_snake_case)] impl crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::_default { - pub fn DynamoDBClient() -> ::std::rc::Rc< + pub fn DynamoDBClient() -> ::dafny_runtime::Rc< crate::r#_Wrappers_Compile::Result< ::dafny_runtime::Object, - ::std::rc::Rc + ::dafny_runtime::Rc > >{ let shared_config = match tokio::runtime::Handle::try_current() { @@ -36,7 +36,7 @@ impl crate::r#software::amazon::cryptography::services::dynamodb::internaldafny: let inner = aws_sdk_dynamodb::Client::new(&shared_config); let client = crate::deps::com_amazonaws_dynamodb::client::Client { inner }; let dafny_client = ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(client)); - std::rc::Rc::new(crate::r#_Wrappers_Compile::Result::Success { + dafny_runtime::Rc::new(crate::r#_Wrappers_Compile::Result::Success { value: dafny_client, }) } diff --git a/TestModels/CallingAWSSDKFromLocalService/runtimes/rust/src/kms.rs b/TestModels/CallingAWSSDKFromLocalService/runtimes/rust/src/kms.rs index e672a5d866..5afc0721b9 100644 --- a/TestModels/CallingAWSSDKFromLocalService/runtimes/rust/src/kms.rs +++ b/TestModels/CallingAWSSDKFromLocalService/runtimes/rust/src/kms.rs @@ -17,7 +17,7 @@ static DAFNY_TOKIO_RUNTIME: LazyLock = LazyLock::new(|| impl crate::r#software::amazon::cryptography::services::kms::internaldafny::_default { #[allow(non_snake_case)] - pub fn KMSClient() -> ::std::rc::Rc, ::std::rc::Rc>>{ + pub fn KMSClient() -> ::dafny_runtime::Rc, ::dafny_runtime::Rc>>{ let shared_config = match tokio::runtime::Handle::try_current() { Ok(curr) => tokio::task::block_in_place(|| { curr.block_on(async { @@ -32,7 +32,7 @@ impl crate::r#software::amazon::cryptography::services::kms::internaldafny::_def let inner = aws_sdk_kms::Client::new(&shared_config); let client = crate::deps::com_amazonaws_kms::client::Client { inner }; let dafny_client = ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(client)); - std::rc::Rc::new(crate::r#_Wrappers_Compile::Result::Success { + dafny_runtime::Rc::new(crate::r#_Wrappers_Compile::Result::Success { value: dafny_client, }) } diff --git a/TestModels/CallingAWSSDKFromLocalService/runtimes/rust/src/lib.rs b/TestModels/CallingAWSSDKFromLocalService/runtimes/rust/src/lib.rs index 1fd5fcde26..20a547c769 100644 --- a/TestModels/CallingAWSSDKFromLocalService/runtimes/rust/src/lib.rs +++ b/TestModels/CallingAWSSDKFromLocalService/runtimes/rust/src/lib.rs @@ -1,9 +1,9 @@ #![allow( - deprecated, - non_upper_case_globals, - unused, - non_snake_case, - non_camel_case_types + deprecated, + non_upper_case_globals, + unused, + non_snake_case, + non_camel_case_types )] pub mod client; @@ -14,10 +14,10 @@ pub mod error; pub(crate) mod implementation_from_dafny; /// All operations that this crate can perform. pub mod operation; -pub mod validation; mod standard_library_conversions; mod standard_library_externs; pub mod types; +pub mod validation; pub mod wrapped; pub(crate) use crate::implementation_from_dafny::r#_Wrappers_Compile; pub(crate) use crate::implementation_from_dafny::simple; @@ -30,4 +30,4 @@ pub use crate::deps::com_amazonaws_kms; pub mod ddb; pub mod kms; -pub(crate) use crate::implementation_from_dafny::software; \ No newline at end of file +pub(crate) use crate::implementation_from_dafny::software; diff --git a/TestModels/Constraints/runtimes/rust/Cargo.toml b/TestModels/Constraints/runtimes/rust/Cargo.toml index bdd001675f..e8f9a61de6 100644 --- a/TestModels/Constraints/runtimes/rust/Cargo.toml +++ b/TestModels/Constraints/runtimes/rust/Cargo.toml @@ -12,7 +12,7 @@ wrapped-client = [] 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"} +dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]} [dependencies.tokio] version = "1.26.0" diff --git a/TestModels/Constructor/runtimes/rust/Cargo.toml b/TestModels/Constructor/runtimes/rust/Cargo.toml index 15e9e63917..7820e69b25 100644 --- a/TestModels/Constructor/runtimes/rust/Cargo.toml +++ b/TestModels/Constructor/runtimes/rust/Cargo.toml @@ -11,7 +11,7 @@ wrapped-client = [] [dependencies] aws-smithy-runtime-api = {version = "1.7.0", features = ["client"] } aws-smithy-types = "1.2.0" -dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust"} +dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]} [dev-dependencies] constructor = { path = ".", features = ["wrapped-client"] } diff --git a/TestModels/Dependencies/runtimes/rust/Cargo.toml b/TestModels/Dependencies/runtimes/rust/Cargo.toml index 2776afc748..7b77bb2bf0 100644 --- a/TestModels/Dependencies/runtimes/rust/Cargo.toml +++ b/TestModels/Dependencies/runtimes/rust/Cargo.toml @@ -11,7 +11,7 @@ wrapped-client = [] [dependencies] aws-smithy-runtime-api = {version = "1.7.0", features = ["client"] } aws-smithy-types = "1.2.0" -dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust"} +dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]} [dev-dependencies] dependencies = { path = ".", features = ["wrapped-client"] } diff --git a/TestModels/Documentation/runtimes/rust/Cargo.toml b/TestModels/Documentation/runtimes/rust/Cargo.toml index d221418757..5911289ff8 100644 --- a/TestModels/Documentation/runtimes/rust/Cargo.toml +++ b/TestModels/Documentation/runtimes/rust/Cargo.toml @@ -10,7 +10,7 @@ wrapped-client = [] 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"} +dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]} [dev-dependencies] documentation = { path = ".", features = ["wrapped-client"] } diff --git a/TestModels/Errors/runtimes/rust/Cargo.toml b/TestModels/Errors/runtimes/rust/Cargo.toml index 3f6cb79641..6a38c1c4b0 100644 --- a/TestModels/Errors/runtimes/rust/Cargo.toml +++ b/TestModels/Errors/runtimes/rust/Cargo.toml @@ -12,7 +12,7 @@ wrapped-client = [] 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"} +dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]} [dependencies.tokio] version = "1.26.0" diff --git a/TestModels/Extendable/runtimes/rust/Cargo.toml b/TestModels/Extendable/runtimes/rust/Cargo.toml index 971d9c32b7..49e0c4e9bf 100644 --- a/TestModels/Extendable/runtimes/rust/Cargo.toml +++ b/TestModels/Extendable/runtimes/rust/Cargo.toml @@ -12,7 +12,7 @@ wrapped-client = [] 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"} +dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]} [dependencies.tokio] version = "1.26.0" diff --git a/TestModels/Extendable/runtimes/rust/src/factory.rs b/TestModels/Extendable/runtimes/rust/src/factory.rs index 0d20aa7bba..fc00d77b36 100644 --- a/TestModels/Extendable/runtimes/rust/src/factory.rs +++ b/TestModels/Extendable/runtimes/rust/src/factory.rs @@ -12,7 +12,7 @@ use crate::simple::extendable::resources::internaldafny::types::GetExtendableRes use crate::simple::extendable::resources::internaldafny::types::GetExtendableResourceErrorsInput; use crate::simple::extendable::resources::internaldafny::types::GetExtendableResourceErrorsOutput; use crate::simple::extendable::resources::internaldafny::types::IExtendableResource; -use std::rc::Rc; +use ::dafny_runtime::Rc; pub mod simple { pub mod extendable { @@ -30,8 +30,8 @@ pub struct NativeResource { pub inner: Box, } -impl dafny_runtime::UpcastObject for NativeResource { - dafny_runtime::UpcastObjectFn!(dyn std::any::Any); +impl dafny_runtime::UpcastObject<::dafny_runtime::DynAny> for NativeResource { + dafny_runtime::UpcastObjectFn!(::dafny_runtime::DynAny); } impl IExtendableResource for NativeResource { diff --git a/TestModels/Extendable/runtimes/rust/src/lib.rs b/TestModels/Extendable/runtimes/rust/src/lib.rs index ea7fb7ae21..e5a936b914 100644 --- a/TestModels/Extendable/runtimes/rust/src/lib.rs +++ b/TestModels/Extendable/runtimes/rust/src/lib.rs @@ -11,15 +11,15 @@ pub mod conversions; pub mod deps; /// Common errors and error handling utilities. pub mod error; +pub mod factory; pub(crate) mod implementation_from_dafny; /// All operations that this crate can perform. pub mod operation; -pub mod validation; mod standard_library_conversions; mod standard_library_externs; pub mod types; +pub mod validation; pub mod wrapped; -pub mod factory; pub(crate) use crate::implementation_from_dafny::_SimpleExtendableResourcesTest_Compile; pub(crate) use crate::implementation_from_dafny::_WrappedTest_Compile; pub(crate) use crate::implementation_from_dafny::_Wrappers_Compile; diff --git a/TestModels/LanguageSpecificLogic/runtimes/rust/Cargo.toml b/TestModels/LanguageSpecificLogic/runtimes/rust/Cargo.toml index f3ceb0b316..7cd6e25e40 100644 --- a/TestModels/LanguageSpecificLogic/runtimes/rust/Cargo.toml +++ b/TestModels/LanguageSpecificLogic/runtimes/rust/Cargo.toml @@ -12,7 +12,7 @@ wrapped-client = [] 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"} +dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]} [dev-dependencies] language_specific_logic = { path = ".", features = ["wrapped-client"] } diff --git a/TestModels/LocalService/runtimes/rust/Cargo.toml b/TestModels/LocalService/runtimes/rust/Cargo.toml index 991a0123dd..3eb513fe55 100644 --- a/TestModels/LocalService/runtimes/rust/Cargo.toml +++ b/TestModels/LocalService/runtimes/rust/Cargo.toml @@ -12,7 +12,7 @@ wrapped-client = [] 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"} +dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]} [dev-dependencies] local_service = { path = ".", features = ["wrapped-client"] } diff --git a/TestModels/MultipleModels/runtimes/rust/Cargo.toml b/TestModels/MultipleModels/runtimes/rust/Cargo.toml index a7d0ccb300..1a59f4d89c 100644 --- a/TestModels/MultipleModels/runtimes/rust/Cargo.toml +++ b/TestModels/MultipleModels/runtimes/rust/Cargo.toml @@ -11,7 +11,7 @@ wrapped-client = [] [dependencies] aws-smithy-runtime-api = {version = "1.7.0", features = ["client"] } aws-smithy-types = "1.2.0" -dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust"} +dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]} [dev-dependencies] multiple_models = { path = ".", features = ["wrapped-client"] } diff --git a/TestModels/OrphanedShapes/runtimes/rust/Cargo.toml b/TestModels/OrphanedShapes/runtimes/rust/Cargo.toml index 45c7f4805a..ea69091908 100644 --- a/TestModels/OrphanedShapes/runtimes/rust/Cargo.toml +++ b/TestModels/OrphanedShapes/runtimes/rust/Cargo.toml @@ -12,7 +12,7 @@ wrapped-client = [] 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"} +dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]} [dev-dependencies] simple_orphaned = { path = ".", features = ["wrapped-client"] } diff --git a/TestModels/OrphanedShapes/runtimes/rust/src/extern_definitions.rs b/TestModels/OrphanedShapes/runtimes/rust/src/extern_definitions.rs index 0349a2b625..9952298288 100644 --- a/TestModels/OrphanedShapes/runtimes/rust/src/extern_definitions.rs +++ b/TestModels/OrphanedShapes/runtimes/rust/src/extern_definitions.rs @@ -3,8 +3,8 @@ use crate::r#_Wrappers_Compile::Result; use dafny_runtime::rcmut; +use dafny_runtime::Rc; use std::cell::UnsafeCell; -use std::rc::Rc; pub mod internal_ExternDefinitions_Compile { @@ -14,6 +14,7 @@ pub mod internal_ExternDefinitions_Compile { use crate::simple::orphaned::internaldafny::types as internaldafny_types; use crate::simple::orphaned::internaldafny::types::*; use crate::types::*; + use dafny_runtime::Rc; impl _default { pub fn InitializeOrphanedStructure( @@ -37,7 +38,7 @@ pub mod internal_ExternDefinitions_Compile { { let native_resource_ref = crate::conversions::orphaned_resource::from_dafny(dafny_resource.clone()); - let native_resource = native_resource_ref.inner.borrow(); + let native_resource = native_resource_ref.inner.lock().unwrap(); let native_output = native_resource.orphaned_resource_operation( crate::operation::orphaned_resource_operation::OrphanedResourceOperationInput { some_string: std::option::Option::Some( @@ -52,7 +53,7 @@ pub mod internal_ExternDefinitions_Compile { native_output.unwrap(), ); - ::std::rc::Rc::new(Result::< + Rc::new(Result::< Rc, Rc, >::Success { diff --git a/TestModels/Positional/runtimes/rust/Cargo.toml b/TestModels/Positional/runtimes/rust/Cargo.toml index 7c864483d7..469b789956 100644 --- a/TestModels/Positional/runtimes/rust/Cargo.toml +++ b/TestModels/Positional/runtimes/rust/Cargo.toml @@ -12,7 +12,7 @@ wrapped-client = [] 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"} +dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]} [dev-dependencies] positional = { path = ".", features = ["wrapped-client"] } diff --git a/TestModels/Refinement/runtimes/rust/Cargo.toml b/TestModels/Refinement/runtimes/rust/Cargo.toml index a5ad1fa617..8a3dd773ad 100644 --- a/TestModels/Refinement/runtimes/rust/Cargo.toml +++ b/TestModels/Refinement/runtimes/rust/Cargo.toml @@ -9,7 +9,7 @@ edition = "2021" 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"} +dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]} [dev-dependencies.tokio] version = "1.26.0" diff --git a/TestModels/Resource/runtimes/rust/Cargo.toml b/TestModels/Resource/runtimes/rust/Cargo.toml index 8024014a19..37af19388c 100644 --- a/TestModels/Resource/runtimes/rust/Cargo.toml +++ b/TestModels/Resource/runtimes/rust/Cargo.toml @@ -12,7 +12,7 @@ wrapped-client = [] 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"} +dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]} [dev-dependencies] simple_resources = { path = ".", features = ["wrapped-client"] } diff --git a/TestModels/Resource/runtimes/rust/src/lib.rs b/TestModels/Resource/runtimes/rust/src/lib.rs index 8465254ed1..d2c37cc33e 100644 --- a/TestModels/Resource/runtimes/rust/src/lib.rs +++ b/TestModels/Resource/runtimes/rust/src/lib.rs @@ -14,10 +14,10 @@ pub mod error; pub(crate) mod implementation_from_dafny; /// All operations that this crate can perform. pub mod operation; -pub mod validation; mod standard_library_conversions; mod standard_library_externs; pub mod types; +pub mod validation; pub mod wrapped; pub(crate) use crate::implementation_from_dafny::r#_Wrappers_Compile; pub(crate) use crate::implementation_from_dafny::simple; diff --git a/TestModels/Resource/runtimes/rust/tests/simple_resources_test.rs b/TestModels/Resource/runtimes/rust/tests/simple_resources_test.rs index 8ae2617c91..21844802f5 100644 --- a/TestModels/Resource/runtimes/rust/tests/simple_resources_test.rs +++ b/TestModels/Resource/runtimes/rust/tests/simple_resources_test.rs @@ -1,5 +1,5 @@ -use simple_resources::types::simple_resource::SimpleResourceRef; use simple_resources::operation::get_resource_data::*; +use simple_resources::types::simple_resource::SimpleResourceRef; use simple_resources::*; #[tokio::test] @@ -22,13 +22,23 @@ async fn TestClient(config: SimpleResourcesConfig) { async fn TestNoneGetData(config: SimpleResourcesConfig, resource: SimpleResourceRef) { let input = allNone(); - let result = resource.inner.borrow_mut().get_resource_data(input).unwrap(); + let result = resource + .inner + .lock() + .unwrap() + .get_resource_data(input) + .unwrap(); checkMostNone(config.name().clone().unwrap().to_string(), result); } async fn TestSomeGetData(config: SimpleResourcesConfig, resource: SimpleResourceRef) { let input: GetResourceDataInput = allSome(); - let result = resource.inner.borrow_mut().get_resource_data(input).unwrap(); + let result = resource + .inner + .lock() + .unwrap() + .get_resource_data(input) + .unwrap(); checkSome(config.name().clone().unwrap().to_string(), result); } @@ -67,7 +77,10 @@ pub fn allSome() -> GetResourceDataInput { pub fn checkSome(name: String, output: GetResourceDataOutput) { assert_eq!(Some(name + " Some"), *output.string_value()); - assert_eq!(Some(aws_smithy_types::Blob::new(vec![1u8])), *output.blob_value()); + assert_eq!( + Some(aws_smithy_types::Blob::new(vec![1u8])), + *output.blob_value() + ); assert_eq!(Some(true), *output.boolean_value()); assert_eq!(Some(1), *output.integer_value()); assert_eq!(Some(1), *output.long_value()); diff --git a/TestModels/SQSExtended/runtimes/rust/Cargo.toml b/TestModels/SQSExtended/runtimes/rust/Cargo.toml index 220a6a9516..17c5487473 100644 --- a/TestModels/SQSExtended/runtimes/rust/Cargo.toml +++ b/TestModels/SQSExtended/runtimes/rust/Cargo.toml @@ -15,7 +15,7 @@ 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" # TODO: Wrong path according to the tutorial instructions -dafny_runtime = { path = "../../../../../TestModels/dafny-dependencies/dafny_runtime_rust"} +dafny_runtime = { path = "../../../../../TestModels/dafny-dependencies/dafny_runtime_rust", features = ["sync"]} [dev-dependencies] extended_sqs = { path = ".", features = ["wrapped-client"] } diff --git a/TestModels/SimpleTypes/SimpleBlob/runtimes/rust/Cargo.toml b/TestModels/SimpleTypes/SimpleBlob/runtimes/rust/Cargo.toml index bc838b01c3..b55608e963 100644 --- a/TestModels/SimpleTypes/SimpleBlob/runtimes/rust/Cargo.toml +++ b/TestModels/SimpleTypes/SimpleBlob/runtimes/rust/Cargo.toml @@ -12,7 +12,7 @@ wrapped-client = [] 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"} +dafny_runtime = { path = "../../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]} [dev-dependencies] simple_blob = { path = ".", features = ["wrapped-client"] } diff --git a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/Cargo.toml b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/Cargo.toml index b421ec8d02..8e9d988fbb 100644 --- a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/Cargo.toml +++ b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/Cargo.toml @@ -12,7 +12,7 @@ wrapped-client = [] 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"} +dafny_runtime = { path = "../../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]} [dev-dependencies] simple_boolean = { path = ".", features = ["wrapped-client"] } diff --git a/TestModels/SimpleTypes/SimpleDouble/runtimes/rust/Cargo.toml b/TestModels/SimpleTypes/SimpleDouble/runtimes/rust/Cargo.toml index db596c69e9..ffcf3ac489 100644 --- a/TestModels/SimpleTypes/SimpleDouble/runtimes/rust/Cargo.toml +++ b/TestModels/SimpleTypes/SimpleDouble/runtimes/rust/Cargo.toml @@ -12,7 +12,7 @@ wrapped-client = [] 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"} +dafny_runtime = { path = "../../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]} [dev-dependencies] simple_double = { path = ".", features = ["wrapped-client"] } diff --git a/TestModels/SimpleTypes/SimpleEnum/runtimes/rust/Cargo.toml b/TestModels/SimpleTypes/SimpleEnum/runtimes/rust/Cargo.toml index 123efbd25c..4fd1d43b88 100644 --- a/TestModels/SimpleTypes/SimpleEnum/runtimes/rust/Cargo.toml +++ b/TestModels/SimpleTypes/SimpleEnum/runtimes/rust/Cargo.toml @@ -12,7 +12,7 @@ wrapped-client = [] 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"} +dafny_runtime = { path = "../../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]} [dev-dependencies] simple_enum = { path = ".", features = ["wrapped-client"] } diff --git a/TestModels/SimpleTypes/SimpleEnumV2/runtimes/rust/Cargo.toml b/TestModels/SimpleTypes/SimpleEnumV2/runtimes/rust/Cargo.toml index fe66c062a0..477a75f042 100644 --- a/TestModels/SimpleTypes/SimpleEnumV2/runtimes/rust/Cargo.toml +++ b/TestModels/SimpleTypes/SimpleEnumV2/runtimes/rust/Cargo.toml @@ -12,7 +12,7 @@ wrapped-client = [] 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"} +dafny_runtime = { path = "../../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]} [dev-dependencies] simple_enum_v2 = { path = ".", features = ["wrapped-client"] } diff --git a/TestModels/SimpleTypes/SimpleInteger/runtimes/rust/Cargo.toml b/TestModels/SimpleTypes/SimpleInteger/runtimes/rust/Cargo.toml index 66d31a3dee..a44c53ea6e 100644 --- a/TestModels/SimpleTypes/SimpleInteger/runtimes/rust/Cargo.toml +++ b/TestModels/SimpleTypes/SimpleInteger/runtimes/rust/Cargo.toml @@ -12,7 +12,7 @@ wrapped-client = [] 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"} +dafny_runtime = { path = "../../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]} [dev-dependencies] simple_integer = { path = ".", features = ["wrapped-client"] } diff --git a/TestModels/SimpleTypes/SimpleLong/runtimes/rust/Cargo.toml b/TestModels/SimpleTypes/SimpleLong/runtimes/rust/Cargo.toml index 98f34019cb..fecb7f2f20 100644 --- a/TestModels/SimpleTypes/SimpleLong/runtimes/rust/Cargo.toml +++ b/TestModels/SimpleTypes/SimpleLong/runtimes/rust/Cargo.toml @@ -12,7 +12,7 @@ wrapped-client = [] 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"} +dafny_runtime = { path = "../../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]} [dev-dependencies] simple_long = { path = ".", features = ["wrapped-client"] } diff --git a/TestModels/SimpleTypes/SimpleString/runtimes/rust/Cargo.toml b/TestModels/SimpleTypes/SimpleString/runtimes/rust/Cargo.toml index a653498171..02384d989c 100644 --- a/TestModels/SimpleTypes/SimpleString/runtimes/rust/Cargo.toml +++ b/TestModels/SimpleTypes/SimpleString/runtimes/rust/Cargo.toml @@ -12,7 +12,7 @@ wrapped-client = [] 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"} +dafny_runtime = { path = "../../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]} [dev-dependencies] simple_string = { path = ".", features = ["wrapped-client"] } diff --git a/TestModels/SimpleTypes/SimpleTimestamp/runtimes/rust/Cargo.toml b/TestModels/SimpleTypes/SimpleTimestamp/runtimes/rust/Cargo.toml index bfa2b336c3..f01cc234a4 100644 --- a/TestModels/SimpleTypes/SimpleTimestamp/runtimes/rust/Cargo.toml +++ b/TestModels/SimpleTypes/SimpleTimestamp/runtimes/rust/Cargo.toml @@ -12,7 +12,7 @@ wrapped-client = [] 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"} +dafny_runtime = { path = "../../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]} [dev-dependencies] simple_timestamp = { path = ".", features = ["wrapped-client"] } diff --git a/TestModels/Union/runtimes/rust/Cargo.toml b/TestModels/Union/runtimes/rust/Cargo.toml index 5891ab09a3..9a0126f921 100644 --- a/TestModels/Union/runtimes/rust/Cargo.toml +++ b/TestModels/Union/runtimes/rust/Cargo.toml @@ -12,7 +12,7 @@ wrapped-client = [] 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"} +dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]} [dev-dependencies] simple_union = { path = ".", features = ["wrapped-client"] } diff --git a/TestModels/aws-sdks/ddb-lite/runtimes/rust/Cargo.toml b/TestModels/aws-sdks/ddb-lite/runtimes/rust/Cargo.toml index 59c5c3e405..7b4d284671 100644 --- a/TestModels/aws-sdks/ddb-lite/runtimes/rust/Cargo.toml +++ b/TestModels/aws-sdks/ddb-lite/runtimes/rust/Cargo.toml @@ -9,7 +9,7 @@ edition = "2021" 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"} +dafny_runtime = { path = "../../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]} aws-sdk-dynamodb = "1.35.0" aws-config = "1.5.4" diff --git a/TestModels/aws-sdks/ddb/runtimes/rust/Cargo.toml b/TestModels/aws-sdks/ddb/runtimes/rust/Cargo.toml index a110aaea74..336a593677 100644 --- a/TestModels/aws-sdks/ddb/runtimes/rust/Cargo.toml +++ b/TestModels/aws-sdks/ddb/runtimes/rust/Cargo.toml @@ -14,7 +14,7 @@ aws-config = "1.5.4" 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"} +dafny_runtime = { path = "../../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]} [dev-dependencies] aws_sdk_ddb = { path = ".", features = ["wrapped-client"] } diff --git a/TestModels/aws-sdks/ddb/runtimes/rust/src/ddb.rs b/TestModels/aws-sdks/ddb/runtimes/rust/src/ddb.rs index 8fd807b651..b07c9f55e8 100644 --- a/TestModels/aws-sdks/ddb/runtimes/rust/src/ddb.rs +++ b/TestModels/aws-sdks/ddb/runtimes/rust/src/ddb.rs @@ -16,10 +16,10 @@ static DAFNY_TOKIO_RUNTIME: LazyLock = LazyLock::new(|| #[allow(non_snake_case)] impl crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::_default { - pub fn DynamoDBClient() -> ::std::rc::Rc< + pub fn DynamoDBClient() -> ::dafny_runtime::Rc< crate::r#_Wrappers_Compile::Result< ::dafny_runtime::Object, - ::std::rc::Rc + ::dafny_runtime::Rc > >{ let shared_config = match tokio::runtime::Handle::try_current() { @@ -35,7 +35,7 @@ impl crate::r#software::amazon::cryptography::services::dynamodb::internaldafny: let inner = aws_sdk_dynamodb::Client::new(&shared_config); let client = crate::client::Client { inner }; let dafny_client = ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(client)); - std::rc::Rc::new(crate::r#_Wrappers_Compile::Result::Success { + dafny_runtime::Rc::new(crate::r#_Wrappers_Compile::Result::Success { value: dafny_client, }) } diff --git a/TestModels/aws-sdks/ddb/runtimes/rust/src/lib.rs b/TestModels/aws-sdks/ddb/runtimes/rust/src/lib.rs index a4376aed78..3ceed5406c 100644 --- a/TestModels/aws-sdks/ddb/runtimes/rust/src/lib.rs +++ b/TestModels/aws-sdks/ddb/runtimes/rust/src/lib.rs @@ -8,12 +8,12 @@ pub mod client; pub mod conversions; +pub mod ddb; pub mod deps; pub(crate) mod implementation_from_dafny; mod standard_library_conversions; mod standard_library_externs; pub mod types; -pub mod ddb; pub(crate) use crate::implementation_from_dafny::_Wrappers_Compile; pub use crate::implementation_from_dafny::software; pub use client::Client; diff --git a/TestModels/aws-sdks/ddbv2/runtimes/rust/Cargo.toml b/TestModels/aws-sdks/ddbv2/runtimes/rust/Cargo.toml index a110aaea74..336a593677 100644 --- a/TestModels/aws-sdks/ddbv2/runtimes/rust/Cargo.toml +++ b/TestModels/aws-sdks/ddbv2/runtimes/rust/Cargo.toml @@ -14,7 +14,7 @@ aws-config = "1.5.4" 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"} +dafny_runtime = { path = "../../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]} [dev-dependencies] aws_sdk_ddb = { path = ".", features = ["wrapped-client"] } diff --git a/TestModels/aws-sdks/ddbv2/runtimes/rust/src/ddb.rs b/TestModels/aws-sdks/ddbv2/runtimes/rust/src/ddb.rs index 8fd807b651..b07c9f55e8 100644 --- a/TestModels/aws-sdks/ddbv2/runtimes/rust/src/ddb.rs +++ b/TestModels/aws-sdks/ddbv2/runtimes/rust/src/ddb.rs @@ -16,10 +16,10 @@ static DAFNY_TOKIO_RUNTIME: LazyLock = LazyLock::new(|| #[allow(non_snake_case)] impl crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::_default { - pub fn DynamoDBClient() -> ::std::rc::Rc< + pub fn DynamoDBClient() -> ::dafny_runtime::Rc< crate::r#_Wrappers_Compile::Result< ::dafny_runtime::Object, - ::std::rc::Rc + ::dafny_runtime::Rc > >{ let shared_config = match tokio::runtime::Handle::try_current() { @@ -35,7 +35,7 @@ impl crate::r#software::amazon::cryptography::services::dynamodb::internaldafny: let inner = aws_sdk_dynamodb::Client::new(&shared_config); let client = crate::client::Client { inner }; let dafny_client = ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(client)); - std::rc::Rc::new(crate::r#_Wrappers_Compile::Result::Success { + dafny_runtime::Rc::new(crate::r#_Wrappers_Compile::Result::Success { value: dafny_client, }) } diff --git a/TestModels/aws-sdks/ddbv2/runtimes/rust/src/lib.rs b/TestModels/aws-sdks/ddbv2/runtimes/rust/src/lib.rs index a4376aed78..3ceed5406c 100644 --- a/TestModels/aws-sdks/ddbv2/runtimes/rust/src/lib.rs +++ b/TestModels/aws-sdks/ddbv2/runtimes/rust/src/lib.rs @@ -8,12 +8,12 @@ pub mod client; pub mod conversions; +pub mod ddb; pub mod deps; pub(crate) mod implementation_from_dafny; mod standard_library_conversions; mod standard_library_externs; pub mod types; -pub mod ddb; pub(crate) use crate::implementation_from_dafny::_Wrappers_Compile; pub use crate::implementation_from_dafny::software; pub use client::Client; diff --git a/TestModels/aws-sdks/kms-lite/runtimes/rust/Cargo.toml b/TestModels/aws-sdks/kms-lite/runtimes/rust/Cargo.toml index cd5f9c0db5..5e7459a9da 100644 --- a/TestModels/aws-sdks/kms-lite/runtimes/rust/Cargo.toml +++ b/TestModels/aws-sdks/kms-lite/runtimes/rust/Cargo.toml @@ -9,7 +9,7 @@ edition = "2021" 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"} +dafny_runtime = { path = "../../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]} aws-sdk-kms = "1.35.0" aws-config = "1.5.4" diff --git a/TestModels/aws-sdks/kms/runtimes/rust/Cargo.toml b/TestModels/aws-sdks/kms/runtimes/rust/Cargo.toml index 4fe7ef3323..460afb7f34 100644 --- a/TestModels/aws-sdks/kms/runtimes/rust/Cargo.toml +++ b/TestModels/aws-sdks/kms/runtimes/rust/Cargo.toml @@ -14,7 +14,7 @@ aws-config = "1.5.4" 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"} +dafny_runtime = { path = "../../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]} [dev-dependencies] kms = { path = ".", features = ["wrapped-client"] } diff --git a/TestModels/aws-sdks/kms/runtimes/rust/src/kms.rs b/TestModels/aws-sdks/kms/runtimes/rust/src/kms.rs index 96a180ef46..e4dee95ee7 100644 --- a/TestModels/aws-sdks/kms/runtimes/rust/src/kms.rs +++ b/TestModels/aws-sdks/kms/runtimes/rust/src/kms.rs @@ -17,7 +17,7 @@ static DAFNY_TOKIO_RUNTIME: LazyLock = LazyLock::new(|| impl crate::r#software::amazon::cryptography::services::kms::internaldafny::_default { #[allow(non_snake_case)] - pub fn KMSClientForRegion(region: &::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>) -> ::std::rc::Rc, ::std::rc::Rc>>{ + pub fn KMSClientForRegion(region: &::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>) -> ::dafny_runtime::Rc, ::dafny_runtime::Rc>>{ let region = dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string( region, @@ -41,13 +41,13 @@ impl crate::r#software::amazon::cryptography::services::kms::internaldafny::_def let inner = aws_sdk_kms::Client::new(&shared_config); let client = crate::client::Client { inner }; let dafny_client = ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(client)); - std::rc::Rc::new(crate::r#_Wrappers_Compile::Result::Success { + dafny_runtime::Rc::new(crate::r#_Wrappers_Compile::Result::Success { value: dafny_client, }) } #[allow(non_snake_case)] - pub fn KMSClient() -> ::std::rc::Rc, ::std::rc::Rc>>{ + pub fn KMSClient() -> ::dafny_runtime::Rc, ::dafny_runtime::Rc>>{ let shared_config = match tokio::runtime::Handle::try_current() { Ok(curr) => tokio::task::block_in_place(|| { curr.block_on(async { @@ -62,7 +62,7 @@ impl crate::r#software::amazon::cryptography::services::kms::internaldafny::_def let inner = aws_sdk_kms::Client::new(&shared_config); let client = crate::client::Client { inner }; let dafny_client = ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(client)); - std::rc::Rc::new(crate::r#_Wrappers_Compile::Result::Success { + dafny_runtime::Rc::new(crate::r#_Wrappers_Compile::Result::Success { value: dafny_client, }) } @@ -71,7 +71,7 @@ impl crate::r#software::amazon::cryptography::services::kms::internaldafny::_def pub fn RegionMatch( kmsClient: &::dafny_runtime::Object, region: &::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, - ) -> ::std::rc::Rc> { + ) -> ::dafny_runtime::Rc> { let region = dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string( region, @@ -82,6 +82,6 @@ impl crate::r#software::amazon::cryptography::services::kms::internaldafny::_def Some(r) => r.as_ref() == region, None => false, }; - ::std::rc::Rc::new(crate::r#_Wrappers_Compile::Option::Some { value: flag }) + ::dafny_runtime::Rc::new(crate::r#_Wrappers_Compile::Option::Some { value: flag }) } } diff --git a/TestModels/aws-sdks/kms/runtimes/rust/src/lib.rs b/TestModels/aws-sdks/kms/runtimes/rust/src/lib.rs index 574c9bc554..c4ccdfd222 100644 --- a/TestModels/aws-sdks/kms/runtimes/rust/src/lib.rs +++ b/TestModels/aws-sdks/kms/runtimes/rust/src/lib.rs @@ -9,9 +9,9 @@ pub mod client; pub mod conversions; pub mod deps; +pub(crate) mod implementation_from_dafny; /// Common errors and error handling utilities. pub mod kms; -pub(crate) mod implementation_from_dafny; /// All operations that this crate can perform. mod standard_library_conversions; mod standard_library_externs; diff --git a/TestModels/aws-sdks/kmsv2/runtimes/rust/Cargo.toml b/TestModels/aws-sdks/kmsv2/runtimes/rust/Cargo.toml index 4fe7ef3323..460afb7f34 100644 --- a/TestModels/aws-sdks/kmsv2/runtimes/rust/Cargo.toml +++ b/TestModels/aws-sdks/kmsv2/runtimes/rust/Cargo.toml @@ -14,7 +14,7 @@ aws-config = "1.5.4" 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"} +dafny_runtime = { path = "../../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]} [dev-dependencies] kms = { path = ".", features = ["wrapped-client"] } diff --git a/TestModels/aws-sdks/kmsv2/runtimes/rust/src/kms.rs b/TestModels/aws-sdks/kmsv2/runtimes/rust/src/kms.rs index 96a180ef46..e4dee95ee7 100644 --- a/TestModels/aws-sdks/kmsv2/runtimes/rust/src/kms.rs +++ b/TestModels/aws-sdks/kmsv2/runtimes/rust/src/kms.rs @@ -17,7 +17,7 @@ static DAFNY_TOKIO_RUNTIME: LazyLock = LazyLock::new(|| impl crate::r#software::amazon::cryptography::services::kms::internaldafny::_default { #[allow(non_snake_case)] - pub fn KMSClientForRegion(region: &::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>) -> ::std::rc::Rc, ::std::rc::Rc>>{ + pub fn KMSClientForRegion(region: &::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>) -> ::dafny_runtime::Rc, ::dafny_runtime::Rc>>{ let region = dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string( region, @@ -41,13 +41,13 @@ impl crate::r#software::amazon::cryptography::services::kms::internaldafny::_def let inner = aws_sdk_kms::Client::new(&shared_config); let client = crate::client::Client { inner }; let dafny_client = ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(client)); - std::rc::Rc::new(crate::r#_Wrappers_Compile::Result::Success { + dafny_runtime::Rc::new(crate::r#_Wrappers_Compile::Result::Success { value: dafny_client, }) } #[allow(non_snake_case)] - pub fn KMSClient() -> ::std::rc::Rc, ::std::rc::Rc>>{ + pub fn KMSClient() -> ::dafny_runtime::Rc, ::dafny_runtime::Rc>>{ let shared_config = match tokio::runtime::Handle::try_current() { Ok(curr) => tokio::task::block_in_place(|| { curr.block_on(async { @@ -62,7 +62,7 @@ impl crate::r#software::amazon::cryptography::services::kms::internaldafny::_def let inner = aws_sdk_kms::Client::new(&shared_config); let client = crate::client::Client { inner }; let dafny_client = ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(client)); - std::rc::Rc::new(crate::r#_Wrappers_Compile::Result::Success { + dafny_runtime::Rc::new(crate::r#_Wrappers_Compile::Result::Success { value: dafny_client, }) } @@ -71,7 +71,7 @@ impl crate::r#software::amazon::cryptography::services::kms::internaldafny::_def pub fn RegionMatch( kmsClient: &::dafny_runtime::Object, region: &::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, - ) -> ::std::rc::Rc> { + ) -> ::dafny_runtime::Rc> { let region = dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string( region, @@ -82,6 +82,6 @@ impl crate::r#software::amazon::cryptography::services::kms::internaldafny::_def Some(r) => r.as_ref() == region, None => false, }; - ::std::rc::Rc::new(crate::r#_Wrappers_Compile::Option::Some { value: flag }) + ::dafny_runtime::Rc::new(crate::r#_Wrappers_Compile::Option::Some { value: flag }) } } diff --git a/TestModels/aws-sdks/kmsv2/runtimes/rust/src/lib.rs b/TestModels/aws-sdks/kmsv2/runtimes/rust/src/lib.rs index 574c9bc554..c4ccdfd222 100644 --- a/TestModels/aws-sdks/kmsv2/runtimes/rust/src/lib.rs +++ b/TestModels/aws-sdks/kmsv2/runtimes/rust/src/lib.rs @@ -9,9 +9,9 @@ pub mod client; pub mod conversions; pub mod deps; +pub(crate) mod implementation_from_dafny; /// Common errors and error handling utilities. pub mod kms; -pub(crate) mod implementation_from_dafny; /// All operations that this crate can perform. mod standard_library_conversions; mod standard_library_externs; diff --git a/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/Cargo.toml b/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/Cargo.toml index a682821e81..3f3e045a52 100644 --- a/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/Cargo.toml +++ b/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/Cargo.toml @@ -6,5 +6,5 @@ edition = "2021" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html [dependencies] -dafny_runtime = { path = "../../../dafny_runtime_rust"} +dafny_runtime = { path = "../../../dafny_runtime_rust", features = ["sync"]} aws-smithy-types = "1.2.0" diff --git a/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/src/UTF8_externs.rs b/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/src/UTF8_externs.rs index eca6a29803..0ca1c96324 100644 --- a/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/src/UTF8_externs.rs +++ b/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/src/UTF8_externs.rs @@ -5,7 +5,7 @@ use crate::UTF8; impl crate::UTF8::_default { pub fn Encode( s: &::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, - ) -> ::std::rc::Rc< + ) -> ::dafny_runtime::Rc< r#_Wrappers_Compile::Result< UTF8::ValidUTF8Bytes, ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, @@ -32,7 +32,7 @@ impl crate::UTF8::_default { surrogate = Some(c.0); continue; } - return ::std::rc::Rc::new(r#_Wrappers_Compile::Result::>::Failure { + return ::dafny_runtime::Rc::new(r#_Wrappers_Compile::Result::>::Failure { error: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string( &e.to_string()) }); @@ -40,12 +40,12 @@ impl crate::UTF8::_default { } } if let Some(s) = surrogate { - return ::std::rc::Rc::new(r#_Wrappers_Compile::Result::>::Failure { + return ::dafny_runtime::Rc::new(r#_Wrappers_Compile::Result::>::Failure { error: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string( &format!("Surrogate pair missing: 0x{:04x}", s)) }); } - ::std::rc::Rc::new(r#_Wrappers_Compile::Result::< + ::dafny_runtime::Rc::new(r#_Wrappers_Compile::Result::< UTF8::ValidUTF8Bytes, ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, >::Success { @@ -54,7 +54,7 @@ impl crate::UTF8::_default { } pub fn Decode( b: &::dafny_runtime::Sequence, - ) -> ::std::rc::Rc< + ) -> ::dafny_runtime::Rc< r#_Wrappers_Compile::Result< ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, @@ -63,13 +63,13 @@ impl crate::UTF8::_default { let b = String::from_utf8(b.to_array().as_ref().clone()); match b { Ok(s) => { - ::std::rc::Rc::new(r#_Wrappers_Compile::Result::<::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + ::dafny_runtime::Rc::new(r#_Wrappers_Compile::Result::<::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>>::Success { value: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&s) }) }, Err(e) => { - return ::std::rc::Rc::new(r#_Wrappers_Compile::Result::<::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + return ::dafny_runtime::Rc::new(r#_Wrappers_Compile::Result::<::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>>::Failure { error: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string( &e.to_string()) diff --git a/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/src/conversion.rs b/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/src/conversion.rs index bbef673259..99f80bbe16 100644 --- a/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/src/conversion.rs +++ b/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/src/conversion.rs @@ -2,7 +2,7 @@ use crate::*; pub fn ostring_to_dafny( input: &Option, -) -> ::std::rc::Rc< +) -> ::dafny_runtime::Rc< _Wrappers_Compile::Option<::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>>, > { let dafny_value = match input { @@ -11,11 +11,11 @@ pub fn ostring_to_dafny( }, None => _Wrappers_Compile::Option::None {}, }; - ::std::rc::Rc::new(dafny_value) + ::dafny_runtime::Rc::new(dafny_value) } pub fn ostring_from_dafny( - input: ::std::rc::Rc< + input: ::dafny_runtime::Rc< _Wrappers_Compile::Option<::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>>, >, ) -> Option { @@ -30,15 +30,19 @@ pub fn ostring_from_dafny( } } -pub fn obool_to_dafny(input: &Option) -> ::std::rc::Rc<_Wrappers_Compile::Option> { +pub fn obool_to_dafny( + input: &Option, +) -> ::dafny_runtime::Rc<_Wrappers_Compile::Option> { let dafny_value = match input { Some(b) => _Wrappers_Compile::Option::Some { value: *b }, None => _Wrappers_Compile::Option::None {}, }; - ::std::rc::Rc::new(dafny_value) + ::dafny_runtime::Rc::new(dafny_value) } -pub fn obool_from_dafny(input: ::std::rc::Rc<_Wrappers_Compile::Option>) -> Option { +pub fn obool_from_dafny( + input: ::dafny_runtime::Rc<_Wrappers_Compile::Option>, +) -> Option { if matches!(input.as_ref(), _Wrappers_Compile::Option::Some { .. }) { Some(input.Extract()) } else { @@ -46,15 +50,15 @@ pub fn obool_from_dafny(input: ::std::rc::Rc<_Wrappers_Compile::Option>) - } } -pub fn oint_to_dafny(input: Option) -> ::std::rc::Rc<_Wrappers_Compile::Option> { +pub fn oint_to_dafny(input: Option) -> ::dafny_runtime::Rc<_Wrappers_Compile::Option> { let dafny_value = match input { Some(b) => _Wrappers_Compile::Option::Some { value: b }, None => _Wrappers_Compile::Option::None {}, }; - ::std::rc::Rc::new(dafny_value) + ::dafny_runtime::Rc::new(dafny_value) } -pub fn oint_from_dafny(input: ::std::rc::Rc<_Wrappers_Compile::Option>) -> Option { +pub fn oint_from_dafny(input: ::dafny_runtime::Rc<_Wrappers_Compile::Option>) -> Option { if matches!(input.as_ref(), _Wrappers_Compile::Option::Some { .. }) { Some(input.Extract()) } else { @@ -62,15 +66,15 @@ pub fn oint_from_dafny(input: ::std::rc::Rc<_Wrappers_Compile::Option>) -> } } -pub fn olong_to_dafny(input: Option) -> ::std::rc::Rc<_Wrappers_Compile::Option> { +pub fn olong_to_dafny(input: Option) -> ::dafny_runtime::Rc<_Wrappers_Compile::Option> { let dafny_value = match input { Some(b) => _Wrappers_Compile::Option::Some { value: b }, None => _Wrappers_Compile::Option::None {}, }; - ::std::rc::Rc::new(dafny_value) + ::dafny_runtime::Rc::new(dafny_value) } -pub fn olong_from_dafny(input: ::std::rc::Rc<_Wrappers_Compile::Option>) -> Option { +pub fn olong_from_dafny(input: ::dafny_runtime::Rc<_Wrappers_Compile::Option>) -> Option { if matches!(input.as_ref(), _Wrappers_Compile::Option::Some { .. }) { Some(input.Extract()) } else { @@ -87,24 +91,24 @@ pub fn blob_to_dafny(input: &::aws_smithy_types::Blob) -> ::dafny_runtime::Seque pub fn oblob_to_dafny( input: &Option<::aws_smithy_types::Blob>, -) -> ::std::rc::Rc<_Wrappers_Compile::Option<::dafny_runtime::Sequence>> { +) -> ::dafny_runtime::Rc<_Wrappers_Compile::Option<::dafny_runtime::Sequence>> { let dafny_value = match input { Some(b) => _Wrappers_Compile::Option::Some { value: blob_to_dafny(&b), }, None => _Wrappers_Compile::Option::None {}, }; - ::std::rc::Rc::new(dafny_value) + ::dafny_runtime::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()), + ::dafny_runtime::Rc::try_unwrap(input.to_array()).unwrap_or_else(|rc| (*rc).clone()), ) } pub fn oblob_from_dafny( - input: ::std::rc::Rc<_Wrappers_Compile::Option<::dafny_runtime::Sequence>>, + input: ::dafny_runtime::Rc<_Wrappers_Compile::Option<::dafny_runtime::Sequence>>, ) -> Option<::aws_smithy_types::Blob> { if matches!(input.as_ref(), _Wrappers_Compile::Option::Some { .. }) { Some(blob_from_dafny(input.Extract())) @@ -122,14 +126,14 @@ pub fn double_to_dafny(input: f64) -> ::dafny_runtime::Sequence { pub fn odouble_to_dafny( input: &Option, -) -> ::std::rc::Rc<_Wrappers_Compile::Option<::dafny_runtime::Sequence>> { +) -> ::dafny_runtime::Rc<_Wrappers_Compile::Option<::dafny_runtime::Sequence>> { let dafny_value = match input { Some(f) => _Wrappers_Compile::Option::Some { value: double_to_dafny(*f), }, None => _Wrappers_Compile::Option::None {}, }; - ::std::rc::Rc::new(dafny_value) + ::dafny_runtime::Rc::new(dafny_value) } pub fn double_from_dafny(input: &::dafny_runtime::Sequence) -> f64 { @@ -138,7 +142,7 @@ pub fn double_from_dafny(input: &::dafny_runtime::Sequence) -> f64 { } pub fn odouble_from_dafny( - input: ::std::rc::Rc<_Wrappers_Compile::Option<::dafny_runtime::Sequence>>, + input: ::dafny_runtime::Rc<_Wrappers_Compile::Option<::dafny_runtime::Sequence>>, ) -> Option { if matches!(input.as_ref(), _Wrappers_Compile::Option::Some { .. }) { Some(double_from_dafny(&input.Extract())) @@ -157,7 +161,7 @@ pub fn timestamp_to_dafny( pub fn otimestamp_to_dafny( input: &Option<::aws_smithy_types::DateTime>, -) -> ::std::rc::Rc< +) -> ::dafny_runtime::Rc< _Wrappers_Compile::Option<::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>>, > { let dafny_value = match input { @@ -166,7 +170,7 @@ pub fn otimestamp_to_dafny( }, None => _Wrappers_Compile::Option::None {}, }; - ::std::rc::Rc::new(dafny_value) + ::dafny_runtime::Rc::new(dafny_value) } pub fn timestamp_from_dafny( @@ -180,7 +184,7 @@ pub fn timestamp_from_dafny( } pub fn otimestamp_from_dafny( - input: ::std::rc::Rc< + input: ::dafny_runtime::Rc< _Wrappers_Compile::Option<::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>>, >, ) -> Option<::aws_smithy_types::DateTime> { @@ -192,7 +196,7 @@ pub fn otimestamp_from_dafny( } pub fn option_from_dafny( - input: ::std::rc::Rc<_Wrappers_Compile::Option>, + input: ::dafny_runtime::Rc<_Wrappers_Compile::Option>, converter: fn(&T) -> TR, ) -> Option { match &*input { @@ -204,17 +208,17 @@ pub fn option_from_dafny( pub fn option_to_dafny( input: &Option, converter: fn(&TR) -> T, -) -> ::std::rc::Rc<_Wrappers_Compile::Option> { +) -> ::dafny_runtime::Rc<_Wrappers_Compile::Option> { match input { - Some(value) => ::std::rc::Rc::new(_Wrappers_Compile::Option::Some { + Some(value) => ::dafny_runtime::Rc::new(_Wrappers_Compile::Option::Some { value: converter(&value), }), - None => ::std::rc::Rc::new(_Wrappers_Compile::Option::None {}), + None => ::dafny_runtime::Rc::new(_Wrappers_Compile::Option::None {}), } } pub fn result_from_dafny( - input: ::std::rc::Rc<_Wrappers_Compile::Result>, + input: ::dafny_runtime::Rc<_Wrappers_Compile::Result>, converter_t: fn(&T) -> TR, converter_e: fn(&E) -> ER, ) -> Result { @@ -228,12 +232,12 @@ pub fn result_to_dafny, converter_t: fn(&TR) -> T, converter_e: fn(&ER) -> E, -) -> ::std::rc::Rc<_Wrappers_Compile::Result> { +) -> ::dafny_runtime::Rc<_Wrappers_Compile::Result> { match input { - Ok(value) => ::std::rc::Rc::new(_Wrappers_Compile::Result::Success { + Ok(value) => ::dafny_runtime::Rc::new(_Wrappers_Compile::Result::Success { value: converter_t(&value), }), - Err(error) => ::std::rc::Rc::new(_Wrappers_Compile::Result::Failure { + Err(error) => ::dafny_runtime::Rc::new(_Wrappers_Compile::Result::Failure { error: converter_e(&error), }), } diff --git a/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/src/lib.rs b/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/src/lib.rs index 1dacabec5a..f675142852 100644 --- a/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/src/lib.rs +++ b/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/src/lib.rs @@ -6,9 +6,9 @@ non_camel_case_types )] -pub(crate) mod implementation_from_dafny; /// All operations that this crate can perform. pub mod UTF8_externs; pub mod conversion; +pub(crate) mod implementation_from_dafny; pub(crate) use crate::implementation_from_dafny::_Wrappers_Compile; -pub(crate) use crate::implementation_from_dafny::UTF8; \ No newline at end of file +pub(crate) use crate::implementation_from_dafny::UTF8; diff --git a/TestModels/dafny-dependencies/dafny_runtime_rust/Cargo.toml b/TestModels/dafny-dependencies/dafny_runtime_rust/Cargo.toml index d5244c747a..ca405a5693 100644 --- a/TestModels/dafny-dependencies/dafny_runtime_rust/Cargo.toml +++ b/TestModels/dafny-dependencies/dafny_runtime_rust/Cargo.toml @@ -7,3 +7,6 @@ edition = "2021" once_cell = "1.18.0" num = "0.4" itertools = "0.11.0" + +[features] +sync = [] \ No newline at end of file diff --git a/TestModels/dafny-dependencies/dafny_runtime_rust/src/lib.rs b/TestModels/dafny-dependencies/dafny_runtime_rust/src/lib.rs index 38144c2d35..77f789abce 100644 --- a/TestModels/dafny-dependencies/dafny_runtime_rust/src/lib.rs +++ b/TestModels/dafny-dependencies/dafny_runtime_rust/src/lib.rs @@ -6,23 +6,29 @@ pub use mem::MaybeUninit; use num::{bigint::ParseBigIntError, Integer, Num, One, Signed}; pub use once_cell::unsync::Lazy; use std::{ - any::Any, borrow::Borrow, boxed::Box, - cell::{RefCell, UnsafeCell}, clone::Clone, cmp::Ordering, collections::{HashMap, HashSet}, convert::From, fmt::{Debug, Display, Formatter}, hash::{Hash, Hasher}, - ptr::NonNull, mem, ops::{Add, Deref, Div, Fn, Mul, Neg, Rem, Sub}, - rc::{Rc, Weak}, + ptr::NonNull, vec::Vec, }; +#[cfg(not(feature = "sync"))] +pub use ::std::{ + cell::RefCell, + rc::{Rc, Weak}, +}; + +#[cfg(feature = "sync")] +pub use ::std::sync::{Arc as Rc, Mutex as RefCell, Weak}; + pub use system::*; pub use itertools; @@ -34,12 +40,55 @@ pub use num::ToPrimitive; pub use num::Zero; pub use std::convert::Into; +pub use ::std::any::Any; +pub use ::std::marker::Send; +pub use ::std::marker::Sync; + +#[cfg(not(feature = "sync"))] +pub type DynAny = dyn Any; +#[cfg(feature = "sync")] +pub type DynAny = dyn Any + Send + Sync; + +#[cfg(not(feature = "sync"))] +pub use ::std::cell::UnsafeCell; + +#[cfg(feature = "sync")] +pub struct UnsafeCell { + data: ::std::cell::UnsafeCell, // UnsafeCell for interior mutability +} +#[cfg(feature = "sync")] +unsafe impl Sync for UnsafeCell where T: Send {} +#[cfg(feature = "sync")] +impl UnsafeCell { + pub fn new(data: T) -> Self { + UnsafeCell { + data: ::std::cell::UnsafeCell::new(data), + } + } +} +#[cfg(feature = "sync")] +impl UnsafeCell { + pub fn get(&self) -> *mut T { + ::std::cell::UnsafeCell::get(&self.data) + } + pub fn raw_get(this: *const UnsafeCell) -> *mut T { + unsafe { ::std::cell::UnsafeCell::raw_get(&(*this).data) } + } +} + // An atomic box is just a RefCell in Rust pub type SizeT = usize; +#[cfg(not(feature = "sync"))] pub trait DafnyType: Clone + DafnyPrint + 'static {} +#[cfg(feature = "sync")] +pub trait DafnyType: Clone + DafnyPrint + Send + Sync + 'static {} +#[cfg(not(feature = "sync"))] impl DafnyType for T where T: Clone + DafnyPrint + 'static {} +#[cfg(feature = "sync")] +impl DafnyType for T where T: Clone + DafnyPrint + Send + Sync + 'static {} + pub trait DafnyTypeEq: DafnyType + Hash + Eq {} impl DafnyTypeEq for T where T: DafnyType + Hash + Eq {} @@ -64,12 +113,14 @@ pub mod dafny_runtime_conversions { use num::BigInt; use num::ToPrimitive; - use std::collections::HashMap; - use std::collections::HashSet; - use std::hash::Hash; - use std::rc::Rc; + use ::std::collections::HashMap; + use ::std::collections::HashSet; + use ::std::hash::Hash; + + pub use super::Rc; pub mod object { + pub use super::Rc; pub type DafnyClass = crate::Object; pub type DafnyArray = crate::Object<[T]>; pub type DafnyArray2 = crate::Object>; @@ -82,7 +133,7 @@ pub mod dafny_runtime_conversions { pub fn dafny_class_to_boxed_struct(ptr: DafnyClass) -> Box { Box::new(dafny_class_to_struct(ptr)) } - pub unsafe fn dafny_class_to_rc_struct(ptr: DafnyClass) -> ::std::rc::Rc { + pub unsafe fn dafny_class_to_rc_struct(ptr: DafnyClass) -> Rc { crate::rcmut::to_rc(ptr.0.unwrap()) } pub fn struct_to_dafny_class(t: T) -> DafnyClass { @@ -91,7 +142,7 @@ pub mod dafny_runtime_conversions { pub fn boxed_struct_to_dafny_class(t: Box) -> DafnyClass { struct_to_dafny_class(*t) } - pub unsafe fn rc_struct_to_dafny_class(t: ::std::rc::Rc) -> DafnyClass { + pub unsafe fn rc_struct_to_dafny_class(t: Rc) -> DafnyClass { crate::Object::from_rc(t) } // Conversions to and from Dafny arrays. They all take ownership @@ -100,9 +151,7 @@ pub mod dafny_runtime_conversions { } pub fn vec_to_dafny_array(array: Vec) -> DafnyArray { // SAFETY: We own the array - unsafe { - crate::Object::from_rc(::std::rc::Rc::from(array.into_boxed_slice())) - } + unsafe { crate::Object::from_rc(Rc::from(array.into_boxed_slice())) } } pub unsafe fn dafny_array2_to_vec(ptr: DafnyArray2) -> Vec> { crate::rd!(ptr).to_vec() @@ -110,6 +159,7 @@ pub mod dafny_runtime_conversions { } pub mod ptr { + pub use super::Rc; pub type DafnyClass = crate::Ptr; pub type DafnyArray = crate::Ptr<[T]>; pub type DafnyArray2 = crate::Ptr>; @@ -200,7 +250,7 @@ pub mod dafny_runtime_conversions { DafnyMap::::from_hashmap(map, converter_k, converter_v) } - // --unicode-chars:true + // --unicode-char:true pub mod unicode_chars_true { use crate::Sequence; @@ -216,7 +266,7 @@ pub mod dafny_runtime_conversions { } } - // --unicode-chars:false + // --unicode-char:false pub mod unicode_chars_false { use crate::Sequence; @@ -576,7 +626,7 @@ impl DafnyInt { #[inline] pub fn parse_bytes(number: &[u8], radix: u32) -> DafnyInt { DafnyInt { - data: ::std::rc::Rc::new(BigInt::parse_bytes(number, radix).unwrap()), + data: Rc::new(BigInt::parse_bytes(number, radix).unwrap()), } } pub fn from_usize(usize: usize) -> DafnyInt { @@ -597,7 +647,7 @@ macro_rules! impl_dafnyint_from { impl ::std::convert::From<$type> for $crate::DafnyInt { fn from(n: $type) -> Self { $crate::DafnyInt { - data: ::std::rc::Rc::new(n.into()), + data: $crate::Rc::new(n.into()), } } } @@ -704,58 +754,46 @@ where pub fn from_array(values: Ptr<[T]>) -> Sequence { let mut v = vec![]; v.extend_from_slice(read!(values)); - Sequence::ArraySequence { - values: Rc::new(v), - } + Sequence::ArraySequence { values: Rc::new(v) } } pub fn from_array_object(values: &Object<[T]>) -> Sequence { let mut v = vec![]; v.extend_from_slice(rd!(values)); - Sequence::ArraySequence { - values: Rc::new(v), - } + Sequence::ArraySequence { values: Rc::new(v) } } pub fn from_array_slice(values: Ptr<[T]>, start: &DafnyInt, end: &DafnyInt) -> Sequence { let mut v = vec![]; v.extend_from_slice(&read!(values)[start.to_usize().unwrap()..end.to_usize().unwrap()]); - Sequence::ArraySequence { - values: Rc::new(v), - } + Sequence::ArraySequence { values: Rc::new(v) } } - pub fn from_array_slice_object(values: &Object<[T]>, start: &DafnyInt, end: &DafnyInt) -> Sequence { + pub fn from_array_slice_object( + values: &Object<[T]>, + start: &DafnyInt, + end: &DafnyInt, + ) -> Sequence { let mut v = vec![]; v.extend_from_slice(&rd!(values)[start.to_usize().unwrap()..end.to_usize().unwrap()]); - Sequence::ArraySequence { - values: Rc::new(v), - } + Sequence::ArraySequence { values: Rc::new(v) } } pub fn from_array_take(values: Ptr<[T]>, n: &DafnyInt) -> Sequence { let mut v = vec![]; v.extend_from_slice(&read!(values)[..n.to_usize().unwrap()]); - Sequence::ArraySequence { - values: Rc::new(v), - } + Sequence::ArraySequence { values: Rc::new(v) } } pub fn from_array_take_object(values: &Object<[T]>, n: &DafnyInt) -> Sequence { let mut v = vec![]; v.extend_from_slice(&rd!(values)[..n.to_usize().unwrap()]); - Sequence::ArraySequence { - values: Rc::new(v), - } + Sequence::ArraySequence { values: Rc::new(v) } } pub fn from_array_drop(values: Ptr<[T]>, n: &DafnyInt) -> Sequence { let mut v = vec![]; v.extend_from_slice(&read!(values)[n.to_usize().unwrap()..]); - Sequence::ArraySequence { - values: Rc::new(v), - } + Sequence::ArraySequence { values: Rc::new(v) } } pub fn from_array_drop_object(values: &Object<[T]>, n: &DafnyInt) -> Sequence { let mut v = vec![]; v.extend_from_slice(&rd!(values)[n.to_usize().unwrap()..]); - Sequence::ArraySequence { - values: Rc::new(v), - } + Sequence::ArraySequence { values: Rc::new(v) } } pub fn from_array_owned(values: Vec) -> Sequence { Sequence::ArraySequence { @@ -784,8 +822,20 @@ where left, right, } => { + #[cfg(feature = "sync")] + let into_boxed = boxed.as_ref(); + #[cfg(feature = "sync")] + let into_boxed_borrowed = into_boxed; + #[cfg(feature = "sync")] + let mut guard = into_boxed_borrowed.lock().unwrap(); + #[cfg(feature = "sync")] + let borrowed: Option<&Rc>> = guard.as_ref(); + + #[cfg(not(feature = "sync"))] let into_boxed = boxed.as_ref().clone(); + #[cfg(not(feature = "sync"))] let into_boxed_borrowed = into_boxed.borrow(); + #[cfg(not(feature = "sync"))] let borrowed: Option<&Rc>> = into_boxed_borrowed.as_ref(); if let Some(cache) = borrowed.as_ref() { return Rc::clone(cache); @@ -793,20 +843,38 @@ where // Let's create an array of size length and fill it up recursively // We don't materialize nested arrays because most of the time they are forgotten let mut array: Vec = Vec::with_capacity(*length); - Sequence::::append_recursive(&mut array, self); + Sequence::::append_recursive_safe(&mut array, &borrowed, left, right); let result = Rc::new(array); - let mut cache = boxed.borrow_mut(); let mutable_left: *mut Sequence = left.get(); let mutable_right: *mut Sequence = right.get(); // safety: Once the array is computed, left and right won't ever be read again. unsafe { *mutable_left = seq!() }; unsafe { *mutable_right = seq!() }; - *cache = Some(result.clone()); + #[cfg(not(feature = "sync"))] + let mut guard = boxed.borrow_mut(); + *guard = Some(result.clone()); result } } } + pub fn append_recursive_safe( + array: &mut Vec, + borrowed: &Option<&Rc>>, + left: &Rc>>, + right: &Rc>>, + ) { + if let Some(values) = borrowed.as_ref() { + for value in values.iter() { + array.push(value.clone()); + } + return; + } + // safety: When a concat is initialized, the left and right are well defined + Sequence::::append_recursive(array, unsafe { &mut *left.get() }); + Sequence::::append_recursive(array, unsafe { &mut *right.get() }); + } + pub fn append_recursive(array: &mut Vec, this: &Sequence) { match this { Sequence::ArraySequence { values, .. } => @@ -821,8 +889,20 @@ where } => // Let's create an array of size length and fill it up recursively { + #[cfg(feature = "sync")] + let into_boxed = boxed.as_ref(); + #[cfg(feature = "sync")] + let into_boxed_borrowed = into_boxed; + #[cfg(feature = "sync")] + let guard = into_boxed_borrowed.lock().unwrap(); + #[cfg(feature = "sync")] + let borrowed: Option<&Rc>> = guard.as_ref(); + + #[cfg(not(feature = "sync"))] let into_boxed = boxed.as_ref().clone(); + #[cfg(not(feature = "sync"))] let into_boxed_borrowed = into_boxed.borrow(); + #[cfg(not(feature = "sync"))] let borrowed: Option<&Rc>> = into_boxed_borrowed.as_ref(); if let Some(values) = borrowed.as_ref() { for value in values.iter() { @@ -1204,7 +1284,6 @@ impl Map { } } - impl Map { pub fn values(&self) -> Set { let mut result: Vec = Vec::new(); @@ -1735,9 +1814,10 @@ impl Multiset { } pub fn iter(&self) -> impl Iterator + '_ { - self.data.iter().flat_map( - |(k, &ref v)| - ::std::iter::repeat(k).take(v.clone().as_usize())).cloned() + self.data + .iter() + .flat_map(|(k, &ref v)| ::std::iter::repeat(k).take(v.clone().as_usize())) + .cloned() } } @@ -1989,16 +2069,29 @@ impl DafnyPrint for LazyFieldWrapper { } } +#[cfg(feature = "sync")] +// Convert the DafnyPrint above into a macro so that we can create it for functions of any input arity +macro_rules! dafny_print_function { + ($($n:tt)*) => { + impl $crate::DafnyPrint for $crate::Rc B + Send + Sync> { + fn fmt_print(&self, f: &mut ::std::fmt::Formatter<'_>, _in_seq: bool) -> ::std::fmt::Result { + write!(f, "") + } + } + } +} +#[cfg(not(feature = "sync"))] // Convert the DafnyPrint above into a macro so that we can create it for functions of any input arity macro_rules! dafny_print_function { ($($n:tt)*) => { - impl $crate::DafnyPrint for ::std::rc::Rc B> { + impl $crate::DafnyPrint for $crate::Rc B> { fn fmt_print(&self, f: &mut ::std::fmt::Formatter<'_>, _in_seq: bool) -> ::std::fmt::Result { write!(f, "") } } } } + // Now create a loop like impl_tuple_print_loop so that we can create functions up to size 32 macro_rules! dafny_print_function_loop { ($first:ident $($rest:ident)*) => { @@ -2067,7 +2160,11 @@ impl DafnyPrint for *const T { macro_rules! impl_print_display { ($name:ty) => { impl $crate::DafnyPrint for $name { - fn fmt_print(&self, f: &mut ::std::fmt::Formatter<'_>, _in_seq: bool) -> ::std::fmt::Result { + fn fmt_print( + &self, + f: &mut ::std::fmt::Formatter<'_>, + _in_seq: bool, + ) -> ::std::fmt::Result { ::std::fmt::Display::fmt(&self, f) } } @@ -2106,7 +2203,7 @@ impl DafnyPrint for () { } } -#[derive(Clone)] +#[derive(Clone, Copy)] pub struct DafnyCharUTF16(pub u16); pub type DafnyStringUTF16 = Sequence; @@ -2182,7 +2279,7 @@ impl Sub for DafnyCharUTF16 { } } -#[derive(Clone)] +#[derive(Clone, Copy)] pub struct DafnyChar(pub char); pub type DafnyString = Sequence; @@ -2336,7 +2433,13 @@ impl DafnyPrint for BigRational { } } -impl DafnyPrint for Rc { +impl DafnyPrint for Rc { + fn fmt_print(&self, f: &mut Formatter<'_>, in_seq: bool) -> std::fmt::Result { + self.as_ref().fmt_print(f, in_seq) + } +} + +impl DafnyPrint for &Rc { fn fmt_print(&self, f: &mut Formatter<'_>, in_seq: bool) -> std::fmt::Result { self.as_ref().fmt_print(f, in_seq) } @@ -2368,12 +2471,20 @@ impl DafnyPrint for Vec { } } +#[cfg(not(feature = "sync"))] impl DafnyPrint for RefCell { fn fmt_print(&self, f: &mut Formatter<'_>, _in_seq: bool) -> std::fmt::Result { self.borrow().fmt_print(f, _in_seq) } } +#[cfg(feature = "sync")] +impl DafnyPrint for RefCell { + fn fmt_print(&self, f: &mut Formatter<'_>, _in_seq: bool) -> std::fmt::Result { + self.lock().unwrap().fmt_print(f, _in_seq) + } +} + impl DafnyPrint for HashSet { fn fmt_print(&self, f: &mut Formatter<'_>, _in_seq: bool) -> std::fmt::Result { write!(f, "{{")?; @@ -2540,7 +2651,7 @@ macro_rules! ARRAY_GETTER_LENGTH0 { pub fn length0_usize(&self) -> usize { self.data.len() } - } + }; } macro_rules! ARRAY_GETTER_LENGTH { ($field: ident, $field_usize: ident) => { @@ -2552,7 +2663,7 @@ macro_rules! ARRAY_GETTER_LENGTH { pub fn $field_usize(&self) -> usize { self.$field } - } + }; } // An 1-dimensional Dafny array is a zero-cost abstraction over a pointer on a native array @@ -2566,7 +2677,7 @@ macro_rules! array { macro_rules! ARRAY_INIT { {$length: ident, $inner: expr} => { $crate::array::initialize_box_usize($length, { - ::std::rc::Rc::new(move |_| { $inner }) + $crate::Rc::new(move |_| { $inner }) }) } } @@ -2574,7 +2685,7 @@ macro_rules! ARRAY_INIT { macro_rules! ARRAY_INIT_INNER { ($length: ident) => { $crate::array::placebos_box_usize::($length) - } + }; } // ARRAY_DATA_TYPE(length0, length1, length2) will return @@ -2657,7 +2768,6 @@ macro_rules! ARRAY_METHODS { }; } - macro_rules! ARRAY_STRUCT { ($ArrayType:ident, $length0: ident, $($length:ident),+) => { pub struct $ArrayType { @@ -2763,25 +2873,25 @@ macro_rules! ARRAY_DEF { // Array2 to Array16 -ARRAY_DEF!{Array2, +ARRAY_DEF! {Array2, (length0, length0_usize), (length1, length1_usize) } -ARRAY_DEF!{Array3, +ARRAY_DEF! {Array3, (length0, length0_usize), (length1, length1_usize), (length2, length2_usize) } -ARRAY_DEF!{Array4, +ARRAY_DEF! {Array4, (length0, length0_usize), (length1, length1_usize), (length2, length2_usize), (length3, length3_usize) } -ARRAY_DEF!{Array5, +ARRAY_DEF! {Array5, (length0, length0_usize), (length1, length1_usize), (length2, length2_usize), @@ -2789,7 +2899,7 @@ ARRAY_DEF!{Array5, (length4, length4_usize) } -ARRAY_DEF!{Array6, +ARRAY_DEF! {Array6, (length0, length0_usize), (length1, length1_usize), (length2, length2_usize), @@ -2798,7 +2908,7 @@ ARRAY_DEF!{Array6, (length5, length5_usize) } -ARRAY_DEF!{Array7, +ARRAY_DEF! {Array7, (length0, length0_usize), (length1, length1_usize), (length2, length2_usize), @@ -2808,7 +2918,7 @@ ARRAY_DEF!{Array7, (length6, length6_usize) } -ARRAY_DEF!{Array8, +ARRAY_DEF! {Array8, (length0, length0_usize), (length1, length1_usize), (length2, length2_usize), @@ -2819,7 +2929,7 @@ ARRAY_DEF!{Array8, (length7, length7_usize) } -ARRAY_DEF!{Array9, +ARRAY_DEF! {Array9, (length0, length0_usize), (length1, length1_usize), (length2, length2_usize), @@ -2831,7 +2941,7 @@ ARRAY_DEF!{Array9, (length8, length8_usize) } -ARRAY_DEF!{Array10, +ARRAY_DEF! {Array10, (length0, length0_usize), (length1, length1_usize), (length2, length2_usize), @@ -2844,7 +2954,7 @@ ARRAY_DEF!{Array10, (length9, length9_usize) } -ARRAY_DEF!{Array11, +ARRAY_DEF! {Array11, (length0, length0_usize), (length1, length1_usize), (length2, length2_usize), @@ -2858,7 +2968,7 @@ ARRAY_DEF!{Array11, (length10, length10_usize) } -ARRAY_DEF!{Array12, +ARRAY_DEF! {Array12, (length0, length0_usize), (length1, length1_usize), (length2, length2_usize), @@ -2873,7 +2983,7 @@ ARRAY_DEF!{Array12, (length11, length11_usize) } -ARRAY_DEF!{Array13, +ARRAY_DEF! {Array13, (length0, length0_usize), (length1, length1_usize), (length2, length2_usize), @@ -2889,7 +2999,7 @@ ARRAY_DEF!{Array13, (length12, length12_usize) } -ARRAY_DEF!{Array14, +ARRAY_DEF! {Array14, (length0, length0_usize), (length1, length1_usize), (length2, length2_usize), @@ -2906,7 +3016,7 @@ ARRAY_DEF!{Array14, (length13, length13_usize) } -ARRAY_DEF!{Array15, +ARRAY_DEF! {Array15, (length0, length0_usize), (length1, length1_usize), (length2, length2_usize), @@ -2924,7 +3034,7 @@ ARRAY_DEF!{Array15, (length14, length14_usize) } -ARRAY_DEF!{Array16, +ARRAY_DEF! {Array16, (length0, length0_usize), (length1, length1_usize), (length2, length2_usize), @@ -2945,10 +3055,12 @@ ARRAY_DEF!{Array16, pub mod array { use super::DafnyInt; - use num::ToPrimitive; - use std::mem::MaybeUninit; - use std::{boxed::Box, rc::Rc, vec::Vec}; use super::Ptr; + use super::Rc; + use ::std::boxed::Box; + use ::std::mem::MaybeUninit; + use ::std::vec::Vec; + use num::ToPrimitive; #[inline] pub fn from_native(v: Box<[T]>) -> Ptr<[T]> { @@ -3113,7 +3225,7 @@ macro_rules! is_object { #[macro_export] macro_rules! cast_any { ($raw:expr) => { - $crate::Upcast::::upcast($crate::read!($raw)) + $crate::Upcast::<$crate::DynAny>::upcast($crate::read!($raw)) }; } // cast_any_object is meant to be used on references only, to convert any references (classes or traits)* @@ -3121,7 +3233,7 @@ macro_rules! cast_any { #[macro_export] macro_rules! cast_any_object { ($obj:expr) => { - $crate::UpcastObject::::upcast($crate::md!($obj)) + $crate::UpcastObject::<$crate::DynAny>::upcast($crate::md!($obj)) }; } @@ -3161,25 +3273,22 @@ macro_rules! update_nodrop { // Given a class or array pointer, transforms it to a mutable reference #[macro_export] macro_rules! modify { - ($ptr:expr) => { - { - #[allow(unused_unsafe)] - let tmp = unsafe {&mut *(::std::cell::UnsafeCell::raw_get($ptr.0.unwrap_unchecked().as_ptr()))}; - tmp - } - } + ($ptr:expr) => {{ + #[allow(unused_unsafe)] + let tmp = + unsafe { &mut *($crate::UnsafeCell::raw_get($ptr.0.unwrap_unchecked().as_ptr())) }; + tmp + }}; } // Given a class or array pointer, transforms it to a read-only reference #[macro_export] macro_rules! read { - ($ptr:expr) => { - { - #[allow(unused_unsafe)] - let tmp = unsafe {&*(::std::cell::UnsafeCell::raw_get($ptr.0.unwrap_unchecked().as_ptr()))}; - tmp - } - } + ($ptr:expr) => {{ + #[allow(unused_unsafe)] + let tmp = unsafe { &*($crate::UnsafeCell::raw_get($ptr.0.unwrap_unchecked().as_ptr())) }; + tmp + }}; } // If the field is guaranteed to be assigned only once, update_field_nodrop is sufficient @@ -3243,7 +3352,13 @@ macro_rules! update_field_mut_if_uninit { // This Ptr has the same run-time space as *mut pub struct Ptr(pub Option>>); -impl Ptr { +#[cfg(feature = "sync")] +unsafe impl Send for Ptr {} + +#[cfg(feature = "sync")] +unsafe impl Sync for Ptr {} + +impl Ptr { pub fn null() -> Self { Ptr(None) } @@ -3252,7 +3367,12 @@ impl Ptr { } #[inline] pub fn from_raw_nonnull(t: *mut T) -> Ptr { - unsafe { Ptr(Some(::std::mem::transmute::, NonNull>>(NonNull::new_unchecked(t)))) } + unsafe { + Ptr(Some(::std::mem::transmute::< + NonNull, + NonNull>, + >(NonNull::new_unchecked(t)))) + } } pub fn from_box(t: Box) -> Ptr { Self::from_raw_nonnull(Box::into_raw(t)) @@ -3266,12 +3386,12 @@ impl Ptr { } } -impl > Ptr { +impl> Ptr { pub fn is_instance_of(self) -> bool { if self.is_null() { false } else { - read!(Upcast::::upcast(read!(self))) + read!(Upcast::::upcast(read!(self))) .downcast_ref::() .is_some() } @@ -3285,13 +3405,12 @@ impl NontrivialDefault for Ptr { } } -impl Ptr { +impl Ptr { pub fn new(val: T) -> Ptr { Self::from_box(Box::new(val)) } } - impl Eq for Ptr {} impl Clone for Ptr { @@ -3300,9 +3419,9 @@ impl Clone for Ptr { } } -impl Copy for Ptr { } +impl Copy for Ptr {} -impl Default for Ptr { +impl Default for Ptr { fn default() -> Self { Ptr::null() } @@ -3313,22 +3432,22 @@ impl Debug for Ptr { self.fmt_print(f, false) } } -impl DafnyPrint for Ptr { +impl DafnyPrint for Ptr { fn fmt_print(&self, f: &mut Formatter<'_>, _in_seq: bool) -> std::fmt::Result { write!(f, "") } } - -impl PartialEq> for Ptr { +impl PartialEq> for Ptr { fn eq(&self, other: &Ptr) -> bool { if !self.is_null() { if !other.is_null() { // To compare addresses, we need to ensure we only compare thin pointers // https://users.rust-lang.org/t/comparing-addresses-between-fat-and-thin-pointers/89008 ::std::ptr::eq( - self.clone().into_raw() as *const (), - other.clone().into_raw() as *const ()) + self.clone().into_raw() as *const (), + other.clone().into_raw() as *const (), + ) } else { false } @@ -3340,7 +3459,7 @@ impl PartialEq> for Ptr { } } -impl std::hash::Hash for Ptr { +impl std::hash::Hash for Ptr { fn hash(&self, state: &mut H) { if !self.is_null() { (read!(self.clone()) as *const T as *const ()).hash(state); @@ -3350,44 +3469,39 @@ impl std::hash::Hash for Ptr { } } -impl AsMut for Ptr { +impl AsMut for Ptr { fn as_mut(&mut self) -> &mut T { modify!(self.clone()) } } -impl AsRef for Ptr { +impl AsRef for Ptr { fn as_ref(&self) -> &T { read!(self.clone()) } } -impl Ptr { +impl Ptr { // Never use on local values, only on &self types previously called on Ptr types. pub fn from_ref(r: &T) -> Ptr { - Ptr(unsafe {::std::mem::transmute::<_, Option>>>(r as *const T)}) + Ptr(unsafe { ::std::mem::transmute::<_, Option>>>(r as *const T) }) } } // cast is meant to be used on references only, to downcast a trait reference to a class reference #[macro_export] macro_rules! cast { - ($raw:expr, $id:ty) => { - { - #[allow(unused_unsafe)] - let tmp = - unsafe { - let expr = $raw; - let res: $crate::Ptr<$id> = - if expr.is_null() { - $crate::Ptr::null() - } else { - $crate::Ptr::from_raw_nonnull(expr.into_raw() as *mut $id) - }; - res - }; - tmp - } - }; - + ($raw:expr, $id:ty) => {{ + #[allow(unused_unsafe)] + let tmp = unsafe { + let expr = $raw; + let res: $crate::Ptr<$id> = if expr.is_null() { + $crate::Ptr::null() + } else { + $crate::Ptr::from_raw_nonnull(expr.into_raw() as *mut $id) + }; + res + }; + tmp + }}; } ///////////////// @@ -3396,7 +3510,7 @@ macro_rules! cast { pub struct Object(pub Option>); -impl Object { +impl Object { // For safety, it requires the Rc to have been created with Rc::new() pub unsafe fn from_rc(rc: Rc) -> Object { Object(Some(rcmut::from_rc(rc))) @@ -3408,15 +3522,15 @@ impl Object { self.0.is_none() } } -impl > Object { +impl> Object { pub fn is_instance_of(self) -> bool { - // safety: Dafny won't call this function unless it can guarantee the object is still allocated - rd!(UpcastObject::::upcast(rd!(self))) + // safety: Dafny won't call this function unless it can guarantee the object is still allocated + rd!(UpcastObject::::upcast(rd!(self))) .downcast_ref::() .is_some() } } -impl Object { +impl Object { pub fn new(val: T) -> Object { Object(Some(rcmut::new(val))) } @@ -3429,20 +3543,20 @@ impl Clone for Object { } } -impl Default for Object { +impl Default for Object { fn default() -> Self { Object(None) } } -impl> Debug for Object { +impl> Debug for Object { fn fmt(&self, f: &mut Formatter) -> std::fmt::Result { self.fmt_print(f, false) } } -impl > DafnyPrint for Object { +impl> DafnyPrint for Object { fn fmt_print(&self, f: &mut Formatter<'_>, _in_seq: bool) -> std::fmt::Result { - let obj_any = UpcastObject::::upcast(self.as_ref()); + let obj_any = UpcastObject::::upcast(self.as_ref()); let option_string = obj_any.as_ref().downcast_ref::(); match option_string { Some(s) => write!(f, "{}", s), @@ -3451,20 +3565,19 @@ impl > DafnyPrint for Object { } } -impl DafnyPrint for Object<[T]> { +impl DafnyPrint for Object<[T]> { fn fmt_print(&self, f: &mut Formatter<'_>, _in_seq: bool) -> std::fmt::Result { write!(f, "") } } - -impl UpcastObject for String { - fn upcast(&self) -> Object { +impl UpcastObject for String { + fn upcast(&self) -> Object { // SAFETY: RC was just created - unsafe { Object::from_rc(Rc::new(self.clone()) as Rc) } + unsafe { Object::from_rc(Rc::new(self.clone()) as Rc) } } } -impl PartialEq> for Object { +impl PartialEq> for Object { fn eq(&self, other: &Object) -> bool { if let Some(p) = &self.0 { if let Some(q) = &other.0 { @@ -3482,7 +3595,7 @@ impl PartialEq> for Object { } } -impl std::hash::Hash for Object { +impl std::hash::Hash for Object { fn hash(&self, state: &mut H) { if let Some(p) = &self.0 { (p.as_ref().get() as *const ()).hash(state); @@ -3492,12 +3605,12 @@ impl std::hash::Hash for Object { } } -impl AsMut for Object { +impl AsMut for Object { fn as_mut(&mut self) -> &mut T { unsafe { &mut *(&self.0).as_ref().unwrap_unchecked().as_ref().get() } } } -impl AsRef for Object { +impl AsRef for Object { fn as_ref(&self) -> &T { unsafe { &*(&self.0).as_ref().unwrap_unchecked().as_ref().get() } } @@ -3509,11 +3622,11 @@ fn increment_strong_count(data: *const T) { // SAFETY: This method is called only on values that were constructed from an Rc unsafe { // Black box avoids the compiler wrongly inferring that increment strong count does nothing since the data it was applied to can be traced to be borrowed - ::std::hint::black_box(Rc::increment_strong_count(data)); + ::std::hint::black_box(Rc::increment_strong_count(data)); } } -impl Object { +impl Object { // SAFETY: This function needs to be called from a reference obtained by calling read!(o) on an object // We never inline this function, otherwise the compiler might figure out a way to remove the increment_strong_count #[inline(never)] @@ -3534,9 +3647,9 @@ impl Object { macro_rules! cast_object { ($raw:expr, $id:ty) => { unsafe { - let res: $crate::Object<$id> = - $crate::Object(Some(::std::rc::Rc::from_raw( - ::std::rc::Rc::into_raw($raw.0.unwrap()) as _))); + let res: $crate::Object<$id> = $crate::Object(Some($crate::Rc::from_raw( + $crate::Rc::into_raw($raw.0.unwrap()) as _, + ))); res } }; @@ -3548,12 +3661,23 @@ pub fn allocate_object() -> Object { } pub struct AllocationTracker { - allocations: Vec> + allocations: Vec>, } +#[cfg(feature = "sync")] +pub fn allocate_object_track(allocation_tracker: &mut AllocationTracker) -> Object { + let res = allocate_object::(); + allocation_tracker + .allocations + .push(Rc::>::downgrade(&res.0.clone().unwrap())); + res +} +#[cfg(not(feature = "sync"))] pub fn allocate_object_track(allocation_tracker: &mut AllocationTracker) -> Object { let res = allocate_object::(); - allocation_tracker.allocations.push(Rc::>::downgrade(&res.0.clone().unwrap())); + allocation_tracker + .allocations + .push(Rc::>::downgrade(&res.0.clone().unwrap())); res } @@ -3561,7 +3685,10 @@ pub fn allocate_object_track(allocation_tracker: &mut AllocationTrac #[macro_export] macro_rules! update_field_nodrop_object { ($ptr:expr, $field: ident, $value:expr) => { - $crate::update_nodrop_object!(($crate::rcmut::borrow_mut(&mut $ptr.0.clone().unwrap())).$field, $value) + $crate::update_nodrop_object!( + ($crate::rcmut::borrow_mut(&mut $ptr.0.clone().unwrap())).$field, + $value + ) }; } @@ -3569,7 +3696,12 @@ macro_rules! update_field_nodrop_object { #[macro_export] macro_rules! update_field_mut_nodrop_object { ($ptr:expr, $field: ident, $value:expr) => { - unsafe { ($crate::rcmut::borrow_mut(&mut $ptr.0.clone().unwrap())).$field.get().write($value) } + unsafe { + ($crate::rcmut::borrow_mut(&mut $ptr.0.clone().unwrap())) + .$field + .get() + .write($value) + } }; } @@ -3637,7 +3769,6 @@ macro_rules! update_field_mut_uninit_object { }}; } - // Equivalent of modify but for rcmut #[macro_export] macro_rules! md { @@ -3657,24 +3788,20 @@ macro_rules! rd { // To use when modifying a mutable field that is wrapped with UnsafeCell #[macro_export] macro_rules! modify_field { - ($pointer:expr, $rhs:expr) => { - { - let lhs = $pointer.get(); - let rhs = $rhs; - unsafe {*lhs = rhs} - } - }; + ($pointer:expr, $rhs:expr) => {{ + let lhs = $pointer.get(); + let rhs = $rhs; + unsafe { *lhs = rhs } + }}; } // To use when reading a mutable field that is wrapped with UnsafeCell #[macro_export] macro_rules! read_field { - ($pointer:expr) => { - { + ($pointer:expr) => {{ let lhs = $pointer.get(); - unsafe {(*lhs).clone()} - } - }; + unsafe { (*lhs).clone() } + }}; } pub type Field = UnsafeCell; @@ -3686,33 +3813,31 @@ pub fn new_field(t: T) -> Field { #[macro_export] macro_rules! refcount { ($x:expr) => { - ::std::rc::Rc::strong_count(unsafe { $crate::rcmut::as_rc($x.0.as_ref().unwrap()) }) + $crate::Rc::strong_count(unsafe { $crate::rcmut::as_rc($x.0.as_ref().unwrap()) }) }; } pub mod object { - use std::any::Any; + use crate::{Any, DynAny}; + + pub fn downcast(_self: crate::Object) -> crate::Object { + super::cast_object!(_self, T) + } pub fn new(val: T) -> crate::Object { crate::Object(Some(crate::rcmut::new(val))) } - pub fn downcast(_self: crate::Object) -> crate::Object { - unsafe { - crate::Object(Some(crate::rcmut::downcast::(_self.0.unwrap()).unwrap())) // Use unwrap_unchecked? - } - } #[inline] - pub fn is(_self: crate::Object) -> bool { + pub fn is(_self: crate::Object) -> bool { is_object!(_self, T) } } // Inspired from https://crates.io/crates/rcmut pub mod rcmut { - use std::cell::UnsafeCell; - use std::mem::{self, MaybeUninit}; - use std::rc::Rc; - use std::sync::Arc; + use crate::Rc; + use crate::UnsafeCell; + use ::std::mem::{self, MaybeUninit}; pub fn array_object_from_rc(data: Rc<[T]>) -> crate::Object<[T]> { crate::Object(Some(unsafe { crate::rcmut::from_rc(data) })) @@ -3774,54 +3899,20 @@ pub mod rcmut { mem::transmute(this.get()) } - pub unsafe fn downcast(this: RcMut) -> Option> { - let t: Rc = to_rc(this); + #[cfg(feature = "sync")] + pub unsafe fn downcast( + this: RcMut, + ) -> Option> { + let t: Rc = to_rc(this); let t: Rc = Rc::downcast::(t).ok()?; mem::transmute(t) } - /// A reference counted smart pointer with unrestricted mutability. - pub struct ArcMut { - inner: Arc>, - } - - impl Clone for ArcMut { - fn clone(&self) -> ArcMut { - ArcMut { - inner: self.inner.clone(), - } - } - } - - impl ArcMut { - /// Create a new ArcMut for a value. - pub fn new(val: T) -> ArcMut { - ArcMut { - inner: Arc::new(UnsafeCell::new(val)), - } - } - } - - impl ArcMut { - /// Retrieve the inner Rc as a reference. - pub unsafe fn as_arc(&self) -> &Arc { - mem::transmute(&self.inner) - } - - /// Retrieve the inner Rc as a mutable reference. - pub unsafe fn as_arc_mut(&mut self) -> &mut Arc { - mem::transmute(&mut self.inner) - } - - /// Get a reference to the value. - pub unsafe fn borrow(&self) -> &T { - mem::transmute(self.inner.get()) - } - - /// Get a mutable reference to the value. - pub unsafe fn borrow_mut(&mut self) -> &mut T { - mem::transmute(self.inner.get()) - } + #[cfg(not(feature = "sync"))] + pub unsafe fn downcast(this: RcMut) -> Option> { + let t: Rc = to_rc(this); + let t: Rc = Rc::downcast::(t).ok()?; + mem::transmute(t) } } @@ -3882,19 +3973,33 @@ macro_rules! maybe_placebos_from { //////////////// pub fn upcast_object() -> Rc) -> Object> - where A : UpcastObject +where + A: UpcastObject, { Rc::new(|x: Object| x.as_ref().upcast()) } pub fn upcast() -> Rc) -> Ptr> - where A: Upcast +where + A: Upcast, { Rc::new(|x: Ptr| read!(x).upcast()) } -pub fn upcast_id() -> Rc A> +pub fn upcast_box() -> Rc Box> +where + A: UpcastBox, +{ + Rc::new(|x: A| UpcastBox::upcast(&x)) +} +pub fn upcast_box_box() -> Rc) -> Box> +where + Box: UpcastBox, { + Rc::new(|x: Box| UpcastBox::upcast(&x)) +} + +pub fn upcast_id() -> Rc A> { Rc::new(|x: A| x) } @@ -3906,8 +4011,8 @@ pub fn box_coerce(f: Box U>) -> Box( - a_to_r: Rc R + 'static>) -> - Rc A>) -> Rc R> + 'static> { + a_to_r: Rc R + 'static>, +) -> Rc A>) -> Rc R> + 'static> { Rc::new(move |t_to_a: Rc A>| { let a_to_r = a_to_r.clone(); let t_to_a = t_to_a.clone(); @@ -3923,18 +4028,22 @@ pub trait Upcast { pub trait UpcastObject { fn upcast(&self) -> Object; } - -impl Upcast for T { +impl Upcast for T { fn upcast(&self) -> Ptr { Ptr::from_raw_nonnull(self as *const T as *mut T) } } -impl UpcastObject for T { +impl UpcastObject for T { fn upcast(&self) -> Object { Object::from_ref(self) } } +// For general traits +pub trait UpcastBox { + fn upcast(&self) -> Box; +} + #[macro_export] macro_rules! Extends { ($traitType: tt) => { @@ -3960,8 +4069,6 @@ macro_rules! UpcastObjectFn { }; } - - // It works only when there is no type parameters for $A... #[macro_export] macro_rules! UpcastDef { @@ -3992,8 +4099,7 @@ macro_rules! UpcastDefObject { } // Coercions for sets -impl Set -{ +impl Set { pub fn coerce(f: Rc V>) -> Rc) -> Set> { Rc::new(move |x: Set| { // We need to upcast individual elements @@ -4008,8 +4114,7 @@ impl Set } // Coercions for sequences -impl Sequence -{ +impl Sequence { pub fn coerce(f: Rc V>) -> Rc) -> Sequence> { // We need to upcast individual elements Rc::new(move |x: Sequence| { @@ -4024,12 +4129,13 @@ impl Sequence } // Coercions for multisets -impl Multiset -{ - pub fn coerce(f: Rc V>) -> Rc) -> Multiset> { +impl Multiset { + pub fn coerce( + f: Rc V>, + ) -> Rc) -> Multiset> { // We need to upcast individual elements Rc::new(move |x: Multiset| { - let f2 = f.clone(); + let f2 = f.clone(); // We need to upcast individual elements let mut new_multiset: HashMap = HashMap::::default(); for (value, count) in x.data.into_iter() { @@ -4041,8 +4147,7 @@ impl Multiset } // Coercions for Maps -impl Map -{ +impl Map { pub fn coerce(f: Rc V>) -> Rc) -> Map> { // We need to upcast individual elements Rc::new(move |x: Map| { @@ -4054,4 +4159,4 @@ impl Map Map::from_hashmap_owned(new_map) }) } -} \ No newline at end of file +} diff --git a/TestModels/dafny-dependencies/dafny_runtime_rust/src/system/mod.rs b/TestModels/dafny-dependencies/dafny_runtime_rust/src/system/mod.rs index d30d8671ec..5397a38279 100644 --- a/TestModels/dafny-dependencies/dafny_runtime_rust/src/system/mod.rs +++ b/TestModels/dafny-dependencies/dafny_runtime_rust/src/system/mod.rs @@ -8,7 +8,7 @@ pub mod _System { pub use ::std::fmt::Formatter; pub use ::std::fmt::Result; pub use crate::DafnyPrint; - pub use ::std::rc::Rc; + #[cfg(feature = "sync")] pub use ::std::sync::{Arc as Rc}; #[cfg(not(feature = "sync"))] pub use ::std::rc::Rc; pub use ::std::cmp::Eq; pub use ::std::hash::Hash; pub use ::std::hash::Hasher; @@ -28,11 +28,13 @@ pub mod _System { } impl Tuple2 { + /// Returns a borrow of the field _0 pub fn _0(&self) -> &T0 { match self { Tuple2::_T2{_0, _1, } => _0, } } + /// Returns a borrow of the field _1 pub fn _1(&self) -> &T1 { match self { Tuple2::_T2{_0, _1, } => _1, @@ -64,8 +66,9 @@ pub mod _System { } impl Tuple2 { - pub fn coerce(f_0: Rc r#__T0 + 'static>, f_1: Rc r#__T1 + 'static>) -> Rc) -> Tuple2> { - Rc::new(move |this: Self| -> Tuple2{ + /// Given type parameter conversions, returns a lambda to convert this structure + pub fn coerce<__T0: DafnyType, __T1: DafnyType>(f_0: Rc __T0 + 'static>, f_1: Rc __T1 + 'static>) -> Rc) -> Tuple2<__T0, __T1>> { + Rc::new(move |this: Self| -> Tuple2<__T0, __T1>{ match this { Tuple2::_T2{_0, _1, } => { Tuple2::_T2 { @@ -104,8 +107,8 @@ pub mod _System { } impl AsRef> - for &Tuple2 { - fn as_ref(&self) -> Self { + for Tuple2 { + fn as_ref(&self) -> &Self { self } } @@ -137,6 +140,7 @@ pub mod _System { } impl Tuple0 { + /// Enumerates all possible values of Tuple0 pub fn _AllSingletonConstructors() -> SequenceIter> { seq![Rc::new(Tuple0::_T0 {})].iter() } @@ -164,8 +168,8 @@ pub mod _System { } impl AsRef - for &Tuple0 { - fn as_ref(&self) -> Self { + for Tuple0 { + fn as_ref(&self) -> &Self { self } } @@ -178,6 +182,7 @@ pub mod _System { } impl Tuple1 { + /// Returns a borrow of the field _0 pub fn _0(&self) -> &T0 { match self { Tuple1::_T1{_0, } => _0, @@ -207,8 +212,9 @@ pub mod _System { } impl Tuple1 { - pub fn coerce(f_0: Rc r#__T0 + 'static>) -> Rc) -> Tuple1> { - Rc::new(move |this: Self| -> Tuple1{ + /// Given type parameter conversions, returns a lambda to convert this structure + pub fn coerce<__T0: DafnyType>(f_0: Rc __T0 + 'static>) -> Rc) -> Tuple1<__T0>> { + Rc::new(move |this: Self| -> Tuple1<__T0>{ match this { Tuple1::_T1{_0, } => { Tuple1::_T1 { @@ -244,8 +250,8 @@ pub mod _System { } impl AsRef> - for &Tuple1 { - fn as_ref(&self) -> Self { + for Tuple1 { + fn as_ref(&self) -> &Self { self } } @@ -260,16 +266,19 @@ pub mod _System { } impl Tuple3 { + /// Returns a borrow of the field _0 pub fn _0(&self) -> &T0 { match self { Tuple3::_T3{_0, _1, _2, } => _0, } } + /// Returns a borrow of the field _1 pub fn _1(&self) -> &T1 { match self { Tuple3::_T3{_0, _1, _2, } => _1, } } + /// Returns a borrow of the field _2 pub fn _2(&self) -> &T2 { match self { Tuple3::_T3{_0, _1, _2, } => _2, @@ -303,8 +312,9 @@ pub mod _System { } impl Tuple3 { - pub fn coerce(f_0: Rc r#__T0 + 'static>, f_1: Rc r#__T1 + 'static>, f_2: Rc r#__T2 + 'static>) -> Rc) -> Tuple3> { - Rc::new(move |this: Self| -> Tuple3{ + /// Given type parameter conversions, returns a lambda to convert this structure + pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType>(f_0: Rc __T0 + 'static>, f_1: Rc __T1 + 'static>, f_2: Rc __T2 + 'static>) -> Rc) -> Tuple3<__T0, __T1, __T2>> { + Rc::new(move |this: Self| -> Tuple3<__T0, __T1, __T2>{ match this { Tuple3::_T3{_0, _1, _2, } => { Tuple3::_T3 { @@ -346,8 +356,8 @@ pub mod _System { } impl AsRef> - for &Tuple3 { - fn as_ref(&self) -> Self { + for Tuple3 { + fn as_ref(&self) -> &Self { self } } @@ -363,21 +373,25 @@ pub mod _System { } impl Tuple4 { + /// Returns a borrow of the field _0 pub fn _0(&self) -> &T0 { match self { Tuple4::_T4{_0, _1, _2, _3, } => _0, } } + /// Returns a borrow of the field _1 pub fn _1(&self) -> &T1 { match self { Tuple4::_T4{_0, _1, _2, _3, } => _1, } } + /// Returns a borrow of the field _2 pub fn _2(&self) -> &T2 { match self { Tuple4::_T4{_0, _1, _2, _3, } => _2, } } + /// Returns a borrow of the field _3 pub fn _3(&self) -> &T3 { match self { Tuple4::_T4{_0, _1, _2, _3, } => _3, @@ -413,8 +427,9 @@ pub mod _System { } impl Tuple4 { - pub fn coerce(f_0: Rc r#__T0 + 'static>, f_1: Rc r#__T1 + 'static>, f_2: Rc r#__T2 + 'static>, f_3: Rc r#__T3 + 'static>) -> Rc) -> Tuple4> { - Rc::new(move |this: Self| -> Tuple4{ + /// Given type parameter conversions, returns a lambda to convert this structure + pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType>(f_0: Rc __T0 + 'static>, f_1: Rc __T1 + 'static>, f_2: Rc __T2 + 'static>, f_3: Rc __T3 + 'static>) -> Rc) -> Tuple4<__T0, __T1, __T2, __T3>> { + Rc::new(move |this: Self| -> Tuple4<__T0, __T1, __T2, __T3>{ match this { Tuple4::_T4{_0, _1, _2, _3, } => { Tuple4::_T4 { @@ -459,8 +474,8 @@ pub mod _System { } impl AsRef> - for &Tuple4 { - fn as_ref(&self) -> Self { + for Tuple4 { + fn as_ref(&self) -> &Self { self } } @@ -477,26 +492,31 @@ pub mod _System { } impl Tuple5 { + /// Returns a borrow of the field _0 pub fn _0(&self) -> &T0 { match self { Tuple5::_T5{_0, _1, _2, _3, _4, } => _0, } } + /// Returns a borrow of the field _1 pub fn _1(&self) -> &T1 { match self { Tuple5::_T5{_0, _1, _2, _3, _4, } => _1, } } + /// Returns a borrow of the field _2 pub fn _2(&self) -> &T2 { match self { Tuple5::_T5{_0, _1, _2, _3, _4, } => _2, } } + /// Returns a borrow of the field _3 pub fn _3(&self) -> &T3 { match self { Tuple5::_T5{_0, _1, _2, _3, _4, } => _3, } } + /// Returns a borrow of the field _4 pub fn _4(&self) -> &T4 { match self { Tuple5::_T5{_0, _1, _2, _3, _4, } => _4, @@ -534,8 +554,9 @@ pub mod _System { } impl Tuple5 { - pub fn coerce(f_0: Rc r#__T0 + 'static>, f_1: Rc r#__T1 + 'static>, f_2: Rc r#__T2 + 'static>, f_3: Rc r#__T3 + 'static>, f_4: Rc r#__T4 + 'static>) -> Rc) -> Tuple5> { - Rc::new(move |this: Self| -> Tuple5{ + /// Given type parameter conversions, returns a lambda to convert this structure + pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType>(f_0: Rc __T0 + 'static>, f_1: Rc __T1 + 'static>, f_2: Rc __T2 + 'static>, f_3: Rc __T3 + 'static>, f_4: Rc __T4 + 'static>) -> Rc) -> Tuple5<__T0, __T1, __T2, __T3, __T4>> { + Rc::new(move |this: Self| -> Tuple5<__T0, __T1, __T2, __T3, __T4>{ match this { Tuple5::_T5{_0, _1, _2, _3, _4, } => { Tuple5::_T5 { @@ -583,8 +604,8 @@ pub mod _System { } impl AsRef> - for &Tuple5 { - fn as_ref(&self) -> Self { + for Tuple5 { + fn as_ref(&self) -> &Self { self } } @@ -602,31 +623,37 @@ pub mod _System { } impl Tuple6 { + /// Returns a borrow of the field _0 pub fn _0(&self) -> &T0 { match self { Tuple6::_T6{_0, _1, _2, _3, _4, _5, } => _0, } } + /// Returns a borrow of the field _1 pub fn _1(&self) -> &T1 { match self { Tuple6::_T6{_0, _1, _2, _3, _4, _5, } => _1, } } + /// Returns a borrow of the field _2 pub fn _2(&self) -> &T2 { match self { Tuple6::_T6{_0, _1, _2, _3, _4, _5, } => _2, } } + /// Returns a borrow of the field _3 pub fn _3(&self) -> &T3 { match self { Tuple6::_T6{_0, _1, _2, _3, _4, _5, } => _3, } } + /// Returns a borrow of the field _4 pub fn _4(&self) -> &T4 { match self { Tuple6::_T6{_0, _1, _2, _3, _4, _5, } => _4, } } + /// Returns a borrow of the field _5 pub fn _5(&self) -> &T5 { match self { Tuple6::_T6{_0, _1, _2, _3, _4, _5, } => _5, @@ -666,8 +693,9 @@ pub mod _System { } impl Tuple6 { - pub fn coerce(f_0: Rc r#__T0 + 'static>, f_1: Rc r#__T1 + 'static>, f_2: Rc r#__T2 + 'static>, f_3: Rc r#__T3 + 'static>, f_4: Rc r#__T4 + 'static>, f_5: Rc r#__T5 + 'static>) -> Rc) -> Tuple6> { - Rc::new(move |this: Self| -> Tuple6{ + /// Given type parameter conversions, returns a lambda to convert this structure + pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType>(f_0: Rc __T0 + 'static>, f_1: Rc __T1 + 'static>, f_2: Rc __T2 + 'static>, f_3: Rc __T3 + 'static>, f_4: Rc __T4 + 'static>, f_5: Rc __T5 + 'static>) -> Rc) -> Tuple6<__T0, __T1, __T2, __T3, __T4, __T5>> { + Rc::new(move |this: Self| -> Tuple6<__T0, __T1, __T2, __T3, __T4, __T5>{ match this { Tuple6::_T6{_0, _1, _2, _3, _4, _5, } => { Tuple6::_T6 { @@ -718,8 +746,8 @@ pub mod _System { } impl AsRef> - for &Tuple6 { - fn as_ref(&self) -> Self { + for Tuple6 { + fn as_ref(&self) -> &Self { self } } @@ -738,36 +766,43 @@ pub mod _System { } impl Tuple7 { + /// Returns a borrow of the field _0 pub fn _0(&self) -> &T0 { match self { Tuple7::_T7{_0, _1, _2, _3, _4, _5, _6, } => _0, } } + /// Returns a borrow of the field _1 pub fn _1(&self) -> &T1 { match self { Tuple7::_T7{_0, _1, _2, _3, _4, _5, _6, } => _1, } } + /// Returns a borrow of the field _2 pub fn _2(&self) -> &T2 { match self { Tuple7::_T7{_0, _1, _2, _3, _4, _5, _6, } => _2, } } + /// Returns a borrow of the field _3 pub fn _3(&self) -> &T3 { match self { Tuple7::_T7{_0, _1, _2, _3, _4, _5, _6, } => _3, } } + /// Returns a borrow of the field _4 pub fn _4(&self) -> &T4 { match self { Tuple7::_T7{_0, _1, _2, _3, _4, _5, _6, } => _4, } } + /// Returns a borrow of the field _5 pub fn _5(&self) -> &T5 { match self { Tuple7::_T7{_0, _1, _2, _3, _4, _5, _6, } => _5, } } + /// Returns a borrow of the field _6 pub fn _6(&self) -> &T6 { match self { Tuple7::_T7{_0, _1, _2, _3, _4, _5, _6, } => _6, @@ -809,8 +844,9 @@ pub mod _System { } impl Tuple7 { - pub fn coerce(f_0: Rc r#__T0 + 'static>, f_1: Rc r#__T1 + 'static>, f_2: Rc r#__T2 + 'static>, f_3: Rc r#__T3 + 'static>, f_4: Rc r#__T4 + 'static>, f_5: Rc r#__T5 + 'static>, f_6: Rc r#__T6 + 'static>) -> Rc) -> Tuple7> { - Rc::new(move |this: Self| -> Tuple7{ + /// Given type parameter conversions, returns a lambda to convert this structure + pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType>(f_0: Rc __T0 + 'static>, f_1: Rc __T1 + 'static>, f_2: Rc __T2 + 'static>, f_3: Rc __T3 + 'static>, f_4: Rc __T4 + 'static>, f_5: Rc __T5 + 'static>, f_6: Rc __T6 + 'static>) -> Rc) -> Tuple7<__T0, __T1, __T2, __T3, __T4, __T5, __T6>> { + Rc::new(move |this: Self| -> Tuple7<__T0, __T1, __T2, __T3, __T4, __T5, __T6>{ match this { Tuple7::_T7{_0, _1, _2, _3, _4, _5, _6, } => { Tuple7::_T7 { @@ -864,8 +900,8 @@ pub mod _System { } impl AsRef> - for &Tuple7 { - fn as_ref(&self) -> Self { + for Tuple7 { + fn as_ref(&self) -> &Self { self } } @@ -885,41 +921,49 @@ pub mod _System { } impl Tuple8 { + /// Returns a borrow of the field _0 pub fn _0(&self) -> &T0 { match self { Tuple8::_T8{_0, _1, _2, _3, _4, _5, _6, _7, } => _0, } } + /// Returns a borrow of the field _1 pub fn _1(&self) -> &T1 { match self { Tuple8::_T8{_0, _1, _2, _3, _4, _5, _6, _7, } => _1, } } + /// Returns a borrow of the field _2 pub fn _2(&self) -> &T2 { match self { Tuple8::_T8{_0, _1, _2, _3, _4, _5, _6, _7, } => _2, } } + /// Returns a borrow of the field _3 pub fn _3(&self) -> &T3 { match self { Tuple8::_T8{_0, _1, _2, _3, _4, _5, _6, _7, } => _3, } } + /// Returns a borrow of the field _4 pub fn _4(&self) -> &T4 { match self { Tuple8::_T8{_0, _1, _2, _3, _4, _5, _6, _7, } => _4, } } + /// Returns a borrow of the field _5 pub fn _5(&self) -> &T5 { match self { Tuple8::_T8{_0, _1, _2, _3, _4, _5, _6, _7, } => _5, } } + /// Returns a borrow of the field _6 pub fn _6(&self) -> &T6 { match self { Tuple8::_T8{_0, _1, _2, _3, _4, _5, _6, _7, } => _6, } } + /// Returns a borrow of the field _7 pub fn _7(&self) -> &T7 { match self { Tuple8::_T8{_0, _1, _2, _3, _4, _5, _6, _7, } => _7, @@ -963,8 +1007,9 @@ pub mod _System { } impl Tuple8 { - pub fn coerce(f_0: Rc r#__T0 + 'static>, f_1: Rc r#__T1 + 'static>, f_2: Rc r#__T2 + 'static>, f_3: Rc r#__T3 + 'static>, f_4: Rc r#__T4 + 'static>, f_5: Rc r#__T5 + 'static>, f_6: Rc r#__T6 + 'static>, f_7: Rc r#__T7 + 'static>) -> Rc) -> Tuple8> { - Rc::new(move |this: Self| -> Tuple8{ + /// Given type parameter conversions, returns a lambda to convert this structure + pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType>(f_0: Rc __T0 + 'static>, f_1: Rc __T1 + 'static>, f_2: Rc __T2 + 'static>, f_3: Rc __T3 + 'static>, f_4: Rc __T4 + 'static>, f_5: Rc __T5 + 'static>, f_6: Rc __T6 + 'static>, f_7: Rc __T7 + 'static>) -> Rc) -> Tuple8<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7>> { + Rc::new(move |this: Self| -> Tuple8<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7>{ match this { Tuple8::_T8{_0, _1, _2, _3, _4, _5, _6, _7, } => { Tuple8::_T8 { @@ -1021,8 +1066,8 @@ pub mod _System { } impl AsRef> - for &Tuple8 { - fn as_ref(&self) -> Self { + for Tuple8 { + fn as_ref(&self) -> &Self { self } } @@ -1043,46 +1088,55 @@ pub mod _System { } impl Tuple9 { + /// Returns a borrow of the field _0 pub fn _0(&self) -> &T0 { match self { Tuple9::_T9{_0, _1, _2, _3, _4, _5, _6, _7, _8, } => _0, } } + /// Returns a borrow of the field _1 pub fn _1(&self) -> &T1 { match self { Tuple9::_T9{_0, _1, _2, _3, _4, _5, _6, _7, _8, } => _1, } } + /// Returns a borrow of the field _2 pub fn _2(&self) -> &T2 { match self { Tuple9::_T9{_0, _1, _2, _3, _4, _5, _6, _7, _8, } => _2, } } + /// Returns a borrow of the field _3 pub fn _3(&self) -> &T3 { match self { Tuple9::_T9{_0, _1, _2, _3, _4, _5, _6, _7, _8, } => _3, } } + /// Returns a borrow of the field _4 pub fn _4(&self) -> &T4 { match self { Tuple9::_T9{_0, _1, _2, _3, _4, _5, _6, _7, _8, } => _4, } } + /// Returns a borrow of the field _5 pub fn _5(&self) -> &T5 { match self { Tuple9::_T9{_0, _1, _2, _3, _4, _5, _6, _7, _8, } => _5, } } + /// Returns a borrow of the field _6 pub fn _6(&self) -> &T6 { match self { Tuple9::_T9{_0, _1, _2, _3, _4, _5, _6, _7, _8, } => _6, } } + /// Returns a borrow of the field _7 pub fn _7(&self) -> &T7 { match self { Tuple9::_T9{_0, _1, _2, _3, _4, _5, _6, _7, _8, } => _7, } } + /// Returns a borrow of the field _8 pub fn _8(&self) -> &T8 { match self { Tuple9::_T9{_0, _1, _2, _3, _4, _5, _6, _7, _8, } => _8, @@ -1128,8 +1182,9 @@ pub mod _System { } impl Tuple9 { - pub fn coerce(f_0: Rc r#__T0 + 'static>, f_1: Rc r#__T1 + 'static>, f_2: Rc r#__T2 + 'static>, f_3: Rc r#__T3 + 'static>, f_4: Rc r#__T4 + 'static>, f_5: Rc r#__T5 + 'static>, f_6: Rc r#__T6 + 'static>, f_7: Rc r#__T7 + 'static>, f_8: Rc r#__T8 + 'static>) -> Rc) -> Tuple9> { - Rc::new(move |this: Self| -> Tuple9{ + /// Given type parameter conversions, returns a lambda to convert this structure + pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType, __T8: DafnyType>(f_0: Rc __T0 + 'static>, f_1: Rc __T1 + 'static>, f_2: Rc __T2 + 'static>, f_3: Rc __T3 + 'static>, f_4: Rc __T4 + 'static>, f_5: Rc __T5 + 'static>, f_6: Rc __T6 + 'static>, f_7: Rc __T7 + 'static>, f_8: Rc __T8 + 'static>) -> Rc) -> Tuple9<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8>> { + Rc::new(move |this: Self| -> Tuple9<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8>{ match this { Tuple9::_T9{_0, _1, _2, _3, _4, _5, _6, _7, _8, } => { Tuple9::_T9 { @@ -1189,8 +1244,8 @@ pub mod _System { } impl AsRef> - for &Tuple9 { - fn as_ref(&self) -> Self { + for Tuple9 { + fn as_ref(&self) -> &Self { self } } @@ -1212,51 +1267,61 @@ pub mod _System { } impl Tuple10 { + /// Returns a borrow of the field _0 pub fn _0(&self) -> &T0 { match self { Tuple10::_T10{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, } => _0, } } + /// Returns a borrow of the field _1 pub fn _1(&self) -> &T1 { match self { Tuple10::_T10{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, } => _1, } } + /// Returns a borrow of the field _2 pub fn _2(&self) -> &T2 { match self { Tuple10::_T10{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, } => _2, } } + /// Returns a borrow of the field _3 pub fn _3(&self) -> &T3 { match self { Tuple10::_T10{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, } => _3, } } + /// Returns a borrow of the field _4 pub fn _4(&self) -> &T4 { match self { Tuple10::_T10{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, } => _4, } } + /// Returns a borrow of the field _5 pub fn _5(&self) -> &T5 { match self { Tuple10::_T10{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, } => _5, } } + /// Returns a borrow of the field _6 pub fn _6(&self) -> &T6 { match self { Tuple10::_T10{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, } => _6, } } + /// Returns a borrow of the field _7 pub fn _7(&self) -> &T7 { match self { Tuple10::_T10{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, } => _7, } } + /// Returns a borrow of the field _8 pub fn _8(&self) -> &T8 { match self { Tuple10::_T10{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, } => _8, } } + /// Returns a borrow of the field _9 pub fn _9(&self) -> &T9 { match self { Tuple10::_T10{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, } => _9, @@ -1304,8 +1369,9 @@ pub mod _System { } impl Tuple10 { - pub fn coerce(f_0: Rc r#__T0 + 'static>, f_1: Rc r#__T1 + 'static>, f_2: Rc r#__T2 + 'static>, f_3: Rc r#__T3 + 'static>, f_4: Rc r#__T4 + 'static>, f_5: Rc r#__T5 + 'static>, f_6: Rc r#__T6 + 'static>, f_7: Rc r#__T7 + 'static>, f_8: Rc r#__T8 + 'static>, f_9: Rc r#__T9 + 'static>) -> Rc) -> Tuple10> { - Rc::new(move |this: Self| -> Tuple10{ + /// Given type parameter conversions, returns a lambda to convert this structure + pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType, __T8: DafnyType, __T9: DafnyType>(f_0: Rc __T0 + 'static>, f_1: Rc __T1 + 'static>, f_2: Rc __T2 + 'static>, f_3: Rc __T3 + 'static>, f_4: Rc __T4 + 'static>, f_5: Rc __T5 + 'static>, f_6: Rc __T6 + 'static>, f_7: Rc __T7 + 'static>, f_8: Rc __T8 + 'static>, f_9: Rc __T9 + 'static>) -> Rc) -> Tuple10<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9>> { + Rc::new(move |this: Self| -> Tuple10<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9>{ match this { Tuple10::_T10{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, } => { Tuple10::_T10 { @@ -1368,8 +1434,8 @@ pub mod _System { } impl AsRef> - for &Tuple10 { - fn as_ref(&self) -> Self { + for Tuple10 { + fn as_ref(&self) -> &Self { self } } @@ -1392,56 +1458,67 @@ pub mod _System { } impl Tuple11 { + /// Returns a borrow of the field _0 pub fn _0(&self) -> &T0 { match self { Tuple11::_T11{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, } => _0, } } + /// Returns a borrow of the field _1 pub fn _1(&self) -> &T1 { match self { Tuple11::_T11{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, } => _1, } } + /// Returns a borrow of the field _2 pub fn _2(&self) -> &T2 { match self { Tuple11::_T11{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, } => _2, } } + /// Returns a borrow of the field _3 pub fn _3(&self) -> &T3 { match self { Tuple11::_T11{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, } => _3, } } + /// Returns a borrow of the field _4 pub fn _4(&self) -> &T4 { match self { Tuple11::_T11{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, } => _4, } } + /// Returns a borrow of the field _5 pub fn _5(&self) -> &T5 { match self { Tuple11::_T11{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, } => _5, } } + /// Returns a borrow of the field _6 pub fn _6(&self) -> &T6 { match self { Tuple11::_T11{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, } => _6, } } + /// Returns a borrow of the field _7 pub fn _7(&self) -> &T7 { match self { Tuple11::_T11{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, } => _7, } } + /// Returns a borrow of the field _8 pub fn _8(&self) -> &T8 { match self { Tuple11::_T11{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, } => _8, } } + /// Returns a borrow of the field _9 pub fn _9(&self) -> &T9 { match self { Tuple11::_T11{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, } => _9, } } + /// Returns a borrow of the field _10 pub fn _10(&self) -> &T10 { match self { Tuple11::_T11{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, } => _10, @@ -1491,8 +1568,9 @@ pub mod _System { } impl Tuple11 { - pub fn coerce(f_0: Rc r#__T0 + 'static>, f_1: Rc r#__T1 + 'static>, f_2: Rc r#__T2 + 'static>, f_3: Rc r#__T3 + 'static>, f_4: Rc r#__T4 + 'static>, f_5: Rc r#__T5 + 'static>, f_6: Rc r#__T6 + 'static>, f_7: Rc r#__T7 + 'static>, f_8: Rc r#__T8 + 'static>, f_9: Rc r#__T9 + 'static>, f_10: Rc r#__T10 + 'static>) -> Rc) -> Tuple11> { - Rc::new(move |this: Self| -> Tuple11{ + /// Given type parameter conversions, returns a lambda to convert this structure + pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType, __T8: DafnyType, __T9: DafnyType, __T10: DafnyType>(f_0: Rc __T0 + 'static>, f_1: Rc __T1 + 'static>, f_2: Rc __T2 + 'static>, f_3: Rc __T3 + 'static>, f_4: Rc __T4 + 'static>, f_5: Rc __T5 + 'static>, f_6: Rc __T6 + 'static>, f_7: Rc __T7 + 'static>, f_8: Rc __T8 + 'static>, f_9: Rc __T9 + 'static>, f_10: Rc __T10 + 'static>) -> Rc) -> Tuple11<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10>> { + Rc::new(move |this: Self| -> Tuple11<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10>{ match this { Tuple11::_T11{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, } => { Tuple11::_T11 { @@ -1558,8 +1636,8 @@ pub mod _System { } impl AsRef> - for &Tuple11 { - fn as_ref(&self) -> Self { + for Tuple11 { + fn as_ref(&self) -> &Self { self } } @@ -1583,61 +1661,73 @@ pub mod _System { } impl Tuple12 { + /// Returns a borrow of the field _0 pub fn _0(&self) -> &T0 { match self { Tuple12::_T12{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, } => _0, } } + /// Returns a borrow of the field _1 pub fn _1(&self) -> &T1 { match self { Tuple12::_T12{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, } => _1, } } + /// Returns a borrow of the field _2 pub fn _2(&self) -> &T2 { match self { Tuple12::_T12{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, } => _2, } } + /// Returns a borrow of the field _3 pub fn _3(&self) -> &T3 { match self { Tuple12::_T12{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, } => _3, } } + /// Returns a borrow of the field _4 pub fn _4(&self) -> &T4 { match self { Tuple12::_T12{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, } => _4, } } + /// Returns a borrow of the field _5 pub fn _5(&self) -> &T5 { match self { Tuple12::_T12{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, } => _5, } } + /// Returns a borrow of the field _6 pub fn _6(&self) -> &T6 { match self { Tuple12::_T12{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, } => _6, } } + /// Returns a borrow of the field _7 pub fn _7(&self) -> &T7 { match self { Tuple12::_T12{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, } => _7, } } + /// Returns a borrow of the field _8 pub fn _8(&self) -> &T8 { match self { Tuple12::_T12{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, } => _8, } } + /// Returns a borrow of the field _9 pub fn _9(&self) -> &T9 { match self { Tuple12::_T12{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, } => _9, } } + /// Returns a borrow of the field _10 pub fn _10(&self) -> &T10 { match self { Tuple12::_T12{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, } => _10, } } + /// Returns a borrow of the field _11 pub fn _11(&self) -> &T11 { match self { Tuple12::_T12{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, } => _11, @@ -1689,8 +1779,9 @@ pub mod _System { } impl Tuple12 { - pub fn coerce(f_0: Rc r#__T0 + 'static>, f_1: Rc r#__T1 + 'static>, f_2: Rc r#__T2 + 'static>, f_3: Rc r#__T3 + 'static>, f_4: Rc r#__T4 + 'static>, f_5: Rc r#__T5 + 'static>, f_6: Rc r#__T6 + 'static>, f_7: Rc r#__T7 + 'static>, f_8: Rc r#__T8 + 'static>, f_9: Rc r#__T9 + 'static>, f_10: Rc r#__T10 + 'static>, f_11: Rc r#__T11 + 'static>) -> Rc) -> Tuple12> { - Rc::new(move |this: Self| -> Tuple12{ + /// Given type parameter conversions, returns a lambda to convert this structure + pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType, __T8: DafnyType, __T9: DafnyType, __T10: DafnyType, __T11: DafnyType>(f_0: Rc __T0 + 'static>, f_1: Rc __T1 + 'static>, f_2: Rc __T2 + 'static>, f_3: Rc __T3 + 'static>, f_4: Rc __T4 + 'static>, f_5: Rc __T5 + 'static>, f_6: Rc __T6 + 'static>, f_7: Rc __T7 + 'static>, f_8: Rc __T8 + 'static>, f_9: Rc __T9 + 'static>, f_10: Rc __T10 + 'static>, f_11: Rc __T11 + 'static>) -> Rc) -> Tuple12<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11>> { + Rc::new(move |this: Self| -> Tuple12<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11>{ match this { Tuple12::_T12{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, } => { Tuple12::_T12 { @@ -1759,8 +1850,8 @@ pub mod _System { } impl AsRef> - for &Tuple12 { - fn as_ref(&self) -> Self { + for Tuple12 { + fn as_ref(&self) -> &Self { self } } @@ -1785,66 +1876,79 @@ pub mod _System { } impl Tuple13 { + /// Returns a borrow of the field _0 pub fn _0(&self) -> &T0 { match self { Tuple13::_T13{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, } => _0, } } + /// Returns a borrow of the field _1 pub fn _1(&self) -> &T1 { match self { Tuple13::_T13{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, } => _1, } } + /// Returns a borrow of the field _2 pub fn _2(&self) -> &T2 { match self { Tuple13::_T13{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, } => _2, } } + /// Returns a borrow of the field _3 pub fn _3(&self) -> &T3 { match self { Tuple13::_T13{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, } => _3, } } + /// Returns a borrow of the field _4 pub fn _4(&self) -> &T4 { match self { Tuple13::_T13{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, } => _4, } } + /// Returns a borrow of the field _5 pub fn _5(&self) -> &T5 { match self { Tuple13::_T13{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, } => _5, } } + /// Returns a borrow of the field _6 pub fn _6(&self) -> &T6 { match self { Tuple13::_T13{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, } => _6, } } + /// Returns a borrow of the field _7 pub fn _7(&self) -> &T7 { match self { Tuple13::_T13{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, } => _7, } } + /// Returns a borrow of the field _8 pub fn _8(&self) -> &T8 { match self { Tuple13::_T13{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, } => _8, } } + /// Returns a borrow of the field _9 pub fn _9(&self) -> &T9 { match self { Tuple13::_T13{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, } => _9, } } + /// Returns a borrow of the field _10 pub fn _10(&self) -> &T10 { match self { Tuple13::_T13{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, } => _10, } } + /// Returns a borrow of the field _11 pub fn _11(&self) -> &T11 { match self { Tuple13::_T13{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, } => _11, } } + /// Returns a borrow of the field _12 pub fn _12(&self) -> &T12 { match self { Tuple13::_T13{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, } => _12, @@ -1898,8 +2002,9 @@ pub mod _System { } impl Tuple13 { - pub fn coerce(f_0: Rc r#__T0 + 'static>, f_1: Rc r#__T1 + 'static>, f_2: Rc r#__T2 + 'static>, f_3: Rc r#__T3 + 'static>, f_4: Rc r#__T4 + 'static>, f_5: Rc r#__T5 + 'static>, f_6: Rc r#__T6 + 'static>, f_7: Rc r#__T7 + 'static>, f_8: Rc r#__T8 + 'static>, f_9: Rc r#__T9 + 'static>, f_10: Rc r#__T10 + 'static>, f_11: Rc r#__T11 + 'static>, f_12: Rc r#__T12 + 'static>) -> Rc) -> Tuple13> { - Rc::new(move |this: Self| -> Tuple13{ + /// Given type parameter conversions, returns a lambda to convert this structure + pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType, __T8: DafnyType, __T9: DafnyType, __T10: DafnyType, __T11: DafnyType, __T12: DafnyType>(f_0: Rc __T0 + 'static>, f_1: Rc __T1 + 'static>, f_2: Rc __T2 + 'static>, f_3: Rc __T3 + 'static>, f_4: Rc __T4 + 'static>, f_5: Rc __T5 + 'static>, f_6: Rc __T6 + 'static>, f_7: Rc __T7 + 'static>, f_8: Rc __T8 + 'static>, f_9: Rc __T9 + 'static>, f_10: Rc __T10 + 'static>, f_11: Rc __T11 + 'static>, f_12: Rc __T12 + 'static>) -> Rc) -> Tuple13<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12>> { + Rc::new(move |this: Self| -> Tuple13<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12>{ match this { Tuple13::_T13{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, } => { Tuple13::_T13 { @@ -1971,8 +2076,8 @@ pub mod _System { } impl AsRef> - for &Tuple13 { - fn as_ref(&self) -> Self { + for Tuple13 { + fn as_ref(&self) -> &Self { self } } @@ -1998,71 +2103,85 @@ pub mod _System { } impl Tuple14 { + /// Returns a borrow of the field _0 pub fn _0(&self) -> &T0 { match self { Tuple14::_T14{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, } => _0, } } + /// Returns a borrow of the field _1 pub fn _1(&self) -> &T1 { match self { Tuple14::_T14{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, } => _1, } } + /// Returns a borrow of the field _2 pub fn _2(&self) -> &T2 { match self { Tuple14::_T14{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, } => _2, } } + /// Returns a borrow of the field _3 pub fn _3(&self) -> &T3 { match self { Tuple14::_T14{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, } => _3, } } + /// Returns a borrow of the field _4 pub fn _4(&self) -> &T4 { match self { Tuple14::_T14{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, } => _4, } } + /// Returns a borrow of the field _5 pub fn _5(&self) -> &T5 { match self { Tuple14::_T14{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, } => _5, } } + /// Returns a borrow of the field _6 pub fn _6(&self) -> &T6 { match self { Tuple14::_T14{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, } => _6, } } + /// Returns a borrow of the field _7 pub fn _7(&self) -> &T7 { match self { Tuple14::_T14{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, } => _7, } } + /// Returns a borrow of the field _8 pub fn _8(&self) -> &T8 { match self { Tuple14::_T14{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, } => _8, } } + /// Returns a borrow of the field _9 pub fn _9(&self) -> &T9 { match self { Tuple14::_T14{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, } => _9, } } + /// Returns a borrow of the field _10 pub fn _10(&self) -> &T10 { match self { Tuple14::_T14{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, } => _10, } } + /// Returns a borrow of the field _11 pub fn _11(&self) -> &T11 { match self { Tuple14::_T14{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, } => _11, } } + /// Returns a borrow of the field _12 pub fn _12(&self) -> &T12 { match self { Tuple14::_T14{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, } => _12, } } + /// Returns a borrow of the field _13 pub fn _13(&self) -> &T13 { match self { Tuple14::_T14{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, } => _13, @@ -2118,8 +2237,9 @@ pub mod _System { } impl Tuple14 { - pub fn coerce(f_0: Rc r#__T0 + 'static>, f_1: Rc r#__T1 + 'static>, f_2: Rc r#__T2 + 'static>, f_3: Rc r#__T3 + 'static>, f_4: Rc r#__T4 + 'static>, f_5: Rc r#__T5 + 'static>, f_6: Rc r#__T6 + 'static>, f_7: Rc r#__T7 + 'static>, f_8: Rc r#__T8 + 'static>, f_9: Rc r#__T9 + 'static>, f_10: Rc r#__T10 + 'static>, f_11: Rc r#__T11 + 'static>, f_12: Rc r#__T12 + 'static>, f_13: Rc r#__T13 + 'static>) -> Rc) -> Tuple14> { - Rc::new(move |this: Self| -> Tuple14{ + /// Given type parameter conversions, returns a lambda to convert this structure + pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType, __T8: DafnyType, __T9: DafnyType, __T10: DafnyType, __T11: DafnyType, __T12: DafnyType, __T13: DafnyType>(f_0: Rc __T0 + 'static>, f_1: Rc __T1 + 'static>, f_2: Rc __T2 + 'static>, f_3: Rc __T3 + 'static>, f_4: Rc __T4 + 'static>, f_5: Rc __T5 + 'static>, f_6: Rc __T6 + 'static>, f_7: Rc __T7 + 'static>, f_8: Rc __T8 + 'static>, f_9: Rc __T9 + 'static>, f_10: Rc __T10 + 'static>, f_11: Rc __T11 + 'static>, f_12: Rc __T12 + 'static>, f_13: Rc __T13 + 'static>) -> Rc) -> Tuple14<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13>> { + Rc::new(move |this: Self| -> Tuple14<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13>{ match this { Tuple14::_T14{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, } => { Tuple14::_T14 { @@ -2194,8 +2314,8 @@ pub mod _System { } impl AsRef> - for &Tuple14 { - fn as_ref(&self) -> Self { + for Tuple14 { + fn as_ref(&self) -> &Self { self } } @@ -2222,76 +2342,91 @@ pub mod _System { } impl Tuple15 { + /// Returns a borrow of the field _0 pub fn _0(&self) -> &T0 { match self { Tuple15::_T15{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, } => _0, } } + /// Returns a borrow of the field _1 pub fn _1(&self) -> &T1 { match self { Tuple15::_T15{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, } => _1, } } + /// Returns a borrow of the field _2 pub fn _2(&self) -> &T2 { match self { Tuple15::_T15{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, } => _2, } } + /// Returns a borrow of the field _3 pub fn _3(&self) -> &T3 { match self { Tuple15::_T15{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, } => _3, } } + /// Returns a borrow of the field _4 pub fn _4(&self) -> &T4 { match self { Tuple15::_T15{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, } => _4, } } + /// Returns a borrow of the field _5 pub fn _5(&self) -> &T5 { match self { Tuple15::_T15{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, } => _5, } } + /// Returns a borrow of the field _6 pub fn _6(&self) -> &T6 { match self { Tuple15::_T15{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, } => _6, } } + /// Returns a borrow of the field _7 pub fn _7(&self) -> &T7 { match self { Tuple15::_T15{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, } => _7, } } + /// Returns a borrow of the field _8 pub fn _8(&self) -> &T8 { match self { Tuple15::_T15{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, } => _8, } } + /// Returns a borrow of the field _9 pub fn _9(&self) -> &T9 { match self { Tuple15::_T15{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, } => _9, } } + /// Returns a borrow of the field _10 pub fn _10(&self) -> &T10 { match self { Tuple15::_T15{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, } => _10, } } + /// Returns a borrow of the field _11 pub fn _11(&self) -> &T11 { match self { Tuple15::_T15{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, } => _11, } } + /// Returns a borrow of the field _12 pub fn _12(&self) -> &T12 { match self { Tuple15::_T15{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, } => _12, } } + /// Returns a borrow of the field _13 pub fn _13(&self) -> &T13 { match self { Tuple15::_T15{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, } => _13, } } + /// Returns a borrow of the field _14 pub fn _14(&self) -> &T14 { match self { Tuple15::_T15{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, } => _14, @@ -2349,8 +2484,9 @@ pub mod _System { } impl Tuple15 { - pub fn coerce(f_0: Rc r#__T0 + 'static>, f_1: Rc r#__T1 + 'static>, f_2: Rc r#__T2 + 'static>, f_3: Rc r#__T3 + 'static>, f_4: Rc r#__T4 + 'static>, f_5: Rc r#__T5 + 'static>, f_6: Rc r#__T6 + 'static>, f_7: Rc r#__T7 + 'static>, f_8: Rc r#__T8 + 'static>, f_9: Rc r#__T9 + 'static>, f_10: Rc r#__T10 + 'static>, f_11: Rc r#__T11 + 'static>, f_12: Rc r#__T12 + 'static>, f_13: Rc r#__T13 + 'static>, f_14: Rc r#__T14 + 'static>) -> Rc) -> Tuple15> { - Rc::new(move |this: Self| -> Tuple15{ + /// Given type parameter conversions, returns a lambda to convert this structure + pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType, __T8: DafnyType, __T9: DafnyType, __T10: DafnyType, __T11: DafnyType, __T12: DafnyType, __T13: DafnyType, __T14: DafnyType>(f_0: Rc __T0 + 'static>, f_1: Rc __T1 + 'static>, f_2: Rc __T2 + 'static>, f_3: Rc __T3 + 'static>, f_4: Rc __T4 + 'static>, f_5: Rc __T5 + 'static>, f_6: Rc __T6 + 'static>, f_7: Rc __T7 + 'static>, f_8: Rc __T8 + 'static>, f_9: Rc __T9 + 'static>, f_10: Rc __T10 + 'static>, f_11: Rc __T11 + 'static>, f_12: Rc __T12 + 'static>, f_13: Rc __T13 + 'static>, f_14: Rc __T14 + 'static>) -> Rc) -> Tuple15<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14>> { + Rc::new(move |this: Self| -> Tuple15<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14>{ match this { Tuple15::_T15{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, } => { Tuple15::_T15 { @@ -2428,8 +2564,8 @@ pub mod _System { } impl AsRef> - for &Tuple15 { - fn as_ref(&self) -> Self { + for Tuple15 { + fn as_ref(&self) -> &Self { self } } @@ -2457,81 +2593,97 @@ pub mod _System { } impl Tuple16 { + /// Returns a borrow of the field _0 pub fn _0(&self) -> &T0 { match self { Tuple16::_T16{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, } => _0, } } + /// Returns a borrow of the field _1 pub fn _1(&self) -> &T1 { match self { Tuple16::_T16{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, } => _1, } } + /// Returns a borrow of the field _2 pub fn _2(&self) -> &T2 { match self { Tuple16::_T16{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, } => _2, } } + /// Returns a borrow of the field _3 pub fn _3(&self) -> &T3 { match self { Tuple16::_T16{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, } => _3, } } + /// Returns a borrow of the field _4 pub fn _4(&self) -> &T4 { match self { Tuple16::_T16{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, } => _4, } } + /// Returns a borrow of the field _5 pub fn _5(&self) -> &T5 { match self { Tuple16::_T16{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, } => _5, } } + /// Returns a borrow of the field _6 pub fn _6(&self) -> &T6 { match self { Tuple16::_T16{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, } => _6, } } + /// Returns a borrow of the field _7 pub fn _7(&self) -> &T7 { match self { Tuple16::_T16{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, } => _7, } } + /// Returns a borrow of the field _8 pub fn _8(&self) -> &T8 { match self { Tuple16::_T16{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, } => _8, } } + /// Returns a borrow of the field _9 pub fn _9(&self) -> &T9 { match self { Tuple16::_T16{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, } => _9, } } + /// Returns a borrow of the field _10 pub fn _10(&self) -> &T10 { match self { Tuple16::_T16{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, } => _10, } } + /// Returns a borrow of the field _11 pub fn _11(&self) -> &T11 { match self { Tuple16::_T16{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, } => _11, } } + /// Returns a borrow of the field _12 pub fn _12(&self) -> &T12 { match self { Tuple16::_T16{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, } => _12, } } + /// Returns a borrow of the field _13 pub fn _13(&self) -> &T13 { match self { Tuple16::_T16{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, } => _13, } } + /// Returns a borrow of the field _14 pub fn _14(&self) -> &T14 { match self { Tuple16::_T16{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, } => _14, } } + /// Returns a borrow of the field _15 pub fn _15(&self) -> &T15 { match self { Tuple16::_T16{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, } => _15, @@ -2591,8 +2743,9 @@ pub mod _System { } impl Tuple16 { - pub fn coerce(f_0: Rc r#__T0 + 'static>, f_1: Rc r#__T1 + 'static>, f_2: Rc r#__T2 + 'static>, f_3: Rc r#__T3 + 'static>, f_4: Rc r#__T4 + 'static>, f_5: Rc r#__T5 + 'static>, f_6: Rc r#__T6 + 'static>, f_7: Rc r#__T7 + 'static>, f_8: Rc r#__T8 + 'static>, f_9: Rc r#__T9 + 'static>, f_10: Rc r#__T10 + 'static>, f_11: Rc r#__T11 + 'static>, f_12: Rc r#__T12 + 'static>, f_13: Rc r#__T13 + 'static>, f_14: Rc r#__T14 + 'static>, f_15: Rc r#__T15 + 'static>) -> Rc) -> Tuple16> { - Rc::new(move |this: Self| -> Tuple16{ + /// Given type parameter conversions, returns a lambda to convert this structure + pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType, __T8: DafnyType, __T9: DafnyType, __T10: DafnyType, __T11: DafnyType, __T12: DafnyType, __T13: DafnyType, __T14: DafnyType, __T15: DafnyType>(f_0: Rc __T0 + 'static>, f_1: Rc __T1 + 'static>, f_2: Rc __T2 + 'static>, f_3: Rc __T3 + 'static>, f_4: Rc __T4 + 'static>, f_5: Rc __T5 + 'static>, f_6: Rc __T6 + 'static>, f_7: Rc __T7 + 'static>, f_8: Rc __T8 + 'static>, f_9: Rc __T9 + 'static>, f_10: Rc __T10 + 'static>, f_11: Rc __T11 + 'static>, f_12: Rc __T12 + 'static>, f_13: Rc __T13 + 'static>, f_14: Rc __T14 + 'static>, f_15: Rc __T15 + 'static>) -> Rc) -> Tuple16<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14, __T15>> { + Rc::new(move |this: Self| -> Tuple16<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14, __T15>{ match this { Tuple16::_T16{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, } => { Tuple16::_T16 { @@ -2673,8 +2826,8 @@ pub mod _System { } impl AsRef> - for &Tuple16 { - fn as_ref(&self) -> Self { + for Tuple16 { + fn as_ref(&self) -> &Self { self } } @@ -2703,86 +2856,103 @@ pub mod _System { } impl Tuple17 { + /// Returns a borrow of the field _0 pub fn _0(&self) -> &T0 { match self { Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, } => _0, } } + /// Returns a borrow of the field _1 pub fn _1(&self) -> &T1 { match self { Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, } => _1, } } + /// Returns a borrow of the field _2 pub fn _2(&self) -> &T2 { match self { Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, } => _2, } } + /// Returns a borrow of the field _3 pub fn _3(&self) -> &T3 { match self { Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, } => _3, } } + /// Returns a borrow of the field _4 pub fn _4(&self) -> &T4 { match self { Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, } => _4, } } + /// Returns a borrow of the field _5 pub fn _5(&self) -> &T5 { match self { Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, } => _5, } } + /// Returns a borrow of the field _6 pub fn _6(&self) -> &T6 { match self { Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, } => _6, } } + /// Returns a borrow of the field _7 pub fn _7(&self) -> &T7 { match self { Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, } => _7, } } + /// Returns a borrow of the field _8 pub fn _8(&self) -> &T8 { match self { Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, } => _8, } } + /// Returns a borrow of the field _9 pub fn _9(&self) -> &T9 { match self { Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, } => _9, } } + /// Returns a borrow of the field _10 pub fn _10(&self) -> &T10 { match self { Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, } => _10, } } + /// Returns a borrow of the field _11 pub fn _11(&self) -> &T11 { match self { Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, } => _11, } } + /// Returns a borrow of the field _12 pub fn _12(&self) -> &T12 { match self { Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, } => _12, } } + /// Returns a borrow of the field _13 pub fn _13(&self) -> &T13 { match self { Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, } => _13, } } + /// Returns a borrow of the field _14 pub fn _14(&self) -> &T14 { match self { Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, } => _14, } } + /// Returns a borrow of the field _15 pub fn _15(&self) -> &T15 { match self { Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, } => _15, } } + /// Returns a borrow of the field _16 pub fn _16(&self) -> &T16 { match self { Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, } => _16, @@ -2844,8 +3014,9 @@ pub mod _System { } impl Tuple17 { - pub fn coerce(f_0: Rc r#__T0 + 'static>, f_1: Rc r#__T1 + 'static>, f_2: Rc r#__T2 + 'static>, f_3: Rc r#__T3 + 'static>, f_4: Rc r#__T4 + 'static>, f_5: Rc r#__T5 + 'static>, f_6: Rc r#__T6 + 'static>, f_7: Rc r#__T7 + 'static>, f_8: Rc r#__T8 + 'static>, f_9: Rc r#__T9 + 'static>, f_10: Rc r#__T10 + 'static>, f_11: Rc r#__T11 + 'static>, f_12: Rc r#__T12 + 'static>, f_13: Rc r#__T13 + 'static>, f_14: Rc r#__T14 + 'static>, f_15: Rc r#__T15 + 'static>, f_16: Rc r#__T16 + 'static>) -> Rc) -> Tuple17> { - Rc::new(move |this: Self| -> Tuple17{ + /// Given type parameter conversions, returns a lambda to convert this structure + pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType, __T8: DafnyType, __T9: DafnyType, __T10: DafnyType, __T11: DafnyType, __T12: DafnyType, __T13: DafnyType, __T14: DafnyType, __T15: DafnyType, __T16: DafnyType>(f_0: Rc __T0 + 'static>, f_1: Rc __T1 + 'static>, f_2: Rc __T2 + 'static>, f_3: Rc __T3 + 'static>, f_4: Rc __T4 + 'static>, f_5: Rc __T5 + 'static>, f_6: Rc __T6 + 'static>, f_7: Rc __T7 + 'static>, f_8: Rc __T8 + 'static>, f_9: Rc __T9 + 'static>, f_10: Rc __T10 + 'static>, f_11: Rc __T11 + 'static>, f_12: Rc __T12 + 'static>, f_13: Rc __T13 + 'static>, f_14: Rc __T14 + 'static>, f_15: Rc __T15 + 'static>, f_16: Rc __T16 + 'static>) -> Rc) -> Tuple17<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14, __T15, __T16>> { + Rc::new(move |this: Self| -> Tuple17<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14, __T15, __T16>{ match this { Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, } => { Tuple17::_T17 { @@ -2929,8 +3100,8 @@ pub mod _System { } impl AsRef> - for &Tuple17 { - fn as_ref(&self) -> Self { + for Tuple17 { + fn as_ref(&self) -> &Self { self } } @@ -2960,91 +3131,109 @@ pub mod _System { } impl Tuple18 { + /// Returns a borrow of the field _0 pub fn _0(&self) -> &T0 { match self { Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => _0, } } + /// Returns a borrow of the field _1 pub fn _1(&self) -> &T1 { match self { Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => _1, } } + /// Returns a borrow of the field _2 pub fn _2(&self) -> &T2 { match self { Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => _2, } } + /// Returns a borrow of the field _3 pub fn _3(&self) -> &T3 { match self { Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => _3, } } + /// Returns a borrow of the field _4 pub fn _4(&self) -> &T4 { match self { Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => _4, } } + /// Returns a borrow of the field _5 pub fn _5(&self) -> &T5 { match self { Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => _5, } } + /// Returns a borrow of the field _6 pub fn _6(&self) -> &T6 { match self { Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => _6, } } + /// Returns a borrow of the field _7 pub fn _7(&self) -> &T7 { match self { Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => _7, } } + /// Returns a borrow of the field _8 pub fn _8(&self) -> &T8 { match self { Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => _8, } } + /// Returns a borrow of the field _9 pub fn _9(&self) -> &T9 { match self { Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => _9, } } + /// Returns a borrow of the field _10 pub fn _10(&self) -> &T10 { match self { Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => _10, } } + /// Returns a borrow of the field _11 pub fn _11(&self) -> &T11 { match self { Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => _11, } } + /// Returns a borrow of the field _12 pub fn _12(&self) -> &T12 { match self { Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => _12, } } + /// Returns a borrow of the field _13 pub fn _13(&self) -> &T13 { match self { Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => _13, } } + /// Returns a borrow of the field _14 pub fn _14(&self) -> &T14 { match self { Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => _14, } } + /// Returns a borrow of the field _15 pub fn _15(&self) -> &T15 { match self { Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => _15, } } + /// Returns a borrow of the field _16 pub fn _16(&self) -> &T16 { match self { Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => _16, } } + /// Returns a borrow of the field _17 pub fn _17(&self) -> &T17 { match self { Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => _17, @@ -3108,8 +3297,9 @@ pub mod _System { } impl Tuple18 { - pub fn coerce(f_0: Rc r#__T0 + 'static>, f_1: Rc r#__T1 + 'static>, f_2: Rc r#__T2 + 'static>, f_3: Rc r#__T3 + 'static>, f_4: Rc r#__T4 + 'static>, f_5: Rc r#__T5 + 'static>, f_6: Rc r#__T6 + 'static>, f_7: Rc r#__T7 + 'static>, f_8: Rc r#__T8 + 'static>, f_9: Rc r#__T9 + 'static>, f_10: Rc r#__T10 + 'static>, f_11: Rc r#__T11 + 'static>, f_12: Rc r#__T12 + 'static>, f_13: Rc r#__T13 + 'static>, f_14: Rc r#__T14 + 'static>, f_15: Rc r#__T15 + 'static>, f_16: Rc r#__T16 + 'static>, f_17: Rc r#__T17 + 'static>) -> Rc) -> Tuple18> { - Rc::new(move |this: Self| -> Tuple18{ + /// Given type parameter conversions, returns a lambda to convert this structure + pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType, __T8: DafnyType, __T9: DafnyType, __T10: DafnyType, __T11: DafnyType, __T12: DafnyType, __T13: DafnyType, __T14: DafnyType, __T15: DafnyType, __T16: DafnyType, __T17: DafnyType>(f_0: Rc __T0 + 'static>, f_1: Rc __T1 + 'static>, f_2: Rc __T2 + 'static>, f_3: Rc __T3 + 'static>, f_4: Rc __T4 + 'static>, f_5: Rc __T5 + 'static>, f_6: Rc __T6 + 'static>, f_7: Rc __T7 + 'static>, f_8: Rc __T8 + 'static>, f_9: Rc __T9 + 'static>, f_10: Rc __T10 + 'static>, f_11: Rc __T11 + 'static>, f_12: Rc __T12 + 'static>, f_13: Rc __T13 + 'static>, f_14: Rc __T14 + 'static>, f_15: Rc __T15 + 'static>, f_16: Rc __T16 + 'static>, f_17: Rc __T17 + 'static>) -> Rc) -> Tuple18<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14, __T15, __T16, __T17>> { + Rc::new(move |this: Self| -> Tuple18<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14, __T15, __T16, __T17>{ match this { Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => { Tuple18::_T18 { @@ -3196,8 +3386,8 @@ pub mod _System { } impl AsRef> - for &Tuple18 { - fn as_ref(&self) -> Self { + for Tuple18 { + fn as_ref(&self) -> &Self { self } } @@ -3228,96 +3418,115 @@ pub mod _System { } impl Tuple19 { + /// Returns a borrow of the field _0 pub fn _0(&self) -> &T0 { match self { Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => _0, } } + /// Returns a borrow of the field _1 pub fn _1(&self) -> &T1 { match self { Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => _1, } } + /// Returns a borrow of the field _2 pub fn _2(&self) -> &T2 { match self { Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => _2, } } + /// Returns a borrow of the field _3 pub fn _3(&self) -> &T3 { match self { Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => _3, } } + /// Returns a borrow of the field _4 pub fn _4(&self) -> &T4 { match self { Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => _4, } } + /// Returns a borrow of the field _5 pub fn _5(&self) -> &T5 { match self { Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => _5, } } + /// Returns a borrow of the field _6 pub fn _6(&self) -> &T6 { match self { Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => _6, } } + /// Returns a borrow of the field _7 pub fn _7(&self) -> &T7 { match self { Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => _7, } } + /// Returns a borrow of the field _8 pub fn _8(&self) -> &T8 { match self { Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => _8, } } + /// Returns a borrow of the field _9 pub fn _9(&self) -> &T9 { match self { Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => _9, } } + /// Returns a borrow of the field _10 pub fn _10(&self) -> &T10 { match self { Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => _10, } } + /// Returns a borrow of the field _11 pub fn _11(&self) -> &T11 { match self { Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => _11, } } + /// Returns a borrow of the field _12 pub fn _12(&self) -> &T12 { match self { Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => _12, } } + /// Returns a borrow of the field _13 pub fn _13(&self) -> &T13 { match self { Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => _13, } } + /// Returns a borrow of the field _14 pub fn _14(&self) -> &T14 { match self { Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => _14, } } + /// Returns a borrow of the field _15 pub fn _15(&self) -> &T15 { match self { Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => _15, } } + /// Returns a borrow of the field _16 pub fn _16(&self) -> &T16 { match self { Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => _16, } } + /// Returns a borrow of the field _17 pub fn _17(&self) -> &T17 { match self { Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => _17, } } + /// Returns a borrow of the field _18 pub fn _18(&self) -> &T18 { match self { Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => _18, @@ -3383,8 +3592,9 @@ pub mod _System { } impl Tuple19 { - pub fn coerce(f_0: Rc r#__T0 + 'static>, f_1: Rc r#__T1 + 'static>, f_2: Rc r#__T2 + 'static>, f_3: Rc r#__T3 + 'static>, f_4: Rc r#__T4 + 'static>, f_5: Rc r#__T5 + 'static>, f_6: Rc r#__T6 + 'static>, f_7: Rc r#__T7 + 'static>, f_8: Rc r#__T8 + 'static>, f_9: Rc r#__T9 + 'static>, f_10: Rc r#__T10 + 'static>, f_11: Rc r#__T11 + 'static>, f_12: Rc r#__T12 + 'static>, f_13: Rc r#__T13 + 'static>, f_14: Rc r#__T14 + 'static>, f_15: Rc r#__T15 + 'static>, f_16: Rc r#__T16 + 'static>, f_17: Rc r#__T17 + 'static>, f_18: Rc r#__T18 + 'static>) -> Rc) -> Tuple19> { - Rc::new(move |this: Self| -> Tuple19{ + /// Given type parameter conversions, returns a lambda to convert this structure + pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType, __T8: DafnyType, __T9: DafnyType, __T10: DafnyType, __T11: DafnyType, __T12: DafnyType, __T13: DafnyType, __T14: DafnyType, __T15: DafnyType, __T16: DafnyType, __T17: DafnyType, __T18: DafnyType>(f_0: Rc __T0 + 'static>, f_1: Rc __T1 + 'static>, f_2: Rc __T2 + 'static>, f_3: Rc __T3 + 'static>, f_4: Rc __T4 + 'static>, f_5: Rc __T5 + 'static>, f_6: Rc __T6 + 'static>, f_7: Rc __T7 + 'static>, f_8: Rc __T8 + 'static>, f_9: Rc __T9 + 'static>, f_10: Rc __T10 + 'static>, f_11: Rc __T11 + 'static>, f_12: Rc __T12 + 'static>, f_13: Rc __T13 + 'static>, f_14: Rc __T14 + 'static>, f_15: Rc __T15 + 'static>, f_16: Rc __T16 + 'static>, f_17: Rc __T17 + 'static>, f_18: Rc __T18 + 'static>) -> Rc) -> Tuple19<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14, __T15, __T16, __T17, __T18>> { + Rc::new(move |this: Self| -> Tuple19<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14, __T15, __T16, __T17, __T18>{ match this { Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => { Tuple19::_T19 { @@ -3474,8 +3684,8 @@ pub mod _System { } impl AsRef> - for &Tuple19 { - fn as_ref(&self) -> Self { + for Tuple19 { + fn as_ref(&self) -> &Self { self } } @@ -3507,101 +3717,121 @@ pub mod _System { } impl Tuple20 { + /// Returns a borrow of the field _0 pub fn _0(&self) -> &T0 { match self { Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => _0, } } + /// Returns a borrow of the field _1 pub fn _1(&self) -> &T1 { match self { Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => _1, } } + /// Returns a borrow of the field _2 pub fn _2(&self) -> &T2 { match self { Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => _2, } } + /// Returns a borrow of the field _3 pub fn _3(&self) -> &T3 { match self { Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => _3, } } + /// Returns a borrow of the field _4 pub fn _4(&self) -> &T4 { match self { Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => _4, } } + /// Returns a borrow of the field _5 pub fn _5(&self) -> &T5 { match self { Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => _5, } } + /// Returns a borrow of the field _6 pub fn _6(&self) -> &T6 { match self { Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => _6, } } + /// Returns a borrow of the field _7 pub fn _7(&self) -> &T7 { match self { Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => _7, } } + /// Returns a borrow of the field _8 pub fn _8(&self) -> &T8 { match self { Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => _8, } } + /// Returns a borrow of the field _9 pub fn _9(&self) -> &T9 { match self { Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => _9, } } + /// Returns a borrow of the field _10 pub fn _10(&self) -> &T10 { match self { Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => _10, } } + /// Returns a borrow of the field _11 pub fn _11(&self) -> &T11 { match self { Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => _11, } } + /// Returns a borrow of the field _12 pub fn _12(&self) -> &T12 { match self { Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => _12, } } + /// Returns a borrow of the field _13 pub fn _13(&self) -> &T13 { match self { Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => _13, } } + /// Returns a borrow of the field _14 pub fn _14(&self) -> &T14 { match self { Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => _14, } } + /// Returns a borrow of the field _15 pub fn _15(&self) -> &T15 { match self { Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => _15, } } + /// Returns a borrow of the field _16 pub fn _16(&self) -> &T16 { match self { Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => _16, } } + /// Returns a borrow of the field _17 pub fn _17(&self) -> &T17 { match self { Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => _17, } } + /// Returns a borrow of the field _18 pub fn _18(&self) -> &T18 { match self { Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => _18, } } + /// Returns a borrow of the field _19 pub fn _19(&self) -> &T19 { match self { Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => _19, @@ -3669,8 +3899,9 @@ pub mod _System { } impl Tuple20 { - pub fn coerce(f_0: Rc r#__T0 + 'static>, f_1: Rc r#__T1 + 'static>, f_2: Rc r#__T2 + 'static>, f_3: Rc r#__T3 + 'static>, f_4: Rc r#__T4 + 'static>, f_5: Rc r#__T5 + 'static>, f_6: Rc r#__T6 + 'static>, f_7: Rc r#__T7 + 'static>, f_8: Rc r#__T8 + 'static>, f_9: Rc r#__T9 + 'static>, f_10: Rc r#__T10 + 'static>, f_11: Rc r#__T11 + 'static>, f_12: Rc r#__T12 + 'static>, f_13: Rc r#__T13 + 'static>, f_14: Rc r#__T14 + 'static>, f_15: Rc r#__T15 + 'static>, f_16: Rc r#__T16 + 'static>, f_17: Rc r#__T17 + 'static>, f_18: Rc r#__T18 + 'static>, f_19: Rc r#__T19 + 'static>) -> Rc) -> Tuple20> { - Rc::new(move |this: Self| -> Tuple20{ + /// Given type parameter conversions, returns a lambda to convert this structure + pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType, __T8: DafnyType, __T9: DafnyType, __T10: DafnyType, __T11: DafnyType, __T12: DafnyType, __T13: DafnyType, __T14: DafnyType, __T15: DafnyType, __T16: DafnyType, __T17: DafnyType, __T18: DafnyType, __T19: DafnyType>(f_0: Rc __T0 + 'static>, f_1: Rc __T1 + 'static>, f_2: Rc __T2 + 'static>, f_3: Rc __T3 + 'static>, f_4: Rc __T4 + 'static>, f_5: Rc __T5 + 'static>, f_6: Rc __T6 + 'static>, f_7: Rc __T7 + 'static>, f_8: Rc __T8 + 'static>, f_9: Rc __T9 + 'static>, f_10: Rc __T10 + 'static>, f_11: Rc __T11 + 'static>, f_12: Rc __T12 + 'static>, f_13: Rc __T13 + 'static>, f_14: Rc __T14 + 'static>, f_15: Rc __T15 + 'static>, f_16: Rc __T16 + 'static>, f_17: Rc __T17 + 'static>, f_18: Rc __T18 + 'static>, f_19: Rc __T19 + 'static>) -> Rc) -> Tuple20<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14, __T15, __T16, __T17, __T18, __T19>> { + Rc::new(move |this: Self| -> Tuple20<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14, __T15, __T16, __T17, __T18, __T19>{ match this { Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => { Tuple20::_T20 { @@ -3763,8 +3994,8 @@ pub mod _System { } impl AsRef> - for &Tuple20 { - fn as_ref(&self) -> Self { + for Tuple20 { + fn as_ref(&self) -> &Self { self } } diff --git a/TestModels/dafny-dependencies/dafny_runtime_rust/src/tests/mod.rs b/TestModels/dafny-dependencies/dafny_runtime_rust/src/tests/mod.rs index d287da43dd..7b252cce42 100644 --- a/TestModels/dafny-dependencies/dafny_runtime_rust/src/tests/mod.rs +++ b/TestModels/dafny-dependencies/dafny_runtime_rust/src/tests/mod.rs @@ -1,3 +1,5 @@ +#![allow(nonstandard_style)] + // Test module #[cfg(test)] mod tests { @@ -42,7 +44,10 @@ mod tests { assert_eq!(*length, 6); assert_eq!(unsafe { &*left.get() }.cardinality_usize(), 3); // Test that boxed is None + #[cfg(not(feature = "sync"))] assert!(boxed.as_ref().clone().borrow().as_ref().is_none()); + #[cfg(feature = "sync")] + assert!(boxed.as_ref().lock().unwrap().as_ref().is_none()); } _ => panic!("This should never happen"), } @@ -50,10 +55,16 @@ mod tests { assert_eq!(value, 1); match &concat { crate::Sequence::ConcatSequence { boxed, .. } => { + #[cfg(not(feature = "sync"))] assert_eq!( *boxed.as_ref().clone().borrow().as_ref().unwrap().as_ref(), vec![1, 2, 3, 4, 5, 6] ); + #[cfg(feature = "sync")] + assert_eq!( + *boxed.as_ref().lock().unwrap().as_ref().unwrap().as_ref(), + vec![1, 2, 3, 4, 5, 6] + ); } _ => panic!("This should never happen"), } @@ -438,11 +449,11 @@ mod tests { } } - impl Upcast for ClassWrapper { - UpcastFn!(dyn Any); + impl Upcast for ClassWrapper { + UpcastFn!(crate::DynAny); } - impl UpcastObject for ClassWrapper { - UpcastObjectFn!(dyn Any); + impl UpcastObject for ClassWrapper { + UpcastObjectFn!(crate::DynAny); } #[test] @@ -544,19 +555,19 @@ mod tests { #[test] fn test_coercion_immutable() { let o = ClassWrapper::::constructor(1); - let a: Ptr = Upcast::::upcast(read!(o)); + let a: Ptr = Upcast::::upcast(read!(o)); assert_eq!(cast!(a, ClassWrapper), o); let seq_o = seq![o]; - let seq_a = Sequence::>>::coerce(upcast::, dyn Any>())(seq_o); + let seq_a = Sequence::>>::coerce(upcast::, crate::DynAny>())(seq_o); assert_eq!(cast!(seq_a.get_usize(0), ClassWrapper), o); let set_o = set! {o}; - let set_a = Set::>>::coerce(upcast::, dyn Any>())(set_o); + let set_a = Set::>>::coerce(upcast::, crate::DynAny>())(set_o); assert_eq!(cast!(set_a.peek(), ClassWrapper), o); let multiset_o = multiset! {o, o}; - let multiset_a = Multiset::>>::coerce(upcast::, dyn Any>())(multiset_o); + let multiset_a = Multiset::>>::coerce(upcast::, crate::DynAny>())(multiset_o); assert_eq!(cast!(multiset_a.peek(), ClassWrapper), o); let map_o = map![1 => o, 2 => o]; - let map_a = Map::>>::coerce(upcast::, dyn Any>())(map_o); + let map_a = Map::>>::coerce(upcast::, crate::DynAny>())(map_o); assert_eq!(cast!(map_a.get(&1), ClassWrapper), o); deallocate(o); } @@ -589,7 +600,7 @@ mod tests { #[test] fn test_function_wrappers() { - let f: Rc i32> = Rc::new(|i: i32| i + 1); + let f: Rc i32 + Send + Sync> = Rc::new(|i: i32| i + 1); let g = f.clone(); let _h = seq![g]; } @@ -683,10 +694,22 @@ mod tests { let count_inner = count.clone(); multiset!{1, 1, 5, 7, 8} .iter().for_each(move |_i: u32| { - let c: i32 = *count_inner.as_ref().borrow(); - *count_inner.borrow_mut() = c + 1; + #[cfg(not(feature = "sync"))] + { + let c: i32 = *count_inner.as_ref().borrow(); + *count_inner.borrow_mut() = c + 1; + } + #[cfg(feature = "sync")] + { + let mut guard = count_inner.as_ref().lock().unwrap(); + let c: i32 = *guard; + *guard = c + 1; + } }); + #[cfg(not(feature = "sync"))] assert_eq!(*count.as_ref().borrow(), 5); + #[cfg(feature = "sync")] + assert_eq!(*count.as_ref().lock().unwrap(), 5); let m = map![1 => 4, 3 => 6, 5 => 8]; let m2 = m.clone(); @@ -743,7 +766,7 @@ mod tests { assert_eq!(sum, 55); } - trait SuperTrait: Upcast + UpcastObject { + trait SuperTrait: Upcast + UpcastObject { } trait NodeRcMutTrait: SuperTrait + Upcast + UpcastObject{ @@ -762,11 +785,11 @@ mod tests { } } impl SuperTrait for NodeRcMut {} - impl UpcastObject for NodeRcMut { - UpcastObjectFn!(dyn Any); + impl UpcastObject for NodeRcMut { + UpcastObjectFn!(crate::DynAny); } - impl Upcast for NodeRcMut { - UpcastFn!(dyn Any); + impl Upcast for NodeRcMut { + UpcastFn!(crate::DynAny); } impl UpcastObject for NodeRcMut { UpcastObjectFn!(dyn NodeRcMutTrait); @@ -793,7 +816,7 @@ mod tests { assert_eq!(x.as_ref().next.as_ref().val, int!(42)); md!(rd!(x).next).next = Object(None); assert_eq!(refcount!(x), 1); - let y: Object = upcast_object::<_, _>()(x.clone()); + let y: Object = upcast_object::<_, _>()(x.clone()); assert_eq!(refcount!(x), 2); let z: Object = upcast_object::<_, _>()(x.clone()); assert_eq!(refcount!(x), 3); @@ -829,7 +852,7 @@ mod tests { } assert_eq!(refcount!(x), previous_count); - let objects: Set> = crate::set!{y.clone(), cast_any_object!(x.clone())}; + let objects: Set> = crate::set!{y.clone(), cast_any_object!(x.clone())}; assert_eq!(objects.cardinality_usize(), 1); test_dafny_type(a.clone()); } @@ -845,8 +868,8 @@ mod tests { } } impl NodeRcMutTrait for NodeRawMut {} - UpcastDefObject!(NodeRawMut, dyn NodeRcMutTrait, dyn SuperTrait, dyn Any); - UpcastDef!(NodeRawMut, dyn NodeRcMutTrait, dyn SuperTrait, dyn Any); + UpcastDefObject!(NodeRawMut, dyn NodeRcMutTrait, dyn SuperTrait, crate::DynAny); + UpcastDef!(NodeRawMut, dyn NodeRcMutTrait, dyn SuperTrait, crate::DynAny); impl SuperTrait for NodeRawMut {} @@ -858,7 +881,7 @@ mod tests { modify!(x.clone()).next = x.clone(); assert_eq!(read!(read!(x.clone()).next.clone()).val, int!(42)); modify!(read!(x.clone()).next.clone()).next = Ptr::null(); - let y: Ptr = upcast::<_, _>()(x); + let y: Ptr = upcast::<_, _>()(x); assert!(y.is_instance_of::()); assert!(!y.is_instance_of::()); let z: Ptr = upcast::<_, _>()(x); @@ -902,13 +925,13 @@ mod tests { pub message: String, } - crate::UpcastDefObject!(InternalOpaqueError, dyn Any); + crate::UpcastDefObject!(InternalOpaqueError, crate::DynAny); #[test] fn test_native_string_upcast() { let s = InternalOpaqueError { message: "Hello, World!".to_string() }; let o: Object = Object::new(s); - let n: Object = upcast_object::()(o); + let n: Object = upcast_object::()(o); let x = cast_object!(n, InternalOpaqueError); let s2 = crate::dafny_runtime_conversions::object::dafny_class_to_struct(x); assert_eq!(s2.message, "Hello, World!"); @@ -918,8 +941,125 @@ mod tests { fn test_native_string_upcast_raw() { let message = "Hello, World!".to_string(); let object = Object::new(message.clone()); - let object_any: Object = UpcastObject::::upcast(object.as_ref()); + let object_any: Object = UpcastObject::::upcast(object.as_ref()); let resulting_message = format!("{:?}", object_any); assert_eq!(resulting_message, message); } + + // Every general trait must declare how to clone a Box of itself + trait GeneralTraitSuper { + fn _clone(&self) -> Box>; + fn _is_GeneralTrait(&self) -> bool; + fn _as_GeneralTrait(&self) -> Box; + fn _is_Datatype(&self) -> bool; + fn _as_Datatype(&self) -> ADatatype; + } + impl Clone for Box> { + fn clone(&self) -> Self { + GeneralTraitSuper::_clone(self.as_ref()) + } + } + impl DafnyPrint for Box> { + fn fmt_print(&self, f: &mut Formatter<'_>, _in_seq: bool) -> std::fmt::Result { + write!(f, "GeneralTraitSuper") + } + } + // Traits extending other traits also implement a direct way to upcast their Box of themselves + trait GeneralTrait: GeneralTraitSuper + UpcastBox> { + fn _clone(&self) -> Box; + } + impl UpcastBox> for Box { + fn upcast(&self) -> ::std::boxed::Box> { + crate::tests::tests::GeneralTraitSuper::::_clone(self.as_ref()) + } + } + impl Clone for Box { + fn clone(&self) -> Self { + GeneralTrait::_clone(self.as_ref()) + } + } + impl DafnyPrint for Box { + fn fmt_print(&self, f: &mut Formatter<'_>, _in_seq: bool) -> std::fmt::Result { + write!(f, "GeneralTrait") + } + } + + #[derive(Clone, PartialEq, Debug)] + struct ADatatype{i: i32} + impl GeneralTrait for ADatatype { + fn _clone(&self) -> Box { + Box::new(self.clone()) as Box + } + } + impl GeneralTraitSuper for ADatatype { + fn _clone(&self) -> Box> { + Box::new(self.clone()) + } + + fn _is_GeneralTrait(&self) -> bool { + true + } + + fn _as_GeneralTrait(&self) -> Box { + GeneralTrait::_clone(self) + } + + fn _is_Datatype(&self) -> bool { + true + } + + fn _as_Datatype(&self) -> ADatatype { + self.clone() + } + } + impl UpcastBox for ADatatype { + fn upcast(&self) -> ::std::boxed::Box { + GeneralTrait::_clone(self) + } + } + impl UpcastBox> for ADatatype { + fn upcast(&self) -> ::std::boxed::Box> { + GeneralTraitSuper::::_clone(self) + } + } + #[test] + fn test_general_traits() { + let x = ADatatype{i: 3}; + let gt = upcast_box::()(x.clone()); + let gts = upcast_box::>()(x.clone()); + let gtgts = upcast_box_box::>()(gt.clone()); + assert!(gt._is_Datatype()); + assert!(gts._is_Datatype()); + assert!(gtgts._is_Datatype()); + assert!(gts._is_GeneralTrait()); + assert!(gtgts._is_GeneralTrait()); + assert_eq!(gt._as_Datatype(), x); + assert_eq!(gts._as_Datatype(), x); + assert_eq!(gtgts._as_Datatype(), x); + let gtsgt = gts._as_GeneralTrait(); + let gtgtsgt = gtgts._as_GeneralTrait(); + assert!(gtsgt._is_Datatype()); + assert!(gtgtsgt._is_Datatype()); + assert_eq!(gtsgt._as_Datatype(), x); + assert_eq!(gtsgt._as_Datatype(), x); + } + + #[test] + fn test_chars_copy() { + let c = DafnyChar('a'); + let c2 = c; + let c3 = c; + assert_eq!(c3, c2); + let c = DafnyCharUTF16(213); + let c2 = c; + let c3 = c; + assert_eq!(c3, c2); + } + /*impl GeneralTrait for Rc { + fn _clone(&self) -> Box { + Box::new(self.as_ref().clone()) + } + }*/ + + } 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 e1143e4095..1c06c9612d 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 @@ -22,6 +22,8 @@ class RustTestModels extends TestModelTest { DISABLED_TESTS.add("CodegenPatches"); DISABLED_TESTS.add("Dependencies"); DISABLED_TESTS.add("Extern"); + DISABLED_TESTS.add("LanguageSpecificLogic"); + DISABLED_TESTS.add("Refinement"); DISABLED_TESTS.add("SimpleTypes/BigDecimal"); DISABLED_TESTS.add("SimpleTypes/BigInteger"); DISABLED_TESTS.add("SimpleTypes/SimpleByte"); diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyrust/generator/AbstractRustShimGenerator.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyrust/generator/AbstractRustShimGenerator.java index aab91aa029..b7d69064ce 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyrust/generator/AbstractRustShimGenerator.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyrust/generator/AbstractRustShimGenerator.java @@ -243,8 +243,8 @@ protected TokenTree structureToDafnyFunction( #[allow(dead_code)] pub fn to_dafny( value: &$rustTypesModuleName:L::$rustStructureName:L, - ) -> ::std::rc::Rc{ - ::std::rc::Rc::new( + ) -> ::dafny_runtime::Rc{ + ::dafny_runtime::Rc::new( crate::r#$dafnyTypesModuleName:L::$structureName:L::$structureName:L { $variants:L } @@ -293,7 +293,7 @@ protected TokenTree structureFromDafnyFunction( """ #[allow(dead_code)] pub fn from_dafny( - dafny_value: ::std::rc::Rc< + dafny_value: ::dafny_runtime::Rc< crate::r#$dafnyTypesModuleName:L::$structureName:L, >, ) -> $rustTypesModuleName:L::$rustStructureName:L { @@ -903,8 +903,8 @@ protected TokenTree enumToDafnyFunction(final EnumShape enumShape) { pub fn to_dafny( value: $rustTypesModuleName:L::$rustEnumName:L, - ) -> ::std::rc::Rc{ - ::std::rc::Rc::new(match value { + ) -> ::dafny_runtime::Rc{ + ::dafny_runtime::Rc::new(match value { $branches:L _ => panic!("Unknown enum variant: {}", value), }) @@ -1268,7 +1268,7 @@ protected HashMap operationVariables( variables.put( "operationDafnyInputType", evalTemplate( - "&::std::rc::Rc", + "&::dafny_runtime::Rc", inputShapeVariables ) ); @@ -1297,7 +1297,7 @@ protected HashMap operationVariables( variables.put( "operationDafnyOutputType", evalTemplate( - "::std::rc::Rc", + "::dafny_runtime::Rc", outputShapeVariables ) ); @@ -1749,7 +1749,7 @@ protected String dafnyTypeForShape(final Shape originalShape) { EnumShape enumShape = ModelUtils.stringToEnumShape( shape.asStringShape().orElseThrow() ); - yield "::std::rc::Rc"; } - case ENUM -> "::std::rc::Rc "::dafny_runtime::Rc "::std::rc::Rc "::dafny_runtime::Rc"; - case UNION -> "::std::rc::Rc "::dafny_runtime::Rc Client { .unwrap() }); - impl dafny_runtime::UpcastObject for Client { - ::dafny_runtime::UpcastObjectFn!(dyn::std::any::Any); + impl dafny_runtime::UpcastObject<::dafny_runtime::DynAny> for Client { + ::dafny_runtime::UpcastObjectFn!(::dafny_runtime::DynAny); } impl dafny_runtime::UpcastObject for Client { @@ -160,17 +160,17 @@ fn into(self) -> Client { """ #[allow(non_snake_case)] impl crate::r#$dafnyInternalModuleName:L::_default { - pub fn $clientName:L() -> ::std::rc::Rc< + pub fn $clientName:L() -> ::dafny_runtime::Rc< crate::r#_Wrappers_Compile::Result< ::dafny_runtime::Object, - ::std::rc::Rc + ::dafny_runtime::Rc > > { let shared_config = dafny_tokio_runtime.block_on(aws_config::load_defaults(aws_config::BehaviorVersion::v2024_03_28())); let inner = $sdkCrate:L::Client::new(&shared_config); let client = Client { inner }; let dafny_client = ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(client)); - std::rc::Rc::new(crate::r#_Wrappers_Compile::Result::Success { value: dafny_client }) + dafny_runtime::Rc::new(crate::r#_Wrappers_Compile::Result::Success { value: dafny_client }) } } """, @@ -205,7 +205,7 @@ private TokenTree operationClientFunction( final String outputType = outputShape.hasTrait(UnitTypeTrait.class) ? "()" : evalTemplate( - "std::rc::Rc", + "dafny_runtime::Rc", variables ); variables.put("outputType", outputType); @@ -237,10 +237,10 @@ private TokenTree operationClientFunction( return TokenTree.of( evalTemplate( """ - fn $operationName:L(&self, input: &std::rc::Rc) - -> std::rc::Rc) + -> dafny_runtime::Rc + dafny_runtime::Rc > > { let inner_input = $rustRootModuleName:L::conversions::$snakeCaseOperationName:L::_$snakeCaseOperationName:L_request::from_dafny(input.clone()); @@ -416,10 +416,10 @@ protected TokenTree operationRequestToDafnyFunction( #[allow(dead_code)] pub fn to_dafny( value: &$sdkCrate:L::operation::$snakeCaseOperationName:L::$sdkOperationInputStruct:L, - ) -> ::std::rc::Rc< + ) -> ::dafny_runtime::Rc< crate::r#$dafnyTypesModuleName:L::$operationInputName:L, >{ - ::std::rc::Rc::new(crate::r#$dafnyTypesModuleName:L::$operationInputName:L::$operationInputName:L { + ::dafny_runtime::Rc::new(crate::r#$dafnyTypesModuleName:L::$operationInputName:L::$operationInputName:L { $variants:L }) } @@ -500,7 +500,7 @@ protected TokenTree operationRequestFromDafnyFunction( """ #[allow(dead_code)] pub fn from_dafny( - dafny_value: ::std::rc::Rc< + dafny_value: ::dafny_runtime::Rc< crate::r#$dafnyTypesModuleName:L::$operationInputName:L, > ) -> $sdkCrate:L::operation::$snakeCaseOperationName:L::$sdkOperationInputStruct:L { @@ -556,10 +556,10 @@ pub fn to_dafny( #[allow(dead_code)] pub fn to_dafny( value: &$sdkCrate:L::operation::$snakeCaseOperationName:L::$sdkOperationOutputStruct:L - ) -> ::std::rc::Rc< + ) -> ::dafny_runtime::Rc< crate::r#$dafnyTypesModuleName:L::$structureName:L, >{ - ::std::rc::Rc::new(crate::r#$dafnyTypesModuleName:L::$structureName:L::$structureName:L { + ::dafny_runtime::Rc::new(crate::r#$dafnyTypesModuleName:L::$structureName:L::$structureName:L { $variants:L }) } @@ -601,7 +601,7 @@ protected TokenTree operationResponseFromDafnyFunction( """ #[allow(dead_code)] pub fn from_dafny( - dafny_value: ::std::rc::Rc< + dafny_value: ::dafny_runtime::Rc< crate::r#$dafnyTypesModuleName:L::$operationOutputName:L, > ) -> $sdkCrate:L::operation::$snakeCaseOperationName:L::$sdkOperationOutputStruct:L { @@ -661,7 +661,7 @@ pub fn to_dafny_error( $sdkCrate:L::operation::$snakeCaseOperationName:L::$operationName:LError, ::aws_smithy_runtime_api::client::orchestrator::HttpResponse, >, - ) -> ::std::rc::Rc { + ) -> ::dafny_runtime::Rc { match value { $sdkCrate:L::error::SdkError::ServiceError(service_error) => match service_error.err() { $errorCases:L @@ -752,8 +752,8 @@ private RustFile errorConversionModule(final StructureShape errorStructure) { #[allow(dead_code)] pub fn to_dafny( value: $rustTypesModuleName:L::error::$pascalCaseName:L, - ) -> ::std::rc::Rc{ - ::std::rc::Rc::new( + ) -> ::dafny_runtime::Rc{ + ::dafny_runtime::Rc::new( crate::r#$dafnyTypesModuleName:L::Error::$structureName:L { $variants:L } @@ -860,7 +860,7 @@ protected TokenTree toDafny( if (isDafnyOption) { yield TokenTree.of( """ - ::std::rc::Rc::new(match &%s { + ::dafny_runtime::Rc::new(match &%s { Some(x) => crate::_Wrappers_Compile::Option::Some { value: %s::conversions::%s::to_dafny(x.clone()) }, None => crate::_Wrappers_Compile::Option::None { } }) @@ -900,7 +900,9 @@ protected TokenTree toDafny( } else { valueToDafny = rustToDafny.formatted(rustValue); } - yield TokenTree.of("::std::rc::Rc::new(%s)".formatted(valueToDafny)); + yield TokenTree.of( + "::dafny_runtime::Rc::new(%s)".formatted(valueToDafny) + ); } else { if (isRustOption) { var result = TokenTree.of( @@ -1067,7 +1069,7 @@ protected TokenTree toDafny( } else { yield TokenTree.of( """ - ::std::rc::Rc::new(match &%s { + ::dafny_runtime::Rc::new(match &%s { Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x, |e| %s, @@ -1115,7 +1117,7 @@ protected TokenTree toDafny( yield TokenTree.of( """ - ::std::rc::Rc::new(match &%s { + ::dafny_runtime::Rc::new(match &%s { Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, |k| %s, @@ -1151,7 +1153,7 @@ protected TokenTree toDafny( } else { yield TokenTree.of( """ - ::std::rc::Rc::new(match &%s { + ::dafny_runtime::Rc::new(match &%s { Some(x) => crate::_Wrappers_Compile::Option::Some { value: %s::conversions::%s::to_dafny(x) }, None => crate::_Wrappers_Compile::Option::None { } }) diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyrust/generator/RustLibraryShimGenerator.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyrust/generator/RustLibraryShimGenerator.java index b2f7033b2c..b568aecf4a 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyrust/generator/RustLibraryShimGenerator.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyrust/generator/RustLibraryShimGenerator.java @@ -853,7 +853,7 @@ private RustFile operationOuterModule( variables.put( "operationSendBody", evalTemplate( - "$snakeCaseResourceName:L.inner.borrow_mut().$snakeCaseOperationName:L(input)", + "$snakeCaseResourceName:L.inner.lock().unwrap().$snakeCaseOperationName:L(input)", MapUtils.merge( variables, resourceVariables(bindingShape.asResourceShape().orElseThrow()) @@ -2003,10 +2003,10 @@ private TokenTree operationStructureToDafnyFunction( #[allow(dead_code)] pub fn to_dafny( value: $rustRootModuleName:L::operation::$snakeCaseOperationName:L::$rustStructureName:L, - ) -> ::std::rc::Rc< + ) -> ::dafny_runtime::Rc< crate::r#$dafnyTypesModuleName:L::$structureName:L, >{ - ::std::rc::Rc::new(crate::r#$dafnyTypesModuleName:L::$structureName:L::$structureName:L { + ::dafny_runtime::Rc::new(crate::r#$dafnyTypesModuleName:L::$structureName:L::$structureName:L { $variants:L }) } @@ -2064,7 +2064,7 @@ private TokenTree operationStructureFromDafnyFunction( """ #[allow(dead_code)] pub fn from_dafny( - dafny_value: ::std::rc::Rc< + dafny_value: ::dafny_runtime::Rc< crate::r#$dafnyTypesModuleName:L::$structureName:L, >, ) -> $rustRootModuleName:L::operation::$snakeCaseOperationName:L::$rustStructureName:L { @@ -2364,7 +2364,7 @@ protected TokenTree toDafny( if (isDafnyOption) { yield TokenTree.of( """ - ::std::rc::Rc::new(match &%s { + ::dafny_runtime::Rc::new(match &%s { Some(x) => crate::_Wrappers_Compile::Option::Some { value: %s::conversions::%s::to_dafny(x.clone()) }, None => crate::_Wrappers_Compile::Option::None { } }) @@ -2396,7 +2396,7 @@ protected TokenTree toDafny( final String coercion = isDafnyOption ? "into()" : "Extract()"; yield TokenTree.of( """ - std::rc::Rc::new(match %s { + dafny_runtime::Rc::new(match %s { Some(s) => crate::_Wrappers_Compile::Option::Some { value: %s }, None => crate::_Wrappers_Compile::Option::None {}, }).%s""".formatted(rustValue, rustToDafny.formatted("s"), coercion) @@ -2577,7 +2577,7 @@ protected TokenTree toDafny( } else { yield TokenTree.of( """ - ::std::rc::Rc::new(match &%s { + ::dafny_runtime::Rc::new(match &%s { Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x, |e| %s, @@ -2625,7 +2625,7 @@ protected TokenTree toDafny( yield TokenTree.of( """ - ::std::rc::Rc::new(match &%s { + ::dafny_runtime::Rc::new(match &%s { Some(x) => crate::r#_Wrappers_Compile::Option::Some { value : ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x, |k| %s, @@ -2663,7 +2663,7 @@ protected TokenTree toDafny( } else { yield TokenTree.of( """ - ::std::rc::Rc::new(match &%s { + ::dafny_runtime::Rc::new(match &%s { Some(x) => crate::_Wrappers_Compile::Option::Some { value: %s::to_dafny(&x.clone()) }, None => crate::_Wrappers_Compile::Option::None { } }) @@ -2693,7 +2693,7 @@ protected TokenTree toDafny( } else { yield TokenTree.of( """ - ::std::rc::Rc::new(match &%s { + ::dafny_runtime::Rc::new(match &%s { Some(x) => crate::_Wrappers_Compile::Option::Some { value: %s::conversions::%s::to_dafny(&x.clone()) }, None => crate::_Wrappers_Compile::Option::None { } }) @@ -2720,7 +2720,7 @@ protected TokenTree toDafny( } else { yield TokenTree.of( """ - ::std::rc::Rc::new(match &%s { + ::dafny_runtime::Rc::new(match &%s { Some(x) => crate::_Wrappers_Compile::Option::Some { value: %s::conversions::client::to_dafny(&x.clone()) }, None => crate::_Wrappers_Compile::Option::None { } }) diff --git a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/client_awssdk.rs b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/client_awssdk.rs index 80dee8702d..be32854b12 100644 --- a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/client_awssdk.rs +++ b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/client_awssdk.rs @@ -10,8 +10,8 @@ pub fn to_dafny( ) -> ::dafny_runtime::Object { - let x: std::rc::Rc<$rustClientType:L> = std::rc::Rc::new(value.clone()); - let y = x as std::rc::Rc; + let x: dafny_runtime::Rc<$rustClientType:L> = dafny_runtime::Rc::new(value.clone()); + let y = x as dafny_runtime::Rc; unsafe { ::dafny_runtime::dafny_runtime_conversions::object::rc_struct_to_dafny_class(y) } diff --git a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/config/_config.rs b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/config/_config.rs index b37b7444d6..d5d7bbb26e 100644 --- a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/config/_config.rs +++ b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/config/_config.rs @@ -2,15 +2,15 @@ pub fn to_dafny( value: $rustTypesModuleName:L::$snakeCaseConfigName:L::$configName:L, -) -> ::std::rc::Rc< +) -> ::dafny_runtime::Rc< crate::r#$dafnyTypesModuleName:L::$configName:L, > { - ::std::rc::Rc::new(to_dafny_plain(value)) + ::dafny_runtime::Rc::new(to_dafny_plain(value)) } #[allow(dead_code)] pub fn from_dafny( - dafny_value: ::std::rc::Rc< + dafny_value: ::dafny_runtime::Rc< crate::r#$dafnyTypesModuleName:L::$configName:L, >, ) -> $rustTypesModuleName:L::$snakeCaseConfigName:L::$configName:L { diff --git a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/error_awssdk.rs b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/error_awssdk.rs index dfac406502..7710de42bb 100644 --- a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/error_awssdk.rs +++ b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/error_awssdk.rs @@ -1,15 +1,15 @@ pub fn to_dafny( value: $qualifiedRustServiceErrorType:L, -) -> ::std::rc::Rc { +) -> ::dafny_runtime::Rc { match value { $toDafnyArms:L $qualifiedRustServiceErrorType:L::Opaque { obj } => - ::std::rc::Rc::new(crate::r#$dafnyTypesModuleName:L::Error::Opaque { + ::dafny_runtime::Rc::new(crate::r#$dafnyTypesModuleName:L::Error::Opaque { obj: ::dafny_runtime::Object(obj.0) }), $qualifiedRustServiceErrorType:L::OpaqueWithText { obj, objMessage } => - ::std::rc::Rc::new(crate::r#$dafnyTypesModuleName:L::Error::OpaqueWithText { + ::dafny_runtime::Rc::new(crate::r#$dafnyTypesModuleName:L::Error::OpaqueWithText { obj: ::dafny_runtime::Object(obj.0), objMessage: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&objMessage), }), @@ -18,7 +18,7 @@ pub fn to_dafny( #[allow(dead_code)] pub fn from_dafny( - dafny_value: ::std::rc::Rc< + dafny_value: ::dafny_runtime::Rc< crate::r#$dafnyTypesModuleName:L::Error, >, ) -> $qualifiedRustServiceErrorType:L { diff --git a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/error_common.rs b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/error_common.rs index 5a5d576d4e..68fd91575e 100644 --- a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/error_common.rs +++ b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/error_common.rs @@ -1,13 +1,13 @@ /// Wraps up an arbitrary Rust Error value as a Dafny Error pub fn to_opaque_error(value: String) -> - ::std::rc::Rc + ::dafny_runtime::Rc { let error_msg = value.clone(); let error_msg = ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&error_msg); - let error_obj: ::dafny_runtime::Object = ::dafny_runtime::Object(Some( - ::std::rc::Rc::new(::std::cell::UnsafeCell::new(value)), + let error_obj: ::dafny_runtime::Object<::dafny_runtime::DynAny> = ::dafny_runtime::Object(Some( + ::dafny_runtime::Rc::new(::dafny_runtime::UnsafeCell::new(value)), )); - ::std::rc::Rc::new( + ::dafny_runtime::Rc::new( crate::r#$dafnyTypesModuleName:L::Error::OpaqueWithText { obj: error_obj, objMessage: error_msg @@ -17,14 +17,14 @@ pub fn to_opaque_error(value: String) -> /// Wraps up an arbitrary Rust Error value as a Dafny Result.Failure pub fn to_opaque_error_result(value: String) -> - ::std::rc::Rc< + ::dafny_runtime::Rc< crate::_Wrappers_Compile::Result< T, - ::std::rc::Rc + ::dafny_runtime::Rc > > { - ::std::rc::Rc::new(crate::_Wrappers_Compile::Result::Failure { + ::dafny_runtime::Rc::new(crate::_Wrappers_Compile::Result::Failure { error: to_opaque_error(value), }) } diff --git a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/error_library.rs b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/error_library.rs index 75c5be4bc1..de05facdb5 100644 --- a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/error_library.rs +++ b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/error_library.rs @@ -1,8 +1,8 @@ pub fn to_dafny( value: $qualifiedRustServiceErrorType:L, -) -> ::std::rc::Rc { - ::std::rc::Rc::new(match value { +) -> ::dafny_runtime::Rc { + ::dafny_runtime::Rc::new(match value { $toDafnyArms:L $qualifiedRustServiceErrorType:L::CollectionOfErrors { list, message } => crate::r#$dafnyTypesModuleName:L::Error::CollectionOfErrors { @@ -12,7 +12,7 @@ pub fn to_dafny( $qualifiedRustServiceErrorType:L::ValidationError(inner) => crate::r#$dafnyTypesModuleName:L::Error::Opaque { obj: { - let rc = ::std::rc::Rc::new(inner) as ::std::rc::Rc; + let rc = ::dafny_runtime::Rc::new(inner) as ::dafny_runtime::Rc<::dafny_runtime::DynAny>; // 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) @@ -33,7 +33,7 @@ pub fn to_dafny( #[allow(dead_code)] pub fn from_dafny( - dafny_value: ::std::rc::Rc< + dafny_value: ::dafny_runtime::Rc< crate::r#$dafnyTypesModuleName:L::Error, >, ) -> $qualifiedRustServiceErrorType:L { diff --git a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/resource.rs b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/resource.rs index e2f90c4395..fee042f5a3 100644 --- a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/resource.rs +++ b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/resource.rs @@ -7,7 +7,7 @@ pub fn to_dafny( let wrap = $rustResourceName:LWrapper { obj: value.clone(), }; - let inner = ::std::rc::Rc::new(::std::cell::UnsafeCell::new(wrap)); + let inner = ::dafny_runtime::Rc::new(::dafny_runtime::UnsafeCell::new(wrap)); ::dafny_runtime::Object (Some(inner) ) } @@ -15,8 +15,8 @@ pub struct $rustResourceName:LWrapper { obj: $rustTypesModuleName:L::$snakeCaseResourceName:L::$rustResourceName:LRef, } -impl ::dafny_runtime::UpcastObject for $rustResourceName:LWrapper { - ::dafny_runtime::UpcastObjectFn!(dyn ::std::any::Any); +impl ::dafny_runtime::UpcastObject<::dafny_runtime::DynAny> for $rustResourceName:LWrapper { + ::dafny_runtime::UpcastObjectFn!(::dafny_runtime::DynAny); } #[allow(dead_code)] @@ -29,7 +29,7 @@ pub fn from_dafny( obj: dafny_value.clone(), }; $rustTypesModuleName:L::$snakeCaseResourceName:L::$rustResourceName:LRef { - inner: ::std::rc::Rc::new(::std::cell::RefCell::new(wrap)) + inner: ::dafny_runtime::Rc::new(::dafny_runtime::RefCell::new(wrap)) } } diff --git a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/resource_wrapper_operation.rs b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/resource_wrapper_operation.rs index 6b2a688a55..d28848b0e9 100644 --- a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/resource_wrapper_operation.rs +++ b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/resource_wrapper_operation.rs @@ -1,15 +1,15 @@ fn r#_$operationName:L_k( &self, input: $operationDafnyInputType:L, -) -> ::std::rc::Rc< +) -> ::dafny_runtime::Rc< crate::r#_Wrappers_Compile::Result< $operationDafnyOutputType:L, - ::std::rc::Rc, + ::dafny_runtime::Rc, >, > { let inner_input = $inputFromDafny:L; - let inner_result = self.obj.inner.borrow_mut().$snakeCaseOperationName:L(inner_input); + let inner_result = self.obj.inner.lock().unwrap().$snakeCaseOperationName:L(inner_input); let result = match inner_result { Ok(x) => crate::r#_Wrappers_Compile::Result::Success { value: $outputToDafny:L, @@ -18,5 +18,5 @@ fn r#_$operationName:L_k( error: $rustRootModuleName:L::conversions::error::to_dafny(x), }, }; - ::std::rc::Rc::new(result) + ::dafny_runtime::Rc::new(result) } \ No newline at end of file diff --git a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/standard_structure.rs b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/standard_structure.rs index ca6869c2f9..3d4e3c46da 100644 --- a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/standard_structure.rs +++ b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/standard_structure.rs @@ -1,10 +1,10 @@ #[allow(dead_code)] pub fn to_dafny( value: &$qualifiedRustStructureType:L, -) -> ::std::rc::Rc< +) -> ::dafny_runtime::Rc< crate::r#$dafnyTypesModuleName:L::$structureName:L, > { - ::std::rc::Rc::new(to_dafny_plain(value.clone())) + ::dafny_runtime::Rc::new(to_dafny_plain(value.clone())) } #[allow(dead_code)] @@ -19,20 +19,20 @@ pub fn to_dafny_plain( #[allow(dead_code)] pub fn option_to_dafny( value: ::std::option::Option<$qualifiedRustStructureType:L>, -) -> ::std::rc::Rc ::dafny_runtime::Rc>>{ - ::std::rc::Rc::new(match value { + ::dafny_runtime::Rc::new(match value { ::std::option::Option::None => crate::_Wrappers_Compile::Option::None {}, ::std::option::Option::Some(x) => crate::_Wrappers_Compile::Option::Some { - value: ::std::rc::Rc::new(to_dafny_plain(x)), + value: ::dafny_runtime::Rc::new(to_dafny_plain(x)), }, }) } #[allow(dead_code)] pub fn from_dafny( - dafny_value: ::std::rc::Rc< + dafny_value: ::dafny_runtime::Rc< crate::r#$dafnyTypesModuleName:L::$structureName:L, >, ) -> $qualifiedRustStructureType:L { @@ -54,7 +54,7 @@ pub fn plain_from_dafny( #[allow(dead_code)] pub fn option_from_dafny( - dafny_value: ::std::rc::Rc>>, ) -> ::std::option::Option<$qualifiedRustStructureType:L> { diff --git a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/union.rs b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/union.rs index 199e095b4b..9cdfa303be 100644 --- a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/union.rs +++ b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/union.rs @@ -1,10 +1,10 @@ #[allow(dead_code)] pub fn to_dafny( value: &$qualifiedRustUnionName:L, -) -> ::std::rc::Rc< +) -> ::dafny_runtime::Rc< crate::r#$dafnyTypesModuleName:L::$dafnyUnionName:L, > { - ::std::rc::Rc::new(match value { + ::dafny_runtime::Rc::new(match value { $toDafnyVariants:L _ => panic!("Unknown union variant: {:?}", value), }) @@ -12,11 +12,11 @@ pub fn to_dafny( #[allow(dead_code)] pub fn from_dafny( - dafny_value: ::std::rc::Rc< + dafny_value: ::dafny_runtime::Rc< crate::r#$dafnyTypesModuleName:L::$dafnyUnionName:L, >, ) -> $qualifiedRustUnionName:L { - match &::std::rc::Rc::unwrap_or_clone(dafny_value) { + match &::dafny_runtime::Rc::unwrap_or_clone(dafny_value) { $fromDafnyVariants:L } } \ No newline at end of file diff --git a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/error/sealed_unhandled.rs b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/error/sealed_unhandled.rs index ba56c61ad6..5131559b97 100644 --- a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/error/sealed_unhandled.rs +++ b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/error/sealed_unhandled.rs @@ -24,6 +24,6 @@ pub struct Unhandled { pub(crate) meta: ::aws_smithy_types::error::metadata::ErrorMetadata, } -impl UpcastObject for Unhandled { - ::dafny_runtime::UpcastObjectFn!(dyn ::std::any::Any); +impl UpcastObject<::dafny_runtime::DynAny> for Unhandled { + ::dafny_runtime::UpcastObjectFn!(::dafny_runtime::DynAny); } \ No newline at end of file diff --git a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/operation/builders.rs b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/operation/builders.rs index 15a3fa4e24..5ffed2aec7 100644 --- a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/operation/builders.rs +++ b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/operation/builders.rs @@ -52,7 +52,7 @@ impl $pascalCaseOperationName:LFluentBuilder { .map_err(|mut e| { let msg = format!("{:?}", e); $qualifiedRustServiceErrorType:L::OpaqueWithText { - obj: ::dafny_runtime::Object::from_ref(&mut e as &mut dyn ::std::any::Any), + obj: ::dafny_runtime::Object::from_ref(&mut e as &mut ::dafny_runtime::DynAny), objMessage: msg }})?; $rustRootModuleName:L::operation::$snakeCaseOperationName:L::$pascalCaseOperationName:L::send(&self.$operationTargetName:L, input).await diff --git a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/src/standard_library_conversions.rs b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/src/standard_library_conversions.rs index 5c00049018..636e25a269 100644 --- a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/src/standard_library_conversions.rs +++ b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/src/standard_library_conversions.rs @@ -3,7 +3,7 @@ pub fn ostring_to_dafny( input: &Option, -) -> ::std::rc::Rc< +) -> ::dafny_runtime::Rc< crate::_Wrappers_Compile::Option<::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>>, > { let dafny_value = match input { @@ -12,11 +12,11 @@ pub fn ostring_to_dafny( }, None => crate::_Wrappers_Compile::Option::None {}, }; - ::std::rc::Rc::new(dafny_value) + ::dafny_runtime::Rc::new(dafny_value) } pub fn ostring_from_dafny( - input: ::std::rc::Rc< + input: ::dafny_runtime::Rc< crate::_Wrappers_Compile::Option< ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, >, @@ -38,16 +38,16 @@ pub fn ostring_from_dafny( pub fn obool_to_dafny( input: &Option, -) -> ::std::rc::Rc> { +) -> ::dafny_runtime::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) + ::dafny_runtime::Rc::new(dafny_value) } pub fn obool_from_dafny( - input: ::std::rc::Rc>, + input: ::dafny_runtime::Rc>, ) -> Option { if matches!( input.as_ref(), @@ -59,15 +59,15 @@ pub fn obool_from_dafny( } } -pub fn oint_to_dafny(input: Option) -> ::std::rc::Rc> { +pub fn oint_to_dafny(input: Option) -> ::dafny_runtime::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) + ::dafny_runtime::Rc::new(dafny_value) } -pub fn oint_from_dafny(input: ::std::rc::Rc>) -> Option { +pub fn oint_from_dafny(input: ::dafny_runtime::Rc>) -> Option { if matches!( input.as_ref(), crate::_Wrappers_Compile::Option::Some { .. } @@ -78,16 +78,16 @@ pub fn oint_from_dafny(input: ::std::rc::Rc) -> ::std::rc::Rc> { +pub fn olong_to_dafny(input: &Option) -> ::dafny_runtime::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) + ::dafny_runtime::Rc::new(dafny_value) } pub fn olong_from_dafny( - input: ::std::rc::Rc>, + input: ::dafny_runtime::Rc>, ) -> Option { if matches!( input.as_ref(), @@ -105,24 +105,24 @@ pub fn blob_to_dafny(input: &::aws_smithy_types::Blob) -> ::dafny_runtime::Seque pub fn oblob_to_dafny( input: &Option<::aws_smithy_types::Blob>, -) -> ::std::rc::Rc>> { +) -> ::dafny_runtime::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) + ::dafny_runtime::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()), + ::dafny_runtime::Rc::try_unwrap(input.to_array()).unwrap_or_else(|rc| (*rc).clone()), ) } pub fn oblob_from_dafny( - input: ::std::rc::Rc>>, + input: ::dafny_runtime::Rc>>, ) -> Option<::aws_smithy_types::Blob> { if matches!( input.as_ref(), @@ -143,14 +143,14 @@ pub fn double_to_dafny(input: f64) -> ::dafny_runtime::Sequence { pub fn odouble_to_dafny( input: &Option, -) -> ::std::rc::Rc>> { +) -> ::dafny_runtime::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) + ::dafny_runtime::Rc::new(dafny_value) } pub fn double_from_dafny(input: &::dafny_runtime::Sequence) -> f64 { @@ -159,7 +159,7 @@ pub fn double_from_dafny(input: &::dafny_runtime::Sequence) -> f64 { } pub fn odouble_from_dafny( - input: ::std::rc::Rc>>, + input: ::dafny_runtime::Rc>>, ) -> Option { if matches!( input.as_ref(), @@ -181,7 +181,7 @@ pub fn timestamp_to_dafny( pub fn otimestamp_to_dafny( input: &Option<::aws_smithy_types::DateTime>, -) -> ::std::rc::Rc< +) -> ::dafny_runtime::Rc< crate::_Wrappers_Compile::Option<::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>>, > { let dafny_value = match input { @@ -190,7 +190,7 @@ pub fn otimestamp_to_dafny( }, None => crate::_Wrappers_Compile::Option::None {}, }; - ::std::rc::Rc::new(dafny_value) + ::dafny_runtime::Rc::new(dafny_value) } pub fn timestamp_from_dafny( @@ -204,7 +204,7 @@ pub fn timestamp_from_dafny( } pub fn otimestamp_from_dafny( - input: ::std::rc::Rc< + input: ::dafny_runtime::Rc< crate::_Wrappers_Compile::Option< ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, >, @@ -221,7 +221,7 @@ pub fn otimestamp_from_dafny( } pub fn option_from_dafny( - input: ::std::rc::Rc>, + input: ::dafny_runtime::Rc>, converter: fn(&T) -> TR, ) -> Option { match &*input { @@ -233,17 +233,17 @@ pub fn option_from_dafny( pub fn option_to_dafny( input: &Option, converter: fn(&TR) -> T, -) -> ::std::rc::Rc> { +) -> ::dafny_runtime::Rc> { match input { - Some(value) => ::std::rc::Rc::new(crate::_Wrappers_Compile::Option::Some { + Some(value) => ::dafny_runtime::Rc::new(crate::_Wrappers_Compile::Option::Some { value: converter(&value), }), - None => ::std::rc::Rc::new(crate::_Wrappers_Compile::Option::None {}), + None => ::dafny_runtime::Rc::new(crate::_Wrappers_Compile::Option::None {}), } } pub fn result_from_dafny( - input: ::std::rc::Rc>, + input: ::dafny_runtime::Rc>, converter_t: fn(&T) -> TR, converter_e: fn(&E) -> ER, ) -> Result { @@ -257,12 +257,12 @@ pub fn result_to_dafny, converter_t: fn(&TR) -> T, converter_e: fn(&ER) -> E, -) -> ::std::rc::Rc> { +) -> ::dafny_runtime::Rc> { match input { - Ok(value) => ::std::rc::Rc::new(crate::_Wrappers_Compile::Result::Success { + Ok(value) => ::dafny_runtime::Rc::new(crate::_Wrappers_Compile::Result::Success { value: converter_t(&value), }), - Err(error) => ::std::rc::Rc::new(crate::_Wrappers_Compile::Result::Failure { + Err(error) => ::dafny_runtime::Rc::new(crate::_Wrappers_Compile::Result::Failure { error: converter_e(&error), }), } diff --git a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/src/standard_library_externs.rs b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/src/standard_library_externs.rs index 54198eafa0..6165ee389c 100644 --- a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/src/standard_library_externs.rs +++ b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/src/standard_library_externs.rs @@ -8,7 +8,7 @@ use crate::implementation_from_dafny::UTF8; impl crate::implementation_from_dafny::UTF8::_default { pub fn Encode( s: &::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, - ) -> ::std::rc::Rc< + ) -> ::dafny_runtime::Rc< r#_Wrappers_Compile::Result< UTF8::ValidUTF8Bytes, ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, @@ -35,7 +35,7 @@ impl crate::implementation_from_dafny::UTF8::_default { surrogate = Some(c.0); continue; } - return ::std::rc::Rc::new(r#_Wrappers_Compile::Result::>::Failure { + return ::dafny_runtime::Rc::new(r#_Wrappers_Compile::Result::>::Failure { error: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string( &e.to_string()) }); @@ -43,12 +43,12 @@ impl crate::implementation_from_dafny::UTF8::_default { } } if let Some(s) = surrogate { - return ::std::rc::Rc::new(r#_Wrappers_Compile::Result::>::Failure { + return ::dafny_runtime::Rc::new(r#_Wrappers_Compile::Result::>::Failure { error: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string( &format!("Surrogate pair missing: 0x{:04x}", s)) }); } - ::std::rc::Rc::new(r#_Wrappers_Compile::Result::< + ::dafny_runtime::Rc::new(r#_Wrappers_Compile::Result::< UTF8::ValidUTF8Bytes, ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, >::Success { @@ -57,7 +57,7 @@ impl crate::implementation_from_dafny::UTF8::_default { } pub fn Decode( b: &::dafny_runtime::Sequence, - ) -> ::std::rc::Rc< + ) -> ::dafny_runtime::Rc< r#_Wrappers_Compile::Result< ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, @@ -66,13 +66,13 @@ impl crate::implementation_from_dafny::UTF8::_default { let b = String::from_utf8(b.to_array().as_ref().clone()); match b { Ok(s) => { - ::std::rc::Rc::new(r#_Wrappers_Compile::Result::<::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + ::dafny_runtime::Rc::new(r#_Wrappers_Compile::Result::<::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>>::Success { value: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&s) }) }, Err(e) => { - return ::std::rc::Rc::new(r#_Wrappers_Compile::Result::<::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + return ::dafny_runtime::Rc::new(r#_Wrappers_Compile::Result::<::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>>::Failure { error: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string( &e.to_string()) diff --git a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/types/error.rs b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/types/error.rs index 9d3142f828..5912a2a05f 100644 --- a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/types/error.rs +++ b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/types/error.rs @@ -7,10 +7,10 @@ pub enum Error { }, ValidationError(ValidationError), Opaque { - obj: ::dafny_runtime::Object, + obj: ::dafny_runtime::Object<::dafny_runtime::DynAny>, }, OpaqueWithText { - obj: ::dafny_runtime::Object, + obj: ::dafny_runtime::Object<::dafny_runtime::DynAny>, objMessage: ::std::string::String, }, } @@ -38,18 +38,18 @@ impl ::std::error::Error for Error { impl Error { pub fn wrap_validation_err(err: E) -> Self where - E: ::std::error::Error + 'static, + E: ::std::error::Error + Send + Sync + 'static, { - Self::ValidationError(ValidationError(::std::rc::Rc::new(err))) + Self::ValidationError(ValidationError(::dafny_runtime::Rc::new(err))) } } #[derive(::std::clone::Clone, ::std::fmt::Debug)] -pub struct ValidationError(::std::rc::Rc); +pub struct ValidationError(::dafny_runtime::Rc); impl ::std::cmp::PartialEq for ValidationError { fn eq(&self, other: &Self) -> bool { - ::std::rc::Rc::<(dyn std::error::Error + 'static)>::ptr_eq(&self.0, &other.0) + ::dafny_runtime::Rc::<(dyn std::error::Error + Send + Sync + 'static)>::ptr_eq(&self.0, &other.0) } } diff --git a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/types/error_awssdk.rs b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/types/error_awssdk.rs index e761e9d8c5..e6befee17b 100644 --- a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/types/error_awssdk.rs +++ b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/types/error_awssdk.rs @@ -2,10 +2,10 @@ pub enum Error { $modeledErrorVariants:L Opaque { - obj: ::dafny_runtime::Object, + obj: ::dafny_runtime::Object<::dafny_runtime::DynAny>, }, OpaqueWithText { - obj: ::dafny_runtime::Object, + obj: ::dafny_runtime::Object<::dafny_runtime::DynAny>, objMessage: ::std::string::String, }, } diff --git a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/types/resource.rs b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/types/resource.rs index 6d57e14582..dd8dae6dcc 100644 --- a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/types/resource.rs +++ b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/types/resource.rs @@ -1,24 +1,24 @@ $rustResourceComment:L -pub trait $rustResourceName:L { +pub trait $rustResourceName:L : Send + Sync { $resourceOperations:L } #[derive(::std::clone::Clone)] /// A reference to a $rustResourceName:L pub struct $rustResourceName:LRef { - pub inner: ::std::rc::Rc> + pub inner: ::dafny_runtime::Rc<::dafny_runtime::RefCell> } impl From for $rustResourceName:LRef { fn from(value: T) -> Self { - Self { inner: std::rc::Rc::new(std::cell::RefCell::new(value)) } + Self { inner: dafny_runtime::Rc::new(::dafny_runtime::RefCell::new(value)) } } } impl ::std::cmp::PartialEq for $rustResourceName:LRef { fn eq(&self, other: &$rustResourceName:LRef) -> bool { - ::std::rc::Rc::ptr_eq(&self.inner, &other.inner) + ::dafny_runtime::Rc::ptr_eq(&self.inner, &other.inner) } } diff --git a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/wrapped.rs b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/wrapped.rs index 83b6b90367..71479c64f8 100644 --- a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/wrapped.rs +++ b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/wrapped.rs @@ -1,11 +1,11 @@ pub mod client; impl crate::r#$dafnyInternalModuleName:L::wrapped::_default { - pub fn Wrapped$sdkId:L(config: &::std::rc::Rc< + pub fn Wrapped$sdkId:L(config: &::dafny_runtime::Rc< crate::r#$dafnyTypesModuleName:L::$configName:L, - >) -> ::std::rc::Rc) -> ::dafny_runtime::Rc, - ::std::rc::Rc + ::dafny_runtime::Rc >>{ $rustRootModuleName:L::wrapped::client::Client::from_conf(config) } diff --git a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/wrapped/client.rs b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/wrapped/client.rs index 703b613e30..3887f4da49 100644 --- a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/wrapped/client.rs +++ b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/wrapped/client.rs @@ -17,17 +17,17 @@ impl dafny_runtime::UpcastObject for Client { - ::dafny_runtime::UpcastObjectFn!(dyn ::std::any::Any); +impl dafny_runtime::UpcastObject<::dafny_runtime::DynAny> for Client { + ::dafny_runtime::UpcastObjectFn!(::dafny_runtime::DynAny); } impl Client { - pub fn from_conf(config: &::std::rc::Rc< + pub fn from_conf(config: &::dafny_runtime::Rc< crate::r#$dafnyTypesModuleName:L::$configName:L, >) -> -::std::rc::Rc, - ::std::rc::Rc + ::dafny_runtime::Rc >> { let result = $rustRootModuleName:L::client::Client::from_conf( $rustRootModuleName:L::conversions::$snakeCaseConfigName:L::_$snakeCaseConfigName:L::from_dafny( @@ -39,7 +39,7 @@ impl Client { let wrap = $rustRootModuleName:L::wrapped::client::Client { wrapped: client }; - std::rc::Rc::new( + dafny_runtime::Rc::new( crate::_Wrappers_Compile::Result::Success { value: ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(wrap)) } diff --git a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/wrapped/client_operation_impl.part.rs b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/wrapped/client_operation_impl.part.rs index 767854c691..52b0cd4494 100644 --- a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/wrapped/client_operation_impl.part.rs +++ b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/wrapped/client_operation_impl.part.rs @@ -1,9 +1,9 @@ fn $operationName:L( $operationInputParams:L - ) -> std::rc::Rc< + ) -> dafny_runtime::Rc< crate::r#_Wrappers_Compile::Result< $operationOutputDafnyType:L, - std::rc::Rc, + dafny_runtime::Rc, >, >{ let inner_input = $inputFromDafny:L; @@ -11,12 +11,12 @@ dafny_tokio_runtime.block_on($rustRootModuleName:L::operation::$snakeCaseOperationName:L::$pascalCaseOperationName:L::send(&self.wrapped, inner_input)) }); match result { - Err(error) => ::std::rc::Rc::new( + Err(error) => ::dafny_runtime::Rc::new( crate::_Wrappers_Compile::Result::Failure { error: $rustRootModuleName:L::conversions::error::to_dafny(error), }, ), - Ok(inner_result) => ::std::rc::Rc::new( + Ok(inner_result) => ::dafny_runtime::Rc::new( crate::_Wrappers_Compile::Result::Success { value: $outputToDafny:L, },