16 | %hide Builtin.infixr.(#)
17 | %hide Data.Vect.Quantifiers.All.index
19 | {-------------------------------------------------------------------------------
20 | {-------------------------------------------------------------------------------
21 | Various utilities necessary for TensorType, but that don't fit anywhere else
22 | Does not depend on any other file within this project.
24 | Some of these feel like they should be in the Idris standard library
26 | -------------------------------------------------------------------------------}
27 | -------------------------------------------------------------------------------}
51 | ||| Graph of a dependent function
58 | ||| Version of `map` for dependent function
59 | ||| Note that here `x : a` is identity in some sense, it comes from `f a`
68 | ||| The proof that a decidable property leads to a contradiction
69 | ||| `IsNo` is a type Idris can automatically synthesise, unlike `Not`
70 | ||| See example below
77 | failing
98 | ||| Proof of inequality yields IsNo
138 | ||| If an element `i` is not in the singleton list `[j]`, then `j` is not in
139 | ||| the singleton list `[i]`
144 | ||| If an element `i` is in the singleton list `[j]`, then `j` is in the
145 | ||| singleton list `[i]`
153 | ||| Tensorial strength
160 | ||| Implementation of Foldable for Vect that is denotationally equivalent to
161 | ||| one in Data.Vect, but which does not use `foldrImpl` and therefore
162 | ||| reduces in the typechecker
168 | ||| toList with a different foldable implementation
178 | ||| Duplicate of utilities for Data.Vect in their Naperian form
184 | -- Because of the way foldr for Vect is implemented in Idris
185 | -- we have to use this approach below, otherwise allSuccThenProdSucc breaks
189 | -- prod [] = fromInteger 1
190 | -- prod (x :: xs) = x * prod xs
212 | ||| Dual to concat from Data.Vect
219 | ||| Trim a specified trailing value
224 | ||| Combination of `cons` and `snoc`: adds an element in front, and at the end
229 | ||| Pad a vector with a specified element to exactly `targetSize`
238 | ||| Drop the first i elements of a vector
239 | ||| Analogous to Data.Vect.drop, except the index is Fin n instead of Nat
246 | ||| Drop all the elements up and until the element `x` from a vector
270 | ||| Map each element along with its zero-based position in the list.
274 | where
279 | ||| Split a list into consecutive chunks of size `n` (clamped to at least 1).
280 | ||| The final chunk may be shorter than `n`, this is why the length of the
281 | ||| list is needed as upper bound.
285 | where
305 | ||| Trim a specified trailing value
310 | ||| Combination of `cons` and `snoc`: adds an element in front, and at the end
315 | ||| Pad a list with a specified element to at least `targetSize`
321 | ||| Drop all the elements after the element `x` from a list
328 | ||| Analogue of `(::)`
334 | -- dcons : x -> ((i : Fin k) -> i' i) -> ((i : Fin (S k)) -> i' (cons x i'))
344 | ||| All but the last element
349 | ||| Analogus to `Data.Vect.take`
369 | ||| Proof that subtracting from a successor is the same as taking the sucessor
370 | ||| of the subtraction
378 | ||| A version of `weakenN` from Data.Fin with `n` on the other side of `+`
383 | ||| Variant of `weakenN` from `Data.Fin`, but for multiplication
384 | ||| Like shiftMul, but without changing the value of the index
400 | ||| Variant of `shift` from Data.Fin, but for multiplication
401 | ||| Given a stride and an index `i : Fin n`, it returns a stride-sized step
402 | ||| That is, it returns `stride * i` : Fin (stride * n)
403 | ||| Implemented by recursing on i, adding stride each time
413 | ||| Analogue of `strengthen` from Data.Fin
414 | ||| Attempts to strengthen the bound on Fin (m + n) to Fin m
415 | ||| If it doesn't succeed, then returns the remainder in Fin n
424 | ||| Analogue of `finS` from `Data.Fin`, but without without wrapping
425 | ||| That is, `finS' last = last`
431 | --finS' {n = S _} x = case strengthen x of
432 | -- Nothing => x
433 | -- Just y => FS y
442 | ||| This can be implemented using `Data.Fin.Order`, but it doesn't seem worth
443 | ||| the effort, as the typechecker ends up needing a lot of extra hand holding
452 | -- lastBiggerThanOthers {n = 0} FZ = FromNatPrf LTEZero
453 | -- lastBiggerThanOthers {n = (S k)} FZ = FromNatPrf LTEZero
454 | -- lastBiggerThanOthers {n = (S k)} (FS x) = FSFinLTE (lastBiggerThanOthers x)
456 | ||| Adds two bounded numbers, bounds the result
457 | ||| That is, `addFinsBounded {n=5} 3 4 = 4`
458 | ||| `assert_smaller` is only needed for totality checking
471 | ||| Divides a Fin by 2, rounding down
472 | ||| `half {n=10} 6 = 3`
473 | ||| `half {n=10} 5 = 2`
474 | ||| `half {n=10} 4 = 2`
475 | ||| `half {n=10} 3 = 1`
476 | ||| `half {n=10} 2 = 1`
477 | ||| `half {n=10} 1 = 0`
484 | ||| Computes the midway index between two bounds
492 | -- ||| There is a similar function in Data.Fin.Arith, which has the smallest
493 | -- ||| possible bound. This one does not, but has a simpler type signature.
494 | -- public export
495 | -- multFin : {m, n : Nat} -> Fin m -> Fin n -> Fin (m * n)
496 | -- multFin {n = (S _)} FZ y = FZ
497 | -- multFin {n = (S _)} (FS x) y = FinArith.(+) y (weaken (multFin x y))
510 | ||| Data structure storing a lower and upper bound during a search
517 | ||| Given a non-empty sorted vector `xs`, an element `x` and a lower and upper
518 | ||| bound, it finds the "right bin", i.e. the index of the smallest element
519 | ||| between the bounds that's bigger than `x`
520 | ||| If `x` is bigger than the largest element, returns `Nothing`
521 | ||| `findBinBetween [2,7,10] 1 (MkRange 0 2) = Just 0`
522 | ||| `findBinBetween [2,7,10] 3 (MkRange 0 2) = Just 1`
523 | ||| `findBinBetween [2,7,10] 9 (MkRange 0 2) = Just 2`
524 | ||| `findBinBetween [2,7,10] 7 (MkRange 0 2) = Just 2`
525 | ||| `findbinbetween [2,7,15] 7 (MkRange 0 2) = Nothing`
526 | ||| `findBinBetween [1,2,3,4,5] 6 (MkRange 0 4) = Nothing`
527 | ||| Done using binary search
566 | ||| Todo can this eventually be generalised to non-cubical tensors?
567 | ||| Given a non-empty sorted vector `xs` and an element `x` it finds the
568 | ||| "right bin", i.e. the index of the smallest element that's bigger than `x`
569 | ||| If `x` is bigger than the highest element, returns `Nothing`
570 | ||| `findBin [2,7,10] 1 = Just 0`
571 | ||| `findBin [2,7,10] 3 = Just 1`
572 | ||| `findBin [2,4,6,8] 7 = Just 3`
580 | -- t : Double -> Type
581 | -- t 4 = Double
582 | -- t _ = String
583 | --
584 | -- th : (x : Double ** t x)
585 | -- th = (4 ** 5)
586 | --
587 | -- thh : (x : Double) -> Show (t x)
588 | -- thh x = ?thh_rhs
615 | -- Probably there's a faster way to do this
616 | -- public export
617 | -- {n : Nat} -> Random a => Random (Vect n a) where
618 | -- randomIO = sequence $ replicate n randomIO
619 | -- randomRIO (lo, hi) = sequence $ zipWith (\l, h => randomRIO (l, h)) lo hi
646 | ||| Cnvert an all to a vector if it's made out of replicated things
659 | ||| Dependent parametric traverse
677 | -- ||| Duplicate of `index` from Data.Vect.Quantifiers.All, but with an
678 | -- ||| additional `public` export modifier
688 | where
714 | {-
716 | interface Comult (f : Type -> Type) a where
717 | comult : f a -> f (f a)
719 | {shape : Vect n Nat} -> Num a => Comult (TensorA shape) a where
720 | comult t = ?eir
722 | gg : TensorA [3] Double -> TensorA [3, 3] Double
723 | gg (TS xs) = TS $ map ?fn ?gg_rhs_0
725 | -- [1, 2, 3]
726 | -- can we even do outer product?
727 | -- we wouldn't need reduce, but something like multiply?
728 | outer : {f : Type -> Type} -> {a : Type}
729 | -> (Num a, Applicative f, Algebra f a)
730 | => f a -> f a -> f (f a)
731 | outer xs ys = let t = liftA2 xs ys
732 | in ?outer_rhs
734 | -}
736 | |||| filter' works without `with`?
742 | ||| filter'' implemented with `with`
748 | {-
749 | Prelude.absurd : Uninhabited t => t -> a
750 | believe_me : a -> b
751 | -}
761 | -- Should this be detected as `using` the variable `n`?
762 | -- in pattern matching, we'd have to unify type of `xs` which has in itself `len`
763 | -- and `n` which in this case is computed to be `S len`?
764 | -- this step of `ll2` is decomposing `n` only one level down, but the entire recursion ends up using the entire `n`
783 | -- public export
784 | -- filter : (elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
785 | -- filter p [] = ( _ ** [] )
786 | -- filter p (x::xs) =
787 | -- let (_ ** tail) = filter p xs
788 | -- in if p x then
789 | -- (_ ** x::tail)
790 | -- else
791 | -- (_ ** tail)
797 | -- ||| Splits xs at each occurence of delimeter (general version for lists)
798 | -- public export
799 | -- splitList : Eq a =>
800 | -- (xs : List a) -> (delimeter : List a) -> (n : Nat ** Vect n (List a))
801 | -- splitList xs delimeter =
802 | -- if delimeter == []
803 | -- then (1 ** [xs]) -- Empty delimiter returns original list
804 | -- else case isInfixOfList delimeter xs of
805 | -- False => (1 ** [xs]) -- Delimiter not found, return original list
806 | -- True =>
807 | -- let (before, after) = breakOnList delimeter xs
808 | -- in case after of
809 | -- [] => (1 ** [before]) -- No more occurrences
810 | -- _ => let (restCount ** restVect) = splitList (drop (length delimeter) after) delimeter
811 | -- in (S restCount ** before :: restVect)
812 | -- where
813 | -- -- Check if list starts with delimiter
814 | -- isPrefixOfList : List a -> List a -> Bool
815 | -- isPrefixOfList [] _ = True
816 | -- isPrefixOfList _ [] = False
817 | -- isPrefixOfList (d :: ds) (x :: xs) = d == x && isPrefixOfList ds xs
818 | --
819 | -- -- Check if delimiter occurs anywhere in the list
820 | -- isInfixOfList : List a -> List a -> Bool
821 | -- isInfixOfList del [] = del == []
822 | -- isInfixOfList del xs@(_ :: xs') =
823 | -- isPrefixOfList del xs || isInfixOfList del xs'
824 | --
825 | -- -- Break list at first occurrence of delimiter
826 | -- breakOnList : List a -> List a -> (List a, List a)
827 | -- breakOnList del xs = breakOnListAcc del xs []
828 | -- where
829 | -- breakOnListAcc : List a -> List a -> List a -> (List a, List a)
830 | -- breakOnListAcc del remaining acc =
831 | -- case isPrefixOfList del remaining of
832 | -- True => (reverse acc, remaining)
833 | -- False => case remaining of
834 | -- [] => (reverse acc, [])
835 | -- (c :: cs) => breakOnListAcc del cs (c :: acc)
836 | --
837 | -- ||| Splits xs at each occurence of delimeter (string version)
838 | -- public export
839 | -- splitString : (xs : String) -> (delimeter : String) -> (n : Nat ** Vect n String)
840 | -- splitString xs delimeter =
841 | -- let (n ** result) = splitList (unpack xs) (unpack delimeter)
842 | -- in (n ** pack <$> result)
843 | --
844 | -- ||| Simple string replacement function
845 | -- public export
846 | -- replaceString : String -> String -> String -> String
847 | -- replaceString old new str =
848 | -- let chars = unpack str
849 | -- oldChars = unpack old
850 | -- newChars = unpack new
851 | -- in pack (replaceInList oldChars newChars chars)
852 | -- where
853 | -- replaceInList : List Char -> List Char -> List Char -> List Char
854 | -- replaceInList [] _ xs = xs
855 | -- replaceInList old new [] = []
856 | -- replaceInList old new xs@(x :: rest) =
857 | -- if isPrefixOf old xs
858 | -- then new ++ replaceInList old new (drop (length old) xs)
859 | -- else x :: replaceInList old new rest