[new] Vect.Quantifiers.All QoL (#2843)

* Add Show for Vect.All

* Add an alias for HVect to Data.Vect.Quantifiers.All

* Add a few utilities for Vect.Quantifiers.All to make it more at home in listy uses.

* Add CHANGELOG entries.

CHANGELOG.md

@@ -64,6 +64,11 @@
   convert a `Bits8` to an `Int`), as their values are limited, as opposed to the
   assumption in `setByte` that the value is between 0 and 255.
 * Adds RefC support for 16- and 32-bit access in `Data.Buffer`.
+* Add `Show` instance to `Data.Vect.Quantifiers.All` and add a few helpers for listy
+  computations on the `All` type.
+* Add an alias for `HVect` to `All id` in `Data.Vect.Quantifiers.All`. This is the
+  approach to getting a heterogeneous Vect of elements that is generall preferred by
+  the community vs. a standalone type as seen in `contrib`.
 
 #### System
 

libs/base/Data/Vect/Quantifiers.idr

@@ -125,3 +125,43 @@ namespace All
   forget : All (const p) {n} xs -> Vect n p
   forget []      = []
   forget (x::xs) = x :: forget xs
+
+  export
+  {0 xs : Vect n _} -> All Show (map p xs) => Show (All p xs) where
+    show pxs = "[" ++ show' "" pxs ++ "]"
+      where
+        show' : {0 xs' : Vect n' _} -> String -> All Show (map p xs') => All p xs' -> String
+        show' acc @{[]} [] = acc
+        show' acc @{[_]} [px] = acc ++ show px
+        show' acc @{_ :: _} (px :: pxs) = show' (acc ++ show px ++ ", ") pxs
+
+  ||| A heterogeneous vector of arbitrary types
+  public export
+  HVect : Vect n Type -> Type
+  HVect = All id
+
+  ||| Take the first element.
+  export
+  head : All p (x :: xs) -> p x
+  head (y :: _) = y
+
+  ||| Take all but the first element.
+  export
+  tail : All p (x :: xs) -> All p xs
+  tail (_ :: ys) = ys
+
+  ||| Drop the first n elements given knowledge that
+  ||| there are at least n elements available.
+  export
+  drop : {0 m : _} -> (n : Nat) -> {0 xs : Vect (n + m) a} -> All p xs -> All p (the (Vect m a) (Vect.drop n xs))
+  drop 0 ys = ys
+  drop (S k) (y :: ys) = drop k ys
+
+  ||| Drop up to the first l elements, stopping early
+  ||| if all elements have been dropped.
+  export
+  drop' : {0 k : _} -> {0 xs : Vect k _} -> (l : Nat) -> All p xs -> All p (Vect.drop' l xs)
+  drop' 0 ys = rewrite minusZeroRight k in ys
+  drop' (S k) [] = []
+  drop' (S k) (y :: ys) = drop' k ys
+