7c5819b · Idris-dev · git.iko.soy

libs/base/Data/List/Views.idr+4−4

compare with master

unifiedsplit

@@ -82,7 +82,7 @@ public export

82data SnocList : List a -> Type where

83 Empty : SnocList []

84 Snoc : {x : a} -> {xs : List a} -> -- Explicit, so don't erase

85− SnocList xs -> SnocList (xs ++ [x])

85+ (rec : SnocList xs) -> SnocList (xs ++ [x])

86

87snocListHelp : SnocList xs -> (ys : List a) -> SnocList (xs ++ ys)

88snocListHelp {xs} x [] = rewrite appendNilRightNeutral xs in x

@@ -100,8 +100,8 @@ snocList xs = snocListHelp Empty xs

100public export

101data Filtered : (a -> a -> Bool) -> List a -> Type where

102 FNil : Filtered p []

103− FRec : Lazy (Filtered p (filter (\y => p y x) xs)) ->

103+ FRec : (lrec : Lazy (Filtered p (filter (\y => p y x) xs))) ->

104− Lazy (Filtered p (filter (\y => not (p y x)) xs)) ->

104+ (rrec : Lazy (Filtered p (filter (\y => not (p y x)) xs))) ->

105 Filtered p (x :: xs)

106

107filteredLOK : (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

178 VNil : VList []

179 VOne : VList [x]

180 VCons : {x : a} -> {y : a} -> {xs : List a} ->

181− VList xs -> VList (x :: xs ++ [y])

181+ (rec : VList xs) -> VList (x :: xs ++ [y])

182

183total

184balRec : (zs, xs : List a) ->

libs/base/Data/Vect.idr+15

@@ -194,6 +194,21 @@ replicate : (n : Nat) -> (x : a) -> Vect n a

194replicate Z x = []

195replicate (S k) x = x :: replicate k x

196

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+

197--------------------------------------------------------------------------------

212--------------------------------------------------------------------------------

198-- Zips and unzips

213-- Zips and unzips

199--------------------------------------------------------------------------------

214--------------------------------------------------------------------------------

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,

13

14 Data.Morphisms,

15 Data.Bits, Data.Mod2,

16− Data.Fin, Data.Vect,

16+ Data.Fin, Data.Vect, Data.Vect.Views,

17 Data.HVect, Data.Vect.Quantifiers,

18 Data.Complex,

19 Data.Erased, Data.List, Data.List.Views,

test/views001/expected+2

@@ -1,3 +1,5 @@

1Sorting list

2[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]

3[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 @@

1#!/usr/bin/env bash

2${IDRIS:-idris} $@ views001.idr -o views001

3./views001

4+${IDRIS:-idris} $@ views001a.idr -o views001a

5+./views001a

4−rm -f views001 *.ibc

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+