game.bend

minebender-game@1.0.0.0 · 591 lines · 82 definitions

1import Base
2import minebender-game@1.0.0.0/types.bend as T
3import minebender-game@1.0.0.0/board.bend as B
4import minebender-game@1.0.0.0/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.
10type 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
17def status(g: Game) -> T.Status:
18  match g:
19    case Game{w, h, layout, shown, flags, status}:
20      status
21
22def 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.
30def 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
33def 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.
39def 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
48def 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
51def 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
59def 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
67def 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.
73def 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
80def 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
83def 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
93def 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
97def clamp(lo: Nat, hi: Nat, x: Nat) -> Nat:
98  Nat.max(lo, Nat.min(hi, x))
99
100def 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
105def 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`.
127type Zone is Data:
128  Zone{first: T.Pos, wide: Bool}
129
130def 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
135type GenState is Data:
136  GenState{need: Nat, left: Nat, rs: List<&2, U32>}
137
138def 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.
143def 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.
151def 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
156def 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.
165def 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
170def 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.
179def 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
186def 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.
195def 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.
203def 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).
212type 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.
216def 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`.
224def 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
231def 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.
241def 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
259def 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
264def 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
271def 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.
281def 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
286def 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).
292def open(+g: Game, +p: T.Pos) -> Game:
293  open.go(can_open(g, p), B.mine(layout_of(g), p), g, p)
294
295def 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
302def reveal(+g: Game, +p: T.Pos) -> Game:
303  reveal.go(flagged(g, p), g, p)
304
305# Chording
306# --------
307
308def 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
315def is_hidden(s: T.Seen) -> Bool:
316  match s:
317    case T.Hidden{}:
318      True{}
319    case o:
320      False{}
321
322def 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
327def 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
332def 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
340def 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
349def 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
354def chord_targets(+g: Game, p: T.Pos) -> List<&2, T.Pos>:
355  chord_targets.go(g, knowledge(g), p)
356
357def 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
367def 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
374def toggle(+flags: List<&2, T.Pos>, +p: T.Pos) -> List<&2, T.Pos>:
375  toggle.go(B.contains(flags, p), flags, p)
376
377def 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
386def 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
391def 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.
398def 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
405def 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.
418def 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
422def 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.
430def 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.
439def 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.
447def 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
451def 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
456def 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
461def 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
468def 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
475def 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
482def assist(+g: Game, +k: Nat) -> Game:
483  assist.go(is_playing(status(g)), g, k)
484
485# Actions
486# -------
487
488def 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
506def 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.
514def 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
521def 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
532def 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
541def 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
548def 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
560def 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
564def 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
572def 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
580def 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.
586def 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))