aws_db_esdk/deps/aws_cryptography_dbEncryptionSdk_dynamoDb/conversions/
virtual_field.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::VirtualField,
7) -> ::dafny_runtime::Rc<
8    crate::r#software::amazon::cryptography::dbencryptionsdk::dynamodb::internaldafny::types::VirtualField,
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::VirtualField,
16) -> crate::r#software::amazon::cryptography::dbencryptionsdk::dynamodb::internaldafny::types::VirtualField{
17    crate::r#software::amazon::cryptography::dbencryptionsdk::dynamodb::internaldafny::types::VirtualField::VirtualField {
18        name: crate::standard_library_conversions::ostring_to_dafny(&value.name) .Extract(),
19 parts: ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(&value.parts.clone().unwrap(),
20    |e| crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb::conversions::virtual_part::to_dafny(&e.clone())
21,
22)
23,
24    }
25}
26
27#[allow(dead_code)]
28pub fn option_to_dafny(
29  value: ::std::option::Option<crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb::types::VirtualField>,
30) -> ::dafny_runtime::Rc<crate::_Wrappers_Compile::Option<::dafny_runtime::Rc<
31  crate::r#software::amazon::cryptography::dbencryptionsdk::dynamodb::internaldafny::types::VirtualField,
32>>>{
33    ::dafny_runtime::Rc::new(match value {
34        ::std::option::Option::None => crate::_Wrappers_Compile::Option::None {},
35        ::std::option::Option::Some(x) => crate::_Wrappers_Compile::Option::Some {
36            value: ::dafny_runtime::Rc::new(to_dafny_plain(x)),
37        },
38    })
39}
40
41#[allow(dead_code)]
42pub fn from_dafny(
43    dafny_value: ::dafny_runtime::Rc<
44        crate::r#software::amazon::cryptography::dbencryptionsdk::dynamodb::internaldafny::types::VirtualField,
45    >,
46) -> crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb::types::VirtualField {
47    plain_from_dafny(&*dafny_value)
48}
49
50#[allow(dead_code)]
51pub fn plain_from_dafny(
52    dafny_value: &crate::r#software::amazon::cryptography::dbencryptionsdk::dynamodb::internaldafny::types::VirtualField,
53) -> crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb::types::VirtualField {
54    match dafny_value {
55        crate::r#software::amazon::cryptography::dbencryptionsdk::dynamodb::internaldafny::types::VirtualField::VirtualField {..} =>
56            crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb::types::VirtualField::builder()
57                .set_name(Some( dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(dafny_value.name()) ))
58 .set_parts(Some( ::dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(dafny_value.parts(),
59    |e: &::dafny_runtime::Rc<crate::r#software::amazon::cryptography::dbencryptionsdk::dynamodb::internaldafny::types::VirtualPart>| crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb::conversions::virtual_part::from_dafny(e.clone())
60,
61)
62 ))
63                .build()
64                .unwrap()
65    }
66}
67
68#[allow(dead_code)]
69pub fn option_from_dafny(
70    dafny_value: ::dafny_runtime::Rc<crate::_Wrappers_Compile::Option<::dafny_runtime::Rc<
71        crate::r#software::amazon::cryptography::dbencryptionsdk::dynamodb::internaldafny::types::VirtualField,
72    >>>,
73) -> ::std::option::Option<
74    crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb::types::VirtualField,
75> {
76    match &*dafny_value {
77        crate::_Wrappers_Compile::Option::Some { value } => {
78            ::std::option::Option::Some(plain_from_dafny(value))
79        }
80        _ => ::std::option::Option::None,
81    }
82}
aws_db_esdk/deps/aws_cryptography_dbEncryptionSdk_dynamoDb/conversions/virtual_field.rs

aws_db_esdk/deps/aws_cryptography_dbEncryptionSdk_dynamoDb/conversions/
virtual_field.rs
