aws_db_esdk/deps/aws_cryptography_dbEncryptionSdk_dynamoDb/conversions/
compound_beacon.rs1#[allow(dead_code)]
5pub fn to_dafny(
6 value: &crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb::types::CompoundBeacon,
7) -> ::dafny_runtime::Rc<
8 crate::r#software::amazon::cryptography::dbencryptionsdk::dynamodb::internaldafny::types::CompoundBeacon,
9>{
10 ::dafny_runtime::Rc::new(to_dafny_plain(value.clone()))
11}
12
13#[allow(dead_code)]
14pub fn to_dafny_plain(
15 value: crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb::types::CompoundBeacon,
16) -> crate::r#software::amazon::cryptography::dbencryptionsdk::dynamodb::internaldafny::types::CompoundBeacon{
17 crate::r#software::amazon::cryptography::dbencryptionsdk::dynamodb::internaldafny::types::CompoundBeacon::CompoundBeacon {
18 name: crate::standard_library_conversions::ostring_to_dafny(&value.name) .Extract(),
19 split: crate::standard_library_conversions::ostring_to_dafny(&value.split) .Extract(),
20 encrypted: ::dafny_runtime::Rc::new(match &value.encrypted {
21 Some(x) => crate::r#_Wrappers_Compile::Option::Some { value :
22 ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x,
23 |e| crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb::conversions::encrypted_part::to_dafny(&e.clone())
24,
25 )
26 },
27 None => crate::r#_Wrappers_Compile::Option::None {}
28})
29,
30 signed: ::dafny_runtime::Rc::new(match &value.signed {
31 Some(x) => crate::r#_Wrappers_Compile::Option::Some { value :
32 ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x,
33 |e| crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb::conversions::signed_part::to_dafny(&e.clone())
34,
35 )
36 },
37 None => crate::r#_Wrappers_Compile::Option::None {}
38})
39,
40 constructors: ::dafny_runtime::Rc::new(match &value.constructors {
41 Some(x) => crate::r#_Wrappers_Compile::Option::Some { value :
42 ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x,
43 |e| crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb::conversions::constructor::to_dafny(&e.clone())
44,
45 )
46 },
47 None => crate::r#_Wrappers_Compile::Option::None {}
48})
49,
50 }
51}
52
53#[allow(dead_code)]
54pub fn option_to_dafny(
55 value: ::std::option::Option<crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb::types::CompoundBeacon>,
56) -> ::dafny_runtime::Rc<crate::_Wrappers_Compile::Option<::dafny_runtime::Rc<
57 crate::r#software::amazon::cryptography::dbencryptionsdk::dynamodb::internaldafny::types::CompoundBeacon,
58>>>{
59 ::dafny_runtime::Rc::new(match value {
60 ::std::option::Option::None => crate::_Wrappers_Compile::Option::None {},
61 ::std::option::Option::Some(x) => crate::_Wrappers_Compile::Option::Some {
62 value: ::dafny_runtime::Rc::new(to_dafny_plain(x)),
63 },
64 })
65}
66
67#[allow(dead_code)]
68pub fn from_dafny(
69 dafny_value: ::dafny_runtime::Rc<
70 crate::r#software::amazon::cryptography::dbencryptionsdk::dynamodb::internaldafny::types::CompoundBeacon,
71 >,
72) -> crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb::types::CompoundBeacon {
73 plain_from_dafny(&*dafny_value)
74}
75
76#[allow(dead_code)]
77pub fn plain_from_dafny(
78 dafny_value: &crate::r#software::amazon::cryptography::dbencryptionsdk::dynamodb::internaldafny::types::CompoundBeacon,
79) -> crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb::types::CompoundBeacon {
80 match dafny_value {
81 crate::r#software::amazon::cryptography::dbencryptionsdk::dynamodb::internaldafny::types::CompoundBeacon::CompoundBeacon {..} =>
82 crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb::types::CompoundBeacon::builder()
83 .set_name(Some( dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(dafny_value.name()) ))
84 .set_split(Some( dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(dafny_value.split()) ))
85 .set_encrypted(match (*dafny_value.encrypted()).as_ref() {
86 crate::r#_Wrappers_Compile::Option::Some { value } =>
87 Some(
88 ::dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(value,
89 |e: &::dafny_runtime::Rc<crate::r#software::amazon::cryptography::dbencryptionsdk::dynamodb::internaldafny::types::EncryptedPart>| crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb::conversions::encrypted_part::from_dafny(e.clone())
90,
91 )
92 ),
93 _ => None
94}
95)
96 .set_signed(match (*dafny_value.signed()).as_ref() {
97 crate::r#_Wrappers_Compile::Option::Some { value } =>
98 Some(
99 ::dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(value,
100 |e: &::dafny_runtime::Rc<crate::r#software::amazon::cryptography::dbencryptionsdk::dynamodb::internaldafny::types::SignedPart>| crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb::conversions::signed_part::from_dafny(e.clone())
101,
102 )
103 ),
104 _ => None
105}
106)
107 .set_constructors(match (*dafny_value.constructors()).as_ref() {
108 crate::r#_Wrappers_Compile::Option::Some { value } =>
109 Some(
110 ::dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(value,
111 |e: &::dafny_runtime::Rc<crate::r#software::amazon::cryptography::dbencryptionsdk::dynamodb::internaldafny::types::Constructor>| crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb::conversions::constructor::from_dafny(e.clone())
112,
113 )
114 ),
115 _ => None
116}
117)
118 .build()
119 .unwrap()
120 }
121}
122
123#[allow(dead_code)]
124pub fn option_from_dafny(
125 dafny_value: ::dafny_runtime::Rc<crate::_Wrappers_Compile::Option<::dafny_runtime::Rc<
126 crate::r#software::amazon::cryptography::dbencryptionsdk::dynamodb::internaldafny::types::CompoundBeacon,
127 >>>,
128) -> ::std::option::Option<
129 crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb::types::CompoundBeacon,
130> {
131 match &*dafny_value {
132 crate::_Wrappers_Compile::Option::Some { value } => {
133 ::std::option::Option::Some(plain_from_dafny(value))
134 }
135 _ => ::std::option::Option::None,
136 }
137}