126 lines
2.5 KiB
Markdown
126 lines
2.5 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
|
|
|
|
%default total
|
|
```
|
|
|
|
## 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
|
|
```
|
|
|
|
## 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
|
|
```
|