## TinyChess — the board and the way the pieces move.
##
## Four files by four ranks, kings and pawns, a queen and a knight. Everything in
## this file is COMPUTABLE and has no holes: squares are numbers, the
## step rules are Bools, and the checker can simply run them. That is
## deliberate, because it is what lets the counterexample search in the
## editor walk a claim and hand you the two squares that break it.
##
## What is NOT here is the game: occupancy, captures against a real
## position, check, and mate. Those live in game.bend; the laws about them
## are stated in LAWS.bend and proved, where they are proved, in PROOF.bend.
##
## Squares are 0..15, counting along the files first:
##
##       a  b  c  d
##   4  12 13 14 15      rank 4, black's back rank
##   3   8  9 10 11
##   2   4  5  6  7
##   1   0  1  2  3      rank 1, white's back rank
##
## so file = s mod 4 and rank = s div 4, and both are written out by
## structural recursion rather than by arithmetic, because the checker
## evaluates a Nat one successor at a time and these stay under sixteen.

import Base

# ---- the small arithmetic these rules need -------------------------------

def nat_eq(a: Nat, b: Nat) -> Bool:
  match a:
    case 0n:
      match b:
        case 0n:
          True{}
        case 1n+q:
          False{}
    case 1n+p:
      match b:
        case 0n:
          False{}
        case 1n+q:
          nat_eq(p, q)

def nat_lt(a: Nat, b: Nat) -> Bool:
  match a:
    case 0n:
      match b:
        case 0n:
          False{}
        case 1n+q:
          True{}
    case 1n+p:
      match b:
        case 0n:
          False{}
        case 1n+q:
          nat_lt(p, q)

# the distance between two numbers, whichever way round they are
def gap(a: Nat, b: Nat) -> Nat:
  match a:
    case 0n:
      b
    case 1n+p:
      match b:
        case 0n:
          1n+p
        case 1n+q:
          gap(p, q)

# ---- the board's geometry ------------------------------------------------

# which file a square is on: 0 is the a-file, 3 is the d-file
def file(s: Nat) -> Nat:
  match s:
    case 0n:
      0n
    case 1n+a:
      match a:
        case 0n:
          1n
        case 1n+b:
          match b:
            case 0n:
              2n
            case 1n+c:
              match c:
                case 0n:
                  3n
                case 1n+d:
                  file(d)

# which rank a square is on: 0 is white's back rank, 3 is black's
def rank(s: Nat) -> Nat:
  match s:
    case 0n:
      0n
    case 1n+a:
      match a:
        case 0n:
          0n
        case 1n+b:
          match b:
            case 0n:
              0n
            case 1n+c:
              match c:
                case 0n:
                  0n
                case 1n+d:
                  r = rank(d)
                  1n+r

# a square is on the board when it is one of the sixteen
def on_board(s: Nat) -> Bool:
  nat_lt(s, 16n)

# ---- how each piece steps, on an empty board -----------------------------

# A king steps to a touching square: at most one file across, at most one
# rank up or down, and never onto the square it is already on.
def king_step(+a: Nat, +b: Nat) -> Bool:
  Bool.and(
    Bool.and(on_board(a), on_board(b)),
    Bool.and(
      Bool.not(nat_eq(a, b)),
      Bool.and(nat_lt(gap(file(a), file(b)), 2n),
               nat_lt(gap(rank(a), rank(b)), 2n))))

# A queen steps along a rank, a file or a diagonal. The path being clear
# is a question about a position, not about geometry, so it is not asked
# here — it is one of the open claims.
def queen_line(+a: Nat, +b: Nat) -> Bool:
  Bool.and(
    Bool.and(on_board(a), on_board(b)),
    Bool.and(
      Bool.not(nat_eq(a, b)),
      Bool.or(
        Bool.or(nat_eq(file(a), file(b)), nat_eq(rank(a), rank(b))),
        nat_eq(gap(file(a), file(b)), gap(rank(a), rank(b))))))

# White pawns walk up the board, black pawns walk down. `up` says whether
# b is exactly one rank ahead of a for the side given.
def ahead(+white: Bool, +a: Nat, +b: Nat) -> Bool:
  match white:
    case True{}:
      ra = rank(a)
      nat_eq(rank(b), 1n+ra)
    case False{}:
      rb = rank(b)
      nat_eq(rank(a), 1n+rb)

# A pawn's quiet move: one rank forward, same file. There is no double
# step on a board this short, and nowhere to promote to.
def pawn_push(+white: Bool, +a: Nat, +b: Nat) -> Bool:
  Bool.and(
    Bool.and(on_board(a), on_board(b)),
    Bool.and(ahead(white, a, b), nat_eq(file(a), file(b))))

# A pawn's capture: one rank forward, one file sideways. A pawn can only
# take this way, and can never take the piece directly in front of it.
def pawn_capture(+white: Bool, +a: Nat, +b: Nat) -> Bool:
  Bool.and(
    Bool.and(on_board(a), on_board(b)),
    Bool.and(ahead(white, a, b), nat_eq(gap(file(a), file(b)), 1n)))

# every way a pawn may move, capture or not
def pawn_step(+white: Bool, +a: Nat, +b: Nat) -> Bool:
  Bool.or(pawn_push(white, a, b), pawn_capture(white, a, b))

# A knight's leap: two squares one way and one the other, which is the
# only move on the board that does not care what stands between.
def knight_step(+a: Nat, +b: Nat) -> Bool:
  +df = gap(file(a), file(b))
  +dr = gap(rank(a), rank(b))
  Bool.and(
    Bool.and(on_board(a), on_board(b)),
    Bool.or(
      Bool.and(nat_eq(df, 1n), nat_eq(dr, 2n)),
      Bool.and(nat_eq(df, 2n), nat_eq(dr, 1n))))