Thinking with Types: TicTacToe

q.lean

import data.string.basic
import system.io

def unlines := string.intercalate "\n"
def unwords := string.intercalate " "

abbreviation ix := fin 3
namespace ix
def op : ix → ix
| ⟨0, _⟩ := 2
| ⟨1, _⟩ := 1
| ⟨2, _⟩ := 0
| ⟨_, _⟩ := 0
instance : has_neg ix := ⟨op⟩
end ix

def board (α : Type) := ix → ix → α
namespace board
  variable {α : Type}

  def rot_right : board α → board α
  | b x y := b (-y) x

  def empty : board (option bool)
  | _ _ := none

  def place : board α → ix → ix → α → board α
  | b x y t x₁ y₁ := if x = x₁ ∧ y = y₁ then t else b x₁ y₁

  def to_string [has_to_string α] : board α → string
  | b :=
    unlines $
      [ [b 0 0, b 0 1, b 0 2]
      , [b 1 0, b 1 1, b 1 2]
      , [b 2 0, b 2 1, b 2 2]
      ].map (unwords ∘ list.map (has_to_string.to_string))

  instance [has_to_string α] : has_to_string (board α) := ⟨to_string⟩
end board

def main : io unit := do
  io.print_ln (board.empty.place 0 1 (some true)).rot_right