tictactoe.idr

module TicTacToe

import Data.Vect

||| All possible player pieces, where N represents empty
data Piece = X | O | N

||| Select next player 
next : Piece -> Piece
next X = O
next O = X
next N = N

||| Place a new piece in a cell if it's empy.
place : (new : Piece) -> (old : Piece) -> Piece
place x' N = x'
place x' x = x

||| Type representing a 3x3 board
Board : Type
Board = Vect 3 $ Vect 3 Piece

||| A turn holds a board and has to be played by a certain player.
data Turn : (player : Piece) -> Type where
  MkTurn : (board : Board) -> Turn player

||| A new game, where player X starts on an empty board.
newGame : Turn X
newGame = MkTurn emptyBoard
  where emptyBoard = [ [N, N, N]
                     , [N, N, N]
                     , [N, N, N] ]
             
||| Place a player's piece in the given coordinates, and return the updated
||| board for the next player's turn.
play : (Fin 3, Fin 3) -> Turn player -> Turn (next player)
play {player} (x, y) (MkTurn board) = MkTurn board'
  where board' = updateAt y (updateAt x (place player)) board

||| Convenience function to play and represent games
(>>) : Turn p -> (Fin 3, Fin 3) -> Turn (next p)
(>>) b cs = play cs b

-- example game: newGame >> (0, 0) >> (1, 0) >> (1, 1) >> (2, 0) >> (2, 2)