module Data.List import Decidable.Equality public exportisNil : List a -> BoolisNil []      = TrueisNil (x::xs) = False public exportisCons : List a -> BoolisCons []      = FalseisCons (x::xs) = True public exportlength : List a -> Natlength []      = Zlength (x::xs) = S (length xs) public exporttake : Nat -> List a -> List atake Z xs = []take (S k) [] = []take (S k) (x :: xs) = x :: take k xs public exportdrop : (n : Nat) -> (xs : List a) -> List adrop Z     xs      = xsdrop (S n) []      = []drop (S n) (x::xs) = drop n xs public exporttakeWhile : (p : a -> Bool) -> List a -> List atakeWhile p []      = []takeWhile p (x::xs) = if p x then x :: takeWhile p xs else [] public exportdropWhile : (p : a -> Bool) -> List a -> List adropWhile p []      = []dropWhile p (x::xs) = if p x then dropWhile p xs else x::xs public exportfilter : (p : a -> Bool) -> List a -> List afilter p [] = []filter p (x :: xs)   = if p x        then x :: filter p xs        else filter p xs ||| Find associated information in a list using a custom comparison.public exportlookupBy : (a -> a -> Bool) -> a -> List (a, b) -> Maybe blookupBy p e []      = NothinglookupBy p e (x::xs) =  let (l, r) = x in    if p e l then      Just r    else      lookupBy p e xs ||| Find associated information in a list using Boolean equality.public exportlookup : Eq a => a -> List (a, b) -> Maybe blookup = lookupBy (==) ||| Check if something is a member of a list using a custom comparison.public exportelemBy : (a -> a -> Bool) -> a -> List a -> BoolelemBy p e []      = FalseelemBy p e (x::xs) =  if p e x then    True  else    elemBy p e xs public exportnubBy : (a -> a -> Bool) -> List a -> List anubBy = nubBy' []  where    nubBy' : List a -> (a -> a -> Bool) -> List a -> List a    nubBy' acc p []      = []    nubBy' acc p (x::xs) =      if elemBy p x acc then        nubBy' acc p xs      else        x :: nubBy' (x::acc) p xs ||| O(n^2). The nub function removes duplicate elements from a list. In||| particular, it keeps only the first occurrence of each element. It is a||| special case of nubBy, which allows the programmer to supply their own||| equality test.|||||| ```idris example||| nub (the (List _) [1,2,1,3])||| ```public exportnub : Eq a => List a -> List anub = nubBy (==) ||| The deleteBy function behaves like delete, but takes a user-supplied equality predicate.public exportdeleteBy : (a -> a -> Bool) -> a -> List a -> List adeleteBy _  _ []      = []deleteBy eq x (y::ys) = if x `eq` y then ys else y :: deleteBy eq x ys ||| `delete x` removes the first occurrence of `x` from its list argument. For||| example,||||||````idris example|||delete 'a' ['b', 'a', 'n', 'a', 'n', 'a']|||````|||||| It is a special case of deleteBy, which allows the programmer to supply||| their own equality test.public exportdelete : Eq a => a -> List a -> List adelete = deleteBy (==) ||| The unionBy function returns the union of two lists by user-supplied equality predicate.public exportunionBy : (a -> a -> Bool) -> List a -> List a -> List aunionBy eq xs ys = xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs ||| Compute the union of two lists according to their `Eq` implementation.|||||| ```idris example||| union ['d', 'o', 'g'] ['c', 'o', 'w']||| ```|||public exportunion : Eq a => List a -> List a -> List aunion = unionBy (==) public exportspan : (a -> Bool) -> List a -> (List a, List a)span p []      = ([], [])span p (x::xs) =  if p x then    let (ys, zs) = span p xs in      (x::ys, zs)  else    ([], x::xs) public exportbreak : (a -> Bool) -> List a -> (List a, List a)break p xs = span (not . p) xs public exportsplit : (a -> Bool) -> List a -> List (List a)split p xs =  case break p xs of    (chunk, [])          => [chunk]    (chunk, (c :: rest)) => chunk :: split p rest public exportsplitAt : (n : Nat) -> (xs : List a) -> (List a, List a)splitAt Z xs = ([], xs)splitAt (S k) [] = ([], [])splitAt (S k) (x :: xs)      = let (tk, dr) = splitAt k xs in            (x :: tk, dr) public exportpartition : (a -> Bool) -> List a -> (List a, List a)partition p []      = ([], [])partition p (x::xs) =  let (lefts, rights) = partition p xs in    if p x then      (x::lefts, rights)    else      (lefts, x::rights) ||| The inits function returns all initial segments of the argument, shortest||| first. For example,|||||| ```idris example||| inits [1,2,3]||| ```public exportinits : List a -> List (List a)inits xs = [] :: case xs of  []        => []  x :: xs'  => map (x ::) (inits xs') ||| The tails function returns all final segments of the argument, longest||| first. For example,|||||| ```idris example||| tails [1,2,3] == [[1,2,3], [2,3], [3], []]|||```public exporttails : List a -> List (List a)tails xs = xs :: case xs of  []        => []  _ :: xs'  => tails xs' ||| Split on the given element.|||||| ```idris example||| splitOn 0 [1,0,2,0,0,3]||| ```|||public exportsplitOn : Eq a => a -> List a -> List (List a)splitOn a = split (== a) ||| Replaces all occurences of the first argument with the second argument in a list.|||||| ```idris example||| replaceOn '-' ',' ['1', '-', '2', '-', '3']||| ```|||public exportreplaceOn : Eq a => a -> a -> List a -> List areplaceOn a b l = map (\c => if c == a then b else c) l public exportreverseOnto : List a -> List a -> List areverseOnto acc [] = accreverseOnto acc (x::xs) = reverseOnto (x::acc) xs public exportreverse : List a -> List areverse = reverseOnto [] ||| Construct a list with `n` copies of `x`.||| @ n how many copies||| @ x the element to replicatepublic exportreplicate : (n : Nat) -> (x : a) -> List areplicate Z     _ = []replicate (S n) x = x :: replicate n x ||| Compute the intersect of two lists by user-supplied equality predicate.exportintersectBy : (a -> a -> Bool) -> List a -> List a -> List aintersectBy eq xs ys = [x | x <- xs, any (eq x) ys] ||| Compute the intersect of two lists according to the `Eq` implementation for the elements.exportintersect : Eq a => List a -> List a -> List aintersect = intersectBy (==) ||| Combine two lists elementwise using some function.|||||| If the lists are different lengths, the result is truncated to the||| length of the shortest list.exportzipWith : (a -> b -> c) -> List a -> List b -> List czipWith _ [] _ = []zipWith _ _ [] = []zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys ||| Combine two lists elementwise into pairs.|||||| If the lists are different lengths, the result is truncated to the||| length of the shortest list.exportzip : List a -> List b -> List (a, b)zip = zipWith \x, y => (x, y) exportzipWith3 : (a -> b -> c -> d) -> List a -> List b -> List c -> List dzipWith3 _ [] _ _ = []zipWith3 _ _ [] _ = []zipWith3 _ _ _ [] = []zipWith3 f (x::xs) (y::ys) (z::zs) = f x y z :: zipWith3 f xs ys zs ||| Combine three lists elementwise into tuples.|||||| If the lists are different lengths, the result is truncated to the||| length of the shortest list.exportzip3 : List a -> List b -> List c -> List (a, b, c)zip3 = zipWith3 \x, y, z => (x, y, z) public exportdata NonEmpty : (xs : List a) -> Type where    IsNonEmpty : NonEmpty (x :: xs) exportUninhabited (NonEmpty []) where  uninhabited IsNonEmpty impossible ||| Get the head of a non-empty list.||| @ ok proof the list is non-emptypublic exporthead : (l : List a) -> {auto ok : NonEmpty l} -> ahead [] impossiblehead (x :: xs) = x ||| Get the tail of a non-empty list.||| @ ok proof the list is non-emptypublic exporttail : (l : List a) -> {auto ok : NonEmpty l} -> List atail [] impossibletail (x :: xs) = xs ||| Attempt to get the head of a list. If the list is empty, return `Nothing`.exporthead' : List a -> Maybe ahead' []      = Nothinghead' (x::xs) = Just x ||| Attempt to get the tail of a list. If the list is empty, return `Nothing`.exporttail' : List a -> Maybe (List a)tail' []      = Nothingtail' (x::xs) = Just xs ||| Convert any Foldable structure to a list.exporttoList : Foldable t => t a -> List atoList = foldr (::) [] ||| Prefix every element in the list with the given element|||||| ```idris example||| with List (mergeReplicate '>' ['a', 'b', 'c', 'd', 'e'])||| ```|||exportmergeReplicate : a -> List a -> List amergeReplicate sep []      = []mergeReplicate sep (y::ys) = sep :: y :: mergeReplicate sep ys  ||| Insert some separator between the elements of a list.|||||| ````idris example||| with List (intersperse ',' ['a', 'b', 'c', 'd', 'e'])||| ````|||exportintersperse : a -> List a -> List aintersperse sep []      = []intersperse sep (x::xs) = x :: mergeReplicate sep xs ||| Given a separator list and some more lists, produce a new list by||| placing the separator between each of the lists.|||||| @ sep the separator||| @ xss the lists between which the separator will be placed|||||| ```idris example||| intercalate [0, 0, 0] [ [1, 2, 3], [4, 5, 6], [7, 8, 9] ]||| ```exportintercalate : (sep : List a) -> (xss : List (List a)) -> List aintercalate sep xss = concat $ intersperse sep xss ||| Apply a partial function to the elements of a list, keeping the ones at which||| it is defined.exportmapMaybe : (a -> Maybe b) -> List a -> List bmapMaybe f []      = []mapMaybe f (x::xs) =  case f x of    Nothing => mapMaybe f xs    Just j  => j :: mapMaybe f xs ---------------------------------------------------------------------------------- Sorting-------------------------------------------------------------------------------- ||| Check whether a list is sorted with respect to the default ordering for the type of its elements.exportsorted : Ord a => List a -> Boolsorted []      = Truesorted (x::xs) =  case xs of    Nil     => True    (y::ys) => x <= y && sorted (y::ys) ||| Merge two sorted lists using an arbitrary comparison||| predicate. Note that the lists must have been sorted using this||| predicate already.exportmergeBy : (a -> a -> Ordering) -> List a -> List a -> List amergeBy order []      right   = rightmergeBy order left    []      = leftmergeBy order (x::xs) (y::ys) =  -- The code below will emit `y` before `x` whenever `x == y`.  -- If you change this, `sortBy` will stop being stable, unless you fix `sortBy`, too.  case order x y of       LT => x :: mergeBy order xs (y::ys)       _  => y :: mergeBy order (x::xs) ys ||| Merge two sorted lists using the default ordering for the type of their elements.exportmerge : Ord a => List a -> List a -> List amerge left right = mergeBy compare left right ||| Sort a list using some arbitrary comparison predicate.|||||| @ cmp how to compare elements||| @ xs the list to sortexportsortBy : (cmp : a -> a -> Ordering) -> (xs : List a) -> List asortBy cmp []  = []sortBy cmp [x] = [x]sortBy cmp xs  = let (x, y) = split xs in    mergeBy cmp          (sortBy cmp (assert_smaller xs x))          (sortBy cmp (assert_smaller xs y)) -- not structurally smaller, hence assert  where    splitRec : List b -> List a -> (List a -> List a) -> (List a, List a)    splitRec (_::_::xs) (y::ys) zs = splitRec xs ys (zs . ((::) y))    splitRec _          ys      zs = (ys, zs [])    -- In the above base-case clause, we put `ys` on the LHS to get a stable sort.    -- This is because `mergeBy` prefers taking elements from its RHS operand    -- if both heads are equal, and all elements in `zs []` precede all elements of `ys`    -- in the original list.     split : List a -> (List a, List a)    split xs = splitRec xs xs id ||| Sort a list using the default ordering for the type of its elements.exportsort : Ord a => List a -> List asort = sortBy compare exportisPrefixOfBy : (eq : a -> a -> Bool) -> (left, right : List a) -> BoolisPrefixOfBy p [] right        = TrueisPrefixOfBy p left []         = FalseisPrefixOfBy p (x::xs) (y::ys) =  if p x y then    isPrefixOfBy p xs ys  else    False ||| The isPrefixOf function takes two lists and returns True iff the first list is a prefix of the second.exportisPrefixOf : Eq a => List a -> List a -> BoolisPrefixOf = isPrefixOfBy (==) exportisSuffixOfBy : (a -> a -> Bool) -> List a -> List a -> BoolisSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right) ||| The isSuffixOf function takes two lists and returns True iff the first list is a suffix of the second.exportisSuffixOf : Eq a => List a -> List a -> BoolisSuffixOf = isSuffixOfBy (==) ||| The isInfixOf function takes two lists and returns True iff the first list||| is contained, wholly and intact, anywhere within the second.|||||| ```idris example||| isInfixOf ['b','c'] ['a', 'b', 'c', 'd']||| ```||| ```idris example||| isInfixOf ['b','d'] ['a', 'b', 'c', 'd']||| ```|||exportisInfixOf : Eq a => List a -> List a -> BoolisInfixOf n h = any (isPrefixOf n) (tails h) ||| Transposes rows and columns of a list of lists.|||||| ```idris example||| with List transpose [[1, 2], [3, 4]]||| ```|||||| This also works for non square scenarios, thus||| involution does not always hold:||||||     transpose [[], [1, 2]] = [[1], [2]]|||     transpose (transpose [[], [1, 2]]) = [[1, 2]]exporttranspose : List (List a) -> List (List a)transpose [] = []transpose (heads :: tails) = spreadHeads heads (transpose tails) where  spreadHeads : List a -> List (List a) -> List (List a)  spreadHeads []              tails           = tails  spreadHeads (head :: heads) []              = [head] :: spreadHeads heads []  spreadHeads (head :: heads) (tail :: tails) = (head :: tail) :: spreadHeads heads tails ---------------------------------------------------------------------------------- Properties-------------------------------------------------------------------------------- exportUninhabited ([] = Prelude.(::) x xs) where  uninhabited Refl impossible exportUninhabited (Prelude.(::) x xs = []) where  uninhabited Refl impossible---- ||| (::) is injective-- consInjective : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->--                 (x :: xs) = (y :: ys) -> (x = y, xs = ys)-- consInjective Refl = (Refl, Refl)---- ||| Two lists are equal, if their heads are equal and their tails are equal.-- consCong2 : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->--             x = y -> xs = ys -> x :: xs = y :: ys

Lines 1–500 of 585. Load more