game.bend checks

raw source on the hub · import 0x6d15da24c6555ddee2181d043774a796/game.bend as Game

# TinyChess — the game. # # chess.bend says how a piece steps on an empty board. This file is the # rest: what stands where, what a capture is, when a king is attacked, # and when a side is mated. Everything here is computable and has no # holes, so the checker can settle a claim about a position by running # it rather than by being argued with. # # The opening position, black at the top: # # a b c d # 4 ♟ ♟ ♚ ♟ 12 13 14 15 # 3 · · · · 8 9 10 11 # 2 · · · · 4 5 6 7 # 1 ♙ ♔ ♙ ♙ 0 1 2 3 # # Both back ranks are full and the kings stand on different files, so # neither side begins in opposition and every pawn has somewhere to go. # # Sizes are the point of every loop below. There are sixteen squares and # eight pieces, so a scan is sixteen steps, an attack test is sixteen # scans, and the whole "can white win on the first move" question is a # few tens of thousands of steps. That is small enough for the checker # to simply evaluate, which is why the law about it needs no argument.

2 imports

import Base
import ./chess.bend as C

Types

type Piece source · line 31 · raw

Data

Empty
```
Piece
```
WKing
```
Piece
```
WPawn
```
Piece
```
WQueen
```
Piece
```
WKnight
```
Piece
```
BKing
```
Piece
```
BPawn
```
Piece
```
BQueen
```
Piece
```
BKnight
```
Piece
```

type Cells source · line 120 · raw

Data

the sixteen squares, a1 first. Base's List is kind-polymorphic and a plain Data field wants a plain Data list, so this one is its own.

End
```
Cells
```
Put
```
@head:Piece -> @tail:Cells -> Cells
```

type Board source · line 124 · raw

Data

Board
```
@cells:Cells -> Board
```

type Step source · line 127 · raw

Data

Step
```
@from:Nat -> @to:Nat -> Step
```

Definitions

def is_white source · line 42 · raw

@p:Piece -> Bool

def is_empty_piece source · line 63 · raw

@p:Piece -> Bool

def is_king source · line 84 · raw

@p:Piece -> Bool

def mine source · line 106 · raw

@+white:Bool -> @+p:Piece -> Bool

whether a piece belongs to the side to move

def theirs source · line 113 · raw

@+white:Bool -> @+p:Piece -> Bool

def Step.from source · line 130 · raw

@m:Step -> Nat

def Step.to source · line 135 · raw

@m:Step -> Nat

def cell source · line 140 · raw

@c:Cells -> @s:Nat -> Piece

def put_cell source · line 151 · raw

@c:Cells -> @s:Nat -> @+p:Piece -> Cells

def occupant source · line 164 · raw

@+b:Board -> @+s:Nat -> Piece

what stands on a square. Off the board reads as empty, which is what makes the scans below safe to run past the last square.

def place source · line 169 · raw

@+b:Board -> @+s:Nat -> @+p:Piece -> Board

def pick_nat source · line 175 · raw

@c:Bool -> @+a:Nat -> @+b:Nat -> Nat

choosing between two numbers, which the scans need and Bool.pick is not

def mid3 source · line 186 · raw

@+x:Nat -> @+y:Nat -> @+z:Nat -> Bool

y lies between x and z along one axis: strictly, or all three equal, which is the case where the move does not travel on that axis at all

def between source · line 196 · raw

@+a:Nat -> @+s:Nat -> @+b:Nat -> Bool

s is strictly inside the line from a to b. On a board four wide there are at most two such squares, so testing all sixteen is cheaper than working out a direction and stepping along it.

def clear_go source · line 202 · raw

@+bd:Board -> @+a:Nat -> @+b:Nat -> @n:Nat -> Bool

def clear source · line 212 · raw

@+bd:Board -> @+a:Nat -> @+b:Nat -> Bool

nothing stands between a and b

def attacks_as source · line 222 · raw

@p:Piece -> @+bd:Board -> @+from:Nat -> @+to:Nat -> Bool

whether the piece standing on from attacks to. A pawn attacks only where it could take, never where it could push, which is the rule that makes pawn structure mean anything. the checker will not match on a computed value, so the piece arrives as a parameter and the lookup happens in the caller

def attacks source · line 243 · raw

@+bd:Board -> @+from:Nat -> @+to:Nat -> Bool

def attacked_go source · line 246 · raw

@+bd:Board -> @+w:Bool -> @+s:Nat -> @n:Nat -> Bool

def attacked source · line 256 · raw

@+bd:Board -> @+w:Bool -> @+s:Nat -> Bool

whether the given side attacks a square

def king_go source · line 259 · raw

@+bd:Board -> @+w:Bool -> @n:Nat -> Nat

def king_square source · line 270 · raw

@+bd:Board -> @+w:Bool -> Nat

where the given side's king stands. A board with no king answers 16, which is off the board and therefore attacked by nothing.

def in_check source · line 273 · raw

@+bd:Board -> @+w:Bool -> Bool

def play source · line 278 · raw

@+bd:Board -> @+m:Step -> Board

def shape_ok source · line 287 · raw

@moving:Piece -> @+target:Piece -> @+bd:Board -> @+w:Bool -> @+f:Nat -> @+t:Nat -> Bool

the geometry, plus what the position allows: your own piece is not a target, a queen needs a clear line, a pawn pushes only onto an empty square and takes only onto an occupied one.

def pseudo_legal source · line 312 · raw

@+bd:Board -> @+w:Bool -> @+m:Step -> Bool

def legal source · line 322 · raw

@+bd:Board -> @+w:Bool -> @+m:Step -> Bool

and the rule that separates a move from a step: you may not leave your own king attacked

def any_to source · line 327 · raw

@+bd:Board -> @+w:Bool -> @+f:Nat -> @n:Nat -> Bool

def any_from source · line 335 · raw

@+bd:Board -> @+w:Bool -> @n:Nat -> Bool

def has_legal_move source · line 343 · raw

@+bd:Board -> @+w:Bool -> Bool

def is_checkmate source · line 347 · raw

@+bd:Board -> @+w:Bool -> Bool

in check, and nothing to do about it

def is_stalemate source · line 350 · raw

@+bd:Board -> @+w:Bool -> Bool

def no_move source · line 357 · raw

Step

"there isn't one". Square 16 is off the board, so no real move can collide with it, and a failed law prints this against the move it found.

def found source · line 360 · raw

@+m:Step -> Bool

def pick_move source · line 363 · raw

@c:Bool -> @+a:Step -> @+b:Step -> Step

def wins_to source · line 370 · raw

@+bd:Board -> @+f:Nat -> @n:Nat -> Step

def wins_from source · line 380 · raw

@+bd:Board -> @n:Nat -> Step

def winning_first_move source · line 392 · raw

@+bd:Board -> Step

The move that mates, or no_move() when there is none. Returning the move rather than a Bool is what lets a broken law name its own counterexample: the checker prints what it observed, so the error carries Step{from, to}.

def white_wins_in_one source · line 396 · raw

@+bd:Board -> Bool

whether white has a first move that mates black on the spot

def row source · line 401 · raw

@a:Piece -> @b:Piece -> @c:Piece -> @d:Piece -> @rest:Cells -> Cells

def empty_row source · line 404 · raw

@rest:Cells -> Cells

def initial source · line 409 · raw

Board

rank 1 first: white pawn, white king, white pawn, white pawn, then two empty ranks, then black's pawn, pawn, king, pawn

def initial_with_queen source · line 416 · raw

Board

the same, with the pawn beside white's king traded for a queen

def initial_with_queens source · line 424 · raw

Board

a queen each, on the square beside each king, so the position stays symmetric under turning the board around

def initial_with_knight source · line 431 · raw

Board

a knight for white alone, on the square the queen took

def initial_with_knights source · line 438 · raw

Board

and the same two squares, knights instead