Revision of tic-tac-toe.maude

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

capitalex / tic-tac-toe.maude

capitalex revised this gist 1733714378. Go to revision

		@@ -0,0 +1,243 @@
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