advent/src/Util.md

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

%default total

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)

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)