advent/src/Grid.md

2D Grid utilities

Types and utilities for dealing with a 2D grid of things

We base our Grid type on Data.Seq.Sized from contrib, a finger tree based collection that tracks its size in its type, since it provides somewhat efficient random access and updates.

module Grid
  
import Data.Seq.Sized
import Data.Fin
import Data.Fin.Extra
import Data.List.Lazy
import Data.Zippable
import Data.Vect
import Data.String
import Decidable.Equality

%default total

Coordinates

A coordinate is a pair of numbers both less than their respective bounds.

Since Grids will always be non-empty in the contexts we will be using them in, this type alias adds one to each of the bounds to ensure non-emptyness

public export
Coord : (rows, cols : Nat) -> Type
Coord rows cols = (Fin (S rows), Fin (S cols))

Coordinate utility functions

Lazily generate all the coordinates for a given pair of bounds

Uses an internal helper function to generate a lazy list of all the fins of a given bound in ascending order (all), and another to convert a lazy list of Fin into a lazy list of pairs of Fins.

The totality checker likes to go in the descending direction, since then it can reason about values getting structurally "smaller", so it has issues with all' moving in the ascending direction. We know this function is total because the acc < last check will always eventually be triggered, since Fins only have a finite number of values.

We pull out an assert_smaller to tell Idris that the argument to the recursive call is getting structurally smaller, which while not strictly correct, does convey to the compiler that we are getting closer to our recursive base case and that the function is thus total.

export
allCords : {rows, cols : Nat} -> LazyList (Coord rows cols)
allCords = concat . map row $ all
  where
    all : {n : Nat} -> LazyList (Fin (S n))
    all = FZ :: all' FZ
      where
        all' : {n : Nat} -> (acc : Fin (S n)) -> LazyList (Fin (S n))
        all' acc =
          if acc < last
            then finS acc :: all' (assert_smaller acc (finS acc))
            else []
    row : Fin (S rows) -> LazyList (Coord rows cols)
    row r = map (\c => (r, c)) all

Add a given vector to a coordinate, returning Nothing if we go off the ends of the bounds in the process.

To keep this function simple and reasonably efficient, we perform the arithmetic in integer space, using integerToFin to fallably convert back to Fin space, making use of the Maybe monad to keep the code clean.

export
step : {rows, cols : Nat} -> (input : Coord rows cols) -> (direction : (Integer, Integer))
     -> Maybe (Coord rows cols)
step (row, col) (d_row, d_col) = do
  let (row, col) = (finToInteger row, finToInteger col)
  row <- integerToFin (row + d_row) (S rows)
  col <- integerToFin (col + d_col) (S cols)
  pure (row, col)

Grid

A grid is a Seq of Seqs with the given size bounds.

The inner Seqs are kept opaque to maintain flexability in the implementation

export
record Grid (rows, cols : Nat) (e : Type) where
  constructor MkGrid
  grid : Seq (S rows) (Seq (S cols) e)
%name Grid grid, grid2, grid3

Constructors

Construct a Grid by filling every slot with identical copies of the provided element

export
replicate : {rows, cols : Nat} -> (seed : e) -> Grid rows cols e
replicate seed = 
  let row = replicate (S cols) seed
      grid = replicate (S rows) row
  in MkGrid grid

Attempt to construct a Grid from a Foldable of Foldables. Will return Nothing if either the rows are of heterogeneous size, or if either the rows or columns are empty. Requires that the outer Foldable also be Traversable.

We make heavy use of the Maybe monad to keep the code clean here.

export
fromFoldable : Traversable a => Foldable a => Foldable b => a (b e) -> 
  Maybe (rows : Nat ** cols : Nat ** Grid rows cols e)
fromFoldable xs = do
  -- First collect the number of rows from the outer foldable
  let (S rows) = foldl (\acc, e => acc + 1) 0 xs
    | _ => Nothing -- Return Nothing if there are no rows
  -- Get the number of columns in the largest row in the inner foldable
  let (S cols) = foldl (\acco, eo => max acco (foldl (\acci, ei => acci +1) 0 eo)) 0 xs
    | _ => Nothing -- Return Nothing if all the rows are empty
  -- Convert the rows by traversing our foldToSeq function over the outer foldable
  xs <- traverse (foldToSeq (S cols)) xs
  -- Reuse our foldToSeq helper function to convert the outer foldable
  xs <- foldToSeq (S rows) xs
  -- wrap it up and return
  pure (rows ** cols ** MkGrid xs)
  where
    -- Convert each row to a seq using an intermediate list
    foldToSeq : Foldable c => (n : Nat) -> c f -> Maybe (Seq n f)
    foldToSeq n x = 
      let list = toList x
      -- Check to see if the list is of the correct length, then rewrite the
      -- output type to match if that's the case, otherwise return Nothing
      in case decEq (length list) n of
        Yes Refl => Just $ fromList list
        No _ => Nothing

Construct a Grid from a non-empty Vect of non-empty Vects. To keep the function simple, we require that both the row and column dimension are known to be non-zero before calling this constructor.

export
fromVect : Vect (S rows) (Vect (S cols) e) -> Grid rows cols e
fromVect xs = MkGrid . fromVect . map fromVect $ xs

Construct Grid containing the coordinate of the location in each location

export
coordinateGrid : {rows, cols : Nat} -> Grid rows cols (Coord rows cols)
coordinateGrid = 
  let row = fromVect $ allFins (S cols) 
      grid = zip (fromVect $ allFins (S rows)) (replicate _ row)
      grid = map (\(x, xs) => map (x,) xs) grid
  in MkGrid grid

Accessors and Mutators

Get the value at a specific index in the grid

export
index : Coord rows cols -> Grid rows cols e -> e
index (row, col) grid = 
  index' (index' grid.grid row) col

Replace the value at a specific index in the grid

export
replaceAt : Coord rows cols -> e -> Grid rows cols e -> Grid rows cols e
replaceAt (row, col) x (MkGrid grid) = 
  let r = index' grid row
      r = update (finToNat col) x r @{elemSmallerThanBound col}
      grid = update (finToNat row) r grid @{elemSmallerThanBound row}
  in MkGrid grid

Update the value at a specific index in the grid

export
updateAt : Coord rows cols -> (e -> e) -> Grid rows cols e -> Grid rows cols e
updateAt (row, col) f (MkGrid grid) = 
  let r = index' grid row
      r = adjust f (finToNat col) r @{elemSmallerThanBound col}
      grid = update (finToNat row) r grid @{elemSmallerThanBound row}
  in MkGrid grid

Lazily provide all the values in the grid as a flat collection

export
flat : {rows, cols : Nat} -> Grid rows cols e -> LazyList e
flat (MkGrid grid) = 
  let grid = seqToLazy . map (seqToLazy {n = S cols}) $ grid 
      grid = grid []
  in foldrLazy (\a, acc => a acc) [] grid
  where
    seqToLazy : {n : Nat} -> (seq : Seq n a) -> (rest : LazyList a) -> LazyList a
    seqToLazy {n = 0} seq rest = rest
    seqToLazy {n = (S k)} seq rest = 
      let (head, tail) = viewl seq
      in head :: seqToLazy tail rest

Interface Implementations

Show

export
{rows, cols : Nat} -> Show e => Show (Grid rows cols e) where
  show (MkGrid grid) = 
    show . toVect . map toVect $ grid

Eq/Ord

export
Eq e => Eq (Grid rows cols e) where
  (MkGrid grid_x) == (MkGrid grid_y) = grid_x == grid_y

export
Ord e => Ord (Grid rows cols e) where
  compare (MkGrid grid_x) (MkGrid grid_y) = compare grid_x grid_y

Functor

export
Functor (Grid rows cols) where
  map f (MkGrid grid) = 
    MkGrid . map (map f) $ grid

Foldable

Cheeze it a little and use our flat function internally here.

Also, null can statically return false, as Grid is structurally non-empty

export
{rows, cols : Nat} -> Foldable (Grid rows cols) where
  foldr f acc grid = foldr f acc (flat grid)
  foldl f acc grid = foldl f acc (flat grid)
  null _ = False
  toList grid = toList (flat grid)

Applicative

export
{rows, cols : Nat} -> Applicative (Grid rows cols) where
  pure a = replicate a
  (MkGrid f) <*> (MkGrid grid) = 
    MkGrid . map (\(a,b) => a <*> b) . zip f $ grid

Traversable

export
{rows, cols : Nat} -> Traversable (Grid rows cols) where
  traverse f (MkGrid grid) = 
    map MkGrid . traverse (traverse f) $ grid 

Zippable

export
Zippable (Grid rows cols) where
  zipWith f (MkGrid grid_x) (MkGrid grid_y) = 
    let xs = zip grid_x grid_y
    in MkGrid . map (\(a,b) => zipWith f a b) $ xs
  unzipWith f (MkGrid grid) = 
    let (xs, ys) = unzip . map (unzipWith f) $ grid
    in (MkGrid xs, MkGrid ys)
  zipWith3 f (MkGrid as) (MkGrid bs) (MkGrid cs) = 
    let xs = zip3 as bs cs
    in MkGrid . map (\(a, b, c) => zipWith3 f a b c) $ xs 
  unzipWith3 f (MkGrid grid) = 
    let (a, b, c) = unzip3 . map (unzipWith3 f) $ grid
    in (MkGrid a, MkGrid b, MkGrid c)

Extra

Extensions of the above functionality

Indexing

Convert this grid to one with both the index of the location and the element in each location

export
indexed : {rows, cols : Nat} -> Grid rows cols e -> Grid rows cols (Coord rows cols, e)
indexed grid = zip coordinateGrid grid

Same as flat above, but indexed

export
flatIndexed : {rows, cols : Nat} -> Grid rows cols e -> LazyList (Coord rows cols, e)
flatIndexed = flat . indexed

String functionality

Attempts to convert a string, with newline delimited rows, to a grid of characters

export
stringToGrid : String -> Maybe (rows : Nat ** cols : Nat ** Grid rows cols Char) 
stringToGrid = fromFoldable . map (unpack . trim) . lines . trim

Converts a grid of chars to a string, delimiting the rows with newlines

export
gridToString : Grid rows cols Char -> String
gridToString (MkGrid grid) = unlines . toList . map (pack . toList) $ grid

Conversion

Convert a grid to a vect of vects

export
toVects : {rows, cols : Nat} -> Grid rows cols e -> Vect (S rows) (Vect (S cols) e)
toVects (MkGrid grid) = toVect . map toVect $ grid

Convert a grid to a list of lists

export
toLists : Grid rows cols e -> List (List e)
toLists (MkGrid grid) = toList . map toList $ grid