vstd/std_specs/
borrow.rs

Help
1#![allow(unused_imports)]
2use super::super::prelude::*;
3
4#[cfg(feature = "alloc")]
5use alloc::borrow::Borrow;
6#[cfg(feature = "alloc")]
7use alloc::borrow::Cow;
8#[cfg(feature = "alloc")]
9use alloc::borrow::ToOwned;
10
11verus! {
12
13#[cfg(feature = "alloc")]
14#[verifier::external_trait_specification]
15pub(crate) trait ExToOwned {
16    type ExternalTraitSpecificationFor: ToOwned;
17
18    type Owned: Borrow<Self>;
19}
20
21#[cfg(feature = "alloc")]
22#[verifier::external_type_specification]
23#[verifier::reject_recursive_types(B)]
24pub struct ExCow<'a, B: 'a + ?Sized + ToOwned>(Cow<'a, B>);
25
26// We are using `T: Clone` as a more restrictive bound than what's in std (where
27// T: ToOwned), since ToOwned::Owned may be a different type than `T`.
28#[cfg(feature = "alloc")]
29impl<'a, T: View + Clone> View for Cow<'a, T> {
30    type V = T::V;
31
32    open spec fn view(&self) -> Self::V {
33        match self {
34            Cow::Borrowed(borrowed) => borrowed@,
35            Cow::Owned(owned) => owned@,
36        }
37    }
38}
39
40// We are using `T: Clone` as a more restrictive bound than what's in std (where
41// T: ToOwned), since ToOwned::Owned may be a different type than `T`.
42#[cfg(feature = "alloc")]
43impl<'a, T: DeepView + Clone> DeepView for Cow<'a, T> {
44    type V = T::V;
45
46    open spec fn deep_view(&self) -> Self::V {
47        match self {
48            Cow::Borrowed(borrowed) => borrowed.deep_view(),
49            Cow::Owned(owned) => owned.deep_view(),
50        }
51    }
52}
53
54// Note: this is not covered by the blanket impl for `T: View + Clone`, since `str` does not implement clone.
55#[cfg(feature = "alloc")]
56impl<'a> View for Cow<'a, str> {
57    type V = Seq<char>;
58
59    open spec fn view(&self) -> Self::V {
60        match self {
61            Cow::Borrowed(borrowed) => borrowed@,
62            Cow::Owned(owned) => owned@,
63        }
64    }
65}
66
67#[cfg(feature = "alloc")]
68impl<'a> DeepView for Cow<'a, str> {
69    type V = Seq<char>;
70
71    open spec fn deep_view(&self) -> Self::V {
72        match self {
73            Cow::Borrowed(borrowed) => borrowed.deep_view(),
74            Cow::Owned(owned) => owned.deep_view(),
75        }
76    }
77}
78
79#[cfg(feature = "alloc")]
80impl<'a, T: View + Clone> View for Cow<'a, [T]> {
81    type V = Seq<T>;
82
83    open spec fn view(&self) -> Self::V {
84        match self {
85            Cow::Borrowed(borrowed) => borrowed@,
86            Cow::Owned(owned) => owned@,
87        }
88    }
89}
90
91#[cfg(feature = "alloc")]
92impl<'a, T: DeepView + Clone> DeepView for Cow<'a, [T]> {
93    type V = Seq<T::V>;
94
95    open spec fn deep_view(&self) -> Self::V {
96        match self {
97            Cow::Borrowed(borrowed) => borrowed.deep_view(),
98            Cow::Owned(owned) => owned.deep_view(),
99        }
100    }
101}
102
103} // verus!
vstd/std_specs/borrow.rs

vstd/std_specs/
borrow.rs
