chess.bend source
chess.bend on the hub · documented module
## TinyChess — the board and the way the pieces move.#### Four files by four ranks, kings and pawns and a queen. 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 aredef 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-filedef 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'sdef 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 sixteendef 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 notdef 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))))