15 | %hide Builtin.infixr.(#)
16 | %hide Data.Vect.Quantifiers.All.index
19 | ||| IsNo is a type Idris can automatically synthesise, in contrast to
20 | ||| in contrast to `Not (x = y)`
25 | ||| Can this be simplified?
41 | ||| Proof of inequality yields IsNo
51 | ||| Definition of liftA2 in terms of (<*>)
56 | ||| Tensorial strength
61 | ||| Pointwise Num structure for Applicative functors
71 | ||| Implementation of Foldable for Vect that is denotationally equivalent to
72 | ||| one in Data.Vect, but which does not use `foldrImpl` and therefore
73 | ||| reduces in the typechecker
79 | ||| toList with a different foldable implementation
84 | ||| Drop the first i elements of a vector
85 | ||| Analogous to Data.Vect.drop, except the index is Fin n instead of Nat
92 | ||| Drop all the elements up and until the element `x` from a vector
119 | ||| If an element `i` is not in the singleton list `[j]`, then `j` is not in
120 | ||| the singleton list `[i]`
125 | ||| If an element `i` is in the singleton list `[j]`, then `j` is in the
126 | ||| singleton list `[i]`
131 | ||| This already exists in Data.Vect.Elem, but it is not marked with %hint
146 | ||| Pointwise Num structure for Applicative functors
153 | ||| Duplicate of utilities for Data.Vect in their Naperian form
155 | ||| Analogue of `(::)`
161 | -- dcons : x -> ((i : Fin k) -> i' i) -> ((i : Fin (S k)) -> i' (cons x i'))
171 | ||| All but the last element
176 | ||| Analogus to `Data.Vect.take`
187 | -- Because of the way foldr for Vect is implemented in Idris
188 | -- we have to use this approach below, otherwise allSuccThenProdSucc breaks
192 | -- prod [] = fromInteger 1
193 | -- prod (x :: xs) = x * prod xs
205 | ||| Dual to concat from Data.Vect
238 | ||| Like weakenN from Data.Fin, but where n is on the other side of +
243 | ||| Like weakenN, but with mutliplication
244 | ||| Like shiftMul, but without changing the value of the index
260 | ||| Variant of `shift` from Data.Fin, but with multiplication
261 | ||| Given an index i : Fin n, it recasts it as one where steps are stride sized
262 | ||| That is, returns stride * i : Fin (stride * n)
263 | ||| Implemented by recursing on i, adding stride each time
274 | ||| Analogous to strengthen from Data.Fin
275 | ||| Attempts to strengthen the bound on Fin (m + n) to Fin m
276 | ||| If it doesn't succeed, then returns the remainder in Fin n
284 | -- strengthenN {m = 0} x = Nothing
285 | -- strengthenN {m = (S k)} FZ = Just FZ
286 | -- strengthenN {m = (S k)} (FS x) with (strengthenN x)
287 | -- _ | Nothing = Nothing
288 | -- _ | (Just p) = Just $ FS p
289 | --= let t = strengthenN x
290 | -- in ?strengthenN_rhs_3
292 | -- strengthenN {n = 0} x = Just x
293 | -- strengthenN {m = 0} {n = (S k)} FZ = Nothing
294 | -- strengthenN {m = (S j)} {n = (S k)} FZ = Just FZ
295 | -- strengthenN {m} {n = (S k)} (FS x)
296 | -- = let t = strengthenN x
297 | -- v = Fin.FS
298 | -- in ?what -- strengthenN x
301 | -- restCount = indexCount is -- fpn = 13 : Fin (20)
302 | -- iCTest1 : indexCount {shape = [3, 4, 5]} [1, 2, 3] = 33
303 | -- iCTest1 = ?iCTest_rhs
305 | ||| Like finS, but without wrapping
306 | ||| finS' last = last
312 | --finS' {n = S _} x = case strengthen x of
313 | -- Nothing => x
314 | -- Just y => FS y
317 | ||| Adds two Fin n, and bounds the result
318 | ||| Meaning (93:Fin 5) + (4 : Fin 5) = 4
330 | ||| Divides a Fin by 2, rounding down
337 | ||| Computes the midway index between two bounds
345 | ||| Given a non-empty sorted vector `xs`, finds the "right bin", i.e. the index
346 | ||| of the smallest element between the bounds that `x` is not bigger than.
347 | ||| If `x` is bigger than the highest element, returns `Nothing`
348 | ||| `findBinBetween [2,7,10] 1 0 2 = Just 0`
349 | ||| `findBinBetween [2,7,10] 3 0 2 = Just 1`
350 | ||| `findBinBetween [2,7,10] 9 0 2 = Just 2`
351 | ||| `findBinBetween [2,7,10] 7 0 2 = Just 2`
352 | ||| `findBinBetween [1,2,3,4,5] 6 0 4 = Nothing`
369 | ||| Todo can this eventually be generalised to non-cubical tensors?
370 | ||| Given a non-empty sorted vector `xs`, finds the "right bin", i.e. the index
371 | ||| of the smallest element between the bounds that `x` is not bigger than.
372 | ||| If `x` is bigger than the highest element, returns `Nothing`
373 | ||| `findBin [2,7,10] 1 = Just 0`
374 | ||| `findBin [2,7,10] 3 = Just 1`
375 | ||| `findBin [2,4,6,8] 7 = Just 3`
385 | -- t : Double -> Type
386 | -- t 4 = Double
387 | -- t _ = String
388 | --
389 | -- th : (x : Double ** t x)
390 | -- th = (4 ** 5)
391 | --
392 | -- thh : (x : Double) -> Show (t x)
393 | -- thh x = ?thh_rhs
403 | ||| Interface describing how a type can be displayed as a 2d grid of characters
408 | -- ||| Any type that implements Display can be shown as a string
409 | -- public export
410 | -- {a : Type} -> Display a => Show a where
411 | -- show x = let (h ** w ** xs) = display x
412 | -- ss = toList (intersperse "\n" (pack . toList <$> xs)) -- add intercalate here, and newline
413 | -- in fastUnlines ss
415 | -- public export
416 | -- Display Char where
417 | -- display x = (1 ** 1 ** [[x]])
419 | -- public export
420 | -- Num Unit where
421 | -- fromInteger _ = ()
422 | -- () * () = ()
423 | -- () + () = ()
439 | -- Probably there's a faster way to do this
440 | -- public export
441 | -- {n : Nat} -> Random a => Random (Vect n a) where
442 | -- randomIO = sequence $ replicate n randomIO
443 | -- randomRIO (lo, hi) = sequence $ zipWith (\l, h => randomRIO (l, h)) lo hi
458 | -- for reshaping a tensor
463 | -- -> Data.Fin.Arith.(*) (Fin (S x)) (Fin (S y))
466 | ||| There is a similar function in Data.Fin.Arith, which has the smallest
467 | ||| possible bound. This one does not, but has a simpler type signature.
473 | ||| Splits xs at each occurence of delimeter (general version for lists)
488 | where
489 | -- Check if list starts with delimiter
495 | -- Check if delimiter occurs anywhere in the list
501 | -- Break list at first occurrence of delimiter
504 | where
513 | ||| Splits xs at each occurence of delimeter (string version)
520 | ||| Simple string replacement function
528 | where
581 | ||| Cnvert an all to a vector if it's made out of replicated things
594 | ||| Dependent parametric traverse
627 | ||| Graph of a dependent function
634 | ||| Version of `map` for dependent function
635 | ||| Note that here `x : a` is identity in some sense, it comes from `f a`
643 | -- ||| Duplicate of `index` from Data.Vect.Quantifiers.All, but with an
644 | -- ||| additional `public` export modifier
651 | {-
653 | interface Comult (f : Type -> Type) a where
654 | comult : f a -> f (f a)
656 | {shape : Vect n Nat} -> Num a => Comult (TensorA shape) a where
657 | comult t = ?eir
659 | gg : TensorA [3] Double -> TensorA [3, 3] Double
660 | gg (TS xs) = TS $ map ?fn ?gg_rhs_0
662 | -- [1, 2, 3]
663 | -- can we even do outer product?
664 | -- we wouldn't need reduce, but something like multiply?
665 | outer : {f : Type -> Type} -> {a : Type}
666 | -> (Num a, Applicative f, Algebra f a)
667 | => f a -> f a -> f (f a)
668 | outer xs ys = let t = liftA2 xs ys
669 | in ?outer_rhs
671 | -}
673 | |||| filter' works without `with`?
679 | ||| filter'' implemented with `with`
685 | {-
686 | Prelude.absurd : Uninhabited t => t -> a
687 | believe_me : a -> b
689 | -}
699 | -- Should this be detected as `using` the variable `n`?
700 | -- in pattern matching, we'd have to unify type of `xs` which has in itself `len`
701 | -- and `n` which in this case is computed to be `S len`?
702 | -- this step of `ll2` is decomposing `n` only one level down, but the entire recursion ends up using the entire `n`