juvix/examples/milestone/TicTacToe/CLI/TicTacToe.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.
---
--- The module Logic.Game contains the game logic.
module CLI.TicTacToe;

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

-- IO Utils

axiom readline : String;
compile readline {
  c ↦ "readline()";
};

axiom parsePositiveInt : String → ℕ;

compile parsePositiveInt {
  c ↦ "parsePositiveInt";
};

-- IO

getMove : Maybe ℕ;
getMove ≔ validMove (parsePositiveInt (readline));

do : IO × GameState -> GameState;
do (_ , s) ≔ playMove getMove s;

prompt : GameState → String;
prompt x ≔ "\n" ++str (showGameState x) ++str "\nPlayer " ++str showSymbol (player x) ++str ": ";

terminating
run : (IO × GameState → GameState) → GameState → IO;
run _ (state b p (terminate msg)) ≔ putStrLn ("\n" ++str (showGameState (state b p noError)) ++str "\n" ++str msg);
run f (state b p (continue msg)) ≔ run f (f (putStr (msg ++str prompt (state b p noError)) , state b p noError));
run f x ≔ run f (f (putStr (prompt x) , x));

--- The welcome message
welcome : String;
welcome ≔ "MiniTicTacToe\n-------------\n\nType a number then ENTER to make a move";

--- The entry point of the program
main : IO;
main ≔ putStrLn welcome >> run do beginState;
end;