Idris type-level tic-tac-toe

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

data Move : Piece -> (Fin 3, Fin 3) -> Type where
  MkMove : (piece : Piece) -> (cs : (Fin 3, Fin 3)) -> Move piece cs

testBoard : Board
testBoard = [ [X, N, N]
            , [N, O, N]
            , [N, N, X] ]

possible : (board : Board) -> (cs : (Fin 3, Fin 3)) -> Bool
possible b (x, y) = case (Data.Vect.index x (Data.Vect.index y b)) of
                      N => True
                      _ => False

data TurnBoard : (board : Board) -> (player : Piece) -> Type where
  MkTurnBoard : (b : Board) -> (player : Piece) -> TurnBoard board player

newGameBoard : TurnBoard board X
newGameBoard = MkTurnBoard emptyBoard X
  where emptyBoard = [ [N, N, N]
                     , [N, N, N]
                     , [N, N, N] ]

play : (Fin 3, Fin 3) -> TurnBoard oldboard player -> TurnBoard newboard (next player)
play {player} (x, y) (MkTurnBoard board player) = MkTurnBoard board' (next player)
 where board' = updateAt y (updateAt x (place player)) board

(>>) : TurnBoard oldboard p -> Move p cs -> TurnBoard newboard (next p)
(>>) turn (MkMove p cs) = play cs turn

-- newGameBoard  >> MkMove X (0, 0)

todo: type-level validation with 'possible' and the current board