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.

```idris
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 `Grid`s 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

```idris
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 `Fin`s.

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 `Fin`s 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.

```idris
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.

```idris
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 `Seq`s with the given size bounds.

The inner `Seq`s are kept opaque to maintain flexability in the implementation

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

```idris
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.

```idris
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 `Vect`s. To keep the function simple, we require that both the row and column dimension are known to be non-zero before calling this constructor.

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

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

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

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

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

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

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

#### Eq/Ord

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

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

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

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

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

#### Zippable

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

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

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

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

```idris
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
```idris
export
toLists : Grid rows cols e -> List (List e)
toLists (MkGrid grid) = toList . map toList $ grid
```