1	import Base
2	import ./types.bend as T
3	import ./board.bend as B
4	
5	# The no-guess solver: finds a provably safe hidden cell, or none.
6	#
7	# A hidden cell c is provably safe exactly when no layout consistent with
8	# what the player knows has a mine on c. For each hidden cell (row by row),
9	# the solver searches for such a layout with a mine on c; the first cell
10	# with none is the answer. A layout found also shows that every other cell
11	# it mines is not provably safe, which saves most searches.
12	#
13	# The search is a depth-first walk over the hidden cells, cells next to a
14	# number first. A partial layout gives each cell Some{mine} or None
15	# (unassigned). After each choice, the numbers around the cell and the
16	# total mine count are checked against what can still be reached; a full
17	# layout is checked for consistency before it counts.
18	#
19	# Speed comes from the order of the walk, the standard constraint-solving
20	# approach to Minesweeper: the cells linked to c through numbers first,
21	# nearest first, so a contradiction near c shows up before anything far
22	# away is enumerated; then each other group of linked cells in turn, so
23	# backtracking never mixes unrelated groups; then the cells next to no
24	# number, rotated per search so the layouts found spread their mines and
25	# rule out many cells at once. The order is a heuristic: the proofs only
26	# need every cell to appear, so it runs before the plain order, whose cells
27	# the walk then skips as already assigned.
28	
29	# A revealed cell, and for a number, the cells it counts.
30	type Item is Data:
31	  Item{p: T.Pos, s: T.Seen, ns: List<&2, T.Pos>}
32	
33	# A hidden cell to assign, and the numbers around it.
34	type Todo is Data:
35	  Todo{c: T.Pos, rel: List<&2, Item>}
36	
37	type Ctx is Data:
38	  Ctx{w: Nat, h: Nat, n: Nat, rows: T.Grid(T.Seen), items: List<&2, Item>}
39	
40	# Checking a full layout
41	# ----------------------
42	
43	def items.put(s: T.Seen, +p: T.Pos, w: Nat, h: Nat, rest: List<&2, Item>) -> List<&2, Item>:
44	  match s:
45	    case T.Hidden{}:
46	      rest
47	    case T.Shown{k}:
48	      Item{p, T.Shown{k}, B.neighbours(w, h, p)} <> rest
49	    case T.Boom{}:
50	      Item{p, T.Boom{}, Nil{}} <> rest
51	
52	# The revealed cells of ps.
53	def items(+w: Nat, +h: Nat, +rows: T.Grid(T.Seen), ps: List<&2, T.Pos>) -> List<&2, Item>:
54	  match ps:
55	    case Nil{}:
56	      Nil{}
57	    case +p <> t:
58	      items.put(B.at(T.Seen, T.Hidden{}, rows, p), p, w, h, items(w, h, rows, t))
59	
60	def item_ok(s: T.Seen, +p: T.Pos, ns: List<&2, T.Pos>, +layout: T.Grid(Bool)) -> Bool:
61	  match s:
62	    case T.Hidden{}:
63	      True{}
64	    case T.Shown{k}:
65	      Bool.not(B.mine(layout, p)) && Nat.is_eq(B.count_mines(layout, ns), k)
66	    case T.Boom{}:
67	      B.mine(layout, p)
68	
69	def items_ok(its: List<&2, Item>, +layout: T.Grid(Bool)) -> Bool:
70	  match its:
71	    case Nil{}:
72	      True{}
73	    case Item{p, s, ns} <> t:
74	      item_ok(s, p, ns, layout) && items_ok(t, layout)
75	
76	# The layout is consistent with what the player knows.
77	def check(ctx: Ctx, +layout: T.Grid(Bool)) -> Bool:
78	  match ctx:
79	    case Ctx{+w, +h, n, rows, items}:
80	      B.shaped(Bool, w, h, layout) && B.shaped(T.Seen, w, h, rows)
81	        && Nat.is_eq(B.total_mines(layout), n) && items_ok(items, layout)
82	
83	# Partial layouts
84	# ---------------
85	
86	def start.cell(s: T.Seen) -> Maybe<&2, Bool>:
87	  match s:
88	    case T.Hidden{}:
89	      None{}
90	    case T.Shown{k}:
91	      Some{False{}}
92	    case T.Boom{}:
93	      Some{True{}}
94	
95	def start.row(r: List<&2, T.Seen>) -> List<&2, Maybe<&2, Bool>>:
96	  match r:
97	    case Nil{}:
98	      Nil{}
99	    case s <> t:
100	      start.cell(s) <> start.row(t)
101	
102	# What the revealed cells fix: no mine under a number, one under a Boom.
103	def start(rows: T.Grid(T.Seen)) -> T.Grid(Maybe<&2, Bool>):
104	  match rows:
105	    case Nil{}:
106	      Nil{}
107	    case r <> t:
108	      start.row(r) <> start(t)
109	
110	def fill.row(r: List<&2, Maybe<&2, Bool>>) -> List<&2, Bool>:
111	  match r:
112	    case Nil{}:
113	      Nil{}
114	    case m <> t:
115	      Maybe.default(&2, Bool, m, False{}) <> fill.row(t)
116	
117	def fill(part: T.Grid(Maybe<&2, Bool>)) -> T.Grid(Bool):
118	  match part:
119	    case Nil{}:
120	      Nil{}
121	    case r <> t:
122	      fill.row(r) <> fill(t)
123	
124	def look(+part: T.Grid(Maybe<&2, Bool>), p: T.Pos) -> Maybe<&2, Bool>:
125	  B.at(Maybe<&2, Bool>, None{}, part, p)
126	
127	def is_true(m: Maybe<&2, Bool>) -> Bool:
128	  match m:
129	    case Some{b}:
130	      b
131	    case None{}:
132	      False{}
133	
134	def is_none(m: Maybe<&2, Bool>) -> Bool:
135	  match m:
136	    case Some{b}:
137	      False{}
138	    case None{}:
139	      True{}
140	
141	def one_if(b: Bool) -> Nat:
142	  Bool.pick(Nat, b, 1n, 0n)
143	
144	def row_true(r: List<&2, Maybe<&2, Bool>>) -> Nat:
145	  match r:
146	    case Nil{}:
147	      0n
148	    case m <> t:
149	      Nat.add(one_if(is_true(m)), row_true(t))
150	
151	def row_none(r: List<&2, Maybe<&2, Bool>>) -> Nat:
152	  match r:
153	    case Nil{}:
154	      0n
155	    case +m <> t:
156	      Nat.add(one_if(is_none(m)), row_none(t))
157	
158	def part_true(part: T.Grid(Maybe<&2, Bool>)) -> Nat:
159	  match part:
160	    case Nil{}:
161	      0n
162	    case r <> t:
163	      Nat.add(row_true(r), part_true(t))
164	
165	def part_none(part: T.Grid(Maybe<&2, Bool>)) -> Nat:
166	  match part:
167	    case Nil{}:
168	      0n
169	    case r <> t:
170	      Nat.add(row_none(r), part_none(t))
171	
172	def true_among(+part: T.Grid(Maybe<&2, Bool>), ps: List<&2, T.Pos>) -> Nat:
173	  match ps:
174	    case Nil{}:
175	      0n
176	    case q <> t:
177	      Nat.add(one_if(is_true(look(part, q))), true_among(part, t))
178	
179	def none_among(+part: T.Grid(Maybe<&2, Bool>), ps: List<&2, T.Pos>) -> Nat:
180	  match ps:
181	    case Nil{}:
182	      0n
183	    case q <> t:
184	      Nat.add(one_if(is_none(look(part, q))), none_among(part, t))
185	
186	# Pruning
187	# -------
188	
189	# k is still reachable from what is fixed: t mines, f unassigned cells.
190	def between(+t: Nat, +f: Nat, +k: Nat) -> Bool:
191	  Nat.is_le(t, k) && Nat.is_le(k, Nat.add(t, f))
192	
193	def item_open(s: T.Seen, +part: T.Grid(Maybe<&2, Bool>), +ns: List<&2, T.Pos>) -> Bool:
194	  match s:
195	    case T.Shown{k}:
196	      between(true_among(part, ns), none_among(part, ns), k)
197	    case o:
198	      True{}
199	
200	def items_open(+part: T.Grid(Maybe<&2, Bool>), its: List<&2, Item>) -> Bool:
201	  match its:
202	    case Nil{}:
203	      True{}
204	    case Item{p, s, ns} <> t:
205	      item_open(s, part, ns) && items_open(part, t)
206	
207	# Some completion of the partial layout may still be consistent.
208	def open_ok(+part: T.Grid(Maybe<&2, Bool>), rel: List<&2, Item>, n: Nat) -> Bool:
209	  between(part_true(part), part_none(part), n) && items_open(part, rel)
210	
211	# The search
212	# ----------
213	
214	def ctx_n(ctx: Ctx) -> Nat:
215	  match ctx:
216	    case Ctx{w, h, n, rows, items}:
217	      n
218	
219	def dfs.or(r: Maybe<&2, T.Grid(Bool)>, k: Unit -> Maybe<&2, T.Grid(Bool)>) ->
220	  Maybe<&2, T.Grid(Bool)>:
221	  match r:
222	    case None{}:
223	      k(Unit{})
224	    case Some{l}:
225	      Some{l}
226	
227	def dfs.when(ok: Bool, k: Unit -> Maybe<&2, T.Grid(Bool)>) -> Maybe<&2, T.Grid(Bool)>:
228	  match ok:
229	    case False{}:
230	      None{}
231	    case True{}:
232	      k(Unit{})
233	
234	def dfs.free(free: Bool, skip: Unit -> Maybe<&2, T.Grid(Bool)>,
235	  branch: Unit -> Maybe<&2, T.Grid(Bool)>) -> Maybe<&2, T.Grid(Bool)>:
236	  match free:
237	    case False{}:
238	      skip(Unit{})
239	    case True{}:
240	      branch(Unit{})
241	
242	def leaf(+ctx: Ctx, +layout: T.Grid(Bool)) -> Maybe<&2, T.Grid(Bool)>:
243	  Bool.pick(Maybe<&2, T.Grid(Bool)>, check(ctx, layout), Some{layout}, None{})
244	
245	# A consistent layout completing the partial one, assigning the cells of
246	# `todo` in order (cells already assigned are skipped).
247	def dfs(todo: List<&2, Todo>, +part: T.Grid(Maybe<&2, Bool>), +ctx: Ctx) ->
248	  Maybe<&2, T.Grid(Bool)>:
249	  match todo:
250	    case Nil{}:
251	      leaf(ctx, fill(part))
252	    case Todo{+c, +rel} <> +rest:
253	      +p0 = B.set_at(Maybe<&2, Bool>, part, c, Some{False{}})
254	      +p1 = B.set_at(Maybe<&2, Bool>, part, c, Some{True{}})
255	      +n = ctx_n(ctx)
256	      dfs.free(is_none(look(part, c)),
257	        u => dfs(rest, part, ctx),
258	        v => dfs.or(dfs.when(open_ok(p0, rel, n), x => dfs(rest, p0, ctx)),
259	          y => dfs.when(open_ok(p1, rel, n), z => dfs(rest, p1, ctx))))
260	
261	# The same search, carrying the mines t and unassigned cells f of the partial
262	# layout instead of recounting the whole grid at every step. PROOF.bend
263	# shows it answers exactly as dfs.
264	def dfs2(todo: List<&2, Todo>, +part: T.Grid(Maybe<&2, Bool>), +t: Nat, +f: Nat, +ctx: Ctx) ->
265	  Maybe<&2, T.Grid(Bool)>:
266	  match todo:
267	    case Nil{}:
268	      leaf(ctx, fill(part))
269	    case Todo{+c, +rel} <> +rest:
270	      +p0 = B.set_at(Maybe<&2, Bool>, part, c, Some{False{}})
271	      +p1 = B.set_at(Maybe<&2, Bool>, part, c, Some{True{}})
272	      +n = ctx_n(ctx)
273	      +f1 = Nat.sub(f, 1n)
274	      dfs.free(is_none(look(part, c)),
275	        u => dfs2(rest, part, t, f, ctx),
276	        v => dfs.or(dfs.when(between(t, f1, n) && items_open(p0, rel), x => dfs2(rest, p0, t, f1, ctx)),
277	          y => dfs.when(between(1n+t, f1, n) && items_open(p1, rel), z => dfs2(rest, p1, 1n+t, f1, ctx))))
278	
279	# The cells of a solve
280	# --------------------
281	
282	def is_hidden(s: T.Seen) -> Bool:
283	  match s:
284	    case T.Hidden{}:
285	      True{}
286	    case o:
287	      False{}
288	
289	def hidden_cells(+rows: T.Grid(T.Seen), ps: List<&2, T.Pos>) -> List<&2, T.Pos>:
290	  match ps:
291	    case Nil{}:
292	      Nil{}
293	    case +p <> t:
294	      List.filter.put(T.Pos, p, hidden_cells(rows, t),
295	        is_hidden(B.at(T.Seen, T.Hidden{}, rows, p)))
296	
297	def is_number(s: T.Seen) -> Bool:
298	  match s:
299	    case T.Shown{k}:
300	      True{}
301	    case o:
302	      False{}
303	
304	def around.put(+i: Item, +c: T.Pos, rest: List<&2, Item>) -> List<&2, Item>:
305	  match i:
306	    case Item{p, s, ns}:
307	      List.filter.put(Item, i, rest, is_number(s) && B.contains(ns, c))
308	
309	# The numbers of `is` that count c.
310	def around(its: List<&2, Item>, +c: T.Pos) -> List<&2, Item>:
311	  match its:
312	    case Nil{}:
313	      Nil{}
314	    case +i <> t:
315	      around.put(i, c, around(t, c))
316	
317	def todos(+its: List<&2, Item>, cs: List<&2, T.Pos>) -> List<&2, Todo>:
318	  match cs:
319	    case Nil{}:
320	      Nil{}
321	    case +c <> t:
322	      Todo{c, around(its, c)} <> todos(its, t)
323	
324	def has_rel(t: Todo) -> Bool:
325	  match t:
326	    case Todo{c, rel}:
327	      Bool.not(List.is_empty(&2, Item, rel))
328	
329	# The cells next to a number.
330	def nears(ts: List<&2, Todo>) -> List<&2, Todo>:
331	  match ts:
332	    case Nil{}:
333	      Nil{}
334	    case +t <> rest:
335	      List.filter.put(Todo, t, nears(rest), has_rel(t))
336	
337	# The other cells.
338	def fars(ts: List<&2, Todo>) -> List<&2, Todo>:
339	  match ts:
340	    case Nil{}:
341	      Nil{}
342	    case +t <> rest:
343	      List.filter.put(Todo, t, fars(rest), Bool.not(has_rel(t)))
344	
345	# The cells next to a number first, then the rest.
346	def order(+ts: List<&2, Todo>) -> List<&2, Todo>:
347	  List.append(&2, Todo, nears(ts), fars(ts))
348	
349	# The order of a search
350	# ----------------------
351	
352	def todo_c(t: Todo) -> T.Pos:
353	  match t:
354	    case Todo{c, rel}:
355	      c
356	
357	# The numbers around each cell next to one; Nil elsewhere.
358	def rel_grid(+w: Nat, +h: Nat, ts: List<&2, Todo>) -> T.Grid(List<&2, Item>):
359	  match ts:
360	    case Nil{}:
361	      B.blank(List<&2, Item>, w, h, Nil{})
362	    case Todo{c, rel} <> t:
363	      B.set_at(List<&2, Item>, rel_grid(w, h, t), c, rel)
364	
365	# A breadth-first walk over cells linked by a number: the cells to visit,
366	# the cells reached (latest first) and a grid of the cells reached.
367	type Reach is Data:
368	  Reach{queue: List<&2, T.Pos>, order: List<&2, T.Pos>, vis: T.Grid(Bool)}
369	
370	def reach.add.go(fresh: Bool, +p: T.Pos, queue: List<&2, T.Pos>, order: List<&2, T.Pos>, +vis: T.Grid(Bool)) -> Reach:
371	  match fresh:
372	    case True{}:
373	      Reach{List.append(&2, T.Pos, queue, [p]), p <> order, B.set_at(Bool, vis, p, True{})}
374	    case False{}:
375	      Reach{queue, order, vis}
376	
377	# Reach p, if it is next to a number and not reached yet.
378	def reach.add(+p: T.Pos, +relg: T.Grid(List<&2, Item>), r: Reach) -> Reach:
379	  match r:
380	    case Reach{queue, order, +vis}:
381	      reach.add.go(Bool.not(B.at(Bool, True{}, vis, p))
382	        && Bool.not(List.is_empty(&2, Item, B.at(List<&2, Item>, Nil{}, relg, p))), p, queue, order, vis)
383	
384	def reach.ns(ns: List<&2, T.Pos>, +relg: T.Grid(List<&2, Item>), r: Reach) -> Reach:
385	  match ns:
386	    case Nil{}:
387	      r
388	    case p <> t:
389	      reach.ns(t, relg, reach.add(p, relg, r))
390	
391	def reach.items(rel: List<&2, Item>, +relg: T.Grid(List<&2, Item>), r: Reach) -> Reach:
392	  match rel:
393	    case Nil{}:
394	      r
395	    case Item{p, s, ns} <> t:
396	      reach.items(t, relg, reach.ns(ns, relg, r))
397	
398	# Visit cells until none is left to visit (fuel: more than the cells).
399	def reach.run(fuel: Nat, +relg: T.Grid(List<&2, Item>), r: Reach) -> Reach:
400	  match fuel:
401	    case 0n:
402	      r
403	    case 1n+f:
404	      match r:
405	        case Reach{queue, order, vis}:
406	          match queue:
407	            case Nil{}:
408	              Reach{Nil{}, order, vis}
409	            case +q <> rest:
410	              reach.run(f, relg, reach.items(B.at(List<&2, Item>, Nil{}, relg, q), relg, Reach{rest, order, vis}))
411	
412	def reach.order(r: Reach) -> List<&2, T.Pos>:
413	  match r:
414	    case Reach{queue, order, vis}:
415	      List.reverse(&2, T.Pos, order)
416	
417	def reach.start(+w: Nat, +h: Nat) -> Reach:
418	  Reach{Nil{}, Nil{}, B.blank(Bool, w, h, False{})}
419	
420	# The cells linked to c through numbers, nearest first (none when c is next
421	# to no number).
422	def linked(+c: T.Pos, +w: Nat, +h: Nat, +fuel: Nat, +relg: T.Grid(List<&2, Item>)) -> List<&2, T.Pos>:
423	  reach.order(reach.run(fuel, relg, reach.add(c, relg, reach.start(w, h))))
424	
425	def groups.go(ts: List<&2, Todo>, +fuel: Nat, +relg: T.Grid(List<&2, Item>), r: Reach) -> Reach:
426	  match ts:
427	    case Nil{}:
428	      r
429	    case Todo{c, rel} <> t:
430	      groups.go(t, fuel, relg, reach.run(fuel, relg, reach.add(c, relg, r)))
431	
432	# The cells next to a number, one group of linked cells at a time.
433	def groups(+w: Nat, +h: Nat, ts: List<&2, Todo>, +fuel: Nat, +relg: T.Grid(List<&2, Item>)) -> List<&2, T.Pos>:
434	  reach.order(groups.go(ts, fuel, relg, reach.start(w, h)))
435	
436	def with_c(ts: List<&2, Todo>, +q: T.Pos) -> List<&2, Todo>:
437	  match ts:
438	    case Nil{}:
439	      Nil{}
440	    case +t <> rest:
441	      List.filter.put(Todo, t, with_c(rest, q), B.same(todo_c(t), q))
442	
443	# The todos of ts for the cells qs, in the order of qs.
444	def gather(qs: List<&2, T.Pos>, +ts: List<&2, Todo>) -> List<&2, Todo>:
445	  match qs:
446	    case Nil{}:
447	      Nil{}
448	    case q <> t:
449	      List.append(&2, Todo, with_c(ts, q), gather(t, ts))
450	
451	# ts from its k-th element on, then the first k.
452	def rot(+ts: List<&2, Todo>, +k: Nat) -> List<&2, Todo>:
453	  List.append(&2, Todo, List.drop(&2, Todo, ts, k), List.take(&2, Todo, ts, k))
454	
455	# How far to rotate the far cells for c: searches for nearby cells start
456	# about n cells apart, so their layouts mine different far cells.
457	def spin(c: T.Pos, +w: Nat, +n: Nat, +nf: Nat) -> Nat:
458	  match c:
459	    case T.Pos{x, y}:
460	      Nat.mod(Nat.mul(Nat.add(Nat.mul(y, w), x), Nat.add(n, 1n)), Nat.add(nf, 1n))
461	
462	# What every search of a solve shares: the cells next to a number and the
463	# rest, the groups, the plain order, and the numbers around each cell.
464	type Plan is Data:
465	  Plan{near: List<&2, Todo>, far: List<&2, Todo>, nf: Nat, gq: List<&2, T.Pos>, base: List<&2, Todo>,
466	    fuel: Nat, relg: T.Grid(List<&2, Item>)}
467	
468	def plan(+w: Nat, +h: Nat, +ts: List<&2, Todo>) -> Plan:
469	  +near = nears(ts)
470	  +far = fars(ts)
471	  +fuel = Nat.add(List.length(&2, Todo, near), 1n)
472	  +relg = rel_grid(w, h, near)
473	  Plan{near, far, List.length(&2, Todo, far), groups(w, h, near, fuel, relg), order(ts), fuel, relg}
474	
475	# The order of the search for c.
476	def plan_todo(+c: T.Pos, pl: Plan, +ctx: Ctx) -> List<&2, Todo>:
477	  match pl:
478	    case Plan{+near, far, +nf, gq, base, +fuel, +relg}:
479	      match ctx:
480	        case Ctx{+w, +h, +n, rows, items}:
481	          List.append(&2, Todo, gather(List.append(&2, T.Pos, linked(c, w, h, fuel, relg), gq), near),
482	            List.append(&2, Todo, rot(far, spin(c, w, n, nf)), base))
483	
484	# The outer loop
485	# --------------
486	
487	def covered(ls: List<&2, T.Grid(Bool)>, +c: T.Pos) -> Bool:
488	  match ls:
489	    case Nil{}:
490	      False{}
491	    case l <> t:
492	      B.mine(l, c) || covered(t, c)
493	
494	# A consistent layout with a mine on c, if there is one.
495	def search(+c: T.Pos, +pl: Plan, +part: T.Grid(Maybe<&2, Bool>), +ctx: Ctx) ->
496	  Maybe<&2, T.Grid(Bool)>:
497	  +p = B.set_at(Maybe<&2, Bool>, part, c, Some{True{}})
498	  dfs2(plan_todo(c, pl, ctx), p, part_true(p), part_none(p), ctx)
499	
500	def loop.if(b: Bool, yes: Unit -> Maybe<&2, T.Pos>, no: Unit -> Maybe<&2, T.Pos>) ->
501	  Maybe<&2, T.Pos>:
502	  match b:
503	    case True{}:
504	      yes(Unit{})
505	    case False{}:
506	      no(Unit{})
507	
508	def loop.found(r: Maybe<&2, T.Grid(Bool)>, c: T.Pos,
509	  k: T.Grid(Bool) -> Maybe<&2, T.Pos>) -> Maybe<&2, T.Pos>:
510	  match r:
511	    case None{}:
512	      Some{c}
513	    case Some{l}:
514	      k(l)
515	
516	# The first cell of hs that no consistent layout mines, given layouts
517	# `found` already shown consistent.
518	def loop(hs: List<&2, T.Pos>, +found: List<&2, T.Grid(Bool)>, +pl: Plan,
519	  +part: T.Grid(Maybe<&2, Bool>), +ctx: Ctx) -> Maybe<&2, T.Pos>:
520	  match hs:
521	    case Nil{}:
522	      None{}
523	    case +c <> +t:
524	      loop.if(covered(found, c),
525	        u => loop(t, found, pl, part, ctx),
526	        v => loop.found(search(c, pl, part, ctx), c,
527	          l => loop(t, l <> found, pl, part, ctx)))
528	
529	def solve.go(ok: Bool, +hs: List<&2, T.Pos>, +w: Nat, +h: Nat, n: Nat,
530	  +rows: T.Grid(T.Seen)) -> Maybe<&2, T.Pos>:
531	  match ok:
532	    case False{}:
533	      List.head(&2, T.Pos, hs)
534	    case True{}:
535	      +its = items(w, h, rows, B.cells(w, h))
536	      loop(hs, Nil{}, plan(w, h, todos(its, hs)), start(rows), Ctx{w, h, n, rows, its})
537	
538	# A provably safe hidden cell, or None when every hidden cell might hold a
539	# mine.
540	def solve(k: T.Knowledge) -> Maybe<&2, T.Pos>:
541	  match k:
542	    case T.Knowledge{+w, +h, n, +rows}:
543	      solve.go(B.shaped(T.Seen, w, h, rows), hidden_cells(rows, B.cells(w, h)), w, h, n, rows)