Utility functions
This module contains functions that extend the functionality of standard data types, other types of utility functionality get their own module
module Util
import Data.SortedSet
import Data.String
import Data.List.Lazy
import Data.List1
import Data.Vect
import Data.Fin
%default total
Foldable
General utility functions for foldables
minBy
||| Get the minimum element of a collection using the provided comparison
||| function and seed value
export
minBy : Foldable f => (cmp : a -> a -> Ordering) -> (acc : a) -> f a -> a
minBy cmp acc x =
foldl
(\acc, e =>
case e `cmp` acc of
LT => e
_ => acc)
acc x
||| Get the maximum element of a collection using the provided comparison
||| function and seed value
export
maxBy : Foldable f => (cmp : a -> a -> Ordering) -> (acc : a) -> f a -> a
maxBy cmp acc x =
foldl
(\acc, e =>
case e `cmp` acc of
GT => e
_ => acc)
acc x
Functions
repeatN
Recursively applies f to seed N times
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
mapLeft
Applies a function to the contents of a Left if the value of the given
Either is actually a Left, otherwise, leaves Rights untouched.
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
contains
Returns True if the list contains the given value
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]]
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)
permutations
Lazily generate all of the permutations of a list
export
permutations : List a -> LazyList (List a)
permutations [] = pure []
permutations xs = do
(head, tail) <- select xs
tail <- permutations (assert_smaller xs tail)
pure $ head :: tail
where
consSnd : a -> (a, List a) -> (a, List a)
consSnd x (y, xs) = (y, x :: xs)
select : List a -> LazyList (a, List a)
select [] = []
select (x :: xs) = (x, xs) :: map (consSnd x) (select xs)
Vect
permutations
Lazily generate all the permutations of a Vect
export
permutations : Vect n a -> LazyList (Vect n a)
permutations [] = []
permutations [x] = [[x]]
permutations (x :: xs) = do
(head, tail) <- select (x :: xs)
tail <- permutations tail
pure $ head :: tail
where
consSnd : a -> (a, Vect m a) -> (a, Vect (S m) a)
consSnd x (y, xs) = (y, x :: xs)
select : Vect (S m) a -> LazyList (a, Vect m a)
select [y] = [(y, [])]
select (y :: (z :: ys)) =
(y, z :: ys) :: map (consSnd y) (select (z :: ys))
minBy and maxBy
||| Get the minimum element of a non-empty vector by using the provided
||| comparison function
export
minBy : (f : a -> a -> Ordering) -> Vect (S n) a -> a
minBy f (x :: xs) = Foldable.minBy f x xs
||| Get the maximum element of a non-empty vector by using the provided
||| comparison function
export
maxBy : (f : a -> a -> Ordering) -> Vect (S n) a -> a
maxBy f (x :: xs) = Foldable.maxBy f x xs
Convert a list to a vect as a sigma type
export
listToVect : List a -> (n : Nat ** Vect n a)
listToVect xs = (length xs ** fromList xs)
Fin
||| Decriment a Fin, wrapping on overflow
export
unfinS : {n : _} -> Fin n -> Fin n
unfinS FZ = last
unfinS (FS x) = weaken x
Vectors
Define some operations for pairs of numbers, treating them roughly like vectors
Addition and Subtraction
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
length
Count the number of elements in a sorted set
export
length : SortedSet k -> Nat
length x = foldl (\acc, e => acc + 1) 0 x
String
Extend Data.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.
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
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
export
lazyConcat : LazyList (LazyList a) -> LazyList a
lazyConcat [] = []
lazyConcat (x :: xs) = x ++ lazyConcat xs
Group
Lazily group a LazyList
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)
length
Calculate the length of a LazyList
export
length : LazyList a -> Nat
length = length' 0
where
length' : Nat -> LazyList a -> Nat
length' k [] = k
length' k (x :: xs) = length' (S k) xs