CSP Spec
| Paradigm(s) | Declarative |
|---|---|
| Designed by | User:Hakerh400 |
| Appeared in | 2021 |
| Computational class | Category:Turing complete |
| Major implementations | Implementation in Electron |
| File extension(s) | .txt |
CSP Spec is a work-in-progress declarative esoteric programming language invented by User:Hakerh400 in 2021. CSP stands for Constraint satisfaction problem and Spec stands for "Specification".
Overview
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.
Examples
Currently, there is only one game implemented in CSP Spec: Sudoku.
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 9x9 sudoku, dim has value (3, 3)).
Next, def n | mulv dim defines constant n which is equal to the product of elements of dim. Function mulv is like product in Haskell. The number n represents the size (width and height) of the sudoku puzzle (for 9x9 sudoku, n is 9).
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 0 to n-1, instead of 1 to n.
def f \(v p) div p dim defines function f which takes two arguments v and p. Then we return the result of dividing p with dim (division of natural numbers rounds down). Dividing two pairs represents dividing corresponding elements.
The line [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 v, p and 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 Maybe). Variable 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 white, black and blue are global constants (there is also a way to specify color by RGB values).
Finally, 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].
Level generator
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).