0 | module Data.List1
  1 |
  2 | import public Data.Zippable
  3 | import public Control.Function
  4 |
  5 | %default total
  6 |
  7 | export infixr 7 :::
  8 |
  9 | ||| Non-empty lists.
 10 | public export
 11 | record List1 a where
 12 |   constructor (:::)
 13 |   head : a
 14 |   tail : List a
 15 |
 16 | %name List1 xs, ys, zs
 17 |
 18 | ------------------------------------------------------------------------
 19 | -- Basic functions
 20 |
 21 | public export
 22 | fromList : List a -> Maybe (List1 a)
 23 | fromList [] = Nothing
 24 | fromList (x :: xs) = Just (x ::: xs)
 25 |
 26 | public export
 27 | singleton : (x : a) -> List1 a
 28 | singleton a = a ::: []
 29 |
 30 | ||| Forget that a list is non-empty.
 31 | public export
 32 | forget : List1 a -> List a
 33 | forget (x ::: xs) = x :: xs
 34 |
 35 | export
 36 | last : List1 a -> a
 37 | last (x ::: xs) = loop x xs where
 38 |   loop : a -> List a -> a
 39 |   loop x [] = x
 40 |   loop _ (x :: xs) = loop x xs
 41 |
 42 | export
 43 | init : List1 a -> List a
 44 | init (x ::: xs) = loop x xs where
 45 |   loop : a -> List a -> List a
 46 |   loop x [] = []
 47 |   loop x (y :: xs) = x :: loop y xs
 48 |
 49 | public export
 50 | foldr1By : (func : a -> b -> b) -> (map : a -> b) -> (l : List1 a) -> b
 51 | foldr1By f map (x ::: xs) = loop x xs where
 52 |   loop : a -> List a -> b
 53 |   loop x [] = map x
 54 |   loop x (y :: xs) = f x (loop y xs)
 55 |
 56 | public export
 57 | foldl1By : (func : b -> a -> b) -> (map : a -> b) -> (l : List1 a) -> b
 58 | foldl1By f map (x ::: xs) = foldl f (map x) xs
 59 |
 60 | public export
 61 | foldr1 : (func : a -> a -> a) -> (l : List1 a) -> a
 62 | foldr1 f = foldr1By f id
 63 |
 64 | public export
 65 | foldl1 : (func : a -> a -> a) -> (l : List1 a) -> a
 66 | foldl1 f = foldl1By f id
 67 |
 68 | public export
 69 | length : List1 a -> Nat
 70 | length (_ ::: xs) = S (length xs)
 71 |
 72 | ------------------------------------------------------------------------
 73 | -- Append
 74 |
 75 | public export
 76 | appendl : (xs : List1 a) -> (ys : List a) -> List1 a
 77 | appendl (x ::: xs) ys = x ::: xs ++ ys
 78 |
 79 | public export
 80 | (++) : (xs, ys : List1 a) -> List1 a
 81 | (++) xs ys = appendl xs (forget ys)
 82 |
 83 | public export
 84 | lappend : (xs : List a) -> (ys : List1 a) -> List1 a
 85 | lappend [] ys = ys
 86 | lappend (x :: xs) ys = (x ::: xs) ++ ys
 87 |
 88 | ------------------------------------------------------------------------
 89 | -- Cons/Snoc
 90 |
 91 | public export
 92 | cons : (x : a) -> (xs : List1 a) -> List1 a
 93 | cons x xs = x ::: forget xs
 94 |
 95 | public export
 96 | snoc : (xs : List1 a) -> (x : a) -> List1 a
 97 | snoc xs x = xs ++ (singleton x)
 98 |
 99 | public export
100 | unsnoc : (xs : List1 a) -> (List a, a)
101 | unsnoc (x ::: xs) = go x xs where
102 |
103 |   go : (x : a) -> (xs : List a) -> (List a, a)
104 |   go x [] = ([], x)
105 |   go x (y :: ys) = let (ini,lst) = go y ys
106 |                    in (x :: ini, lst)
107 |
108 | ------------------------------------------------------------------------
109 | -- Reverse
110 |
111 | public export
112 | reverseOnto : (acc : List1 a) -> (xs : List a) -> List1 a
113 | reverseOnto acc [] = acc
114 | reverseOnto acc (x :: xs) = reverseOnto (x ::: forget acc) xs
115 |
116 | public export
117 | reverse : (xs : List1 a) -> List1 a
118 | reverse (x ::: xs) = reverseOnto (singleton x) xs
119 |
120 | ------------------------------------------------------------------------
121 | -- Instances
122 |
123 | public export
124 | Semigroup (List1 a) where
125 |   (<+>) = (++)
126 |
127 | public export
128 | Functor List1 where
129 |   map f (x ::: xs) = f x ::: map f xs
130 |
131 | public export
132 | Applicative List1 where
133 |   pure x = singleton x
134 |   f ::: fs <*> xs = appendl (map f xs) (fs <*> forget xs)
135 |
136 | public export
137 | Monad List1 where
138 |   (x ::: xs) >>= f = appendl (f x) (xs >>= forget . f)
139 |
140 | public export
141 | Foldable List1 where
142 |   foldr c n (x ::: xs) = c x (foldr c n xs)
143 |   foldl f z (x ::: xs) = foldl f (f z x) xs
144 |   null _ = False
145 |   toList = forget
146 |   foldMap f (x ::: xs) = f x <+> foldMap f xs
147 |
148 | public export
149 | Traversable List1 where
150 |   traverse f (x ::: xs) = [| f x ::: traverse f xs |]
151 |
152 | export
153 | Show a => Show (List1 a) where
154 |   show = show . forget
155 |
156 | public export
157 | Eq a => Eq (List1 a) where
158 |   (x ::: xs) == (y ::: ys) = x == y && xs == ys
159 |
160 | public export
161 | Ord a => Ord (List1 a) where
162 |   compare xs ys = compare (forget xs) (forget ys)
163 |
164 | ------------------------------------------------------------------------
165 | -- Zippable
166 |
167 | public export
168 | Zippable List1 where
169 |   zipWith f (x ::: xs) (y ::: ys) = f x y ::: zipWith' xs ys
170 |   where
171 |       zipWith' : List a -> List b -> List c
172 |       zipWith' [] _ = []
173 |       zipWith' _ [] = []
174 |       zipWith' (x :: xs) (y :: ys) = f x y :: zipWith' xs ys
175 |
176 |   zipWith3 f (x ::: xs) (y ::: ys) (z ::: zs) = f x y z ::: zipWith3' xs ys zs
177 |     where
178 |       zipWith3' : List a -> List b -> List c -> List d
179 |       zipWith3' [] _ _ = []
180 |       zipWith3' _ [] _ = []
181 |       zipWith3' _ _ [] = []
182 |       zipWith3' (x :: xs) (y :: ys) (z :: zs) = f x y z :: zipWith3' xs ys zs
183 |
184 |   unzipWith f (x ::: xs) = let (b, c) = f x
185 |                                (bs, cs) = unzipWith' xs in
186 |                                (b ::: bs, c ::: cs)
187 |     where
188 |       unzipWith' : List a -> (List b, List c)
189 |       unzipWith' [] = ([], [])
190 |       unzipWith' (x :: xs) = let (b, c) = f x
191 |                                  (bs, cs) = unzipWith' xs in
192 |                                  (b :: bs, c :: cs)
193 |
194 |   unzipWith3 f (x ::: xs) = let (b, c, d) = f x
195 |                                 (bs, cs, ds) = unzipWith3' xs in
196 |                                 (b ::: bs, c ::: cs, d ::: ds)
197 |     where
198 |       unzipWith3' : List a -> (List b, List c, List d)
199 |       unzipWith3' [] = ([], [], [])
200 |       unzipWith3' (x :: xs) = let (b, c, d) = f x
201 |                                   (bs, cs, ds) = unzipWith3' xs in
202 |                                   (b :: bs, c :: cs, d :: ds)
203 |
204 | ------------------------------------------------------------------------
205 | -- Uninhabited
206 |
207 | export
208 | Uninhabited a => Uninhabited (List1 a) where
209 |   uninhabited (hd ::: _) = uninhabited hd
210 |
211 | ------------------------------------------------------------------------
212 | -- Filtering
213 |
214 | public export %inline
215 | filter : (a -> Bool) -> List1 a -> Maybe $ List1 a
216 | filter f = fromList . filter f . forget
217 |