-- lean --run Sudoku.lean http://localhost:3000
-- Lean 4 standard library + curl. No Lake dependencies.
-- x = column, y = row (0–8); n = value (1–9); game.board[y][x].
-- Functional client: use the Game returned by game.move.
import Lean
open Lean

structure Game where
  id : String
  board : Array (Array Nat)
  baseUrl : String

def unwrap (value : Except String α) : IO α :=
  match value with
  | .ok result => pure result
  | .error message => throw (IO.userError message)

def request (base path method : String) (body : Option String := none) : IO Json := do
  let args := #["--silent", "--show-error", "--fail-with-body", "--max-time", "10",
    "--request", method, "--header", "Content-Type: application/json"]
  let args := match body with
    | some value => args ++ #["--data-raw", value]
    | none => args
  let result ← IO.Process.output { cmd := "curl", args := args ++ #["--url", base ++ path] }
  if result.exitCode != 0 then
    throw (IO.userError s!"curl {result.exitCode}: {result.stderr}{result.stdout}")
  unwrap (Json.parse result.stdout)

def newGame (baseUrl : String := "http://localhost:3000") : IO Game := do
  let created ← request baseUrl "/board" "POST"
  let id ← unwrap (created.getObjValAs? String "id")
  let data ← request baseUrl s!"/board/{id}" "GET"
  let board ← unwrap (data.getObjValAs? (Array (Array Nat)) "board")
  pure { id, board, baseUrl }

def Game.move (game : Game) (x y n : Nat) : IO Game := do
  if x > 8 || y > 8 || n < 1 || n > 9 then
    throw (IO.userError "x and y must be 0–8; n must be 1–9")
  let body := (Json.mkObj [("row", toJson y), ("col", toJson x), ("value", toJson n)]).compress
  let data ← request game.baseUrl s!"/board/{game.id}/turn" "PATCH" (some body)
  let board ← unwrap (data.getObjValAs? (Array (Array Nat)) "board")
  pure { game with board }

def main (args : List String) : IO Unit := do
  let game ← newGame (args.headD "http://localhost:3000")
  let game ← game.move 2 1 5
  IO.println (toJson game.board).compress