1	import Base
2	import ./types.bend as T
3	
4	# Board helpers for the game. The ones named after a definition in LAWS.bend
5	# are copies of it (the code cannot import the laws), proven equal to it in
6	# the proofs.
7	
8	def at(-A: Data, d: A, g: T.Grid(A), p: T.Pos) -> A:
9	  match p:
10	    case T.Pos{x, y}:
11	      row = Maybe.default(&2, List<&2, A>, List.get(&2, List<&2, A>, g, y), Nil{})
12	      Maybe.default(&2, A, List.get(&2, A, row, x), d)
13	
14	def mine(layout: T.Grid(Bool), p: T.Pos) -> Bool:
15	  at(Bool, False{}, layout, p)
16	
17	def on_board(w: Nat, h: Nat, p: T.Pos) -> Bool:
18	  match p:
19	    case T.Pos{x, y}:
20	      Nat.is_lt(x, w) && Nat.is_lt(y, h)
21	
22	def same(p: T.Pos, q: T.Pos) -> Bool:
23	  match p q:
24	    case T.Pos{px, py} T.Pos{qx, qy}:
25	      Nat.is_eq(px, qx) && Nat.is_eq(py, qy)
26	
27	def dist(+a: Nat, +b: Nat) -> Nat:
28	  Nat.add(Nat.sub(a, b), Nat.sub(b, a))
29	
30	def within_one(p: T.Pos, q: T.Pos) -> Bool:
31	  match p q:
32	    case T.Pos{px, py} T.Pos{qx, qy}:
33	      Nat.is_le(dist(px, qx), 1n) && Nat.is_le(dist(py, qy), 1n)
34	
35	def adjacent(+p: T.Pos, +q: T.Pos) -> Bool:
36	  Bool.not(same(p, q)) && within_one(p, q)
37	
38	def row_cells(+y: Nat, xs: List<&2, Nat>) -> List<&2, T.Pos>:
39	  match xs:
40	    case Nil{}:
41	      Nil{}
42	    case x <> t:
43	      T.Pos{x, y} <> row_cells(y, t)
44	
45	def cells.go(+w: Nat, ys: List<&2, Nat>) -> List<&2, T.Pos>:
46	  match ys:
47	    case Nil{}:
48	      Nil{}
49	    case y <> t:
50	      List.append(&2, T.Pos, row_cells(y, List.range(w)), cells.go(w, t))
51	
52	def cells(w: Nat, h: Nat) -> List<&2, T.Pos>:
53	  cells.go(w, List.range(h))
54	
55	def touching(+p: T.Pos, qs: List<&2, T.Pos>) -> List<&2, T.Pos>:
56	  match qs:
57	    case Nil{}:
58	      Nil{}
59	    case +q <> t:
60	      List.filter.put(T.Pos, q, touching(p, t), adjacent(p, q))
61	
62	def neighbours(w: Nat, h: Nat, p: T.Pos) -> List<&2, T.Pos>:
63	  touching(p, cells(w, h))
64	
65	def count_mines(+layout: T.Grid(Bool), ps: List<&2, T.Pos>) -> Nat:
66	  match ps:
67	    case Nil{}:
68	      0n
69	    case q <> t:
70	      Nat.add(Bool.pick(Nat, mine(layout, q), 1n, 0n), count_mines(layout, t))
71	
72	def adj_mines(w: Nat, h: Nat, layout: T.Grid(Bool), p: T.Pos) -> Nat:
73	  count_mines(layout, neighbours(w, h, p))
74	
75	def row_mines(row: List<&2, Bool>) -> Nat:
76	  match row:
77	    case Nil{}:
78	      0n
79	    case b <> t:
80	      Nat.add(Bool.pick(Nat, b, 1n, 0n), row_mines(t))
81	
82	def total_mines(layout: T.Grid(Bool)) -> Nat:
83	  match layout:
84	    case Nil{}:
85	      0n
86	    case r <> t:
87	      Nat.add(row_mines(r), total_mines(t))
88	
89	def zero(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +p: T.Pos) -> Bool:
90	  on_board(w, h, p) && Bool.not(mine(layout, p))
91	    && Nat.is_eq(adj_mines(w, h, layout, p), 0n)
92	
93	def rows_wide(-A: Data, +w: Nat, g: T.Grid(A)) -> Bool:
94	  match g:
95	    case Nil{}:
96	      True{}
97	    case r <> t:
98	      Nat.is_eq(List.length(&2, A, r), w) && rows_wide(A, w, t)
99	
100	def shaped(-A: Data, w: Nat, h: Nat, +g: T.Grid(A)) -> Bool:
101	  Nat.is_eq(List.length(&2, List<&2, A>, g), h) && rows_wide(A, w, g)
102	
103	# Game-only helpers
104	# -----------------
105	
106	# The grid g with the cell at p replaced by v (unchanged when p is off it).
107	def set_at(-A: Data, +g: T.Grid(A), p: T.Pos, v: A) -> T.Grid(A):
108	  match p:
109	    case T.Pos{x, +y}:
110	      row = Maybe.default(&2, List<&2, A>, List.get(&2, List<&2, A>, g, y), Nil{})
111	      List.set(&2, List<&2, A>, g, y, List.set(&2, A, row, x, v))
112	
113	# A w-by-h grid of v.
114	def blank(-A: Data, w: Nat, h: Nat, +v: A) -> T.Grid(A):
115	  List.replicate(List<&2, A>, h, List.replicate(A, w, v))
116	
117	def row_false(row: List<&2, Bool>) -> Nat:
118	  match row:
119	    case Nil{}:
120	      0n
121	    case b <> t:
122	      Nat.add(Bool.pick(Nat, b, 0n, 1n), row_false(t))
123	
124	# How many cells of the grid are False.
125	def count_false(g: T.Grid(Bool)) -> Nat:
126	  match g:
127	    case Nil{}:
128	      0n
129	    case r <> t:
130	      Nat.add(row_false(r), count_false(t))
131	
132	def contains(xs: List<&2, T.Pos>, +p: T.Pos) -> Bool:
133	  match xs:
134	    case Nil{}:
135	      False{}
136	    case q <> t:
137	      same(q, p) || contains(t, p)
138	
139	def remove(xs: List<&2, T.Pos>, +p: T.Pos) -> List<&2, T.Pos>:
140	  match xs:
141	    case Nil{}:
142	      Nil{}
143	    case +q <> t:
144	      List.filter.put(T.Pos, q, remove(t, p), Bool.not(same(q, p)))