# Utility functions

This module contains functions that extend the functionality of standard data
types, other types of utility functionality get their own module

```idris
module Util

import Data.SortedSet
import Data.String
import Data.List.Lazy
import Data.List1

%default total
```

## Functions

### repeatN

Recursively applies `f` to `seed` N times

```idris
export
repeatN : (times : Nat) -> (f : a -> a) -> (seed : a) -> a
repeatN 0 f seed = seed
repeatN (S times') f seed = repeatN times' f (f seed)
```

## Either

```idris hide
namespace Either
```

### mapLeft

Applies a function to the contents of a `Left` if the value of the given
`Either` is actually a `Left`, otherwise, leaves `Right`s untouched.

```idris
  export
  mapLeft : (f : a -> b) -> Either a c -> Either b c
  mapLeft f (Left x) = Left (f x)
  mapLeft f (Right x) = Right x
```

## List

```idris hide
namespace List
```

### contains

Returns `True` if the list contains the given value

```idris
export
contains : Eq a => a -> List a -> Bool
contains x [] = False
contains x (y :: xs) = 
  if x == y 
    then True
    else contains x xs
```

### rotations

Provides all the 'rotations' of a list.

Example:

```
rotations [1, 2, 3] == [[1, 2, 3], [3, 1, 2], [2, 3, 1]]
```

```idris
export
rotations : List a -> List (List a) 
rotations xs = rotations' (length xs) xs []
  where
    rotations' : Nat -> List a -> (acc : List (List a)) -> List (List a)
    rotations' 0 xs acc = acc
    rotations' (S k) [] acc = acc
    rotations' (S k) (x :: xs) acc = 
      let next = xs ++ [x]
      in rotations' k next (next :: acc)
```

## Vectors

Define some operations for pairs of numbers, treating them roughly like vectors

### Addition and Subtraction

```idris hide
export infixl 8 >+<
export infixl 8 >-<

namespace Pair
```

```idris
  public export
  (>+<) : Num a => (x, y : (a, a)) -> (a, a)
  (x_1, x_2) >+< (y_1, y_2) = (x_1 + y_1, x_2 + y_2)

  public export
  (>-<) : Neg a => (x, y : (a, a)) -> (a, a)
  (x_1, x_2) >-< (y_1, y_2) = (x_1 - y_1, x_2 - y_2)
```

## Set

Extend `Data.SortedSet`

```idris hide
namespace Set
```

### length

Count the number of elements in a sorted set

```idris
  export
  length : SortedSet k -> Nat
  length x = foldl (\acc, e => acc + 1) 0 x
```

## String

Extend `Data.String`

```idris hide
namespace String
```

### isSubstr

Returns `True` if `needle` is a substring of `haystack`

We first check to see if the needle is a prefix of the top level haystack,
before calling into a tail recursive helper function that peels one character
off of the string at a time, checking if the needle is a prefix at each step.

```idris
  export
  isSubstr : (needle, haystack : String) -> Bool
  isSubstr needle haystack = 
    if needle `isPrefixOf` haystack 
      then True
      else isSubstr' haystack
    where
    isSubstr' : String -> Bool
    isSubstr' str with (asList str)
      isSubstr' "" | [] = False
      isSubstr' (strCons c str) | (c :: x) = 
        if needle `isPrefixOf` str
          then True
          else isSubstr' str | x
```

## Lazy List

### Cartesian product

Lazily take the cartesian product of two foldables

```idris
export
cartProd : Foldable a => Foldable b => a e -> b f -> LazyList (e, f)
cartProd x y = 
  let y = foldToLazy y
  in foldr (\e, acc => combine e y acc) [] x
  where
    foldToLazy : Foldable a' => a' e' -> LazyList e'
    foldToLazy x = foldr (\e, acc => e :: acc) [] x
    combine : e -> LazyList f -> LazyList (e, f) -> LazyList (e, f)
    combine x [] rest = rest
    combine x (y :: ys) rest = (x, y) :: combine x ys rest
```

### Concat

Lazily concatenate a LazyList of LazyLists

```idris
export
lazyConcat : LazyList (LazyList a) -> LazyList a
lazyConcat [] = []
lazyConcat (x :: xs) = x ++ lazyConcat xs
```

### Group

Lazily group a LazyList

```idris
export
lazyGroup : Eq a => LazyList a -> LazyList (List1 a)
lazyGroup [] = []
lazyGroup (x :: xs) = lazyGroup' xs x (x ::: [])
  where
    lazyGroup' : LazyList a -> (current : a) -> (acc : List1 a) -> LazyList (List1 a)
    lazyGroup' [] current acc = [acc]
    lazyGroup' (y :: ys) current acc@(head ::: tail) = 
      if y == current
        then lazyGroup' ys current (head ::: (y :: tail))
        else acc :: lazyGroup (y :: ys)
```