Skip to content

Commit

Permalink
fmt
Browse files Browse the repository at this point in the history
  • Loading branch information
lucasmcdonald3 committed Jan 16, 2025
1 parent 6d76995 commit b6f21d4
Show file tree
Hide file tree
Showing 2 changed files with 30 additions and 30 deletions.
56 changes: 28 additions & 28 deletions TestModels/OrphanedShapes/runtimes/rust/src/extern_definitions.rs
Original file line number Diff line number Diff line change
@@ -1,25 +1,24 @@
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0

use std::rc::Rc;
use std::cell::UnsafeCell;
use dafny_runtime::rcmut;
use crate::r#_Wrappers_Compile::Result;
use crate::simple::orphaned::internaldafny::types;
use dafny_runtime::rcmut;
use std::cell::UnsafeCell;
use std::rc::Rc;

pub mod internal_ExternDefinitions_Compile {

use crate::conversions::*;
use crate::types::*;
use crate::implementation_from_dafny::_OrphanedResource_Compile::*;
use crate::implementation_from_dafny::_ExternDefinitions_Compile::_default;
use crate::implementation_from_dafny::_OrphanedResource_Compile::*;
use crate::simple::orphaned::internaldafny::types::*;

use crate::types::*;

impl _default {
pub fn InitializeOrphanedStructure(
uninitialized_structure: &Rc<crate::simple::orphaned::internaldafny::types::OrphanedStructure>,
) -> Rc<crate::simple::orphaned::internaldafny::types::OrphanedStructure> {

uninitialized_structure: &Rc<types::OrphanedStructure>,
) -> Rc<types::OrphanedStructure> {
let native_structure = orphaned_structure::from_dafny(uninitialized_structure.clone());
// I don't think generated Rust objects have a "toBuilder" method.
// Ideally, this extern would convert the Dafny structure to native,
Expand All @@ -34,31 +33,32 @@ pub mod internal_ExternDefinitions_Compile {

pub fn CallNativeOrphanedResource(
dafny_resource: &Object<dyn IOrphanedResource>,
) -> Rc<Result<Rc<crate::simple::orphaned::internaldafny::types::OrphanedResourceOperationOutput>, Rc<Error>>>
{
let native_resource_ref = crate::conversions::orphaned_resource::from_dafny(dafny_resource.clone());
) -> Rc<Result<Rc<types::OrphanedResourceOperationOutput>, Rc<Error>>> {
let native_resource_ref =
crate::conversions::orphaned_resource::from_dafny(dafny_resource.clone());
let native_resource = native_resource_ref.inner.borrow();
let native_output = native_resource.orphaned_resource_operation(
crate::operation::orphaned_resource_operation::OrphanedResourceOperationInput{
some_string : std::option::Option::Some (
"the extern MUST provide this string to the native resource's operation".to_string()
)
}
crate::operation::orphaned_resource_operation::OrphanedResourceOperationInput {
some_string: std::option::Option::Some(
"the extern MUST provide this string to the native resource's operation"
.to_string(),
),
},
);

let dafny_output = orphaned_resource_operation::_orphaned_resource_operation_output::to_dafny(native_output.unwrap());

::std::rc::Rc::new(Result::<
Rc<crate::simple::orphaned::internaldafny::types::OrphanedResourceOperationOutput>,
Rc<Error>
>::Success {
value: dafny_output,
})
let dafny_output =
orphaned_resource_operation::_orphaned_resource_operation_output::to_dafny(
native_output.unwrap(),
);

::std::rc::Rc::new(
Result::<Rc<types::OrphanedResourceOperationOutput>, Rc<Error>>::Success {
value: dafny_output,
},
)
}

pub fn CallNativeOrphanedError(
dafny_error: &Rc<Error>,
) -> Rc<Error> {
pub fn CallNativeOrphanedError(dafny_error: &Rc<Error>) -> Rc<Error> {
let native_error = crate::conversions::error::from_dafny(dafny_error.clone());
// I don't think generated Rust objects have a way for me to update the message
// on a pre-existing object (i.e. public fields or a .toBuilder).
Expand Down
4 changes: 2 additions & 2 deletions TestModels/OrphanedShapes/runtimes/rust/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -11,15 +11,15 @@ pub mod conversions;
pub mod deps;
/// Common errors and error handling utilities.
pub mod error;
pub mod extern_definitions;
pub(crate) mod implementation_from_dafny;
/// All operations that this crate can perform.
pub mod operation;
pub mod validation;
mod standard_library_conversions;
mod standard_library_externs;
pub mod types;
pub mod validation;
pub mod wrapped;
pub mod extern_definitions;
pub(crate) use crate::implementation_from_dafny::r#_Wrappers_Compile;
pub(crate) use crate::implementation_from_dafny::simple;
pub use crate::types::simple_orphaned_config::SimpleOrphanedConfig;
Expand Down

0 comments on commit b6f21d4

Please sign in to comment.