board.bend source
board.bend on the hub · documented module
# Board: the rules of Minesweeper, written as parallel grid passes.# =================================================================## Every rule here is one pass over the whole board. A pass reads the# old board and writes a new one, so the four quadrants never race and# Bend can fork them onto four cores. The board is Data, so each leaf# of a pass holds its own reference to the old board and reads any# cell it likes.## Mine layout is the one part that is not obvious. A cell is a mine# when fewer than `mines` other cells sort before it, under a strict# total order on (hash, index). Exactly `mines` cells can win that# race, so the count is exact without a shuffle, and each cell decides# on its own with no coordination.import Baseimport ./grid.bend as Gimport ./cell.bend as C# depth: the quadtree depth. side: 2^depth. bits: 2*depth, the index width.# sx, sy: the first click. That cell and its eight neighbours never# get a mine, so the first click always opens a region.type Conf is Data: Conf{depth: Nat, side: U32, bits: Nat, mines: U32, seed: U32, sx: U32, sy: U32}type Phase is Data: Playing{} Won{} Lost{}def Phase.is_playing(p: Phase) -> Bool: match p: case Playing{}: True{} case Won{}: False{} case Lost{}: False{}def Phase.is_lost(p: Phase) -> Bool: match p: case Playing{}: False{} case Won{}: False{} case Lost{}: True{}# The payload of a mine-layout pass.type Layout is Data: Layout{conf: Conf, mines: G.Grid<&2, Bool>}# The payload of a flood pass.type Field is Data: Field{conf: Conf, cells: G.Grid<&2, C.Cell>}# The payload of a chord pass. cx, cy is the cell that was chorded.type Chord is Data: Chord{conf: Conf, cells: G.Grid<&2, C.Cell>, cx: U32, cy: U32}def Conf.depth(cf: Conf) -> Nat: match cf: case Conf{d, sd, b, m, s, sx, sy}: ddef Conf.side(cf: Conf) -> U32: match cf: case Conf{d, sd, b, m, s, sx, sy}: sddef Conf.bits(cf: Conf) -> Nat: match cf: case Conf{d, sd, b, m, s, sx, sy}: bdef Conf.mines(cf: Conf) -> U32: match cf: case Conf{d, sd, b, m, s, sx, sy}: mdef Conf.seed(cf: Conf) -> U32: match cf: case Conf{d, sd, b, m, s, sx, sy}: sdef Conf.sx(cf: Conf) -> U32: match cf: case Conf{d, sd, b, m, s, sx, sy}: sxdef Conf.sy(cf: Conf) -> U32: match cf: case Conf{d, sd, b, m, s, sx, sy}: sydef Conf.cells(+cf: Conf) -> U32: (Conf.side(cf) * Conf.side(cf) : U32)# Builds a config. `mines` must leave room for the nine safe cells.def Conf.new(+d: Nat, mines: U32, seed: U32, sx: U32, sy: U32) -> Conf: Conf{d, U32.shln(1, d), Nat.add(d, d), mines, seed, sx, sy}# Moves the safe cell. The first click calls this, then lays the board out.def Conf.aim(cf: Conf, sx: U32, sy: U32) -> Conf: match cf: case Conf{d, sd, b, m, s, ox, oy}: Conf{d, sd, b, m, s, sx, sy}def Layout.conf(ly: Layout) -> Conf: match ly: case Layout{cf, mg}: cfdef Layout.mines(ly: Layout) -> G.Grid<&2, Bool>: match ly: case Layout{cf, mg}: mgdef Field.conf(fd: Field) -> Conf: match fd: case Field{cf, cg}: cfdef Field.cells(fd: Field) -> G.Grid<&2, C.Cell>: match fd: case Field{cf, cg}: cgdef Chord.conf(ch: Chord) -> Conf: match ch: case Chord{cf, cg, cx, cy}: cfdef Chord.cells(ch: Chord) -> G.Grid<&2, C.Cell>: match ch: case Chord{cf, cg, cx, cy}: cgdef Chord.cx(ch: Chord) -> U32: match ch: case Chord{cf, cg, cx, cy}: cxdef Chord.cy(ch: Chord) -> U32: match ch: case Chord{cf, cg, cx, cy}: cy# A 32-bit avalanche hash. Two cells one apart land far apart.def Board.hash(+s: U32, i: U32) -> U32: +a = (i * 2654435761 + s + 374761393 : U32) +b = U32.xor(a, U32.shrn(a, 15n)) +c = (b * 2246822519 : U32) +e = U32.xor(c, U32.shrn(c, 13n)) +f = (e * 3266489917 : U32) U32.xor(f, U32.shrn(f, 16n))# True when a is within one step of b. The subtraction wraps, so a# single unsigned test covers both sides and the edge of the board.def Board.within1(a: U32, b: U32) -> Bool: U32.is_le(U32.sub((a + 1 : U32), b), 2)def Board.in_board(+cf: Conf, x: U32, y: U32) -> Bool: +sd = Conf.side(cf) Bool.and(U32.is_lt(x, sd), U32.is_lt(y, sd))# The nine cells around the first click.def Board.in_safe(+cf: Conf, x: U32, y: U32) -> Bool: Bool.and(Board.within1(x, Conf.sx(cf)), Board.within1(y, Conf.sy(cf)))# A safe cell keeps the largest odd key; every other key is even.# The two ranges cannot tie, so no safe cell is ever picked while# `mines` leaves at least that many cells outside the safe block.def Board.key.pick(+cf: Conf, idx: U32, safe: Bool) -> U32: match safe: case True{}: 4294967295 case False{}: U32.and(Board.hash(Conf.seed(cf), idx), 4294967294)def Board.key(+cf: Conf, +idx: U32) -> U32: +sd = Conf.side(cf) x = U32.and(idx, (sd - 1 : U32)) y = U32.shrn(idx, Conf.depth(cf)) Board.key.pick(cf, idx, Board.in_safe(cf, x, y))# The strict total order. The index breaks a tie between equal keys.def Board.before(+cf: Conf, +j: U32, +ki: U32, ii: U32) -> Bool: +kj = Board.key(cf, j) Bool.or(U32.is_lt(kj, ki), Bool.and(U32.is_eq(kj, ki), U32.is_lt(j, ii)))# Counts the cells that sort before (ki, ii). The index range splits in# two at every step, so the whole count is a parallel reduction.def Board.rank(bits: Nat, +cf: Conf, +ki: U32, +ii: U32, +base: U32) -> U32: match bits: case 0n: Bool.to_u32(Board.before(cf, base, ki, ii)) case Succ{+b}: +h = U32.shln(1, b) lo hi = Board.rank(b, cf, ki, ii, base) Board.rank(b, cf, ki, ii, (base + h : U32)) (lo + hi : U32)# True when the cell at (x, y) hides a mine.def Board.mine_at(+cf: Conf, +x: U32, +y: U32) -> Bool: +idx = (y * Conf.side(cf) + x : U32) +k = Board.key(cf, idx) U32.is_lt(Board.rank(Conf.bits(cf), cf, k, idx, 0), Conf.mines(cf))# Reads one neighbour of a Bool grid. Off the board counts as 0.def Board.one_mine.pick(d: Nat, mg: G.Grid<&2, Bool>, x: U32, y: U32, ok: Bool) -> U32: match ok: case False{}: 0 case True{}: Bool.to_u32(G.Grid.get(Bool, mg, G.Grid.path(d, x, y)))def Board.one_mine(+cf: Conf, mg: G.Grid<&2, Bool>, +x: U32, +y: U32) -> U32: Board.one_mine.pick(Conf.depth(cf), mg, x, y, Board.in_board(cf, x, y))# Reads one neighbour of a Cell grid and asks whether the flood may# cross it: a shown cell with no mine next to it.def Board.one_blank.pick(d: Nat, cg: G.Grid<&2, C.Cell>, x: U32, y: U32, ok: Bool) -> U32: match ok: case False{}: 0 case True{}: Bool.to_u32(C.Cell.is_open_blank(G.Grid.get(C.Cell, cg, G.Grid.path(d, x, y))))def Board.one_blank(+cf: Conf, cg: G.Grid<&2, C.Cell>, +x: U32, +y: U32) -> U32: Board.one_blank.pick(Conf.depth(cf), cg, x, y, Board.in_board(cf, x, y))# Reads one neighbour of a Cell grid and asks whether it carries a flag.def Board.one_flag.pick(d: Nat, cg: G.Grid<&2, C.Cell>, x: U32, y: U32, ok: Bool) -> U32: match ok: case False{}: 0 case True{}: Bool.to_u32(C.Cell.is_flagged(G.Grid.get(C.Cell, cg, G.Grid.path(d, x, y))))def Board.one_flag(+cf: Conf, cg: G.Grid<&2, C.Cell>, +x: U32, +y: U32) -> U32: Board.one_flag.pick(Conf.depth(cf), cg, x, y, Board.in_board(cf, x, y))# Adds a per-cell number over the eight neighbours of (x, y).# The eight reads are the same depth, so they finish together, which# is what a fork-join scheduler needs to stay busy.def Board.around( ~T: Data, ~f: @+a: Conf -> @b: G.Grid<&2, T> -> @+u: U32 -> @+v: U32 -> U32, +cf: Conf, +cg: G.Grid<&2, T>, +x: U32, +y: U32) -> U32: +xa = (x - 1 : U32) +xc = (x + 1 : U32) +ya = (y - 1 : U32) +yc = (y + 1 : U32) n1 n2 n3 n4 n5 n6 n7 n8 = f(cf, cg, xa, ya) f(cf, cg, x, ya) f(cf, cg, xc, ya) f(cf, cg, xa, y) f(cf, cg, xc, y) f(cf, cg, xa, yc) f(cf, cg, x, yc) f(cf, cg, xc, yc) (n1 + n2 + n3 + n4 + n5 + n6 + n7 + n8 : U32)# Lays out one cell: its own mine bit, and the count of mines touching it.def Board.cell_at(+ly: Layout, +x: U32, +y: U32) -> C.Cell: +cf = Layout.conf(ly) +mg = Layout.mines(ly) mine = G.Grid.get(Bool, mg, G.Grid.path(Conf.depth(cf), x, y)) near = Board.around(~Bool, ~Board.one_mine, cf, mg, x, y) C.Cell{mine, near, C.Hidden{}}# Lays out the whole board. Two parallel passes: mines, then counts.def Board.make(+cf: Conf) -> G.Grid<&2, C.Cell>: mg = G.Grid.init(~Bool, ~Conf, ~Board.mine_at, Conf.depth(cf), cf, 0, 0) G.Grid.init(~C.Cell, ~Layout, ~Board.cell_at, Conf.depth(cf), Layout{cf, mg}, 0, 0)def Board.spread_at.pick(c: C.Cell, go: Bool) -> C.Cell: match go: case True{}: C.Cell.open(c) case False{}: c# One round of the flood: a hidden cell next to an open blank opens.def Board.spread_at(+fd: Field, +x: U32, +y: U32) -> C.Cell: +cf = Field.conf(fd) +cg = Field.cells(fd) +me = G.Grid.get(C.Cell, cg, G.Grid.path(Conf.depth(cf), x, y)) near = U32.is_ne(Board.around(~C.Cell, ~Board.one_blank, cf, cg, x, y), 0) Board.spread_at.pick(me, Bool.and(C.Cell.is_hidden(me), near))def Board.spread(+fd: Field) -> G.Grid<&2, C.Cell>: G.Grid.init(~C.Cell, ~Field, ~Board.spread_at, Conf.depth(Field.conf(fd)), fd, 0, 0)def Board.shown(+cg: G.Grid<&2, C.Cell>) -> U32: G.Grid.sum(~C.Cell, ~C.Cell.one_shown, cg)def Board.flags(+cg: G.Grid<&2, C.Cell>) -> U32: G.Grid.sum(~C.Cell, ~C.Cell.one_flag, cg)def Board.booms(+cg: G.Grid<&2, C.Cell>) -> U32: G.Grid.sum(~C.Cell, ~C.Cell.one_boom, cg)# Runs rounds until nothing more opens. Every round that keeps going# opens at least one cell, so the cell count is fuel enough.# `alive` is a parameter, not a test on a computed value, because a# match may only scrutinise a parameter.def Board.flood( fuel: Nat, alive: Bool, +cf: Conf, cg: G.Grid<&2, C.Cell>, before: U32) -> G.Grid<&2, C.Cell>: match fuel alive: case 0n k: cg case Succ{f} False{}: cg case Succ{f} True{}: +next = Board.spread(Field{cf, cg}) +after = Board.shown(next) Board.flood(f, U32.is_ne(after, before), cf, next, after)def Board.flood_all(+cf: Conf, +cg: G.Grid<&2, C.Cell>) -> G.Grid<&2, C.Cell>: Board.flood(U32.to_nat(Conf.cells(cf)), True{}, cf, cg, Board.shown(cg))# Left-click: open the cell, then let the flood run out of it.def Board.open_at(+cf: Conf, +cg: G.Grid<&2, C.Cell>, x: U32, y: U32) -> G.Grid<&2, C.Cell>: +pt = G.Grid.path(Conf.depth(cf), x, y) c = G.Grid.get(C.Cell, cg, pt) Board.flood_all(cf, G.Grid.set(C.Cell, cg, pt, C.Cell.open(c)))# Right-click: turn a flag on or off.def Board.flag_at(+cf: Conf, +cg: G.Grid<&2, C.Cell>, x: U32, y: U32) -> G.Grid<&2, C.Cell>: +pt = G.Grid.path(Conf.depth(cf), x, y) c = G.Grid.get(C.Cell, cg, pt) G.Grid.set(C.Cell, cg, pt, C.Cell.flag(c))def Board.chord_cell.pick(c: C.Cell, go: Bool) -> C.Cell: match go: case True{}: C.Cell.open(c) case False{}: c# The chord pass: every hidden cell touching (cx, cy) opens.def Board.chord_cell(+ch: Chord, +x: U32, +y: U32) -> C.Cell: +cf = Chord.conf(ch) +cg = Chord.cells(ch) +me = G.Grid.get(C.Cell, cg, G.Grid.path(Conf.depth(cf), x, y)) touch = Bool.and(Board.within1(x, Chord.cx(ch)), Board.within1(y, Chord.cy(ch))) Board.chord_cell.pick(me, Bool.and(C.Cell.is_hidden(me), touch))def Board.chord_go(+cf: Conf, +cg: G.Grid<&2, C.Cell>, x: U32, y: U32, ok: Bool) -> G.Grid<&2, C.Cell>: match ok: case False{}: cg case True{}: opened = G.Grid.init( ~C.Cell, ~Chord, ~Board.chord_cell, Conf.depth(cf), Chord{cf, cg, x, y}, 0, 0) Board.flood_all(cf, opened)# Middle-click, or a left-click on a number that already has its flags.# It opens every hidden neighbour at once. That is how a player clears# a board fast, and it is how a careless player loses one.def Board.chord_at(+cf: Conf, +cg: G.Grid<&2, C.Cell>, +x: U32, +y: U32) -> G.Grid<&2, C.Cell>: +me = G.Grid.get(C.Cell, cg, G.Grid.path(Conf.depth(cf), x, y)) +n = C.Cell.near(me) ready = Bool.and(U32.is_ne(n, 0), U32.is_eq(Board.around(~C.Cell, ~Board.one_flag, cf, cg, x, y), n)) Board.chord_go(cf, cg, x, y, Bool.and(C.Cell.is_shown(me), ready))# The end of a lost game: every mine that is not flagged comes up.def Board.expose(cg: G.Grid<&2, C.Cell>) -> G.Grid<&2, C.Cell>: G.Grid.map(~C.Cell, ~C.Cell, ~C.Cell.expose, cg)# Where the mines are, with every move the player made stripped off.# LAWS.bend uses this to say that no move ever shifts a mine.def Board.mines_of(cg: G.Grid<&2, C.Cell>) -> G.Grid<&2, Bool>: G.Grid.map(~C.Cell, ~Bool, ~C.Cell.is_mine, cg)def Board.status.pick(lost: Bool, won: Bool) -> Phase: match lost won: case True{} w: Lost{} case False{} True{}: Won{} case False{} False{}: Playing{}# A shown mine loses. Every other cell shown wins.def Board.status(+cf: Conf, +cg: G.Grid<&2, C.Cell>) -> Phase: lost = U32.is_ne(Board.booms(cg), 0) won = U32.is_eq((Board.shown(cg) + Conf.mines(cf) : U32), Conf.cells(cf)) Board.status.pick(lost, won)