Deep view unsupported for &[u8]

[gancherj]

This works:

spec fn test(xs : &[u8]) -> Seq<u8> { 
    xs.view()
}

but this doesn't:

spec fn test(xs : &[u8]) -> Seq<u8> { 
    xs.deep_view()
}

as it returns the error

  ^^^^^^^^^ method cannot be called on `&'a [u8]` due to unsatisfied trait bounds
  
   = note: the following trait bounds were not satisfied:
           `[u8]: std::marker::Sized`
           which is required by `&[u8]: vstd::view::DeepView`
           `[u8]: vstd::view::DeepView`
           which is required by `&[u8]: vstd::view::DeepView`

Is this simply a matter of adding the function to SliceAdditionalSpecFns?

[jaybosamiya]

Adding this to source/vstd/view.rs works:

modified   source/vstd/view.rs
@@ -1,4 +1,6 @@
 #[allow(unused_imports)]
+use crate::prelude::*;
+#[allow(unused_imports)]
 use builtin::*;
 #[allow(unused_imports)]
 use builtin_macros::*;
@@ -40,6 +42,16 @@ impl<A: DeepView> DeepView for &A {
     }
 }
 
+impl<T: DeepView> DeepView for [T] {
+    type V = Seq<T::V>;
+
+    #[verifier::inline]
+    open spec fn deep_view(&self) -> Self::V {
+        let v = self.view();
+        Seq::new(v.len(), |i: int| v[i].deep_view())
+    }
+}
+
 #[cfg(feature = "alloc")]
 impl<A: View> View for alloc::boxed::Box<A> {
     type V = A::V;

To make a PR, this probably needs some tests, but otherwise yeah, this code is sufficient to get deep_view on slices

[Chris-Hawblitzel]

@jaybosamiya Thanks! I turned this into pull request #1078 .

[Chris-Hawblitzel]

Implemented by #1078