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
import Data.Vect
import Data.Fin

%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

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 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

namespace 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

namespace 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))

Fin

namespace 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

export infixl 8 >+<
export infixl 8 >-<

namespace Pair

  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

namespace Set

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

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.

  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

namespace LazyList

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