Skip to content

Commit 078db21

Browse files
Return a Vect from Stream take (#1812)
Co-authored-by: Guillaume ALLAIS <[email protected]>
1 parent cdc157a commit 078db21

File tree

5 files changed

+24
-0
lines changed

5 files changed

+24
-0
lines changed

libs/base/Data/Vect.idr

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -87,6 +87,15 @@ take : (n : Nat)
8787
take 0 xs = Nil
8888
take (S k) (x :: xs) = x :: take k xs
8989

90+
namespace Stream
91+
||| Take precisely n elements from the stream.
92+
||| @ n how many elements to take
93+
||| @ xs the stream
94+
public export
95+
take : (n : Nat) -> (xs : Stream a) -> Vect n a
96+
take Z xs = []
97+
take (S k) (x :: xs) = x :: take k xs
98+
9099
||| Drop the first `n` elements of a Vect.
91100
public export
92101
drop : (n : Nat) -> Vect (n + m) elem -> Vect m elem

tests/base/data_vect001/Vect.idr

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
import Data.Vect
2+
3+
takeFromStream : List (n ** Vect n Int)
4+
takeFromStream = [(n ** take n [3..]) | n <- [0, 1, 5]]
5+
6+
main : IO ()
7+
main = do printLn takeFromStream

tests/base/data_vect001/expected

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
1/1: Building Vect (Vect.idr)
2+
Main> [(0 ** []), (1 ** [3]), (5 ** [3, 4, 5, 6, 7])]
3+
Main> Bye for now!

tests/base/data_vect001/input

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
:exec main
2+
:q

tests/base/data_vect001/run

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
rm -rf build
2+
3+
$1 --no-banner --no-color --console-width 0 Vect.idr < input

0 commit comments

Comments
 (0)