Chore refactoring types

Source/DafnyRuntime.Tests/DafnyRuntimeRustTest/.gitignore

@@ -0,0 +1 @@
+target/

Source/DafnyRuntime.Tests/DafnyRuntimeRustTest/Cargo.toml

@@ -0,0 +1,7 @@
+[package]
+name = "DafnyRuntimeRustTest"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]
+dafny_runtime = {path= "../../DafnyRuntime/DafnyRuntimeRust"}

Source/DafnyRuntime.Tests/DafnyRuntimeRustTest/src/main.rs

@@ -0,0 +1,39 @@
+use dafny_runtime::{Upcast, UpcastObject};
+
+
+
+struct SmokeStruct {
+    pub i: i32,
+}
+pub struct OtherSmokeStruct(pub i32);
+
+impl UpcastObject<dyn ::std::any::Any> for SmokeStruct {
+    dafny_runtime::UpcastObjectFn!(dyn ::std::any::Any);
+}
+impl Upcast<dyn ::std::any::Any> for SmokeStruct {
+    dafny_runtime::UpcastFn!(dyn ::std::any::Any);
+}
+
+#[test]
+fn smoke_test() {
+    let mut x = ::dafny_runtime::dafny_runtime_conversions::object::boxed_struct_to_dafny_class(Box::new(SmokeStruct{i: 3}));
+    assert_eq!(::dafny_runtime::refcount!(x), 1);
+    let y = ::dafny_runtime::cast_any_object!(x);
+    assert_eq!(::dafny_runtime::refcount!(x), 2);
+    assert!(::dafny_runtime::is_object!(y, SmokeStruct));
+    assert!(!::dafny_runtime::is_object!(y, OtherSmokeStruct));
+    assert_eq!(::dafny_runtime::rd!(x).i, 3);
+    x = ::dafny_runtime::cast_object!(y, SmokeStruct);
+    assert_eq!(::dafny_runtime::rd!(x).i, 3);
+    let mut x = ::dafny_runtime::dafny_runtime_conversions::ptr::boxed_struct_to_dafny_class(Box::new(SmokeStruct{i: 3}));
+    let y = ::dafny_runtime::cast_any!(x);
+    assert!(::dafny_runtime::is!(y, SmokeStruct));
+    assert!(!::dafny_runtime::is!(y, OtherSmokeStruct));
+    assert_eq!(::dafny_runtime::read!(x).i, 3);
+    x = ::dafny_runtime::cast!(y, SmokeStruct);
+    assert_eq!(::dafny_runtime::read!(x).i, 3);
+    let z = ::dafny_runtime::truncate!(::dafny_runtime::int!(3), usize);
+    let a = ::dafny_runtime::array!(1, 2, 3);
+    assert_eq!(z, 3);
+    assert_eq!(::dafny_runtime::read!(a)[2], 3);
+}

Source/DafnyRuntime/DafnyRuntimeRust/Makefile

@@ -18,4 +18,5 @@ update-system-module: build-system-module
 	cp $(GENERATED_SYSTEM_MODULE_SOURCE) $(GENERATED_SYSTEM_MODULE_TARGET)
 
 test:
-	cargo test
+	cargo test
+	(cd ../../DafnyRuntime.Tests/DafnyRuntimeRustTest; cargo test)

Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs

@@ -322,7 +322,7 @@ impl AsRef<BigInt> for DafnyInt {
 #[macro_export]
 macro_rules! truncate {
     ($x:expr, $t:ty) => {
-        <$crate::DafnyInt as $crate::Into<$t>>::into($x)
+        <$crate::DafnyInt as ::std::convert::Into<$t>>::into($x)
     };
 }
 
@@ -594,10 +594,10 @@ impl DafnyInt {
 macro_rules! impl_dafnyint_from {
     () => {};
     ($type:ident) => {
-        impl $crate::From<$type> for $crate::DafnyInt {
+        impl ::std::convert::From<$type> for $crate::DafnyInt {
             fn from(n: $type) -> Self {
                 $crate::DafnyInt {
-                    data: $crate::Rc::new(n.into()),
+                    data: ::std::rc::Rc::new(n.into()),
                 }
             }
         }
@@ -1990,7 +1990,7 @@ impl<A: DafnyPrint> DafnyPrint for LazyFieldWrapper<A> {
 // Convert the DafnyPrint above into a macro so that we can create it for functions of any input arity
 macro_rules! dafny_print_function {
     ($($n:tt)*) => {
-        impl <B, $($n),*> $crate::DafnyPrint for $crate::Rc<dyn $crate::Fn($($n),*) -> B> {
+        impl <B, $($n),*> $crate::DafnyPrint for ::std::rc::Rc<dyn ::std::ops::Fn($($n),*) -> B> {
             fn fmt_print(&self, f: &mut ::std::fmt::Formatter<'_>, _in_seq: bool) -> ::std::fmt::Result {
                 write!(f, "<function>")
             }
@@ -2557,14 +2557,14 @@ macro_rules! ARRAY_GETTER_LENGTH {
 #[macro_export]
 macro_rules! array {
     ($($x:expr), *) => {
-        $crate::array::from_native($crate::Box::new([$($x), *]))
+        $crate::array::from_native(::std::boxed::Box::new([$($x), *]))
     }
 }
 
 macro_rules! ARRAY_INIT {
     {$length: ident, $inner: expr} => {
         $crate::array::initialize_box_usize($length, {
-            $crate::Rc::new(move |_| { $inner })
+            ::std::rc::Rc::new(move |_| { $inner })
         })
     }
 }
@@ -2579,10 +2579,10 @@ macro_rules! ARRAY_INIT_INNER {
 // Box<[Box<[Box<[T]>]>]>
 macro_rules! ARRAY_DATA_TYPE {
     ($length:ident) => {
-        $crate::Box<[T]>
+        ::std::boxed::Box<[T]>
     };
     ($length:ident, $($rest_length:ident),+) => {
-        $crate::Box<[ARRAY_DATA_TYPE!($($rest_length),+)]>
+        ::std::boxed::Box<[ARRAY_DATA_TYPE!($($rest_length),+)]>
     };
 }
 
@@ -2606,8 +2606,8 @@ macro_rules! ARRAY_METHODS {
         pub fn placebos_box_usize(
             $length0: usize,
             $($length: usize),+
-        ) -> $crate::Box<$ArrayType<$crate::MaybeUninit<T>>> {
-            $crate::Box::new($ArrayType {
+        ) -> ::std::boxed::Box<$ArrayType<$crate::MaybeUninit<T>>> {
+            ::std::boxed::Box::new($ArrayType {
                 $($length: $length),+,
                 data: INIT_ARRAY_DATA!($ArrayType, $length0, $($length),+),
             })
@@ -2676,15 +2676,15 @@ macro_rules! ARRAY_TO_VEC_LOOP {
     };
     (@inner $self: ident, $outerTmp: ident, $data: expr $(, $rest_length_usize: ident)*) => {
         {
-            let mut tmp = $crate::Vec::new();
+            let mut tmp = ::std::vec::Vec::new();
             ARRAY_TO_VEC_LOOP!(@for $self, tmp, $data $(, $rest_length_usize)*);
             $outerTmp.push(tmp);
         }
     };
 
     ($self: ident, $data: expr $(, $rest_length_usize: ident)*) => {
         {
-            let mut tmp = $crate::Vec::new();
+            let mut tmp = ::std::vec::Vec::new();
             ARRAY_TO_VEC_LOOP!(@for $self, tmp, $data $(, $rest_length_usize)*);
             tmp
         }
@@ -2693,10 +2693,10 @@ macro_rules! ARRAY_TO_VEC_LOOP {
 
 macro_rules! ARRAY_TO_VEC_TYPE {
     ($length0: ident) => {
-        $crate::Vec<T>
+        ::std::vec::Vec<T>
     };
     ($length0: ident $(, $res_length: ident)*) => {
-        $crate::Vec<ARRAY_TO_VEC_TYPE!($($res_length), *)>
+        ::std::vec::Vec<ARRAY_TO_VEC_TYPE!($($res_length), *)>
     }
 }
 
@@ -2751,7 +2751,7 @@ macro_rules! ARRAY_DEF {
                 $(($length, $length_usize)), +
             }
         }
-        impl<T: $crate::Clone> $ArrayType<T> {
+        impl<T: ::std::clone::Clone> $ArrayType<T> {
             ARRAY_TO_VEC_WRAPPER!{
                 $(($length, $length_usize)), +
             }
@@ -3111,15 +3111,15 @@ macro_rules! is_object {
 #[macro_export]
 macro_rules! cast_any {
     ($raw:expr) => {
-        $crate::Upcast::<dyn $crate::Any>::upcast($crate::read!($raw))
+        $crate::Upcast::<dyn ::std::any::Any>::upcast($crate::read!($raw))
     };
 }
 // cast_any_object is meant to be used on references only, to convert any references (classes or traits)*
 // to an Any reference trait
 #[macro_export]
 macro_rules! cast_any_object {
     ($obj:expr) => {
-        $crate::UpcastObject::<dyn $crate::Any>::upcast($crate::md!($obj))
+        $crate::UpcastObject::<dyn ::std::any::Any>::upcast($crate::md!($obj))
     };
 }
 
@@ -3555,7 +3555,7 @@ macro_rules! rd {
 #[macro_export]
 macro_rules! refcount {
     ($x:expr) => {
-        $crate::Rc::strong_count(unsafe { $crate::rcmut::as_rc($x.0.as_ref().unwrap()) })
+        ::std::rc::Rc::strong_count(unsafe { $crate::rcmut::as_rc($x.0.as_ref().unwrap()) })
     };
 }
 

Source/DafnyRuntime/DafnyRuntimeRust/src/tests/mod.rs

@@ -853,9 +853,7 @@ mod tests {
         let o: Object<InternalOpaqueError> = Object::new(s);
         let n: Object<dyn ::std::any::Any> = upcast_object::<InternalOpaqueError, dyn ::std::any::Any>()(o);
         let x = cast_object!(n, InternalOpaqueError);
-        let s2 = unsafe {
-            crate::dafny_runtime_conversions::object::dafny_class_to_struct(x)
-        };
+        let s2 = crate::dafny_runtime_conversions::object::dafny_class_to_struct(x);
         assert_eq!(s2.message, "Hello, World!");
     }
 }