Merge branch 'master' into feat-simplified-rust-identifiers

dafny-lang · Oct 24, 2024 · e732a5f · e732a5f
2 parents 74d4d75 + a38e8a4
commit e732a5f
Show file tree

Hide file tree

Showing 3 changed files with 22 additions and 7 deletions.
diff --git a/.github/workflows/nightly-build.yml b/.github/workflows/nightly-build.yml
@@ -23,11 +23,11 @@ on:
   workflow_dispatch:
 
 jobs:
-  nightly-build-for-master:
+  nightly-build-for-4-9:
     if: github.repository_owner == 'dafny-lang'
     uses: ./.github/workflows/nightly-build-reusable.yml
     with:
-      ref: master
+      ref: 4.9
       publish-prerelease: true
     secrets:
       nuget_api_key: ${{ secrets.NUGET_API_KEY }}
diff --git a/Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs b/Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs
@@ -3450,6 +3450,13 @@ impl <T: ?Sized + UpcastObject<dyn Any>> DafnyPrint for Object<T> {
         }
     }
 }
+
+impl <T: DafnyType> DafnyPrint for Object<[T]> {
+    fn fmt_print(&self, f: &mut Formatter<'_>, _in_seq: bool) -> std::fmt::Result {
+        write!(f, "<object>")
+    }
+}
+
 impl UpcastObject<dyn Any> for String {
     fn upcast(&self) -> Object<dyn Any> {
         // SAFETY: RC was just created
@@ -3642,9 +3649,11 @@ macro_rules! rd {
 #[macro_export]
 macro_rules! modify_field {
     ($pointer:expr, $rhs:expr) => {
-        let lhs = $pointer.get();
-        let rhs = $rhs;
-        unsafe {*lhs = rhs}
+        {
+            let lhs = $pointer.get();
+            let rhs = $rhs;
+            unsafe {*lhs = rhs}
+        }
     };
 }
 
@@ -4036,4 +4045,4 @@ impl<K: DafnyTypeEq, U: DafnyTypeEq> Map<K, U>
             Map::from_hashmap_owned(new_map)
         })
     }
-}
+}
diff --git a/Source/DafnyRuntime/DafnyRuntimeRust/src/tests/mod.rs b/Source/DafnyRuntime/DafnyRuntimeRust/src/tests/mod.rs
@@ -478,7 +478,9 @@ mod tests {
         assert_eq!(rd!(c).constant_plus_x(), int!(42));
         md!(c).increment_x();
         assert_eq!(rd!(c).constant_plus_x(), int!(43));
-        modify_field!(rd!(c).x,int!(40));
+        if true {
+          modify_field!(rd!(c).x,int!(40))
+        }
         assert_eq!(rd!(c).constant_plus_x(), int!(82));
         modify_field!(rd!(c).t,54);
         assert_eq!(read_field!(rd!(c).t), 54);
@@ -829,6 +831,7 @@ mod tests {
 
         let objects: Set<Object<dyn ::std::any::Any>> = crate::set!{y.clone(), cast_any_object!(x.clone())};
         assert_eq!(objects.cardinality_usize(), 1);
+        test_dafny_type(a.clone());
     }
 
     pub struct NodeRawMut {
@@ -890,6 +893,9 @@ mod tests {
     // Tests that we can compose Dafny types, like a sequence of maps
     fn _test<X: DafnyTypeEq, Y: DafnyType>(_input: Sequence<Map<X, Y>>) {
     }
+    // Tests that the input type is a DafnyType
+    fn test_dafny_type<X: DafnyType>(_input: X) {
+    }
 
     #[derive(Clone)]
     pub struct InternalOpaqueError {