Sudoku
From The Twelf Project
In the Sudoku puzzle, a 9x9 board must be filled with the numbers 
such that no row, column, or box contains the same digit twice.
| This article or section needs to be completed. |
% Sudoku solver, brute force
cell : type.
1 : cell.
2 : cell.
3 : cell.
4 : cell.
5 : cell.
6 : cell.
7 : cell.
8 : cell.
9 : cell.
nat : type.
z : nat.
s : nat -> nat. %prefix 5 s.
nine = s s s s s s s s s z.
cells : nat -> type.
// : cell -> cells N -> cells (s N).
%infix right 5 //.
nil : cells z.
cellss : nat -> type.
/// : cells nine -> cellss N -> cellss (s N).
%infix right 4 ///.
nill : cellss z.
remove : cells (s N) -> cell -> cells N -> type.
%mode remove +L +C -L'.
rem-hit : remove (X // C) X C.
% okay that we can also skip this one
rem-miss : remove (X // C) Y (X // C')
<- remove C Y C'.
%worlds () (remove _ _ _).
%terminates D (remove D _ _).
nodups : cells X -> cells Y -> type.
%mode nodups +OK +L.
nd-nil : nodups _ nil.
nd-hit : nodups OK (X // C)
<- remove OK X OK'
<- nodups OK' C.
%worlds () (nodups _ _).
%terminates D (nodups _ D).
% valid if there are no duplicates
allcells = 1 // 2 // 3 //
4 // 5 // 6 //
7 // 8 // 9 // nil.
unitok : cells nine -> type.
uo : unitok C
<- nodups allcells C.
% the nine rows
%abbrev board = cellss nine.
% extract three boxes from three rows
boxes : cells nine -> cells nine -> cells nine ->
cells nine -> cells nine -> cells nine -> type.
%mode boxes +A +B +C -A' -B' -C'.
b : boxes
(A1 // B1 // C1 // D1 // E1 // F1 // G1 // H1 // I1 // nil)
(A2 // B2 // C2 // D2 // E2 // F2 // G2 // H2 // I2 // nil)
(A3 // B3 // C3 // D3 // E3 // F3 // G3 // H3 // I3 // nil)
%
(A1 // B1 // C1 //
A2 // B2 // C2 //
A3 // B3 // C3 // nil)
%
(D1 // E1 // F1 //
D2 // E2 // F2 //
D3 // E3 // F3 // nil)
%
(G1 // H1 // I1 //
G2 // H2 // I2 //
G3 // H3 // I3 // nil).
%worlds () (boxes _ _ _ _ _ _).
%total {} (boxes _ _ _ _ _ _).
% transpose a whole board
transpose : board -> board -> type.
%mode transpose +B -B'.
tr : transpose ((A1 // B1 // C1 // D1 // E1 // F1 // G1 // H1 // I1 // nil) ///
(A2 // B2 // C2 // D2 // E2 // F2 // G2 // H2 // I2 // nil) ///
(A3 // B3 // C3 // D3 // E3 // F3 // G3 // H3 // I3 // nil) ///
(A4 // B4 // C4 // D4 // E4 // F4 // G4 // H4 // I4 // nil) ///
(A5 // B5 // C5 // D5 // E5 // F5 // G5 // H5 // I5 // nil) ///
(A6 // B6 // C6 // D6 // E6 // F6 // G6 // H6 // I6 // nil) ///
(A7 // B7 // C7 // D7 // E7 // F7 // G7 // H7 // I7 // nil) ///
(A8 // B8 // C8 // D8 // E8 // F8 // G8 // H8 // I8 // nil) ///
(A9 // B9 // C9 // D9 // E9 // F9 // G9 // H9 // I9 // nil) /// nill)
%
((A1 // A2 // A3 // A4 // A5 // A6 // A7 // A8 // A9 // nil) ///
(B1 // B2 // B3 // B4 // B5 // B6 // B7 // B8 // B9 // nil) ///
(C1 // C2 // C3 // C4 // C5 // C6 // C7 // C8 // C9 // nil) ///
(D1 // D2 // D3 // D4 // D5 // D6 // D7 // D8 // D9 // nil) ///
(E1 // E2 // E3 // E4 // E5 // E6 // E7 // E8 // E9 // nil) ///
(F1 // F2 // F3 // F4 // F5 // F6 // F7 // F8 // F9 // nil) ///
(G1 // G2 // G3 // G4 // G5 // G6 // G7 // G8 // G9 // nil) ///
(H1 // H2 // H3 // H4 // H5 // H6 // H7 // H8 // H9 // nil) ///
(I1 // I2 // I3 // I4 // I5 // I6 // I7 // I8 // I9 // nil) /// nill).
%worlds () (transpose _ _).
%total {} (transpose C _).
boardok : board -> type.
bo : boardok
(A /// B /// C /// D /// E /// F /// G /// H /// I /// nill)
% rows
<- unitok A <- unitok B <- unitok C
<- unitok D <- unitok E <- unitok F
<- unitok G <- unitok H <- unitok I
% boxes
<- boxes A B C Ab Bb Cb
<- unitok Ab <- unitok Bb <- unitok Cb
<- boxes D E F Db Eb Fb
<- unitok Da <- unitok Ea <- unitok Fa
<- boxes G H I Gb Hb Ib
<- unitok Gb <- unitok Hb <- unitok Ib
% cols
<- transpose (A /// B /// C /// D /// E /// F /// G /// H /// I /// nill)
(At /// Bt /// Ct /// Dt /// Et /// Ft /// Gt /// Ht /// It /// nill)
<- unitok At <- unitok Bt <- unitok Ct
<- unitok Dt <- unitok Et <- unitok Ft
<- unitok Gt <- unitok Ht <- unitok It.
%solve _ : boardok
(
(8 // 2 // 6 // 7 // 1 // 4 // 9 // 5 // 3 // nil) ///
(3 // 4 // 5 // 8 // 6 // 9 // 2 // 1 // 7 // nil) ///
(9 // 7 // 1 // 2 // 5 // 3 // 4 // 8 // 6 // nil) ///
(1 // 6 // 3 // 9 // 2 // 5 // 7 // 4 // 8 // nil) ///
(5 // 9 // 4 // 6 // 7 // 8 // 1 // 3 // 2 // nil) ///
(2 // 8 // 7 // 3 // 4 // 1 // 5 // 6 // 9 // nil) ///
(7 // 5 // 9 // 4 // 3 // 6 // 8 // 2 // 1 // nil) ///
(4 // 3 // 2 // 1 // 8 // 7 // 6 // 9 // 5 // nil) ///
(6 // 1 // 8 // 5 // 9 // 2 // 3 // 7 // 4 // nil) /// nill).
%solve _ : boardok
(
(8 // 2 // 6 // 7 // 1 // 4 // 9 // 5 // 3 // nil) ///
(3 // 4 // 5 // 8 // 6 // 9 // 2 // 1 // 7 // nil) ///
(9 // 7 // 1 // 2 // 5 // 3 // 4 // 8 // 6 // nil) ///
(1 // 6 // 3 // _ // 2 // 5 // 7 // 4 // 8 // nil) ///
(5 // 9 // 4 // _ // 7 // 8 // 1 // 3 // 2 // nil) ///
(2 // 8 // 7 // _ // _ // 1 // 5 // 6 // 9 // nil) ///
(7 // 5 // 9 // 4 // 3 // 6 // 8 // 2 // 1 // nil) ///
(4 // 3 // 2 // 1 // 8 // 7 // 6 // 9 // 5 // nil) ///
(6 // 1 // 8 // 5 // 9 // 2 // 3 // 7 // 4 // nil) /// nill).
All code from this tutorial. Twelf's output from this tutorial.
Read more Twelf case studies and other Twelf documentation.
