mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-17 16:21:46 +03:00
374 lines
13 KiB
Idris
374 lines
13 KiB
Idris
||| Contains:
|
|
|||
|
|
||| 1. Tail recursive versions of the list processing functions from
|
|
||| Data.List.
|
|
|||
|
|
||| 2. Extensional equality proofs that these variants are
|
|
||| (extensionally) equivalent to their non-tail-recursive
|
|
||| counterparts.
|
|
|||
|
|
||| Note:
|
|
|||
|
|
||| 1. Written in one sitting, feel free to refactor
|
|
|||
|
|
||| 2. The proofs below also work on non-publicly exported
|
|
||| definitions. This could be due to a bug, and will need to be
|
|
||| moved elsewhere if it's fixed.
|
|
module Data.List.TailRec
|
|
|
|
import Syntax.PreorderReasoning
|
|
import Syntax.WithProof
|
|
|
|
import Data.List
|
|
import Data.List1
|
|
import Data.Vect
|
|
import Data.Nat
|
|
|
|
total
|
|
lengthAcc : List a -> Nat -> Nat
|
|
lengthAcc [] acc = acc
|
|
lengthAcc (_::xs) acc = lengthAcc xs $ S acc
|
|
|
|
export total
|
|
length : List a -> Nat
|
|
length xs = lengthAcc xs Z
|
|
|
|
total
|
|
lengthAccSucc : (xs : List a) -> (n : Nat) -> lengthAcc xs (S n) = S (lengthAcc xs n)
|
|
lengthAccSucc [] _ = Refl
|
|
lengthAccSucc (_::xs) n = rewrite lengthAccSucc xs (S n) in cong S Refl
|
|
|
|
export total
|
|
length_ext : (xs : List a) -> List.length xs = Data.List.TailRec.length xs
|
|
length_ext [] = Refl
|
|
length_ext (_::xs) = rewrite length_ext xs in sym $ lengthAccSucc xs Z
|
|
|
|
take_aux : Nat -> List a -> List a -> List a
|
|
take_aux Z xs acc = reverseOnto [] acc
|
|
take_aux (S n) [] acc = reverseOnto [] acc
|
|
take_aux (S n) (x :: xs) acc = take_aux n xs (x :: acc)
|
|
|
|
export
|
|
take : Nat -> List a -> List a
|
|
take n xs = take_aux n xs []
|
|
|
|
export
|
|
take_ext :
|
|
(n : Nat) -> (xs : List a) ->
|
|
Data.List.take n xs = Data.List.TailRec.take n xs
|
|
take_ext n xs = Calc $
|
|
|~ Data.List.take n xs
|
|
~~ reverse [] ++ (Data.List.take n xs) ...( Refl )
|
|
~~ reverseOnto (Data.List.take n xs) [] ...( sym (revOnto (Data.List.take n xs) []) )
|
|
~~ take_aux n xs [] ...( sym (lemma n xs []) )
|
|
where
|
|
lemma : (n : Nat) -> (xs, acc : List a) ->
|
|
take_aux n xs acc = reverseOnto (Data.List.take n xs) acc
|
|
lemma Z xs acc = Refl
|
|
lemma (S n) [] acc = Refl
|
|
lemma (S n) (x::xs) acc = lemma n xs (x :: acc)
|
|
|
|
|
|
span_aux : (a -> Bool) -> List a -> List a -> (List a, List a)
|
|
span_aux p [] acc = (reverseOnto [] acc, [])
|
|
span_aux p (x::xs) acc =
|
|
if p x then
|
|
Data.List.TailRec.span_aux p xs (x :: acc)
|
|
else
|
|
(reverseOnto [] acc, x::xs)
|
|
|
|
export
|
|
span : (a -> Bool) -> List a -> (List a, List a)
|
|
span p xs = span_aux p xs []
|
|
|
|
coe : (f : (i : a) -> Type) -> i = i' -> f i -> f i'
|
|
coe f Refl x = x
|
|
|
|
span_aux_ext : (p : a -> Bool) -> (xs, acc : List a) ->
|
|
(reverseOnto (fst $ Data.List.span p xs) acc, snd $ Data.List.span p xs)
|
|
=
|
|
span_aux p xs acc
|
|
span_aux_ext p [] acc = Refl
|
|
-- This is disgusting. Please teach me a better way.
|
|
span_aux_ext p (x::xs) acc with (@@(p x), @@(Data.List.span p xs))
|
|
span_aux_ext p (x::xs) acc | ((True ** px_tru), ((pre, rest)**dl_pf)) =
|
|
rewrite px_tru in
|
|
rewrite dl_pf in
|
|
let u = span_aux_ext p xs (x::acc) in
|
|
coe (\u => (reverseOnto (x :: fst u) acc, snd u) =
|
|
Data.List.TailRec.span_aux p xs (x :: acc)) dl_pf u
|
|
span_aux_ext p (x::xs) acc | ((False**px_fls), ((pre,rest)**dl_pf)) =
|
|
rewrite px_fls in
|
|
Refl
|
|
|
|
export
|
|
span_ext : (p : a -> Bool) -> (xs : List a) ->
|
|
Data.List.span p xs = Data.List.TailRec.span p xs
|
|
span_ext p xs with (@@(Data.List.span p xs))
|
|
span_ext p xs | ((pre, rest) ** pf) =
|
|
rewrite pf in
|
|
let u = span_aux_ext p xs [] in
|
|
coe (\u => (fst u, snd u) = span_aux p xs []) pf u
|
|
|
|
export
|
|
break : (a -> Bool) -> List a -> (List a, List a)
|
|
break p xs = Data.List.TailRec.span (not . p) xs
|
|
|
|
export
|
|
break_ext : (p : a -> Bool) -> (xs : List a) ->
|
|
Data.List.break p xs = Data.List.TailRec.break p xs
|
|
break_ext p xs = span_ext (not . p) xs
|
|
|
|
splitOnto : List (List a) -> (a -> Bool) -> List a -> List1 (List a)
|
|
splitOnto acc p xs =
|
|
case Data.List.break p xs of
|
|
(chunk, [] ) => reverseOnto (chunk ::: []) acc
|
|
(chunk, (c::rest)) => splitOnto (chunk::acc) p rest
|
|
|
|
export
|
|
split : (a -> Bool) -> List a -> List1 (List a)
|
|
split p xs = splitOnto [] p xs
|
|
|
|
splitOnto_ext : (acc : List (List a)) -> (p : a -> Bool) -> (xs : List a) ->
|
|
reverseOnto (Data.List.split p xs) acc
|
|
= Data.List.TailRec.splitOnto acc p xs
|
|
splitOnto_ext acc p xs with (@@(Data.List.break p xs))
|
|
splitOnto_ext acc p xs | ((chunk, [] )**pf) =
|
|
rewrite pf in
|
|
Refl
|
|
splitOnto_ext acc p xs | ((chunk, c::rest)**pf) =
|
|
rewrite pf in
|
|
rewrite splitOnto_ext (chunk::acc) p rest in
|
|
Refl
|
|
|
|
export
|
|
split_ext : (p : a -> Bool) -> (xs : List a) ->
|
|
Data.List.split p xs = Data.List.TailRec.split p xs
|
|
split_ext p xs = splitOnto_ext [] p xs
|
|
|
|
|
|
splitAtOnto : List a -> (n : Nat) -> (xs : List a) -> (List a, List a)
|
|
splitAtOnto acc Z xs = (reverseOnto [] acc, xs)
|
|
splitAtOnto acc (S n) [] = (reverseOnto [] acc, [])
|
|
splitAtOnto acc (S n) (x::xs) = splitAtOnto (x::acc) n xs
|
|
|
|
export
|
|
splitAt : (n : Nat) -> (xs : List a) -> (List a, List a)
|
|
splitAt n xs = splitAtOnto [] n xs
|
|
|
|
splitAtOnto_ext : (acc : List a) -> (n : Nat) -> (xs : List a) ->
|
|
(reverseOnto (fst $ Data.List.splitAt n xs) acc, snd $ Data.List.splitAt n xs)
|
|
= splitAtOnto acc n xs
|
|
splitAtOnto_ext acc Z xs = Refl
|
|
splitAtOnto_ext acc (S n) [] = Refl
|
|
splitAtOnto_ext acc (S n) (x::xs) with (@@(Data.List.splitAt n xs))
|
|
splitAtOnto_ext acc (S n) (x::xs) | ((tk, dr)**pf) =
|
|
rewrite pf in
|
|
let u = splitAtOnto_ext (x::acc) n xs in
|
|
coe (\u => (reverseOnto (x :: fst u) acc, snd u) =
|
|
splitAtOnto (x :: acc) n xs) pf u
|
|
|
|
export
|
|
splitAt_ext : (n : Nat) -> (xs : List a) ->
|
|
Data.List.splitAt n xs =
|
|
Data.List.TailRec.splitAt n xs
|
|
splitAt_ext n xs with (@@(Data.List.splitAt n xs))
|
|
splitAt_ext n xs | ((tk, dr)**pf) =
|
|
rewrite pf in
|
|
rewrite sym $ splitAtOnto_ext [] n xs in
|
|
rewrite pf in
|
|
Refl
|
|
|
|
partitionOnto : List a -> List a -> (a -> Bool) -> List a -> (List a, List a)
|
|
partitionOnto lfts rgts p [] = (reverseOnto [] lfts, reverseOnto [] rgts)
|
|
partitionOnto lfts rgts p (x::xs) =
|
|
if p x then
|
|
partitionOnto (x :: lfts) rgts p xs
|
|
else
|
|
partitionOnto lfts (x::rgts) p xs
|
|
|
|
export
|
|
partition : (a -> Bool) -> List a -> (List a, List a)
|
|
partition p xs = partitionOnto [] [] p xs
|
|
|
|
partitionOnto_ext : (lfts, rgts : List a) -> (p : a -> Bool) -> (xs : List a) ->
|
|
(reverseOnto (fst $ Data.List.partition p xs) lfts
|
|
,reverseOnto (snd $ Data.List.partition p xs) rgts)
|
|
= Data.List.TailRec.partitionOnto lfts rgts p xs
|
|
partitionOnto_ext lfts rgts p [] = Refl
|
|
partitionOnto_ext lfts rgts p (x::xs) with (@@(p x), @@(Data.List.partition p xs))
|
|
partitionOnto_ext lfts rgts p (x::xs) | ((True **px_tru), ((dl_l, dl_r)**dl_pf))
|
|
= rewrite px_tru in
|
|
rewrite dl_pf in
|
|
rewrite px_tru in
|
|
let u = partitionOnto_ext (x :: lfts) rgts p xs in
|
|
coe (\u => (reverseOnto (x :: fst u) lfts
|
|
,reverseOnto ( snd u) rgts)
|
|
= partitionOnto (x :: lfts) rgts p xs) dl_pf u
|
|
|
|
partitionOnto_ext lfts rgts p (x::xs) | ((False**px_fls), ((dl_l, dl_r)**dl_pf))
|
|
= rewrite px_fls in
|
|
rewrite dl_pf in
|
|
rewrite px_fls in
|
|
let u = partitionOnto_ext lfts (x :: rgts) p xs in
|
|
coe (\u => (reverseOnto ( fst u) lfts
|
|
,reverseOnto (x :: snd u) rgts)
|
|
= partitionOnto lfts (x::rgts) p xs) dl_pf u
|
|
|
|
mergeReplicate_aux : a -> List a -> List a -> List a
|
|
mergeReplicate_aux sep [] acc = reverseOnto [] acc
|
|
mergeReplicate_aux sep (x::xs) acc = mergeReplicate_aux sep xs (x :: sep :: acc)
|
|
|
|
mergeReplicate_ext : (sep : a) -> (xs : List a) -> (acc : List a) ->
|
|
mergeReplicate_aux sep xs acc =
|
|
reverseOnto (mergeReplicate sep xs) acc
|
|
mergeReplicate_ext sep [] acc = Refl
|
|
mergeReplicate_ext sep (x::xs) acc = Calc $
|
|
|~ mergeReplicate_aux sep xs (x :: sep :: acc)
|
|
~~ reverseOnto (sep :: x :: mergeReplicate sep xs) acc
|
|
...( mergeReplicate_ext sep xs (x :: sep :: acc) )
|
|
|
|
export
|
|
intersperse : a -> List a -> List a
|
|
intersperse sep [] = []
|
|
intersperse sep (y::ys) = y :: mergeReplicate_aux sep ys []
|
|
|
|
export
|
|
intersperse_ext : (sep : a) -> (xs : List a) ->
|
|
Data.List.intersperse sep xs =
|
|
Data.List.TailRec.intersperse sep xs
|
|
intersperse_ext sep [] = Refl
|
|
intersperse_ext sep (y::ys) = cong (y::) (sym $ mergeReplicate_ext sep ys [])
|
|
|
|
mapMaybeOnto : List b -> (a -> Maybe b) -> List a -> List b
|
|
mapMaybeOnto acc f [] = reverseOnto [] acc
|
|
mapMaybeOnto acc f (x::xs) =
|
|
case f x of
|
|
Nothing => mapMaybeOnto acc f xs
|
|
Just y => mapMaybeOnto (y :: acc) f xs
|
|
|
|
export
|
|
mapMaybe : (a -> Maybe b) -> List a -> List b
|
|
mapMaybe f xs = mapMaybeOnto [] f xs
|
|
|
|
mapMaybeOnto_ext : (acc : List b) -> (f : a -> Maybe b) -> (xs : List a) ->
|
|
reverseOnto (Data.List.mapMaybe f xs) acc
|
|
=
|
|
mapMaybeOnto acc f xs
|
|
mapMaybeOnto_ext acc f [] = Refl
|
|
mapMaybeOnto_ext acc f (x::xs) with (f x)
|
|
mapMaybeOnto_ext acc f (x::xs) | Nothing = mapMaybeOnto_ext acc f xs
|
|
mapMaybeOnto_ext acc f (x::xs) | Just y = mapMaybeOnto_ext (y :: acc) f xs
|
|
|
|
export
|
|
mapMaybe_ext : (f : a -> Maybe b) -> (xs : List a) ->
|
|
Data.List.mapMaybe f xs = Data.List.TailRec.mapMaybe f xs
|
|
mapMaybe_ext f xs = mapMaybeOnto_ext [] f xs
|
|
|
|
export
|
|
sorted : Ord a => List a -> Bool
|
|
sorted [ ] = True
|
|
sorted [x] = True
|
|
sorted (x :: xs@(y :: ys)) = case (x <= y) of
|
|
False => False
|
|
True => Data.List.TailRec.sorted xs
|
|
|
|
export
|
|
sorted_ext : Ord a => (xs : List a) ->
|
|
Data.List.sorted xs = Data.List.TailRec.sorted xs
|
|
sorted_ext [] = Refl
|
|
sorted_ext [x] = Refl
|
|
sorted_ext (x :: y :: ys) with (x <= y)
|
|
sorted_ext (x :: y :: ys) | False = Refl
|
|
sorted_ext (x :: y :: ys) | True = sorted_ext (y::ys)
|
|
|
|
mergeByOnto : List a -> (a -> a -> Ordering) -> List a -> List a -> List a
|
|
mergeByOnto acc order [] right = reverseOnto right acc
|
|
mergeByOnto acc order left [] = reverseOnto left acc
|
|
mergeByOnto acc order left@(x::xs) right@(y::ys) =
|
|
-- We need the variant annotations (bug #300)
|
|
case order x y of
|
|
LT => mergeByOnto (x :: acc) order (assert_smaller left xs) right
|
|
_ => mergeByOnto (y :: acc) order left (assert_smaller right ys)
|
|
|
|
mergeByOnto_ext : (acc : List a)
|
|
-> (order : a -> a -> Ordering)
|
|
-> (left, right : List a)
|
|
-> reverseOnto (mergeBy order left right) acc
|
|
= mergeByOnto acc order left right
|
|
mergeByOnto_ext acc order [] right = Refl
|
|
mergeByOnto_ext acc order left [] with( left)
|
|
mergeByOnto_ext acc order _ [] | [] = Refl
|
|
mergeByOnto_ext acc order _ [] | (_::_) = Refl
|
|
mergeByOnto_ext acc order left@(x::xs) right@(y::ys) with (order x y)
|
|
mergeByOnto_ext acc order left@(x::xs) right@(y::ys) | LT =
|
|
mergeByOnto_ext (x :: acc) order xs (y::ys)
|
|
-- We need to exhaust the two other cases explicitly to convince the
|
|
-- typecheker. See #140
|
|
mergeByOnto_ext acc order left@(x::xs) right@(y::ys) | EQ =
|
|
mergeByOnto_ext (y :: acc) order (x::xs) ys
|
|
mergeByOnto_ext acc order left@(x::xs) right@(y::ys) | GT =
|
|
mergeByOnto_ext (y :: acc) order (x::xs) ys
|
|
|
|
export
|
|
mergeBy : (a -> a -> Ordering) -> List a -> List a -> List a
|
|
mergeBy order left right = mergeByOnto [] order left right
|
|
|
|
export
|
|
mergeBy_ext : (order : a -> a -> Ordering) -> (left, right : List a) ->
|
|
Data.List.mergeBy order left right =
|
|
Data.List.TailRec.mergeBy order left right
|
|
mergeBy_ext order left right = mergeByOnto_ext [] order left right
|
|
|
|
export
|
|
merge : Ord a => List a -> List a -> List a
|
|
merge = Data.List.TailRec.mergeBy compare
|
|
|
|
export
|
|
merge_ext : Ord a => (left, right : List a) ->
|
|
Data.List.merge left right = Data.List.TailRec.merge left right
|
|
merge_ext left right = mergeBy_ext compare left right
|
|
|
|
|
|
-- Not quite finished due to a bug.
|
|
|
|
sortBy_splitRec : List a -> List a -> (List a -> List a) -> (List a, List a)
|
|
sortBy_splitRec (_::_::xs) (y::ys) zs = sortBy_splitRec xs ys (zs . ((::) y))
|
|
sortBy_splitRec _ ys zs = (zs [], ys)
|
|
|
|
sortBy_split : List a -> (List a, List a)
|
|
sortBy_split xs = sortBy_splitRec xs xs id
|
|
|
|
export
|
|
sortBy : (cmp : a -> a -> Ordering) -> (xs : List a) -> List a
|
|
sortBy cmp [] = []
|
|
sortBy cmp [x] = [x]
|
|
sortBy cmp zs = let (xs, ys) = sortBy_split zs in
|
|
Data.List.TailRec.mergeBy cmp
|
|
(Data.List.TailRec.sortBy cmp (assert_smaller zs xs))
|
|
(Data.List.TailRec.sortBy cmp (assert_smaller zs ys))
|
|
|
|
|
|
{- Can't really finish this proof because Data.List doesn't export the definition of sortBy. -}
|
|
{-
|
|
export
|
|
sortBy_ext : (cmp : a -> a -> Ordering) -> (xs : List a) ->
|
|
Data.List.sortBy cmp xs = Data.List.TailRec.sortBy cmp xs
|
|
sortBy_ext cmp [] = Refl
|
|
sortBy_ext cmp [x] = Refl
|
|
sortBy_ext cmp zs'@(z::zs) =
|
|
Calc $
|
|
|~ Data.List.sortBy cmp (z::zs)
|
|
~~ (let (xs, ys) = sortBy_split zs' in
|
|
Data.List.mergeBy cmp
|
|
(Data.List.sortBy cmp xs)
|
|
(Data.List.sortBy cmp ys))
|
|
...( ?help0 )
|
|
~~
|
|
let (xs, ys) = sortBy_split (z::zs) in
|
|
Data.List.TailRec.mergeBy cmp
|
|
(Data.List.TailRec.sortBy cmp xs)
|
|
(Data.List.TailRec.sortBy cmp ys)
|
|
...( ?help1 )
|
|
-}
|