cell.bend source

cell.bend on the hub · documented module

# Cell: one square of the board, and the two moves that act on it.# ================================================================## A cell carries three facts: whether it hides a mine, how many mines# touch it, and what the player has done to it. `near` is fixed when# the board is laid out. `mine` is fixed for the whole game. Only# `mark` moves, and it moves through a small state machine:##   Hidden  --flag-->  Flagged  --flag-->  Hidden#   Hidden  --open-->  Shown## A flag blocks an open, and a shown cell is final. LAWS.bend states# these as claims, and PROOF.bend proves them.import Basetype Mark is Data:  Hidden{}  Flagged{}  Shown{}type Cell is Data:  Cell{mine: Bool, near: U32, mark: Mark}def Mark.is_hidden(k: Mark) -> Bool:  match k:    case Hidden{}:      True{}    case Flagged{}:      False{}    case Shown{}:      False{}def Mark.is_flagged(k: Mark) -> Bool:  match k:    case Hidden{}:      False{}    case Flagged{}:      True{}    case Shown{}:      False{}def Mark.is_shown(k: Mark) -> Bool:  match k:    case Hidden{}:      False{}    case Flagged{}:      False{}    case Shown{}:      True{}# A flag on a mine stays a flag, so a won board keeps its flags.# Anything else on a mine comes up when the game is lost.def Mark.expose(k: Mark) -> Mark:  match k:    case Hidden{}:      Shown{}    case Flagged{}:      Flagged{}    case Shown{}:      Shown{}def Cell.is_mine(c: Cell) -> Bool:  match c:    case Cell{m, n, k}:      mdef Cell.near(c: Cell) -> U32:  match c:    case Cell{m, n, k}:      ndef Cell.mark(c: Cell) -> Mark:  match c:    case Cell{m, n, k}:      kdef Cell.is_hidden(c: Cell) -> Bool:  match c:    case Cell{m, n, k}:      Mark.is_hidden(k)def Cell.is_shown(c: Cell) -> Bool:  match c:    case Cell{m, n, k}:      Mark.is_shown(k)def Cell.is_flagged(c: Cell) -> Bool:  match c:    case Cell{m, n, k}:      Mark.is_flagged(k)# Right-click. It turns a flag on or off and leaves a shown cell alone.def Cell.flag(c: Cell) -> Cell:  match c:    case Cell{m, n, k}:      match k:        case Hidden{}:          Cell{m, n, Flagged{}}        case Flagged{}:          Cell{m, n, Hidden{}}        case Shown{}:          Cell{m, n, Shown{}}# Left-click. A flagged cell does not open; a shown cell does not change.def Cell.open(c: Cell) -> Cell:  match c:    case Cell{m, n, k}:      match k:        case Hidden{}:          Cell{m, n, Shown{}}        case Flagged{}:          Cell{m, n, Flagged{}}        case Shown{}:          Cell{m, n, Shown{}}# The end of a lost game: every mine that is not flagged comes up.def Cell.expose(c: Cell) -> Cell:  match c:    case Cell{m, n, k}:      match m:        case True{}:          Cell{True{}, n, Mark.expose(k)}        case False{}:          Cell{False{}, n, k}# A shown cell with no mine next to it. The flood spreads out of these.def Cell.is_open_blank(c: Cell) -> Bool:  match c:    case Cell{m, n, k}:      Bool.and(Mark.is_shown(k), U32.is_eq(n, 0))# Counters. Grid.sum adds these up over the whole board in parallel.def Cell.one_shown(c: Cell) -> U32:  Bool.to_u32(Cell.is_shown(c))def Cell.one_flag(c: Cell) -> U32:  Bool.to_u32(Cell.is_flagged(c))def Cell.one_mine(c: Cell) -> U32:  Bool.to_u32(Cell.is_mine(c))# A shown mine. One of these means the game is lost.def Cell.one_boom(c: Cell) -> U32:  match c:    case Cell{m, n, k}:      Bool.to_u32(Bool.and(m, Mark.is_shown(k)))