Skip to content

Instantly share code, notes, and snippets.

@clojj
Last active Oct 12, 2017
Embed
What would you like to do?
Idris type-level tic-tac-toe
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)
@clojj

This comment has been minimized.

Copy link
Owner Author

@clojj clojj commented Oct 12, 2017

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment