diff --git a/advent.ipkg b/advent.ipkg index c9776ba..189172e 100644 --- a/advent.ipkg +++ b/advent.ipkg @@ -28,7 +28,6 @@ modules = Runner , Util , Util.Eff , Util.Digits - , Grid -- main file (i.e. file to load at REPL) main = Main diff --git a/src/Grid.md b/src/Grid.md deleted file mode 100644 index ceb6a22..0000000 --- a/src/Grid.md +++ /dev/null @@ -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 -```