git.iko.soy/Idris-dev
on master help sign in
Clean up
8d63fcfhowtonotwin
libs/base/Data/Vect.idr+8−6
compare with master
unifiedsplit
@@ -457,14 +457,16 @@ delete = deleteBy (==)
457
457
458||| A tuple where the first element is a `Vect` of the `n` first elements and
458||| A tuple where the first element is a `Vect` of the `n` first elements and
459||| the second element is a `Vect` of the remaining elements of the original.
459||| the second element is a `Vect` of the remaining elements of the original.
460−||| It is equivalent to `(take n xs, drop n xs)`, but is more efficient.
460+||| It is equivalent to `(take n xs, drop n xs)` (`splitAtTakeDrop`),
461+||| but is more efficient.
462+|||
461||| @ n the index to split at
463||| @ n the index to split at
462−||| @ xs the Vect to split in two
464+||| @ xs the `Vect` to split in two
463splitAt : (n : Nat) -> (xs : Vect (n + m) elem) -> (Vect n elem, Vect m elem)
465splitAt : (n : Nat) -> (xs : Vect (n + m) elem) -> (Vect n elem, Vect m elem)
464splitAt Z xs = ([], xs)
466splitAt Z xs = ([], xs)
465−splitAt (S k) (x::xs) =
467+splitAt (S k) (x :: xs) =
466 let (tk, dr) = splitAt k xs
468 let (tk, dr) = splitAt k xs
467− in (x::tk, dr)
469+ in (x :: tk, dr)
468
470
469partition : (elem -> Bool) -> Vect len elem -> ((p ** Vect p elem), (q ** Vect q elem))
471partition : (elem -> Bool) -> Vect len elem -> ((p ** Vect p elem), (q ** Vect q elem))
470partition p [] = ((_ ** []), (_ ** []))
472partition p [] = ((_ ** []), (_ ** []))
@@ -547,8 +549,8 @@ implementation Monad (Vect len) where
547 m >>= f = diag (map f m)
549 m >>= f = diag (map f m)
548
550
549implementation Traversable (Vect n) where
551implementation Traversable (Vect n) where
550− traverse f [] = pure []
552+ traverse f [] = [| [] |]
551− traverse f (x::xs) = [| f x :: traverse f xs |]
553+ traverse f (x :: xs) = [| f x :: traverse f xs |]
552
554
553--------------------------------------------------------------------------------
555--------------------------------------------------------------------------------
554-- Show
556-- Show
libs/contrib/Control/Isomorphism/Vect.idr+14−5
@@ -31,6 +31,7 @@ splitPair {n} {m} = MkIso (splitAt n) (uncurry (++)) toFrom fromTo
31 toFrom (ns, ms) = trans (splitAtTakeDrop n (ns ++ ms)) $ pairify (takePrefix ns ms) (dropPrefix ns ms)
31 toFrom (ns, ms) = trans (splitAtTakeDrop n (ns ++ ms)) $ pairify (takePrefix ns ms) (dropPrefix ns ms)
32 fromTo xs = rewrite splitAtTakeDrop {m=m} n xs in takeDropConcat n xs
32 fromTo xs = rewrite splitAtTakeDrop {m=m} n xs in takeDropConcat n xs
33
33
34+||| An `Iso` based on `zip` and `unzip`.
34zipped : Iso (Vect n a, Vect n b) (Vect n (a, b))
35zipped : Iso (Vect n a, Vect n b) (Vect n (a, b))
35zipped = MkIso (uncurry zip) unzip toFrom (\(as, bs) => fromTo as bs)
36zipped = MkIso (uncurry zip) unzip toFrom (\(as, bs) => fromTo as bs)
36 where toFrom : {n : Nat} -> (xs : Vect n (a, b)) -> uncurry Vect.zip (unzip xs) = xs
37 where toFrom : {n : Nat} -> (xs : Vect n (a, b)) -> uncurry Vect.zip (unzip xs) = xs
@@ -41,6 +42,7 @@ zipped = MkIso (uncurry zip) unzip toFrom (\(as, bs) => fromTo as bs)
41 fromTo [] [] = Refl
42 fromTo [] [] = Refl
42 fromTo (a :: as) (b :: bs) = rewrite fromTo as bs in Refl
43 fromTo (a :: as) (b :: bs) = rewrite fromTo as bs in Refl
43
44
45+||| An `Iso` based on `zip3` and `unzip3`.
44zipped3 : Iso (Vect n a, Vect n b, Vect n c) (Vect n (a, b, c))
46zipped3 : Iso (Vect n a, Vect n b, Vect n c) (Vect n (a, b, c))
45zipped3 = MkIso (uncurrry zip3) unzip3 toFrom (\(as, bs, cs) => fromTo as bs cs)
47zipped3 = MkIso (uncurrry zip3) unzip3 toFrom (\(as, bs, cs) => fromTo as bs cs)
46 where uncurrry : (w -> x -> y -> z) -> ((w, x, y) -> z)
48 where uncurrry : (w -> x -> y -> z) -> ((w, x, y) -> z)
@@ -59,6 +61,7 @@ transposition {a} = MkIso transpose transpose prf prf
59 where prf : {i : Nat} -> {o : Nat} -> (xss : Vect o (Vect i a)) -> transpose (transpose xss) = xss
61 where prf : {i : Nat} -> {o : Nat} -> (xss : Vect o (Vect i a)) -> transpose (transpose xss) = xss
60 prf [] = vectMustBeNil $ transpose [| [] |]
62 prf [] = vectMustBeNil $ transpose [| [] |]
61 prf (xs :: xss) = rewrite transposeCons xs (transpose xss) in cong (prf xss)
63 prf (xs :: xss) = rewrite transposeCons xs (transpose xss) in cong (prf xss)
64+
62||| Split the `Vect` every `m` elements, making `n` `Vect m a`s.
65||| Split the `Vect` every `m` elements, making `n` `Vect m a`s.
63||| The result is rectangular and has the same order as the original.
66||| The result is rectangular and has the same order as the original.
64|||
67|||
@@ -97,6 +100,7 @@ rectangular = MkIso unconcat concat toFrom fromTo
97unindex : (Fin n -> a) -> Vect n a
100unindex : (Fin n -> a) -> Vect n a
98unindex {n = Z} _ = []
101unindex {n = Z} _ = []
99unindex {n = S k} f = f FZ :: unindex (f . FS)
102unindex {n = S k} f = f FZ :: unindex (f . FS)
103+
100||| Indexing into the table of outputs of `f` is like calling `f` itself.
104||| Indexing into the table of outputs of `f` is like calling `f` itself.
101indexUnindex : (i : Fin n) -> (f : Fin n -> a) -> index i (unindex f) = f i
105indexUnindex : (i : Fin n) -> (f : Fin n -> a) -> index i (unindex f) = f i
102indexUnindex FZ _ = Refl
106indexUnindex FZ _ = Refl
@@ -117,6 +121,8 @@ unindexIndex : (xs : Vect n a) -> unindex (\i => index i xs) = xs
117unindexIndex xs = unindexIndex' xs (\i => index i xs) (\i => Refl)
121unindexIndex xs = unindexIndex' xs (\i => index i xs) (\i => Refl)
118
122
119||| Given a function that computes an index in the input from the index in the output, produce a `Vect o` of elements from the input.
123||| Given a function that computes an index in the input from the index in the output, produce a `Vect o` of elements from the input.
124+|||
125+||| This is the map function of the functor `\i => Vect i a` from `\i, o => Fin o -> Fin i` to `\i, o => Vect i a -> Vect o a`.
120fromIndices : (Fin o -> Fin i) -> Vect i a -> Vect o a
126fromIndices : (Fin o -> Fin i) -> Vect i a -> Vect o a
121fromIndices f xs = unindex (flip index xs . f)
127fromIndices f xs = unindex (flip index xs . f)
122indexFromIndices : (f : Fin o -> Fin i) -> (xs : Vect i a) -> (n : Fin o) -> index n (fromIndices f xs) = index (f n) xs
128indexFromIndices : (f : Fin o -> Fin i) -> (xs : Vect i a) -> (n : Fin o) -> index n (fromIndices f xs) = index (f n) xs
@@ -126,22 +132,25 @@ fromIndicesFromIndices to from fromTo xs = unindexIndex' xs (\x => index (to x)
126 rewrite indexUnindex (to i) (\x' => index (from x') xs) in rewrite fromTo i in Refl
132 rewrite indexUnindex (to i) (\x' => index (from x') xs) in rewrite fromTo i in Refl
127
133
128||| Given a permutation of the indices, provide an `Iso` that can permute a `Vect n` the "same" way. More precisely,
134||| Given a permutation of the indices, provide an `Iso` that can permute a `Vect n` the "same" way. More precisely,
129−||| if the index `i` is sent to `j`, then the element at index `i` ends up at index `j` (`indexPermuted`).
135+||| if the index `i` is sent to `j`, then the element at index `i` ends up at index `j` (`indexPermuted`). An
136+||| `Iso (Fin n) (Fin n)` represents a permutation of the integers `[0, n)` because it ensures that no elements
137+||| are "lost" or "duplicated".
130|||
138|||
131||| Note this has the *opposite* behavior to `fromIndices`. This function is more "visceral"; it can be imagined
139||| Note this has the *opposite* behavior to `fromIndices`. This function is more "visceral"; it can be imagined
132−||| as shuffling a `Vect` in the same way `map (to permutation)` shuffles `unindex id`.
140+||| as shuffling a `Vect` in the same way `map (to permutation)` shuffles `range`. Or, in more categorical terms,
133−|||
141+||| `fromIndices` represents a contravariant functor from the category `\i, o => Fin i -> Fin o` to `\i, o => Vect i a -> Vect o a`,
134−||| An `Iso (Fin n) (Fin n)` represents a permutation of the integers `[0, n)`, because an `Iso` ensures that no elements are "lost" or "duplicated".
142+||| and `permuted` represents that functor restricted to isomorphisms and made covariant with `isoSym`.
135|||
143|||
136||| ```idris example
144||| ```idris example
137||| to (permuted (stimes 2 rotatedDown)) [1, 2, 3, 4, 5] == [3, 4, 5, 1, 2]
145||| to (permuted (stimes 2 rotatedDown)) [1, 2, 3, 4, 5] == [3, 4, 5, 1, 2]
146+||| to (permuted (swapped 3 0)) [1, 2, 3, 4, 5] == [4, 2, 3, 1, 5]
138||| ```
147||| ```
139|||
148|||
140||| @ permutation an `Iso` representing the transformation on the indices
149||| @ permutation an `Iso` representing the transformation on the indices
141permuted : (permutation : Iso (Fin n) (Fin n)) -> Iso (Vect n a) (Vect n a)
150permuted : (permutation : Iso (Fin n) (Fin n)) -> Iso (Vect n a) (Vect n a)
142−permuted (MkIso toI fromI toFromI fromToI) = MkIso (fromIndices fromI) (fromIndices toI) (fromIndicesFromIndices fromI toI toFromI) (fromIndicesFromIndices toI fromI fromToI)
143-- [to, from => f from, f to] is not a typo
151-- [to, from => f from, f to] is not a typo
144-- fromIndices needs a function outputIdx => inputIdx, so to "align" the "motion" of the Fins with the elements, to uses from and from uses to.
152-- fromIndices needs a function outputIdx => inputIdx, so to "align" the "motion" of the Fins with the elements, to uses from and from uses to.
153+permuted (MkIso toI fromI toFromI fromToI) = MkIso (fromIndices fromI) (fromIndices toI) (fromIndicesFromIndices fromI toI toFromI) (fromIndicesFromIndices toI fromI fromToI)
145permutedSym : (permutation : Iso (Fin n) (Fin n)) -> permuted (isoSym permutation) = isoSym (permuted permutation)
154permutedSym : (permutation : Iso (Fin n) (Fin n)) -> permuted (isoSym permutation) = isoSym (permuted permutation)
146permutedSym (MkIso to from toFrom fromTo) = Refl
155permutedSym (MkIso to from toFrom fromTo) = Refl
147indexPermuted : (permutation : Iso (Fin n) (Fin n)) -> (i : Fin n) -> (xs : Vect n a) -> index i xs = index (to permutation i) (to (permuted permutation) xs)
156indexPermuted : (permutation : Iso (Fin n) (Fin n)) -> (i : Fin n) -> (xs : Vect n a) -> index i xs = index (to permutation i) (to (permuted permutation) xs)
libs/prelude/Prelude/List.idr+5−3
@@ -677,15 +677,17 @@ split p xs =
677
677
678||| A tuple where the first element is a `List` of the `n` first elements and
678||| A tuple where the first element is a `List` of the `n` first elements and
679||| the second element is a `List` of the remaining elements of the original.
679||| the second element is a `List` of the remaining elements of the original.
680−||| It is equivalent to `(take n xs, drop n xs)`, but is more efficient.
680+||| It is equivalent to `(take n xs, drop n xs)` (`splitAtTakeDrop`),
681+||| but is more efficient.
682+|||
681||| @ n the index to split at
683||| @ n the index to split at
682||| @ xs the `List` to split in two
684||| @ xs the `List` to split in two
683splitAt : (n : Nat) -> (xs : List a) -> (List a, List a)
685splitAt : (n : Nat) -> (xs : List a) -> (List a, List a)
684splitAt Z xs = ([], xs)
686splitAt Z xs = ([], xs)
685splitAt (S k) [] = ([], [])
687splitAt (S k) [] = ([], [])
686−splitAt (S k) (x::xs) =
688+splitAt (S k) (x :: xs) =
687 let (tk, dr) = splitAt k xs
689 let (tk, dr) = splitAt k xs
688− in (x::tk, dr)
690+ in (x :: tk, dr)
689
691
690splitAtTakeDrop : (n : Nat) -> (xs : List a) -> splitAt n xs = (take n xs, drop n xs)
692splitAtTakeDrop : (n : Nat) -> (xs : List a) -> splitAt n xs = (take n xs, drop n xs)
691splitAtTakeDrop Z xs = Refl
693splitAtTakeDrop Z xs = Refl