[racket] proof assistants, DrRacket and Bootstrap
Matthias's last post makes it clear that I've been misunderstanding Scheme meta-interpreters for years time, and I have three followup questions.
A Racket meta-interpreter emulates Racket, but it can not handle Racket code that was previously evaluated, unless one (as in Matthias's example) manually defines an environment with all the previous variable binding. That wouldn't be convenient for me, as in HOL Light, there are tons of theorems that have already been proved. So I just misunderstood the meaning of a Racket meta-interpreter.
What I clearly want is (as Prabhakar Ragde posted) is some kind of macros that turn my dialect into standard code, and of course Scheme is famous for its macros. Does anyone know if the OCaml parser Camlp is similarly useful for macro purposes?
Can we save the interactions window as a pdf? Or something like that?
I just posted on my web page the Racket interactions file of a solution to a Sudoku puzzle
http://www.math.northwestern.edu/~richter/10-31-2014.rkt
but this is only visible if one saves the file and runs it in Dr Racket. I think it looks very nice, and it's Racket code my son Ben wrote 4 years ago, plus some manual interventions of mine.
BTW I want my 7th grade student to write a Racket Sudoku solver. He thinks Dr Racket looks really cool. I wonder if anyone has a suggestion about better coding, maybe more accessible Bootstrap-type code. I'm including the program below.
--
Best,
Bill
#lang slideshow
;;;;;;;;;;;;;; basic Racket functions
;; List-ref: (list of X) integer[>0] -> X
;; to get the k-th element of the list L
(define (List-ref L k)
(list-ref L (sub1 k)))
;; Build-list: integer function -> list
;; to make the list {(f 1) (f 2)...(f n)} of length n using f
(define (Build-list n f)
(build-list n (lambda (i) (f (add1 i)))))
;; Build-string: integer function -> string
;; to make the string "(f 1) (f 2)...(f n)" of length n using f
(define (Build-string n f)
(build-string n (lambda (i) (f (add1 i)))))
;; NoRepetitions?: list -> boolean
;; to test if there are no repetitions in L
(define (NoRepetitions? L)
(or (empty? L)
(and (not (member (first L) (rest L)))
(NoRepetitions? (rest L)))))
;; map2: function (list of (list of X)) -> (list of (list of Y))
;; to make a list of lists of (f x), where f: X -> Y
(define (map2 f LoL)
(map (lambda (z) (map f z)) LoL))
;; ormap2: function (list of A) (list of B) -> C | false
;; to get first true (g x y) for x in X and y in Y or false otherwise, where
;; g: A B -> C
(define (ormap2 g X Y)
(ormap (lambda (y)
(ormap (lambda (x) (g x y)) X)) Y))
;; digit->char: digit -> character
;; to turn a digit i into #\i
(define (digit->char i)
(integer->char (+ 48 i)))
;; Intersection: (list of X) (list of X) -> (list of X)
;; to construct the list of elements that belong to both A and B
(define (Intersection A B)
(filter (lambda (a) (member a B)) A))
;; Intersect?: (list of X) (list of X) -> boolean
;; to test if A and B intersect
(define (Intersect? A B)
(not (empty? (Intersection A B))))
;; Subset?: (list of X) (list of X) -> boolean
;; to test if A is a subset of B
(define (Subset? A B)
(andmap (lambda (a) (member a B)) A))
;; Set-equal?: (list of X) (list of X) -> boolean
;; to test if the elements in A are equal to the elements in B
(define (Set-equal? A B)
(and (Subset? A B)
(Subset? B A)))
;; Choose2: (list of Y) -> (list of (list of Y)[length 2])
;; to build the list of length k choose 2, where k = (length X)
(define (Choose2 X)
(if (< (length X) 2)
empty
(append
(map (lambda (Z) (list (first X) Z)) (rest X))
(Choose2 (rest X)))))
;; Choose3: (list of Y) -> (list of (list of Y)[length 3])
;; to build the list of lists of length 3 from list X
;; The length of (Choose3 X) is (length X) choose 3.
(define (Choose3 X)
(if (< (length X) 3)
empty
(let ([x1 (first X)]
[X1 (rest X)])
(append (map (λ (xy) (cons x1 xy))
(Choose2 X1))
(Choose3 X1)))))
;; Remove-Multiples: (list of Y) -> (list of Y)
;; to remove all multiples from a list X
(define (Remove-Multiples X)
(if (> 2 (length X))
X
(if (member (first X) (rest X))
(Remove-Multiples (rest X))
(cons (first X) (Remove-Multiples (rest X))))))
;; Union: (list of X) ... (list of X) -> (list of X)
;; to take the union of lists of X (stored in loloX)
(define Union (λ loloX (Remove-Multiples (apply append loloX))))
;;;;;;;;;;;;;; basic Sudoku functions and definitions
;; Digits = 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9
(define Digits '(1 2 3 4 5 6 7 8 9))
(define (Digit? X)
(member X Digits))
;; NL = Digit | (list of Digits)[not empty], meaning a number or a list
(define (NL? X)
(or (Digit? X)
(and (list? X) (not (empty? X)) (andmap Digit? X))))
;; Sudoku = (list of (list of NL)[length 9])[length 9]
(define (Sudoku? X)
(define (ListLength9? x)
(and (list? x) (= (length x) 9)))
(and (ListLength9? X) (andmap ListLength9? X) (andmap NL? (apply append X))))
;; loloCells is a list of lists of cells, where each cell is a list of three
;; digits: a row, a column and a box. I think of these cells the Andrew Stuart
;; way http://www.sudokuwiki.org: {{A1 ... A9} ... (J1 ... J9}}
(define loloCells
'(((1 1 1) (1 2 1) (1 3 1) (1 4 2) (1 5 2) (1 6 2) (1 7 3) (1 8 3) (1 9 3))
((2 1 1) (2 2 1) (2 3 1) (2 4 2) (2 5 2) (2 6 2) (2 7 3) (2 8 3) (2 9 3))
((3 1 1) (3 2 1) (3 3 1) (3 4 2) (3 5 2) (3 6 2) (3 7 3) (3 8 3) (3 9 3))
((4 1 4) (4 2 4) (4 3 4) (4 4 5) (4 5 5) (4 6 5) (4 7 6) (4 8 6) (4 9 6))
((5 1 4) (5 2 4) (5 3 4) (5 4 5) (5 5 5) (5 6 5) (5 7 6) (5 8 6) (5 9 6))
((6 1 4) (6 2 4) (6 3 4) (6 4 5) (6 5 5) (6 6 5) (6 7 6) (6 8 6) (6 9 6))
((7 1 7) (7 2 7) (7 3 7) (7 4 8) (7 5 8) (7 6 8) (7 7 9) (7 8 9) (7 9 9))
((8 1 7) (8 2 7) (8 3 7) (8 4 8) (8 5 8) (8 6 8) (8 7 9) (8 8 9) (8 9 9))
((9 1 7) (9 2 7) (9 3 7) (9 4 8) (9 5 8) (9 6 8) (9 7 9) (9 8 9) (9 9 9))))
;; loCells is the list of 81 cells.
(define loCells
(apply append loloCells))
;; Cell = the 81 cells
(define (Cell? X)
(member X loCells))
;; Cell-row: Cell -> Digit
(define (Cell-row P) (first P))
;; Cell-col: Cell -> Digit
(define (Cell-col P) (second P))
;; Cell-box: Cell -> Digit
(define (Cell-box P) (third P))
;; empty-cell?: Cell Sudoku -> boolean
;; to test if cell P of sudoku S is empty
(define (empty-cell? P S)
(not (member (Val P S) Digits)))
;; Val: Cell Sudoku -> NL
;; to get the value of cell P of sudoku S
(define (Val P S)
(List-ref (List-ref S (Cell-row P)) (Cell-col P)))
;; Cell-see?: Cell Cell -> boolean
;; to test if P and Q see each other, meaning that P != Q and Q is in the row
;; column or box P is in
(define (Cell-see? P Q)
(and (not (equal? P Q))
(or (= (Cell-row P) (Cell-row Q))
(= (Cell-col P) (Cell-col Q))
(= (Cell-box P) (Cell-box Q)))))
;; Cell-display: Cell -> void
;; to display cell P the Andrew Stuart way
(define (Cell-display P)
(let ([i (Cell-row P)])
(display (cond [(= i 1) "A"]
[(= i 2) "B"]
[(= i 3) "C"]
[(= i 4) "D"]
[(= i 5) "E"]
[(= i 6) "F"]
[(= i 7) "G"]
[(= i 8) "H"]
[(= i 9) "J"]))
(display (Cell-col P))))
;; loCell-display: (list of Cell) -> void
;; to display a list of cells loCell
(define (loCell-display loCell)
(display "{")
(Cell-display (first loCell))
(map (lambda (cell)
(display " ") (Cell-display cell))
(rest loCell))
(display "}"))
;; Display-unit-text: Unit -> void
;; to display text of a unit u such as "box 5"
(define (Display-unit u)
(cond [(member u Rows)
(display "row ") (display (Cell-row (first u)))]
[(member u Cols)
(display "col ") (display (Cell-col (first u)))]
[(member u Boxes)
(display "box ") (display (Cell-box (first u)))]))
;; Build-sudoku: function -> Sudoku
;; to make a sudoku out of a function f: Cell -> NL
;; {{(f A1) ... (f A9)} ... {(f J1) ... (f J9)}}
(define (Build-sudoku f)
(map2 f loloCells))
;; sudoku->picture: Sudoku -> pict
;; to turn a sudoku into a pict which has a table of big and little numbers
;; aligned and surrounded by boxes
(define (sudoku->picture S)
(define (little-num-align LoD)
(table 3
(map (lambda (i)
(if (member i LoD)
(text (make-string 1 (digit->char i)) "Helvetica" 14 0)
(text (make-string 1 #\space) "Helvetica" 14 0))) Digits)
(make-list 9 cc-superimpose)
(make-list 9 cc-superimpose)
(make-list 9 0) (make-list 9 0)))
(define (NL->PictText nl)
(cc-superimpose
(rectangle 60 60)
(if (list? nl)
(little-num-align nl)
(text (string-append " " (make-string 1 (digit->char nl)) " ")
"Helvetica" 32 0))))
(let* ([table-with-pict-boxes
(table 9 (map NL->PictText (apply append S))
(make-list 9 cc-superimpose)
(make-list 9 cc-superimpose)
(make-list 9 0) (make-list 9 0))]
[pw (pict-width table-with-pict-boxes)]
[ph (pict-height table-with-pict-boxes)])
(cc-superimpose
table-with-pict-boxes
(linewidth 7 (lt-superimpose
(rectangle pw ph)
(rectangle (/ pw 3) ph) (rectangle (* 2 (/ pw 3)) ph)
(rectangle pw (/ ph 3)) (rectangle pw (* 2 (/ ph 3))))))))
;; Rows is the list of 9 rows.
(define Rows
loloCells)
;; Cols is the list of 9 columns.
(define Cols
(let ([Col
(lambda (i)
(map (lambda (row) (List-ref row i)) loloCells))])
(Build-list 9 Col)))
;; Boxes is the list of 9 boxes.
(define Boxes
(let ([Box
(lambda (i)
(filter (lambda (Q) (= (Cell-box Q) i)) loCells))])
(Build-list 9 Box)))
;; Units is the list of 27 units.
(define Units
(append Boxes Rows Cols))
;; Row-List: Cell -> Row
;; to get the row with P in it
(define (Row-List P)
(List-ref Rows (Cell-row P)))
;; Col-List: Cell -> Column
;; to get the column with P in it
(define (Col-List P)
(List-ref Cols (Cell-col P)))
;; Box-List: Cell -> Box
;; to get the box with P in it
(define (Box-List P)
(List-ref Boxes (Cell-box P)))
;; Big-numbers-in-box: Cell Sudoku -> (list of Digits)
;; to get the list of big numbers in the box of P
(define (Big-numbers-in-box P S)
(map (lambda (Q) (Val Q S))
(filter (lambda (Q) (not (empty-cell? Q S)))
(Box-List P))))
;; Big-numbers-in-row: Cell Sudoku -> (list of Digits)
;; to get the list of big numbers in the row of P
(define (Big-numbers-in-row P S)
(map (lambda (Q) (Val Q S))
(filter (lambda (Q) (not (empty-cell? Q S)))
(Row-List P))))
;; Big-numbers-in-col: Cell Sudoku -> (list of Digits)
;; to get the list of big numbers in the col of P
(define (Big-numbers-in-col P S)
(map (lambda (Q) (Val Q S))
(filter (lambda (Q) (not (empty-cell? Q S)))
(Col-List P))))
;;;;;;;;;;;;;; Sudoku techniques
;; Valid?: Sudoku -> boolean
;; to test whether a sudoku S has one of these two errors: a repetition of a big
;; number in the same unit, or an empty number list
(define (Valid? S)
(and (Sudoku? S)
(andmap (lambda (u)
(NoRepetitions?
(map (lambda (P) (Val P S))
(filter (lambda (P) (not (empty-cell? P S)))
u))))
Units)))
;; fix-fresh-sudoku: Sudoku -> Sudoku
;; to replace each 0 with Digits on a fresh Sudoku
(define (fix-fresh-sudoku S)
(Build-sudoku
(lambda (P)
(if (empty-cell? P S)
Digits
(Val P S)))))
;; update-sudoku: Sudoku -> Sudoku
;; to delete little numbers that are in the box, row and column.
(define (update-sudoku S)
(define (f P)
(if (empty-cell? P S)
(remove* (append (Big-numbers-in-box P S)
(Big-numbers-in-row P S)
(Big-numbers-in-col P S))
(Val P S))
(Val P S)))
(Build-sudoku f))
;; Single?: Cell Sudoku -> boolean
;; to test if cell P of sudoku S is a Single
(define (Single? P S)
(and (empty-cell? P S)
(= 1 (length (Val P S)))))
;; FindSingle: Sudoku -> Cell | false
;; to get the first Single or false when there are no Singles
(define (FindSingle S)
(ormap (lambda (P) (and (Single? P S) P)) loCells))
;; Single->big-num: Sudoku Single -> Sudoku
(define (Single->big-num S FS)
(display "Single ") (display (first (Val FS S)))
(display " in cell ") (Cell-display FS) (newline) (newline)
(Build-sudoku (lambda (P)
(if (equal? P FS)
(first (Val P S))
(Val P S)))))
;; (i-cells i u S) will be the list of i-cells in u, which is the list of empty
;; cells in u that have i in them.
(define (i-cells i u S)
(filter (lambda (P) (and (empty-cell? P S)
(member i (Val P S))))
u))
;; HiddenSingle = (list Digit Cell Unit)
;; A Hidden Single {i P U} means the cell P is the only i-cell in unit u.
;; FindHiddenSingle: Sudoku -> HiddenSingle | false
;; to find the first Hidden Single or false when there are no Hidden Singles
(define (FindHiddenSingle S)
(ormap2
(lambda (i u)
(let ([X (i-cells i u S)])
(and (= 1 (length X))
(list i (first X) u))))
Digits Units))
;; HiddenSingle->big-num: Sudoku HiddenSingle -> Sudoku
;; to construct the sudoku with Hidden Single HS of sudoku S turned to a big
;; number, and to display a statement such as
;; "Hidden Single 5 in cell B5 of box 2"
(define (HiddenSingle->big-num S HS)
(let ([i (first HS)]
[P (second HS)]
[u (third HS)])
(display "Hidden Single ") (display i) (display " in cell ")
(Cell-display P) (display " of ") (Display-unit u) (newline) (newline))
(Build-sudoku (lambda (P)
(if (equal? P (second HS))
(first HS)
(Val P S)))))
;; PossiblePP/LBR is the list of {u v}, where u and v are units to attempt a
;; Digit/Unit-Unit Pattern. Andrew Stuart uses PP (Pointing Pair) and LBR
;; (Line Block Reduction) for Digit/Unit-Unit Patterns.
(define PossiblePP/LBR
(let* ([PossibleLBR (filter (lambda (Z)
(let ([u (first Z)]
[v (second Z)])
(= 3 (length (Intersection u v)))))
(Choose2 Units))]
[PossiblePP (map reverse PossibleLBR)])
(append PossiblePP PossibleLBR)))
;; findD/U-U: Sudoku -> (list Digit (list of Cell) (list of Cell)) | false
;; to find a Digit/Unit-Unit Pattern in sudoku S and the list of cells that have
;; little numbers to be removed by the Digit/Unit-Unit Pattern, or false when
;; there is no useful Digit/Unit-Unit Pattern
(define (findD/U-U S)
(define (D/U-Ufinder Z)
(let ([u (first Z)]
[v (second Z)])
(ormap (lambda (i)
(let* ([D/U-U (i-cells i v S)]
[X (remove* D/U-U (i-cells i u S))])
(and (not (empty? D/U-U))
(not (empty? X))
(Subset? D/U-U u)
(list i
D/U-U
X))))
Digits)))
(ormap D/U-Ufinder PossiblePP/LBR))
;; D/U-U->remove-little-num: Sudoku D/U-U -> Sudoku
;; to build the sudoku with the little numbers in the way of the Digit/Unit-Unit
;; Pattern of sudoku S removed, and to print out a statement such as
;; "Digit/Unit-Unit Pattern in cells {A1 B1} removes 7 from cells {D1 E1}"
(define (D/U-U->remove-little-num S FD/U-U)
(let ([i (first FD/U-U)]
[D/U-U (second FD/U-U)]
[remove-cells (third FD/U-U)])
(display "Digit/Unit-Unit Pattern in cells ") (loCell-display D/U-U)
(display " removes ") (display i)
(display " from cells ") (loCell-display remove-cells)
(newline)(newline)
(Build-sudoku (lambda (R)
(if (member R (third FD/U-U))
(remove i (Val R S))
(Val R S))))))
;; findVP: Sudoku -> (list (list Cell Cell) (list of Cell)) | false
;; to get a Visible Pair {P Q} in sudoku S and the list of cells that see P and
;; Q with little numbers to be removed by the Visible Pair, or false when there
;; is no useful Visible Pair
(define (findVP S)
(define (VP-in-unit u)
(let ([length-2-empty-cells (filter (lambda (P)
(and (empty-cell? P S)
(= (length (Val P S)) 2)))
u)])
(and (not (empty? length-2-empty-cells))
(ormap (lambda (PQ)
(let ([P (first PQ)]
[Q (second PQ)])
(and (equal? (Val P S)
(Val Q S))
(Intersect?
(Val P S)
(apply append
(map (lambda (T) (Val T S))
(filter
(lambda (P) (empty-cell? P S))
(remove* PQ u)))))
(list PQ
(filter (lambda (X)
(and (empty-cell? X S)
(Cell-see? X P)
(Cell-see? X Q)
(Intersect? (Val P S)
(Val X S))))
loCells)))))
(Choose2 length-2-empty-cells)))))
(ormap VP-in-unit Units))
;; VP->remove-little-num: Sudoku VP -> Sudoku
;; to build the sudoku with the little numbers in the way of the Visible Pair VP
;; of sudoku S removed, and to print out a statement such as
;; "Visible Pair in cells {C2 C3} removes 1 and 5 from cells {A2 C4 C6}"
(define (VP->remove-little-num S FVP)
(let ([P (first (first FVP))]
[Q (second (first FVP))])
(display "Visible Pair in cells {") (Cell-display P) (display " ")
(Cell-display Q) (display "} removes ") (display (first (Val P S)))
(display " and ") (display (second (Val P S)))
(display " from cells ")
(loCell-display (second FVP))
(newline)(newline)
(Build-sudoku (lambda (R)
(if (member R (second FVP))
(remove* (Val P S) (Val R S))
(Val R S))))))
;; HiddenPair = (list (list Digit Digit) (list Cell Cell) Unit)
;; A Hidden Pair {{i j} {P Q} u} means the cells P and Q are the only i-cells in
;; unit u, and P and Q are the only j-cells in u.
;; FindHiddenPair: Sudoku -> HiddenPair | false
;; to find the first Hidden Pair, or false when there are no useful Hidden Pairs
(define (FindHiddenPair S)
(ormap2
(lambda (ij u)
(let* ([i (first ij)]
[j (second ij)]
[A (i-cells i u S)]
[B (i-cells j u S)])
(and (= 2 (length A))
(Set-equal? A B)
(let ([P (first A)]
[Q (second A)])
(and (or (not (empty? (remove* ij (Val P S))))
(not (empty? (remove* ij (Val Q S)))))
(list ij A u))))))
(Choose2 Digits) Units))
;; HiddenPair->remove-little-num: Sudoku HiddenSingle -> Sudoku
;; to remove all the little numbers in P and Q that are not i or j, where
;; FHP = {{i j} {P Q} u}, and to print out a statement such as
;; "Hidden Pair (7 8) in cells {B8 C8} of box 3"
(define (HiddenPair->remove-little-num S FHP)
(let* ([ij (first FHP)]
[PQ (second FHP)]
[u (third FHP)]
[i (first ij)]
[j (second ij)]
[P (first PQ)]
[Q (second PQ)])
(display "Hidden Pair ") (display ij) (display " in cells ")
(loCell-display PQ) (display " of ") (Display-unit u) (newline) (newline)
(Build-sudoku (lambda (X)
(if (member X PQ)
ij
(Val X S))))))
;; findVT: Sudoku -> (list (list of Cell) (list of Digit) (list of Cell)) | #f
;; to find a Visible Triple {P Q R} in sudoku S, the list of digits in the
;; Visible Triple, and the list of cells that see P, Q and R with little numbers
;; to be removed by the Visible Triple, or false otherwise
(define (findVT S)
(define (VT-in-unit u)
(let ([Z (Choose3 (filter (lambda (P)
(and (empty-cell? P S)
(<= (length (Val P S)) 3)))
u))])
(and (not (empty? Z))
(ormap (lambda (PQR)
(let* ([P (first PQR)]
[Q (second PQR)]
[R (third PQR)]
[Y (Union (Val P S) (Val Q S) (Val R S))])
(and (= 3 (length Y))
(Intersect?
Y
(apply append
(map (lambda (T) (Val T S))
(filter
(lambda (P) (empty-cell? P S))
(remove* PQR u)))))
(list PQR
Y
(filter (lambda (X)
(and (empty-cell? X S)
(Cell-see? X P)
(Cell-see? X Q)
(Cell-see? X R)
(Intersect? Y
(Val X S))))
loCells)))))
Z))))
(ormap VT-in-unit Units))
;; VT->remove-little-num: Sudoku VT -> Sudoku
;; to build the sudoku with the little numbers in the way of the Visible Triple
;; of sudoku S removed, and to print out a statement such as
;; "Visible Triple in cells {C2 C3} removes 1 and 5 from cells {A2 C4 C6}"
(define (VT->remove-little-num S FVT)
(let ([PQR (first FVT)]
[Y (second FVT)]
[seen-cells (third FVT)])
(display "Visible Triple in cells ") (loCell-display PQR)
(display " removes ") (display Y) (display " from cells ")
(loCell-display seen-cells)
(newline)(newline)
(Build-sudoku (lambda (R)
(if (member R seen-cells)
(remove* Y (Val R S))
(Val R S))))))
;;;;;;;;;;;;; Solving the Sudoku
;; sudoku-solver: Sudoku symbol -> void
;; to solve the sudoku S using these techniques: Hidden Singles, Singles,
;; Digit/Unit-Unit Pattern, Visible Pairs, and Hidden Pairs.
(define (sudoku-solver S technique)
(cond
[(symbol=? technique 'fresh)
(print (sudoku->picture
(Build-sudoku (lambda (P)
(let ([nl (Val P S)])
(if (zero? nl)
empty
nl))))))
(newline)(newline)
(let ([ffs (fix-fresh-sudoku S)])
(print (sudoku->picture ffs))
(newline)(newline)
(sudoku-solver ffs 'update))]
[(symbol=? technique 'update)
(let ([S1 (update-sudoku S)])
(if (Valid? S1)
(begin
(print (sudoku->picture S1))
(newline)(newline)
(sudoku-solver S1 'hidden-single))
(begin (display "error")
(newline)
(pretty-print S))))]
[(symbol=? technique 'hidden-single)
(let ([HS (FindHiddenSingle S)])
(if HS
(let ([S1 (HiddenSingle->big-num S HS)])
(sudoku-solver S1 'update))
(sudoku-solver S 'single)))]
[(symbol=? technique 'single)
(let ([FS (FindSingle S)])
(if FS
(let ([S1 (Single->big-num S FS)])
(sudoku-solver S1 'update))
(sudoku-solver S 'D/U-U)))]
[(symbol=? technique 'D/U-U)
(let ([FD/U-U (findD/U-U S)])
(if FD/U-U
(let ([S1 (D/U-U->remove-little-num S FD/U-U)])
(sudoku-solver S1 'update))
(sudoku-solver S 'VP)))]
[(symbol=? technique 'VP)
(let ([FVP (findVP S)])
(if FVP
(let ([S1 (VP->remove-little-num S FVP)])
(sudoku-solver S1 'update))
(sudoku-solver S 'HP)))]
[(symbol=? technique 'HP)
(let ([FHP (FindHiddenPair S)])
(if FHP
(let ([S1 (HiddenPair->remove-little-num S FHP)])
(sudoku-solver S1 'update))
(sudoku-solver S 'VT)))]
[(symbol=? technique 'VT)
(let ([FVT (findVT S)])
(if FVT
(let ([S1 (VT->remove-little-num S FVT)])
(sudoku-solver S1 'update))
(sudoku-solver S 'done)))]
[(symbol=? technique 'done)
(display "done") (newline)
(pretty-print S) (newline)]))
;;;;;;;;;;;;;; Examples
;; Use Overwrite Mode to type in big numbers of fresh sudokus.
(define template
'((0 0 0 0 0 0 0 0 0)
(0 0 0 0 0 0 0 0 0)
(0 0 0 0 0 0 0 0 0)
(0 0 0 0 0 0 0 0 0)
(0 0 0 0 0 0 0 0 0)
(0 0 0 0 0 0 0 0 0)
(0 0 0 0 0 0 0 0 0)
(0 0 0 0 0 0 0 0 0)
(0 0 0 0 0 0 0 0 0)))
;(sudoku-solver template 'fresh)
(define puzzle
'((0 0 0 9 0 0 0 0 4)
(0 0 7 0 0 4 0 0 0)
(8 0 0 0 0 0 7 2 0)
(1 0 0 3 0 0 0 0 0)
(0 0 6 1 0 7 2 0 0)
(3 0 0 0 0 6 0 0 9)
(0 3 8 0 4 0 0 6 7)
(0 0 0 6 0 0 9 0 0)
(4 0 0 0 0 9 0 0 0)))
(sudoku-solver puzzle 'fresh)
(define puzzle1
'(((2 ) (1 5) 3 9 7 (1 2) (6 8) (1 5 8) 4)
((2 6) (1 5) 7 8 (1 2 3) 4 (3 6) 9 (1 3 5))
(8 9 4 5 6 (1 3) 7 2 (1 3))
(1 (7 8) 9 3 (2 5 8) (2 5 8) 4 (5 7) 6)
(5 4 6 1 9 7 2 (3 8) (3 8))
(3 (7 8) 2 4 (5 8) 6 (1 5) (1 5 7) 9)
(9 3 8 2 4 (1 5) (1 5) 6 7)
(7 2 (1 5) 6 (1 3 5 8) (1 3 5 8) 9 4 (1 3 5 8))
(4 6 (1 5) 7 (1 3 5 8) 9 (3 8) (1 3 5 8) 2)))
;(sudoku-solver puzzle1 'update)
(define puzzle2
'(((2 6) (1 5) 3 9 7 (1 2) (6 8) (1 5 8) 4)
((2 6) (1 5) 7 8 (1 2 3) 4 (3 6) 9 (1 3 5))
(8 9 4 5 6 (1 3) 7 2 (1 3))
(1 (7 8) 9 3 (2 5 8) (2 5 8) 4 (5 7) 6)
(5 4 6 1 9 7 2 (3 8) (3 8))
(3 (7 8) 2 4 (5 8) 6 (1 5) (1 5 7) 9)
(9 3 8 2 4 (1 5) (1 5) 6 7)
(7 2 (1 5) 6 (1 3 5 8) (1 3 5 8) 9 4 (1 3 5 8))
(4 6 (1 5) 7 (1 3 5 8) 9 (3 8) (1 3 5 8) 2)))
;(sudoku-solver puzzle2 'update)
(newline)
(display "Bilocation Chain G6 -1- G7 + F7 -1- F8 -7- F2 -8- D2 + D6 -8- H6 -3- C6 removes 1 in cell C6")
(newline)(newline)
(define puzzle3
'(((2 6) (1 5) 3 9 7 (1 2) (6 8) (1 5 8) 4)
((2 6) (1 5) 7 8 (1 2 3) 4 (3 6) 9 (1 3 5))
(8 9 4 5 6 (3) 7 2 (1 3))
(1 (7 8) 9 3 (2 5 8) (2 5 8) 4 (5 7) 6)
(5 4 6 1 9 7 2 (3 8) (3 8))
(3 (7 8) 2 4 (5 8) 6 (1 5) (1 5 7) 9)
(9 3 8 2 4 (1 5) (1 5) 6 7)
(7 2 (1 5) 6 (1 3 5 8) (1 3 5 8) 9 4 (1 3 5 8))
(4 6 (1 5) 7 (1 3 5 8) 9 (3 8) (1 3 5 8) 2)))
(sudoku-solver puzzle3 'update)
(newline)
(display "Bivalue Chain 35B9 + 58A8 + 83E8 removes 3 in cell E9")
(newline)(newline)
(define puzzle4
'(((2 6) (1 5) 3 9 7 (1 2) (6 8) (5 8) 4)
((2 6) (1 5) 7 8 (1 2) 4 (3 6) 9 (3 5))
(8 9 4 5 6 3 7 2 1)
(1 (7 8) 9 3 (2 5 8) (2 5 8) 4 (5 7) 6)
(5 4 6 1 9 7 2 (3 8) (8))
(3 (7 8) 2 4 (5 8) 6 (1 5) (1 5 7) 9)
(9 3 8 2 4 (1 5) (1 5) 6 7)
(7 2 (1 5) 6 (1 3 5 8) (1 5 8) 9 4 (3 5 8))
(4 6 (1 5) 7 (1 3 5 8) 9 (3 8) (1 3 5 8) 2)))
(sudoku-solver puzzle4 'update)
(newline)
(display "Bivalue Chain 53H9 + 35B9 + 51B2 + 12B5 + 21A6 + 15G6 removes 5 in cell G7")
(newline)(newline)
(define puzzle5
'(((2 6) (1 5) 3 9 7 (1 2) (6 8) (5 8) 4)
((2 6) (1 5) 7 8 (1 2) 4 (3 6) 9 (3 5))
(8 9 4 5 6 3 7 2 1)
(1 (7 8) 9 3 (2 5 8) (2 5 8) 4 (5 7) 6)
(5 4 6 1 9 7 2 3 8)
(3 (7 8) 2 4 (5 8) 6 (1 5) (1 5 7) 9)
(9 3 8 2 4 (1 5) (1) 6 7)
(7 2 (1 5) 6 (1 3 5 8) (1 5 8) 9 4 (3 5))
(4 6 (1 5) 7 (1 3 5) 9 (3 8) (1 5 8) 2)))
(sudoku-solver puzzle5 'update)
![[logo]](/logo.png){kind=logo}