Skip to content

Commit 10c60f4

Browse files
MikaelMayerMikaelMayer
committed
Support for sync-ed functions
1 parent dfb533a commit 10c60f4

File tree

7 files changed

+106
-44
lines changed

7 files changed

+106
-44
lines changed

‎Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy

+6-5
Original file line numberDiff line numberDiff line change
@@ -70,7 +70,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
7070
const AnyTrait := if syncType.NoSync? then
7171
R.dafny_runtime.MSel("Any").AsType()
7272
else
73-
R.IntersectionType(R.dafny_runtime.MSel("Any").AsType(), SyncSendType);
73+
R.IntersectionType(R.dafny_runtime.MSel("Any").AsType(), SyncSendType)
7474
const DynAny := R.dafny_runtime.MSel("DynAny").AsType()
7575

7676
var error: Option<string>
@@ -591,9 +591,6 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
591591
];
592592
}
593593
}
594-
if syncType.Sync? {
595-
parents := parents + [R.SyncType, R.SendType];
596-
}
597594
s := [
598595
R.TraitDecl(
599596
R.Trait(
@@ -1508,8 +1505,12 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
15081505
}
15091506

15101507
var resultType := GenType(result, GenTypeContext.default());
1508+
var fnType := R.DynType(R.FnType(argTypes, resultType));
1509+
if syncType.Sync? {
1510+
fnType := R.IntersectionType(fnType, SyncSendType);
1511+
}
15111512
s :=
1512-
rc(R.DynType(R.FnType(argTypes, resultType)));
1513+
rc(fnType);
15131514
}
15141515
case TypeArg(Ident(name)) => s := R.TIdentifier(escapeName(name));
15151516
case Primitive(p) => {

‎Source/DafnyCore/GeneratedFromDafny/DCOMP.cs

+18-13
Original file line numberDiff line numberDiff line change
@@ -492,7 +492,7 @@ public void GetName(Dafny.ISequence<DAST._IAttribute> attributes, Dafny.ISequenc
492492
_out13 = (this).GenPathType(path);
493493
_28_genSelfPath = _out13;
494494
if (!(_16_className).Equals(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("_default"))) {
495-
s = Dafny.Sequence<RAST._IModDecl>.Concat(s, Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(_2_rTypeParamsDecls, (((RAST.__default.dafny__runtime).MSel((this).Upcast)).AsType()).Apply(Dafny.Sequence<RAST._IType>.FromElements(RAST.Type.create_DynType((this).AnyTrait))), RAST.Type.create_TypeApp(_28_genSelfPath, _1_rTypeParams), Dafny.Sequence<RAST._IImplMember>.FromElements(RAST.ImplMember.create_ImplMemberMacro((((RAST.__default.dafny__runtime).MSel((this).UpcastFnMacro)).AsExpr()).Apply1(RAST.Expr.create_ExprFromType(RAST.Type.create_DynType((this).AnyTrait)))))))));
495+
s = Dafny.Sequence<RAST._IModDecl>.Concat(s, Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(_2_rTypeParamsDecls, (((RAST.__default.dafny__runtime).MSel((this).Upcast)).AsType()).Apply(Dafny.Sequence<RAST._IType>.FromElements((this).DynAny)), RAST.Type.create_TypeApp(_28_genSelfPath, _1_rTypeParams), Dafny.Sequence<RAST._IImplMember>.FromElements(RAST.ImplMember.create_ImplMemberMacro((((RAST.__default.dafny__runtime).MSel((this).UpcastFnMacro)).AsExpr()).Apply1(RAST.Expr.create_ExprFromType((this).DynAny))))))));
496496
}
497497
Dafny.ISequence<DAST._IType> _29_superTraitTypes;
498498
if ((_16_className).Equals(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("_default"))) {
@@ -579,9 +579,6 @@ public void GetName(Dafny.ISequence<DAST._IAttribute> attributes, Dafny.ISequenc
579579
_15_upcastImplemented = Dafny.Sequence<RAST._IModDecl>.Concat(_15_upcastImplemented, Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(_1_rTypeParamsDecls, (((RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("UpcastBox"))).AsType()).Apply1(RAST.Type.create_DynType(_18_parentTpe)), RAST.__default.Box(RAST.Type.create_DynType(_10_traitFulltype)), Dafny.Sequence<RAST._IImplMember>.FromElements(RAST.ImplMember.create_FnDecl(RAST.__default.NoDoc, RAST.__default.NoAttr, RAST.Visibility.create_PRIV(), RAST.Fn.create(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("upcast"), Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(), Dafny.Sequence<RAST._IFormal>.FromElements(RAST.Formal.selfBorrowed), Std.Wrappers.Option<RAST._IType>.create_Some(RAST.__default.Box(RAST.Type.create_DynType(_18_parentTpe))), Std.Wrappers.Option<RAST._IExpr>.create_Some(((_11_traitFullExpr).FSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("_clone"))).Apply1(((RAST.__default.self).FSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("as_ref"))).Apply0())))))))));
580580
}
581581
}
582-
if (((this).syncType).is_Sync) {
583-
_14_parents = Dafny.Sequence<RAST._IType>.Concat(_14_parents, Dafny.Sequence<RAST._IType>.FromElements(RAST.__default.SyncType, RAST.__default.SendType));
584-
}
585582
s = Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_TraitDecl(RAST.Trait.create((t).dtor_docString, Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), _1_rTypeParamsDecls, _10_traitFulltype, _14_parents, _12_implBody)));
586583
if (((t).dtor_traitType).is_GeneralTrait) {
587584
s = Dafny.Sequence<RAST._IModDecl>.Concat(s, Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(_1_rTypeParamsDecls, (((RAST.__default.std).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("clone"))).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Clone"))).AsType(), RAST.__default.Box(RAST.Type.create_DynType(_10_traitFulltype)), Dafny.Sequence<RAST._IImplMember>.FromElements(RAST.ImplMember.create_FnDecl(RAST.__default.NoDoc, RAST.__default.NoAttr, RAST.Visibility.create_PRIV(), RAST.Fn.create(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("clone"), Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(), Dafny.Sequence<RAST._IFormal>.FromElements(RAST.Formal.selfBorrowed), Std.Wrappers.Option<RAST._IType>.create_Some(RAST.__default.SelfOwned), Std.Wrappers.Option<RAST._IExpr>.create_Some(((_11_traitFullExpr).FSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("_clone"))).Apply1(((RAST.__default.self).Sel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("as_ref"))).Apply0())))))))));
@@ -1641,24 +1638,29 @@ public RAST._IType GenType(DAST._IType c, bool genTypeContext)
16411638
RAST._IType _out15;
16421639
_out15 = (this).GenType(_35_result, Defs.GenTypeContext.@default());
16431640
_39_resultType = _out15;
1644-
s = Dafny.Helpers.Id<Func<RAST._IType, RAST._IType>>((this).rc)(RAST.Type.create_DynType(RAST.Type.create_FnType(_36_argTypes, _39_resultType)));
1641+
RAST._IType _40_fnType;
1642+
_40_fnType = RAST.Type.create_DynType(RAST.Type.create_FnType(_36_argTypes, _39_resultType));
1643+
if (((this).syncType).is_Sync) {
1644+
_40_fnType = RAST.Type.create_IntersectionType(_40_fnType, (this).SyncSendType);
1645+
}
1646+
s = Dafny.Helpers.Id<Func<RAST._IType, RAST._IType>>((this).rc)(_40_fnType);
16451647
}
16461648
goto after_match0;
16471649
}
16481650
}
16491651
{
16501652
if (_source0.is_TypeArg) {
16511653
Dafny.ISequence<Dafny.Rune> _h90 = _source0.dtor_TypeArg_a0;
1652-
Dafny.ISequence<Dafny.Rune> _40_name = _h90;
1653-
s = RAST.Type.create_TIdentifier(Defs.__default.escapeName(_40_name));
1654+
Dafny.ISequence<Dafny.Rune> _41_name = _h90;
1655+
s = RAST.Type.create_TIdentifier(Defs.__default.escapeName(_41_name));
16541656
goto after_match0;
16551657
}
16561658
}
16571659
{
16581660
if (_source0.is_Primitive) {
1659-
DAST._IPrimitive _41_p = _source0.dtor_Primitive_a0;
1661+
DAST._IPrimitive _42_p = _source0.dtor_Primitive_a0;
16601662
{
1661-
DAST._IPrimitive _source2 = _41_p;
1663+
DAST._IPrimitive _source2 = _42_p;
16621664
{
16631665
if (_source2.is_Int) {
16641666
s = ((RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyInt"))).AsType();
@@ -1698,8 +1700,8 @@ public RAST._IType GenType(DAST._IType c, bool genTypeContext)
16981700
}
16991701
}
17001702
{
1701-
Dafny.ISequence<Dafny.Rune> _42_v = _source0.dtor_Passthrough_a0;
1702-
s = RAST.__default.RawType(_42_v);
1703+
Dafny.ISequence<Dafny.Rune> _43_v = _source0.dtor_Passthrough_a0;
1704+
s = RAST.__default.RawType(_43_v);
17031705
}
17041706
after_match0: ;
17051707
return s;
@@ -7022,9 +7024,9 @@ public RAST._IType SyncSendType { get {
70227024
} }
70237025
public RAST._IType AnyTrait { get {
70247026
if (((this).syncType).is_NoSync) {
7025-
return RAST.__default.AnyTrait;
7027+
return ((RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Any"))).AsType();
70267028
} else {
7027-
return RAST.Type.create_IntersectionType(RAST.__default.AnyTrait, (this).SyncSendType);
7029+
return RAST.Type.create_IntersectionType(((RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Any"))).AsType(), (this).SyncSendType);
70287030
}
70297031
} }
70307032
public RAST._IExpr read__mutable__field__macro { get {
@@ -7033,5 +7035,8 @@ public RAST._IExpr read__mutable__field__macro { get {
70337035
public RAST._IExpr modify__mutable__field__macro { get {
70347036
return ((RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("modify_field!"))).AsExpr();
70357037
} }
7038+
public RAST._IType DynAny { get {
7039+
return ((RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DynAny"))).AsType();
7040+
} }
70367041
}
70377042
} // end of namespace DCOMP

‎Source/DafnyRuntime/DafnyRuntimeRust/Makefile

+1
Original file line numberDiff line numberDiff line change
@@ -19,4 +19,5 @@ update-system-module: build-system-module
1919

2020
test:
2121
cargo test
22+
cargo test --features sync
2223
(cd ../../DafnyRuntime.Tests/DafnyRuntimeRustTest; cargo test)

‎Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs

+26
Original file line numberDiff line numberDiff line change
@@ -79,9 +79,16 @@ impl<T: ?Sized> UnsafeCell<T> {
7979
// An atomic box is just a RefCell in Rust
8080
pub type SizeT = usize;
8181

82+
#[cfg(not(feature = "sync"))]
8283
pub trait DafnyType: Clone + DafnyPrint + 'static {}
84+
#[cfg(feature = "sync")]
85+
pub trait DafnyType: Clone + DafnyPrint + Send + Sync + 'static {}
8386

87+
#[cfg(not(feature = "sync"))]
8488
impl<T> DafnyType for T where T: Clone + DafnyPrint + 'static {}
89+
#[cfg(feature = "sync")]
90+
impl<T> DafnyType for T where T: Clone + DafnyPrint + Send + Sync + 'static {}
91+
8592
pub trait DafnyTypeEq: DafnyType + Hash + Eq {}
8693

8794
impl<T> DafnyTypeEq for T where T: DafnyType + Hash + Eq {}
@@ -2062,6 +2069,18 @@ impl<A: DafnyPrint> DafnyPrint for LazyFieldWrapper<A> {
20622069
}
20632070
}
20642071

2072+
#[cfg(feature = "sync")]
2073+
// Convert the DafnyPrint above into a macro so that we can create it for functions of any input arity
2074+
macro_rules! dafny_print_function {
2075+
($($n:tt)*) => {
2076+
impl <B, $($n),*> $crate::DafnyPrint for $crate::Rc<dyn ::std::ops::Fn($($n),*) -> B + Send + Sync> {
2077+
fn fmt_print(&self, f: &mut ::std::fmt::Formatter<'_>, _in_seq: bool) -> ::std::fmt::Result {
2078+
write!(f, "<function>")
2079+
}
2080+
}
2081+
}
2082+
}
2083+
#[cfg(not(feature = "sync"))]
20652084
// Convert the DafnyPrint above into a macro so that we can create it for functions of any input arity
20662085
macro_rules! dafny_print_function {
20672086
($($n:tt)*) => {
@@ -2072,6 +2091,7 @@ macro_rules! dafny_print_function {
20722091
}
20732092
}
20742093
}
2094+
20752095
// Now create a loop like impl_tuple_print_loop so that we can create functions up to size 32
20762096
macro_rules! dafny_print_function_loop {
20772097
($first:ident $($rest:ident)*) => {
@@ -3332,6 +3352,12 @@ macro_rules! update_field_mut_if_uninit {
33323352
// This Ptr has the same run-time space as *mut
33333353
pub struct Ptr<T: ?Sized>(pub Option<NonNull<UnsafeCell<T>>>);
33343354

3355+
#[cfg(feature = "sync")]
3356+
unsafe impl<T: ?Sized> Send for Ptr<T> {}
3357+
3358+
#[cfg(feature = "sync")]
3359+
unsafe impl<T: ?Sized> Sync for Ptr<T> {}
3360+
33353361
impl<T: ?Sized> Ptr<T> {
33363362
pub fn null() -> Self {
33373363
Ptr(None)

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

+44-26
Original file line numberDiff line numberDiff line change
@@ -47,18 +47,24 @@ mod tests {
4747
#[cfg(not(feature = "sync"))]
4848
assert!(boxed.as_ref().clone().borrow().as_ref().is_none());
4949
#[cfg(feature = "sync")]
50-
assert!(boxed.as_ref().clone().borrow().lock().unwrap().as_ref().is_none());
50+
assert!(boxed.as_ref().lock().unwrap().as_ref().is_none());
5151
}
5252
_ => panic!("This should never happen"),
5353
}
5454
let value = concat.get_usize(0);
5555
assert_eq!(value, 1);
5656
match &concat {
5757
crate::Sequence::ConcatSequence { boxed, .. } => {
58+
#[cfg(not(feature = "sync"))]
5859
assert_eq!(
5960
*boxed.as_ref().clone().borrow().as_ref().unwrap().as_ref(),
6061
vec![1, 2, 3, 4, 5, 6]
6162
);
63+
#[cfg(feature = "sync")]
64+
assert_eq!(
65+
*boxed.as_ref().lock().unwrap().as_ref().unwrap().as_ref(),
66+
vec![1, 2, 3, 4, 5, 6]
67+
);
6268
}
6369
_ => panic!("This should never happen"),
6470
}
@@ -443,11 +449,11 @@ mod tests {
443449
}
444450
}
445451

446-
impl <T: DafnyType> Upcast<dyn Any> for ClassWrapper<T> {
447-
UpcastFn!(dyn Any);
452+
impl <T: DafnyType> Upcast<crate::DynAny> for ClassWrapper<T> {
453+
UpcastFn!(crate::DynAny);
448454
}
449-
impl <T: DafnyType> UpcastObject<dyn Any> for ClassWrapper<T> {
450-
UpcastObjectFn!(dyn Any);
455+
impl <T: DafnyType> UpcastObject<crate::DynAny> for ClassWrapper<T> {
456+
UpcastObjectFn!(crate::DynAny);
451457
}
452458

453459
#[test]
@@ -549,19 +555,19 @@ mod tests {
549555
#[test]
550556
fn test_coercion_immutable() {
551557
let o = ClassWrapper::<i32>::constructor(1);
552-
let a: Ptr<dyn Any> = Upcast::<dyn Any>::upcast(read!(o));
558+
let a: Ptr<crate::DynAny> = Upcast::<crate::DynAny>::upcast(read!(o));
553559
assert_eq!(cast!(a, ClassWrapper<i32>), o);
554560
let seq_o = seq![o];
555-
let seq_a = Sequence::<Ptr<ClassWrapper<i32>>>::coerce(upcast::<ClassWrapper<i32>, dyn Any>())(seq_o);
561+
let seq_a = Sequence::<Ptr<ClassWrapper<i32>>>::coerce(upcast::<ClassWrapper<i32>, crate::DynAny>())(seq_o);
556562
assert_eq!(cast!(seq_a.get_usize(0), ClassWrapper<i32>), o);
557563
let set_o = set! {o};
558-
let set_a = Set::<Ptr<ClassWrapper<i32>>>::coerce(upcast::<ClassWrapper<i32>, dyn Any>())(set_o);
564+
let set_a = Set::<Ptr<ClassWrapper<i32>>>::coerce(upcast::<ClassWrapper<i32>, crate::DynAny>())(set_o);
559565
assert_eq!(cast!(set_a.peek(), ClassWrapper<i32>), o);
560566
let multiset_o = multiset! {o, o};
561-
let multiset_a = Multiset::<Ptr<ClassWrapper<i32>>>::coerce(upcast::<ClassWrapper<i32>, dyn Any>())(multiset_o);
567+
let multiset_a = Multiset::<Ptr<ClassWrapper<i32>>>::coerce(upcast::<ClassWrapper<i32>, crate::DynAny>())(multiset_o);
562568
assert_eq!(cast!(multiset_a.peek(), ClassWrapper<i32>), o);
563569
let map_o = map![1 => o, 2 => o];
564-
let map_a = Map::<i32, Ptr<ClassWrapper<i32>>>::coerce(upcast::<ClassWrapper<i32>, dyn Any>())(map_o);
570+
let map_a = Map::<i32, Ptr<ClassWrapper<i32>>>::coerce(upcast::<ClassWrapper<i32>, crate::DynAny>())(map_o);
565571
assert_eq!(cast!(map_a.get(&1), ClassWrapper<i32>), o);
566572
deallocate(o);
567573
}
@@ -594,7 +600,7 @@ mod tests {
594600

595601
#[test]
596602
fn test_function_wrappers() {
597-
let f: Rc<dyn Fn(i32) -> i32> = Rc::new(|i: i32| i + 1);
603+
let f: Rc<dyn Fn(i32) -> i32 + Send + Sync> = Rc::new(|i: i32| i + 1);
598604
let g = f.clone();
599605
let _h = seq![g];
600606
}
@@ -688,10 +694,22 @@ mod tests {
688694
let count_inner = count.clone();
689695
multiset!{1, 1, 5, 7, 8}
690696
.iter().for_each(move |_i: u32| {
691-
let c: i32 = *count_inner.as_ref().borrow();
692-
*count_inner.borrow_mut() = c + 1;
697+
#[cfg(not(feature = "sync"))]
698+
{
699+
let c: i32 = *count_inner.as_ref().borrow();
700+
*count_inner.borrow_mut() = c + 1;
701+
}
702+
#[cfg(feature = "sync")]
703+
{
704+
let mut guard = count_inner.as_ref().lock().unwrap();
705+
let c: i32 = *guard;
706+
*guard = c + 1;
707+
}
693708
});
709+
#[cfg(not(feature = "sync"))]
694710
assert_eq!(*count.as_ref().borrow(), 5);
711+
#[cfg(feature = "sync")]
712+
assert_eq!(*count.as_ref().lock().unwrap(), 5);
695713

696714
let m = map![1 => 4, 3 => 6, 5 => 8];
697715
let m2 = m.clone();
@@ -748,7 +766,7 @@ mod tests {
748766
assert_eq!(sum, 55);
749767
}
750768

751-
trait SuperTrait: Upcast<dyn Any> + UpcastObject<dyn Any> {
769+
trait SuperTrait: Upcast<crate::DynAny> + UpcastObject<crate::DynAny> {
752770
}
753771

754772
trait NodeRcMutTrait: SuperTrait + Upcast<dyn SuperTrait> + UpcastObject<dyn SuperTrait>{
@@ -767,11 +785,11 @@ mod tests {
767785
}
768786
}
769787
impl SuperTrait for NodeRcMut {}
770-
impl UpcastObject<dyn Any> for NodeRcMut {
771-
UpcastObjectFn!(dyn Any);
788+
impl UpcastObject<crate::DynAny> for NodeRcMut {
789+
UpcastObjectFn!(crate::DynAny);
772790
}
773-
impl Upcast<dyn Any> for NodeRcMut {
774-
UpcastFn!(dyn Any);
791+
impl Upcast<crate::DynAny> for NodeRcMut {
792+
UpcastFn!(crate::DynAny);
775793
}
776794
impl UpcastObject<dyn NodeRcMutTrait> for NodeRcMut {
777795
UpcastObjectFn!(dyn NodeRcMutTrait);
@@ -798,7 +816,7 @@ mod tests {
798816
assert_eq!(x.as_ref().next.as_ref().val, int!(42));
799817
md!(rd!(x).next).next = Object(None);
800818
assert_eq!(refcount!(x), 1);
801-
let y: Object<dyn Any> = upcast_object::<_, _>()(x.clone());
819+
let y: Object<crate::DynAny> = upcast_object::<_, _>()(x.clone());
802820
assert_eq!(refcount!(x), 2);
803821
let z: Object<dyn NodeRcMutTrait> = upcast_object::<_, _>()(x.clone());
804822
assert_eq!(refcount!(x), 3);
@@ -834,7 +852,7 @@ mod tests {
834852
}
835853
assert_eq!(refcount!(x), previous_count);
836854

837-
let objects: Set<Object<dyn ::std::any::Any>> = crate::set!{y.clone(), cast_any_object!(x.clone())};
855+
let objects: Set<Object<crate::DynAny>> = crate::set!{y.clone(), cast_any_object!(x.clone())};
838856
assert_eq!(objects.cardinality_usize(), 1);
839857
test_dafny_type(a.clone());
840858
}
@@ -850,8 +868,8 @@ mod tests {
850868
}
851869
}
852870
impl NodeRcMutTrait for NodeRawMut {}
853-
UpcastDefObject!(NodeRawMut, dyn NodeRcMutTrait, dyn SuperTrait, dyn Any);
854-
UpcastDef!(NodeRawMut, dyn NodeRcMutTrait, dyn SuperTrait, dyn Any);
871+
UpcastDefObject!(NodeRawMut, dyn NodeRcMutTrait, dyn SuperTrait, crate::DynAny);
872+
UpcastDef!(NodeRawMut, dyn NodeRcMutTrait, dyn SuperTrait, crate::DynAny);
855873

856874
impl SuperTrait for NodeRawMut {}
857875

@@ -863,7 +881,7 @@ mod tests {
863881
modify!(x.clone()).next = x.clone();
864882
assert_eq!(read!(read!(x.clone()).next.clone()).val, int!(42));
865883
modify!(read!(x.clone()).next.clone()).next = Ptr::null();
866-
let y: Ptr<dyn Any> = upcast::<_, _>()(x);
884+
let y: Ptr<crate::DynAny> = upcast::<_, _>()(x);
867885
assert!(y.is_instance_of::<NodeRawMut>());
868886
assert!(!y.is_instance_of::<NodeRcMut>());
869887
let z: Ptr<dyn NodeRcMutTrait> = upcast::<_, _>()(x);
@@ -907,13 +925,13 @@ mod tests {
907925
pub message: String,
908926
}
909927

910-
crate::UpcastDefObject!(InternalOpaqueError, dyn Any);
928+
crate::UpcastDefObject!(InternalOpaqueError, crate::DynAny);
911929

912930
#[test]
913931
fn test_native_string_upcast() {
914932
let s = InternalOpaqueError { message: "Hello, World!".to_string() };
915933
let o: Object<InternalOpaqueError> = Object::new(s);
916-
let n: Object<dyn ::std::any::Any> = upcast_object::<InternalOpaqueError, dyn ::std::any::Any>()(o);
934+
let n: Object<crate::DynAny> = upcast_object::<InternalOpaqueError, crate::DynAny>()(o);
917935
let x = cast_object!(n, InternalOpaqueError);
918936
let s2 = crate::dafny_runtime_conversions::object::dafny_class_to_struct(x);
919937
assert_eq!(s2.message, "Hello, World!");
@@ -923,7 +941,7 @@ mod tests {
923941
fn test_native_string_upcast_raw() {
924942
let message = "Hello, World!".to_string();
925943
let object = Object::new(message.clone());
926-
let object_any: Object<dyn Any> = UpcastObject::<dyn Any>::upcast(object.as_ref());
944+
let object_any: Object<crate::DynAny> = UpcastObject::<crate::DynAny>::upcast(object.as_ref());
927945
let resulting_message = format!("{:?}", object_any);
928946
assert_eq!(resulting_message, message);
929947
}

0 commit comments

Comments
 (0)