212 lines
4.2 KiB
Markdown
212 lines
4.2 KiB
Markdown
# 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
|
|
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
|
|
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
|
|
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
|
|
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
|
|
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)
|
|
```
|