Skip to content
Merged
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
19 changes: 15 additions & 4 deletions Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3358,6 +3358,7 @@ macro_rules! cast {
pub struct Object<T: ?Sized>(pub Option<rcmut::RcMut<T>>);

impl <T: ?Sized> Object<T> {
// For safety, it requires the Rc to have been created with Rc::new()
pub unsafe fn from_rc(rc: Rc<T>) -> Object<T> {
Object(Some(rcmut::from_rc(rc)))
}
Expand Down Expand Up @@ -3395,17 +3396,27 @@ impl <T: ?Sized>Default for Object<T> {
}
}

impl<T: ?Sized> Debug for Object<T> {
impl<T: ?Sized + UpcastObject<dyn Any>> Debug for Object<T> {
fn fmt(&self, f: &mut Formatter) -> std::fmt::Result {
self.fmt_print(f, false)
}
}
impl <T: ?Sized> DafnyPrint for Object<T> {
impl <T: ?Sized + UpcastObject<dyn Any>> DafnyPrint for Object<T> {
fn fmt_print(&self, f: &mut Formatter<'_>, _in_seq: bool) -> std::fmt::Result {
write!(f, "<object>")
let obj_any = UpcastObject::<dyn Any>::upcast(self.as_ref());
let option_string = obj_any.as_ref().downcast_ref::<String>();
match option_string {
Some(s) => write!(f, "{}", s),
None => write!(f, "<object>"),
}
}
}
impl UpcastObject<dyn Any> for String {
fn upcast(&self) -> Object<dyn Any> {
// SAFETY: RC was just created
unsafe { Object::from_rc(Rc::new(self.clone()) as Rc<dyn Any>) }
}
}


impl <T: ?Sized, U: ?Sized> PartialEq<Object<U>> for Object<T> {
fn eq(&self, other: &Object<U>) -> bool {
Expand Down
9 changes: 9 additions & 0 deletions Source/DafnyRuntime/DafnyRuntimeRust/src/tests/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -856,4 +856,13 @@ mod tests {
let s2 = crate::dafny_runtime_conversions::object::dafny_class_to_struct(x);
assert_eq!(s2.message, "Hello, World!");
}

#[test]
fn test_native_string_upcast_raw() {
let message = "Hello, World!".to_string();
let object = Object::new(message.clone());
let object_any: Object<dyn Any> = UpcastObject::<dyn Any>::upcast(object.as_ref());
let resulting_message = format!("{:?}", object_any);
assert_eq!(resulting_message, message);
}
}