Minesweeper.idr

module Minesweeper

import Data.Fin
import Data.Vect

data Board : Type where
     MkBoard : (rows : Nat) ->
               (cols : Nat) ->
               (mines : List (Fin rows, Fin cols)) ->
               Board

Projection : Nat -> Nat -> Type
Projection rows cols = Vect rows (Vect cols Bool)

empty_projection : (rows : Nat) -> (cols : Nat) -> Projection rows cols
empty_projection rows cols = replicate rows (replicate cols False)

add_mine : Projection rows cols -> (Fin rows, Fin cols) -> Projection rows cols
add_mine projection (row, col) = updateAt row (replaceAt col True) projection

-- These boardGetters seem awful
boardRows : Board -> Nat
boardRows (MkBoard rows cols mines) = rows

boardCols : Board -> Nat
boardCols (MkBoard rows cols mines) = cols

project : (board : Board) -> Projection (boardRows board) (boardCols board)
project (MkBoard rows cols []) = empty_projection rows cols
project (MkBoard rows cols (mine :: mines)) = add_mine (project (MkBoard rows cols \
mines)) mine

sampleBoard : Board
sampleBoard = MkBoard 2 3 [(1, 1)]

sampleProjection : Projection 2 3
sampleProjection = project sampleBoard