Every possible game of Tic Tac Toe! This was a bit hard to prove total…

AllTicTacToe.idr

import Data.Vect
%default total


||| A player in the Tic Tac Toe game
data Move = X | O

implementation Eq Move where
  X == X = True
  O == O = True
  _ == _ = False

next : Move -> Move
next X = O
next O = X


||| A List that encodes how many open spaces remain in it
data GapList : (n : Nat) -> (m : Nat) -> Type -> Type where
  Nil : GapList Z Z a
  Gap : GapList n k a -> GapList (S n) (S k) a
  Item : a -> GapList n k a -> GapList (S n) k a

||| Index the GapList, giving Nothing if you index into a gap
idx : Fin n -> GapList n k a -> Maybe a
idx FZ (Gap _) = Nothing
idx FZ (Item x _) = Just x
idx (FS k) (Gap xs) = idx k xs
idx (FS k) (Item _ xs) = idx k xs

||| Produce a vector of all the ways to fill one spot in the GapList
fillGap : a -> GapList n (S k) a -> Vect (S k) (GapList n k a)
fillGap y (Gap    xs) {k=Z}   = [Item y xs]
fillGap y (Gap    xs) {k=S _} = Item y xs :: (Gap <$> fillGap y xs)
fillGap y (Item x xs)         = Item x <$> fillGap y xs


||| A Tic Tac Toe board with k open spaces
Board : Nat -> Type
Board k = GapList 9 k Move

||| An empty Tic Tac Toe board
emptyBoard : Board 9
emptyBoard = (Gap . Gap . Gap) . (Gap . Gap . Gap) . (Gap . Gap . Gap) $ []


||| A tree of Tic Tac Toe games with at most (S k) levels
data GameTree : Nat -> Type where
  Done : Maybe Move -> Board k -> GameTree k
  Play : Board (S k) -> Vect (S k) (GameTree k) -> GameTree (S k)

||| Returns the winner of the Tic Tac Toe game, or Nothing if there's no winner
winner : Board k -> Maybe Move
winner b = find (isRun b) winningPositions >>= \(k, _, _) => idx k b
  where
    winningPositions : Vect 8 (Fin 9, Fin 9, Fin 9)
    winningPositions = [
      (0, 1, 2), (3, 4, 5), (6, 7, 8), -- rows
      (0, 3, 6), (1, 4, 7), (2, 5, 8), -- cols
      (0, 4, 8), (2, 4, 6)             -- diagonals
    ]

    isRun : Board k -> (Fin 9, Fin 9, Fin 9) -> Bool
    isRun b (k, n, m) = idx k b /= Nothing && idx k b == idx n b && idx n b == idx m b

||| Produce a GameTree starting at the given Move and Board
play : Move -> Board k -> GameTree k
play {k=Z}   _ b = Done (winner b) b
play {k=S _} m b =
  case winner b of
    Nothing => Play b (play (next m) <$> fillGap m b)
    Just win => Done (Just win) b


implementation Show (GameTree k) where
  show = show' ""
    where
      showMove : Maybe Move -> String
      showMove Nothing = " "
      showMove (Just X) = "X"
      showMove (Just O) = "O"

      shidx : Fin 9 -> Board k -> String
      shidx k b = showMove (idx k b)

      showGame : String -> Board k -> String
      showGame pad b =
        pad ++ shidx 0 b ++ shidx 1 b ++ shidx 2 b ++ "\n" ++
        pad ++ shidx 3 b ++ shidx 4 b ++ shidx 5 b ++ "\n" ++
        pad ++ shidx 6 b ++ shidx 7 b ++ shidx 8 b ++ "\n"

      show' : String -> GameTree k -> String
      show' pad (Done Nothing b) = pad ++ "Tie Game:\n" ++ showGame pad b
      show' pad (Done (Just win) b) =
        pad ++ "Winner: " ++ showMove (Just win) ++ "\n" ++ showGame pad b
      show' pad (Play b xs) =
        let subtrees = show' (pad ++ "  ") <$> xs in
        showGame pad b ++ foldl (\acc, x => acc ++ "\n" ++ x) "" subtrees

stats : GameTree k -> (Nat, Nat, Nat)
stats (Play x xs) = foldl (\(a, b, c), (x, y, z) => (a + x, b + y, c + z)) (0, 0, 0) (stats <$> xs)
stats (Done w  _) = toTup w
  where
    toTup : Maybe Move -> (Nat, Nat, Nat)
    toTup Nothing  = (1, 0, 0)
    toTup (Just X) = (0, 1, 0)
    toTup (Just O) = (0, 0, 1)


testBoard : Board 5
testBoard = Item X $ Gap $ Item O $ Gap $ Item O $ Gap $ Gap $ Gap $ Item X []

main : IO ()
main = do
  let games = play X emptyBoard
  let (cat, x, o) = stats games
  putStrLn $ "Cat: " ++ show cat ++ ", X: " ++ show x ++ ", O: " ++ show o
  print games