board.bend

minebender-game@1.0.0.0 · 144 lines · 25 definitions

1import Base
2import minebender-game@1.0.0.0/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
8def 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
14def mine(layout: T.Grid(Bool), p: T.Pos) -> Bool:
15  at(Bool, False{}, layout, p)
16
17def 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
22def 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
27def dist(+a: Nat, +b: Nat) -> Nat:
28  Nat.add(Nat.sub(a, b), Nat.sub(b, a))
29
30def 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
35def adjacent(+p: T.Pos, +q: T.Pos) -> Bool:
36  Bool.not(same(p, q)) && within_one(p, q)
37
38def 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
45def 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
52def cells(w: Nat, h: Nat) -> List<&2, T.Pos>:
53  cells.go(w, List.range(h))
54
55def 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
62def neighbours(w: Nat, h: Nat, p: T.Pos) -> List<&2, T.Pos>:
63  touching(p, cells(w, h))
64
65def 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
72def adj_mines(w: Nat, h: Nat, layout: T.Grid(Bool), p: T.Pos) -> Nat:
73  count_mines(layout, neighbours(w, h, p))
74
75def 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
82def 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
89def 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
93def 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
100def 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).
107def 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.
114def 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
117def 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.
125def 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
132def 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
139def 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)))