git.iko.soy/Idris-dev
on master help sign in
Make splitAt more efficient
4d69b3fhowtonotwin
libs/base/Data/Vect.idr+18−4
compare with master
unifiedsplit
@@ -321,6 +321,7 @@ foldr1 f (x::xs) = foldr f x xs
321||| Foldl without seeding the accumulator
321||| Foldl without seeding the accumulator
322foldl1 : (t -> t -> t) -> Vect (S n) t -> t
322foldl1 : (t -> t -> t) -> Vect (S n) t -> t
323foldl1 f (x::xs) = foldl f x xs
323foldl1 f (x::xs) = foldl f x xs
324+
324--------------------------------------------------------------------------------
325--------------------------------------------------------------------------------
325-- Scans
326-- Scans
326--------------------------------------------------------------------------------
327--------------------------------------------------------------------------------
@@ -455,13 +456,26 @@ delete = deleteBy (==)
455-- Splitting and breaking lists
456-- Splitting and breaking lists
456--------------------------------------------------------------------------------
457--------------------------------------------------------------------------------
457
458
458−||| A tuple where the first element is a Vect of the n first elements and
459+||| 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 Vect
460+||| the second element is a `Vect` of the remaining elements of the original.
460−||| It is equivalent to (take n xs, drop n xs)
461+||| It is equivalent to `(take n xs, drop n xs)`, but is more efficient.
461||| @ n the index to split at
462||| @ n the index to split at
462||| @ xs the Vect to split in two
463||| @ xs the Vect to split in two
463splitAt : (n : Nat) -> (xs : Vect (n + m) elem) -> (Vect n elem, Vect m elem)
464splitAt : (n : Nat) -> (xs : Vect (n + m) elem) -> (Vect n elem, Vect m elem)
465+splitAt Z xs = ([], xs)
466+splitAt (S k) (x::xs) =
467+ let (tk, dr) = splitAt k xs
468+ in (x::tk, dr)
469+
464−splitAt n xs = (take n xs, drop n xs)
470+splitAtTakeDrop : (n : Nat) -> (xs : Vect (n + m) a) -> splitAt n xs = (take n xs, drop n xs)
471+splitAtTakeDrop Z xs = Refl
472+splitAtTakeDrop (S k) (x::xs) with (splitAt k xs) proof p
473+ | (tk, dr) =
474+ let rec = sym $ trans p $ splitAtTakeDrop k xs
475+ tkp = cong {f=fst} rec
476+ drp = cong {f=snd} rec
477+ in replace {P = \tk' => (x::tk', dr) = (x::take k xs, drop k xs)} tkp $
478+ replace {P = \dr' => (x::take k xs, dr') = (x::take k xs, drop k xs) } drp Refl
465
479
466partition : (elem -> Bool) -> Vect len elem -> ((p ** Vect p elem), (q ** Vect q elem))
480partition : (elem -> Bool) -> Vect len elem -> ((p ** Vect p elem), (q ** Vect q elem))
467partition p [] = ((_ ** []), (_ ** []))
481partition p [] = ((_ ** []), (_ ** []))
libs/prelude/Prelude/List.idr+20−5
@@ -675,13 +675,28 @@ split p xs =
675 (chunk, []) => [chunk]
675 (chunk, []) => [chunk]
676 (chunk, (c :: rest)) => chunk :: split p (assert_smaller xs rest)
676 (chunk, (c :: rest)) => chunk :: split p (assert_smaller xs rest)
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 list
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)
680+||| It is equivalent to `(take n xs, drop n xs)`, but is more efficient.
681||| @ n the index to split at
681||| @ n the index to split at
682−||| @ xs the list to split in two
682+||| @ xs the `List` to split in two
683splitAt : (n : Nat) -> (xs : List a) -> (List a, List a)
683splitAt : (n : Nat) -> (xs : List a) -> (List a, List a)
684+splitAt Z xs = ([], xs)
685+splitAt (S k) [] = ([], [])
686+splitAt (S k) (x::xs) =
687+ let (tk, dr) = splitAt k xs
688+ in (x::tk, dr)
689+
684−splitAt n xs = (take n xs, drop n xs)
690+splitAtTakeDrop : (n : Nat) -> (xs : List a) -> splitAt n xs = (take n xs, drop n xs)
691+splitAtTakeDrop Z xs = Refl
692+splitAtTakeDrop (S k) [] = Refl
693+splitAtTakeDrop (S k) (x::xs) with (splitAt k xs) proof p
694+ | (tk, dr) =
695+ let rec = sym $ trans p $ splitAtTakeDrop k xs
696+ tkp = cong {f=fst} rec
697+ drp = cong {f=snd} rec
698+ in replace {P = \tk' => (x::tk', dr) = (x::take k xs, drop k xs)} tkp $
699+ replace {P = \dr' => (x::take k xs, dr') = (x::take k xs, drop k xs) } drp Refl
685
700
686||| The partition function takes a predicate a list and returns the pair of
701||| The partition function takes a predicate a list and returns the pair of
687||| lists of elements which do and do not satisfy the predicate, respectively;
702||| lists of elements which do and do not satisfy the predicate, respectively;