Return a Vect from Stream take (#1812)

Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>

libs/base/Data/Vect.idr

@@ -87,6 +87,15 @@ take : (n  : Nat)
 take 0 xs = Nil
 take (S k) (x :: xs) = x :: take k xs
 
+namespace Stream
+  ||| Take precisely n elements from the stream.
+  ||| @ n how many elements to take
+  ||| @ xs the stream
+  public export
+  take : (n : Nat) -> (xs : Stream a) -> Vect n a
+  take Z xs = []
+  take (S k) (x :: xs) = x :: take k xs
+
 ||| Drop the first `n` elements of a Vect.
 public export
 drop : (n : Nat) -> Vect (n + m) elem -> Vect m elem

tests/base/data_vect001/Vect.idr

@@ -0,0 +1,7 @@
+import Data.Vect
+
+takeFromStream : List (n ** Vect n Int)
+takeFromStream = [(n ** take n [3..]) | n <- [0, 1, 5]]
+
+main : IO ()
+main = do printLn takeFromStream

tests/base/data_vect001/expected

@@ -0,0 +1,3 @@
+1/1: Building Vect (Vect.idr)
+Main> [(0 ** []), (1 ** [3]), (5 ** [3, 4, 5, 6, 7])]
+Main> Bye for now!

tests/base/data_vect001/input

@@ -0,0 +1,2 @@
+:exec main
+:q

tests/base/data_vect001/run

@@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --no-banner --no-color --console-width 0 Vect.idr < input