fresh start on typed tic tac toe

ttt.idr

module TicTacToe

import Data.Vect

data Piece = X | O | N

next : Piece -> Piece
next X = O
next O = X
next N = N

place : (new : Piece) -> (old : Piece) -> Piece
place x' N = x'
place x' x = x

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 -> Piece -> Type where
  MkTurnBoard : (board : Board) -> (piece : Piece) -> TurnBoard board piece

emptyBoard : Board
emptyBoard = [ [N, N, N]
             , [N, N, N]
             , [N, N, N] ]

newGameBoard : TurnBoard TicTacToe.emptyBoard X

play : (Fin 3, Fin 3) -> TurnBoard board piece -> TurnBoard board' (next piece)
play (x, y) (MkTurnBoard b piece) = MkTurnBoard b' (next piece)
 where b' = updateAt y (updateAt x (place p)) b
--
-- (>>) : TurnBoard oldboard p -> Move p cs -> TurnBoard newboard (next p)
-- (>>) turn (MkMove p cs) = play cs turn

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