git.iko.soy/Idris-dev
on master help sign in
Add Data.Vect.Views

With SnocVect, Split and SplitRec, also added to views001 test

commit7c5819b55de9233039d9f3fdba7ebf0631a64236 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 23 Apr 2016, 12:03 (11 years ago) parent1d0e33c
7 files changed+137−6
compare with master
unifiedsplit
libs/base/Data/List/Views.idr+4−4 libs/base/Data/Vect.idr+15 libs/base/Data/Vect/Views.idr+83 libs/base/base.ipkg+1−1 test/views001/expected+2 test/views001/run+3−1 test/views001/views001a.idr+29
libs/base/Data/List/Views.idr+4−4
@@ -82,7 +82,7 @@ public export
8282data SnocList : List a -> Type where
8383 Empty : SnocList []
8484 Snoc : {x : a} -> {xs : List a} -> -- Explicit, so don't erase
85− SnocList xs -> SnocList (xs ++ [x])
85+ (rec : SnocList xs) -> SnocList (xs ++ [x])
8686
8787snocListHelp : SnocList xs -> (ys : List a) -> SnocList (xs ++ ys)
8888snocListHelp {xs} x [] = rewrite appendNilRightNeutral xs in x
@@ -100,8 +100,8 @@ snocList xs = snocListHelp Empty xs
100100public export
101101data Filtered : (a -> a -> Bool) -> List a -> Type where
102102 FNil : Filtered p []
103− FRec : Lazy (Filtered p (filter (\y => p y x) xs)) ->
104− Lazy (Filtered p (filter (\y => not (p y x)) xs)) ->
103+ FRec : (lrec : Lazy (Filtered p (filter (\y => p y x) xs))) ->
104+ (rrec : Lazy (Filtered p (filter (\y => not (p y x)) xs))) ->
105105 Filtered p (x :: xs)
106106
107107filteredLOK : (p : a -> a -> Bool) -> (x : a) -> (xs : List a) -> smaller (filter (\y => p y x) xs) (x :: xs)
@@ -178,7 +178,7 @@ data VList : List a -> Type where
178178 VNil : VList []
179179 VOne : VList [x]
180180 VCons : {x : a} -> {y : a} -> {xs : List a} ->
181− VList xs -> VList (x :: xs ++ [y])
181+ (rec : VList xs) -> VList (x :: xs ++ [y])
182182
183183total
184184balRec : (zs, xs : List a) ->
libs/base/Data/Vect.idr+15
@@ -194,6 +194,21 @@ replicate : (n : Nat) -> (x : a) -> Vect n a
194194replicate Z x = []
195195replicate (S k) x = x :: replicate k x
196196
197+||| Merge two ordered vectors
198+mergeBy : (a -> a -> Ordering) -> Vect n a -> Vect m a -> Vect (n + m) a
199+mergeBy order [] [] = []
200+mergeBy order [] (x :: xs) = x :: xs
201+mergeBy {n = S k} order (x :: xs) [] = rewrite plusZeroRightNeutral (S k) in
202+ x :: xs
203+mergeBy {n = S k} {m = S k'} order (x :: xs) (y :: ys)
204+ = if order x y == LT
205+ then x :: mergeBy order xs (y :: ys)
206+ else rewrite sym (plusSuccRightSucc k k') in
207+ y :: mergeBy order (x :: xs) ys
208+
209+merge : Ord a => Vect n a -> Vect m a -> Vect (n + m) a
210+merge = mergeBy compare
211+
197212--------------------------------------------------------------------------------
198213-- Zips and unzips
199214--------------------------------------------------------------------------------
libs/base/Data/Vect/Views.idrnew file+83
@@ -0,0 +1,83 @@
1+module Data.Vect.Views
2+
3+import Data.Vect
4+
5+||| View for traversing a vector backwards
6+public export
7+data SnocVect : Vect n a -> Type where
8+ Empty : SnocVect []
9+ Snoc : {x : a} -> {xs : Vect n a} ->
10+ (rec : SnocVect xs) -> SnocVect (xs ++ [x])
11+
12+snocVectHelp : {xs : Vect n a} ->
13+ SnocVect xs -> (ys : Vect m a) -> SnocVect (xs ++ ys)
14+snocVectHelp {xs} x [] = rewrite vectNilRightNeutral xs in x
15+snocVectHelp {xs} x (y :: ys)
16+ = rewrite vectAppendAssociative xs [y] ys in
17+ snocVectHelp (Snoc x {x=y}) ys
18+
19+||| Covering function for the `SnocVect` view
20+||| Constructs the view in linear time
21+export
22+snocVect : (xs : Vect n a) -> SnocVect xs
23+snocVect xs = snocVectHelp Empty xs
24+
25+||| View for splitting a vector in half, non-recursively
26+public export
27+data Split : Vect n a -> Type where
28+ SplitNil : Split []
29+ SplitOne : Split [x]
30+ SplitPair : {x, y : a} -> {xs : Vect n a} -> {ys : Vect m a} ->
31+ Split (x :: xs ++ y :: ys)
32+
33+splitHelp : (head : a) ->
34+ (xs : Vect n a) ->
35+ (counter : Vect m a) -> Split (head :: xs)
36+splitHelp head [] counter = SplitOne
37+splitHelp head (x :: xs) [] = SplitPair {xs = []} {ys = xs}
38+splitHelp head (x :: xs) [y] = SplitPair {xs = []} {ys = xs}
39+splitHelp head (x :: xs) (_ :: _ :: ys)
40+ = case splitHelp head xs ys of
41+ SplitOne => SplitPair {xs = []} {ys = []}
42+ SplitPair {xs} {ys} => SplitPair {xs = x :: xs} {ys}
43+
44+||| Covering function for the `Split` view
45+||| Constructs the view in linear time
46+export
47+split : (xs : Vect n a) -> Split xs
48+split [] = SplitNil
49+split (x :: xs) = splitHelp x xs xs
50+
51+||| View for splitting a vector in half, recursively
52+|||
53+||| This allows us to define recursive functions which repeatedly split vectors
54+||| in half, with base cases for the empty and singleton lists.
55+public export
56+data SplitRec : Vect n a -> Type where
57+ SplitRecNil : SplitRec []
58+ SplitRecOne : {x : a} -> SplitRec [x]
59+ SplitRecPair : {xs : Vect n a} ->
60+ {ys : Vect m a} -> -- Explicit, don't erase
61+ (lrec : Lazy (SplitRec xs)) ->
62+ (rrec : Lazy (SplitRec ys)) -> SplitRec (xs ++ ys)
63+
64+smallerPlus : LTE (S (S m)) (S (plus m (S k)))
65+smallerPlus {m} {k} = rewrite sym (plusSuccRightSucc m k) in
66+ (LTESucc (LTESucc (lteAddRight _)))
67+
68+smallerPlus' : LTE (S (S k)) (S (plus m (S k)))
69+smallerPlus' {m} {k} = rewrite sym (plusSuccRightSucc m k) in
70+ LTESucc (LTESucc (rewrite plusCommutative m k in (lteAddRight _)))
71+
72+||| Covering function for the `SplitRec` view
73+||| Constructs the view in O(n lg n)
74+export
75+splitRec : (xs : Vect n a) -> SplitRec xs
76+splitRec {n} input with (ltAccessible n)
77+ splitRec input | acc with (split input)
78+ splitRec [] | acc | SplitNil = SplitRecNil
79+ splitRec [x] | acc | SplitOne = SplitRecOne
80+ splitRec (x :: (xs ++ (y :: ys))) | (Access rec) | SplitPair
81+ = let left = splitRec (x :: xs) | rec _ smallerPlus
82+ right = splitRec (y :: ys) | rec _ smallerPlus' in
83+ SplitRecPair left right
libs/base/base.ipkg+1−1
@@ -13,7 +13,7 @@ modules = System,
1313
1414 Data.Morphisms,
1515 Data.Bits, Data.Mod2,
16− Data.Fin, Data.Vect,
16+ Data.Fin, Data.Vect, Data.Vect.Views,
1717 Data.HVect, Data.Vect.Quantifiers,
1818 Data.Complex,
1919 Data.Erased, Data.List, Data.List.Views,
test/views001/expected+2
@@ -1,3 +1,5 @@
11Sorting list
22[1, 5, 5, 5, 5, 5, 9, 9, 9, 9, 9, 13, 13, 13, 13, 13, 13, 17, 17, 17, 17, 17, 21, 21, 21, 21, 21, 25, 29, 29, 29, 29, 29, 29, 29, 29, 33, 33, 33, 33, 33, 33, 37, 37, 37, 37, 37, 37, 37, 37, 37, 41, 41, 41, 45, 49, 53, 53, 53, 57, 57, 57, 57, 61, 61, 61, 61, 61, 61, 61, 65, 65, 65, 69, 69, 73, 73, 73, 73, 73, 77, 77, 77, 77, 81, 81, 85, 85, 85, 85, 89, 89, 93, 93, 93, 93, 97, 97, 97, 97]
33[97, 97, 97, 97, 93, 93, 93, 93, 89, 89, 85, 85, 85, 85, 81, 81, 77, 77, 77, 77, 73, 73, 73, 73, 73, 69, 69, 65, 65, 65, 61, 61, 61, 61, 61, 61, 61, 57, 57, 57, 57, 53, 53, 53, 49, 45, 41, 41, 41, 37, 37, 37, 37, 37, 37, 37, 37, 37, 33, 33, 33, 33, 33, 33, 29, 29, 29, 29, 29, 29, 29, 29, 25, 21, 21, 21, 21, 21, 17, 17, 17, 17, 17, 13, 13, 13, 13, 13, 13, 9, 9, 9, 9, 9, 5, 5, 5, 5, 5, 1]
4+Sorting list
5+[1, 5, 5, 5, 5, 5, 9, 9, 9, 9, 9, 13, 13, 13, 13, 13, 13, 17, 17, 17, 17, 17, 21, 21, 21, 21, 21, 25, 29, 29, 29, 29, 29, 29, 29, 29, 33, 33, 33, 33, 33, 33, 37, 37, 37, 37, 37, 37, 37, 37, 37, 41, 41, 41, 45, 49, 53, 53, 53, 57, 57, 57, 57, 61, 61, 61, 61, 61, 61, 61, 65, 65, 65, 69, 69, 73, 73, 73, 73, 73, 77, 77, 77, 77, 81, 81, 85, 85, 85, 85, 89, 89, 93, 93, 93, 93, 97, 97, 97, 97]
test/views001/run+3−1
@@ -1,4 +1,6 @@
11#!/usr/bin/env bash
22${IDRIS:-idris} $@ views001.idr -o views001
33./views001
4−rm -f views001 *.ibc
4+${IDRIS:-idris} $@ views001a.idr -o views001a
5+./views001a
6+rm -f views001 views001a *.ibc
test/views001/views001a.idrnew file+29
@@ -0,0 +1,29 @@
1+import Data.Vect
2+import Data.Vect.Views
3+
4+total
5+mergeSort : Ord a => Vect n a -> Vect n a
6+mergeSort xs with (splitRec xs)
7+ mergeSort [] | SplitRecNil = []
8+ mergeSort [x] | SplitRecOne = [x]
9+ mergeSort (ys ++ zs) | SplitRecPair ysrec zsrec
10+ = merge (mergeSort ys | ysrec)
11+ (mergeSort zs | zsrec)
12+
13+testList : Int -> Int -> List Int -> List Int
14+testList 0 seed acc = acc
15+-- Need to explicitly mod since different back ends overflow differently
16+testList x seed acc = let seed' = seed * 12345 + 768 `mod` 65536 in
17+ testList (x - 1) seed'
18+ ((seed' `mod` 100) :: acc)
19+
20+myhead : List a -> a
21+myhead (x :: xs) = x
22+
23+main : IO ()
24+main = do let list = fromList (testList 100 12345 [])
25+ putStrLn "Sorting list"
26+ let list' = mergeSort list
27+ printLn list'
28+
29+