0 | module OStream -- If just "Stream", irreconsilable conflict with names from Prelude.Stream
 1 |
 2 | %default total
 3 |
 4 | mutual
 5 |   public export
 6 |   data StreamCell a = Nil | (::) a (OStream a)
 7 |
 8 |   public export
 9 |   infixr 7 ::
10 |
11 |   {-
12 |   I haven't figured out how define Stream at the top-level and not conflict with the version from
13 |   Prelude.
14 |   -}
15 |   public export
16 |   OStream : Type -> Type
17 |   OStream a = Lazy (StreamCell a)
18 |
19 | mutual
20 |   append' : OStream a -> OStream a -> OStream a
21 |   append' []       t = t
22 |   append' (x :: s) t = x :: append s t
23 |
24 |   export
25 |   append : OStream a -> OStream a -> OStream a
26 |   append s t = Delay (Force (append' s t))
27 |
28 |   export
29 |   (++) : OStream a -> OStream a -> OStream a
30 |   (++) = append
31 |
32 | mutual
33 |   take' : Int -> OStream a -> OStream a
34 |   take' 0 s        = []
35 |   take' n []       = []
36 |   take' n (x :: s) = x :: take (n - 1) s
37 |
38 |   export
39 |   take : Int -> OStream a -> OStream a
40 |   take n s = Delay (Force (take' n s))
41 |
42 | drop' : Int -> OStream a -> OStream a
43 | drop' 0 s        = s
44 | drop' n []       = []
45 | drop' n (x :: s) = drop' (n - 1) s
46 |
47 | export
48 | drop : Int -> OStream a -> OStream a
49 | drop n s = Delay (Force (drop' n s))
50 |
51 | reverse' : OStream a -> OStream a -> OStream a
52 | reverse' []       r = r
53 | reverse' (x :: s) r = reverse' s (x :: r)
54 |
55 | export
56 | reverse : OStream a -> OStream a
57 | reverse s = Delay (Force (reverse' s []))
58 |