aws_db_esdk/deps/aws_cryptography_dbEncryptionSdk_dynamoDb/conversions/
compound_beacon.rs

1// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
2// SPDX-License-Identifier: Apache-2.0
3// Do not modify this file. This file is machine generated, and any changes to it will be overwritten.
4#[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}