juvix/examples/milestone/TicTacToe/Logic/Game.juvix

--- Tic-tac-toe is a paper-and-pencil game for two players who take turns marking the spaces
--- in a three-by-three grid with X or O.
---
--- The player who succeeds in placing three of their marks in a horizontal, vertical, or
--- diagonal row is the winner. It is a solved game, with a forced draw assuming best play from both players.
---
module Logic.Game;

open import Stdlib.Data.Nat.Ord;
open import Stdlib.Prelude;

-- Render Utils

infixr 5 ++str;
--- Concatenation of ;String;s
axiom ++str : String → String → String;
compile ++str {
  c ↦ "concat";
};

--- Concatenates a list of strings
---
--- ;concat (("a" ∷ nil) ∷ ("b" ∷ nil)); evaluates to ;"a" ∷ "b" ∷ nil;
concat : List String → String;
concat ≔ foldl (++str) "";

surround : String → List String → List String;
surround x xs ≔ (x ∷ intersperse x xs) ++ (x ∷ nil);

intercalate : String → List String → String;
intercalate sep xs ≔ concat (intersperse sep xs);

--- Joins a list of strings with the newline character
unlines : List String → String;
unlines ≔ intercalate "\n";

-- Symbol

--- A symbol represents a token that can be placed in a square
inductive Symbol {
--- The circle token
  O : Symbol;
--- The cross token
  X : Symbol;
};

--- Equality for ;Symbol;s
==Symbol : Symbol → Symbol → Bool;
==Symbol O O ≔ true;
==Symbol X X ≔ true;
==Symbol _ _ ≔ false;

--- Turns ;O; into ;X; and ;X; into ;O;
switch : Symbol → Symbol;
switch O ≔ X;
switch X ≔ O;

--- Textual representation of a ;Symbol;
showSymbol : Symbol → String;
showSymbol O ≔ "O";
showSymbol X ≔ "X";

-- Square
--- A square is each of the holes in a board
inductive Square {
  --- An empty square has a ;ℕ; that uniquely identifies it
  empty : ℕ → Square;
  --- An occupied square has a ;Symbol; in it
  occupied : Symbol → Square;
};

-- --- A row in a board implemented as ;List Square;
-- ---
-- --- >>> Row;
-- Row : Type;
-- Row ≔ List Square;

-- A column in a board implemented as ;List Square;
-- Column : Type;
-- Column ≔ Row;

--- Equality for ;Square;s
==Square : Square → Square → Bool;
==Square (empty m) (empty n) ≔ m == n;
==Square (occupied s) (occupied t) ≔ ==Symbol s t;
==Square _ _ ≔ false;

--- Textual representation of a ;Square;
showSquare : Square → String;
showSquare (empty n) ≔ " " ++str natToStr n ++str " ";
showSquare (occupied s) ≔ " " ++str showSymbol s ++str " ";

-- TODO use a type alias?
--- A grid of squares
inductive Board {
  board : List (List Square) → Board;
};

--- Returns the list of numbers corresponding to the empty ;Square;s
possibleMoves : List Square → List ℕ;
possibleMoves nil ≔ nil;
possibleMoves ((empty n) ∷ xs) ≔ n ∷ possibleMoves xs;
possibleMoves (_ ∷ xs) ≔ possibleMoves xs;

--- ;true; if all the ;Square;s in the list are equal
full : List Square → Bool;
full (a ∷ b ∷ c ∷ nil) ≔ (==Square a b) && (==Square b c);

diagonals : List (List Square) → List (List Square);
diagonals ((a1 ∷ _ ∷ b1 ∷ nil) ∷ (_ ∷ c ∷ _ ∷ nil) ∷ (b2 ∷ _ ∷ a2 ∷ nil) ∷ nil) ≔ (a1 ∷ c ∷ a2 ∷ nil) ∷ (b1 ∷ c ∷ b2 ∷ nil) ∷ nil;

columns : List (List Square) → List (List Square);
columns ≔ transpose;

rows : List (List Square) → List (List Square);
rows ≔ id;

--- Textual representation of a ;(List Square);
showRow : (List Square) → String;
showRow xs ≔ concat (surround "|" (map showSquare xs));

showBoard : Board → String;
showBoard (board squares) ≔ unlines (surround "+---+---+---+" (map showRow squares));

-- Error

inductive Error {
--- no error occurred
  noError : Error;
--- a non-fatal error occurred
  continue : String → Error;
--- a fatal occurred
  terminate : String → Error;
};

-- GameState

inductive GameState {
  state : Board → Symbol → Error → GameState;
};

--- Textual representation of a ;GameState;
showGameState : GameState → String;
showGameState (state b _ _) ≔ showBoard b;

--- Projects the player
player : GameState → Symbol;
player (state _ p _) ≔ p;

--- initial ;GameState;
beginState : GameState;
beginState ≔ state
     (board (map (map empty) ((one ∷ two ∷ three ∷ nil) ∷ (four ∷ five ∷ six ∷ nil) ∷ (seven ∷ eight ∷ nine ∷ nil) ∷ nil)))
     X
     noError;

--- ;true; if some player has won the game
won : GameState → Bool;
won (state (board squares) _ _) ≔ any full (diagonals squares ++ rows squares ++ columns squares);

--- ;true; if there is a draw
draw : GameState → Bool;
draw (state (board squares) _ _) ≔ null (possibleMoves (flatten squares));

-- Move

replace : Symbol → ℕ → Square → Square;
replace player k (empty n) ≔ if (n Stdlib.Data.Nat.Ord.== k) (occupied player) (empty n);
replace _ _ s ≔ s;

checkState : GameState → GameState;
checkState (state b p e) ≔
  if (won (state b p e))
     (state b p (terminate ("Player " ++str (showSymbol (switch p)) ++str " wins!")))
     (if (draw (state b p e))
         (state b p (terminate "It's a draw!"))
         (state b p e));

playMove : Maybe ℕ → GameState → GameState;
playMove nothing (state b p _) ≔
    state b p (continue "\nInvalid number, try again\n");
playMove (just k) (state (board s) player e) ≔
    if (not (elem (==) k (possibleMoves (flatten s))))
        (state (board s) player (continue "\nThe square is already occupied, try again\n"))
        (checkState (state (board (map (map (replace player k)) s))
                           (switch player)
                           noError));

validMove : ℕ → Maybe ℕ;
validMove n ≔ if ((n <= nine) && (n >= one)) (just n) nothing;

end;