omod TIC-TAC-TOE is including STD-STREAM . including NAT . sorts Player X O . subsorts X O < Player . op Xs : -> X . op Os : -> O . op next-player : Player -> Player . eq next-player(Xs) = Os . eq next-player(Os) = Xs . sorts Cell Row Grid . op ___ : Cell Cell Cell -> Row . op _ : -> Cell [format (! o)] . op x : -> Cell [format (b! o)] . op o : -> Cell [format (r! o)] . op is-empty : Cell -> [Bool] . eq is-empty(_) = true . eq is-empty(x) = false . eq is-empty(o) = false . op to-cell : Player -> Cell . eq to-cell(Xs) = x . eq to-cell(Os) = o . sort GameState . ops read-row read-column show-grid wait-show-grid wait-make-turn check-win : -> GameState . class GameClass | turn : Player , state : GameState . class RowClass | index : Nat , cells : Row . ops Game Row1 Row2 Row3 : -> Oid . op RowX : -> Oid . op play : -> Configuration . var S : String . var O : Oid . var P : Player . vars N M : Nat . vars R1 R2 R3 : Row . vars C1 C2 C3 C4 C5 C6 C7 C8 C9 : Cell . op has-won : Row Row Row -> [Bool] . ceq has-won((C1 C1 C1), R2, R3) = true if C1 =/= _ . ceq has-won(R1, (C1 C1 C1), R3) = true if C1 =/= _ . ceq has-won(R1, R2, (C1 C1 C1)) = true if C1 =/= _ . ceq has-won((C1 C2 C3), (C1 C5 C6), (C1 C8 C9)) = true if C1 =/= _ . ceq has-won((C1 C2 C3), (C4 C2 C6), (C7 C2 C9)) = true if C2 =/= _ . ceq has-won((C1 C2 C3), (C4 C5 C3), (C7 C8 C3)) = true if C3 =/= _ . ceq has-won((C1 C2 C3), (C4 C1 C6), (C7 C8 C1)) = true if C1 =/= _ . ceq has-won((C1 C2 C3), (C4 C3 C6), (C3 C8 C9)) = true if C3 =/= _ . eq has-won(R1, R2, R3) = false . op to-string(_) : Cell -> String . eq to-string(_) = " _ " . eq to-string(x) = " x " . eq to-string(o) = " o " . op to-string(_) : Player -> String . eq to-string(Xs) = "Xs" . eq to-string(Os) = "Os" . --- serious? the new line is in the string ._. op to-index(_) : String -> Nat . eq to-index("1\n") = 1 . eq to-index("2\n") = 2 . eq to-index("3\n") = 3 . op show-row : Oid Nat -> Msg . op show-row-iter : Nat -> Msg . op print-cells : String -> Msg . op wait-for-print-cells : Nat -> Msg . ops turn-row turn-column : Nat -> Msg . op target-row : Row Nat -> Msg . eq play = <> < Game : GameClass | turn : Xs, state : show-grid > < Row1 : RowClass | index : 1, cells : _ _ _ > < Row2 : RowClass | index : 2, cells : _ _ _ > < Row3 : RowClass | index : 3, cells : _ _ _ > . rl [show-grid] : < Game : GameClass | state : show-grid > => < Game : GameClass | state : wait-show-grid > show-row(Row1, 3) show-row(Row2, 2) show-row(Row3, 1) show-row-iter(3) . rl [show-row] : show-row-iter(N) show-row(O, N) < O : RowClass | cells : (C1 C2 C3) > => < O : RowClass | cells : (C1 C2 C3) > print-cells(to-string(C1) + to-string(C2) + to-string(C3)) wait-for-print-cells(N) . rl [print-cells] : print-cells(S) wait-for-print-cells(s N) < Game : GameClass | > => write(stdout, Game, S + "\n") < Game : GameClass | > show-row-iter(N) . rl [start-turn] : < Game : GameClass | state : wait-show-grid > show-row-iter(0) => < Game : GameClass | state : read-column > getLine(stdin, Game, "Enter column: ") . rl [column-retry] : < Game : GameClass | state : read-column > gotLine(Game, O, S) => if S == "1\n" or S == "2\n" or S == "3\n" then < Game : GameClass | state : read-row > turn-column(to-index(S)) getLine(stdin, Game, "Enter row: ") else < Game : GameClass | state : read-column > getLine(stdin, Game, "Enter column: ") fi . rl [column-retry] : < Game : GameClass | state : read-row > gotLine(Game, O, S) => if S == "1\n" or S == "2\n" or S == "3\n" then < Game : GameClass | state : wait-make-turn > turn-row(to-index(S)) else < Game : GameClass | state : read-row > getLine(stdin, Game, "Enter row: ") fi . rl [update-column-1] : turn-column(1) turn-row(N) < O : RowClass | index : N, cells : (C1 C2 C3) > < Game : GameClass | turn : P, state : wait-make-turn > => if is-empty(C1) then < O : RowClass | index : N, cells : (to-cell(P) C2 C3) > < Game : GameClass | turn : P, state : check-win > else < O : RowClass | index : N, cells : (C1 C2 C3) > < Game : GameClass | turn : P, state : read-column > getLine(stdin, Game, "Enter column: ") fi . rl [update-column-1] : turn-column(2) turn-row(N) < O : RowClass | index : N, cells : (C1 C2 C3) > < Game : GameClass | turn : P, state : wait-make-turn > => if is-empty(C2) then < O : RowClass | index : N, cells : (C1 to-cell(P) C3) > < Game : GameClass | turn : P, state : check-win > else < O : RowClass | index : N, cells : (C1 C2 C3) > < Game : GameClass | turn : P, state : read-column > getLine(stdin, Game, "Enter column: ") fi . rl [update-column-1] : turn-column(3) turn-row(N) < O : RowClass | index : N, cells : (C1 C2 C3) > < Game : GameClass | turn : P, state : wait-make-turn > => if is-empty(C3) then < O : RowClass | index : N, cells : (C1 C2 to-cell(P)) > < Game : GameClass | turn : P, state : check-win > else < O : RowClass | index : N, cells : (C1 C2 C3) > < Game : GameClass | turn : P, state : read-column > getLine(stdin, Game, "Enter column: ") fi . rl [check-win] : < Row1 : RowClass | cells : R1 > < Row2 : RowClass | cells : R2 > < Row3 : RowClass | cells : R3 > < Game : GameClass | turn : P, state : check-win > => if has-won(R1, R2, R3) then write(stdout, Game, to-string(P) + " Wins!\n") else < Row1 : RowClass | cells : R1 > < Row2 : RowClass | cells : R2 > < Row3 : RowClass | cells : R3 > < Game : GameClass | turn : next-player(P), state : show-grid > fi . rl [clean-up] : wrote(O, stdout) => none . endom