# 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 Base
import ./grid.bend as G
import ./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}:
      d

def Conf.side(cf: Conf) -> U32:
  match cf:
    case Conf{d, sd, b, m, s, sx, sy}:
      sd

def Conf.bits(cf: Conf) -> Nat:
  match cf:
    case Conf{d, sd, b, m, s, sx, sy}:
      b

def Conf.mines(cf: Conf) -> U32:
  match cf:
    case Conf{d, sd, b, m, s, sx, sy}:
      m

def Conf.seed(cf: Conf) -> U32:
  match cf:
    case Conf{d, sd, b, m, s, sx, sy}:
      s

def Conf.sx(cf: Conf) -> U32:
  match cf:
    case Conf{d, sd, b, m, s, sx, sy}:
      sx

def Conf.sy(cf: Conf) -> U32:
  match cf:
    case Conf{d, sd, b, m, s, sx, sy}:
      sy

def 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}:
      cf

def Layout.mines(ly: Layout) -> G.Grid<&2, Bool>:
  match ly:
    case Layout{cf, mg}:
      mg

def Field.conf(fd: Field) -> Conf:
  match fd:
    case Field{cf, cg}:
      cf

def Field.cells(fd: Field) -> G.Grid<&2, C.Cell>:
  match fd:
    case Field{cf, cg}:
      cg

def Chord.conf(ch: Chord) -> Conf:
  match ch:
    case Chord{cf, cg, cx, cy}:
      cf

def Chord.cells(ch: Chord) -> G.Grid<&2, C.Cell>:
  match ch:
    case Chord{cf, cg, cx, cy}:
      cg

def Chord.cx(ch: Chord) -> U32:
  match ch:
    case Chord{cf, cg, cx, cy}:
      cx

def 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)