8d63fcf · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Clean up

commit8d63fcfa749591c42dcb915096147312d2c1453c authorhowtonotwin <rasheeqhere@gmail.com> dateWed 4 Jul 2018, 23:55 (8 years ago) parent9aa0517

3 files changed+27−14

compare with master

unifiedsplit

libs/base/Data/Vect.idr+8−6 libs/contrib/Control/Isomorphism/Vect.idr+14−5 libs/prelude/Prelude/List.idr+5−3

libs/base/Data/Vect.idr+8−6

@@ -457,14 +457,16 @@ delete = deleteBy (==)

457457

458458||| A tuple where the first element is a `Vect` of the `n` first elements and

459459||| 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+|||

461463||| @ n the index to split at

462−||| @ xs the Vect to split in two

464+||| @ xs the `Vect` to split in two

463465splitAt : (n : Nat) -> (xs : Vect (n + m) elem) -> (Vect n elem, Vect m elem)

464466splitAt Z xs = ([], xs)

465−splitAt (S k) (x::xs) =

467+splitAt (S k) (x :: xs) =

466468 let (tk, dr) = splitAt k xs

467− in (x::tk, dr)

469+ in (x :: tk, dr)

468470

469471partition : (elem -> Bool) -> Vect len elem -> ((p ** Vect p elem), (q ** Vect q elem))

470472partition p [] = ((_ ** []), (_ ** []))

@@ -547,8 +549,8 @@ implementation Monad (Vect len) where

547549 m >>= f = diag (map f m)

548550

549551implementation Traversable (Vect n) where

550− traverse f [] = pure []

551− traverse f (x::xs) = [| f x :: traverse f xs |]

552+ traverse f [] = [| [] |]

553+ traverse f (x :: xs) = [| f x :: traverse f xs |]

552554

553555--------------------------------------------------------------------------------

554556-- Show

libs/contrib/Control/Isomorphism/Vect.idr+14−5

@@ -31,6 +31,7 @@ splitPair {n} {m} = MkIso (splitAt n) (uncurry (++)) toFrom fromTo

3131 toFrom (ns, ms) = trans (splitAtTakeDrop n (ns ++ ms)) $ pairify (takePrefix ns ms) (dropPrefix ns ms)

3232 fromTo xs = rewrite splitAtTakeDrop {m=m} n xs in takeDropConcat n xs

3333

34+||| An `Iso` based on `zip` and `unzip`.

3435zipped : Iso (Vect n a, Vect n b) (Vect n (a, b))

3536zipped = MkIso (uncurry zip) unzip toFrom (\(as, bs) => fromTo as bs)

3637 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)

4142 fromTo [] [] = Refl

4243 fromTo (a :: as) (b :: bs) = rewrite fromTo as bs in Refl

4344

45+||| An `Iso` based on `zip3` and `unzip3`.

4446zipped3 : Iso (Vect n a, Vect n b, Vect n c) (Vect n (a, b, c))

4547zipped3 = MkIso (uncurrry zip3) unzip3 toFrom (\(as, bs, cs) => fromTo as bs cs)

4648 where uncurrry : (w -> x -> y -> z) -> ((w, x, y) -> z)

@@ -59,6 +61,7 @@ transposition {a} = MkIso transpose transpose prf prf

5961 where prf : {i : Nat} -> {o : Nat} -> (xss : Vect o (Vect i a)) -> transpose (transpose xss) = xss

6062 prf [] = vectMustBeNil $ transpose [| [] |]

6163 prf (xs :: xss) = rewrite transposeCons xs (transpose xss) in cong (prf xss)

64+

6265||| Split the `Vect` every `m` elements, making `n` `Vect m a`s.

6366||| The result is rectangular and has the same order as the original.

6467|||

@@ -97,6 +100,7 @@ rectangular = MkIso unconcat concat toFrom fromTo

97100unindex : (Fin n -> a) -> Vect n a

98101unindex {n = Z} _ = []

99102unindex {n = S k} f = f FZ :: unindex (f . FS)

103+

100104||| Indexing into the table of outputs of `f` is like calling `f` itself.

101105indexUnindex : (i : Fin n) -> (f : Fin n -> a) -> index i (unindex f) = f i

102106indexUnindex FZ _ = Refl

@@ -117,6 +121,8 @@ unindexIndex : (xs : Vect n a) -> unindex (\i => index i xs) = xs

117121unindexIndex xs = unindexIndex' xs (\i => index i xs) (\i => Refl)

118122

119123||| 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`.

120126fromIndices : (Fin o -> Fin i) -> Vect i a -> Vect o a

121127fromIndices f xs = unindex (flip index xs . f)

122128indexFromIndices : (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)

126132 rewrite indexUnindex (to i) (\x' => index (from x') xs) in rewrite fromTo i in Refl

127133

128134||| 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".

130138|||

131139||| 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`.

133−|||

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".

140+||| as shuffling a `Vect` in the same way `map (to permutation)` shuffles `range`. Or, in more categorical terms,

141+||| `fromIndices` represents a contravariant functor from the category `\i, o => Fin i -> Fin o` to `\i, o => Vect i a -> Vect o a`,

142+||| and `permuted` represents that functor restricted to isomorphisms and made covariant with `isoSym`.

135143|||

136144||| ```idris example

137145||| 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]

138147||| ```

139148|||

140149||| @ permutation an `Iso` representing the transformation on the indices

141150permuted : (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)

143151-- [to, from => f from, f to] is not a typo

144152-- 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)

145154permutedSym : (permutation : Iso (Fin n) (Fin n)) -> permuted (isoSym permutation) = isoSym (permuted permutation)

146155permutedSym (MkIso to from toFrom fromTo) = Refl

147156indexPermuted : (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 =

677677

678678||| A tuple where the first element is a `List` of the `n` first elements and

679679||| 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+|||

681683||| @ n the index to split at

682684||| @ xs the `List` to split in two

683685splitAt : (n : Nat) -> (xs : List a) -> (List a, List a)

684686splitAt Z xs = ([], xs)

685687splitAt (S k) [] = ([], [])

686−splitAt (S k) (x::xs) =

688+splitAt (S k) (x :: xs) =

687689 let (tk, dr) = splitAt k xs

688− in (x::tk, dr)

690+ in (x :: tk, dr)

689691

690692splitAtTakeDrop : (n : Nat) -> (xs : List a) -> splitAt n xs = (take n xs, drop n xs)

691693splitAtTakeDrop Z xs = Refl