0 | module Data.Linear.List
 1 |
 2 | import public Data.Linear.Token
 3 |
 4 | %default total
 5 |
 6 | ||| Filters a list using a predicate based on mutable
 7 | ||| linear state.
 8 | export
 9 | filter1 : (a -> F1 s Bool) -> List a -> F1 s (List a)
10 | filter1 f = go [<]
11 |   where
12 |     go : SnocList a -> List a -> F1 s (List a)
13 |     go sx []        t = (sx <>> []) # t
14 |     go sx (x :: xs) t =
15 |       let b # t := f x t
16 |        in if b then go (sx :< x) xs t else go sx xs t
17 |
18 | ||| Returns the first value in a list, for which the given
19 | ||| linear predicate returns `True`.
20 | export
21 | find1 : (a -> F1 s Bool) -> List a -> F1 s (Maybe a)
22 | find1 f = go
23 |   where
24 |     go : List a -> F1 s (Maybe a)
25 |     go []        t = Nothing # t
26 |     go (x :: xs) t =
27 |       let b # t := f x t
28 |        in if b then Just x # t else go xs t
29 |
30 | ||| Returns the longest (possibly empty) prefix of the given list
31 | ||| for which the given predicate returns `True`.
32 | |||
33 | ||| The second value of the pair returns the remainder of
34 | ||| the list.
35 | export
36 | span1 : (a -> F1 s Bool) -> List a -> F1 s (List a, List a)
37 | span1 p = go [<]
38 |   where
39 |     go : SnocList a -> List a -> F1 s (List a, List a)
40 |     go sx []        t = (sx<>>[], []) # t
41 |     go sx (x :: xs) t =
42 |       let b # t := p x t
43 |        in if b then go (sx:<x) xs t else (sx<>>[],x::xs) # t
44 |
45 | ||| Like `span1` but returns the longest prefix, for which the
46 | ||| predicate does *not* hold.
47 | export %inline
48 | break1 : (a -> F1 s Bool) -> List a -> F1 s (List a, List a)
49 | break1 p = span1 $ \v,t => let b # t := p v t in not b # t
50 |
51 | ||| Partitions the values in a list according to the given
52 | ||| linear predicate.
53 | |||
54 | ||| Returns a pair of lists, the first of which holds the values
55 | ||| for which the predicate returned `False`. All other values
56 | ||| are returned in the second list.
57 | export
58 | partition1 : (a -> F1 s Bool) -> List a -> F1 s (List a, List a)
59 | partition1 f = go [<] [<]
60 |   where
61 |     go : SnocList a -> SnocList a -> List a -> F1 s (List a, List a)
62 |     go sx sy []        t = (sx <>> [], sy <>> []) # t
63 |     go sx sy (x :: xs) t =
64 |       let b # t := f x t
65 |        in if b then go sx (sy:<x) xs t else go (sx:<x) sy xs t
66 |
67 | ||| Using a `Maybe` function to map and filter a list in one go.
68 | export
69 | mapMaybe1 : (a -> F1 s (Maybe b)) -> List a -> F1 s (List b)
70 | mapMaybe1 f = go [<]
71 |   where
72 |     go : SnocList b -> List a -> F1 s (List b)
73 |     go sx []        t = (sx <>> []) # t
74 |     go sx (x :: xs) t =
75 |       let Just v # t := f x t | Nothing # t => go sx xs t
76 |        in go (sx :< v) xs t
77 |
78 | ||| Fills a list with values from a stateful linear computation.
79 | export
80 | replicate1 : Nat -> F1 s a -> F1 s (List a)
81 | replicate1 n f = go [<] n
82 |   where
83 |     go : SnocList a -> Nat -> F1 s (List a)
84 |     go sx 0     t = (sx <>> []) # t
85 |     go sx (S k) t = let v # t2 := f t in go (sx :< v) k t2
86 |