tic-tac-toe.maude
· 6.7 KiB · Text
原始檔案
Playground
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
| 1 | omod TIC-TAC-TOE is |
| 2 | including STD-STREAM . |
| 3 | including NAT . |
| 4 | |
| 5 | sorts Player X O . |
| 6 | subsorts X O < Player . |
| 7 | |
| 8 | op Xs : -> X . op Os : -> O . |
| 9 | op next-player : Player -> Player . |
| 10 | eq next-player(Xs) = Os . |
| 11 | eq next-player(Os) = Xs . |
| 12 | |
| 13 | sorts Cell Row Grid . |
| 14 | |
| 15 | op ___ : Cell Cell Cell -> Row . |
| 16 | |
| 17 | op _ : -> Cell [format (! o)] . |
| 18 | op x : -> Cell [format (b! o)] . |
| 19 | op o : -> Cell [format (r! o)] . |
| 20 | |
| 21 | op is-empty : Cell -> [Bool] . |
| 22 | eq is-empty(_) = true . |
| 23 | eq is-empty(x) = false . |
| 24 | eq is-empty(o) = false . |
| 25 | |
| 26 | op to-cell : Player -> Cell . |
| 27 | eq to-cell(Xs) = x . |
| 28 | eq to-cell(Os) = o . |
| 29 | |
| 30 | sort GameState . |
| 31 | |
| 32 | ops read-row |
| 33 | read-column |
| 34 | show-grid |
| 35 | wait-show-grid |
| 36 | wait-make-turn |
| 37 | check-win |
| 38 | : -> GameState . |
| 39 | |
| 40 | class GameClass |
| 41 | | turn : Player |
| 42 | , state : GameState |
| 43 | . |
| 44 | |
| 45 | class RowClass |
| 46 | | index : Nat |
| 47 | , cells : Row |
| 48 | . |
| 49 | |
| 50 | ops Game Row1 Row2 Row3 : -> Oid . |
| 51 | op RowX : -> Oid . |
| 52 | op play : -> Configuration . |
| 53 | |
| 54 | var S : String . |
| 55 | var O : Oid . |
| 56 | var P : Player . |
| 57 | vars N M : Nat . |
| 58 | vars R1 R2 R3 : Row . |
| 59 | vars C1 C2 C3 C4 C5 C6 C7 C8 C9 : Cell . |
| 60 | |
| 61 | op has-won : Row Row Row -> [Bool] . |
| 62 | ceq has-won((C1 C1 C1), R2, R3) = true |
| 63 | if C1 =/= _ . |
| 64 | ceq has-won(R1, (C1 C1 C1), R3) = true |
| 65 | if C1 =/= _ . |
| 66 | ceq has-won(R1, R2, (C1 C1 C1)) = true |
| 67 | if C1 =/= _ . |
| 68 | ceq has-won((C1 C2 C3), (C1 C5 C6), (C1 C8 C9)) = true |
| 69 | if C1 =/= _ . |
| 70 | ceq has-won((C1 C2 C3), (C4 C2 C6), (C7 C2 C9)) = true |
| 71 | if C2 =/= _ . |
| 72 | ceq has-won((C1 C2 C3), (C4 C5 C3), (C7 C8 C3)) = true |
| 73 | if C3 =/= _ . |
| 74 | ceq has-won((C1 C2 C3), (C4 C1 C6), (C7 C8 C1)) = true |
| 75 | if C1 =/= _ . |
| 76 | ceq has-won((C1 C2 C3), (C4 C3 C6), (C3 C8 C9)) = true |
| 77 | if C3 =/= _ . |
| 78 | eq has-won(R1, R2, R3) = false . |
| 79 | |
| 80 | op to-string(_) : Cell -> String . |
| 81 | eq to-string(_) = " _ " . |
| 82 | eq to-string(x) = " x " . |
| 83 | eq to-string(o) = " o " . |
| 84 | |
| 85 | op to-string(_) : Player -> String . |
| 86 | eq to-string(Xs) = "Xs" . |
| 87 | eq to-string(Os) = "Os" . |
| 88 | |
| 89 | --- serious? the new line is in the string ._. |
| 90 | op to-index(_) : String -> Nat . |
| 91 | eq to-index("1\n") = 1 . |
| 92 | eq to-index("2\n") = 2 . |
| 93 | eq to-index("3\n") = 3 . |
| 94 | |
| 95 | op show-row : Oid Nat -> Msg . |
| 96 | op show-row-iter : Nat -> Msg . |
| 97 | |
| 98 | op print-cells : String -> Msg . |
| 99 | op wait-for-print-cells : Nat -> Msg . |
| 100 | |
| 101 | ops turn-row turn-column : Nat -> Msg . |
| 102 | |
| 103 | op target-row : Row Nat -> Msg . |
| 104 | |
| 105 | eq play = <> |
| 106 | < Game : GameClass | turn : Xs, state : show-grid > |
| 107 | < Row1 : RowClass | index : 1, cells : _ _ _ > |
| 108 | < Row2 : RowClass | index : 2, cells : _ _ _ > |
| 109 | < Row3 : RowClass | index : 3, cells : _ _ _ > |
| 110 | . |
| 111 | |
| 112 | rl [show-grid] : |
| 113 | < Game : GameClass | state : show-grid > |
| 114 | => |
| 115 | < Game : GameClass | state : wait-show-grid > |
| 116 | show-row(Row1, 3) |
| 117 | show-row(Row2, 2) |
| 118 | show-row(Row3, 1) |
| 119 | show-row-iter(3) |
| 120 | . |
| 121 | |
| 122 | rl [show-row] : |
| 123 | show-row-iter(N) |
| 124 | show-row(O, N) |
| 125 | < O : RowClass | cells : (C1 C2 C3) > |
| 126 | => |
| 127 | < O : RowClass | cells : (C1 C2 C3) > |
| 128 | print-cells(to-string(C1) + to-string(C2) + to-string(C3)) |
| 129 | wait-for-print-cells(N) |
| 130 | . |
| 131 | |
| 132 | rl [print-cells] : |
| 133 | print-cells(S) |
| 134 | wait-for-print-cells(s N) |
| 135 | < Game : GameClass | > |
| 136 | => |
| 137 | write(stdout, Game, S + "\n") |
| 138 | < Game : GameClass | > |
| 139 | show-row-iter(N) |
| 140 | . |
| 141 | |
| 142 | rl [start-turn] : |
| 143 | < Game : GameClass | state : wait-show-grid > |
| 144 | show-row-iter(0) |
| 145 | => |
| 146 | < Game : GameClass | state : read-column > |
| 147 | getLine(stdin, Game, "Enter column: ") |
| 148 | . |
| 149 | |
| 150 | rl [column-retry] : |
| 151 | < Game : GameClass | state : read-column > |
| 152 | gotLine(Game, O, S) |
| 153 | => |
| 154 | if S == "1\n" or S == "2\n" or S == "3\n" then |
| 155 | < Game : GameClass | state : read-row > |
| 156 | turn-column(to-index(S)) |
| 157 | getLine(stdin, Game, "Enter row: ") |
| 158 | else |
| 159 | < Game : GameClass | state : read-column > |
| 160 | getLine(stdin, Game, "Enter column: ") |
| 161 | fi |
| 162 | . |
| 163 | |
| 164 | rl [column-retry] : |
| 165 | < Game : GameClass | state : read-row > |
| 166 | gotLine(Game, O, S) |
| 167 | => |
| 168 | if S == "1\n" or S == "2\n" or S == "3\n" then |
| 169 | < Game : GameClass | state : wait-make-turn > |
| 170 | turn-row(to-index(S)) |
| 171 | else |
| 172 | < Game : GameClass | state : read-row > |
| 173 | getLine(stdin, Game, "Enter row: ") |
| 174 | fi |
| 175 | . |
| 176 | |
| 177 | rl [update-column-1] : turn-column(1) |
| 178 | turn-row(N) |
| 179 | < O : RowClass | index : N, cells : (C1 C2 C3) > |
| 180 | < Game : GameClass | turn : P, state : wait-make-turn > |
| 181 | => |
| 182 | if is-empty(C1) then |
| 183 | < O : RowClass | index : N, cells : (to-cell(P) C2 C3) > |
| 184 | < Game : GameClass | turn : P, state : check-win > |
| 185 | else |
| 186 | < O : RowClass | index : N, cells : (C1 C2 C3) > |
| 187 | < Game : GameClass | turn : P, state : read-column > |
| 188 | getLine(stdin, Game, "Enter column: ") |
| 189 | fi |
| 190 | . |
| 191 | |
| 192 | rl [update-column-1] : turn-column(2) |
| 193 | turn-row(N) |
| 194 | < O : RowClass | index : N, cells : (C1 C2 C3) > |
| 195 | < Game : GameClass | turn : P, state : wait-make-turn > |
| 196 | => |
| 197 | if is-empty(C2) then |
| 198 | < O : RowClass | index : N, cells : (C1 to-cell(P) C3) > |
| 199 | < Game : GameClass | turn : P, state : check-win > |
| 200 | else |
| 201 | < O : RowClass | index : N, cells : (C1 C2 C3) > |
| 202 | < Game : GameClass | turn : P, state : read-column > |
| 203 | getLine(stdin, Game, "Enter column: ") |
| 204 | fi |
| 205 | . |
| 206 | |
| 207 | rl [update-column-1] : turn-column(3) |
| 208 | turn-row(N) |
| 209 | < O : RowClass | index : N, cells : (C1 C2 C3) > |
| 210 | < Game : GameClass | turn : P, state : wait-make-turn > |
| 211 | => |
| 212 | if is-empty(C3) then |
| 213 | < O : RowClass | index : N, cells : (C1 C2 to-cell(P)) > |
| 214 | < Game : GameClass | turn : P, state : check-win > |
| 215 | else |
| 216 | < O : RowClass | index : N, cells : (C1 C2 C3) > |
| 217 | < Game : GameClass | turn : P, state : read-column > |
| 218 | getLine(stdin, Game, "Enter column: ") |
| 219 | fi |
| 220 | . |
| 221 | |
| 222 | rl [check-win] : |
| 223 | < Row1 : RowClass | cells : R1 > |
| 224 | < Row2 : RowClass | cells : R2 > |
| 225 | < Row3 : RowClass | cells : R3 > |
| 226 | < Game : GameClass | turn : P, state : check-win > |
| 227 | => |
| 228 | if has-won(R1, R2, R3) then |
| 229 | write(stdout, Game, to-string(P) + " Wins!\n") |
| 230 | else |
| 231 | < Row1 : RowClass | cells : R1 > |
| 232 | < Row2 : RowClass | cells : R2 > |
| 233 | < Row3 : RowClass | cells : R3 > |
| 234 | < Game : GameClass | turn : next-player(P), state : show-grid > |
| 235 | fi |
| 236 | . |
| 237 | |
| 238 | rl [clean-up] : |
| 239 | wrote(O, stdout) |
| 240 | => |
| 241 | none |
| 242 | . |
| 243 | endom |