Skip to content

Commit

Permalink
Merge branch 'master' into can-call-everywhere
Browse files Browse the repository at this point in the history
  • Loading branch information
RustanLeino committed Sep 27, 2024
2 parents 1cb2672 + 38db1b8 commit bcc497b
Show file tree
Hide file tree
Showing 2 changed files with 24 additions and 4 deletions.
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);
}
}

0 comments on commit bcc497b

Please sign in to comment.