Game of Life in Idris

gol.idr

module GoL

%default total

data Cell = Alive | Dead

Board : Type
Board = Vect 3 (Vect 3 Cell)

nextCellState : Cell -> Nat -> Cell
nextCellState Alive (S (S Z))     = Alive
nextCellState _     (S (S (S Z))) = Alive
nextCellState _     _             = Dead

nextBoardState : Board -> Board
nextBoardState b = b

-- 0,0 :     0,1
--       1,0 1,1
--
-- 1,0 : 0,0     2,0
--       0,1 1,1 2,1
--
-- 0,1 : 0,0 1,0
--           1,1
--       0,2 1,2
--
-- 1,1 : 0,0 1,0 2,0
--       0,1     2,1
--       0,2 1,2 2,2
proximateNeighbors : Nat -> Nat -> List (Nat, Nat)
proximateNeighbors Z     Z     = [        (1, 0),
                                  (1, 0), (1, 1)]

proximateNeighbors (S x) Z     = [(x    , 0    ),                 (x + 2, 0    ),
                                  (x    , 1    ), (x + 1, 1    ), (x + 2,     1)]

proximateNeighbors Z     (S y) = [(0    , y    ), (1    , y    ),
                                                  (1    , y + 1),
                                  (0    , y + 2), (1    , y + 2)]

proximateNeighbors (S x) (S y) = [(x    , y    ), (x + 1, y    ), (x + 2, y    ),
                                  (x    , y + 1),                 (x + 2, y + 1),
                                  (x    , y + 2), (x + 1, y + 2), (x + 2, y + 2)]

myBoard : Board
myBoard = [[Dead, Alive, Dead],
           [Dead, Alive, Dead],
           [Dead, Alive, Dead]]