diff --git a/SmithyDafnyMakefile.mk b/SmithyDafnyMakefile.mk index 6c869e119..0d4cf146d 100644 --- a/SmithyDafnyMakefile.mk +++ b/SmithyDafnyMakefile.mk @@ -242,6 +242,7 @@ transpile_test: -functionSyntax:3 \ -useRuntimeLib \ -out $(OUT) \ + $(DAFNY_OPTIONS) \ $(if $(strip $(STD_LIBRARY)) , -library:$(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy, ) \ $(TRANSPILE_DEPENDENCIES) \ @@ -251,6 +252,10 @@ transpile_dependencies: $(if $(strip $(STD_LIBRARY)), $(MAKE) -C $(PROJECT_ROOT)/$(STD_LIBRARY) transpile_implementation_$(LANG), ) $(patsubst %, $(MAKE) -C $(PROJECT_ROOT)/% transpile_implementation_$(LANG);, $(PROJECT_DEPENDENCIES)) +transpile_dependencies_test: + $(if $(strip $(STD_LIBRARY)), $(MAKE) -C $(PROJECT_ROOT)/$(STD_LIBRARY) transpile_test_$(LANG), ) + $(patsubst %, $(MAKE) -C $(PROJECT_ROOT)/% transpile_test_$(LANG);, $(PROJECT_DEPENDENCIES)) + ########################## Code-Gen targets # The OUTPUT variables are created this way @@ -296,6 +301,7 @@ _polymorph_wrapped: $(OUTPUT_DAFNY_WRAPPED) \ $(OUTPUT_DOTNET_WRAPPED) \ $(OUTPUT_JAVA_WRAPPED) \ + $(OUTPUT_RUST_WRAPPED) \ --model $(if $(DIR_STRUCTURE_V2),$(LIBRARY_ROOT)/dafny/$(SERVICE)/Model,$(LIBRARY_ROOT)/Model) \ --dependent-model $(PROJECT_ROOT)/$(SMITHY_DEPS) \ $(patsubst %, --dependent-model $(PROJECT_ROOT)/%/Model, $($(service_deps_var))) \ @@ -510,10 +516,11 @@ test_java: ########################## Rust targets -# TODO: Dafny test transpilation needs manual patching to work too, -# which isn't a high priority at this stage, -# so don't include transpile_test_rust for now. -transpile_rust: | transpile_implementation_rust transpile_dependencies_rust +# Note that transpile_dependencies_test_rust is necessary +# only because we are patching test code in the StandardLibrary, +# so we don't transpile that code then the recursive call to polymorph_rust +# on the StandardLibrary will fail because the patch does not apply. +transpile_rust: | transpile_implementation_rust transpile_test_rust transpile_dependencies_rust transpile_dependencies_test_rust transpile_implementation_rust: TARGET=rs transpile_implementation_rust: OUT=implementation_from_dafny @@ -535,6 +542,9 @@ transpile_test_rust: _transpile_test_all _mv_test_rust transpile_dependencies_rust: LANG=rust transpile_dependencies_rust: transpile_dependencies +transpile_dependencies_test_rust: LANG=rust +transpile_dependencies_test_rust: transpile_dependencies_test + _mv_implementation_rust: rm -rf runtimes/rust/dafny_impl/src mkdir -p runtimes/rust/dafny_impl/src @@ -544,10 +554,10 @@ _mv_implementation_rust: rustfmt runtimes/rust/dafny_impl/src/implementation_from_dafny.rs rm -rf implementation_from_dafny-rust _mv_test_rust: - rm -rf runtimes/rust/dafny_impl/tests - mkdir -p runtimes/rust/dafny_impl/tests - mv tests_from_dafny-rust/src/tests_from_dafny.rs runtimes/rust/dafny_impl/tests/tests_from_dafny.rs - rustfmt runtimes/rust/dafny_impl/tests/tests_from_dafny.rs + rm -f runtimes/rust/tests/tests_from_dafny/mod.rs + mkdir -p runtimes/rust/tests/tests_from_dafny + mv tests_from_dafny-rust/src/tests_from_dafny.rs runtimes/rust/tests/tests_from_dafny/mod.rs + rustfmt runtimes/rust/tests/tests_from_dafny/mod.rs rm -rf tests_from_dafny-rust build_rust: diff --git a/TestModels/SharedMakefile.mk b/TestModels/SharedMakefile.mk index c1a4384ae..975ba217a 100644 --- a/TestModels/SharedMakefile.mk +++ b/TestModels/SharedMakefile.mk @@ -69,3 +69,12 @@ _polymorph_dotnet: _polymorph _polymorph_dotnet: OUTPUT_DOTNET_WRAPPED=\ $(if $(DIR_STRUCTURE_V2), --output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/Wrapped/$(SERVICE)/, --output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/Wrapped) _polymorph_dotnet: _polymorph_wrapped + +_polymorph_rust: OUTPUT_RUST=--output-rust $(LIBRARY_ROOT)/runtimes/rust +_polymorph_rust: INPUT_DAFNY=\ + --include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy +_polymorph_rust: _polymorph +# TODO: This doesn't yet work for Rust because we are patching transpiled code, +# so this target will complain about "patch does not apply" because it was already applied. +# _polymorph_rust: OUTPUT_RUST_WRAPPED=--output-rust $(LIBRARY_ROOT)/runtimes/rust +# _polymorph_rust: _polymorph_wrapped diff --git a/TestModels/SimpleTypes/SimpleBoolean/codegen-patches/rust/dafny-4.5.0.patch b/TestModels/SimpleTypes/SimpleBoolean/codegen-patches/rust/dafny-4.5.0.patch index 9973c302c..c0f0725f0 100644 --- a/TestModels/SimpleTypes/SimpleBoolean/codegen-patches/rust/dafny-4.5.0.patch +++ b/TestModels/SimpleTypes/SimpleBoolean/codegen-patches/rust/dafny-4.5.0.patch @@ -62,14 +62,54 @@ index 00000000..299b0baa +} diff --git b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/conversions.rs a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/conversions.rs new file mode 100644 -index 00000000..c1acac7b +index 00000000..86f87891 --- /dev/null +++ a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/conversions.rs -@@ -0,0 +1,4 @@ +@@ -0,0 +1,6 @@ +// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. +pub mod get_boolean; + +pub mod simple_boolean_config; ++ ++pub(crate) mod error; +\ No newline at end of file +diff --git b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/conversions/error.rs a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/conversions/error.rs +new file mode 100644 +index 00000000..d6fd32b7 +--- /dev/null ++++ a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/conversions/error.rs +@@ -0,0 +1,30 @@ ++/// Wraps up an arbitrary Rust Error value as a Dafny Error ++pub fn to_opaque_error(value: E) -> ++ ::std::rc::Rc<::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::Error> ++{ ++ let error_obj: ::dafny_runtime::Object = ++ ::dafny_runtime::Object(Some(::std::rc::Rc::new( ++ ::std::cell::UnsafeCell::new(value), ++ ))); ++ ::std::rc::Rc::new( ++ ::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::Error::Opaque { ++ obj: error_obj, ++ }, ++ ) ++} ++ ++/// Wraps up an arbitrary Rust Error value as a Dafny Result.Failure ++pub fn to_opaque_error_result(value: E) -> ++ ::std::rc::Rc< ++ dafny_standard_library::implementation_from_dafny::_Wrappers_Compile::Result< ++ T, ++ ::std::rc::Rc<::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::Error> ++ > ++ > ++{ ++ ::std::rc::Rc::new( ++ dafny_standard_library::implementation_from_dafny::_Wrappers_Compile::Result::Failure { ++ error: to_opaque_error(value) ++ } ++ ) ++} +\ No newline at end of file diff --git b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/conversions/get_boolean.rs a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/conversions/get_boolean.rs new file mode 100644 index 00000000..065d3ad3 @@ -287,10 +327,10 @@ index 00000000..4d66eb2e \ No newline at end of file diff --git b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/lib.rs a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/lib.rs new file mode 100644 -index 00000000..1d16c191 +index 00000000..53977d7d --- /dev/null +++ a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/lib.rs -@@ -0,0 +1,17 @@ +@@ -0,0 +1,20 @@ +#![allow(deprecated)] + +// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT. @@ -306,6 +346,9 @@ index 00000000..1d16c191 + +mod conversions; + ++#[cfg(feature = "wrapped-client")] ++pub mod wrapped; ++ +pub use client::Client; +pub use types::simple_boolean_config::SimpleBooleanConfig; diff --git b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/operation.rs a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/operation.rs @@ -719,3 +762,118 @@ index 00000000..6bf027f6 + ::std::result::Result::Ok(SimpleBooleanConfig {}) + } +} +diff --git b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/wrapped.rs a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/wrapped.rs +new file mode 100644 +index 00000000..39355176 +--- /dev/null ++++ a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/wrapped.rs +@@ -0,0 +1 @@ ++pub mod client; +\ No newline at end of file +diff --git b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/wrapped/client.rs a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/wrapped/client.rs +new file mode 100644 +index 00000000..49c75f76 +--- /dev/null ++++ a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/wrapped/client.rs +@@ -0,0 +1,88 @@ ++use tokio::runtime::Runtime; ++ ++pub struct Client { ++ wrapped: crate::client::Client, ++ ++ /// A `current_thread` runtime for executing operations on the ++ /// asynchronous client in a blocking manner. ++ rt: Runtime ++} ++ ++impl dafny_runtime::UpcastObject for Client { ++ ::dafny_runtime::UpcastObjectFn!(dyn ::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::ISimpleTypesBooleanClient); ++} ++ ++impl dafny_runtime::UpcastObject for Client { ++ ::dafny_runtime::UpcastObjectFn!(dyn ::std::any::Any); ++} ++ ++impl Client { ++ pub fn from_conf(config: &::std::rc::Rc< ++ ::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::SimpleBooleanConfig, ++ >) -> ++::std::rc::Rc<::simple_boolean_dafny::r#_Wrappers_Compile::Result< ++ ::dafny_runtime::Object, ++ ::std::rc::Rc<::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::Error> ++>> { ++ let rt_result = tokio::runtime::Builder::new_current_thread() ++ .enable_all() ++ .build(); ++ let rt = match rt_result { ++ Ok(x) => x, ++ Err(error) => return crate::conversions::error::to_opaque_error_result(error), ++ }; ++ let result = crate::client::Client::from_conf( ++ crate::conversions::simple_boolean_config::_simple_boolean_config::from_dafny( ++ config.clone(), ++ ), ++ ); ++ match result { ++ Ok(client) => { ++ let wrap = crate::wrapped::client::Client { ++ wrapped: client, ++ rt ++ }; ++ std::rc::Rc::new( ++ ::simple_boolean_dafny::_Wrappers_Compile::Result::Success { ++ value: ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(wrap)) ++ } ++ ) ++ }, ++ Err(error) => crate::conversions::error::to_opaque_error_result(error) ++ } ++ } ++} ++ ++impl ::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::ISimpleTypesBooleanClient ++ for Client ++{ ++ fn GetBoolean( ++ &mut self, ++ input: &std::rc::Rc< ++ ::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::GetBooleanInput, ++ >, ++ ) -> std::rc::Rc< ++ ::simple_boolean_dafny::r#_Wrappers_Compile::Result< ++ std::rc::Rc< ++ ::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::GetBooleanOutput, ++ >, ++ std::rc::Rc<::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::Error>, ++ >, ++ >{ ++ let inner_input = ++ crate::conversions::get_boolean::_get_boolean_input::from_dafny(input.clone()); ++ let result = self.rt.block_on(crate::operation::get_boolean::GetBoolean::send(&self.wrapped, inner_input)); ++ match result { ++ Err(error) => ::std::rc::Rc::new( ++ ::simple_boolean_dafny::_Wrappers_Compile::Result::Failure { ++ error: crate::conversions::get_boolean::to_dafny_error(error), ++ }, ++ ), ++ Ok(client) => ::std::rc::Rc::new( ++ ::simple_boolean_dafny::_Wrappers_Compile::Result::Success { ++ value: crate::conversions::get_boolean::_get_boolean_output::to_dafny(client), ++ }, ++ ), ++ } ++ } ++} +diff --git b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/tests/tests_from_dafny/mod.rs a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/tests/tests_from_dafny/mod.rs +index ce6d90a2..7f1ba031 100644 +--- b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/tests/tests_from_dafny/mod.rs ++++ a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/tests/tests_from_dafny/mod.rs +@@ -1,5 +1,8 @@ + #![allow(warnings, unconditional_panic)] + #![allow(nonstandard_style)] ++use ::simple_boolean_dafny::*; ++use simple_boolean::*; ++mod _wrapped; + + pub mod r#_simple_dtypes_dboolean_dinternaldafny_dwrapped { + pub struct _default {} diff --git a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/Cargo.toml b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/Cargo.toml index 8cc533de4..5dbdc056e 100644 --- a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/Cargo.toml +++ b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/Cargo.toml @@ -5,6 +5,9 @@ edition = "2021" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html +[features] +wrapped-client = [] + [dependencies] aws-smithy-runtime = {version = "1.6.0", features = ["client"] } aws-smithy-runtime-api = {version = "1.7.0", features = ["client"] } @@ -13,6 +16,9 @@ dafny_runtime = { path = "../../../../dafny-dependencies/dafny_runtime_rust"} dafny_standard_library = { path = "../../../../dafny-dependencies/StandardLibrary/runtimes/rust"} simple_boolean_dafny = { path = "./dafny_impl"} -[dev-dependencies.tokio] +[dev-dependencies] +simple_boolean = { path = ".", features = ["wrapped-client"] } + +[dependencies.tokio] version = "1.26.0" -features = ["full"] +features = ["full"] \ No newline at end of file diff --git a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/dafny_impl/Cargo.toml b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/dafny_impl/Cargo.toml index a7f8568c4..31b603eef 100644 --- a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/dafny_impl/Cargo.toml +++ b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/dafny_impl/Cargo.toml @@ -10,4 +10,4 @@ dafny_runtime = { path = "../../../../../dafny-dependencies/dafny_runtime_rust"} dafny_standard_library = { path = "../../../../../dafny-dependencies/StandardLibrary/runtimes/rust"} [lib] -path = "src/implementation_from_dafny.rs" +path = "src/implementation_from_dafny.rs" \ No newline at end of file diff --git a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/conversions.rs b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/conversions.rs index c1acac7b2..86f878913 100644 --- a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/conversions.rs +++ b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/conversions.rs @@ -2,3 +2,5 @@ pub mod get_boolean; pub mod simple_boolean_config; + +pub(crate) mod error; \ No newline at end of file diff --git a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/conversions/error.rs b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/conversions/error.rs new file mode 100644 index 000000000..d6fd32b76 --- /dev/null +++ b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/conversions/error.rs @@ -0,0 +1,30 @@ +/// Wraps up an arbitrary Rust Error value as a Dafny Error +pub fn to_opaque_error(value: E) -> + ::std::rc::Rc<::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::Error> +{ + let error_obj: ::dafny_runtime::Object = + ::dafny_runtime::Object(Some(::std::rc::Rc::new( + ::std::cell::UnsafeCell::new(value), + ))); + ::std::rc::Rc::new( + ::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::Error::Opaque { + obj: error_obj, + }, + ) +} + +/// Wraps up an arbitrary Rust Error value as a Dafny Result.Failure +pub fn to_opaque_error_result(value: E) -> + ::std::rc::Rc< + dafny_standard_library::implementation_from_dafny::_Wrappers_Compile::Result< + T, + ::std::rc::Rc<::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::Error> + > + > +{ + ::std::rc::Rc::new( + dafny_standard_library::implementation_from_dafny::_Wrappers_Compile::Result::Failure { + error: to_opaque_error(value) + } + ) +} \ No newline at end of file diff --git a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/lib.rs b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/lib.rs index 1d16c1915..53977d7d6 100644 --- a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/lib.rs +++ b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/lib.rs @@ -13,5 +13,8 @@ pub mod operation; mod conversions; +#[cfg(feature = "wrapped-client")] +pub mod wrapped; + pub use client::Client; pub use types::simple_boolean_config::SimpleBooleanConfig; diff --git a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/wrapped.rs b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/wrapped.rs new file mode 100644 index 000000000..393551766 --- /dev/null +++ b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/wrapped.rs @@ -0,0 +1 @@ +pub mod client; \ No newline at end of file diff --git a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/wrapped/client.rs b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/wrapped/client.rs new file mode 100644 index 000000000..49c75f767 --- /dev/null +++ b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/wrapped/client.rs @@ -0,0 +1,88 @@ +use tokio::runtime::Runtime; + +pub struct Client { + wrapped: crate::client::Client, + + /// A `current_thread` runtime for executing operations on the + /// asynchronous client in a blocking manner. + rt: Runtime +} + +impl dafny_runtime::UpcastObject for Client { + ::dafny_runtime::UpcastObjectFn!(dyn ::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::ISimpleTypesBooleanClient); +} + +impl dafny_runtime::UpcastObject for Client { + ::dafny_runtime::UpcastObjectFn!(dyn ::std::any::Any); +} + +impl Client { + pub fn from_conf(config: &::std::rc::Rc< + ::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::SimpleBooleanConfig, + >) -> +::std::rc::Rc<::simple_boolean_dafny::r#_Wrappers_Compile::Result< + ::dafny_runtime::Object, + ::std::rc::Rc<::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::Error> +>> { + let rt_result = tokio::runtime::Builder::new_current_thread() + .enable_all() + .build(); + let rt = match rt_result { + Ok(x) => x, + Err(error) => return crate::conversions::error::to_opaque_error_result(error), + }; + let result = crate::client::Client::from_conf( + crate::conversions::simple_boolean_config::_simple_boolean_config::from_dafny( + config.clone(), + ), + ); + match result { + Ok(client) => { + let wrap = crate::wrapped::client::Client { + wrapped: client, + rt + }; + std::rc::Rc::new( + ::simple_boolean_dafny::_Wrappers_Compile::Result::Success { + value: ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(wrap)) + } + ) + }, + Err(error) => crate::conversions::error::to_opaque_error_result(error) + } + } +} + +impl ::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::ISimpleTypesBooleanClient + for Client +{ + fn GetBoolean( + &mut self, + input: &std::rc::Rc< + ::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::GetBooleanInput, + >, + ) -> std::rc::Rc< + ::simple_boolean_dafny::r#_Wrappers_Compile::Result< + std::rc::Rc< + ::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::GetBooleanOutput, + >, + std::rc::Rc<::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::Error>, + >, + >{ + let inner_input = + crate::conversions::get_boolean::_get_boolean_input::from_dafny(input.clone()); + let result = self.rt.block_on(crate::operation::get_boolean::GetBoolean::send(&self.wrapped, inner_input)); + match result { + Err(error) => ::std::rc::Rc::new( + ::simple_boolean_dafny::_Wrappers_Compile::Result::Failure { + error: crate::conversions::get_boolean::to_dafny_error(error), + }, + ), + Ok(client) => ::std::rc::Rc::new( + ::simple_boolean_dafny::_Wrappers_Compile::Result::Success { + value: crate::conversions::get_boolean::_get_boolean_output::to_dafny(client), + }, + ), + } + } +} diff --git a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/tests/simple_boolean_test.rs b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/tests/simple_boolean_test.rs index 8f5a0166c..9dc7b5d32 100644 --- a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/tests/simple_boolean_test.rs +++ b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/tests/simple_boolean_test.rs @@ -1,4 +1,8 @@ use simple_boolean::*; + + +mod tests_from_dafny; + /* method{:test} GetBooleanTrue(){ var client :- expect SimpleBoolean.SimpleBoolean(); @@ -50,3 +54,8 @@ pub fn client() -> Client { let config = SimpleBooleanConfig::builder().build().unwrap(); Client::from_conf(config).unwrap() } + +#[test] +fn dafny_tests() { + crate::tests_from_dafny::_module::_default::_Test__Main_() +} diff --git a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/tests/tests_from_dafny/_wrapped.rs b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/tests/tests_from_dafny/_wrapped.rs new file mode 100644 index 000000000..ba1e65204 --- /dev/null +++ b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/tests/tests_from_dafny/_wrapped.rs @@ -0,0 +1,12 @@ +use crate::tests_from_dafny::*; + +impl r#_simple_dtypes_dboolean_dinternaldafny_dwrapped::_default { + pub fn WrappedSimpleBoolean(config: &::std::rc::Rc< + ::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::SimpleBooleanConfig, + >) -> ::std::rc::Rc<::simple_boolean_dafny::r#_Wrappers_Compile::Result< + ::dafny_runtime::Object, + ::std::rc::Rc<::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::Error> + >>{ + crate::wrapped::client::Client::from_conf(config) + } +} diff --git a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/tests/tests_from_dafny/mod.rs b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/tests/tests_from_dafny/mod.rs new file mode 100644 index 000000000..7f1ba0317 --- /dev/null +++ b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/tests/tests_from_dafny/mod.rs @@ -0,0 +1,277 @@ +#![allow(warnings, unconditional_panic)] +#![allow(nonstandard_style)] +use ::simple_boolean_dafny::*; +use simple_boolean::*; +mod _wrapped; + +pub mod r#_simple_dtypes_dboolean_dinternaldafny_dwrapped { + pub struct _default {} + + impl _default { + pub fn _allocate_object() -> ::dafny_runtime::Object { + ::dafny_runtime::allocate_object::() + } + pub fn WrappedDefaultSimpleBooleanConfig() -> ::std::rc::Rc< + super::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::SimpleBooleanConfig, + > { + ::std::rc::Rc::new(super::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::SimpleBooleanConfig::SimpleBooleanConfig {}) + } + } + + impl ::dafny_runtime::UpcastObject + for super::r#_simple_dtypes_dboolean_dinternaldafny_dwrapped::_default + { + ::dafny_runtime::UpcastObjectFn!(dyn::std::any::Any); + } +} +pub mod r#_SimpleBooleanImplTest_Compile { + pub struct _default {} + + impl _default { + pub fn _allocate_object() -> ::dafny_runtime::Object { + ::dafny_runtime::allocate_object::() + } + pub fn GetBooleanTrue() -> () { + let mut valueOrError0 = ::dafny_runtime::MaybePlacebo::< + ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + ::dafny_runtime::Object< + super::r#_simple_dtypes_dboolean_dinternaldafny::SimpleBooleanClient, + >, + ::std::rc::Rc< + super::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::Error, + >, + >, + >, + >::new(); + let mut _out0 = ::dafny_runtime::MaybePlacebo::< + ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + ::dafny_runtime::Object< + super::r#_simple_dtypes_dboolean_dinternaldafny::SimpleBooleanClient, + >, + ::std::rc::Rc< + super::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::Error, + >, + >, + >, + >::new(); + _out0 = ::dafny_runtime::MaybePlacebo::from(super::r#_simple_dtypes_dboolean_dinternaldafny::_default::SimpleBoolean(&super::r#_simple_dtypes_dboolean_dinternaldafny::_default::DefaultSimpleBooleanConfig())); + valueOrError0 = ::dafny_runtime::MaybePlacebo::from(_out0.read()); + if !(!valueOrError0.read().IsFailure()) { + panic!("Halt") + }; + let mut client: ::dafny_runtime::Object< + super::r#_simple_dtypes_dboolean_dinternaldafny::SimpleBooleanClient, + > = valueOrError0.read().Extract(); + super::r#_SimpleBooleanImplTest_Compile::_default::TestGetBooleanTrue(&::dafny_runtime::upcast_object::()(client.clone())); + return (); + } + pub fn GetBooleanFalse() -> () { + let mut valueOrError0 = ::dafny_runtime::MaybePlacebo::< + ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + ::dafny_runtime::Object< + super::r#_simple_dtypes_dboolean_dinternaldafny::SimpleBooleanClient, + >, + ::std::rc::Rc< + super::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::Error, + >, + >, + >, + >::new(); + let mut _out1 = ::dafny_runtime::MaybePlacebo::< + ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + ::dafny_runtime::Object< + super::r#_simple_dtypes_dboolean_dinternaldafny::SimpleBooleanClient, + >, + ::std::rc::Rc< + super::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::Error, + >, + >, + >, + >::new(); + _out1 = ::dafny_runtime::MaybePlacebo::from(super::r#_simple_dtypes_dboolean_dinternaldafny::_default::SimpleBoolean(&super::r#_simple_dtypes_dboolean_dinternaldafny::_default::DefaultSimpleBooleanConfig())); + valueOrError0 = ::dafny_runtime::MaybePlacebo::from(_out1.read()); + if !(!valueOrError0.read().IsFailure()) { + panic!("Halt") + }; + let mut client: ::dafny_runtime::Object< + super::r#_simple_dtypes_dboolean_dinternaldafny::SimpleBooleanClient, + > = valueOrError0.read().Extract(); + super::r#_SimpleBooleanImplTest_Compile::_default::TestGetBooleanFalse(&::dafny_runtime::upcast_object::()(client.clone())); + return (); + } + pub fn TestGetBooleanTrue( + client: &::dafny_runtime::Object, + ) -> () { + let mut valueOrError0 = ::dafny_runtime::MaybePlacebo::<::std::rc::Rc, ::std::rc::Rc>>>::new(); + let mut _out2 = ::dafny_runtime::MaybePlacebo::<::std::rc::Rc, ::std::rc::Rc>>>::new(); + _out2 = ::dafny_runtime::MaybePlacebo::from(super::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::ISimpleTypesBooleanClient::GetBoolean(::dafny_runtime::md!(client.clone()), &::std::rc::Rc::new(super::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::GetBooleanInput::GetBooleanInput { + value: ::std::rc::Rc::new(super::r#_Wrappers_Compile::Option::::Some { + value: true + }) + }))); + valueOrError0 = ::dafny_runtime::MaybePlacebo::from(_out2.read()); + if !(!valueOrError0.read().IsFailure()) { + panic!("Halt") + }; + let mut ret: ::std::rc::Rc< + super::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::GetBooleanOutput, + > = valueOrError0.read().Extract(); + if !(ret.value().UnwrapOr(&false) == true) { + panic!("Halt") + }; + print!("{}", ::dafny_runtime::DafnyPrintWrapper(&ret)); + return (); + } + pub fn TestGetBooleanFalse( + client: &::dafny_runtime::Object, + ) -> () { + let mut valueOrError0 = ::dafny_runtime::MaybePlacebo::<::std::rc::Rc, ::std::rc::Rc>>>::new(); + let mut _out3 = ::dafny_runtime::MaybePlacebo::<::std::rc::Rc, ::std::rc::Rc>>>::new(); + _out3 = ::dafny_runtime::MaybePlacebo::from(super::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::ISimpleTypesBooleanClient::GetBoolean(::dafny_runtime::md!(client.clone()), &::std::rc::Rc::new(super::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::GetBooleanInput::GetBooleanInput { + value: ::std::rc::Rc::new(super::r#_Wrappers_Compile::Option::::Some { + value: false + }) + }))); + valueOrError0 = ::dafny_runtime::MaybePlacebo::from(_out3.read()); + if !(!valueOrError0.read().IsFailure()) { + panic!("Halt") + }; + let mut ret: ::std::rc::Rc< + super::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::GetBooleanOutput, + > = valueOrError0.read().Extract(); + if !(ret.value().UnwrapOr(&true) == false) { + panic!("Halt") + }; + print!("{}", ::dafny_runtime::DafnyPrintWrapper(&ret)); + return (); + } + } + + impl ::dafny_runtime::UpcastObject + for super::r#_SimpleBooleanImplTest_Compile::_default + { + ::dafny_runtime::UpcastObjectFn!(dyn::std::any::Any); + } +} +pub mod r#_WrappedSimpleTypesBooleanTest_Compile { + pub struct _default {} + + impl _default { + pub fn _allocate_object() -> ::dafny_runtime::Object { + ::dafny_runtime::allocate_object::() + } + pub fn GetBooleanTrue() -> () { + let mut valueOrError0 = ::dafny_runtime::MaybePlacebo::<::std::rc::Rc, ::std::rc::Rc>>>::new(); + let mut _out4 = ::dafny_runtime::MaybePlacebo::<::std::rc::Rc, ::std::rc::Rc>>>::new(); + _out4 = ::dafny_runtime::MaybePlacebo::from(super::r#_simple_dtypes_dboolean_dinternaldafny_dwrapped::_default::WrappedSimpleBoolean(&super::r#_simple_dtypes_dboolean_dinternaldafny_dwrapped::_default::WrappedDefaultSimpleBooleanConfig())); + valueOrError0 = ::dafny_runtime::MaybePlacebo::from(_out4.read()); + if !(!valueOrError0.read().IsFailure()) { + panic!("Halt") + }; + let mut client: ::dafny_runtime::Object = valueOrError0.read().Extract(); + super::r#_SimpleBooleanImplTest_Compile::_default::TestGetBooleanTrue(&client); + return (); + } + pub fn GetBooleanFalse() -> () { + let mut valueOrError0 = ::dafny_runtime::MaybePlacebo::<::std::rc::Rc, ::std::rc::Rc>>>::new(); + let mut _out5 = ::dafny_runtime::MaybePlacebo::<::std::rc::Rc, ::std::rc::Rc>>>::new(); + _out5 = ::dafny_runtime::MaybePlacebo::from(super::r#_simple_dtypes_dboolean_dinternaldafny_dwrapped::_default::WrappedSimpleBoolean(&super::r#_simple_dtypes_dboolean_dinternaldafny_dwrapped::_default::WrappedDefaultSimpleBooleanConfig())); + valueOrError0 = ::dafny_runtime::MaybePlacebo::from(_out5.read()); + if !(!valueOrError0.read().IsFailure()) { + panic!("Halt") + }; + let mut client: ::dafny_runtime::Object = valueOrError0.read().Extract(); + super::r#_SimpleBooleanImplTest_Compile::_default::TestGetBooleanFalse(&client); + return (); + } + } + + impl ::dafny_runtime::UpcastObject + for super::r#_WrappedSimpleTypesBooleanTest_Compile::_default + { + ::dafny_runtime::UpcastObjectFn!(dyn::std::any::Any); + } +} +pub mod _module { + pub struct _default {} + + impl _default { + pub fn _allocate_object() -> ::dafny_runtime::Object { + ::dafny_runtime::allocate_object::() + } + pub fn _Test__Main_() -> () { + let mut success: bool = true; + print!( + "{}", + ::dafny_runtime::DafnyPrintWrapper(&::dafny_runtime::string_utf16_of( + r#"SimpleBooleanImplTest.GetBooleanTrue: "# + )) + ); + super::r#_SimpleBooleanImplTest_Compile::_default::GetBooleanTrue(); + print!( + "{}", + ::dafny_runtime::DafnyPrintWrapper(&::dafny_runtime::string_utf16_of( + r#"PASSED +"# + )) + ); + print!( + "{}", + ::dafny_runtime::DafnyPrintWrapper(&::dafny_runtime::string_utf16_of( + r#"SimpleBooleanImplTest.GetBooleanFalse: "# + )) + ); + super::r#_SimpleBooleanImplTest_Compile::_default::GetBooleanFalse(); + print!( + "{}", + ::dafny_runtime::DafnyPrintWrapper(&::dafny_runtime::string_utf16_of( + r#"PASSED +"# + )) + ); + print!( + "{}", + ::dafny_runtime::DafnyPrintWrapper(&::dafny_runtime::string_utf16_of( + r#"WrappedSimpleTypesBooleanTest.GetBooleanTrue: "# + )) + ); + super::r#_WrappedSimpleTypesBooleanTest_Compile::_default::GetBooleanTrue(); + print!( + "{}", + ::dafny_runtime::DafnyPrintWrapper(&::dafny_runtime::string_utf16_of( + r#"PASSED +"# + )) + ); + print!( + "{}", + ::dafny_runtime::DafnyPrintWrapper(&::dafny_runtime::string_utf16_of( + r#"WrappedSimpleTypesBooleanTest.GetBooleanFalse: "# + )) + ); + super::r#_WrappedSimpleTypesBooleanTest_Compile::_default::GetBooleanFalse(); + print!( + "{}", + ::dafny_runtime::DafnyPrintWrapper(&::dafny_runtime::string_utf16_of( + r#"PASSED +"# + )) + ); + if !success { + panic!("Halt") + }; + return (); + } + } + + impl ::dafny_runtime::UpcastObject for super::_module::_default { + ::dafny_runtime::UpcastObjectFn!(dyn::std::any::Any); + } +} +fn main() { + _module::_default::_Test__Main_(); +} diff --git a/TestModels/SimpleTypes/SimpleTimestamp/runtimes/rust/dafny_impl/src/implementation_from_dafny.rs b/TestModels/SimpleTypes/SimpleTimestamp/runtimes/rust/dafny_impl/src/implementation_from_dafny.rs deleted file mode 100644 index 7564c63ad..000000000 --- a/TestModels/SimpleTypes/SimpleTimestamp/runtimes/rust/dafny_impl/src/implementation_from_dafny.rs +++ /dev/null @@ -1,631 +0,0 @@ -#![allow(warnings, unconditional_panic)] -#![allow(nonstandard_style)] -pub use dafny_standard_library::implementation_from_dafny::*; - -pub mod r#_simple_dtypes_dtimestamp_dinternaldafny_dtypes { - #[derive(PartialEq, Clone)] - pub enum DafnyCallEvent { - DafnyCallEvent { input: I, output: O }, - _PhantomVariant(::std::marker::PhantomData, ::std::marker::PhantomData), - } - - impl DafnyCallEvent { - pub fn input(&self) -> &I { - match self { - DafnyCallEvent::DafnyCallEvent { input, output } => input, - DafnyCallEvent::_PhantomVariant(..) => panic!(), - } - } - pub fn output(&self) -> &O { - match self { - DafnyCallEvent::DafnyCallEvent { input, output } => output, - DafnyCallEvent::_PhantomVariant(..) => panic!(), - } - } - } - - impl ::std::fmt::Debug - for DafnyCallEvent - { - fn fmt(&self, f: &mut ::std::fmt::Formatter) -> std::fmt::Result { - ::dafny_runtime::DafnyPrint::fmt_print(self, f, true) - } - } - - impl ::dafny_runtime::DafnyPrint - for DafnyCallEvent - { - fn fmt_print( - &self, - _formatter: &mut ::std::fmt::Formatter, - _in_seq: bool, - ) -> std::fmt::Result { - match self { - DafnyCallEvent::DafnyCallEvent { input, output } => { - write!(_formatter, "r#_simple_dtypes_dtimestamp_dinternaldafny_dtypes.DafnyCallEvent.DafnyCallEvent(")?; - ::dafny_runtime::DafnyPrint::fmt_print(input, _formatter, false)?; - write!(_formatter, ", ")?; - ::dafny_runtime::DafnyPrint::fmt_print(output, _formatter, false)?; - write!(_formatter, ")")?; - Ok(()) - } - DafnyCallEvent::_PhantomVariant(..) => { - panic!() - } - } - } - } - - impl Eq - for DafnyCallEvent - { - } - - impl< - I: ::dafny_runtime::DafnyType + ::std::hash::Hash, - O: ::dafny_runtime::DafnyType + ::std::hash::Hash, - > ::std::hash::Hash for DafnyCallEvent - { - fn hash<_H: ::std::hash::Hasher>(&self, _state: &mut _H) { - match self { - DafnyCallEvent::DafnyCallEvent { input, output } => { - input.hash(_state); - output.hash(_state) - } - DafnyCallEvent::_PhantomVariant(..) => { - panic!() - } - } - } - } - - impl< - I: ::dafny_runtime::DafnyType + ::std::default::Default, - O: ::dafny_runtime::DafnyType + ::std::default::Default, - > ::std::default::Default for DafnyCallEvent - { - fn default() -> DafnyCallEvent { - DafnyCallEvent::DafnyCallEvent { - input: ::std::default::Default::default(), - output: ::std::default::Default::default(), - } - } - } - - impl - ::std::convert::AsRef> for &DafnyCallEvent - { - fn as_ref(&self) -> Self { - self - } - } - - #[derive(PartialEq, Clone)] - pub enum GetTimestampInput { - GetTimestampInput { - value: ::std::rc::Rc< - super::r#_Wrappers_Compile::Option< - ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, - >, - >, - }, - } - - impl GetTimestampInput { - pub fn value( - &self, - ) -> &::std::rc::Rc< - super::r#_Wrappers_Compile::Option< - ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, - >, - > { - match self { - GetTimestampInput::GetTimestampInput { value } => value, - } - } - } - - impl ::std::fmt::Debug for GetTimestampInput { - fn fmt(&self, f: &mut ::std::fmt::Formatter) -> std::fmt::Result { - ::dafny_runtime::DafnyPrint::fmt_print(self, f, true) - } - } - - impl ::dafny_runtime::DafnyPrint for GetTimestampInput { - fn fmt_print( - &self, - _formatter: &mut ::std::fmt::Formatter, - _in_seq: bool, - ) -> std::fmt::Result { - match self { - GetTimestampInput::GetTimestampInput { value } => { - write!(_formatter, "r#_simple_dtypes_dtimestamp_dinternaldafny_dtypes.GetTimestampInput.GetTimestampInput(")?; - ::dafny_runtime::DafnyPrint::fmt_print(value, _formatter, false)?; - write!(_formatter, ")")?; - Ok(()) - } - } - } - } - - impl Eq for GetTimestampInput {} - - impl ::std::hash::Hash for GetTimestampInput { - fn hash<_H: ::std::hash::Hasher>(&self, _state: &mut _H) { - match self { - GetTimestampInput::GetTimestampInput { value } => value.hash(_state), - } - } - } - - impl ::std::default::Default for GetTimestampInput { - fn default() -> GetTimestampInput { - GetTimestampInput::GetTimestampInput { - value: ::std::default::Default::default(), - } - } - } - - impl ::std::convert::AsRef for &GetTimestampInput { - fn as_ref(&self) -> Self { - self - } - } - - #[derive(PartialEq, Clone)] - pub enum GetTimestampOutput { - GetTimestampOutput { - value: ::std::rc::Rc< - super::r#_Wrappers_Compile::Option< - ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, - >, - >, - }, - } - - impl GetTimestampOutput { - pub fn value( - &self, - ) -> &::std::rc::Rc< - super::r#_Wrappers_Compile::Option< - ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, - >, - > { - match self { - GetTimestampOutput::GetTimestampOutput { value } => value, - } - } - } - - impl ::std::fmt::Debug for GetTimestampOutput { - fn fmt(&self, f: &mut ::std::fmt::Formatter) -> std::fmt::Result { - ::dafny_runtime::DafnyPrint::fmt_print(self, f, true) - } - } - - impl ::dafny_runtime::DafnyPrint for GetTimestampOutput { - fn fmt_print( - &self, - _formatter: &mut ::std::fmt::Formatter, - _in_seq: bool, - ) -> std::fmt::Result { - match self { - GetTimestampOutput::GetTimestampOutput { value } => { - write!(_formatter, "r#_simple_dtypes_dtimestamp_dinternaldafny_dtypes.GetTimestampOutput.GetTimestampOutput(")?; - ::dafny_runtime::DafnyPrint::fmt_print(value, _formatter, false)?; - write!(_formatter, ")")?; - Ok(()) - } - } - } - } - - impl Eq for GetTimestampOutput {} - - impl ::std::hash::Hash for GetTimestampOutput { - fn hash<_H: ::std::hash::Hasher>(&self, _state: &mut _H) { - match self { - GetTimestampOutput::GetTimestampOutput { value } => value.hash(_state), - } - } - } - - impl ::std::default::Default for GetTimestampOutput { - fn default() -> GetTimestampOutput { - GetTimestampOutput::GetTimestampOutput { - value: ::std::default::Default::default(), - } - } - } - - impl ::std::convert::AsRef for &GetTimestampOutput { - fn as_ref(&self) -> Self { - self - } - } - - #[derive(PartialEq, Clone)] - pub enum SimpleTimestampConfig { - SimpleTimestampConfig {}, - } - - impl SimpleTimestampConfig {} - - impl ::std::fmt::Debug for SimpleTimestampConfig { - fn fmt(&self, f: &mut ::std::fmt::Formatter) -> std::fmt::Result { - ::dafny_runtime::DafnyPrint::fmt_print(self, f, true) - } - } - - impl ::dafny_runtime::DafnyPrint for SimpleTimestampConfig { - fn fmt_print( - &self, - _formatter: &mut ::std::fmt::Formatter, - _in_seq: bool, - ) -> std::fmt::Result { - match self { - SimpleTimestampConfig::SimpleTimestampConfig {} => { - write!(_formatter, "r#_simple_dtypes_dtimestamp_dinternaldafny_dtypes.SimpleTimestampConfig.SimpleTimestampConfig")?; - Ok(()) - } - } - } - } - - impl Eq for SimpleTimestampConfig {} - - impl ::std::hash::Hash for SimpleTimestampConfig { - fn hash<_H: ::std::hash::Hasher>(&self, _state: &mut _H) { - match self { - SimpleTimestampConfig::SimpleTimestampConfig {} => {} - } - } - } - - impl ::std::default::Default for SimpleTimestampConfig { - fn default() -> SimpleTimestampConfig { - SimpleTimestampConfig::SimpleTimestampConfig {} - } - } - - impl ::std::convert::AsRef for &SimpleTimestampConfig { - fn as_ref(&self) -> Self { - self - } - } - - pub struct ISimpleTypesTimestampClientCallHistory {} - - impl ISimpleTypesTimestampClientCallHistory { - pub fn _allocate_rcmut() -> ::dafny_runtime::Object { - ::dafny_runtime::allocate_rcmut::() - } - } - - pub trait ISimpleTypesTimestampClient { - fn GetTimestamp( - &mut self, - input: &::std::rc::Rc< - super::r#_simple_dtypes_dtimestamp_dinternaldafny_dtypes::GetTimestampInput, - >, - ) -> ::std::rc::Rc< - super::r#_Wrappers_Compile::Result< - ::std::rc::Rc< - super::r#_simple_dtypes_dtimestamp_dinternaldafny_dtypes::GetTimestampOutput, - >, - ::std::rc::Rc, - >, - >; - } - - #[derive(PartialEq, Clone)] - pub enum Error { - CollectionOfErrors { - list: ::dafny_runtime::Sequence< - ::std::rc::Rc, - >, - message: ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, - }, - Opaque { - obj: ::dafny_runtime::Object, - }, - } - - impl Error { - pub fn list( - &self, - ) -> &::dafny_runtime::Sequence< - ::std::rc::Rc, - > { - match self { - Error::CollectionOfErrors { list, message } => list, - Error::Opaque { obj } => panic!("field does not exist on this variant"), - } - } - pub fn message(&self) -> &::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16> { - match self { - Error::CollectionOfErrors { list, message } => message, - Error::Opaque { obj } => panic!("field does not exist on this variant"), - } - } - pub fn obj(&self) -> &::dafny_runtime::Object { - match self { - Error::CollectionOfErrors { list, message } => { - panic!("field does not exist on this variant") - } - Error::Opaque { obj } => obj, - } - } - } - - impl ::std::fmt::Debug for Error { - fn fmt(&self, f: &mut ::std::fmt::Formatter) -> std::fmt::Result { - ::dafny_runtime::DafnyPrint::fmt_print(self, f, true) - } - } - - impl ::dafny_runtime::DafnyPrint for Error { - fn fmt_print( - &self, - _formatter: &mut ::std::fmt::Formatter, - _in_seq: bool, - ) -> std::fmt::Result { - match self { - Error::CollectionOfErrors { list, message } => { - write!(_formatter, "r#_simple_dtypes_dtimestamp_dinternaldafny_dtypes.Error.CollectionOfErrors(")?; - ::dafny_runtime::DafnyPrint::fmt_print(list, _formatter, false)?; - write!(_formatter, ", ")?; - ::dafny_runtime::DafnyPrint::fmt_print(message, _formatter, false)?; - write!(_formatter, ")")?; - Ok(()) - } - Error::Opaque { obj } => { - write!( - _formatter, - "r#_simple_dtypes_dtimestamp_dinternaldafny_dtypes.Error.Opaque(" - )?; - ::dafny_runtime::DafnyPrint::fmt_print(obj, _formatter, false)?; - write!(_formatter, ")")?; - Ok(()) - } - } - } - } - - impl Eq for Error {} - - impl ::std::hash::Hash for Error { - fn hash<_H: ::std::hash::Hasher>(&self, _state: &mut _H) { - match self { - Error::CollectionOfErrors { list, message } => { - list.hash(_state); - message.hash(_state) - } - Error::Opaque { obj } => obj.hash(_state), - } - } - } - - impl ::std::default::Default for Error { - fn default() -> Error { - Error::CollectionOfErrors { - list: ::std::default::Default::default(), - message: ::std::default::Default::default(), - } - } - } - - impl ::std::convert::AsRef for &Error { - fn as_ref(&self) -> Self { - self - } - } - - pub type OpaqueError = - ::std::rc::Rc; -} -pub mod r#_SimpleTypesTimestampImpl_Compile { - pub struct _default {} - - impl _default { - pub fn _allocate_rcmut() -> ::dafny_runtime::Object { - ::dafny_runtime::allocate_rcmut::() - } - pub fn GetTimestamp( - config: &::std::rc::Rc, - input: &::std::rc::Rc< - super::r#_simple_dtypes_dtimestamp_dinternaldafny_dtypes::GetTimestampInput, - >, - ) -> ::std::rc::Rc< - super::r#_Wrappers_Compile::Result< - ::std::rc::Rc< - super::r#_simple_dtypes_dtimestamp_dinternaldafny_dtypes::GetTimestampOutput, - >, - ::std::rc::Rc, - >, - > { - let mut output = ::dafny_runtime::MaybePlacebo::<::std::rc::Rc, ::std::rc::Rc>>>::new(); - let mut res: ::std::rc::Rc = ::std::rc::Rc::new(super::r#_simple_dtypes_dtimestamp_dinternaldafny_dtypes::GetTimestampOutput::GetTimestampOutput { - value: input.value().clone() - }); - res = ::std::rc::Rc::new(super::r#_simple_dtypes_dtimestamp_dinternaldafny_dtypes::GetTimestampOutput::GetTimestampOutput { - value: input.value().clone() - }); - output = ::dafny_runtime::MaybePlacebo::from(::std::rc::Rc::new(super::r#_Wrappers_Compile::Result::<::std::rc::Rc, ::std::rc::Rc>::Success { - value: res.clone() - })); - return output.read(); - return output.read(); - } - } - - #[derive(PartialEq, Clone)] - pub enum Config { - Config {}, - } - - impl Config {} - - impl ::std::fmt::Debug for Config { - fn fmt(&self, f: &mut ::std::fmt::Formatter) -> std::fmt::Result { - ::dafny_runtime::DafnyPrint::fmt_print(self, f, true) - } - } - - impl ::dafny_runtime::DafnyPrint for Config { - fn fmt_print( - &self, - _formatter: &mut ::std::fmt::Formatter, - _in_seq: bool, - ) -> std::fmt::Result { - match self { - Config::Config {} => { - write!( - _formatter, - "r#_SimpleTypesTimestampImpl_Compile.Config.Config" - )?; - Ok(()) - } - } - } - } - - impl Eq for Config {} - - impl ::std::hash::Hash for Config { - fn hash<_H: ::std::hash::Hasher>(&self, _state: &mut _H) { - match self { - Config::Config {} => {} - } - } - } - - impl ::std::default::Default for Config { - fn default() -> Config { - Config::Config {} - } - } - - impl ::std::convert::AsRef for &Config { - fn as_ref(&self) -> Self { - self - } - } -} -pub mod r#_simple_dtypes_dtimestamp_dinternaldafny { - pub struct _default {} - - impl _default { - pub fn _allocate_rcmut() -> ::dafny_runtime::Object { - ::dafny_runtime::allocate_rcmut::() - } - pub fn DefaultSimpleTimestampConfig() -> ::std::rc::Rc< - super::r#_simple_dtypes_dtimestamp_dinternaldafny_dtypes::SimpleTimestampConfig, - > { - ::std::rc::Rc::new(super::r#_simple_dtypes_dtimestamp_dinternaldafny_dtypes::SimpleTimestampConfig::SimpleTimestampConfig {}) - } - pub fn SimpleTimestamp( - config: &::std::rc::Rc< - super::r#_simple_dtypes_dtimestamp_dinternaldafny_dtypes::SimpleTimestampConfig, - >, - ) -> ::std::rc::Rc< - super::r#_Wrappers_Compile::Result< - ::dafny_runtime::Object< - super::r#_simple_dtypes_dtimestamp_dinternaldafny::SimpleTimestampClient, - >, - ::std::rc::Rc, - >, - > { - let mut res = ::dafny_runtime::MaybePlacebo::<::std::rc::Rc, ::std::rc::Rc>>>::new(); - let mut client = ::dafny_runtime::MaybePlacebo::< - ::dafny_runtime::Object< - super::r#_simple_dtypes_dtimestamp_dinternaldafny::SimpleTimestampClient, - >, - >::new(); - let mut _nw0: ::dafny_runtime::Object = super::r#_simple_dtypes_dtimestamp_dinternaldafny::SimpleTimestampClient::_allocate_rcmut(); - super::r#_simple_dtypes_dtimestamp_dinternaldafny::SimpleTimestampClient::_ctor( - &_nw0, - &::std::rc::Rc::new(super::r#_SimpleTypesTimestampImpl_Compile::Config::Config {}), - ); - client = ::dafny_runtime::MaybePlacebo::from(_nw0.clone()); - res = ::dafny_runtime::MaybePlacebo::from(::std::rc::Rc::new( - super::r#_Wrappers_Compile::Result::< - ::dafny_runtime::Object< - super::r#_simple_dtypes_dtimestamp_dinternaldafny::SimpleTimestampClient, - >, - ::std::rc::Rc, - >::Success { - value: client.read(), - }, - )); - return res.read(); - return res.read(); - } - pub fn CreateSuccessOfClient(client: &::dafny_runtime::Object) -> ::std::rc::Rc, ::std::rc::Rc>>{ - ::std::rc::Rc::new(super::r#_Wrappers_Compile::Result::<::dafny_runtime::Object, ::std::rc::Rc>::Success { - value: client.clone() - }) - } - pub fn CreateFailureOfError(error: &::std::rc::Rc) -> ::std::rc::Rc, ::std::rc::Rc>>{ - ::std::rc::Rc::new(super::r#_Wrappers_Compile::Result::<::dafny_runtime::Object, ::std::rc::Rc>::Failure { - error: error.clone() - }) - } - } - - pub struct SimpleTimestampClient { - pub r#__i_config: ::std::rc::Rc, - } - - impl SimpleTimestampClient { - pub fn _allocate_rcmut() -> ::dafny_runtime::Object { - ::dafny_runtime::allocate_rcmut::() - } - pub fn _ctor( - this: &::dafny_runtime::Object, - config: &::std::rc::Rc, - ) -> () { - let mut _set__i_config: bool = false; - ::dafny_runtime::update_field_uninit_rcmut!( - this.clone(), - r#__i_config, - _set__i_config, - config.clone() - ); - return (); - } - pub fn config(&self) -> ::std::rc::Rc { - self.r#__i_config.clone() - } - } - - impl super::r#_simple_dtypes_dtimestamp_dinternaldafny_dtypes::ISimpleTypesTimestampClient - for super::r#_simple_dtypes_dtimestamp_dinternaldafny::SimpleTimestampClient - { - fn GetTimestamp( - &mut self, - input: &::std::rc::Rc< - super::r#_simple_dtypes_dtimestamp_dinternaldafny_dtypes::GetTimestampInput, - >, - ) -> ::std::rc::Rc< - super::r#_Wrappers_Compile::Result< - ::std::rc::Rc< - super::r#_simple_dtypes_dtimestamp_dinternaldafny_dtypes::GetTimestampOutput, - >, - ::std::rc::Rc, - >, - > { - let mut output = ::dafny_runtime::MaybePlacebo::<::std::rc::Rc, ::std::rc::Rc>>>::new(); - let mut _out0 = ::dafny_runtime::MaybePlacebo::<::std::rc::Rc, ::std::rc::Rc>>>::new(); - _out0 = ::dafny_runtime::MaybePlacebo::from( - super::r#_SimpleTypesTimestampImpl_Compile::_default::GetTimestamp( - &self.config(), - input, - ), - ); - output = ::dafny_runtime::MaybePlacebo::from(_out0.read()); - return output.read(); - } - } -} -pub mod _module {} diff --git a/TestModels/dafny-dependencies/StandardLibrary/Makefile b/TestModels/dafny-dependencies/StandardLibrary/Makefile index 3dcd26f9c..1e8efe7e9 100644 --- a/TestModels/dafny-dependencies/StandardLibrary/Makefile +++ b/TestModels/dafny-dependencies/StandardLibrary/Makefile @@ -65,9 +65,7 @@ transpile_java: | transpile_implementation_java transpile_test_java # Override SharedMakefile's transpile_java to not transpile # StandardLibrary as a dependency -transpile_rust: | transpile_implementation_rust - -RUST_TEST_INDEX=test_for_rust +transpile_rust: | transpile_implementation_rust transpile_test_rust # Override the targets to relocate translated Rust code directly into the main crate, # instead of the dafny_impl sub-crate. @@ -76,10 +74,6 @@ _mv_implementation_rust: mv implementation_from_dafny-rust/src/implementation_from_dafny.rs runtimes/rust/src/implementation_from_dafny.rs rustfmt runtimes/rust/src/implementation_from_dafny.rs rm -rf implementation_from_dafny-rust -_mv_test_rust: - mv tests_from_dafny-rust/src/tests_from_dafny.rs runtimes/rust/tests/tests_from_dafny.rs - rustfmt runtimes/rust/tests/tests_from_dafny.rs - rm -rf tests_from_dafny-rust transpile_dependencies: echo "Skipping transpile_dependencies for StandardLibrary" diff --git a/TestModels/dafny-dependencies/StandardLibrary/codegen-patches/rust/dafny-4.5.0.patch b/TestModels/dafny-dependencies/StandardLibrary/codegen-patches/rust/dafny-4.5.0.patch index d21190469..f2dc475ca 100644 --- a/TestModels/dafny-dependencies/StandardLibrary/codegen-patches/rust/dafny-4.5.0.patch +++ b/TestModels/dafny-dependencies/StandardLibrary/codegen-patches/rust/dafny-4.5.0.patch @@ -74,10 +74,10 @@ index 00000000..fb5e7bf9 \ No newline at end of file diff --git b/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/src/conversion.rs a/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/src/conversion.rs new file mode 100644 -index 00000000..3b7c2e76 +index 00000000..a6a27f6f --- /dev/null +++ a/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/src/conversion.rs -@@ -0,0 +1,104 @@ +@@ -0,0 +1,135 @@ +use crate::implementation_from_dafny::*; + +pub fn ostring_to_dafny( @@ -182,307 +182,57 @@ index 00000000..3b7c2e76 + None + } +} ++ ++pub fn result_from_dafny( ++ input: ::std::rc::Rc<_Wrappers_Compile::Result>, ++ converter_t: fn(&T) -> TR, ++ converter_e: fn(&E) -> ER, ++) -> Result { ++ match &*input { ++ _Wrappers_Compile::Result::Success { value } => Ok(converter_t(value)), ++ _Wrappers_Compile::Result::Failure { error } => Err(converter_e(error)), ++ _Wrappers_Compile::Result::_PhantomVariant(_, _) => panic!(), ++ } ++} ++ ++pub fn result_to_dafny( ++ input: Result, ++ converter_t: fn(&TR) -> T, ++ converter_e: fn(&ER) -> E, ++) -> ::std::rc::Rc<_Wrappers_Compile::Result> { ++ match input { ++ Ok(value) => ::std::rc::Rc::new( ++ _Wrappers_Compile::Result::Success { ++ value: converter_t(&value) ++ } ++ ), ++ Err(error) => ::std::rc::Rc::new( ++ _Wrappers_Compile::Result::Failure { ++ error: converter_e(&error) ++ } ++ ), ++ } ++} +\ No newline at end of file diff --git b/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/src/lib.rs a/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/src/lib.rs new file mode 100644 -index 00000000..4b9fb6f8 +index 00000000..12cdf221 --- /dev/null +++ a/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/src/lib.rs -@@ -0,0 +1,298 @@ +@@ -0,0 +1,4 @@ +#[allow(non_snake_case)] +pub mod UTF8; +pub mod conversion; +pub mod implementation_from_dafny; -+ -+#[cfg(test)] -+#[allow(non_snake_case)] -+mod TestUTF8 { -+ use super::*; -+ #[test] -+ fn TestEncodeHappyCase() { -+ let unicodeString = ::dafny_runtime::string_utf16_of("abc\u{0306}\u{01FD}\u{03B2}"); -+ let expectedBytes = -+ dafny_runtime::seq![0x61, 0x62, 0x63, 0xCC, 0x86, 0xC7, 0xBD, 0xCE, 0xB2]; -+ let _r = implementation_from_dafny::UTF8::_default::Encode(&unicodeString); -+ if _r.IsFailure() { -+ panic!("Encode failed"); -+ } -+ let encoded = _r.Extract(); -+ assert_eq!(expectedBytes, encoded); -+ } -+ -+ #[test] -+ fn TestEncodeInvalidUnicode() { -+ let invalidUnicode = ::dafny_runtime::seq![ -+ ::dafny_runtime::DafnyCharUTF16('a' as u16), -+ ::dafny_runtime::DafnyCharUTF16('b' as u16), -+ ::dafny_runtime::DafnyCharUTF16('c' as u16), -+ ::dafny_runtime::DafnyCharUTF16(0xD800) -+ ]; -+ let encoded = implementation_from_dafny::UTF8::_default::Encode(&invalidUnicode); -+ assert!(encoded.IsFailure()); -+ } -+ -+ #[test] -+ fn TestDecodeHappyCase() { -+ let unicodeBytes = -+ ::dafny_runtime::seq![0x61, 0x62, 0x63, 0xCC, 0x86, 0xC7, 0xBD, 0xCE, 0xB2]; -+ assert!( -+ implementation_from_dafny::UTF8::_default::Uses2Bytes( -+ &::dafny_runtime::seq![0xC7 as u8, 0xBD as u8, 0xCE as u8, 0xB2 as u8] -+ ) -+ ); -+ assert_eq!( -+ ::dafny_runtime::seq![0xC7 as u8, 0xBD as u8, 0xCE as u8, 0xB2 as u8], -+ unicodeBytes.slice(&::dafny_runtime::int!(5), &::dafny_runtime::int!(9)) -+ ); -+ assert!( -+ implementation_from_dafny::UTF8::_default::ValidUTF8Range( -+ &unicodeBytes, -+ &::dafny_runtime::int!(7), -+ &::dafny_runtime::int!(9) -+ ) -+ ); -+ assert!( -+ implementation_from_dafny::UTF8::_default::ValidUTF8Range( -+ &unicodeBytes, -+ &::dafny_runtime::int!(0), -+ &::dafny_runtime::int!(9) -+ ) -+ ); -+ let expectedString = ::dafny_runtime::string_utf16_of("abc\u{0306}\u{01FD}\u{03B2}"); -+ let _r = implementation_from_dafny::UTF8::_default::Decode(&unicodeBytes); -+ if _r.IsFailure() { -+ panic!("Decode failed"); -+ } -+ let decoded = _r.Extract(); -+ assert_eq!(expectedString, decoded); -+ } -+ -+ #[test] -+ fn TestDecodeInvalidUnicode() { -+ let invalidUnicode = ::dafny_runtime::seq![ -+ 0x61 as u8, 0x62 as u8, 0x63 as u8, 0xED as u8, 0xA0 as u8, 0x80 as u8 -+ ]; -+ let _r = implementation_from_dafny::UTF8::_default::Decode(&invalidUnicode); -+ assert!(_r.IsFailure()); -+ } -+ -+ #[test] -+ fn Test1Byte() { -+ // Null -+ let mut decoded = ::dafny_runtime::string_utf16_of("\u{0000}"); -+ let mut _r = implementation_from_dafny::UTF8::_default::Encode(&decoded); -+ assert!(!_r.IsFailure()); -+ let mut encoded = _r.Extract(); -+ assert_eq!(::dafny_runtime::seq![0x00 as u8], encoded); -+ assert!(implementation_from_dafny::UTF8::_default::Uses1Byte(&encoded)); -+ let mut _r2 = implementation_from_dafny::UTF8::_default::Decode(&encoded); -+ assert!(!_r2.IsFailure()); -+ let mut redecoded = _r2.Extract(); -+ assert_eq!(decoded, redecoded); -+ -+ // Space -+ decoded = ::dafny_runtime::string_utf16_of(" "); -+ _r = implementation_from_dafny::UTF8::_default::Encode(&decoded); -+ assert!(!_r.IsFailure()); -+ encoded = _r.Extract(); -+ assert_eq!(::dafny_runtime::seq![0x20 as u8], encoded); -+ assert!(implementation_from_dafny::UTF8::_default::Uses1Byte(&encoded)); -+ _r2 = implementation_from_dafny::UTF8::_default::Decode(&encoded); -+ assert!(!_r2.IsFailure()); -+ redecoded = _r2.Extract(); -+ assert_eq!(decoded, redecoded); -+ -+ decoded = ::dafny_runtime::string_utf16_of("$"); -+ _r = implementation_from_dafny::UTF8::_default::Encode(&decoded); -+ assert!(!_r.IsFailure()); -+ encoded = _r.Extract(); -+ assert_eq!(::dafny_runtime::seq![0x24 as u8], encoded); -+ assert!(implementation_from_dafny::UTF8::_default::Uses1Byte(&encoded)); -+ _r2 = implementation_from_dafny::UTF8::_default::Decode(&encoded); -+ assert!(!_r2.IsFailure()); -+ redecoded = _r2.Extract(); -+ assert_eq!(decoded, redecoded); -+ -+ decoded = ::dafny_runtime::string_utf16_of("0"); -+ _r = implementation_from_dafny::UTF8::_default::Encode(&decoded); -+ assert!(!_r.IsFailure()); -+ encoded = _r.Extract(); -+ assert_eq!(::dafny_runtime::seq![0x30 as u8], encoded); -+ assert!(implementation_from_dafny::UTF8::_default::Uses1Byte(&encoded)); -+ _r2 = implementation_from_dafny::UTF8::_default::Decode(&encoded); -+ assert!(!_r2.IsFailure()); -+ redecoded = _r2.Extract(); -+ assert_eq!(decoded, redecoded); -+ decoded = ::dafny_runtime::string_utf16_of("A"); -+ _r = implementation_from_dafny::UTF8::_default::Encode(&decoded); -+ assert!(!_r.IsFailure()); -+ encoded = _r.Extract(); -+ assert_eq!(::dafny_runtime::seq![0x41 as u8], encoded); -+ assert!(implementation_from_dafny::UTF8::_default::Uses1Byte(&encoded)); -+ _r2 = implementation_from_dafny::UTF8::_default::Decode(&encoded); -+ assert!(!_r2.IsFailure()); -+ redecoded = _r2.Extract(); -+ assert_eq!(decoded, redecoded); -+ decoded = ::dafny_runtime::string_utf16_of("a"); -+ _r = implementation_from_dafny::UTF8::_default::Encode(&decoded); -+ assert!(!_r.IsFailure()); -+ encoded = _r.Extract(); -+ assert_eq!(::dafny_runtime::seq![0x61 as u8], encoded); -+ assert!(implementation_from_dafny::UTF8::_default::Uses1Byte(&encoded)); -+ _r2 = implementation_from_dafny::UTF8::_default::Decode(&encoded); -+ assert!(!_r2.IsFailure()); -+ redecoded = _r2.Extract(); -+ assert_eq!(decoded, redecoded); -+ } -+ -+ #[test] -+ fn Test2Bytes() { -+ let mut decoded = ::dafny_runtime::string_utf16_of("\u{00A3}"); -+ let mut _r = implementation_from_dafny::UTF8::_default::Encode(&decoded); -+ assert!(!_r.IsFailure()); -+ let mut encoded = _r.Extract(); -+ assert_eq!(::dafny_runtime::seq![0xC2 as u8, 0xA3 as u8], encoded); -+ assert!(implementation_from_dafny::UTF8::_default::Uses2Bytes(&encoded)); -+ let mut _r2 = implementation_from_dafny::UTF8::_default::Decode(&encoded); -+ assert!(!_r2.IsFailure()); -+ let mut redecoded = _r2.Extract(); -+ assert_eq!(decoded, redecoded); -+ decoded = ::dafny_runtime::string_utf16_of("\u{00A9}"); -+ _r = implementation_from_dafny::UTF8::_default::Encode(&decoded); -+ assert!(!_r.IsFailure()); -+ encoded = _r.Extract(); -+ assert_eq!(::dafny_runtime::seq![0xC2 as u8, 0xA9 as u8], encoded); -+ assert!(implementation_from_dafny::UTF8::_default::Uses2Bytes(&encoded)); -+ _r2 = implementation_from_dafny::UTF8::_default::Decode(&encoded); -+ assert!(!_r2.IsFailure()); -+ redecoded = _r2.Extract(); -+ assert_eq!(decoded, redecoded); -+ decoded = ::dafny_runtime::string_utf16_of("\u{00AE}"); -+ _r = implementation_from_dafny::UTF8::_default::Encode(&decoded); -+ assert!(!_r.IsFailure()); -+ encoded = _r.Extract(); -+ assert_eq!(::dafny_runtime::seq![0xC2 as u8, 0xAE as u8], encoded); -+ assert!(implementation_from_dafny::UTF8::_default::Uses2Bytes(&encoded)); -+ _r2 = implementation_from_dafny::UTF8::_default::Decode(&encoded); -+ assert!(!_r2.IsFailure()); -+ redecoded = _r2.Extract(); -+ assert_eq!(decoded, redecoded); -+ decoded = ::dafny_runtime::string_utf16_of("\u{03C0}"); -+ _r = implementation_from_dafny::UTF8::_default::Encode(&decoded); -+ assert!(!_r.IsFailure()); -+ encoded = _r.Extract(); -+ assert_eq!(::dafny_runtime::seq![0xCF as u8, 0x80 as u8], encoded); -+ assert!(implementation_from_dafny::UTF8::_default::Uses2Bytes(&encoded)); -+ _r2 = implementation_from_dafny::UTF8::_default::Decode(&encoded); -+ assert!(!_r2.IsFailure()); -+ redecoded = _r2.Extract(); -+ assert_eq!(decoded, redecoded); -+ } -+ -+ #[test] -+ fn Test3Bytes() { -+ let mut decoded = ::dafny_runtime::string_utf16_of("\u{2386}"); -+ let mut _r = implementation_from_dafny::UTF8::_default::Encode(&decoded); -+ assert!(!_r.IsFailure()); -+ let mut encoded = _r.Extract(); -+ assert_eq!( -+ ::dafny_runtime::seq![0xE2 as u8, 0x8E as u8, 0x86 as u8], -+ encoded -+ ); -+ assert!(implementation_from_dafny::UTF8::_default::Uses3Bytes(&encoded)); -+ let mut _r2 = implementation_from_dafny::UTF8::_default::Decode(&encoded); -+ assert!(!_r2.IsFailure()); -+ let mut redecoded = _r2.Extract(); -+ assert_eq!(decoded, redecoded); -+ decoded = ::dafny_runtime::string_utf16_of("\u{2387}"); -+ _r = implementation_from_dafny::UTF8::_default::Encode(&decoded); -+ assert!(!_r.IsFailure()); -+ encoded = _r.Extract(); -+ assert_eq!( -+ ::dafny_runtime::seq![0xE2 as u8, 0x8E as u8, 0x87 as u8], -+ encoded -+ ); -+ assert!(implementation_from_dafny::UTF8::_default::Uses3Bytes(&encoded)); -+ _r2 = implementation_from_dafny::UTF8::_default::Decode(&encoded); -+ assert!(!_r2.IsFailure()); -+ redecoded = _r2.Extract(); -+ assert_eq!(decoded, redecoded); -+ decoded = ::dafny_runtime::string_utf16_of("\u{231B}"); -+ _r = implementation_from_dafny::UTF8::_default::Encode(&decoded); -+ assert!(!_r.IsFailure()); -+ encoded = _r.Extract(); -+ assert_eq!( -+ ::dafny_runtime::seq![0xE2 as u8, 0x8C as u8, 0x9B as u8], -+ encoded -+ ); -+ assert!(implementation_from_dafny::UTF8::_default::Uses3Bytes(&encoded)); -+ _r2 = implementation_from_dafny::UTF8::_default::Decode(&encoded); -+ assert!(!_r2.IsFailure()); -+ redecoded = _r2.Extract(); -+ assert_eq!(decoded, redecoded); -+ decoded = ::dafny_runtime::string_utf16_of("\u{1D78}"); -+ _r = implementation_from_dafny::UTF8::_default::Encode(&decoded); -+ assert!(!_r.IsFailure()); -+ encoded = _r.Extract(); -+ assert_eq!( -+ ::dafny_runtime::seq![0xE1 as u8, 0xB5 as u8, 0xB8 as u8], -+ encoded -+ ); -+ assert!(implementation_from_dafny::UTF8::_default::Uses3Bytes(&encoded)); -+ _r2 = implementation_from_dafny::UTF8::_default::Decode(&encoded); -+ assert!(!_r2.IsFailure()); -+ redecoded = _r2.Extract(); -+ assert_eq!(decoded, redecoded); -+ decoded = ::dafny_runtime::string_utf16_of("\u{732B}"); -+ _r = implementation_from_dafny::UTF8::_default::Encode(&decoded); -+ assert!(!_r.IsFailure()); -+ encoded = _r.Extract(); -+ assert_eq!( -+ ::dafny_runtime::seq![0xE7 as u8, 0x8C as u8, 0xAB as u8], -+ encoded -+ ); -+ assert!(implementation_from_dafny::UTF8::_default::Uses3Bytes(&encoded)); -+ _r2 = implementation_from_dafny::UTF8::_default::Decode(&encoded); -+ assert!(!_r2.IsFailure()); -+ redecoded = _r2.Extract(); -+ assert_eq!(decoded, redecoded); -+ } -+ -+ #[test] -+ fn Test4Bytes() { -+ let mut decoded = ::dafny_runtime::seq![ -+ ::dafny_runtime::DafnyCharUTF16(0xD808), -+ ::dafny_runtime::DafnyCharUTF16(0xDC00) -+ ]; -+ let mut _r = implementation_from_dafny::UTF8::_default::Encode(&decoded); -+ println!( -+ "{}", -+ ::dafny_runtime::DafnyPrintWrapper(&_r.as_ref().clone()) -+ ); -+ assert!(!_r.IsFailure()); -+ let mut encoded = _r.Extract(); -+ assert_eq!( -+ ::dafny_runtime::seq![0xF0 as u8, 0x92 as u8, 0x80 as u8, 0x80 as u8], -+ encoded -+ ); -+ assert!(implementation_from_dafny::UTF8::_default::Uses4Bytes(&encoded)); -+ let mut _r2 = implementation_from_dafny::UTF8::_default::Decode(&encoded); -+ assert!(!_r2.IsFailure()); -+ let mut redecoded = _r2.Extract(); -+ assert_eq!(decoded, redecoded); -+ decoded = ::dafny_runtime::string_utf16_of("\u{1D7C1}"); -+ _r = implementation_from_dafny::UTF8::_default::Encode(&decoded); -+ assert!(!_r.IsFailure()); -+ encoded = _r.Extract(); -+ assert_eq!( -+ ::dafny_runtime::seq![0xF0 as u8, 0x9D as u8, 0x9F as u8, 0x81 as u8], -+ encoded -+ ); -+ assert!(implementation_from_dafny::UTF8::_default::Uses4Bytes(&encoded)); -+ _r2 = implementation_from_dafny::UTF8::_default::Decode(&encoded); -+ assert!(!_r2.IsFailure()); -+ redecoded = _r2.Extract(); -+ assert_eq!(decoded, redecoded); -+ } -+} +\ No newline at end of file +diff --git b/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/tests/tests_from_dafny/mod.rs a/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/tests/tests_from_dafny/mod.rs +index 20caf2dd..c4a1c20f 100644 +--- b/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/tests/tests_from_dafny/mod.rs ++++ a/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/tests/tests_from_dafny/mod.rs +@@ -1,5 +1,6 @@ + #![allow(warnings, unconditional_panic)] + #![allow(nonstandard_style)] ++use ::dafny_standard_library::implementation_from_dafny::*; + + pub mod r#_TestUTF8_Compile { + pub struct _default {} diff --git a/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/src/conversion.rs b/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/src/conversion.rs index 3b7c2e767..a6a27f6f6 100644 --- a/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/src/conversion.rs +++ b/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/src/conversion.rs @@ -102,3 +102,34 @@ pub fn oblob_from_dafny( None } } + +pub fn result_from_dafny( + input: ::std::rc::Rc<_Wrappers_Compile::Result>, + converter_t: fn(&T) -> TR, + converter_e: fn(&E) -> ER, +) -> Result { + match &*input { + _Wrappers_Compile::Result::Success { value } => Ok(converter_t(value)), + _Wrappers_Compile::Result::Failure { error } => Err(converter_e(error)), + _Wrappers_Compile::Result::_PhantomVariant(_, _) => panic!(), + } +} + +pub fn result_to_dafny( + input: Result, + converter_t: fn(&TR) -> T, + converter_e: fn(&ER) -> E, +) -> ::std::rc::Rc<_Wrappers_Compile::Result> { + match input { + Ok(value) => ::std::rc::Rc::new( + _Wrappers_Compile::Result::Success { + value: converter_t(&value) + } + ), + Err(error) => ::std::rc::Rc::new( + _Wrappers_Compile::Result::Failure { + error: converter_e(&error) + } + ), + } +} \ No newline at end of file diff --git a/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/src/lib.rs b/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/src/lib.rs index 4b9fb6f84..12cdf2219 100644 --- a/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/src/lib.rs +++ b/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/src/lib.rs @@ -1,298 +1,4 @@ #[allow(non_snake_case)] pub mod UTF8; pub mod conversion; -pub mod implementation_from_dafny; - -#[cfg(test)] -#[allow(non_snake_case)] -mod TestUTF8 { - use super::*; - #[test] - fn TestEncodeHappyCase() { - let unicodeString = ::dafny_runtime::string_utf16_of("abc\u{0306}\u{01FD}\u{03B2}"); - let expectedBytes = - dafny_runtime::seq![0x61, 0x62, 0x63, 0xCC, 0x86, 0xC7, 0xBD, 0xCE, 0xB2]; - let _r = implementation_from_dafny::UTF8::_default::Encode(&unicodeString); - if _r.IsFailure() { - panic!("Encode failed"); - } - let encoded = _r.Extract(); - assert_eq!(expectedBytes, encoded); - } - - #[test] - fn TestEncodeInvalidUnicode() { - let invalidUnicode = ::dafny_runtime::seq![ - ::dafny_runtime::DafnyCharUTF16('a' as u16), - ::dafny_runtime::DafnyCharUTF16('b' as u16), - ::dafny_runtime::DafnyCharUTF16('c' as u16), - ::dafny_runtime::DafnyCharUTF16(0xD800) - ]; - let encoded = implementation_from_dafny::UTF8::_default::Encode(&invalidUnicode); - assert!(encoded.IsFailure()); - } - - #[test] - fn TestDecodeHappyCase() { - let unicodeBytes = - ::dafny_runtime::seq![0x61, 0x62, 0x63, 0xCC, 0x86, 0xC7, 0xBD, 0xCE, 0xB2]; - assert!( - implementation_from_dafny::UTF8::_default::Uses2Bytes( - &::dafny_runtime::seq![0xC7 as u8, 0xBD as u8, 0xCE as u8, 0xB2 as u8] - ) - ); - assert_eq!( - ::dafny_runtime::seq![0xC7 as u8, 0xBD as u8, 0xCE as u8, 0xB2 as u8], - unicodeBytes.slice(&::dafny_runtime::int!(5), &::dafny_runtime::int!(9)) - ); - assert!( - implementation_from_dafny::UTF8::_default::ValidUTF8Range( - &unicodeBytes, - &::dafny_runtime::int!(7), - &::dafny_runtime::int!(9) - ) - ); - assert!( - implementation_from_dafny::UTF8::_default::ValidUTF8Range( - &unicodeBytes, - &::dafny_runtime::int!(0), - &::dafny_runtime::int!(9) - ) - ); - let expectedString = ::dafny_runtime::string_utf16_of("abc\u{0306}\u{01FD}\u{03B2}"); - let _r = implementation_from_dafny::UTF8::_default::Decode(&unicodeBytes); - if _r.IsFailure() { - panic!("Decode failed"); - } - let decoded = _r.Extract(); - assert_eq!(expectedString, decoded); - } - - #[test] - fn TestDecodeInvalidUnicode() { - let invalidUnicode = ::dafny_runtime::seq![ - 0x61 as u8, 0x62 as u8, 0x63 as u8, 0xED as u8, 0xA0 as u8, 0x80 as u8 - ]; - let _r = implementation_from_dafny::UTF8::_default::Decode(&invalidUnicode); - assert!(_r.IsFailure()); - } - - #[test] - fn Test1Byte() { - // Null - let mut decoded = ::dafny_runtime::string_utf16_of("\u{0000}"); - let mut _r = implementation_from_dafny::UTF8::_default::Encode(&decoded); - assert!(!_r.IsFailure()); - let mut encoded = _r.Extract(); - assert_eq!(::dafny_runtime::seq![0x00 as u8], encoded); - assert!(implementation_from_dafny::UTF8::_default::Uses1Byte(&encoded)); - let mut _r2 = implementation_from_dafny::UTF8::_default::Decode(&encoded); - assert!(!_r2.IsFailure()); - let mut redecoded = _r2.Extract(); - assert_eq!(decoded, redecoded); - - // Space - decoded = ::dafny_runtime::string_utf16_of(" "); - _r = implementation_from_dafny::UTF8::_default::Encode(&decoded); - assert!(!_r.IsFailure()); - encoded = _r.Extract(); - assert_eq!(::dafny_runtime::seq![0x20 as u8], encoded); - assert!(implementation_from_dafny::UTF8::_default::Uses1Byte(&encoded)); - _r2 = implementation_from_dafny::UTF8::_default::Decode(&encoded); - assert!(!_r2.IsFailure()); - redecoded = _r2.Extract(); - assert_eq!(decoded, redecoded); - - decoded = ::dafny_runtime::string_utf16_of("$"); - _r = implementation_from_dafny::UTF8::_default::Encode(&decoded); - assert!(!_r.IsFailure()); - encoded = _r.Extract(); - assert_eq!(::dafny_runtime::seq![0x24 as u8], encoded); - assert!(implementation_from_dafny::UTF8::_default::Uses1Byte(&encoded)); - _r2 = implementation_from_dafny::UTF8::_default::Decode(&encoded); - assert!(!_r2.IsFailure()); - redecoded = _r2.Extract(); - assert_eq!(decoded, redecoded); - - decoded = ::dafny_runtime::string_utf16_of("0"); - _r = implementation_from_dafny::UTF8::_default::Encode(&decoded); - assert!(!_r.IsFailure()); - encoded = _r.Extract(); - assert_eq!(::dafny_runtime::seq![0x30 as u8], encoded); - assert!(implementation_from_dafny::UTF8::_default::Uses1Byte(&encoded)); - _r2 = implementation_from_dafny::UTF8::_default::Decode(&encoded); - assert!(!_r2.IsFailure()); - redecoded = _r2.Extract(); - assert_eq!(decoded, redecoded); - decoded = ::dafny_runtime::string_utf16_of("A"); - _r = implementation_from_dafny::UTF8::_default::Encode(&decoded); - assert!(!_r.IsFailure()); - encoded = _r.Extract(); - assert_eq!(::dafny_runtime::seq![0x41 as u8], encoded); - assert!(implementation_from_dafny::UTF8::_default::Uses1Byte(&encoded)); - _r2 = implementation_from_dafny::UTF8::_default::Decode(&encoded); - assert!(!_r2.IsFailure()); - redecoded = _r2.Extract(); - assert_eq!(decoded, redecoded); - decoded = ::dafny_runtime::string_utf16_of("a"); - _r = implementation_from_dafny::UTF8::_default::Encode(&decoded); - assert!(!_r.IsFailure()); - encoded = _r.Extract(); - assert_eq!(::dafny_runtime::seq![0x61 as u8], encoded); - assert!(implementation_from_dafny::UTF8::_default::Uses1Byte(&encoded)); - _r2 = implementation_from_dafny::UTF8::_default::Decode(&encoded); - assert!(!_r2.IsFailure()); - redecoded = _r2.Extract(); - assert_eq!(decoded, redecoded); - } - - #[test] - fn Test2Bytes() { - let mut decoded = ::dafny_runtime::string_utf16_of("\u{00A3}"); - let mut _r = implementation_from_dafny::UTF8::_default::Encode(&decoded); - assert!(!_r.IsFailure()); - let mut encoded = _r.Extract(); - assert_eq!(::dafny_runtime::seq![0xC2 as u8, 0xA3 as u8], encoded); - assert!(implementation_from_dafny::UTF8::_default::Uses2Bytes(&encoded)); - let mut _r2 = implementation_from_dafny::UTF8::_default::Decode(&encoded); - assert!(!_r2.IsFailure()); - let mut redecoded = _r2.Extract(); - assert_eq!(decoded, redecoded); - decoded = ::dafny_runtime::string_utf16_of("\u{00A9}"); - _r = implementation_from_dafny::UTF8::_default::Encode(&decoded); - assert!(!_r.IsFailure()); - encoded = _r.Extract(); - assert_eq!(::dafny_runtime::seq![0xC2 as u8, 0xA9 as u8], encoded); - assert!(implementation_from_dafny::UTF8::_default::Uses2Bytes(&encoded)); - _r2 = implementation_from_dafny::UTF8::_default::Decode(&encoded); - assert!(!_r2.IsFailure()); - redecoded = _r2.Extract(); - assert_eq!(decoded, redecoded); - decoded = ::dafny_runtime::string_utf16_of("\u{00AE}"); - _r = implementation_from_dafny::UTF8::_default::Encode(&decoded); - assert!(!_r.IsFailure()); - encoded = _r.Extract(); - assert_eq!(::dafny_runtime::seq![0xC2 as u8, 0xAE as u8], encoded); - assert!(implementation_from_dafny::UTF8::_default::Uses2Bytes(&encoded)); - _r2 = implementation_from_dafny::UTF8::_default::Decode(&encoded); - assert!(!_r2.IsFailure()); - redecoded = _r2.Extract(); - assert_eq!(decoded, redecoded); - decoded = ::dafny_runtime::string_utf16_of("\u{03C0}"); - _r = implementation_from_dafny::UTF8::_default::Encode(&decoded); - assert!(!_r.IsFailure()); - encoded = _r.Extract(); - assert_eq!(::dafny_runtime::seq![0xCF as u8, 0x80 as u8], encoded); - assert!(implementation_from_dafny::UTF8::_default::Uses2Bytes(&encoded)); - _r2 = implementation_from_dafny::UTF8::_default::Decode(&encoded); - assert!(!_r2.IsFailure()); - redecoded = _r2.Extract(); - assert_eq!(decoded, redecoded); - } - - #[test] - fn Test3Bytes() { - let mut decoded = ::dafny_runtime::string_utf16_of("\u{2386}"); - let mut _r = implementation_from_dafny::UTF8::_default::Encode(&decoded); - assert!(!_r.IsFailure()); - let mut encoded = _r.Extract(); - assert_eq!( - ::dafny_runtime::seq![0xE2 as u8, 0x8E as u8, 0x86 as u8], - encoded - ); - assert!(implementation_from_dafny::UTF8::_default::Uses3Bytes(&encoded)); - let mut _r2 = implementation_from_dafny::UTF8::_default::Decode(&encoded); - assert!(!_r2.IsFailure()); - let mut redecoded = _r2.Extract(); - assert_eq!(decoded, redecoded); - decoded = ::dafny_runtime::string_utf16_of("\u{2387}"); - _r = implementation_from_dafny::UTF8::_default::Encode(&decoded); - assert!(!_r.IsFailure()); - encoded = _r.Extract(); - assert_eq!( - ::dafny_runtime::seq![0xE2 as u8, 0x8E as u8, 0x87 as u8], - encoded - ); - assert!(implementation_from_dafny::UTF8::_default::Uses3Bytes(&encoded)); - _r2 = implementation_from_dafny::UTF8::_default::Decode(&encoded); - assert!(!_r2.IsFailure()); - redecoded = _r2.Extract(); - assert_eq!(decoded, redecoded); - decoded = ::dafny_runtime::string_utf16_of("\u{231B}"); - _r = implementation_from_dafny::UTF8::_default::Encode(&decoded); - assert!(!_r.IsFailure()); - encoded = _r.Extract(); - assert_eq!( - ::dafny_runtime::seq![0xE2 as u8, 0x8C as u8, 0x9B as u8], - encoded - ); - assert!(implementation_from_dafny::UTF8::_default::Uses3Bytes(&encoded)); - _r2 = implementation_from_dafny::UTF8::_default::Decode(&encoded); - assert!(!_r2.IsFailure()); - redecoded = _r2.Extract(); - assert_eq!(decoded, redecoded); - decoded = ::dafny_runtime::string_utf16_of("\u{1D78}"); - _r = implementation_from_dafny::UTF8::_default::Encode(&decoded); - assert!(!_r.IsFailure()); - encoded = _r.Extract(); - assert_eq!( - ::dafny_runtime::seq![0xE1 as u8, 0xB5 as u8, 0xB8 as u8], - encoded - ); - assert!(implementation_from_dafny::UTF8::_default::Uses3Bytes(&encoded)); - _r2 = implementation_from_dafny::UTF8::_default::Decode(&encoded); - assert!(!_r2.IsFailure()); - redecoded = _r2.Extract(); - assert_eq!(decoded, redecoded); - decoded = ::dafny_runtime::string_utf16_of("\u{732B}"); - _r = implementation_from_dafny::UTF8::_default::Encode(&decoded); - assert!(!_r.IsFailure()); - encoded = _r.Extract(); - assert_eq!( - ::dafny_runtime::seq![0xE7 as u8, 0x8C as u8, 0xAB as u8], - encoded - ); - assert!(implementation_from_dafny::UTF8::_default::Uses3Bytes(&encoded)); - _r2 = implementation_from_dafny::UTF8::_default::Decode(&encoded); - assert!(!_r2.IsFailure()); - redecoded = _r2.Extract(); - assert_eq!(decoded, redecoded); - } - - #[test] - fn Test4Bytes() { - let mut decoded = ::dafny_runtime::seq![ - ::dafny_runtime::DafnyCharUTF16(0xD808), - ::dafny_runtime::DafnyCharUTF16(0xDC00) - ]; - let mut _r = implementation_from_dafny::UTF8::_default::Encode(&decoded); - println!( - "{}", - ::dafny_runtime::DafnyPrintWrapper(&_r.as_ref().clone()) - ); - assert!(!_r.IsFailure()); - let mut encoded = _r.Extract(); - assert_eq!( - ::dafny_runtime::seq![0xF0 as u8, 0x92 as u8, 0x80 as u8, 0x80 as u8], - encoded - ); - assert!(implementation_from_dafny::UTF8::_default::Uses4Bytes(&encoded)); - let mut _r2 = implementation_from_dafny::UTF8::_default::Decode(&encoded); - assert!(!_r2.IsFailure()); - let mut redecoded = _r2.Extract(); - assert_eq!(decoded, redecoded); - decoded = ::dafny_runtime::string_utf16_of("\u{1D7C1}"); - _r = implementation_from_dafny::UTF8::_default::Encode(&decoded); - assert!(!_r.IsFailure()); - encoded = _r.Extract(); - assert_eq!( - ::dafny_runtime::seq![0xF0 as u8, 0x9D as u8, 0x9F as u8, 0x81 as u8], - encoded - ); - assert!(implementation_from_dafny::UTF8::_default::Uses4Bytes(&encoded)); - _r2 = implementation_from_dafny::UTF8::_default::Decode(&encoded); - assert!(!_r2.IsFailure()); - redecoded = _r2.Extract(); - assert_eq!(decoded, redecoded); - } -} +pub mod implementation_from_dafny; \ No newline at end of file diff --git a/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/tests/standard_library_tests.rs b/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/tests/standard_library_tests.rs new file mode 100644 index 000000000..fe1c0f50e --- /dev/null +++ b/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/tests/standard_library_tests.rs @@ -0,0 +1,7 @@ + +mod tests_from_dafny; + +#[test] +fn dafny_tests() { + crate::tests_from_dafny::_module::_default::_Test__Main_() +} diff --git a/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/tests/tests_from_dafny/mod.rs b/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/tests/tests_from_dafny/mod.rs new file mode 100644 index 000000000..c4a1c20ff --- /dev/null +++ b/TestModels/dafny-dependencies/StandardLibrary/runtimes/rust/tests/tests_from_dafny/mod.rs @@ -0,0 +1,919 @@ +#![allow(warnings, unconditional_panic)] +#![allow(nonstandard_style)] +use ::dafny_standard_library::implementation_from_dafny::*; + +pub mod r#_TestUTF8_Compile { + pub struct _default {} + + impl _default { + pub fn _allocate_object() -> ::dafny_runtime::Object { + ::dafny_runtime::allocate_object::() + } + pub fn TestEncodeHappyCase() -> () { + let mut unicodeString: ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16> = ::dafny_runtime::seq![ + ::dafny_runtime::DafnyCharUTF16(97 as u16), + ::dafny_runtime::DafnyCharUTF16(98 as u16), + ::dafny_runtime::DafnyCharUTF16(99 as u16), + ::dafny_runtime::DafnyCharUTF16(774 as u16), + ::dafny_runtime::DafnyCharUTF16(509 as u16), + ::dafny_runtime::DafnyCharUTF16(946 as u16) + ]; + let mut expectedBytes: ::dafny_runtime::Sequence = + ::dafny_runtime::seq![97, 98, 99, 204, 134, 199, 189, 206, 178]; + let mut valueOrError0 = ::dafny_runtime::MaybePlacebo::< + ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + super::UTF8::ValidUTF8Bytes, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + >, + >, + >::new(); + valueOrError0 = + ::dafny_runtime::MaybePlacebo::from(super::UTF8::_default::Encode(&unicodeString)); + if !(!valueOrError0.read().IsFailure()) { + panic!("Halt") + }; + let mut encoded: super::UTF8::ValidUTF8Bytes = valueOrError0.read().Extract(); + if !(expectedBytes.clone() == encoded.clone()) { + panic!("Halt") + }; + return (); + } + pub fn TestEncodeInvalidUnicode() -> () { + let mut invalidUnicode: ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16> = ::dafny_runtime::seq![ + ::dafny_runtime::DafnyCharUTF16(97 as u16), + ::dafny_runtime::DafnyCharUTF16(98 as u16), + ::dafny_runtime::DafnyCharUTF16(99 as u16), + ::dafny_runtime::DafnyCharUTF16(55296 as u16) + ]; + let mut encoded: ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + super::UTF8::ValidUTF8Bytes, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + >, + > = super::UTF8::_default::Encode(&invalidUnicode); + if !matches!( + (&encoded).as_ref(), + super::r#_Wrappers_Compile::Result::Failure { .. } + ) { + panic!("Halt") + }; + return (); + } + pub fn TestDecodeHappyCase() -> () { + let mut unicodeBytes: ::dafny_runtime::Sequence = + ::dafny_runtime::seq![97, 98, 99, 204, 134, 199, 189, 206, 178]; + let mut expectedString: ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16> = ::dafny_runtime::seq![ + ::dafny_runtime::DafnyCharUTF16(97 as u16), + ::dafny_runtime::DafnyCharUTF16(98 as u16), + ::dafny_runtime::DafnyCharUTF16(99 as u16), + ::dafny_runtime::DafnyCharUTF16(774 as u16), + ::dafny_runtime::DafnyCharUTF16(509 as u16), + ::dafny_runtime::DafnyCharUTF16(946 as u16) + ]; + let mut valueOrError0 = ::dafny_runtime::MaybePlacebo::< + ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + >, + >, + >::new(); + valueOrError0 = + ::dafny_runtime::MaybePlacebo::from(super::UTF8::_default::Decode(&unicodeBytes)); + if !(!valueOrError0.read().IsFailure()) { + panic!("Halt") + }; + let mut decoded: ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16> = + valueOrError0.read().Extract(); + if !(expectedString.clone() == decoded.clone()) { + panic!("Halt") + }; + return (); + } + pub fn TestDecodeInvalidUnicode() -> () { + let mut invalidUnicode: ::dafny_runtime::Sequence = + ::dafny_runtime::seq![97, 98, 99, 237, 160, 128]; + if !(!super::UTF8::_default::ValidUTF8Seq(&invalidUnicode)) { + panic!("Halt") + }; + if !matches!( + (&super::UTF8::_default::Decode(&invalidUnicode)).as_ref(), + super::r#_Wrappers_Compile::Result::Failure { .. } + ) { + panic!("Halt") + }; + return (); + } + pub fn Test1Byte() -> () { + let mut decoded: ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16> = + ::dafny_runtime::seq![::dafny_runtime::DafnyCharUTF16(0 as u16)]; + let mut valueOrError0 = ::dafny_runtime::MaybePlacebo::< + ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + super::UTF8::ValidUTF8Bytes, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + >, + >, + >::new(); + valueOrError0 = + ::dafny_runtime::MaybePlacebo::from(super::UTF8::_default::Encode(&decoded)); + if !(!valueOrError0.read().IsFailure()) { + panic!("Halt") + }; + let mut encoded: super::UTF8::ValidUTF8Bytes = valueOrError0.read().Extract(); + if !(::dafny_runtime::seq![0] == encoded.clone()) { + panic!("Halt") + }; + if !super::UTF8::_default::Uses1Byte(&encoded) { + panic!("Halt") + }; + let mut valueOrError1 = ::dafny_runtime::MaybePlacebo::< + ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + >, + >, + >::new(); + valueOrError1 = + ::dafny_runtime::MaybePlacebo::from(super::UTF8::_default::Decode(&encoded)); + if !(!valueOrError1.read().IsFailure()) { + panic!("Halt") + }; + let mut redecoded: ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16> = + valueOrError1.read().Extract(); + if !(decoded.clone() == redecoded.clone()) { + panic!("Halt") + }; + decoded = ::dafny_runtime::seq![::dafny_runtime::DafnyCharUTF16(32 as u16)]; + let mut valueOrError2 = ::dafny_runtime::MaybePlacebo::< + ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + super::UTF8::ValidUTF8Bytes, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + >, + >, + >::new(); + valueOrError2 = + ::dafny_runtime::MaybePlacebo::from(super::UTF8::_default::Encode(&decoded)); + if !(!valueOrError2.read().IsFailure()) { + panic!("Halt") + }; + encoded = valueOrError2.read().Extract(); + if !(::dafny_runtime::seq![32] == encoded.clone()) { + panic!("Halt") + }; + if !super::UTF8::_default::Uses1Byte(&encoded) { + panic!("Halt") + }; + let mut valueOrError3 = ::dafny_runtime::MaybePlacebo::< + ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + >, + >, + >::new(); + valueOrError3 = + ::dafny_runtime::MaybePlacebo::from(super::UTF8::_default::Decode(&encoded)); + if !(!valueOrError3.read().IsFailure()) { + panic!("Halt") + }; + redecoded = valueOrError3.read().Extract(); + if !(decoded.clone() == redecoded.clone()) { + panic!("Halt") + }; + decoded = ::dafny_runtime::string_utf16_of("$"); + let mut valueOrError4 = ::dafny_runtime::MaybePlacebo::< + ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + super::UTF8::ValidUTF8Bytes, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + >, + >, + >::new(); + valueOrError4 = + ::dafny_runtime::MaybePlacebo::from(super::UTF8::_default::Encode(&decoded)); + if !(!valueOrError4.read().IsFailure()) { + panic!("Halt") + }; + encoded = valueOrError4.read().Extract(); + if !(::dafny_runtime::seq![36] == encoded.clone()) { + panic!("Halt") + }; + if !super::UTF8::_default::Uses1Byte(&encoded) { + panic!("Halt") + }; + let mut valueOrError5 = ::dafny_runtime::MaybePlacebo::< + ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + >, + >, + >::new(); + valueOrError5 = + ::dafny_runtime::MaybePlacebo::from(super::UTF8::_default::Decode(&encoded)); + if !(!valueOrError5.read().IsFailure()) { + panic!("Halt") + }; + redecoded = valueOrError5.read().Extract(); + if !(decoded.clone() == redecoded.clone()) { + panic!("Halt") + }; + decoded = ::dafny_runtime::string_utf16_of("0"); + let mut valueOrError6 = ::dafny_runtime::MaybePlacebo::< + ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + super::UTF8::ValidUTF8Bytes, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + >, + >, + >::new(); + valueOrError6 = + ::dafny_runtime::MaybePlacebo::from(super::UTF8::_default::Encode(&decoded)); + if !(!valueOrError6.read().IsFailure()) { + panic!("Halt") + }; + encoded = valueOrError6.read().Extract(); + if !(::dafny_runtime::seq![48] == encoded.clone()) { + panic!("Halt") + }; + if !super::UTF8::_default::Uses1Byte(&encoded) { + panic!("Halt") + }; + let mut valueOrError7 = ::dafny_runtime::MaybePlacebo::< + ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + >, + >, + >::new(); + valueOrError7 = + ::dafny_runtime::MaybePlacebo::from(super::UTF8::_default::Decode(&encoded)); + if !(!valueOrError7.read().IsFailure()) { + panic!("Halt") + }; + redecoded = valueOrError7.read().Extract(); + if !(decoded.clone() == redecoded.clone()) { + panic!("Halt") + }; + decoded = ::dafny_runtime::string_utf16_of("A"); + let mut valueOrError8 = ::dafny_runtime::MaybePlacebo::< + ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + super::UTF8::ValidUTF8Bytes, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + >, + >, + >::new(); + valueOrError8 = + ::dafny_runtime::MaybePlacebo::from(super::UTF8::_default::Encode(&decoded)); + if !(!valueOrError8.read().IsFailure()) { + panic!("Halt") + }; + encoded = valueOrError8.read().Extract(); + if !(::dafny_runtime::seq![65] == encoded.clone()) { + panic!("Halt") + }; + if !super::UTF8::_default::Uses1Byte(&encoded) { + panic!("Halt") + }; + let mut valueOrError9 = ::dafny_runtime::MaybePlacebo::< + ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + >, + >, + >::new(); + valueOrError9 = + ::dafny_runtime::MaybePlacebo::from(super::UTF8::_default::Decode(&encoded)); + if !(!valueOrError9.read().IsFailure()) { + panic!("Halt") + }; + redecoded = valueOrError9.read().Extract(); + if !(decoded.clone() == redecoded.clone()) { + panic!("Halt") + }; + decoded = ::dafny_runtime::string_utf16_of("a"); + let mut valueOrError10 = ::dafny_runtime::MaybePlacebo::< + ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + super::UTF8::ValidUTF8Bytes, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + >, + >, + >::new(); + valueOrError10 = + ::dafny_runtime::MaybePlacebo::from(super::UTF8::_default::Encode(&decoded)); + if !(!valueOrError10.read().IsFailure()) { + panic!("Halt") + }; + encoded = valueOrError10.read().Extract(); + if !(::dafny_runtime::seq![97] == encoded.clone()) { + panic!("Halt") + }; + if !super::UTF8::_default::Uses1Byte(&encoded) { + panic!("Halt") + }; + let mut valueOrError11 = ::dafny_runtime::MaybePlacebo::< + ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + >, + >, + >::new(); + valueOrError11 = + ::dafny_runtime::MaybePlacebo::from(super::UTF8::_default::Decode(&encoded)); + if !(!valueOrError11.read().IsFailure()) { + panic!("Halt") + }; + redecoded = valueOrError11.read().Extract(); + if !(decoded.clone() == redecoded.clone()) { + panic!("Halt") + }; + return (); + } + pub fn Test2Bytes() -> () { + let mut decoded: ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16> = + ::dafny_runtime::seq![::dafny_runtime::DafnyCharUTF16(163 as u16)]; + let mut valueOrError0 = ::dafny_runtime::MaybePlacebo::< + ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + super::UTF8::ValidUTF8Bytes, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + >, + >, + >::new(); + valueOrError0 = + ::dafny_runtime::MaybePlacebo::from(super::UTF8::_default::Encode(&decoded)); + if !(!valueOrError0.read().IsFailure()) { + panic!("Halt") + }; + let mut encoded: super::UTF8::ValidUTF8Bytes = valueOrError0.read().Extract(); + if !(::dafny_runtime::seq![194, 163] == encoded.clone()) { + panic!("Halt") + }; + if !super::UTF8::_default::Uses2Bytes(&encoded) { + panic!("Halt") + }; + let mut valueOrError1 = ::dafny_runtime::MaybePlacebo::< + ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + >, + >, + >::new(); + valueOrError1 = + ::dafny_runtime::MaybePlacebo::from(super::UTF8::_default::Decode(&encoded)); + if !(!valueOrError1.read().IsFailure()) { + panic!("Halt") + }; + let mut redecoded: ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16> = + valueOrError1.read().Extract(); + if !(decoded.clone() == redecoded.clone()) { + panic!("Halt") + }; + decoded = ::dafny_runtime::seq![::dafny_runtime::DafnyCharUTF16(169 as u16)]; + let mut valueOrError2 = ::dafny_runtime::MaybePlacebo::< + ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + super::UTF8::ValidUTF8Bytes, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + >, + >, + >::new(); + valueOrError2 = + ::dafny_runtime::MaybePlacebo::from(super::UTF8::_default::Encode(&decoded)); + if !(!valueOrError2.read().IsFailure()) { + panic!("Halt") + }; + encoded = valueOrError2.read().Extract(); + if !(::dafny_runtime::seq![194, 169] == encoded.clone()) { + panic!("Halt") + }; + if !super::UTF8::_default::Uses2Bytes(&encoded) { + panic!("Halt") + }; + let mut valueOrError3 = ::dafny_runtime::MaybePlacebo::< + ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + >, + >, + >::new(); + valueOrError3 = + ::dafny_runtime::MaybePlacebo::from(super::UTF8::_default::Decode(&encoded)); + if !(!valueOrError3.read().IsFailure()) { + panic!("Halt") + }; + redecoded = valueOrError3.read().Extract(); + if !(decoded.clone() == redecoded.clone()) { + panic!("Halt") + }; + decoded = ::dafny_runtime::seq![::dafny_runtime::DafnyCharUTF16(174 as u16)]; + let mut valueOrError4 = ::dafny_runtime::MaybePlacebo::< + ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + super::UTF8::ValidUTF8Bytes, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + >, + >, + >::new(); + valueOrError4 = + ::dafny_runtime::MaybePlacebo::from(super::UTF8::_default::Encode(&decoded)); + if !(!valueOrError4.read().IsFailure()) { + panic!("Halt") + }; + encoded = valueOrError4.read().Extract(); + if !(::dafny_runtime::seq![194, 174] == encoded.clone()) { + panic!("Halt") + }; + if !super::UTF8::_default::Uses2Bytes(&encoded) { + panic!("Halt") + }; + let mut valueOrError5 = ::dafny_runtime::MaybePlacebo::< + ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + >, + >, + >::new(); + valueOrError5 = + ::dafny_runtime::MaybePlacebo::from(super::UTF8::_default::Decode(&encoded)); + if !(!valueOrError5.read().IsFailure()) { + panic!("Halt") + }; + redecoded = valueOrError5.read().Extract(); + if !(decoded.clone() == redecoded.clone()) { + panic!("Halt") + }; + decoded = ::dafny_runtime::seq![::dafny_runtime::DafnyCharUTF16(960 as u16)]; + let mut valueOrError6 = ::dafny_runtime::MaybePlacebo::< + ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + super::UTF8::ValidUTF8Bytes, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + >, + >, + >::new(); + valueOrError6 = + ::dafny_runtime::MaybePlacebo::from(super::UTF8::_default::Encode(&decoded)); + if !(!valueOrError6.read().IsFailure()) { + panic!("Halt") + }; + encoded = valueOrError6.read().Extract(); + if !(::dafny_runtime::seq![207, 128] == encoded.clone()) { + panic!("Halt") + }; + if !super::UTF8::_default::Uses2Bytes(&encoded) { + panic!("Halt") + }; + let mut valueOrError7 = ::dafny_runtime::MaybePlacebo::< + ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + >, + >, + >::new(); + valueOrError7 = + ::dafny_runtime::MaybePlacebo::from(super::UTF8::_default::Decode(&encoded)); + if !(!valueOrError7.read().IsFailure()) { + panic!("Halt") + }; + redecoded = valueOrError7.read().Extract(); + if !(decoded.clone() == redecoded.clone()) { + panic!("Halt") + }; + return (); + } + pub fn Test3Bytes() -> () { + let mut decoded: ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16> = + ::dafny_runtime::seq![::dafny_runtime::DafnyCharUTF16(9094 as u16)]; + let mut valueOrError0 = ::dafny_runtime::MaybePlacebo::< + ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + super::UTF8::ValidUTF8Bytes, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + >, + >, + >::new(); + valueOrError0 = + ::dafny_runtime::MaybePlacebo::from(super::UTF8::_default::Encode(&decoded)); + if !(!valueOrError0.read().IsFailure()) { + panic!("Halt") + }; + let mut encoded: super::UTF8::ValidUTF8Bytes = valueOrError0.read().Extract(); + if !(::dafny_runtime::seq![226, 142, 134] == encoded.clone()) { + panic!("Halt") + }; + if !super::UTF8::_default::Uses3Bytes(&encoded) { + panic!("Halt") + }; + let mut valueOrError1 = ::dafny_runtime::MaybePlacebo::< + ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + >, + >, + >::new(); + valueOrError1 = + ::dafny_runtime::MaybePlacebo::from(super::UTF8::_default::Decode(&encoded)); + if !(!valueOrError1.read().IsFailure()) { + panic!("Halt") + }; + let mut redecoded: ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16> = + valueOrError1.read().Extract(); + if !(decoded.clone() == redecoded.clone()) { + panic!("Halt") + }; + decoded = ::dafny_runtime::seq![::dafny_runtime::DafnyCharUTF16(9095 as u16)]; + let mut valueOrError2 = ::dafny_runtime::MaybePlacebo::< + ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + super::UTF8::ValidUTF8Bytes, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + >, + >, + >::new(); + valueOrError2 = + ::dafny_runtime::MaybePlacebo::from(super::UTF8::_default::Encode(&decoded)); + if !(!valueOrError2.read().IsFailure()) { + panic!("Halt") + }; + encoded = valueOrError2.read().Extract(); + if !(::dafny_runtime::seq![226, 142, 135] == encoded.clone()) { + panic!("Halt") + }; + if !super::UTF8::_default::Uses3Bytes(&encoded) { + panic!("Halt") + }; + let mut valueOrError3 = ::dafny_runtime::MaybePlacebo::< + ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + >, + >, + >::new(); + valueOrError3 = + ::dafny_runtime::MaybePlacebo::from(super::UTF8::_default::Decode(&encoded)); + if !(!valueOrError3.read().IsFailure()) { + panic!("Halt") + }; + redecoded = valueOrError3.read().Extract(); + if !(decoded.clone() == redecoded.clone()) { + panic!("Halt") + }; + decoded = ::dafny_runtime::seq![::dafny_runtime::DafnyCharUTF16(8987 as u16)]; + let mut valueOrError4 = ::dafny_runtime::MaybePlacebo::< + ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + super::UTF8::ValidUTF8Bytes, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + >, + >, + >::new(); + valueOrError4 = + ::dafny_runtime::MaybePlacebo::from(super::UTF8::_default::Encode(&decoded)); + if !(!valueOrError4.read().IsFailure()) { + panic!("Halt") + }; + encoded = valueOrError4.read().Extract(); + if !(::dafny_runtime::seq![226, 140, 155] == encoded.clone()) { + panic!("Halt") + }; + if !super::UTF8::_default::Uses3Bytes(&encoded) { + panic!("Halt") + }; + let mut valueOrError5 = ::dafny_runtime::MaybePlacebo::< + ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + >, + >, + >::new(); + valueOrError5 = + ::dafny_runtime::MaybePlacebo::from(super::UTF8::_default::Decode(&encoded)); + if !(!valueOrError5.read().IsFailure()) { + panic!("Halt") + }; + redecoded = valueOrError5.read().Extract(); + if !(decoded.clone() == redecoded.clone()) { + panic!("Halt") + }; + decoded = ::dafny_runtime::seq![::dafny_runtime::DafnyCharUTF16(7544 as u16)]; + let mut valueOrError6 = ::dafny_runtime::MaybePlacebo::< + ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + super::UTF8::ValidUTF8Bytes, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + >, + >, + >::new(); + valueOrError6 = + ::dafny_runtime::MaybePlacebo::from(super::UTF8::_default::Encode(&decoded)); + if !(!valueOrError6.read().IsFailure()) { + panic!("Halt") + }; + encoded = valueOrError6.read().Extract(); + if !(::dafny_runtime::seq![225, 181, 184] == encoded.clone()) { + panic!("Halt") + }; + if !super::UTF8::_default::Uses3Bytes(&encoded) { + panic!("Halt") + }; + let mut valueOrError7 = ::dafny_runtime::MaybePlacebo::< + ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + >, + >, + >::new(); + valueOrError7 = + ::dafny_runtime::MaybePlacebo::from(super::UTF8::_default::Decode(&encoded)); + if !(!valueOrError7.read().IsFailure()) { + panic!("Halt") + }; + redecoded = valueOrError7.read().Extract(); + if !(decoded.clone() == redecoded.clone()) { + panic!("Halt") + }; + decoded = ::dafny_runtime::seq![::dafny_runtime::DafnyCharUTF16(29483 as u16)]; + let mut valueOrError8 = ::dafny_runtime::MaybePlacebo::< + ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + super::UTF8::ValidUTF8Bytes, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + >, + >, + >::new(); + valueOrError8 = + ::dafny_runtime::MaybePlacebo::from(super::UTF8::_default::Encode(&decoded)); + if !(!valueOrError8.read().IsFailure()) { + panic!("Halt") + }; + encoded = valueOrError8.read().Extract(); + if !(::dafny_runtime::seq![231, 140, 171] == encoded.clone()) { + panic!("Halt") + }; + if !super::UTF8::_default::Uses3Bytes(&encoded) { + panic!("Halt") + }; + let mut valueOrError9 = ::dafny_runtime::MaybePlacebo::< + ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + >, + >, + >::new(); + valueOrError9 = + ::dafny_runtime::MaybePlacebo::from(super::UTF8::_default::Decode(&encoded)); + if !(!valueOrError9.read().IsFailure()) { + panic!("Halt") + }; + redecoded = valueOrError9.read().Extract(); + if !(decoded.clone() == redecoded.clone()) { + panic!("Halt") + }; + return (); + } + pub fn Test4Bytes() -> () { + let mut decoded: ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16> = ::dafny_runtime::seq![ + ::dafny_runtime::DafnyCharUTF16(55304 as u16), + ::dafny_runtime::DafnyCharUTF16(56320 as u16) + ]; + let mut valueOrError0 = ::dafny_runtime::MaybePlacebo::< + ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + super::UTF8::ValidUTF8Bytes, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + >, + >, + >::new(); + valueOrError0 = + ::dafny_runtime::MaybePlacebo::from(super::UTF8::_default::Encode(&decoded)); + if !(!valueOrError0.read().IsFailure()) { + panic!("Halt") + }; + let mut encoded: super::UTF8::ValidUTF8Bytes = valueOrError0.read().Extract(); + if !(::dafny_runtime::seq![240, 146, 128, 128] == encoded.clone()) { + panic!("Halt") + }; + if !super::UTF8::_default::Uses4Bytes(&encoded) { + panic!("Halt") + }; + let mut valueOrError1 = ::dafny_runtime::MaybePlacebo::< + ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + >, + >, + >::new(); + valueOrError1 = + ::dafny_runtime::MaybePlacebo::from(super::UTF8::_default::Decode(&encoded)); + if !(!valueOrError1.read().IsFailure()) { + panic!("Halt") + }; + let mut redecoded: ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16> = + valueOrError1.read().Extract(); + if !(decoded.clone() == redecoded.clone()) { + panic!("Halt") + }; + decoded = ::dafny_runtime::seq![ + ::dafny_runtime::DafnyCharUTF16(55349 as u16), + ::dafny_runtime::DafnyCharUTF16(57281 as u16) + ]; + let mut valueOrError2 = ::dafny_runtime::MaybePlacebo::< + ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + super::UTF8::ValidUTF8Bytes, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + >, + >, + >::new(); + valueOrError2 = + ::dafny_runtime::MaybePlacebo::from(super::UTF8::_default::Encode(&decoded)); + if !(!valueOrError2.read().IsFailure()) { + panic!("Halt") + }; + encoded = valueOrError2.read().Extract(); + if !(::dafny_runtime::seq![240, 157, 159, 129] == encoded.clone()) { + panic!("Halt") + }; + if !super::UTF8::_default::Uses4Bytes(&encoded) { + panic!("Halt") + }; + let mut valueOrError3 = ::dafny_runtime::MaybePlacebo::< + ::std::rc::Rc< + super::r#_Wrappers_Compile::Result< + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + >, + >, + >::new(); + valueOrError3 = + ::dafny_runtime::MaybePlacebo::from(super::UTF8::_default::Decode(&encoded)); + if !(!valueOrError3.read().IsFailure()) { + panic!("Halt") + }; + redecoded = valueOrError3.read().Extract(); + if !(decoded.clone() == redecoded.clone()) { + panic!("Halt") + }; + return (); + } + } + + impl ::dafny_runtime::UpcastObject for super::r#_TestUTF8_Compile::_default { + ::dafny_runtime::UpcastObjectFn!(dyn::std::any::Any); + } +} +pub mod _module { + pub struct _default {} + + impl _default { + pub fn _allocate_object() -> ::dafny_runtime::Object { + ::dafny_runtime::allocate_object::() + } + pub fn _Test__Main_() -> () { + let mut success: bool = true; + print!( + "{}", + ::dafny_runtime::DafnyPrintWrapper(&::dafny_runtime::string_utf16_of( + r#"TestUTF8.TestEncodeHappyCase: "# + )) + ); + super::r#_TestUTF8_Compile::_default::TestEncodeHappyCase(); + print!( + "{}", + ::dafny_runtime::DafnyPrintWrapper(&::dafny_runtime::string_utf16_of( + r#"PASSED +"# + )) + ); + print!( + "{}", + ::dafny_runtime::DafnyPrintWrapper(&::dafny_runtime::string_utf16_of( + r#"TestUTF8.TestEncodeInvalidUnicode: "# + )) + ); + super::r#_TestUTF8_Compile::_default::TestEncodeInvalidUnicode(); + print!( + "{}", + ::dafny_runtime::DafnyPrintWrapper(&::dafny_runtime::string_utf16_of( + r#"PASSED +"# + )) + ); + print!( + "{}", + ::dafny_runtime::DafnyPrintWrapper(&::dafny_runtime::string_utf16_of( + r#"TestUTF8.TestDecodeHappyCase: "# + )) + ); + super::r#_TestUTF8_Compile::_default::TestDecodeHappyCase(); + print!( + "{}", + ::dafny_runtime::DafnyPrintWrapper(&::dafny_runtime::string_utf16_of( + r#"PASSED +"# + )) + ); + print!( + "{}", + ::dafny_runtime::DafnyPrintWrapper(&::dafny_runtime::string_utf16_of( + r#"TestUTF8.TestDecodeInvalidUnicode: "# + )) + ); + super::r#_TestUTF8_Compile::_default::TestDecodeInvalidUnicode(); + print!( + "{}", + ::dafny_runtime::DafnyPrintWrapper(&::dafny_runtime::string_utf16_of( + r#"PASSED +"# + )) + ); + print!( + "{}", + ::dafny_runtime::DafnyPrintWrapper(&::dafny_runtime::string_utf16_of( + r#"TestUTF8.Test1Byte: "# + )) + ); + super::r#_TestUTF8_Compile::_default::Test1Byte(); + print!( + "{}", + ::dafny_runtime::DafnyPrintWrapper(&::dafny_runtime::string_utf16_of( + r#"PASSED +"# + )) + ); + print!( + "{}", + ::dafny_runtime::DafnyPrintWrapper(&::dafny_runtime::string_utf16_of( + r#"TestUTF8.Test2Bytes: "# + )) + ); + super::r#_TestUTF8_Compile::_default::Test2Bytes(); + print!( + "{}", + ::dafny_runtime::DafnyPrintWrapper(&::dafny_runtime::string_utf16_of( + r#"PASSED +"# + )) + ); + print!( + "{}", + ::dafny_runtime::DafnyPrintWrapper(&::dafny_runtime::string_utf16_of( + r#"TestUTF8.Test3Bytes: "# + )) + ); + super::r#_TestUTF8_Compile::_default::Test3Bytes(); + print!( + "{}", + ::dafny_runtime::DafnyPrintWrapper(&::dafny_runtime::string_utf16_of( + r#"PASSED +"# + )) + ); + print!( + "{}", + ::dafny_runtime::DafnyPrintWrapper(&::dafny_runtime::string_utf16_of( + r#"TestUTF8.Test4Bytes: "# + )) + ); + super::r#_TestUTF8_Compile::_default::Test4Bytes(); + print!( + "{}", + ::dafny_runtime::DafnyPrintWrapper(&::dafny_runtime::string_utf16_of( + r#"PASSED +"# + )) + ); + if !success { + panic!("Halt") + }; + return (); + } + } + + impl ::dafny_runtime::UpcastObject for super::_module::_default { + ::dafny_runtime::UpcastObjectFn!(dyn::std::any::Any); + } +} +fn main() { + _module::_default::_Test__Main_(); +} diff --git a/TestModels/dafny-dependencies/StandardLibrary/src_for_rust/Index.dfy b/TestModels/dafny-dependencies/StandardLibrary/src_for_rust/Index.dfy deleted file mode 100644 index 0d6989a8a..000000000 --- a/TestModels/dafny-dependencies/StandardLibrary/src_for_rust/Index.dfy +++ /dev/null @@ -1,10 +0,0 @@ -// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. -// SPDX-License-Identifier: Apache-2.0 - -// Filtering to the subset of code that Dafny Rust code generation -// currently supports. - -// Only building UInt.dfy in Rust to start because other files use unsupported features -// (e.g. the variance specifiers in Option<+T>). -// This scope should be expanded over time. -include "../src/UInt.dfy" diff --git a/TestModels/dafny-dependencies/StandardLibrary/test_for_rust/Index.dfy b/TestModels/dafny-dependencies/StandardLibrary/test_for_rust/Index.dfy deleted file mode 100644 index 20e627c96..000000000 --- a/TestModels/dafny-dependencies/StandardLibrary/test_for_rust/Index.dfy +++ /dev/null @@ -1,5 +0,0 @@ -// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. -// SPDX-License-Identifier: Apache-2.0 - -// Filtering to the subset of code that Dafny Rust code generation -// currently supports.