7454bb2 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Clean up splitAt

7454bb2howtonotwin8 years ago

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

compare with master

unifiedsplit

@@ -464,9 +464,8 @@ delete = deleteBy (==)

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

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

466splitAt Z xs = ([], xs)

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

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

468− let (tk, dr) = splitAt k xs

469− in (x :: tk, dr)

468+ | (tk, dr) = (x :: tk, dr)

470

469

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

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

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

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

@@ -641,12 +640,10 @@ dropTakeTakeDrop (S n) m (_ :: xs) (_ :: ys) prf = dropTakeTakeDrop n m xs ys (v

641splitAtTakeDrop : (n : Nat) -> (xs : Vect (n + m) a) -> splitAt n xs = (take n xs, drop n xs)

640splitAtTakeDrop : (n : Nat) -> (xs : Vect (n + m) a) -> splitAt n xs = (take n xs, drop n xs)

642splitAtTakeDrop Z xs = Refl

641splitAtTakeDrop Z xs = Refl

643splitAtTakeDrop (S k) (x :: xs) with (splitAt k xs) proof p

642splitAtTakeDrop (S k) (x :: xs) with (splitAt k xs) proof p

644− | (tk, dr) =

645− let rec = sym $ trans p $ splitAtTakeDrop k xs

643+ | (tk, dr) = let prf = trans p (splitAtTakeDrop k xs)

646− tkp = cong {f=fst} rec

644+ in aux (cong {f=(x ::) . fst} prf) (cong {f=snd} prf)

647− drp = cong {f=snd} rec

645+ where aux : {a, b : Type} -> {w, x : a} -> {y, z : b} -> w = x -> y = z -> (w, y) = (x, z)

648− in replace {P = \tk' => (x :: tk', dr) = (x :: take k xs, drop k xs)} tkp $

646+ aux Refl Refl = Refl

649− replace {P = \dr' => (x :: take k xs, dr') = (x :: take k xs, drop k xs) } drp Refl

650

647

651zipWithIsLiftA2 : (f : a -> b -> c) -> (as : Vect n a) -> (bs : Vect n b) -> zipWith f as bs = [| f as bs |]

648zipWithIsLiftA2 : (f : a -> b -> c) -> (as : Vect n a) -> (bs : Vect n b) -> zipWith f as bs = [| f as bs |]

652zipWithIsLiftA2 _ [] [] = Refl

649zipWithIsLiftA2 _ [] [] = Refl

libs/contrib/Control/Isomorphism/Vect.idr+10−13

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

29 where pairify : q = w -> e = r -> (q, e) = (w, r)

30 pairify Refl Refl = Refl

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} n xs in takeDropConcat n xs

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

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

@@ -68,7 +68,8 @@ transposition {a} = MkIso transpose transpose prf prf

68||| This is the inverse of `concat`.

69unconcat : Vect (n * m) a -> Vect n (Vect m a)

70unconcat {n = Z} [] = []

71+unconcat {n = S k} {m} xs with (splitAt m xs)

71−unconcat {n = S k} {m} xs = let (xs', xss) = splitAt m xs in xs' :: unconcat xss

72+ | (xs', xss) = xs' :: unconcat xss

72||| An `Iso` based on `unconcat` and `concat`.

73||| An `Iso` based on `unconcat` and `concat`.

73|||

74|||

74||| ```idris example

75||| ```idris example

@@ -76,21 +77,17 @@ unconcat {n = S k} {m} xs = let (xs', xss) = splitAt m xs in xs' :: unconcat xss

76||| ```

77||| ```

77rectangular : Iso (Vect (n * m) a) (Vect n (Vect m a))

78rectangular : Iso (Vect (n * m) a) (Vect n (Vect m a))

78rectangular = MkIso unconcat concat toFrom fromTo

79rectangular = MkIso unconcat concat toFrom fromTo

79−-- TODO: Clean up after #4001 is fixed

80 where toFrom : (xss : Vect i (Vect o a)) -> unconcat (concat xss) = xss

81 toFrom {i = Z} [] = Refl

82− toFrom {i = S k} {o} (xs :: xss) with (splitAt o (xs ++ concat xss)) proof p

83− | (tk, dr) = let sATK = sym $ trans p $ splitAtTakeDrop o (xs ++ concat xss)

82+ toFrom {i = S i} {o} (xs :: xss) = rewrite splitAtTakeDrop o {m = i * o} (xs ++ concat xss) in

84− tkp = trans (sym $ takePrefix xs $ concat xss) $ cong {f=fst} sATK

83+ rewrite takePrefix xs (concat xss) in

85− drp = trans (sym $ toFrom xss) $ cong {f=unconcat} $ trans (sym $ dropPrefix xs $ concat xss) $ cong {f=snd} sATK

84+ rewrite dropPrefix xs (concat xss) in

86− in replace {P = \dr' => tk :: dr' = xs :: xss} drp $ replace {P = \tk' => tk' :: xss = xs :: xss} tkp Refl

85+ cong (toFrom xss)

87 fromTo : (xs : Vect (i * o) a) -> concat (unconcat xs) = xs

86 fromTo : (xs : Vect (i * o) a) -> concat (unconcat xs) = xs

88 fromTo {i = Z} [] = Refl

87 fromTo {i = Z} [] = Refl

89− fromTo {i = S k} {o} xs with (splitAt o xs) proof p

90− | (tk, dr) = let sATK = sym $ trans p $ splitAtTakeDrop o xs

88+ fromTo {i = S i} {o} xs = rewrite splitAtTakeDrop o {m = i * o} xs in

91− tkp = cong {f=fst} sATK

89+ rewrite fromTo {i} {o} (drop o xs) in

92− drp = trans (cong {f=snd} sATK) $ sym $ fromTo dr

93− in replace {P = \dr' => tk ++ dr' = xs} drp $ replace {P = \tk' => tk' ++ drop o xs = xs } tkp $ takeDropConcat o xs

90+ takeDropConcat o xs

95-- Not an Iso because (=) is not extensional, but it works in spirit

92-- Not an Iso because (=) is not extensional, but it works in spirit

96||| Go through all possible inputs and tabulate the outputs in a `Vect`.

93||| Go through all possible inputs and tabulate the outputs in a `Vect`.

libs/prelude/Prelude/List.idr+11−14

@@ -685,20 +685,8 @@ split p xs =

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

686splitAt Z xs = ([], xs)

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

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

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

689− let (tk, dr) = splitAt k xs

690− in (x :: tk, dr)

691−

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

693−splitAtTakeDrop Z xs = Refl

694−splitAtTakeDrop (S k) [] = Refl

695−splitAtTakeDrop (S k) (x::xs) with (splitAt k xs) proof p

696− | (tk, dr) =

689+ | (tk, dr) = (x :: tk, dr)

697− let rec = sym $ trans p $ splitAtTakeDrop k xs

698− tkp = cong {f=fst} rec

699− drp = cong {f=snd} rec

700− in replace {P = \tk' => (x::tk', dr) = (x::take k xs, drop k xs)} tkp $

701− replace {P = \dr' => (x::take k xs, dr') = (x::take k xs, drop k xs) } drp Refl

702

690

703||| The partition function takes a predicate a list and returns the pair of

691||| The partition function takes a predicate a list and returns the pair of

704||| lists of elements which do and do not satisfy the predicate, respectively;

692||| lists of elements which do and do not satisfy the predicate, respectively;

@@ -948,3 +936,12 @@ foldlAsFoldr f z t = foldr (flip (.) . flip f) id t z

948foldlMatchesFoldr : (f : b -> a -> b) -> (q : b) -> (xs : List a) -> foldl f q xs = foldlAsFoldr f q xs

936foldlMatchesFoldr : (f : b -> a -> b) -> (q : b) -> (xs : List a) -> foldl f q xs = foldlAsFoldr f q xs

949foldlMatchesFoldr f q [] = Refl

937foldlMatchesFoldr f q [] = Refl

950foldlMatchesFoldr f q (x :: xs) = foldlMatchesFoldr f (f q x) xs

938foldlMatchesFoldr f q (x :: xs) = foldlMatchesFoldr f (f q x) xs

939+

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

941+splitAtTakeDrop Z xs = Refl

942+splitAtTakeDrop (S k) [] = Refl

943+splitAtTakeDrop (S k) (x :: xs) with (splitAt k xs) proof p

944+ | (tk, dr) = let prf = trans p (splitAtTakeDrop k xs)

945+ in aux (cong {f=(x ::) . fst} prf) (cong {f=snd} prf)

946+ where aux : {a, b : Type} -> {w, x : a} -> {y, z : b} -> w = x -> y = z -> (w, y) = (x, z)

947+ aux Refl Refl = Refl