--- 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;

  axiom readline : String;

  compile readline {
    c  "readline()";
  };

  axiom parsePositiveInt : String  Nat;

  compile parsePositiveInt {
    c  "parsePositiveInt";
  };

  getMove : Maybe Nat;
  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;