1	import Base
2	import ./types.bend as T
3	import ./board.bend as B
4	import ./solver.bend as S
5	
6	# The game. LAWS.bend states what it must do; PROOF.bend proves it does.
7	
8	# The real mines, the cells revealed so far, the player's flags (any cells;
9	# only hidden ones count as flagged) and the status.
10	type Game is Data:
11	  Game{w: Nat, h: Nat, layout: T.Grid(Bool), shown: T.Grid(Bool),
12	    flags: List<&2, T.Pos>, status: T.Status}
13	
14	# Accessors
15	# ---------
16	
17	def status(g: Game) -> T.Status:
18	  match g:
19	    case Game{w, h, layout, shown, flags, status}:
20	      status
21	
22	def is_playing(s: T.Status) -> Bool:
23	  match s:
24	    case T.Playing{}:
25	      True{}
26	    case o:
27	      False{}
28	
29	# p is a cell of the board that is not revealed yet.
30	def unrevealed(+w: Nat, +h: Nat, shown: T.Grid(Bool), +p: T.Pos) -> Bool:
31	  B.on_board(w, h, p) && Bool.not(B.at(Bool, False{}, shown, p))
32	
33	def flagged(g: Game, +p: T.Pos) -> Bool:
34	  match g:
35	    case Game{w, h, layout, shown, flags, status}:
36	      unrevealed(w, h, shown, p) && B.contains(flags, p)
37	
38	# What the player sees at p.
39	def seen_pick(s: Bool, m: Bool, w: Nat, h: Nat, layout: T.Grid(Bool), p: T.Pos) -> T.Seen:
40	  match s m:
41	    case False{} _:
42	      T.Hidden{}
43	    case True{} True{}:
44	      T.Boom{}
45	    case True{} False{}:
46	      T.Shown{B.adj_mines(w, h, layout, p)}
47	
48	def seen_at(+w: Nat, +h: Nat, +layout: T.Grid(Bool), shown: T.Grid(Bool), +p: T.Pos) -> T.Seen:
49	  seen_pick(B.at(Bool, False{}, shown, p), B.mine(layout, p), w, h, layout, p)
50	
51	def know_row(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), +y: Nat,
52	  xs: List<&2, Nat>) -> List<&2, T.Seen>:
53	  match xs:
54	    case Nil{}:
55	      Nil{}
56	    case x <> t:
57	      seen_at(w, h, layout, shown, T.Pos{x, y}) <> know_row(w, h, layout, shown, y, t)
58	
59	def know_rows(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool),
60	  ys: List<&2, Nat>) -> T.Grid(T.Seen):
61	  match ys:
62	    case Nil{}:
63	      Nil{}
64	    case y <> t:
65	      know_row(w, h, layout, shown, y, List.range(w)) <> know_rows(w, h, layout, shown, t)
66	
67	def knowledge(g: Game) -> T.Knowledge:
68	  match g:
69	    case Game{+w, +h, +layout, shown, flags, status}:
70	      T.Knowledge{w, h, B.total_mines(layout), know_rows(w, h, layout, shown, List.range(h))}
71	
72	# Every safe cell is revealed.
73	def all_safe.go(+layout: T.Grid(Bool), +shown: T.Grid(Bool), ps: List<&2, T.Pos>) -> Bool:
74	  match ps:
75	    case Nil{}:
76	      True{}
77	    case +p <> t:
78	      (B.mine(layout, p) || B.at(Bool, False{}, shown, p)) && all_safe.go(layout, shown, t)
79	
80	def all_safe(w: Nat, h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool)) -> Bool:
81	  all_safe.go(layout, shown, B.cells(w, h))
82	
83	def won_or_playing(b: Bool) -> T.Status:
84	  match b:
85	    case True{}:
86	      T.Won{}
87	    case False{}:
88	      T.Playing{}
89	
90	# Starting and setting up
91	# -----------------------
92	
93	def fresh(+w: Nat, +h: Nat, +layout: T.Grid(Bool)) -> Game:
94	  +shown = B.blank(Bool, w, h, False{})
95	  Game{w, h, layout, shown, Nil{}, won_or_playing(all_safe(w, h, layout, shown))}
96	
97	def clamp(lo: Nat, hi: Nat, x: Nat) -> Nat:
98	  Nat.max(lo, Nat.min(hi, x))
99	
100	def custom(w: Nat, h: Nat, m: Nat) -> T.Setup:
101	  +cw = clamp(9n, 30n, w)
102	  +ch = clamp(9n, 25n, h)
103	  T.Setup{cw, ch, Nat.min(clamp(10n, 999n, m), Nat.sub(Nat.mul(cw, ch), 10n))}
104	
105	def setup(l: T.Level) -> T.Setup:
106	  match l:
107	    case T.Beginner{}:
108	      T.Setup{9n, 9n, 10n}
109	    case T.Intermediate{}:
110	      T.Setup{16n, 16n, 40n}
111	    case T.Expert{}:
112	      T.Setup{30n, 16n, 99n}
113	    case T.Custom{w, h, m}:
114	      custom(w, h, m)
115	
116	# Board generation
117	# ----------------
118	# Selection sampling (Knuth's Algorithm S) over the cells outside a zone
119	# kept free, row by row: with `need` mines still to place among `left`
120	# candidates, a cell gets a mine when need = left, or else with probability
121	# about need/left. Whatever the random numbers, exactly n mines come out.
122	#
123	# The zone is the first click and, when there is room, its neighbours too,
124	# so the first click opens an area (as in Windows Vista and later).
125	
126	# The cells kept free of mines: `first`, and its neighbours when `wide`.
127	type Zone is Data:
128	  Zone{first: T.Pos, wide: Bool}
129	
130	def gen.out(z: Zone, +p: T.Pos) -> Bool:
131	  match z:
132	    case Zone{+first, wide}:
133	      Bool.pick(Bool, wide, B.within_one(first, p), B.same(p, first))
134	
135	type GenState is Data:
136	  GenState{need: Nat, left: Nat, rs: List<&2, U32>}
137	
138	def gen.coin(r: U32, +left: Nat, need: Nat) -> Bool:
139	  Nat.is_lt(Nat.mod(U32.to_nat(r), left), need)
140	
141	# Whether the next candidate gets a mine: forced when every candidate left
142	# needs one, else a coin flip that comes up heads about need/left of the time.
143	def gen.pick(+need: Nat, +left: Nat, rs: List<&2, U32>) -> Bool:
144	  match rs:
145	    case Nil{}:
146	      Nat.is_eq(need, left)
147	    case r <> t:
148	      Nat.is_eq(need, left) || gen.coin(r, left, need)
149	
150	# Whether cell p gets a mine.
151	def gen.bit(z: Zone, p: T.Pos, st: GenState) -> Bool:
152	  match st:
153	    case GenState{+need, left, rs}:
154	      Bool.not(gen.out(z, p)) && Nat.is_lt(0n, need) && gen.pick(need, left, rs)
155	
156	def gen.next.go(skip: Bool, bit: Bool, need: Nat, left: Nat, rs: List<&2, U32>) -> GenState:
157	  match skip:
158	    case True{}:
159	      GenState{need, left, rs}
160	    case False{}:
161	      GenState{Nat.sub(need, Bool.pick(Nat, bit, 1n, 0n)), Nat.sub(left, 1n),
162	        List.tail(&2, U32, rs)}
163	
164	# The state after cell p.
165	def gen.next(+z: Zone, +p: T.Pos, +st: GenState) -> GenState:
166	  match st:
167	    case GenState{need, left, rs}:
168	      gen.next.go(gen.out(z, p), gen.bit(z, p, st), need, left, rs)
169	
170	def gen.row(+z: Zone, +y: Nat, xs: List<&2, Nat>, +st: GenState) -> List<&2, Bool>:
171	  match xs:
172	    case Nil{}:
173	      Nil{}
174	    case x <> t:
175	      +p = {T.Pos{x, y} : T.Pos}
176	      gen.bit(z, p, st) <> gen.row(z, y, t, gen.next(z, p, st))
177	
178	# The state after a row.
179	def gen.row_state(+z: Zone, +y: Nat, xs: List<&2, Nat>, +st: GenState) -> GenState:
180	  match xs:
181	    case Nil{}:
182	      st
183	    case x <> t:
184	      gen.row_state(z, y, t, gen.next(z, T.Pos{x, y}, st))
185	
186	def gen.rows(+z: Zone, +w: Nat, ys: List<&2, Nat>, +st: GenState) -> T.Grid(Bool):
187	  match ys:
188	    case Nil{}:
189	      Nil{}
190	    case +y <> t:
191	      gen.row(z, y, List.range(w), st)
192	        <> gen.rows(z, w, t, gen.row_state(z, y, List.range(w), st))
193	
194	# How many cells of ps are outside the zone.
195	def gen.left(+z: Zone, ps: List<&2, T.Pos>) -> Nat:
196	  match ps:
197	    case Nil{}:
198	      0n
199	    case p <> t:
200	      Nat.add(Bool.pick(Nat, gen.out(z, p), 0n, 1n), gen.left(z, t))
201	
202	# Room for the first click's neighbours: at least 9 cells left free.
203	def place_mines(+w: Nat, +h: Nat, +n: Nat, +first: T.Pos, rs: List<&2, U32>) -> T.Grid(Bool):
204	  +z = {Zone{first, Nat.is_le(Nat.add(n, 9n), Nat.mul(w, h))} : Zone}
205	  gen.rows(z, w, List.range(h), GenState{n, gen.left(z, B.cells(w, h)), rs})
206	
207	# Revealing
208	# ---------
209	
210	# A cell queued by the flood, with the path that reached it from the cell
211	# first opened, newest step first (kept only so the proofs can name it).
212	type Work is Data:
213	  Work{c: T.Pos, back: List<&2, T.Pos>}
214	
215	# The first cell of `work` is on the board and not revealed yet.
216	def head_hidden(+w: Nat, +h: Nat, shown: T.Grid(Bool), work: List<&2, Work>) -> Bool:
217	  match work:
218	    case Nil{}:
219	      False{}
220	    case Work{c, back} <> t:
221	      unrevealed(w, h, shown, c)
222	
223	# The cells ns, each reached one step past `back`.
224	def works(ns: List<&2, T.Pos>, +back: List<&2, T.Pos>) -> List<&2, Work>:
225	  match ns:
226	    case Nil{}:
227	      Nil{}
228	    case +r <> t:
229	      Work{r, r <> back} <> works(t, back)
230	
231	def push(z: Bool, ns: List<&2, T.Pos>, back: List<&2, T.Pos>, rest: List<&2, Work>) ->
232	  List<&2, Work>:
233	  match z:
234	    case True{}:
235	      List.append(&2, Work, works(ns, back), rest)
236	    case False{}:
237	      rest
238	
239	# Reveal the cells of `work`, and the neighbours of every zero revealed. n is
240	# how many cells are not revealed yet: each reveal uses one up.
241	def flood(+n: Nat, work: List<&2, Work>, hd: Bool, +w: Nat, +h: Nat,
242	  +layout: T.Grid(Bool), +shown: T.Grid(Bool)) -> T.Grid(Bool):
243	  match n:
244	    case 0n:
245	      shown
246	    case 1n+m:
247	      match work:
248	        case Nil{}:
249	          shown
250	        case Work{+c, +back} <> +rest:
251	          match hd:
252	            case False{}:
253	              flood(n, rest, head_hidden(w, h, shown, rest), w, h, layout, shown)
254	            case True{}:
255	              +sh = B.set_at(Bool, shown, c, True{})
256	              +wk = push(B.zero(w, h, layout, c), B.neighbours(w, h, c), back, rest)
257	              flood(m, wk, head_hidden(w, h, sh, wk), w, h, layout, sh)
258	
259	def explode(g: Game, +p: T.Pos) -> Game:
260	  match g:
261	    case Game{w, h, layout, shown, flags, status}:
262	      Game{w, h, layout, B.set_at(Bool, shown, p, True{}), flags, T.Lost{T.Exploded{p}}}
263	
264	def flood_open(g: Game, +p: T.Pos) -> Game:
265	  match g:
266	    case Game{+w, +h, +layout, +shown, flags, status}:
267	      +start = {[Work{p, Nil{}}] : List<&2, Work>}
268	      +sh = flood(B.count_false(shown), start, head_hidden(w, h, shown, start), w, h, layout, shown)
269	      Game{w, h, layout, sh, flags, won_or_playing(all_safe(w, h, layout, sh))}
270	
271	def open.go(can: Bool, boom: Bool, g: Game, p: T.Pos) -> Game:
272	  match can boom:
273	    case False{} _:
274	      g
275	    case True{} True{}:
276	      explode(g, p)
277	    case True{} False{}:
278	      flood_open(g, p)
279	
280	# During play, a hidden cell of the board can be opened.
281	def can_open(g: Game, +p: T.Pos) -> Bool:
282	  match g:
283	    case Game{w, h, layout, shown, flags, status}:
284	      is_playing(status) && unrevealed(w, h, shown, p)
285	
286	def layout_of(g: Game) -> T.Grid(Bool):
287	  match g:
288	    case Game{w, h, layout, shown, flags, status}:
289	      layout
290	
291	# Reveal p whether or not it is flagged (Reveal, Chord and Assist use it).
292	def open(+g: Game, +p: T.Pos) -> Game:
293	  open.go(can_open(g, p), B.mine(layout_of(g), p), g, p)
294	
295	def reveal.go(f: Bool, g: Game, p: T.Pos) -> Game:
296	  match f:
297	    case True{}:
298	      g
299	    case False{}:
300	      open(g, p)
301	
302	def reveal(+g: Game, +p: T.Pos) -> Game:
303	  reveal.go(flagged(g, p), g, p)
304	
305	# Chording
306	# --------
307	
308	def flags_among(+g: Game, qs: List<&2, T.Pos>) -> Nat:
309	  match qs:
310	    case Nil{}:
311	      0n
312	    case q <> t:
313	      Nat.add(Bool.pick(Nat, flagged(g, q), 1n, 0n), flags_among(g, t))
314	
315	def is_hidden(s: T.Seen) -> Bool:
316	  match s:
317	    case T.Hidden{}:
318	      True{}
319	    case o:
320	      False{}
321	
322	def hidden(v: T.Knowledge, +p: T.Pos) -> Bool:
323	  match v:
324	    case T.Knowledge{w, h, n, rows}:
325	      B.on_board(w, h, p) && is_hidden(B.at(T.Seen, T.Hidden{}, rows, p))
326	
327	def seen(v: T.Knowledge, p: T.Pos) -> T.Seen:
328	  match v:
329	    case T.Knowledge{w, h, n, rows}:
330	      B.at(T.Seen, T.Hidden{}, rows, p)
331	
332	def hidden_unflagged(+g: Game, +v: T.Knowledge, qs: List<&2, T.Pos>) -> List<&2, T.Pos>:
333	  match qs:
334	    case Nil{}:
335	      Nil{}
336	    case +q <> t:
337	      List.filter.put(T.Pos, q, hidden_unflagged(g, v, t),
338	        hidden(v, q) && Bool.not(flagged(g, q)))
339	
340	def chord_targets.pick(+g: Game, v: T.Knowledge, +ns: List<&2, T.Pos>, s: T.Seen) ->
341	  List<&2, T.Pos>:
342	  match s:
343	    case T.Shown{k}:
344	      Bool.pick(List<&2, T.Pos>, Nat.is_eq(flags_among(g, ns), k),
345	        hidden_unflagged(g, v, ns), Nil{})
346	    case o:
347	      Nil{}
348	
349	def chord_targets.go(g: Game, +v: T.Knowledge, +p: T.Pos) -> List<&2, T.Pos>:
350	  match v:
351	    case T.Knowledge{w, h, n, rows}:
352	      chord_targets.pick(g, v, B.neighbours(w, h, p), seen(v, p))
353	
354	def chord_targets(+g: Game, p: T.Pos) -> List<&2, T.Pos>:
355	  chord_targets.go(g, knowledge(g), p)
356	
357	def chord_play(ts: List<&2, T.Pos>, g: Game) -> Game:
358	  match ts:
359	    case Nil{}:
360	      g
361	    case q <> t:
362	      chord_play(t, reveal(g, q))
363	
364	# Flags
365	# -----
366	
367	def toggle.go(has: Bool, flags: List<&2, T.Pos>, +p: T.Pos) -> List<&2, T.Pos>:
368	  match has:
369	    case True{}:
370	      B.remove(flags, p)
371	    case False{}:
372	      p <> flags
373	
374	def toggle(+flags: List<&2, T.Pos>, +p: T.Pos) -> List<&2, T.Pos>:
375	  toggle.go(B.contains(flags, p), flags, p)
376	
377	def flag.go(c: Bool, g: Game, p: T.Pos) -> Game:
378	  match c:
379	    case False{}:
380	      g
381	    case True{}:
382	      match g:
383	        case Game{w, h, layout, shown, flags, status}:
384	          Game{w, h, layout, shown, toggle(flags, p), status}
385	
386	def can_flag(g: Game, +p: T.Pos) -> Bool:
387	  match g:
388	    case Game{w, h, layout, shown, flags, status}:
389	      is_playing(status) && unrevealed(w, h, shown, p)
390	
391	def flag(+g: Game, +p: T.Pos) -> Game:
392	  flag.go(can_flag(g, p), g, p)
393	
394	# The assist
395	# ----------
396	
397	# The first cell of ps is safe and not revealed yet.
398	def safe_here(+layout: T.Grid(Bool), +shown: T.Grid(Bool), ps: List<&2, T.Pos>) -> Bool:
399	  match ps:
400	    case Nil{}:
401	      False{}
402	    case +p <> t:
403	      Bool.not(B.mine(layout, p)) && Bool.not(B.at(Bool, False{}, shown, p))
404	
405	def first_safe.go(ps: List<&2, T.Pos>, hit: Bool, +layout: T.Grid(Bool),
406	  +shown: T.Grid(Bool)) -> Maybe<&2, T.Pos>:
407	  match ps:
408	    case Nil{}:
409	      None{}
410	    case p <> +t:
411	      match hit:
412	        case True{}:
413	          Some{p}
414	        case False{}:
415	          first_safe.go(t, safe_here(layout, shown, t), layout, shown)
416	
417	# The first safe cell of ps that is not revealed yet.
418	def first_safe(+layout: T.Grid(Bool), +shown: T.Grid(Bool), +ps: List<&2, T.Pos>) ->
419	  Maybe<&2, T.Pos>:
420	  first_safe.go(ps, safe_here(layout, shown, ps), layout, shown)
421	
422	def any_shown(+shown: T.Grid(Bool), ps: List<&2, T.Pos>) -> Bool:
423	  match ps:
424	    case Nil{}:
425	      False{}
426	    case p <> t:
427	      B.at(Bool, False{}, shown, p) || any_shown(shown, t)
428	
429	# The cells of ps not revealed yet but next to a revealed one.
430	def edges(+w: Nat, +h: Nat, +shown: T.Grid(Bool), ps: List<&2, T.Pos>) -> List<&2, T.Pos>:
431	  match ps:
432	    case Nil{}:
433	      Nil{}
434	    case +p <> t:
435	      List.filter.put(T.Pos, p, edges(w, h, shown, t),
436	        Bool.not(B.at(Bool, False{}, shown, p)) && any_shown(shown, B.neighbours(w, h, p)))
437	
438	# ps from a point picked by k, wrapping around.
439	def turn(+ps: List<&2, T.Pos>, +k: Nat) -> List<&2, T.Pos>:
440	  +i = Nat.mod(k, Nat.add(List.length(&2, T.Pos, ps), 1n))
441	  List.append(&2, T.Pos, List.drop(&2, T.Pos, ps, i), List.take(&2, T.Pos, ps, i))
442	
443	# Where the assist looks for a safe cell, k being a random number: first
444	# the hidden cells next to a revealed one, then every cell, each from a
445	# random point; last every cell in order, which never comes into play but
446	# lets the proofs see a safe cell is always found.
447	def safe_list(+w: Nat, +h: Nat, +shown: T.Grid(Bool), +k: Nat) -> List<&2, T.Pos>:
448	  +cs = B.cells(w, h)
449	  List.append(&2, T.Pos, turn(edges(w, h, shown, cs), k), List.append(&2, T.Pos, turn(cs, k), cs))
450	
451	def safe_cell(g: Game, +k: Nat) -> Maybe<&2, T.Pos>:
452	  match g:
453	    case Game{+w, +h, +layout, +shown, flags, status}:
454	      first_safe(layout, shown, safe_list(w, h, shown, k))
455	
456	def lose(g: Game, p: T.Pos) -> Game:
457	  match g:
458	    case Game{w, h, layout, shown, flags, status}:
459	      Game{w, h, layout, shown, flags, T.Lost{T.AssistTooEarly{p}}}
460	
461	def assist.safe(m: Maybe<&2, T.Pos>, g: Game) -> Game:
462	  match m:
463	    case None{}:
464	      g
465	    case Some{p}:
466	      open(g, p)
467	
468	def assist.pick(r: Maybe<&2, T.Pos>, +g: Game, +k: Nat) -> Game:
469	  match r:
470	    case Some{q}:
471	      lose(g, q)
472	    case None{}:
473	      assist.safe(safe_cell(g, k), g)
474	
475	def assist.go(playing: Bool, +g: Game, +k: Nat) -> Game:
476	  match playing:
477	    case False{}:
478	      g
479	    case True{}:
480	      assist.pick(S.solve(knowledge(g)), g, k)
481	
482	def assist(+g: Game, +k: Nat) -> Game:
483	  assist.go(is_playing(status(g)), g, k)
484	
485	# Actions
486	# -------
487	
488	def step(+g: Game, a: T.Action) -> Game:
489	  match a:
490	    case T.Reveal{p}:
491	      reveal(g, p)
492	    case T.Chord{p}:
493	      chord_play(chord_targets(g, p), g)
494	    case T.Flag{p}:
495	      flag(g, p)
496	    case T.Assist{k}:
497	      assist(g, k)
498	
499	# The display
500	# -----------
501	# What every cell looks like on screen. During play it shows exactly what the
502	# player knows, plus their flags. Once the game is over it also shows the
503	# mines, like Windows: the mine that exploded, every other mine, crosses on
504	# wrong flags, and (after an assist pressed too early) the safe cell missed.
505	
506	def mark.why(why: T.Loss, +p: T.Pos) -> Maybe<&2, T.Tile>:
507	  match why:
508	    case T.Exploded{e}:
509	      Bool.pick(Maybe<&2, T.Tile>, B.same(e, p), Some{T.Blast{}}, None{})
510	    case T.AssistTooEarly{s}:
511	      Bool.pick(Maybe<&2, T.Tile>, B.same(s, p), Some{T.Hint{}}, None{})
512	
513	# A cell the end of the game singles out.
514	def mark(st: T.Status, +p: T.Pos) -> Maybe<&2, T.Tile>:
515	  match st:
516	    case T.Lost{why}:
517	      mark.why(why, p)
518	    case o:
519	      None{}
520	
521	def tile_lost(m: Bool, f: Bool) -> T.Tile:
522	  match m f:
523	    case True{} True{}:
524	      T.Flagged{}
525	    case True{} False{}:
526	      T.Mine{}
527	    case False{} True{}:
528	      T.BadFlag{}
529	    case False{} False{}:
530	      T.Covered{}
531	
532	def tile_hidden(st: T.Status, m: Bool, f: Bool) -> T.Tile:
533	  match st:
534	    case T.Playing{}:
535	      Bool.pick(T.Tile, f, T.Flagged{}, T.Covered{})
536	    case T.Won{}:
537	      Bool.pick(T.Tile, m, T.Flagged{}, T.Covered{})
538	    case T.Lost{why}:
539	      tile_lost(m, f)
540	
541	def tile_shown(m: Bool, w: Nat, h: Nat, layout: T.Grid(Bool), p: T.Pos) -> T.Tile:
542	  match m:
543	    case True{}:
544	      T.Blast{}
545	    case False{}:
546	      T.Number{B.adj_mines(w, h, layout, p)}
547	
548	def tile.go(mk: Maybe<&2, T.Tile>, s: Bool, m: Bool, f: Bool, st: T.Status, w: Nat, h: Nat,
549	  layout: T.Grid(Bool), p: T.Pos) -> T.Tile:
550	  match mk:
551	    case Some{t}:
552	      t
553	    case None{}:
554	      match s:
555	        case True{}:
556	          tile_shown(m, w, h, layout, p)
557	        case False{}:
558	          tile_hidden(st, m, f)
559	
560	def tile_at(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), +flags: List<&2, T.Pos>,
561	  +st: T.Status, +p: T.Pos) -> T.Tile:
562	  tile.go(mark(st, p), B.at(Bool, False{}, shown, p), B.mine(layout, p), B.contains(flags, p), st, w, h, layout, p)
563	
564	def disp_row(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), +flags: List<&2, T.Pos>,
565	  +st: T.Status, +y: Nat, xs: List<&2, Nat>) -> List<&2, T.Tile>:
566	  match xs:
567	    case Nil{}:
568	      Nil{}
569	    case x <> t:
570	      tile_at(w, h, layout, shown, flags, st, T.Pos{x, y}) <> disp_row(w, h, layout, shown, flags, st, y, t)
571	
572	def disp_rows(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), +flags: List<&2, T.Pos>,
573	  +st: T.Status, ys: List<&2, Nat>) -> T.Grid(T.Tile):
574	  match ys:
575	    case Nil{}:
576	      Nil{}
577	    case y <> t:
578	      disp_row(w, h, layout, shown, flags, st, y, List.range(w)) <> disp_rows(w, h, layout, shown, flags, st, t)
579	
580	def display(g: Game) -> T.Grid(T.Tile):
581	  match g:
582	    case Game{+w, +h, +layout, +shown, +flags, +status}:
583	      disp_rows(w, h, layout, shown, flags, status, List.range(h))
584	
585	# How many flags the mine counter shows: the mines, less the flags placed.
586	def flags_shown(+w: Nat, +h: Nat, +shown: T.Grid(Bool), flags: List<&2, T.Pos>) -> Nat:
587	  match flags:
588	    case Nil{}:
589	      0n
590	    case +p <> t:
591	      Nat.add(Bool.pick(Nat, unrevealed(w, h, shown, p), 1n, 0n), flags_shown(w, h, shown, t))