TicTacToe.agda

module TicTacToe where

open import Data.Bool
  using (Bool; true; false; _∧_; _∨_)
open import Data.Empty
  using (⊥-elim)
open import Data.Fin
  using (Fin; zero; suc)
open import Data.Maybe
  using (Maybe; just; nothing)
open import Data.Nat
  using (ℕ; zero; suc; _<_; z≤n; s≤s)
open import Data.Product
  using (Σ; Σ-syntax; ∃; _×_; _,_; ,_; map)
open import Relation.Binary.PropositionalEquality
  using (_≢_; inspect; [_])

data Player : Set where
  x o : Player

infixl 1 _!_
infix  3 _≟_
infixr 4 _∷_ -∷_

data SquareVec : (len : ℕ) (empty : ℕ) → Set where
  []  :                                        SquareVec 0 0
  -∷_ : ∀ {l e}              → SquareVec l e → SquareVec (suc l) (suc e)
  _∷_ : ∀ {l e} (p : Player) → SquareVec l e → SquareVec (suc l) e

move : ∀ {l e} → Player → SquareVec l (suc e) → Fin (suc e) → SquareVec l e
move             p (  -∷ sqv) zero     = p  ∷ sqv
move {e = zero}  p (  -∷ _  ) (suc ())
move {e = suc e} p (  -∷ sqv) (suc fe) =   -∷ move p sqv fe
move             p (p′ ∷ sqv) fe       = p′ ∷ move p sqv fe

empty : ∀ {n} → SquareVec n n
empty {zero}  = []
empty {suc _} = -∷ empty


data Game : ∀ {e} → SquareVec 9 e → Set where
  start  :                                             Game empty
  move-p : ∀ {e} {gs} p (fe : Fin (suc e)) → Game gs → Game (move p gs fe)

data Result : Set where
  win  : Player → Result
  draw :          Result

data State : Set where
  ended : Result → State
  going :          State


_≟_ : (p₁ p₂ : Player) → Bool
x ≟ x = true
x ≟ o = false
o ≟ x = false
o ≟ o = true

_!_ : ∀ {n e} → SquareVec n e → ℕ → Maybe Player
[]     ! n     = nothing
-∷  _  ! zero  = nothing
-∷  xs ! suc n = xs ! n
p ∷ _  ! zero  = just p
_ ∷ xs ! suc n = xs ! n

check3 : ∀ {e} → Player → SquareVec 9 e → (a b c : ℕ) → Bool
check3 p sqv a b c = check (sqv ! a) ∧ check (sqv ! b) ∧ check (sqv ! c)
  where
  check : Maybe Player → Bool
  check (just p′) = p ≟ p′
  check nothing   = false

win? : ∀ {e} → Player → SquareVec 9 e → Bool
win? p sqv =
  check 0 1 2 ∨ check 3 4 5 ∨ check 6 7 8 ∨
  check 0 3 6 ∨ check 1 4 7 ∨ check 2 5 8 ∨
  check 0 4 8 ∨ check 2 4 6
  where
  check = check3 p sqv

result : ∀ {e} → SquareVec 9 e → Result
result sqv with win? x sqv
... | true  = win x
... | false with win? o sqv
...   | true  = win o
...   | false = draw

gameState : ∀ {e} {gs : SquareVec 9 e} → Game gs → State
gameState {zero}  {gs} _ = ended (result gs)
gameState {suc e} {gs} _ with result gs
gameState {suc e}      _ | win p = ended (win p)
gameState {suc e}      _ | draw  = going

game-ended : {gs : SquareVec 9 0} (g : Game gs) → gameState g ≢ going
game-ended _ ()

AI : Set
AI = ∀ {e} {sqv : SquareVec 9 (suc e)} → Game sqv → Fin (suc e)

∃Game : Set
∃Game = ∃ λ e → Σ (SquareVec 9 e) Game

gameMaster : ∀ {e} {sqv : SquareVec 9 e} (sp : Player)
  (x-move o-move : AI) → Game sqv → Result × ∃Game
gameMaster sp xAI oAI g with gameState g | inspect gameState g
... | ended s | _ = s , , , g
gameMaster {zero}  sp xAI oAI g | going | [ eq ] = ⊥-elim (game-ended g eq)
gameMaster {suc e} x  xAI oAI g | going | _      = gameMaster o xAI oAI (move-p x (xAI g) g)
gameMaster {suc e} o  xAI oAI g | going | _      = gameMaster x xAI oAI (move-p o (oAI g) g)


player-lowest : AI
player-lowest _ = zero

max : ∀ {e} → Fin (suc e)
max {zero}  = zero
max {suc e} = suc max

player-highest : AI
player-highest _ = max