git.iko.soy/Idris-dev
on master help sign in
Reverse improvements (#4310)
5102e48Boyd Stephen Smith Jr
libs/contrib/Data/List/Extra.idrnew file+44
compare with master
unifiedsplit
@@ -0,0 +1,44 @@
1+module Data.List.Extra
2+
3+%default total
4+%access export
5+
6+||| Serves as a specification for reverseOnto.
7+reverseOntoSpec : (xs, ys : List a) -> reverseOnto xs ys = reverse ys ++ xs
8+reverseOntoSpec _ [] = Refl
9+reverseOntoSpec xs (y::ys) =
10+ trans (reverseOntoSpec (y::xs) ys)
11+ (trans (appendAssociative (reverse ys) [y] xs)
12+ (cong {f = \l => l ++ xs} (sym (reverseOntoSpec [y] ys))))
13+
14+||| The reverse of an empty list is an empty list. Together with reverseCons,
15+||| serves as a specification for reverse.
16+reverseNil : reverse [] = []
17+reverseNil = Refl
18+
19+||| The reverse of a cons is the reverse of the tail followed by the head.
20+||| Together with reverseNil serves as a specification for reverse.
21+reverseCons : (x : a) -> (xs : List a) -> reverse (x::xs) = reverse xs ++ [x]
22+reverseCons x xs = reverseOntoSpec [x] xs
23+
24+||| Reversing an append is appending reversals backwards.
25+reverseAppend : (xs, ys : List a) ->
26+ reverse (xs ++ ys) = reverse ys ++ reverse xs
27+reverseAppend [] ys = sym (appendNilRightNeutral (reverse ys))
28+reverseAppend (x :: xs) ys =
29+ trans (trans (reverseCons x (xs ++ ys))
30+ (cong {f = \l => l ++ [x]} (reverseAppend xs ys)))
31+ (sym (trans (cong (reverseCons x xs))
32+ (appendAssociative (reverse ys) (reverse xs) [x])))
33+
34+||| Reversing a singleton list is a no-op.
35+reverseSingletonId : (x : a) -> reverse [x] = [x]
36+reverseSingletonId _ = Refl
37+
38+||| Reversing a reverse gives the original.
39+reverseReverseId : (xs : List a) -> reverse (reverse xs) = xs
40+reverseReverseId [] = Refl
41+reverseReverseId (x :: xs) =
42+ trans (cong (reverseCons x xs))
43+ (trans (reverseAppend (reverse xs) [x])
44+ (cong (reverseReverseId xs)))
libs/contrib/contrib.ipkg+1
@@ -36,6 +36,7 @@ modules = CFFI
36 , Data.Heap
36 , Data.Heap
37 , Data.IOArray
37 , Data.IOArray
38 , Data.List.Zipper
38 , Data.List.Zipper
39+ , Data.List.Extra
39
40
40 , Data.Matrix
41 , Data.Matrix
41 , Data.Matrix.Algebraic
42 , Data.Matrix.Algebraic
libs/prelude/Prelude/List.idr+6−5
@@ -394,13 +394,14 @@ scanl1 f (x::xs) = scanl f x xs
394-- Transformations
394-- Transformations
395--------------------------------------------------------------------------------
395--------------------------------------------------------------------------------
396
396
397+||| Reverse a list onto an existing tail.
398+reverseOnto : List a -> List a -> List a
399+reverseOnto acc [] = acc
400+reverseOnto acc (x::xs) = reverseOnto (x::acc) xs
401+
397||| Return the elements of a list in reverse order.
402||| Return the elements of a list in reverse order.
398reverse : List a -> List a
403reverse : List a -> List a
399−reverse = reverse' []
404+reverse = reverseOnto []
400− where
401− reverse' : List a -> List a -> List a
402− reverse' acc [] = acc
403− reverse' acc (x::xs) = reverse' (x::acc) xs
404
405
405||| Insert some separator between the elements of a list.
406||| Insert some separator between the elements of a list.
406|||
407|||