|Computational class||Category:Turing complete|
|Major implementations||Implementation in Electron|
This programming language is intended to be used for specifying and implementing puzzle games. The language is not finished yet, but most of the features are already implemented. The goal is to be able to specify a puzzle game in a short, concise way.
A program written in CSP Spec defines a puzzle game. It includes: shape of the board, rules, controls, options, parameters, user input, graphical rendering of the game, level generator and level solver. Therefore, CSP Spec can be considered a framework for defining puzzle games.
Currently, there is only one game implemented in CSP Spec: Sudoku.
params | dim | pair pnat def n | mulv dim clues grid | grid_squares n n | fin n def f \(v p) div p dim [rows, cols, group f].all \f (f grid).all neqv grid.render_group f \(v p g) [bg white, text v.inc <g black blue>] grid.input_int [1, n] dec
The code above is the entire specification and implementation of the Sudoku game. Let's analyze it line by line.
The first line
params | dim | pair pnat defines the parameters for the game. Function
params takes parameters from the level generator form and passes them to the program. Here we specify parameter
dim, which represents the dimensions of the board (grid). The pipe character
| is like the dollar operator in Haskell. The
pair pnat defined the type of the parameter
dim. The type
pair pnat represents a pair of two positive natural numbers. The
dim represents width and height of sections of the grid (for the regular
dim has value
def n | mulv dim defines constant
n which is equal to the product of elements of
mulv is like
product in Haskell. The number
n represents the size (width and height) of the sudoku puzzle (for
clues grid | grid_squares n n | fin n defines clues (numbers on the grid that are "given" to the player). It is defined as a grid of dimensions . Each grid cell (tile) is of type
fin n, which represents the type of natural numbers smaller than
n. It means that the numbers in the grid are internally represented as numbers from
n-1, instead of
def f \(v p) div p dim defines function
f which takes two arguments
p. Then we return the result of dividing
dim (division of natural numbers rounds down). Dividing two pairs represents dividing corresponding elements.
[rows, cols, group f].all \f (f grid).all neqv specifies the rules of the game. It says that in each row, collumn and section all numbers are different. Function
group partitions the grid based on the given partition function.
grid.render_group f \(v p g) [bg white, text v.inc <g black blue>] - this specifies how the game is rendered (displayed on screen). The
<> brackets represent ternary if-then-else statement. Basically, we render the grid by highlighting grid regions based on partition function
f. We render each tile by taking three variables
g, and then we pass two monadic actions to the rendering monad. Variable
v represents the value of the current tile (in the
Maybe monad, so all actions are implicitly lifted to
p represents the coordinates of the tile. Variable
g is boolean which is true iff the value of the given tile has been "given" to the user at the start of the game. The first action we execute is
bg white, which paints the background of the tile in
white. The second action is
text v.inc <g black blue>, which renders the text representing the value (number) of the current tile. The colors
blue are global constants (there is also a way to specify color by RGB values).
grid.input_int [1, n] dec specifies user input. It says that the user can input a number from interval
[1, n] to any tile of the grid as long as the number is not "given". The post-processing function
dec decrements the number to adapt it to the internal representation, which is in interval
[0, n - 1].
The interpreter uses SAT solver to automatically generate level generator and level solver for the game, based on the game specification. The user may specify SAT solver to be used. The SAT solver must support input in DIMACS format. The interpreter has been tested on CaDiCaL, Cryptominisat and Kissat solvers.
The level generator starts with the empty grid. Generator represents all tiles as placeholders for lists of bits. Generator then picks a random bit and assigns it a random value (0 or 1). Then generator asks the SAT solver whether there exists a level that has a bit with that value in that position. If the SAT solver says "yes", then the generator picks the next bit and proceeds. If the answer is "no", the generator flips the bit and proceeds. This is repeated until all bits have values.
Next, the generator starts removing clues in groups, as long as the level has a unique solution. Generator picks a random tile and removes the clue from that tile. Then asks the SAT solver whether there exists a unique solution. If the answer is "yes", then it proceeds to next random tile. If the answer is "no", the generator restores the clue and moves on. It keeps doing so until it checks all clues.
The resulting generated level has a unique solution according to the rules of the game. Moreover, removing any given clue will introduce another solution. So, in some sense, it contains the minimal number of clues (although it's not the global minimum).