# 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 Base

type 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}:
      m

def Cell.near(c: Cell) -> U32:
  match c:
    case Cell{m, n, k}:
      n

def Cell.mark(c: Cell) -> Mark:
  match c:
    case Cell{m, n, k}:
      k

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