Idris/advent
1
0
Fork 0
Code Issues Pull requests Actions Packages Projects Releases Wiki Activity

Remove defective Grid module for now

Browse source
This commit is contained in:
Nathan McCarty 2025-01-23 00:30:33 -05:00
parent 76fcb6c34b
commit d405c43683
2 changed files with 0 additions and 372 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
advent.ipkg
View file

@ -28,7 +28,6 @@ modules = Runner
, Util , Util
, Util.Eff , Util.Eff
, Util.Digits , Util.Digits
, Grid
-- main file (i.e. file to load at REPL) -- main file (i.e. file to load at REPL)
main = Main main = Main

371
src/Grid.md
View file

@ -1,371 +0,0 @@
# 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
```