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 []      t = Nothing # t
 23 | find1 f (x::xs) t =
 24 |  let b # t := f x t
 25 |   in if b then Just x # t else find1 f xs t
 26 |
 27 | ||| Returns `True` if the given list holds at least one value,
 28 | ||| for which the given linear predicate returns `True`
 29 | |||
 30 | ||| Trivially, this returns `False` for the empty list.
 31 | export
 32 | any1 : (a -> F1 s Bool) -> List a -> F1 s Bool
 33 | any1 f [] t = False # t
 34 | any1 f (x::xs) t =
 35 |  let b # t := f x t
 36 |   in if b then True # t else any1 f xs t
 37 |
 38 | ||| Returns `True` if the given list holds only values,
 39 | ||| for which the given linear predicate returns `True`
 40 | |||
 41 | ||| Trivially, this returns `True` for the empty list.
 42 | export
 43 | all1 : (a -> F1 s Bool) -> List a -> F1 s Bool
 44 | all1 f [] t = True # t
 45 | all1 f (x::xs) t =
 46 |  let b # t := f x t
 47 |   in if b then all1 f xs t else False # t
 48 |
 49 | ||| Returns the longest (possibly empty) prefix of the given list
 50 | ||| for which the given predicate returns `True`.
 51 | |||
 52 | ||| The second value of the pair returns the remainder of
 53 | ||| the list.
 54 | export
 55 | span1 : (a -> F1 s Bool) -> List a -> F1 s (List a, List a)
 56 | span1 p = go [<]
 57 |   where
 58 |     go : SnocList a -> List a -> F1 s (List a, List a)
 59 |     go sx []        t = (sx<>>[], []) # t
 60 |     go sx (x :: xs) t =
 61 |       let b # t := p x t
 62 |        in if b then go (sx:<x) xs t else (sx<>>[],x::xs) # t
 63 |
 64 | ||| Like `span1` but returns the longest prefix, for which the
 65 | ||| predicate does *not* hold.
 66 | export %inline
 67 | break1 : (a -> F1 s Bool) -> List a -> F1 s (List a, List a)
 68 | break1 p = span1 $ \v,t => let b # t := p v t in not b # t
 69 |
 70 | ||| Partitions the values in a list according to the given
 71 | ||| linear predicate.
 72 | |||
 73 | ||| Returns a pair of lists, the first of which holds the values
 74 | ||| for which the predicate returned `False`. All other values
 75 | ||| are returned in the second list.
 76 | export
 77 | partition1 : (a -> F1 s Bool) -> List a -> F1 s (List a, List a)
 78 | partition1 f = go [<] [<]
 79 |   where
 80 |     go : SnocList a -> SnocList a -> List a -> F1 s (List a, List a)
 81 |     go sx sy []        t = (sx <>> [], sy <>> []) # t
 82 |     go sx sy (x :: xs) t =
 83 |       let b # t := f x t
 84 |        in if b then go sx (sy:<x) xs t else go (sx:<x) sy xs t
 85 |
 86 | ||| Using a `Maybe` function to map and filter a list in one go.
 87 | export
 88 | mapMaybe1 : (a -> F1 s (Maybe b)) -> List a -> F1 s (List b)
 89 | mapMaybe1 f = go [<]
 90 |   where
 91 |     go : SnocList b -> List a -> F1 s (List b)
 92 |     go sx []        t = (sx <>> []) # t
 93 |     go sx (x :: xs) t =
 94 |       let Just v # t := f x t | Nothing # t => go sx xs t
 95 |        in go (sx :< v) xs t
 96 |
 97 | ||| Fills a list with values from a stateful linear computation.
 98 | export
 99 | replicate1 : Nat -> F1 s a -> F1 s (List a)
100 | replicate1 n f = go [<] n
101 |   where
102 |     go : SnocList a -> Nat -> F1 s (List a)
103 |     go sx 0     t = (sx <>> []) # t
104 |     go sx (S k) t = let v # t2 := f t in go (sx :< v) k t2
105 |