a39a3dd · Idris-dev · git.iko.soy

idris.cabal+3

compare with master

unifiedsplit

@@ -820,6 +820,9 @@ Extra-source-files:

820 test/views001/run

821 test/views001/*.idr

822 test/views001/expected

823+ test/views002/run

824+ test/views002/*.idr

825+ test/views002/expected

823

826

824 test/docs001/run

827 test/docs001/run

825 test/docs001/input

828 test/docs001/input

libs/base/Data/List/Views.idr+21

@@ -88,6 +88,27 @@ export

88snocList : (xs : List a) -> SnocList xs

89snocList xs = snocListHelp Empty xs

90

91+||| View for recursively filtering a list by a predicate, applied to the

92+||| first item in each recursively filtered list

93+public export

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

95+ FNil : Filtered p []

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

97+ Lazy (Filtered p (filter (\y => not (p y x)) xs)) ->

98+ Filtered p (x :: xs)

99+

100+filteredLOK : (p : a -> a -> Bool) -> (x : a) -> (xs : List a) -> smaller (filter (\y => p y x) xs) (x :: xs)

101+filteredLOK p x xs = LTESucc (filterSmaller xs)

91

102

103+filteredROK : (p : a -> a -> Bool) -> (x : a) -> (xs : List a) -> smaller (filter (\y => not (p y x)) xs) (x :: xs)

104+filteredROK p x xs = LTESucc (filterSmaller xs)

92

105

106+||| Covering function for the `Filtered` view

107+export

108+filtered : (p : a -> a -> Bool) -> (xs : List a) -> Filtered p xs

109+filtered p inp with (smallerAcc inp)

110+ filtered p [] | with_pat = FNil

111+ filtered p (x :: xs) | (Access xsrec)

112+ = FRec (Delay (filtered p (filter (\y => p y x) xs) | xsrec _ (filteredLOK p x xs)))

113+ (Delay (filtered p (filter (\y => not (p y x)) xs) | xsrec _ (filteredROK p x xs)))

93

114

libs/prelude/Prelude/List.idr+8

@@ -536,6 +536,14 @@ filter p (x::xs) =

536 else

537 filter p xs

538

539+||| A filtered list is no longer than its input

540+filterSmaller : (xs : _) -> LTE (length (filter p xs)) (length xs)

541+filterSmaller [] = LTEZero

542+filterSmaller {p} (x :: xs) with (p x)

543+ filterSmaller {p = p} (x :: xs) | False = lteSuccRight (filterSmaller xs)

544+ filterSmaller {p = p} (x :: xs) | True = LTESucc (filterSmaller xs)

545+

546+

539||| The nubBy function behaves just like nub, except it uses a user-supplied equality predicate instead of the overloaded == function.

547||| The nubBy function behaves just like nub, except it uses a user-supplied equality predicate instead of the overloaded == function.

540nubBy : (a -> a -> Bool) -> List a -> List a

548nubBy : (a -> a -> Bool) -> List a -> List a

541nubBy = nubBy' []

549nubBy = nubBy' []

test/views002/expectednew file+2

@@ -0,0 +1,2 @@

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]

test/views002/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

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

3+./views002

4+rm -f views002 *.ibc

test/views002/views002.idrnew file+24

@@ -0,0 +1,24 @@

1+import Data.List.Views

2+

3+total

4+qsort : Ord a => (xs : List a) -> List a

5+qsort inp with (filtered (<) inp)

6+ qsort [] | FNil = []

7+ qsort (x :: xs) | (FRec lrec rrec)

8+ = qsort (filter (\v => v < x) xs) | lrec ++

9+ x :: qsort (filter (\v => not (v < x)) xs) | rrec

10+

11+testList : Int -> Int -> List Int -> List Int

12+testList 0 seed acc = acc

13+testList x seed acc = testList (x - 1) (seed * 12345 + 789)

14+ ((seed `mod` 100) :: acc)

15+

16+myhead : List a -> a

17+myhead (x :: xs) = x

18+

19+main : IO ()

20+main = do let list = testList 100 12345 []

21+ putStrLn "Sorting list"

22+ let list' = qsort list

23+ printLn list'

24+