Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ pub fn from_dafny(
obj: dafny_value.clone(),
};
$rustTypesModuleName:L::$snakeCaseResourceName:L::$rustResourceName:LRef {
inner: ::dafny_runtime::Rc::new(::dafny_runtime::RefCell::new(wrap))
inner: $rustTypesModuleName:L::$snakeCaseResourceName:L::ResourceInner::new(wrap)
}
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -7,18 +7,89 @@ pub trait $rustResourceName:L : Send + Sync {
#[derive(::std::clone::Clone)]
/// A reference to a $rustResourceName:L
pub struct $rustResourceName:LRef {
pub inner: ::dafny_runtime::Rc<::dafny_runtime::RefCell<dyn $rustResourceName:L>>
pub inner: ResourceInner<dyn $rustResourceName:L>
}

/// A wrapper around Rc (or Arc with the `sync` feature) that provides a no-op .lock() method for backwards compatibility.
///
/// Since the trait requires Send + Sync, no actual locking is needed - the inner value
/// is already thread-safe. The .lock() method simply returns a guard that derefs to the inner value.
pub struct ResourceInner<T: ?Sized>(::dafny_runtime::Rc<T>);

impl<T: ?Sized> Clone for ResourceInner<T> {
fn clone(&self) -> Self {
ResourceInner(self.0.clone())
}
}

impl<T: ?Sized> ResourceInner<T> {
/// Returns a guard providing access to the inner resource.
///
/// This method exists for backwards compatibility with code that used the old
/// Mutex-based API. No actual locking occurs - the guard simply provides access
/// to the inner Arc.
#[inline]
pub fn lock(&self) -> Result<ResourceGuard<'_, T>, ::std::convert::Infallible> {
Ok(ResourceGuard(&self.0))
}

/// Compares two ResourceInner pointers for equality.
#[inline]
pub fn ptr_eq(&self, other: &Self) -> bool {
::dafny_runtime::Rc::ptr_eq(&self.0, &other.0)
}
}

impl ResourceInner<dyn $rustResourceName:L> {
/// Creates a new ResourceInner wrapping the given value.
pub fn new<T: $rustResourceName:L + 'static>(value: T) -> Self {
ResourceInner(::dafny_runtime::Rc::new(value) as ::dafny_runtime::Rc<dyn $rustResourceName:L>)
}
}

impl<T: ?Sized> ::std::ops::Deref for ResourceInner<T> {
type Target = T;
#[inline]
fn deref(&self) -> &Self::Target {
&self.0
}
}

/// A guard that provides access to a resource. Returned by ResourceInner::lock().
///
/// Unlike MutexGuard, this does not actually hold a lock - it simply provides
/// a reference to the underlying resource.
pub struct ResourceGuard<'a, T: ?Sized>(&'a ::dafny_runtime::Rc<T>);

impl<T: ?Sized> ::std::ops::Deref for ResourceGuard<'_, T> {
type Target = T;
#[inline]
fn deref(&self) -> &Self::Target {
&self.0
}
}

impl<T: ?Sized> ::std::fmt::Debug for ResourceInner<T> {
fn fmt(&self, f: &mut ::std::fmt::Formatter<'_>) -> ::std::fmt::Result {
write!(f, "ResourceInner(...)")
}
}

impl<T: ?Sized> ::std::fmt::Debug for ResourceGuard<'_, T> {
fn fmt(&self, f: &mut ::std::fmt::Formatter<'_>) -> ::std::fmt::Result {
write!(f, "ResourceGuard(...)")
}
}

impl<T : $rustResourceName:L + 'static> From<T> for $rustResourceName:LRef {
fn from(value: T) -> Self {
Self { inner: dafny_runtime::Rc::new(::dafny_runtime::RefCell::new(value)) }
Self { inner: ResourceInner::new(value) }
}
}

impl ::std::cmp::PartialEq for $rustResourceName:LRef {
fn eq(&self, other: &$rustResourceName:LRef) -> bool {
::dafny_runtime::Rc::ptr_eq(&self.inner, &other.inner)
self.inner.ptr_eq(&other.inner)
}
}

Expand Down