Skip to content

Instantly share code, notes, and snippets.

@clojj
Created Sep 29, 2017
Embed
What would you like to do?
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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment