15 | %hide Builtin.infixr.(#)
16 | %hide Data.Vect.Quantifiers.All.index
18 | {-------------------------------------------------------------------------------
19 | {-------------------------------------------------------------------------------
20 | Various utilities necessary for TensorType, but that don't fit anywhere else
21 | Does not depend on any other file within this project.
23 | Some of these feel like they should be in the Idris standard library
25 | -------------------------------------------------------------------------------}
26 | -------------------------------------------------------------------------------}
50 | ||| Graph of a dependent function
57 | ||| Version of `map` for dependent function
58 | ||| Note that here `x : a` is identity in some sense, it comes from `f a`
67 | ||| The proof that a decidable property leads to a contradiction
68 | ||| `IsNo` is a type Idris can automatically synthesise, unlike `Not`
69 | ||| See example below
76 | failing
97 | ||| Proof of inequality yields IsNo
137 | ||| If an element `i` is not in the singleton list `[j]`, then `j` is not in
138 | ||| the singleton list `[i]`
143 | ||| If an element `i` is in the singleton list `[j]`, then `j` is in the
144 | ||| singleton list `[i]`
152 | ||| Definition of liftA2 in terms of (<*>)
157 | ||| Tensorial strength
162 | ||| Pointwise Num structure for Applicative functors
171 | ||| Implementation of Foldable for Vect that is denotationally equivalent to
172 | ||| one in Data.Vect, but which does not use `foldrImpl` and therefore
173 | ||| reduces in the typechecker
179 | ||| toList with a different foldable implementation
189 | ||| Duplicate of utilities for Data.Vect in their Naperian form
195 | -- Because of the way foldr for Vect is implemented in Idris
196 | -- we have to use this approach below, otherwise allSuccThenProdSucc breaks
200 | -- prod [] = fromInteger 1
201 | -- prod (x :: xs) = x * prod xs
223 | ||| Dual to concat from Data.Vect
230 | ||| Trim a specified trailing value
235 | ||| Combination of `cons` and `snoc`: adds an element in front, and at the end
240 | ||| Pad a vector with a specified element to exactly `targetSize`
249 | ||| Drop the first i elements of a vector
250 | ||| Analogous to Data.Vect.drop, except the index is Fin n instead of Nat
257 | ||| Drop all the elements up and until the element `x` from a vector
281 | ||| Map each element along with its zero-based position in the list.
285 | where
290 | ||| Split a list into consecutive chunks of size `n` (clamped to at least 1).
291 | ||| The final chunk may be shorter than `n`, this is why the length of the
292 | ||| list is needed as upper bound.
296 | where
316 | ||| Trim a specified trailing value
321 | ||| Combination of `cons` and `snoc`: adds an element in front, and at the end
326 | ||| Pad a list with a specified element to at least `targetSize`
332 | ||| Drop all the elements after the element `x` from a list
339 | ||| Analogue of `(::)`
345 | -- dcons : x -> ((i : Fin k) -> i' i) -> ((i : Fin (S k)) -> i' (cons x i'))
355 | ||| All but the last element
360 | ||| Analogus to `Data.Vect.take`
380 | ||| Proof that subtracting from a successor is the same as taking the sucessor
381 | ||| of the subtraction
389 | ||| A version of `weakenN` from Data.Fin with `n` on the other side of `+`
394 | ||| Variant of `weakenN` from `Data.Fin`, but for multiplication
395 | ||| Like shiftMul, but without changing the value of the index
411 | ||| Variant of `shift` from Data.Fin, but for multiplication
412 | ||| Given a stride and an index `i : Fin n`, it returns a stride-sized step
413 | ||| That is, it returns `stride * i` : Fin (stride * n)
414 | ||| Implemented by recursing on i, adding stride each time
424 | ||| Analogue of `strengthen` from Data.Fin
425 | ||| Attempts to strengthen the bound on Fin (m + n) to Fin m
426 | ||| If it doesn't succeed, then returns the remainder in Fin n
435 | ||| Analogue of `finS` from `Data.Fin`, but without without wrapping
436 | ||| That is, `finS' last = last`
442 | --finS' {n = S _} x = case strengthen x of
443 | -- Nothing => x
444 | -- Just y => FS y
453 | ||| This can be implemented using `Data.Fin.Order`, but it doesn't seem worth
454 | ||| the effort, as the typechecker ends up needing a lot of extra hand holding
463 | -- lastBiggerThanOthers {n = 0} FZ = FromNatPrf LTEZero
464 | -- lastBiggerThanOthers {n = (S k)} FZ = FromNatPrf LTEZero
465 | -- lastBiggerThanOthers {n = (S k)} (FS x) = FSFinLTE (lastBiggerThanOthers x)
467 | ||| Adds two bounded numbers, bounds the result
468 | ||| That is, `addFinsBounded {n=5} 3 4 = 4`
469 | ||| `assert_smaller` is only needed for totality checking
482 | ||| Divides a Fin by 2, rounding down
483 | ||| `half {n=10} 6 = 3`
484 | ||| `half {n=10} 5 = 2`
485 | ||| `half {n=10} 4 = 2`
486 | ||| `half {n=10} 3 = 1`
487 | ||| `half {n=10} 2 = 1`
488 | ||| `half {n=10} 1 = 0`
495 | ||| Computes the midway index between two bounds
503 | -- ||| There is a similar function in Data.Fin.Arith, which has the smallest
504 | -- ||| possible bound. This one does not, but has a simpler type signature.
505 | -- public export
506 | -- multFin : {m, n : Nat} -> Fin m -> Fin n -> Fin (m * n)
507 | -- multFin {n = (S _)} FZ y = FZ
508 | -- multFin {n = (S _)} (FS x) y = FinArith.(+) y (weaken (multFin x y))
521 | ||| Data structure storing a lower and upper bound during a search
528 | ||| Given a non-empty sorted vector `xs`, an element `x` and a lower and upper
529 | ||| bound, it finds the "right bin", i.e. the index of the smallest element
530 | ||| between the bounds that's bigger than `x`
531 | ||| If `x` is bigger than the largest element, returns `Nothing`
532 | ||| `findBinBetween [2,7,10] 1 (MkRange 0 2) = Just 0`
533 | ||| `findBinBetween [2,7,10] 3 (MkRange 0 2) = Just 1`
534 | ||| `findBinBetween [2,7,10] 9 (MkRange 0 2) = Just 2`
535 | ||| `findBinBetween [2,7,10] 7 (MkRange 0 2) = Just 2`
536 | ||| `findbinbetween [2,7,15] 7 (MkRange 0 2) = Nothing`
537 | ||| `findBinBetween [1,2,3,4,5] 6 (MkRange 0 4) = Nothing`
538 | ||| Done using binary search
577 | ||| Todo can this eventually be generalised to non-cubical tensors?
578 | ||| Given a non-empty sorted vector `xs` and an element `x` it finds the
579 | ||| "right bin", i.e. the index of the smallest element that's bigger than `x`
580 | ||| If `x` is bigger than the highest element, returns `Nothing`
581 | ||| `findBin [2,7,10] 1 = Just 0`
582 | ||| `findBin [2,7,10] 3 = Just 1`
583 | ||| `findBin [2,4,6,8] 7 = Just 3`
591 | -- t : Double -> Type
592 | -- t 4 = Double
593 | -- t _ = String
594 | --
595 | -- th : (x : Double ** t x)
596 | -- th = (4 ** 5)
597 | --
598 | -- thh : (x : Double) -> Show (t x)
599 | -- thh x = ?thh_rhs
634 | -- Probably there's a faster way to do this
635 | -- public export
636 | -- {n : Nat} -> Random a => Random (Vect n a) where
637 | -- randomIO = sequence $ replicate n randomIO
638 | -- randomRIO (lo, hi) = sequence $ zipWith (\l, h => randomRIO (l, h)) lo hi
665 | ||| Cnvert an all to a vector if it's made out of replicated things
678 | ||| Dependent parametric traverse
696 | -- ||| Duplicate of `index` from Data.Vect.Quantifiers.All, but with an
697 | -- ||| additional `public` export modifier
704 | {-
706 | interface Comult (f : Type -> Type) a where
707 | comult : f a -> f (f a)
709 | {shape : Vect n Nat} -> Num a => Comult (TensorA shape) a where
710 | comult t = ?eir
712 | gg : TensorA [3] Double -> TensorA [3, 3] Double
713 | gg (TS xs) = TS $ map ?fn ?gg_rhs_0
715 | -- [1, 2, 3]
716 | -- can we even do outer product?
717 | -- we wouldn't need reduce, but something like multiply?
718 | outer : {f : Type -> Type} -> {a : Type}
719 | -> (Num a, Applicative f, Algebra f a)
720 | => f a -> f a -> f (f a)
721 | outer xs ys = let t = liftA2 xs ys
722 | in ?outer_rhs
724 | -}
726 | |||| filter' works without `with`?
732 | ||| filter'' implemented with `with`
738 | {-
739 | Prelude.absurd : Uninhabited t => t -> a
740 | believe_me : a -> b
741 | -}
751 | -- Should this be detected as `using` the variable `n`?
752 | -- in pattern matching, we'd have to unify type of `xs` which has in itself `len`
753 | -- and `n` which in this case is computed to be `S len`?
754 | -- this step of `ll2` is decomposing `n` only one level down, but the entire recursion ends up using the entire `n`
773 | -- public export
774 | -- filter : (elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
775 | -- filter p [] = ( _ ** [] )
776 | -- filter p (x::xs) =
777 | -- let (_ ** tail) = filter p xs
778 | -- in if p x then
779 | -- (_ ** x::tail)
780 | -- else
781 | -- (_ ** tail)
787 | -- ||| Splits xs at each occurence of delimeter (general version for lists)
788 | -- public export
789 | -- splitList : Eq a =>
790 | -- (xs : List a) -> (delimeter : List a) -> (n : Nat ** Vect n (List a))
791 | -- splitList xs delimeter =
792 | -- if delimeter == []
793 | -- then (1 ** [xs]) -- Empty delimiter returns original list
794 | -- else case isInfixOfList delimeter xs of
795 | -- False => (1 ** [xs]) -- Delimiter not found, return original list
796 | -- True =>
797 | -- let (before, after) = breakOnList delimeter xs
798 | -- in case after of
799 | -- [] => (1 ** [before]) -- No more occurrences
800 | -- _ => let (restCount ** restVect) = splitList (drop (length delimeter) after) delimeter
801 | -- in (S restCount ** before :: restVect)
802 | -- where
803 | -- -- Check if list starts with delimiter
804 | -- isPrefixOfList : List a -> List a -> Bool
805 | -- isPrefixOfList [] _ = True
806 | -- isPrefixOfList _ [] = False
807 | -- isPrefixOfList (d :: ds) (x :: xs) = d == x && isPrefixOfList ds xs
808 | --
809 | -- -- Check if delimiter occurs anywhere in the list
810 | -- isInfixOfList : List a -> List a -> Bool
811 | -- isInfixOfList del [] = del == []
812 | -- isInfixOfList del xs@(_ :: xs') =
813 | -- isPrefixOfList del xs || isInfixOfList del xs'
814 | --
815 | -- -- Break list at first occurrence of delimiter
816 | -- breakOnList : List a -> List a -> (List a, List a)
817 | -- breakOnList del xs = breakOnListAcc del xs []
818 | -- where
819 | -- breakOnListAcc : List a -> List a -> List a -> (List a, List a)
820 | -- breakOnListAcc del remaining acc =
821 | -- case isPrefixOfList del remaining of
822 | -- True => (reverse acc, remaining)
823 | -- False => case remaining of
824 | -- [] => (reverse acc, [])
825 | -- (c :: cs) => breakOnListAcc del cs (c :: acc)
826 | --
827 | -- ||| Splits xs at each occurence of delimeter (string version)
828 | -- public export
829 | -- splitString : (xs : String) -> (delimeter : String) -> (n : Nat ** Vect n String)
830 | -- splitString xs delimeter =
831 | -- let (n ** result) = splitList (unpack xs) (unpack delimeter)
832 | -- in (n ** pack <$> result)
833 | --
834 | -- ||| Simple string replacement function
835 | -- public export
836 | -- replaceString : String -> String -> String -> String
837 | -- replaceString old new str =
838 | -- let chars = unpack str
839 | -- oldChars = unpack old
840 | -- newChars = unpack new
841 | -- in pack (replaceInList oldChars newChars chars)
842 | -- where
843 | -- replaceInList : List Char -> List Char -> List Char -> List Char
844 | -- replaceInList [] _ xs = xs
845 | -- replaceInList old new [] = []
846 | -- replaceInList old new xs@(x :: rest) =
847 | -- if isPrefixOf old xs
848 | -- then new ++ replaceInList old new (drop (length old) xs)
849 | -- else x :: replaceInList old new rest