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

%default total

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

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

2.5 KiB Raw Blame History