in DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToDafny.java [195:241]
public static CompoundBeacon CompoundBeacon(
software.amazon.cryptography.dbencryptionsdk.dynamodb.model.CompoundBeacon nativeValue
) {
DafnySequence<? extends Character> name;
name =
software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(
nativeValue.name()
);
DafnySequence<? extends Character> split;
split =
software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(
nativeValue.split()
);
Option<DafnySequence<? extends EncryptedPart>> encrypted;
encrypted =
(Objects.nonNull(nativeValue.encrypted()) &&
nativeValue.encrypted().size() > 0)
? Option.create_Some(
DafnySequence._typeDescriptor(EncryptedPart._typeDescriptor()),
ToDafny.EncryptedPartsList(nativeValue.encrypted())
)
: Option.create_None(
DafnySequence._typeDescriptor(EncryptedPart._typeDescriptor())
);
Option<DafnySequence<? extends SignedPart>> signed;
signed =
(Objects.nonNull(nativeValue.signed()) && nativeValue.signed().size() > 0)
? Option.create_Some(
DafnySequence._typeDescriptor(SignedPart._typeDescriptor()),
ToDafny.SignedPartsList(nativeValue.signed())
)
: Option.create_None(
DafnySequence._typeDescriptor(SignedPart._typeDescriptor())
);
Option<DafnySequence<? extends Constructor>> constructors;
constructors =
(Objects.nonNull(nativeValue.constructors()) &&
nativeValue.constructors().size() > 0)
? Option.create_Some(
DafnySequence._typeDescriptor(Constructor._typeDescriptor()),
ToDafny.ConstructorList(nativeValue.constructors())
)
: Option.create_None(
DafnySequence._typeDescriptor(Constructor._typeDescriptor())
);
return new CompoundBeacon(name, split, encrypted, signed, constructors);
}