0 | module Misc
  1 |
  2 | import Data.Nat
  3 | import Data.List.Elem
  4 | import Data.Vect
  5 | import Data.Vect.Elem
  6 | import System.Random
  7 | import Data.Fin
  8 | import Data.List1
  9 | import Data.List.Quantifiers
 10 | import Data.Vect.Quantifiers
 11 | import public Decidable.Equality
 12 | import Data.List
 13 | import Data.String
 14 | import Control.ANSI.SGR
 15 | import Control.Monad.State
 16 |
 17 | %hide Data.Vect.Quantifiers.All.index
 18 |
 19 | {-------------------------------------------------------------------------------
 20 | {-------------------------------------------------------------------------------
 21 | Various utilities necessary for TensorType, which don't fit anywhere else.
 22 | This file does not depend on any other file within this project.
 23 |
 24 | Some of these feel like they should be in the Idris standard library
 25 | -------------------------------------------------------------------------------}
 26 | -------------------------------------------------------------------------------}
 27 |
 28 | public export
 29 | constUnit : a -> Unit
 30 | constUnit _ = ()
 31 |
 32 | public export
 33 | const2Unit : a -> b -> Unit
 34 | const2Unit _ _ = ()
 35 |
 36 | public export
 37 | fromBool : Num a => Bool -> a
 38 | fromBool False = fromInteger 0
 39 | fromBool True = fromInteger 1
 40 |
 41 | public export
 42 | applyWhen : Bool -> (a -> a) -> a -> a
 43 | applyWhen False f a = a
 44 | applyWhen True f a = f a
 45 |
 46 | public export
 47 | runIf: HasIO io => Bool -> io () -> io ()
 48 | runIf True action = action
 49 | runIf False action = pure ()
 50 |
 51 | public export
 52 | updateAt : DecEq a => (a -> b) -> (a, b) -> (a -> b)
 53 | updateAt f (i, val) i' = case decEq i i' of
 54 |   Yes _ => val
 55 |   No _ => f i'
 56 |
 57 | ||| Graph of a dependent function
 58 | public export
 59 | graph : {t : a -> Type} ->
 60 |   (g : (x : a) -> t x) ->
 61 |   a -> (x : a ** t x)
 62 | graph g x = (x ** g x)
 63 |
 64 | ||| Version of `map` for dependent function
 65 | ||| Note that here `x : a` is identity in some sense, it comes from `f a`
 66 | public export
 67 | dependentMap : Functor f => {t : a -> Type} ->
 68 |   (g : (x : a) -> t x) ->
 69 |   f a -> f (x : a ** t x)
 70 | dependentMap g fa = (graph g) <$> fa
 71 |
 72 | ||| Dependent parametric traverse
 73 | public export
 74 | dTraverse : Applicative f =>
 75 |   ((p : pType) -> f (q p)) ->
 76 |   (xs : Vect n pType) ->
 77 |   f (All q xs)
 78 | dTraverse f [] = pure []
 79 | dTraverse f (p :: ps) = [| f p :: dTraverse f ps |]
 80 |
 81 |
 82 | ||| The empty type has (vacuously) decidable equality
 83 | public export
 84 | DecEq Void where
 85 |   decEq x _ = absurd x
 86 |
 87 | ||| This should probably be in `Decidable.Equality`?
 88 | ||| Though search cannot find this, so often we have to pass this explicitly
 89 | public export
 90 | [DecEqDPair] DecEq a => ((x : a) -> DecEq (p x)) => DecEq (DPair a p) where
 91 |   decEq (x ** px) (y ** py) = case decEq x y of
 92 |     Yes Refl => case decEq px py of
 93 |       Yes Refl => Yes Refl
 94 |       No contra => No (\Refl => contra Refl)
 95 |     No contra => No (\Refl => contra Refl)
 96 |
 97 | namespace IsNo
 98 |   ||| The proof that a decidable property leads to a contradiction
 99 |   ||| `IsNo` is a type Idris can automatically synthesise, unlike `Not`
100 |   ||| See example below
101 |   public export
102 |   data IsNo : Dec a -> Type where
103 |     ItIsNo : {prop : Type} -> 
104 |       {contra : Not prop} ->
105 |       IsNo (No {prop=prop} contra)
106 |
107 |   failing 
108 |     thisOneFails : Not ("i" = "j")
109 |     thisOneFails = %search
110 |   
111 |   thisOneDoesnt : IsNo (decEq "i" "j")
112 |   thisOneDoesnt = %search
113 |
114 |   public export
115 |   [UninhabitedIsNoRefl] {x : a} -> DecEq a =>
116 |     Uninhabited (IsNo (decEq x x)) where
117 |     uninhabited y with (decEq x x)
118 |       _ | (Yes _) with (y)
119 |         _ | ItIsNo impossible
120 |       _ | (No contra) = contra Refl
121 |   
122 |   public export 
123 |   isNoSym : DecEq a => {x, y : a} -> IsNo (decEq x y) -> IsNo (decEq y x)
124 |   isNoSym z with (decEq x y) | (decEq y x)
125 |     _ | (No contra1) | (Yes prf) = absurd (contra1 (sym prf))
126 |     _ | _           | (No contra) = ItIsNo 
127 |   
128 |   ||| Proof of inequality yields IsNo
129 |   public export
130 |   proofIneqIsNo : {x, y : a} -> DecEq a =>
131 |     Not (x = y) -> IsNo (decEq x y)
132 |   proofIneqIsNo f with (decEq x y)
133 |     _ | (Yes prf) = absurd (f prf)
134 |     _ | (No contra) = ItIsNo
135 |
136 | namespace Maybe
137 |   public export
138 |   data IsNothing : Maybe a -> Type where
139 |     ItIsNothing : IsNothing Nothing
140 |
141 |   public export
142 |   maybeVoidIsNothing : (x : Maybe Void) -> IsNothing x
143 |   maybeVoidIsNothing Nothing = ItIsNothing
144 |   maybeVoidIsNothing (Just v) = absurd v
145 |
146 |   public export
147 |   Uninhabited (IsNothing (Just x)) where
148 |     uninhabited ItIsNothing impossible
149 |
150 |
151 | namespace NotElem
152 |   public export
153 |   data NotElem : DecEq a => (x : a) -> (xs : Vect n a) -> Type where
154 |     NotInEmptyVect : DecEq a => {0 x : a} -> NotElem x []
155 |     NotInNonEmptyVect : DecEq a => {0 x, y : a} ->
156 |       (xs : Vect n a) ->
157 |       IsNo (decEq x y) ->
158 |       (ne : NotElem x xs) =>
159 |       NotElem x (y :: xs)
160 |   
161 |   public export
162 |   notEqualNotElem : DecEq a =>
163 |     {0 x, y : a} ->
164 |     (neq : IsNo (decEq x y)) ->
165 |     NotElem x [y]
166 |   notEqualNotElem neq = NotInNonEmptyVect [] neq
167 |   
168 |   ||| If an element `i` is not in the singleton list `[j]`, then `j` is not in
169 |   ||| the singleton list `[i]`
170 |   public export
171 |   notElemSym : DecEq a => {i, j : a} -> NotElem i [j] -> NotElem j [i]
172 |   notElemSym (NotInNonEmptyVect [] isNo) = notEqualNotElem (isNoSym isNo)
173 |   
174 |   ||| If an element `i` is in the singleton list `[j]`, then `j` is in the 
175 |   ||| singleton list `[i]`
176 |   public export
177 |   elemSym : {i, j : a} -> Vect.Elem.Elem i [j] ->
178 |     Vect.Elem.Elem j [i]
179 |   elemSym Here = Here
180 |
181 |
182 | namespace Applicative
183 |   ||| Tensorial strength
184 |   public export
185 |   strength : Applicative f => a -> f b -> f (a, b)
186 |   strength a fb = [| (pure a, fb) |]
187 |   
188 |
189 | namespace VectFoldable
190 |   ||| Implementation of Foldable for Vect that is denotationally equivalent to
191 |   ||| one in Data.Vect, but which does not use `foldrImpl` and therefore
192 |   ||| reduces in the typechecker
193 |   public export
194 |   [straightforward] Foldable (Vect n) where
195 |     foldr f z [] = z
196 |     foldr f z (x :: xs) = f x (foldr f z xs)
197 |
198 |   ||| toList with a different foldable implementation
199 |   public export
200 |   toList' : Vect n a -> List a
201 |   toList' = foldr @{straightforward} (::) []
202 |
203 |   public export
204 |   fromList' : (xs : List a) -> Vect (length xs) a
205 |   fromList' [] = []
206 |   fromList' (x :: xs) = x :: fromList' xs
207 |
208 | ||| Duplicate of utilities for Data.Vect in their Naperian form
209 | namespace Vect
210 |   public export
211 |   sum : Num a => Vect n a -> a
212 |   sum xs = foldr @{straightforward} (+) (fromInteger 0) xs
213 |   
214 |   -- Because of the way foldr for Vect is implemented in Idris 
215 |   -- we have to use this approach below, otherwise allSuccThenProdSucc breaks
216 |   public export 
217 |   prod : Num a => Vect n a -> a
218 |   prod xs = foldr @{straightforward} (*) (fromInteger 1) xs
219 |   -- prod [] = fromInteger 1
220 |   -- prod (x :: xs) = x * prod xs
221 |
222 |   public export
223 |   max : Ord a => Vect n a -> Maybe a
224 |   max [] = Nothing
225 |   max (x :: xs) = case max xs of
226 |     Nothing => Just x
227 |     Just y => Just (max x y)
228 |
229 |   ||| Dual to concat from Data.Vect
230 |   public export
231 |   unConcat : {n, m : Nat} -> Vect (n * m) a -> Vect n (Vect m a)
232 |   unConcat {n = 0} _ = []
233 |   unConcat {n = (S k)} xs = let (f, s) = splitAt m xs
234 |                             in f :: unConcat s
235 |
236 |   ||| Trim a specified trailing value
237 |   public export
238 |   dropFromEnd : Eq a => a -> Vect n a -> List a
239 |   dropFromEnd c row = reverse (dropWhile (== c) (reverse (toList row)))
240 |   
241 |   ||| Combination of `cons` and `snoc`: adds an element in front, and at the end
242 |   public export
243 |   consSnoc : Vect n a -> a -> a -> Vect (2 + n) a
244 |   consSnoc xs a b = a :: snoc xs b
245 |   
246 |   ||| Pad a vector with a specified element to exactly `targetSize`
247 |   public export
248 |   padToSize : Vect size a -> (targetSize : Nat) -> a ->
249 |     LTE size targetSize => 
250 |     Vect targetSize a
251 |   padToSize [] Z c = []
252 |   padToSize [] (S k) c = c :: padToSize [] k c
253 |   padToSize (x :: xs) (S k) c = x :: padToSize xs k c @{fromLteSucc %search}
254 |
255 |   ||| Drop the first i elements of a vector
256 |   ||| Analogous to Data.Vect.drop, except the index is Fin n instead of Nat
257 |   public export
258 |   drop : (i : Fin (S n)) -> Vect n a -> Vect (minus n (finToNat i)) a
259 |   drop FZ xs = rewrite minusZeroRight n in xs
260 |   drop (FS i) (x :: xs) = drop i xs
261 |   
262 |   namespace DropElem
263 |     ||| Drop all the elements up and until the element `x` from a vector
264 |     public export
265 |     drop : (xs : Vect n a) ->
266 |       (elem : Elem x xs) ->
267 |       Vect (n `minus` (finToNat (FS (elemToFin elem)))) a
268 |     drop {n=S k} (_ :: xs) Here = rewrite minusZeroRight k in xs
269 |     drop (_ :: xs) (There later) = drop xs later
270 |
271 |
272 | namespace List
273 |   public export
274 |   sum : Num a => List a -> a
275 |   sum = foldr (+) (fromInteger 0) 
276 |
277 |   public export
278 |   prod : Num a => List a -> a
279 |   prod = foldr (*) (fromInteger 1)
280 |
281 |   public export
282 |   listZip : List a -> List b -> List (a, b)
283 |   listZip (x :: xs) (y :: ys) = (x, y) :: listZip xs ys
284 |   listZip _ _ = []
285 |
286 |   ||| Map each element along with its zero-based position in the list.
287 |   public export
288 |   mapWithIndex : (Nat -> a -> b) -> List a -> List b
289 |   mapWithIndex f = go 0
290 |     where
291 |       go : Nat -> List a -> List b
292 |       go _ []        = []
293 |       go i (x :: xs) = f i x :: go (S i) xs
294 |
295 |   ||| Split a list into consecutive chunks of size `n` (clamped to at least 1).
296 |   ||| The final chunk may be shorter than `n`, this is why the length of the
297 |   ||| list is needed as upper bound.
298 |   public export
299 |   chunksOf : (n : Nat) -> List a -> List (List a)
300 |   chunksOf n xs = go (max 1 n) xs (length xs)
301 |     where
302 |       go : Nat -> List a -> (len : Nat) -> List (List a)
303 |       go _  []          _     = []
304 |       go _  ys@(_ :: _) Z     = [ys]
305 |       go sz ys@(_ :: _) (S f) = case splitAt sz ys of
306 |                                   (h, t) => h :: go sz t f
307 |   
308 |   public export
309 |   max : Ord a => List a -> Maybe a
310 |   max [] = Nothing
311 |   max (x :: xs) = case max xs of
312 |     Nothing => Just x
313 |     Just y => Just (max x y)
314 |
315 |   namespace NonEmpty
316 |     public export
317 |     max : Ord a => (xs : List a) -> (ne : NonEmpty xs) => a
318 |     max [x] {ne=IsNonEmpty} = x
319 |     max (x :: y :: xs) {ne=IsNonEmpty} = max x (max (y :: xs))
320 |
321 |   ||| Trim a specified trailing value
322 |   public export
323 |   dropFromEnd : Eq a => a -> List a -> List a
324 |   dropFromEnd c row = reverse (dropWhile (== c) (reverse row))
325 |
326 |   ||| Combination of `cons` and `snoc`: adds an element in front, and at the end
327 |   public export
328 |   consSnoc : List a -> a -> a -> List a
329 |   consSnoc xs x y = x :: snoc xs y
330 |
331 |   ||| Pad a list with a specified element to at least `targetSize`
332 |   public export
333 |   padToSize : Nat -> a -> List a -> List a
334 |   padToSize targetSize padValue xs =
335 |     xs ++ replicate (minus targetSize (length xs)) padValue
336 |
337 |   ||| Drop all the elements after the element `x` from a list
338 |   public export
339 |   dropAfterElem : (xs : List a) -> (elem : Elem x xs) -> List a
340 |   dropAfterElem (x :: _) Here = [x]
341 |   dropAfterElem (y :: xs) (There p) = y :: dropAfterElem xs p
342 |
343 | namespace VectNaperianUtils
344 |   ||| Analogue of `(::)`
345 |   public export
346 |   cons : x -> (Fin l -> x) -> (Fin (S l) -> x)
347 |   cons x _ FZ = x
348 |   cons _ f (FS k') = f k'
349 |
350 |   -- dcons : x -> ((i : Fin k) -> i' i) -> ((i : Fin (S k)) -> i' (cons x i'))
351 |   
352 |   public export
353 |   head : (Fin (S l) -> x) -> x
354 |   head f = f FZ
355 |   
356 |   public export
357 |   tail : (Fin (S l) -> x) -> (Fin l -> x)
358 |   tail f = f . FS
359 |   
360 |   ||| All but the last element
361 |   public export
362 |   init : (Fin (S n) -> a) -> Fin n -> a
363 |   init f x = f (weaken x)
364 |   
365 |   ||| Analogus to `Data.Vect.take`
366 |   public export 
367 |   takeFin : (s : Fin (S n)) -> Vect n a -> Vect (finToNat s) a
368 |   takeFin FZ _ = []
369 |   takeFin (FS s) (x :: xs) = x :: takeFin s xs
370 |
371 |   public export
372 |   sum : Num a => {n : Nat} -> (Fin n -> a) -> a
373 |   sum {n = 0} _ = 0
374 |   sum {n = (S k)} content = content FZ + sum (content . FS)
375 |
376 |   public export
377 |   prod : Num a => {n : Nat} -> (Fin n -> a) -> a
378 |   prod = prod . tabulate
379 |
380 |   public export
381 |   toList : {n : Nat} -> (Fin n -> a) -> List a
382 |   toList = toList' . tabulate
383 |
384 | namespace FinArithmetic
385 |   ||| Proof that subtracting from a successor is the same as taking the sucessor
386 |   ||| of the subtraction
387 |   public export
388 |   minusSuccLTE : {n, m : Nat} -> LTE n m ->
389 |     minus (S m) n = S (minus m n)
390 |   minusSuccLTE {m = 0, n = 0} LTEZero = Refl
391 |   minusSuccLTE {m = (S k), n = 0} LTEZero = Refl
392 |   minusSuccLTE {m = (S k), n = (S left)} (LTESucc x) = minusSuccLTE x
393 |
394 |   ||| A version of `weakenN` from Data.Fin with `n` on the other side of `+`
395 |   public export
396 |   weakenN' : (0 n : Nat) -> Fin m -> Fin (n + m)
397 |   weakenN' n x = rewrite plusCommutative n m in weakenN n x
398 |
399 |   ||| Variant of `weakenN` from `Data.Fin`, but for multiplication
400 |   ||| Like shiftMul, but without changing the value of the index
401 |   public export
402 |   weakenMultN : {n : Nat} ->
403 |     (m : Nat) -> {auto prf : IsSucc m} ->
404 |     (i : Fin n) -> Fin (m * n)
405 |   weakenMultN (S 0) {prf = ItIsSucc} i = rewrite multOneLeftNeutral n in i
406 |   weakenMultN (S (S k)) {prf = ItIsSucc} i = weakenN' n (weakenMultN (S k) i)
407 |
408 |   multRightUnit : (m : Nat) -> m * 1 = m
409 |   multRightUnit 0 = Refl
410 |   multRightUnit (S k) = cong S (multRightUnit k)
411 |
412 |   multRightZeroCancel : (m : Nat) -> m * 0 = 0
413 |   multRightZeroCancel 0 = Refl
414 |   multRightZeroCancel (S k) = multRightZeroCancel k
415 |
416 |   ||| Variant of `shift` from Data.Fin, but for multiplication
417 |   ||| Given a stride and an index `i : Fin n`, it returns a stride-sized step
418 |   ||| That is, it returns `stride * i` : Fin (stride * n)
419 |   ||| Implemented by recursing on i, adding stride each time
420 |   public export
421 |   shiftMul : (stride : Nat) -> (prf : IsSucc stride) =>
422 |     (i : Fin n) -> Fin (n * stride)
423 |   shiftMul (S s) {prf = ItIsSucc} FZ = FZ
424 |   shiftMul stride (FS i) = shift stride (shiftMul stride i)
425 |
426 |   shiftMulTest : shiftMul {n=3} 5 1 = 5
427 |   shiftMulTest = Refl
428 |
429 |   ||| Analogue of `strengthen` from Data.Fin
430 |   ||| Attempts to strengthen the bound on Fin (m + n) to Fin m
431 |   ||| If it doesn't succeed, then returns the remainder in Fin n
432 |   public export
433 |   strengthenN : {m, n : Nat} -> Fin (m + n) -> Either (Fin m) (Fin n)
434 |   strengthenN {m = 0} x = Right x
435 |   strengthenN {m = (S k)} FZ = Left FZ
436 |   strengthenN {m = (S k)} (FS x) with (strengthenN x)
437 |     _ | (Left p) = Left $ FS p
438 |     _ | (Right q) = Right q
439 |
440 |   ||| Analogue of `finS` from `Data.Fin`, but without without wrapping
441 |   ||| That is, `finS' last = last`
442 |   public export
443 |   finS' : {n : Nat} -> Fin n -> Fin n
444 |   finS' {n = 1} x = x
445 |   finS' {n = S (S k)} FZ = FS FZ
446 |   finS' {n = S (S k)} (FS x) = FS (finS' x)
447 |   --finS' {n = S _} x = case strengthen x of
448 |   --    Nothing => x
449 |   --    Just y => FS y
450 |
451 |   finS'test1 : finS' {n=10} 4 = 5
452 |   finS'test1 = Refl
453 |
454 |   finS'lastIsLast : {n : Nat} -> finS' {n=S n} Fin.last = Fin.last
455 |   finS'lastIsLast {n = 0} = Refl
456 |   finS'lastIsLast {n = (S k)} = cong FS finS'lastIsLast
457 |
458 |   ||| This can be implemented using `Data.Fin.Order`, but it doesn't seem worth
459 |   ||| the effort, as the typechecker ends up needing a lot of extra hand holding
460 |   public export
461 |   lastBiggerThanOthers : {n : Nat} ->
462 |     (i : Fin (S n)) ->
463 |     So (Fin.last >= i)
464 |   lastBiggerThanOthers {n = 0} FZ = Oh
465 |   lastBiggerThanOthers {n = (S k)} FZ = Oh
466 |   lastBiggerThanOthers {n = (S k)} (FS x) = lastBiggerThanOthers x
467 |   
468 |   -- lastBiggerThanOthers {n = 0} FZ = FromNatPrf LTEZero
469 |   -- lastBiggerThanOthers {n = (S k)} FZ = FromNatPrf LTEZero
470 |   -- lastBiggerThanOthers {n = (S k)} (FS x) = FSFinLTE (lastBiggerThanOthers x)
471 |
472 |   ||| Adds two bounded numbers, bounds the result
473 |   ||| That is, `addFinsBounded {n=5} 3 4 = 4`
474 |   ||| `assert_smaller` is only needed for totality checking
475 |   public export
476 |   addFinsBounded : {n : Nat} -> Fin n -> Fin n -> Fin n
477 |   addFinsBounded x FZ = x
478 |   addFinsBounded x (FS y) = addFinsBounded (finS' x)
479 |     (assert_smaller (FS y) (weaken y))
480 |
481 |   finSTest : finS' {n = 5} 3 = 4
482 |   finSTest = Refl
483 |
484 |   finSTest2 : finS' {n = 5} 4 = 4
485 |   finSTest2 = Refl
486 |
487 |   ||| Divides a Fin by 2, rounding down
488 |   ||| `half {n=10} 6 = 3`
489 |   ||| `half {n=10} 5 = 2`
490 |   ||| `half {n=10} 4 = 2`
491 |   ||| `half {n=10} 3 = 1`
492 |   ||| `half {n=10} 2 = 1`
493 |   ||| `half {n=10} 1 = 0`
494 |   public export
495 |   half : Fin n -> Fin n
496 |   half FZ = FZ
497 |   half (FS FZ) = FZ
498 |   half (FS (FS x)) = weaken (FS (half x))
499 |
500 |   ||| Computes the midway index between two bounds
501 |   public export
502 |   mid : (low, high : Fin n) ->
503 |     So (high >= low) =>
504 |     Fin n
505 |   mid FZ high = half high
506 |   mid (FS x) (FS y) @{prf} = FS (mid x y)
507 |
508 |   -- ||| There is a similar function in Data.Fin.Arith, which has the smallest
509 |   -- ||| possible bound. This one does not, but has a simpler type signature.
510 |   -- public export
511 |   -- multFin : {m, n : Nat} -> Fin m -> Fin n -> Fin (m * n)
512 |   -- multFin {n = (S _)} FZ y = FZ
513 |   -- multFin {n = (S _)} (FS x) y = FinArith.(+) y (weaken (multFin x y))
514 |
515 | public export
516 | multSucc : {m, n : Nat} -> IsSucc m -> IsSucc n -> IsSucc (m * n)
517 | multSucc {m = S m'} {n = S n'} ItIsSucc ItIsSucc = ItIsSucc
518 |
519 | public export
520 | allSuccThenProdSucc : (xs : List Nat) ->
521 |   (ps : All IsSucc xs) =>
522 |   IsSucc (prod xs)
523 | allSuccThenProdSucc [] {ps = []} = ItIsSucc
524 | allSuccThenProdSucc (_ :: xs') {ps = p :: _} = multSucc p (allSuccThenProdSucc xs')
525 |
526 | public export
527 | cumulativeSum : Traversable t => Num a => t a -> t a
528 | cumulativeSum = evalState (the a 0) . traverse (\x => modify (+ x) >> get)
529 |
530 | ||| Data structure storing a lower and upper bound during a search
531 | record Range (n : Nat) where
532 |   constructor MkRange
533 |   lowerBound : Fin n
534 |   higherBound : Fin n
535 |   {auto prf : So (higherBound >= lowerBound)}
536 |
537 | ||| Given a non-empty sorted vector `xs`, an element `x` and a lower and upper
538 | ||| bound, it finds the "right bin", i.e. the index of the smallest element 
539 | ||| between the bounds that's bigger than `x`
540 | ||| If `x` is bigger than the largest element, returns `Nothing`
541 | ||| `findBinBetween [2,7,10] 1 (MkRange 0 2) = Just 0`
542 | ||| `findBinBetween [2,7,10] 3 (MkRange 0 2) = Just 1`
543 | ||| `findBinBetween [2,7,10] 9 (MkRange 0 2) = Just 2`
544 | ||| `findBinBetween [2,7,10] 7 (MkRange 0 2) = Just 2`
545 | ||| `findBinBetween [2,7,10] 15 (MkRange 0 2) = Nothing`
546 | ||| `findBinBetween [1,2,3,4,5] 6 (MkRange 0 4) = Nothing`
547 | ||| Done using binary search
548 | public export
549 | findBinBetween : Ord a => {n : Nat} -> (is : IsSucc n) =>
550 |   (xs : Vect n a) -> -- we assume this is sorted
551 |   (x : a) ->
552 |   (range : Range n) ->
553 |   Maybe (Fin n)
554 | findBinBetween {is = ItIsSucc {n=k}} xs x r@(MkRange lowInd highInd)
555 |   = case x > index highInd xs of
556 |   True => Nothing -- There are no elements bigger than `x`
557 |   False => case x <= index lowInd xs of
558 |     True => Just lowInd
559 |     False => let midInd = mid lowInd highInd
560 |              in case compare x (index midInd xs) of
561 |                LT => let newRange = MkRange lowInd midInd {prf = believe_me ()}
562 |                      in findBinBetween xs x (assert_smaller r newRange)
563 |                EQ => Just (finS' midInd) -- we need the next index after the middle one
564 |                GT => let newRange = MkRange (finS' midInd) highInd {prf = believe_me ()}
565 |                      in findBinBetween xs x (assert_smaller r newRange)
566 |
567 | namespace FindBinTests
568 |   findBinTest1 : findBinBetween [2,7,10] 1 (MkRange 0 2) = Just 0
569 |   findBinTest1 = Refl
570 |
571 |   findBinTest2 : findBinBetween [2,7,10] 3 (MkRange 0 2) = Just 1
572 |   findBinTest2 = Refl
573 |
574 |   findBinTest3 : findBinBetween [2,7,10] 9 (MkRange 0 2) = Just 2
575 |   findBinTest3 = Refl
576 |
577 |   findBinTest4 : findBinBetween [2,7,10] 7 (MkRange 0 2) = Just 2
578 |   findBinTest4 = Refl
579 |
580 |   findBinTest5 : findBinBetween [2,7,10] 15 (MkRange 0 2) = Nothing
581 |   findBinTest5 = Refl
582 |
583 |   findBinTest6 : findBinBetween [1,2,3,4,5] 6 (MkRange 0 4) = Nothing
584 |   findBinTest6 = Refl
585 |
586 | ||| Todo can this eventually be generalised to non-cubical tensors?
587 | ||| Given a non-empty sorted vector `xs` and an element `x` it finds the 
588 | ||| "right bin", i.e. the index of the smallest element that's bigger than `x`
589 | ||| If `x` is bigger than the highest element, returns `Nothing`
590 | ||| `findBin [2,7,10] 1 = Just 0`
591 | ||| `findBin [2,7,10] 3 = Just 1`
592 | ||| `findBin [2,4,6,8] 7 = Just 3`
593 | public export
594 | findBin : Ord a => {n : Nat} -> (is : IsSucc n) =>
595 |   (xs : Vect n a) -> (x : a) -> Maybe (Fin n)
596 | findBin {is = ItIsSucc {n=k}} xs x
597 |   = findBinBetween xs x (MkRange 0 last {prf=lastBiggerThanOthers {n=k} 0})
598 |  
599 | public export
600 | mkDepPairShow : Show a => (ss : (x : a) -> Show (b x)) => (DPair a b -> String)
601 | mkDepPairShow = \(x ** y) => "\{show x} ** \{show (y)}"
602 |
603 | public export
604 | Show a => ((x : a) -> Show (b x)) => Show (DPair a b) where
605 |    show = mkDepPairShow
606 |
607 | namespace RandomUtils
608 |   public export
609 |   Random Unit where
610 |     randomIO = pure ()
611 |     randomRIO _ = pure ()
612 |
613 |   public export
614 |   Random a => Random b => Random (a, b) where
615 |     randomIO = [| (randomIO, randomIO) |]
616 |     randomRIO ((loA, loB), (hiA, hiB))
617 |       = [| (randomRIO (loA, hiA), randomRIO (loB, hiB)) |]
618 |
619 | namespace All
620 |   namespace Vect
621 |     public export
622 |     rewriteAllMap : {xs : Vect n a} ->
623 |       All p (f <$> xs) ->
624 |       All (p . f) xs
625 |     rewriteAllMap {xs = []} [] = []
626 |     rewriteAllMap {xs = (x :: xs)} (a :: as) = a :: rewriteAllMap as
627 |
628 |     public export
629 |     rewriteAllMap' : {xs : Vect n a} ->
630 |       All (p . f) xs ->
631 |       All p (f <$> xs)
632 |     rewriteAllMap' {xs = []} [] = []
633 |     rewriteAllMap' {xs = (x :: xs)} (a :: as) = a :: rewriteAllMap' as
634 |   
635 |   namespace List
636 |     public export
637 |     rewriteAllMap : {xs : List a} ->
638 |       All p (f <$> xs) ->
639 |       All (p . f) xs
640 |     rewriteAllMap {xs = []} [] = []
641 |     rewriteAllMap {xs = (x :: xs)} (a :: as) = a :: rewriteAllMap as
642 |
643 |   ||| Cnvert an all to a vector if it's made out of replicated things
644 |   public export
645 |   allToVect : Vect.Quantifiers.All.All p (replicate n a) -> Vect n (p a)
646 |   allToVect [] = []
647 |   allToVect (aa :: aaps) = aa :: allToVect aaps
648 |
649 |   public export
650 |   constantToVect : {xs : Vect n a} ->
651 |     Vect.Quantifiers.All.All (const b) xs -> Vect n b
652 |   constantToVect [] = []
653 |   constantToVect (bb :: bbs) = bb :: constantToVect bbs
654 |
655 | public export
656 | record Iso (a, b : Type) where
657 |   constructor MkIso
658 |   forward : a -> b
659 |   backward : b -> a
660 |   forwardBackward : (x : a) -> backward (forward x) = x
661 |   backwardForward : (y : b) -> forward (backward y) = y
662 |
663 | ||| The identity isomorphism
664 | public export
665 | idIso : Iso a a
666 | idIso = MkIso id id (\_ => Refl) (\_ => Refl)
667 |
668 | -- ||| Duplicate of `index` from Data.Vect.Quantifiers.All, but with an
669 | -- ||| additional `public` export modifier
670 | public export
671 | index : (i : Fin k) -> Vect.Quantifiers.All.All p ts -> p (Vect.index i ts)
672 | index FZ (x :: xs) = x
673 | index (FS j) (x :: xs) = index j xs
674 |
675 | ||| `Fin n` without ordering, i.e. a set. Quotient not implemented, simply a 
676 | ||| wrapped around `Fin n` to make `Bag` and `List` containers not reduce to 
677 | ||| the same type. Once quotient containers are implemented this will not be
678 | ||| necessary.
679 | public export
680 | record FiniteSet (n : Nat) where
681 |   constructor MkFiniteSet
682 |   toFin : Fin n
683 |
684 | namespace TerminalStyling
685 |   ||| Used to color/style terminal output. Wraps a string in the given SGR 
686 |   ||| attributes from `Control.ANSI.SGR`
687 |   export
688 |   styled : List SGR -> String -> String
689 |   styled sgrs s = escapeSGR sgrs ++ s ++ escapeSGR [Reset]
690 |
691 |   export
692 |   dim : String -> String
693 |   dim = styled [SetStyle Faint]
694 |
695 |   export
696 |   bold : String -> String
697 |   bold = styled [SetStyle Bold]
698 |
699 |   export
700 |   cyan : String -> String
701 |   cyan = styled [SetForeground Cyan]
702 |
703 |   export
704 |   yellow : String -> String
705 |   yellow = styled [SetForeground Yellow]
706 |
707 |   export
708 |   green : String -> String
709 |   green = styled [SetForeground Green]
710 |
711 | {-
712 |
713 | interface Comult (f : Type -> Type) a where
714 |   comult : f a -> f (f a)
715 |
716 | {shape : Vect n Nat} -> Num a => Comult (TensorA shape) a where
717 |   comult t = ?eir
718 |
719 | gg : TensorA [3] Double -> TensorA [3, 3] Double
720 | gg (TS xs) = TS $ map ?fn ?gg_rhs_0
721 |
722 | -- [1, 2, 3]
723 | -- can we even do outer product?
724 | -- we wouldn't need reduce, but something like multiply?
725 | outer : {f : Type -> Type} -> {a : Type}
726 |   -> (Num a, Applicative f, Algebra f a)
727 |   => f a -> f a -> f (f a)
728 | outer xs ys = let t = liftA2 xs ys
729 |               in ?outer_rhs 
730 | -}
731 |
732 | |||| filter' works without `with`?
733 | filter' : (a -> Bool) -> Vect n a -> (p ** Vect p a)
734 | filter' p [] = (0 ** [])
735 | filter' p (x :: xs) = case filter' p xs of 
736 |   (_ ** xs') => if p x then (_ ** x :: xs') else (_ ** xs')
737 |
738 | ||| filter'' implemented with `with`
739 | filter'' : (a -> Bool) -> Vect n a -> (p ** Vect p a)
740 | filter'' p [] = (0 ** [])
741 | filter'' p (x :: xs) with (filter' p xs)
742 |   _ | (_ ** xs') = if p x then (_ ** x :: xs') else (_ ** xs')
743 |
744 | {-
745 | Prelude.absurd : Uninhabited t => t -> a
746 | believe_me : a -> b
747 | -}
748 |
749 | namespace Linearity
750 |   ll1 : {n : Nat} -> Vect n a -> Nat
751 |   ll1 {n} _ = n
752 |   
753 |   -- Should this be detected as `using` the variable `n`?
754 |   -- in pattern matching, we'd have to unify type of `xs` which has in itself `len`
755 |   -- and `n` which in this case is computed to be `S len`?
756 |   -- this step of `ll2` is decomposing `n` only one level down, but the entire recursion ends up using the entire `n`
757 |   ll2 : {0 n : Nat} -> Vect n a -> Nat
758 |   ll2 [] = 0
759 |   ll2 {n=S t} (x :: xs) = 1 + ll2 xs
760 |
761 |
762 |
763 | -- public export
764 | -- filter : (elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
765 | -- filter p []      = ( _ ** [] )
766 | -- filter p (x::xs) =
767 | --   let (_ ** tail) = filter p xs
768 | --    in if p x then
769 | --         (_ ** x::tail)
770 | --       else
771 | --         (_ ** tail)
772 |
773 | public export
774 | filter2 : (a -> Bool) -> Vect len a -> Vect p a
775 | filter2 f xs = ?filter2_rhs
776 |
777 | -- ||| Splits xs at each occurence of delimeter (general version for lists)
778 | -- public export
779 | -- splitList : Eq a =>
780 | --   (xs : List a) -> (delimeter : List a) -> (n : Nat ** Vect n (List a))
781 | -- splitList xs delimeter = 
782 | --   if delimeter == []
783 | --     then (1 ** [xs]) -- Empty delimiter returns original list
784 | --     else case isInfixOfList delimeter xs of
785 | --       False => (1 ** [xs]) -- Delimiter not found, return original list
786 | --       True => 
787 | --         let (before, after) = breakOnList delimeter xs
788 | --         in case after of
789 | --           [] => (1 ** [before]) -- No more occurrences
790 | --           _  => let (restCount ** restVect) = splitList (drop (length delimeter) after) delimeter
791 | --                 in (S restCount ** before :: restVect)
792 | --   where
793 | --     -- Check if list starts with delimiter
794 | --     isPrefixOfList : List a -> List a -> Bool
795 | --     isPrefixOfList [] _ = True
796 | --     isPrefixOfList _ [] = False
797 | --     isPrefixOfList (d :: ds) (x :: xs) = d == x && isPrefixOfList ds xs
798 | --     
799 | --     -- Check if delimiter occurs anywhere in the list
800 | --     isInfixOfList : List a -> List a -> Bool
801 | --     isInfixOfList del [] = del == []
802 | --     isInfixOfList del xs@(_ :: xs') = 
803 | --       isPrefixOfList del xs || isInfixOfList del xs'
804 | --     
805 | --     -- Break list at first occurrence of delimiter
806 | --     breakOnList : List a -> List a -> (List a, List a)
807 | --     breakOnList del xs = breakOnListAcc del xs []
808 | --       where
809 | --         breakOnListAcc : List a -> List a -> List a -> (List a, List a)
810 | --         breakOnListAcc del remaining acc = 
811 | --           case isPrefixOfList del remaining of
812 | --             True => (reverse acc, remaining)
813 | --             False => case remaining of
814 | --               [] => (reverse acc, [])
815 | --               (c :: cs) => breakOnListAcc del cs (c :: acc)
816 | -- 
817 | -- ||| Splits xs at each occurence of delimeter (string version)
818 | -- public export
819 | -- splitString : (xs : String) -> (delimeter : String) -> (n : Nat ** Vect n String)
820 | -- splitString xs delimeter = 
821 | --   let (n ** result) = splitList (unpack xs) (unpack delimeter)
822 | --   in (n ** pack <$> result)
823 | -- 
824 | -- ||| Simple string replacement function
825 | -- public export
826 | -- replaceString : String -> String -> String -> String
827 | -- replaceString old new str = 
828 | --   let chars = unpack str
829 | --       oldChars = unpack old
830 | --       newChars = unpack new
831 | --   in pack (replaceInList oldChars newChars chars)
832 | --   where
833 | --     replaceInList : List Char -> List Char -> List Char -> List Char
834 | --     replaceInList [] _ xs = xs
835 | --     replaceInList old new [] = []
836 | --     replaceInList old new xs@(x :: rest) =
837 | --       if isPrefixOf old xs
838 | --         then new ++ replaceInList old new (drop (length old) xs)
839 | --         else x :: replaceInList old new rest