0 | module Data.List.Alternating
  1 |
  2 | import Data.Bifoldable
  3 | import Data.List
  4 |
  5 | export infixl 5 +>
  6 | export infixr 5 <+
  7 |
  8 | %default total
  9 |
 10 | mutual
 11 |     namespace Odd
 12 |         ||| Non-empty list, starting and ending with an a, where adjacent elements alternate
 13 |         ||| between types a and b.
 14 |         ||| We can think of this type as:
 15 |         ||| - A fence, with the `a`s as fence-posts, and the `b`s as panels.
 16 |         ||| - A non-empty list of `a`s, separated by `b`s
 17 |         ||| - A list of `b`s, separated by, and surrounded by, `a`s
 18 |         ||| - The free extension of a monoid `a`, with variables in `b`
 19 |         public export
 20 |         data Odd a b = (::) a (Even b a)
 21 |
 22 |     namespace Even
 23 |         ||| A list, starting with an a, and ending with a b; where adjacent elements
 24 |         ||| alternate between types a and b.
 25 |         ||| Equivalent to List (a, b)
 26 |         public export
 27 |         data Even a b = Nil | (::) a (Odd b a)
 28 |
 29 | %name Odd xs, ys, zs
 30 | %name Even xs, ys, zs
 31 |
 32 | mutual
 33 |     public export
 34 |     Eq a => Eq b => Eq (Odd a b) where
 35 |         x :: xs == y :: ys = x == y && assert_total (xs == ys)
 36 |
 37 |     public export
 38 |     Eq a => Eq b => Eq (Even a b) where
 39 |         [] == [] = True
 40 |         x :: xs == y :: ys = x == y && xs == ys
 41 |         _ == _ = False
 42 |
 43 | mutual
 44 |     public export
 45 |     Ord a => Ord b => Ord (Odd a b) where
 46 |         compare (x :: xs) (y ::ys)
 47 |            = case compare x y of
 48 |                   EQ => assert_total (compare xs ys)
 49 |                   c => c
 50 |
 51 |     public export
 52 |     Ord a => Ord b => Ord (Even a b) where
 53 |         compare [] [] = EQ
 54 |         compare [] (x :: xs) = LT
 55 |         compare (x :: xs) [] = GT
 56 |         compare (x :: xs) (y ::ys)
 57 |            = case compare x y of
 58 |                   EQ => compare xs ys
 59 |                   c => c
 60 |
 61 | mutual
 62 |     public export
 63 |     Bifunctor Odd where
 64 |         bimap f g (x :: xs) = (f x) :: assert_total (bimap g f xs)
 65 |
 66 |     public export
 67 |     Bifunctor Even where
 68 |         bimap f g [] = []
 69 |         bimap f g (x :: xs) = (f x) :: (bimap g f xs)
 70 |
 71 | mutual
 72 |     public export
 73 |     Bifoldable Odd where
 74 |         bifoldr f g acc (x :: xs) = f x (assert_total $ bifoldr g f acc xs)
 75 |
 76 |         bifoldl f g acc (x :: xs) = assert_total $ bifoldl g f (f acc x) xs
 77 |
 78 |     public export
 79 |     Bifoldable Even where
 80 |         bifoldr f g acc [] = acc
 81 |         bifoldr f g acc (x :: xs) = f x (bifoldr g f acc xs)
 82 |
 83 |         bifoldl f g acc [] = acc
 84 |         bifoldl f g acc (x :: xs) = bifoldl g f (f acc x) xs
 85 |
 86 | mutual
 87 |     public export
 88 |     Bitraversable Odd where
 89 |         bitraverse f g (x :: xs) = [| f x :: assert_total (bitraverse g f xs) |]
 90 |
 91 |     public export
 92 |     Bitraversable Even where
 93 |         bitraverse f g [] = [| [] |]
 94 |         bitraverse f g (x :: xs) = [| f x :: bitraverse g f xs |]
 95 |
 96 | namespace Snd
 97 |     public export
 98 |     Functor (Odd a) where
 99 |         map = mapSnd
100 |
101 | namespace Fst
102 |     public export
103 |     [FstFunctor] Functor (\a => Odd a b) where
104 |         map = mapFst
105 |
106 | mutual
107 |     namespace Odd
108 |         public export
109 |         (++) : Odd a b -> Odd b a -> Even a b
110 |         (x :: xs) ++ ys = x :: xs ++ ys
111 |
112 |     namespace EvenOdd
113 |         public export
114 |         (++) : Even a b -> Odd a b -> Odd a b
115 |         [] ++ ys = ys
116 |         (x :: xs) ++ ys = x :: xs ++ ys
117 |
118 | mutual
119 |     namespace Even
120 |         public export
121 |         (++) : Even a b -> Even a b -> Even a b
122 |         [] ++ ys = ys
123 |         (x :: xs) ++ ys = x :: xs ++ ys
124 |
125 |     namespace OddEven
126 |         public export
127 |         (++) : Odd a b -> Even b a -> Odd a b
128 |         (x :: xs) ++ ys = x :: xs ++ ys
129 |
130 | ||| The semigroup structure induced by treating Odd as the free extension of a
131 | ||| monoid `a`, with variables in `b`
132 | public export
133 | Semigroup a => Semigroup (Odd a b) where
134 |     [x] <+> (y :: ys) = (x <+> y) :: ys
135 |     (x :: y :: xs) <+> ys = x :: y :: xs <+> ys
136 |
137 | namespace Odd
138 |     public export
139 |     (+>) : Semigroup a => Odd a b -> a -> Odd a b
140 |     [x] +> z = [x <+> z]
141 |     x :: y :: xs +> z = x :: y :: (xs +> z)
142 |
143 |     public export
144 |     (<+) : Semigroup a => a -> Odd a b -> Odd a b
145 |     x <+ y :: ys = (x <+> y) :: ys
146 |
147 | public export
148 | Semigroup (Even a b) where
149 |     (<+>) = (++)
150 |
151 | public export
152 | Monoid a => Monoid (Odd a b) where
153 |     neutral = [neutral]
154 |
155 | public export
156 | Monoid (Even a b) where
157 |     neutral = []
158 |
159 | public export
160 | Foldable (Odd a) where
161 |     foldr = bifoldr (flip const)
162 |     foldl = bifoldl const
163 |
164 | public export
165 | singleton : a -> Odd a b
166 | singleton x = [x]
167 |
168 | namespace Snd
169 |     public export
170 |     Monoid a => Applicative (Odd a) where
171 |         pure x = [neutral, x, neutral]
172 |         fs <*> xs = biconcatMap singleton (flip map xs) fs
173 |
174 | public export
175 | flatten : Odd (Odd a b) b -> Odd a b
176 | flatten [x] = x
177 | flatten (x :: y :: xs) = x ++ (y :: flatten xs)
178 |
179 | namespace Fst
180 |     public export
181 |     [FstApplicative] Applicative (\a => Odd a b) using FstFunctor where
182 |         pure x = [x]
183 |         fs <*> xs = flatten $ bimap (flip mapFst xs) id fs
184 |
185 | public export
186 | Monoid a => Alternative (Odd a) where
187 |     empty = [neutral]
188 |     xs <|> ys = xs <+> ys
189 |
190 | namespace Snd
191 |     public export
192 |     [SndMonad] Monoid a => Monad (Odd a) where
193 |         x >>= f = assert_total $ biconcatMap singleton f x
194 |
195 |     public export
196 |     (>>=) : Monoid a => Odd a b -> (b -> Odd a c) -> Odd a c
197 |     (>>=) = (>>=) @{SndMonad}
198 |
199 | namespace Fst
200 |     public export
201 |     [FstMonad] Monad (\a => Odd a b) using FstApplicative where
202 |         x >>= f = flatten $ mapFst f x
203 |         join = flatten
204 |
205 |     public export
206 |     (>>=) : Odd a c -> (a -> Odd b c) -> Odd b c
207 |     (>>=) = (>>=) @{FstMonad}
208 |
209 | public export
210 | Traversable (Odd a) where
211 |     traverse = bitraverse pure
212 |
213 | mutual
214 |     namespace Odd
215 |         public export
216 |         odds : Odd a b -> List a
217 |         odds (x :: xs) = x :: evens xs
218 |
219 |     namespace Even
220 |         public export
221 |         evens : Even a b -> List b
222 |         evens [] = []
223 |         evens (x :: xs) = odds xs
224 |
225 | mutual
226 |     namespace Odd
227 |         public export
228 |         evens : Odd a b -> List b
229 |         evens (x :: xs) = odds xs
230 |
231 |     namespace Even
232 |         public export
233 |         odds : Even a b -> List a
234 |         odds [] = []
235 |         odds (x :: xs) = x :: evens xs
236 |
237 | mutual
238 |     namespace Odd
239 |         public export
240 |         forget : Odd a a -> List a
241 |         forget (x :: xs) = x :: forget xs
242 |
243 |     namespace Even
244 |         public export
245 |         forget : Even a a -> List a
246 |         forget [] = []
247 |         forget (x :: xs) = x :: forget xs
248 |
249 | export
250 | Show a => Show b => Show (Odd a b) where
251 |     show xs = "[\{concat $ intersperse ", " $ forget $ bimap show show xs}]"
252 |
253 | export
254 | Show a => Show b => Show (Even a b) where
255 |     show xs = "[\{concat $ intersperse ", " $ forget $ bimap show show xs}]"
256 |