git.iko.soy/Idris-dev
on master help sign in
Added SnocList view, and a test
commit8705d0f8ae808feca62199f8f04ba1eae940ddec authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 8 Apr 2016, 16:55 (11 years ago) parentc325e23
5 files changed+71
compare with master
unifiedsplit
idris.cabal+4 libs/base/Data/List/Views.idr+19 test/views001/expected+3 test/views001/run+4 test/views001/views001.idr+41
idris.cabal+4
@@ -812,6 +812,10 @@ Extra-source-files:
812812 test/unique003/*.idr
813813 test/unique003/expected
814814
815+ test/views001/run
816+ test/views001/*.idr
817+ test/views001/expected
818+
815819 test/docs001/run
816820 test/docs001/input
817821 test/docs001/*.idr
libs/base/Data/List/Views.idr+19
@@ -96,3 +96,22 @@ splitRec : (xs : List a) -> SplitRec xs
9696splitRec [] = SplitRecNil
9797splitRec (x :: xs) = accInd splitRecFix (x :: xs) (smallerAcc (x :: x :: xs) lteRefl)
9898
99+||| View for traversing a list backwards
100+public export
101+data SnocList : List a -> Type where
102+ Empty : SnocList []
103+ Snoc : SnocList xs -> SnocList (xs ++ [x])
104+
105+snocListHelp : SnocList xs -> (ys : List a) -> SnocList (xs ++ ys)
106+snocListHelp {xs} x [] = rewrite appendNilRightNeutral xs in x
107+snocListHelp {xs} x (y :: ys)
108+ = rewrite appendAssociative xs [y] ys in snocListHelp (Snoc x {x=y}) ys
109+
110+||| Covering function for the `SnocList` view
111+export
112+snocList : (xs : List a) -> SnocList xs
113+snocList xs = snocListHelp Empty xs
114+
115+
116+
117+
test/views001/expectednew file+3
@@ -0,0 +1,3 @@
1+Sorting list
2+[-97, -94, -93, -89, -88, -87, -78, -77, -75, -73, -73, -71, -70, -69, -68, -64, -63, -61, -61, -58, -54, -52, -50, -49, -48, -46, -45, -40, -39, -31, -31, -21, -19, -19, -18, -15, -14, -13, -12, -5, -5, -4, -4, -3, -1, 0, 2, 3, 7, 9, 11, 11, 14, 14, 14, 17, 18, 19, 21, 22, 23, 25, 25, 28, 30, 33, 35, 36, 40, 40, 44, 45, 45, 46, 48, 52, 53, 53, 55, 57, 60, 62, 64, 64, 69, 69, 72, 74, 76, 77, 78, 78, 78, 80, 83, 84, 84, 86, 98, 98]
3+[98, 98, 86, 84, 84, 83, 80, 78, 78, 78, 77, 76, 74, 72, 69, 69, 64, 64, 62, 60, 57, 55, 53, 53, 52, 48, 46, 45, 45, 44, 40, 40, 36, 35, 33, 30, 28, 25, 25, 23, 22, 21, 19, 18, 17, 14, 14, 14, 11, 11, 9, 7, 3, 2, 0, -1, -3, -4, -4, -5, -5, -12, -13, -14, -15, -18, -19, -19, -21, -31, -31, -39, -40, -45, -46, -48, -49, -50, -52, -54, -58, -61, -61, -63, -64, -68, -69, -70, -71, -73, -73, -75, -77, -78, -87, -88, -89, -93, -94, -97]
test/views001/runnew file+4
@@ -0,0 +1,4 @@
1+#!/usr/bin/env bash
2+${IDRIS:-idris} $@ views001.idr -o views001
3+./views001
4+rm -f views001 *.ibc
test/views001/views001.idrnew file+41
@@ -0,0 +1,41 @@
1+import Data.List.Views
2+
3+rev : List a -> List a
4+rev xs with (snocList xs)
5+ rev [] | Empty = []
6+ rev (ys ++ [x]) | (Snoc y) = x :: rev ys | y
7+
8+-- Show all the splits for all the recursive calls, to demonstrate they really
9+-- are split in half
10+showDivisions : (xs : List a) -> List (List a)
11+showDivisions xs with (splitRec xs)
12+ showDivisions [] | SplitRecNil = []
13+ showDivisions [x] | SplitRecOne = [[x]]
14+ showDivisions (ys ++ zs) | (SplitRecPair ysrec zsrec) =
15+ (ys ++ zs) :: showDivisions ys | ysrec ++ showDivisions zs | zsrec
16+
17+total
18+mergeSort : Ord a => List a -> List a
19+mergeSort xs with (splitRec xs)
20+ mergeSort [] | SplitRecNil = []
21+ mergeSort [x] | SplitRecOne = [x]
22+ mergeSort (ys ++ zs) | SplitRecPair ysrec zsrec
23+ = merge (mergeSort ys | ysrec)
24+ (mergeSort zs | zsrec)
25+
26+testList : Int -> Int -> List Int -> List Int
27+testList 0 seed acc = acc
28+testList x seed acc = testList (x - 1) (seed * 12345 + 789)
29+ ((seed `mod` 100) :: acc)
30+
31+myhead : List a -> a
32+myhead (x :: xs) = x
33+
34+main : IO ()
35+main = do let list = testList 100 12345 []
36+ putStrLn "Sorting list"
37+ let list' = mergeSort list
38+ printLn list'
39+ printLn (rev list')
40+
41+