From d936b534684f5b90b1900909ede1ca6297b308d7 Mon Sep 17 00:00:00 2001 From: Ademar Gonzalez Date: Sat, 25 Jul 2026 12:16:04 -0400 Subject: [PATCH 1/2] Add constant-width chessboard figure examples Two takes on enumerating figures of constant width on an n x n board, the problem from https://ademar.name/blog/2009/04/finding-figures-of-constant-wi.html and Hernandez & Robert, American Mathematical Monthly 112 (2005) 42-50. constant-width.ikr transcribes the original F# frontier search: per-line remaining-capacity vectors and a hand-written CPS pipeline. It finds connected figures only, so it cannot express the width-1 case. constant-width-amb.ikr reformulates the search. Multi-shot shift/reset carry an amb layer, so the solver is direct style with no explicit continuation arguments and the undo of board state lives in the choice point. Search strategies are vau operatives over an emit sink, so collect and first-of drive the same solver. Deciding rows in order rather than growing from a seed gives exact (n,k,w) semantics and admits disconnected figures, which makes n-queens the w=1 case. It also implements the paper's algebra -- composition and transversal deletion over an encapsulated figure type -- which builds width 3, 4, 6 and 8 figures in milliseconds where search needs weeks. Counts agree with an independent exhaustive row-by-row search: 92 and 4 for 8- and 6-queens, and 1, 5, 2, 24, 30 figures of type (4,4,2), (5,4,2), (6,6,2), (7,6,2) and (8,8,2). Every constructed figure is checked by fig-type, which shares no code with the searcher or the builders. Co-Authored-By: Claude Opus 5 --- Examples/README.md | 2 + Examples/constant-width-amb.ikr | 434 ++++++++++++++++++++++++++++++++ Examples/constant-width.ikr | 304 ++++++++++++++++++++++ 3 files changed, 740 insertions(+) create mode 100644 Examples/constant-width-amb.ikr create mode 100644 Examples/constant-width.ikr diff --git a/Examples/README.md b/Examples/README.md index c59df37..fffe8ad 100644 --- a/Examples/README.md +++ b/Examples/README.md @@ -26,6 +26,8 @@ dotnet run --project IronKernel -- run hello.ikc | `contracts.ikr` | Operative/applicative contracts and guarded folding | Prints validated results | | `coroutines.ikr` | Cooperative scheduling experiment | Historical example; not yet covered by the compatibility suite | | `zipper.ikr` | Delimited continuations | Functional zipper traversal | +| `constant-width.ikr` | Mutable vectors, CPS backtracking, `args` | Enumerates constant-width chessboard figures; takes `n k w` | +| `constant-width-amb.ikr` | `shift`/`reset` as an `amb` layer, `vau` search strategies, encapsulation types | Same problem, direct style; also solves n-queens and builds width 3/4/8 figures | | `sqrt.ikr` | Operative-based numeric procedure | Defines `sqrt`; intentionally produces no output | | `yingyang.ikr` | Classic yin-yang continuation loop | Intentionally non-terminating; do not use it to test packaging | diff --git a/Examples/constant-width-amb.ikr b/Examples/constant-width-amb.ikr new file mode 100644 index 0000000..7ac23cb --- /dev/null +++ b/Examples/constant-width-amb.ikr @@ -0,0 +1,434 @@ +; Figures of constant width, second take: nondeterminism and algebra +; ================================================================== +; +; `constant-width.ikr` transcribes the backtracking search from +; +; https://ademar.name/blog/2009/04/finding-figures-of-constant-wi.html +; +; faithfully, continuation-passing style and all. This file attacks the same +; problem -- see that file, or the Hernandez-Robert paper it cites, for what a +; figure of constant width is -- from two directions that suit IronKernel +; rather than F#. +; +; 1. Backtracking is not a program shape here, it is a library. +; +; `shift`/`reset` in IronKernel are multi-shot and re-delimiting, which is +; exactly what a nondeterministic `amb` needs: a choice point invokes the +; captured continuation once per alternative. So the solver is written in +; *direct style* -- `(let ((c (pick-column x lo hi))) ...)` reads as "let c +; be a column", and the enumeration, the undo of the board state, and the +; pruning all happen inside `pick-column`. There is not one explicit +; continuation argument in the search. +; +; The other half of that split is that the *strategy* becomes a value. The +; solver only ever calls `emit`; two operatives decide what that means: +; `collect` gathers every solution, `first-of` escapes with the first one +; through `call/cc`. Same solver, different searches, chosen at the call +; site. Adding a "first 10" or a randomized strategy is a handler, not a +; rewrite. +; +; A consequence worth stating: this solver enumerates figures of *exactly* +; type (n,k,w), disconnected ones included. The original algorithm grows a +; figure outward from a seed square and so can only ever find connected +; figures -- it explicitly cannot solve the n-queens problem, which is the +; w=1 case. This one can, and `(figures 8 8 1)` returning 92 is the check. +; +; 2. For width 3 and up, do not search at all -- build. +; +; The paper's Lemma 1 says that composing an *extended* constant width +; figure with any constant width figure multiplies the widths, and that a +; figure decomposable into transversals stays decomposable. That is a +; constructive recipe, and it is far cheaper than search: the original +; program needed about 31 days to exhaust width 3 on an 11x11 board, whereas +; composing the paper's Figure 3 with its Figure 2 and deleting a transversal +; produces a width 3 figure in milliseconds. Widths 4 and 8 come out of the +; same handful of lines, and peeling the width 8 one twice reaches width 6 -- +; which the paper reports its authors never managed to find by search. +; +; `transversal` is itself written against the `amb` layer from part 1, so +; the same three-line nondeterminism library drives both halves of the file. +; +; Run it: +; +; dotnet run --project IronKernel -- Examples/constant-width-amb.ikr +; +; Takes about half a minute, nearly all of it in the 8-queens enumeration -- +; the constructive half of the file runs in milliseconds. Requires the default +; `unrestricted` profile (it prints to the host console). +; +; Everything printed is checked by `fig-type`, which shares no code with the +; searcher or the builders. The searcher's counts also agree with an +; independent exhaustive row-by-row search: 92 and 4 for 8- and 6-queens, and +; 1, 5, 2, 24, 30 figures of type (4,4,2), (5,4,2), (6,6,2), (7,6,2), (8,8,2). + +; --------------------------------------------------------------------------- +; 1. Nondeterminism as a library +; --------------------------------------------------------------------------- + +(defn (reverse xs) + (letrec ((loop (lambda (l acc) + (if (null? l) acc (loop (cdr l) (cons (car l) acc)))))) + (loop xs ()))) + +; The solution sink. Nondeterministic code calls `emit`; what that does is +; whatever the enclosing strategy installed. +(define sink (make-vector 1 (lambda (s) #inert))) +(defn (emit s) ((vector-ref sink 0) s)) + +; Abandon this branch: capture the continuation up to the delimiter and drop +; it, so control returns to the most recent choice point. +(defn (fail) (shift (lambda (k) #inert))) + +; Yield each element of xs in turn. `k` is multi-shot and re-delimits, so the +; whole remaining computation runs once per alternative. +(defn (amb xs) (shift (lambda (k) (for-each xs k)))) + +; Strategy 1: run body, return the list of everything it emitted. +(define collect + (vau body env + (let ((acc (make-vector 1 ())) (saved (vector-ref sink 0))) + (vector-set! sink 0 + (lambda (s) (vector-set! acc 0 (cons s (vector-ref acc 0))))) + (reset (eval env (cons sequence body))) + (vector-set! sink 0 saved) + (reverse (vector-ref acc 0))))) + +; Strategy 2: stop at the first emission and escape with it, or () if there is +; none. The whole search tree below the first hit is never explored. +(define first-of + (vau body env + (let ((saved (vector-ref sink 0))) + (let ((r (call/cc (lambda (return) + (vector-set! sink 0 (lambda (s) (return s))) + (reset (eval env (cons sequence body))) + ())))) + (vector-set! sink 0 saved) + r)))) + +; --------------------------------------------------------------------------- +; 2. The solver: emit every figure of exactly type (n, k, w) +; +; Rows are decided in order. Each row is either skipped or given exactly w +; columns, and a row's squares are chosen left to right. Every line carries a +; count of squares placed on it so far; a line is legal at the end when that +; count is 0 or w, and legal in the middle when the shortfall still fits in the +; rows below. +; --------------------------------------------------------------------------- + +(defn (figures n k w) + (define col (make-vector n 0)) + (define pd (make-vector (- (* 2 n) 1) 0)) + (define nd (make-vector (- (* 2 n) 1) 0)) + (define fig (make-vector 1 ())) + + (defn (pdx x y) (+ x y)) + (defn (ndx x y) (- (+ n (- x y)) 1)) + + (defn (free? x y) + (if (< (vector-ref col y) w) + (if (< (vector-ref pd (pdx x y)) w) + (< (vector-ref nd (ndx x y)) w) + #f) + #f)) + + (defn (bump! x y d) + (vector-set! col y (+ (vector-ref col y) d)) + (vector-set! pd (pdx x y) (+ (vector-ref pd (pdx x y)) d)) + (vector-set! nd (ndx x y) (+ (vector-ref nd (ndx x y)) d))) + + (defn (place! x y) + (bump! x y 1) + (vector-set! fig 0 (cons (cons x y) (vector-ref fig 0)))) + + (defn (unplace! x y) + (bump! x y -1) + (vector-set! fig 0 (cdr (vector-ref fig 0)))) + + ; The one choice point of the search. Each legal column in [lo,hi) is placed, + ; offered to the continuation, and taken back once that continuation has run + ; to exhaustion -- so the board is always consistent with the caller's view, + ; and the caller never sees a continuation at all. + (defn (pick-column x lo hi) + (shift (lambda (k) + (letrec ((loop (lambda (c) + (if (< c hi) + (begin + (if (free? x c) + (begin (place! x c) (k c) (unplace! x c)) + #inert) + (loop (+ c 1))) + #inert)))) + (loop lo))))) + + ; `need` more squares in row x, all in columns >= y. Reads as a loop; is a + ; tree. + (defn (fill-row x y need) + (if (zero? need) + #inert + (let ((c (pick-column x y (+ (- n need) 1)))) + (fill-row x (+ c 1) (- need 1))))) + + ; How many cells of diagonal `d` lie in rows x..n-1. Both diagonal families + ; are indexed so that this one formula serves for each. + (defn (cells-from d x) + (let ((lo (if (> x (- d (- n 1))) x (- d (- n 1)))) + (hi (if (< (- n 1) d) (- n 1) d))) + (if (< hi lo) 0 (+ (- hi lo) 1)))) + + ; A line is still viable if it is untouched, already full, or short by no + ; more than the cells it has left. At x = n this is the 0-or-w test. + (defn (line-ok? used avail) + (if (zero? used) #t (if (eq? used w) #t (<= (- w used) avail)))) + + (define ndiags (- (* 2 n) 1)) + + (defn (feasible? x) + (let ((rowsleft (- n x))) + (letrec + ((cols (lambda (c) + (if (eq? c n) #t + (if (line-ok? (vector-ref col c) rowsleft) + (cols (+ c 1)) #f)))) + ; both diagonal families share an index, so one `cells-from` serves + ; the pair + (diags (lambda (d) + (if (eq? d ndiags) #t + (let ((a (cells-from d x))) + (if (line-ok? (vector-ref pd d) a) + (if (line-ok? (vector-ref nd d) a) + (diags (+ d 1)) #f) + #f)))))) + (if (cols 0) (diags 0) #f)))) + + (defn (solve x placed) + (if (eq? x n) + ; every row decided: the figure must have k filled rows and no line may + ; be left part-way + (if (eq? placed k) + (if (feasible? n) (emit (vector-ref fig 0)) (fail)) + (fail)) + (begin + (if (< (- n x) (- k placed)) (fail) #inert) ; too few rows left + (if (feasible? x) #inert (fail)) + (if (amb (list #t #f)) + (begin (if (< placed k) #inert (fail)) + (fill-row x 0 w) + (solve (+ x 1) (+ placed 1))) + (solve (+ x 1) placed))))) + + (solve 0 0)) + +; --------------------------------------------------------------------------- +; 3. Figures as an abstract type, and the constant width test +; --------------------------------------------------------------------------- + +(provide! (figure figure? fig-n fig-squares) + (define (enc figure? dec) (make-encapsulation-type)) + (define figure (lambda (n squares) (enc (list n squares)))) + (define fig-n (lambda (f) (car (dec f)))) + (define fig-squares (lambda (f) (cadr (dec f))))) + +(defn (tally! v i) (vector-set! v i (+ (vector-ref v i) 1))) + +; (n k w) when f has constant width, () otherwise. Everything this file builds +; is checked with this, and it shares no code with the builders. +(defn (fig-type f) + (let* ((n (fig-n f)) (s (fig-squares f)) (m (- (* 2 n) 1)) + (rw (make-vector n 0)) (cl (make-vector n 0)) + (pd (make-vector m 0)) (nd (make-vector m 0))) + (for-each s (lambda (p) + (tally! rw (car p)) + (tally! cl (cdr p)) + (tally! pd (+ (car p) (cdr p))) + (tally! nd (- (+ n (- (car p) (cdr p))) 1)))) + ; fold the four families together: every non-zero count must agree + (letrec ((scan (lambda (v i len w) + (if (eq? i len) w + (let ((c (vector-ref v i))) + (if (zero? c) (scan v (+ i 1) len w) + (if (zero? w) (scan v (+ i 1) len c) + (if (eq? c w) (scan v (+ i 1) len w) -1)))))))) + (let* ((w1 (scan rw 0 n 0)) (w2 (scan cl 0 n w1)) + (w3 (scan pd 0 m w2)) (w (scan nd 0 m w3))) + (if (< w 1) () (list n (/ (length s) w) w)))))) + +; `/` truncates toward zero, so fold the negative case back by hand. +(defn (modulo a m) (let ((r (- a (* m (/ a m))))) (if (< r 0) (+ r m) r))) + +; Extended constant width: the diagonals wrap around the board, so the lines +; are i+j and i-j taken mod n. Lemma 1 needs this of its left operand. +(defn (extended? f) + (let* ((n (fig-n f)) (s (fig-squares f)) + (p (make-vector n 0)) (q (make-vector n 0))) + (for-each s (lambda (sq) + (tally! p (modulo (+ (car sq) (cdr sq)) n)) + (tally! q (modulo (- (car sq) (cdr sq)) n)))) + (let ((t (fig-type f))) + (if (null? t) #f + (let ((w (car (cddr t)))) + (letrec ((ok (lambda (v i) + (if (eq? i n) #t + (let ((c (vector-ref v i))) + (if (zero? c) (ok v (+ i 1)) + (if (eq? c w) (ok v (+ i 1)) #f))))))) + (if (ok p 0) (ok q 0) #f))))))) + +; --------------------------------------------------------------------------- +; 4. The algebra +; --------------------------------------------------------------------------- + +; Lemma 1: drop a copy of f1 into every square of f2. If f1 has extended +; constant width w1 and f2 constant width w2, the result has constant width +; w1*w2 on a board (n1*n2) wide. +(defn (compose f1 f2) + (let ((m (fig-n f1)) (acc (make-vector 1 ()))) + (for-each (fig-squares f2) (lambda (q) + (for-each (fig-squares f1) (lambda (p) + (vector-set! acc 0 + (cons (cons (+ (car p) (* m (car q))) (+ (cdr p) (* m (cdr q)))) + (vector-ref acc 0))))))) + (figure (* m (fig-n f2)) (vector-ref acc 0)))) + +(defn (same-square? p q) (if (eq? (car p) (car q)) (eq? (cdr p) (cdr q)) #f)) + +(defn (member-of? p s) + (if (null? s) #f (if (same-square? p (car s)) #t (member-of? p (cdr s))))) + +; A transversal is a subset meeting every line of f exactly once. Because f has +; constant width w and kw squares, it touches exactly k lines of each of the +; four families, so a transversal is one square per filled row whose columns +; and diagonals are all distinct -- a perfect matching, found here by the same +; `amb` machinery as the figure search. Nondeterministic: wrap in `first-of`. +(defn (transversal f) + (let* ((n (fig-n f)) (s (fig-squares f)) (m (- (* 2 n) 1)) + (byrow (make-vector n ())) + (uc (make-vector n 0)) (up (make-vector m 0)) (un (make-vector m 0))) + (for-each s (lambda (p) + (vector-set! byrow (car p) (cons p (vector-ref byrow (car p)))))) + (letrec + ((pdx (lambda (p) (+ (car p) (cdr p)))) + (ndx (lambda (p) (- (+ n (- (car p) (cdr p))) 1))) + (avail? (lambda (p) + (if (zero? (vector-ref uc (cdr p))) + (if (zero? (vector-ref up (pdx p))) + (zero? (vector-ref un (ndx p))) + #f) + #f))) + (mark! (lambda (p d) + (vector-set! uc (cdr p) (+ (vector-ref uc (cdr p)) d)) + (vector-set! up (pdx p) (+ (vector-ref up (pdx p)) d)) + (vector-set! un (ndx p) (+ (vector-ref un (ndx p)) d)))) + (pick (lambda (cands) + (shift (lambda (k) + (for-each cands (lambda (p) + (if (avail? p) + (begin (mark! p 1) (k p) (mark! p -1)) + #inert))))))) + (go (lambda (r acc) + (if (eq? r n) + (emit (reverse acc)) + (if (null? (vector-ref byrow r)) + (go (+ r 1) acc) + (let ((p (pick (vector-ref byrow r)))) + (go (+ r 1) (cons p acc)))))))) + (go 0 ())))) + +; Deleting a transversal from a figure of constant width w leaves one of +; constant width w-1. +(defn (fig-remove f t) + (let ((acc (make-vector 1 ()))) + (for-each (fig-squares f) (lambda (p) + (if (member-of? p t) + #inert + (vector-set! acc 0 (cons p (vector-ref acc 0)))))) + (figure (fig-n f) (vector-ref acc 0)))) + +(defn (peel f) + (let ((t (first-of (transversal f)))) + (if (null? t) () (fig-remove f t)))) + +; --------------------------------------------------------------------------- +; 5. Reporting +; --------------------------------------------------------------------------- + +(defn (describe name f) + (let ((t (fig-type f))) + (if (null? t) + (printf " {0}: NOT of constant width\n" name) + (printf " {0}: {1} squares on {2}x{2}, type ({2},{3},{4}){5}\n" + name (length (fig-squares f)) (car t) (cadr t) (car (cddr t)) + (if (extended? f) ", extended" ""))))) + +(defn (draw f) + (let ((n (fig-n f)) (s (fig-squares f))) + (letrec ((loop (lambda (x y) + (if (eq? x n) #inert + (if (eq? y n) + (begin (print "\n") (loop (+ x 1) 0)) + (begin + (print (if (member-of? (cons x y) s) "Q" ".")) + (loop x (+ y 1)))))))) + (loop 0 0)))) + +(defn (draw-squares n s) (draw (figure n s))) + +; --------------------------------------------------------------------------- +; 6. Demonstration +; --------------------------------------------------------------------------- + +(print "searching -- one solver, two strategies\n\n") + +(printf " (8,8,1) queens : {0} solutions\n" + (length (collect (figures 8 8 1)))) +(printf " (6,6,1) queens : {0} solutions\n" + (length (collect (figures 6 6 1)))) +(printf " (4,4,2) : {0} figure(s)\n" + (length (collect (figures 4 4 2)))) +(printf " (5,4,2) : {0} figure(s)\n" + (length (collect (figures 5 4 2)))) +(printf " (6,6,2), all : {0} figure(s)\n" + (length (collect (figures 6 6 2)))) +(printf " (6,6,2), first only : {0} squares\n" + (length (first-of (figures 6 6 2)))) +(print "\n") +(draw-squares 5 (car (collect (figures 5 4 2)))) + +(print "\nbuilding -- Lemma 1 and transversal deletion\n\n") + +; The paper's Figure 2 and Figure 3, the two smallest width 2 figures. Both +; come straight out of the search above; Figure 3 is the one with the wrapping +; diagonals, which is what makes the composition below legal. +(define fig2 (figure 4 '((0 & 1) (0 & 2) (1 & 0) (1 & 3) + (2 & 0) (2 & 3) (3 & 1) (3 & 2)))) +(define fig3 (figure 5 '((0 & 1) (0 & 3) (1 & 0) (1 & 4) + (3 & 0) (3 & 4) (4 & 1) (4 & 3)))) + +(describe "Figure 2" fig2) +(describe "Figure 3" fig3) + +(define w4 (compose fig3 fig2)) +(define w3 (peel w4)) +(define w2 (peel w3)) +(define w1 (peel w2)) + +(describe "fig3 . fig2" w4) +(describe " peeled once" w3) +(describe " peeled twice" w2) +(describe " peeled thrice" w1) + +(print "\n constant width 3 on a 20x20 board (the paper's Figure 6):\n\n") +(draw w3) + +; One more composition doubles the width again, and peeling that reaches the +; widths in between. The paper reports that its authors never found a figure of +; width 6 with a computer search; this one is built and checked in under a +; second. +(define w8 (compose fig3 w4)) +(define w7 (peel w8)) +(define w6 (peel w7)) + +(print "\n") +(describe "fig3 . (fig3 . fig2)" w8) +(describe " peeled once" w7) +(describe " peeled twice" w6) +(print "\n") diff --git a/Examples/constant-width.ikr b/Examples/constant-width.ikr new file mode 100644 index 0000000..814d45d --- /dev/null +++ b/Examples/constant-width.ikr @@ -0,0 +1,304 @@ +; Figures of constant width on a chessboard +; ========================================= +; +; A *figure* is any set of squares on an n x n board. It has *constant width w* +; when every row, every column and every diagonal (slope +1 and slope -1) meets +; it in either 0 or exactly w squares. A figure of constant width w occupying +; k*w squares is said to be of type (n, k, w); k is then also its number of +; non-empty rows. Figures of type (n, n, 1) are exactly the solutions of the +; n-queens problem. +; +; Janko Hernandez, Leonel Robert, "Figures of Constant Width on a Chessboard", +; American Mathematical Monthly 112 (2005) 42-50. +; https://userweb.ucs.louisiana.edu/~C00254569/hernandez-robert.pdf +; +; This program is an IronKernel transcription of the exhaustive backtracking +; search described in +; +; https://ademar.name/blog/2009/04/finding-figures-of-constant-wi.html +; +; It enumerates the *connected* figures of type (n, _, w). Two squares are +; adjacent when they share a row, a column, or a main diagonal; a figure is +; connected when every pair of its squares is joined by a chain of such steps. +; Constant width 1 figures (the n-queens solutions) are totally disconnected, +; so they are never reported. +; +; How the search works +; -------------------- +; For each of the 2n + 2(2n-1) lines of the board we keep the number of squares +; that still have to be placed on it: w for an untouched line, 0 for a saturated +; one. Committing to a square decrements the four counters running through it. +; +; The frontier ("buffer") holds squares that are already committed but whose +; local constraints have not been discharged yet. Popping a square p off the +; frontier means choosing, right there, *every* square that still has to share a +; line with p: exactly (cap-r p) more in its row, (cap-c p) in its column, and +; likewise on both diagonals. Those choices join the frontier, and every other +; square on p's four lines is permanently out of play -- which is what makes the +; search converge instead of wandering the board. +; +; When the frontier drains, every committed square has all four of its lines +; saturated, so the accumulated set is a figure of constant width w. It is +; connected, because the frontier only ever grew along lines of squares already +; in it. +; +; Running it +; ---------- +; dotnet run --project IronKernel -- Examples/constant-width.ikr ; 5 4 2 +; dotnet run --project IronKernel -- Examples/constant-width.ikr 4 4 2 +; dotnet run --project IronKernel -- Examples/constant-width.ikr 6 6 2 +; dotnet run --project IronKernel -- Examples/constant-width.ikr 11 10 3 +; +; The arguments are n k w : the board size, the width, and k as a pruning +; bound. Give all three or none. k*w is not a filter on the output but a cutoff +; on the search: a branch is abandoned as soon as it can no longer reach k*w +; squares, yet a branch that survives still reports whatever figure it lands on, +; which may be a smaller one. So every figure of type (n, k', w) with k' >= k is +; guaranteed to be found, some figures below k appear as a bonus, and raising k +; only makes the search faster. Each figure is printed with the type it really +; has. +; +; The default 5 4 2 run finds five figures in about three seconds: the paper's +; Figure 3, of type (5,4,2), plus the four placements of its Figure 2 -- the +; unique connected figure of type (4,4,2) -- inside the 5x5 board. +; +; args time figures found +; ------ ------ ----------------------------------------------- +; 4 4 2 0.4 s 1 x (4,4,2) the paper's Figure 2 +; 5 4 2 3 s 5 x (5,4,2) the default run +; 6 6 2 16 s 2 x (6,6,2) +; 6 4 2 28 s 15 x (6,4,2), 2 x (6,6,2) +; 7 6 2 5.6 min 24 x (7,6,2), 4 x (7,4,2) +; +; These counts agree with an independent exhaustive row-by-row search. Width 3 +; is a different world: the smallest figure of constant width 3 lives on an +; 11x11 board, and the original F# program needed some 31 days to exhaust +; (11, _, 3), so treat that last command line as a long-running job rather than +; a demo. +; +; The default `unrestricted` profile is required: the program prints through the +; host console and parses its arguments with System.Int32.Parse. +; +; Hot paths below use nested `if` rather than `cond`, `and?` and `or?`. Those +; three are compound operatives from the bootstrap library and cost an `eval` +; per clause; `if` is a primitive. Avoiding them in the innermost loops makes +; the whole search about three times faster. + +; --------------------------------------------------------------------------- +; Small list helpers (the bootstrap library deliberately stays minimal) +; --------------------------------------------------------------------------- + +(defn (append xs ys) + (if (null? xs) ys (cons (car xs) (append (cdr xs) ys)))) + +(defn (>=? a b) (not? (< a b))) + +; --------------------------------------------------------------------------- +; The search +; +; n board size +; w the constant width +; k pruning bound: branches that can no longer reach k*w squares are cut +; report applied to every figure found, as a list of (x . y) squares +; --------------------------------------------------------------------------- + +(defn (find-figures n k w report) + + ; Remaining capacity of every line. Rows and columns are indexed by + ; coordinate; the diagonal of slope -1 through (x, y) is indexed by x + y and + ; the one of slope +1 by n + (x - y) - 1, so both fit in 2n-1 slots. + (define rows (make-vector n w)) + (define columns (make-vector n w)) + (define diag1 (make-vector (- (* 2 n) 1) w)) + (define diag2 (make-vector (- (* 2 n) 1) w)) + + (defn (pdiag p) (+ (car p) (cdr p))) + (defn (ndiag p) (- (+ n (- (car p) (cdr p))) 1)) + + (defn (cap-r p) (vector-ref rows (car p))) + (defn (cap-c p) (vector-ref columns (cdr p))) + (defn (cap-pd p) (vector-ref diag1 (pdiag p))) + (defn (cap-nd p) (vector-ref diag2 (ndiag p))) + + ; Add d to each of the four counters running through p. + (defn (alter! p d) + (let ((r (car p)) (c (cdr p)) (i1 (pdiag p)) (i2 (ndiag p))) + (vector-set! rows r (+ (vector-ref rows r) d)) + (vector-set! columns c (+ (vector-ref columns c) d)) + (vector-set! diag1 i1 (+ (vector-ref diag1 i1) d)) + (vector-set! diag2 i2 (+ (vector-ref diag2 i2) d)) + #inert)) + + (defn (take! p) (alter! p -1)) + (defn (restore! p) (alter! p 1)) + + ; A square becomes unusable as soon as any one of its four lines is full. + (defn (open? p) + (if (zero? (cap-r p)) #f + (if (zero? (cap-c p)) #f + (if (zero? (cap-pd p)) #f + (if (zero? (cap-nd p)) #f #t))))) + + ; The board minus the corner regions, whose diagonals are shorter than w and + ; so can never carry a full width. + (defn (playable-board) + (let ((lo (- w 1)) (hi (- (- (* 2 n) w) 1))) + (letrec + ((keep? (lambda (p) + (and? (<= lo (pdiag p)) (<= (pdiag p) hi) + (<= lo (ndiag p)) (<= (ndiag p) hi)))) + ; built back to front, so the result comes out in row-major order + (loop (lambda (x y acc) + (cond ((< x 0) acc) + ((< y 0) (loop (- x 1) (- n 1) acc)) + (#t (let ((p (cons x y))) + (loop x (- y 1) + (if (keep? p) (cons p acc) acc)))))))) + (loop (- n 1) (- n 1) ())))) + + ; Split the candidate squares by how they see q: same row, same column, same + ; diagonal of slope -1, same diagonal of slope +1, or unrelated. Two distinct + ; squares share at most one of the four lines, so the tests are disjoint. + ; Returns (r rws c cls d1 dg1 d2 dg2 rest), each count beside its list. + (defn (collect q avail) + (let ((qx (car q)) (qy (cdr q)) (qp (pdiag q)) (qn (- (car q) (cdr q)))) + (letrec + ((loop + (lambda (av r rws c cls d1 dg1 d2 dg2 rest) + (if (null? av) + (list r rws c cls d1 dg1 d2 dg2 rest) + (let* ((p (car av)) (tail (cdr av)) + (x (car p)) (y (cdr p))) + (if (eq? x qx) + (loop tail (+ r 1) (cons p rws) c cls d1 dg1 d2 dg2 rest) + (if (eq? y qy) + (loop tail r rws (+ c 1) (cons p cls) d1 dg1 d2 dg2 rest) + (if (eq? (+ x y) qp) + (loop tail r rws c cls (+ d1 1) (cons p dg1) d2 dg2 rest) + (if (eq? (- x y) qn) + (loop tail r rws c cls d1 dg1 (+ d2 1) (cons p dg2) rest) + (loop tail r rws c cls d1 dg1 d2 dg2 (cons p rest))))))))))) + (loop avail 0 () 0 () 0 () 0 () ())))) + + ; Drop the squares that have gone dead, and count what is left. + (defn (count-open avail) + (letrec + ((loop (lambda (av len kept) + (if (null? av) + (list len kept) + (if (open? (car av)) + (loop (cdr av) (+ len 1) (cons (car av) kept)) + (loop (cdr av) len kept)))))) + (loop avail 0 ()))) + + ; Commit to exactly m of the still-open squares of `avail`, in every possible + ; way, appending each choice to the frontier before invoking k*. Every square + ; is restored on the way out, so the counters are unchanged on return. + (defn (choose avail m bufflen buff k*) + (letrec + ((loop (lambda (av chosen j) + (if (zero? j) + (k* (+ bufflen m) (append buff chosen)) + (if (null? av) + #inert + (let ((p (car av)) (tail (cdr av))) + (if (open? p) + (begin (take! p) + (loop tail (cons p chosen) (- j 1)) + (restore! p)) + #inert) + (loop tail chosen j))))))) + (loop avail () m))) + + ; sol squares whose constraints are already discharged + ; len how many more squares this branch still has to reach + ; avail candidate squares, avlen of them + ; buff committed squares awaiting their turn, bufflen of them + (defn (search sol len avlen avail bufflen buff) + (if (< (+ avlen bufflen) len) + #inert ; too few squares left + (if (null? buff) + (report sol) ; frontier drained: a figure + (let* ((p (car buff)) (tail (cdr buff))) + (let (((r rws c cls d1 dg1 d2 dg2 rest) (collect p avail)) + ; The capacities are read before any of the four groups is + ; touched. No square lies on two of p's lines, so choosing + ; within one group cannot disturb the other three counters. + (need-r (cap-r p)) (need-c (cap-c p)) + (need-pd (cap-pd p)) (need-nd (cap-nd p))) + ; not enough candidates left on one of p's lines to fill it + (if (if (< r need-r) #t + (if (< c need-c) #t + (if (< d1 need-pd) #t (< d2 need-nd)))) + #inert + (choose rws need-r (- bufflen 1) tail + (lambda (b1 buf1) + (choose cls need-c b1 buf1 + (lambda (b2 buf2) + (choose dg1 need-pd b2 buf2 + (lambda (b3 buf3) + (choose dg2 need-nd b3 buf3 + (lambda (b4 buf4) + (let (((avlen* avail*) (count-open rest))) + (search (cons p sol) (- len 1) + avlen* avail* b4 buf4)))))))))))))))) + + ; Seed the search at every square in turn. Each figure is found exactly once, + ; from its first square in row-major order: a seed only ever sees the squares + ; that follow it. + (letrec + ((loop (lambda (l avlen) + (if (null? l) + #inert + (let ((p (car l)) (tail (cdr l))) + (take! p) + (search () (* k w) (- avlen 1) tail 1 (list p)) + (restore! p) + (loop tail (- avlen 1))))))) + (let (((len board) (count-open (playable-board)))) + (loop board len)))) + +; --------------------------------------------------------------------------- +; Reporting +; --------------------------------------------------------------------------- + +(defn (occupied? p sol) + (cond ((null? sol) #f) + ((and? (eq? (car p) (car (car sol))) + (eq? (cdr p) (cdr (car sol)))) #t) + (#t (occupied? p (cdr sol))))) + +(defn (draw n sol) + (letrec ((loop (lambda (x y) + (cond ((>=? x n) #inert) + ((>=? y n) (print "\n") (loop (+ x 1) 0)) + (#t (print (if (occupied? (cons x y) sol) "Q " ". ")) + (loop x (+ y 1))))))) + (loop 0 0))) + +(defn (report-figures n k w) + (let ((found (make-vector 1 0))) + (printf "connected figures of constant width {0} on a {1}x{1} board\n" w n) + (printf "(pruning branches that cannot reach {0} squares)\n\n" (* k w)) + (find-figures n k w + (lambda (sol) + (vector-set! found 0 (+ (vector-ref found 0) 1)) + (printf "#{0}: type ({1}, {2}, {3})\n" + (vector-ref found 0) n (/ (length sol) w) w) + (draw n sol) + (print "\n"))) + (printf "{0} figure(s)\n" (vector-ref found 0)))) + +; --------------------------------------------------------------------------- +; Entry point +; --------------------------------------------------------------------------- + +(defn (arg i default) + (letrec ((nth (lambda (xs j) + (cond ((null? xs) default) + ((zero? j) (. System.Int32 Parse (car xs))) + (#t (nth (cdr xs) (- j 1))))))) + (nth args i))) + +(let ((n (arg 0 5)) (k (arg 1 4)) (w (arg 2 2))) + (time (report-figures n k w))) From edc4851865e524b88ad432677186b7014412337f Mon Sep 17 00:00:00 2001 From: Ademar Gonzalez Date: Sat, 25 Jul 2026 12:16:15 -0400 Subject: [PATCH 2/2] Add IronKernel.Amb nondeterministic search library First package under lib/, extracted from Examples/constant-width-amb.ikr. An ordinary .ikproj built with ik test / ik pack; sources land at ironkernel/src/ in the nupkg. Choice points are ordinary expressions built on multi-shot, re-delimiting shift/reset: amb, amb-range, require and fail. Search strategies are vau operatives over an emit sink -- collect, first-of, count-of, and search for callers supplying their own handler -- so the code doing the searching never names a continuation and does not change when the strategy does. amb-bracket and amb-bracket-range cover searches over mutable state. Undo cannot sit at the call site, because by the time a choice expression returns the rest of the search has already run inside the continuation; entering and leaving therefore bracket the continuation from within the choice point. The library performs no host I/O. Tests cover the choice points, the strategies, nesting, state restoration, and n-queens as an integration case. Co-Authored-By: Claude Opus 5 --- README.md | 9 ++ lib/IronKernel.Amb/.gitignore | 3 + lib/IronKernel.Amb/IronKernel.Amb.ikproj | 18 +++ lib/IronKernel.Amb/README.md | 96 +++++++++++++ lib/IronKernel.Amb/src/amb.ikr | 163 +++++++++++++++++++++++ lib/IronKernel.Amb/test/amb_test.ikr | 153 +++++++++++++++++++++ 6 files changed, 442 insertions(+) create mode 100644 lib/IronKernel.Amb/.gitignore create mode 100644 lib/IronKernel.Amb/IronKernel.Amb.ikproj create mode 100644 lib/IronKernel.Amb/README.md create mode 100644 lib/IronKernel.Amb/src/amb.ikr create mode 100644 lib/IronKernel.Amb/test/amb_test.ikr diff --git a/README.md b/README.md index a0cd69b..edc6100 100644 --- a/README.md +++ b/README.md @@ -107,6 +107,15 @@ Public packages use NuGet.org initially. See [`ADR 0001`](docs/adr/0001-source-project-and-package-conventions.md) for the extension and ecosystem decision. +### Libraries in this repository + +[`lib/`](lib/) holds first-party IronKernel packages, each an ordinary +`.ikproj` built with `ik test` / `ik pack`. + +| Package | Provides | +|---|---| +| [`IronKernel.Amb`](lib/IronKernel.Amb/) | Nondeterministic search: `amb`, `require`, bracketed choice, and pluggable search strategies over multi-shot delimited continuations | + ## REPL ```bash diff --git a/lib/IronKernel.Amb/.gitignore b/lib/IronKernel.Amb/.gitignore new file mode 100644 index 0000000..b262931 --- /dev/null +++ b/lib/IronKernel.Amb/.gitignore @@ -0,0 +1,3 @@ +bin/ +obj/ +*.ikc diff --git a/lib/IronKernel.Amb/IronKernel.Amb.ikproj b/lib/IronKernel.Amb/IronKernel.Amb.ikproj new file mode 100644 index 0000000..de85efe --- /dev/null +++ b/lib/IronKernel.Amb/IronKernel.Amb.ikproj @@ -0,0 +1,18 @@ + + + net10.0 + false + true + IronKernel.Amb + 0.1.0 + IronKernel + Nondeterministic search for IronKernel: amb, require, and pluggable search strategies built on multi-shot delimited continuations. + ironkernel + src/amb.ikr + unrestricted + + + + + + diff --git a/lib/IronKernel.Amb/README.md b/lib/IronKernel.Amb/README.md new file mode 100644 index 0000000..49aba5f --- /dev/null +++ b/lib/IronKernel.Amb/README.md @@ -0,0 +1,96 @@ +# IronKernel.Amb + +Nondeterministic search for IronKernel. Choice points are ordinary +expressions, the search strategy is a value, and the code doing the searching +never mentions a continuation. + +```scheme +(collect + (let ((a (amb (list 1 2)))) + (let ((b (amb (list 10 20)))) + (emit (cons a b))))) +; => ((1 . 10) (1 . 20) (2 . 10) (2 . 20)) +``` + +Built on IronKernel's `shift`/`reset`, which are multi-shot and re-delimit when +resumed — so a choice point can invoke its captured continuation once per +alternative. + +## Use + +```bash +ik add IronKernel.Amb 0.1.0 +``` + +Or, from a checkout of this repository: + +```bash +cd lib/IronKernel.Amb +ik test +ik pack +``` + +## API + +### Choice points + +| Form | Meaning | +|---|---| +| `(amb xs)` | Yield each element of `xs`. An empty list fails. | +| `(amb-range lo hi)` | Yield each integer in `[lo, hi)` without building a list. | +| `(require test)` | Continue only if `test` holds, otherwise fail. | +| `(fail)` | Abandon the current branch. | +| `(amb-bracket xs ok? enter! leave!)` | Yield each `x` satisfying `ok?`, with `enter!` applied before the continuation runs and `leave!` after it finishes. | +| `(amb-bracket-range lo hi ok? enter! leave!)` | The same over `[lo, hi)`. | + +### Reporting + +| Form | Meaning | +|---|---| +| `(emit s)` | Report a solution. A no-op outside any strategy. | + +### Strategies + +Operatives. Each installs a delimiter, runs the body, and restores the +previous handler. + +| Form | Returns | +|---|---| +| `(collect body …)` | List of every solution, in the order found. | +| `(first-of body …)` | The first solution, or `()`. Escapes through `call/cc`, so the rest of the tree is never explored. | +| `(count-of body …)` | How many solutions, retaining none of them. | +| `(search handler body …)` | `#inert`; applies `handler` to each solution. Use for strategies of your own. | + +## Mutable state and backtracking + +A search that mutates a board or a set of used lines has to undo that mutation +when a branch is abandoned, and doing it at the call site does not work: by the +time a choice expression returns, the rest of the search has already run inside +the continuation. The undo belongs to the choice point, which is what +`amb-bracket` is for. + +```scheme +(let ((y (amb-bracket-range 0 n + (lambda (c) (free? x c)) ; guard + (lambda (c) (mark! x c 1)) ; before the continuation runs + (lambda (c) (mark! x c -1))))) ; after it has been exhausted + (place-queen (+ x 1))) +``` + +State stays consistent with the caller's view of it, and the caller still never +sees a continuation. `test/amb_test.ikr` builds n-queens this way in about +twenty lines. + +## Notes + +- Strategies nest: an inner search runs to completion inside one branch of an + outer one. +- The library performs no host I/O. +- `amb` and friends must run inside a strategy — that is what installs the + `reset` their `shift` needs. + +## Origin + +Extracted from [`Examples/constant-width-amb.ikr`](../../Examples/constant-width-amb.ikr), +which enumerates figures of constant width on a chessboard and, as the width-1 +case, solves the n-queens problem. diff --git a/lib/IronKernel.Amb/src/amb.ikr b/lib/IronKernel.Amb/src/amb.ikr new file mode 100644 index 0000000..9689d71 --- /dev/null +++ b/lib/IronKernel.Amb/src/amb.ikr @@ -0,0 +1,163 @@ +; IronKernel.Amb -- nondeterministic search as a library +; ====================================================== +; +; Backtracking, expressed so that the code doing the searching never mentions +; a continuation. IronKernel's `shift`/`reset` are multi-shot and re-delimit +; when resumed, so a choice point can simply invoke its captured continuation +; once per alternative: +; +; (collect +; (let ((a (amb (list 1 2)))) +; (let ((b (amb (list 10 20)))) +; (emit (cons a b))))) +; ; => ((1 . 10) (1 . 20) (2 . 10) (2 . 20)) +; +; Two ideas carry the library. +; +; Choice points are ordinary expressions. `amb` returns each element of a +; list, `amb-range` each integer of a half-open interval, and `require` prunes +; the current branch. Search code reads as if it were straight-line code that +; happens to be run once per candidate. +; +; The strategy is a value. Nondeterministic code only ever calls `emit`; what +; that means is decided by the operative wrapping it. `collect` gathers every +; solution, `first-of` escapes with the first, `count-of` tallies without +; retaining anything, and `search` takes an arbitrary handler so you can add +; your own. The searcher does not change when the strategy does. +; +; Mutable state and backtracking +; ------------------------------ +; A search that mutates a board, a counter or a set of used lines has to undo +; that mutation when a branch is abandoned. Doing it at the call site does not +; work: by the time a choice expression returns, the rest of the search has +; already run inside the continuation. The undo belongs to the choice point, +; which is what `amb-bracket` provides -- it enters a candidate, hands it to +; the continuation, and leaves it only once that continuation has run to +; exhaustion: +; +; (let ((c (amb-bracket-range 0 n free? place! unplace!))) +; (place-rest (+ c 1))) +; +; State is therefore always consistent with the caller's view of it, and the +; caller still never sees a continuation. +; +; Notes +; ----- +; * `emit` outside any strategy is a no-op, so a nondeterministic procedure is +; safe to call anywhere. +; * Strategies nest. Each installs its own delimiter, so an inner search runs +; to completion inside one branch of an outer one, and restores the previous +; handler when it is done. +; * Nothing here performs host I/O. + +(provide! (fail require amb amb-range amb-bracket amb-bracket-range + emit search collect first-of count-of) + + ; --- private ------------------------------------------------------------ + + (define list-reverse + (lambda (xs) + (letrec ((loop (lambda (l acc) + (if (null? l) acc (loop (cdr l) (cons (car l) acc)))))) + (loop xs ())))) + + ; The handler in force. Held in a vector so that the strategy operatives can + ; swap it dynamically and put it back afterwards. + (define sink (make-vector 1 (lambda (s) #inert))) + + (define with-sink + (lambda (handler thunk) + (let ((saved (vector-ref sink 0))) + (vector-set! sink 0 handler) + (reset (thunk)) + (vector-set! sink 0 saved)))) + + ; --- choice points ------------------------------------------------------ + + ; Abandon this branch: capture the continuation up to the delimiter and drop + ; it, returning control to the most recent choice point. + (define fail (lambda () (shift (lambda (k) #inert)))) + + ; Keep going only if the test holds. + (define require (lambda (test) (if test #inert (fail)))) + + ; Yield each element of xs. An empty list fails. + (define amb (lambda (xs) (shift (lambda (k) (for-each xs k))))) + + ; Yield each integer in [lo, hi) without building the list. + (define amb-range + (lambda (lo hi) + (shift (lambda (k) + (letrec ((loop (lambda (i) + (if (< i hi) (begin (k i) (loop (+ i 1))) #inert)))) + (loop lo)))))) + + ; Yield each x of xs satisfying ok?, with enter! applied before the + ; continuation runs and leave! after it has finished exploring. Use this + ; whenever a candidate has to be recorded in mutable state. + (define amb-bracket + (lambda (xs ok? enter! leave!) + (shift (lambda (k) + (for-each xs (lambda (x) + (if (ok? x) + (begin (enter! x) (k x) (leave! x)) + #inert))))))) + + ; amb-bracket over the integers in [lo, hi). + (define amb-bracket-range + (lambda (lo hi ok? enter! leave!) + (shift (lambda (k) + (letrec ((loop (lambda (i) + (if (< i hi) + (begin + (if (ok? i) + (begin (enter! i) (k i) (leave! i)) + #inert) + (loop (+ i 1))) + #inert)))) + (loop lo)))))) + + ; --- reporting a solution ------------------------------------------------ + + (define emit (lambda (s) ((vector-ref sink 0) s))) + + ; --- strategies ---------------------------------------------------------- + + ; Run body with an arbitrary handler applied to every solution. + (define search + (vau (handler & body) env + (with-sink (eval env handler) + (lambda () (eval env (cons sequence body)))) + #inert)) + + ; Every solution, in the order found. + (define collect + (vau body env + (let ((acc (make-vector 1 ()))) + (with-sink + (lambda (s) (vector-set! acc 0 (cons s (vector-ref acc 0)))) + (lambda () (eval env (cons sequence body)))) + (list-reverse (vector-ref acc 0))))) + + ; How many solutions, retaining none of them. + (define count-of + (vau body env + (let ((n (make-vector 1 0))) + (with-sink + (lambda (s) (vector-set! n 0 (+ (vector-ref n 0) 1))) + (lambda () (eval env (cons sequence body)))) + (vector-ref n 0)))) + + ; The first solution, or () if there is none. Escapes through call/cc, so + ; the rest of the search tree is never explored. The handler is restored on + ; both paths. + (define first-of + (vau body env + (let ((saved (vector-ref sink 0))) + (let ((found + (call/cc (lambda (return) + (vector-set! sink 0 (lambda (s) (return s))) + (reset (eval env (cons sequence body))) + ())))) + (vector-set! sink 0 saved) + found))))) diff --git a/lib/IronKernel.Amb/test/amb_test.ikr b/lib/IronKernel.Amb/test/amb_test.ikr new file mode 100644 index 0000000..18d510a --- /dev/null +++ b/lib/IronKernel.Amb/test/amb_test.ikr @@ -0,0 +1,153 @@ +; Tests for IronKernel.Amb. +; +; `ik test` loads src/ then this file, and counts the file as failing if +; evaluating it raises. Failures are tallied so that every check runs, then the +; last form references an unbound name to fail the run and point at the tally. + +(define failures (make-vector 1 0)) + +(defn (check name ok) + (if ok + (printf " ok {0}\n" name) + (begin + (printf " FAIL {0}\n" name) + (vector-set! failures 0 (+ (vector-ref failures 0) 1))))) + +(defn (list-equal? xs ys) + (if (null? xs) + (null? ys) + (if (null? ys) #f + (if (eq? (car xs) (car ys)) (list-equal? (cdr xs) (cdr ys)) #f)))) + +; --- choice points ---------------------------------------------------------- + +(check "amb enumerates a list" + (list-equal? (collect (emit (amb (list 1 2 3)))) (list 1 2 3))) + +(check "amb over () fails" + (null? (collect (emit (amb ()))))) + +(check "nested amb takes the cross product" + (eq? 4 (length (collect (let ((a (amb (list 1 2)))) + (let ((b (amb (list 10 20)))) + (emit (cons a b)))))))) + +(check "amb-range enumerates a half-open interval" + (list-equal? (collect (emit (amb-range 2 5))) (list 2 3 4))) + +(check "require prunes a branch" + (list-equal? (collect (let ((a (amb-range 0 10))) + (require (< a 3)) + (emit a))) + (list 0 1 2))) + +(check "fail abandons a branch" + (list-equal? (collect (let ((a (amb (list 1 2 3)))) + (if (eq? a 2) (fail) #inert) + (emit a))) + (list 1 3))) + +; --- strategies ------------------------------------------------------------- + +(check "count-of tallies solutions" + (eq? 4 (count-of (emit (amb-range 0 4))))) + +(check "first-of returns the first solution" + (eq? 6 (first-of (let ((a (amb (list 5 6 7)))) + (require (> a 5)) + (emit a))))) + +(check "first-of returns () when there is none" + (null? (first-of (let ((a (amb (list 1 2)))) (fail) (emit a))))) + +(check "search accepts a custom handler" + (let ((total (make-vector 1 0))) + (search (lambda (s) (vector-set! total 0 (+ (vector-ref total 0) s))) + (emit (amb-range 1 5))) + (eq? 10 (vector-ref total 0)))) + +(check "emit outside a strategy is a no-op" + (begin (emit 'ignored) #t)) + +(check "strategies nest" + (list-equal? (collect (let ((a (amb-range 0 3))) + (emit (count-of (emit (amb-range 0 a)))))) + (list 0 1 2))) + +; --- bracketed choice ------------------------------------------------------- + +(define st (make-vector 1 0)) + +(defn (bump v) (vector-set! st 0 (+ (vector-ref st 0) v))) +(defn (drop v) (vector-set! st 0 (- (vector-ref st 0) v))) + +(check "amb-bracket exposes state to the continuation" + (list-equal? (collect (let ((x (amb-bracket (list 1 2 3) + (lambda (v) #t) bump drop))) + (emit (vector-ref st 0)))) + (list 1 2 3))) + +(check "amb-bracket restores state afterwards" + (zero? (vector-ref st 0))) + +(check "amb-bracket honours its guard" + (list-equal? (collect (let ((x (amb-bracket (list 1 2 3 4) + (lambda (v) (< v 3)) bump drop))) + (emit x))) + (list 1 2))) + +(check "amb-bracket-range brackets nested choices" + (let ((seen (collect (let ((a (amb-bracket-range 1 4 + (lambda (v) #t) bump drop))) + (let ((b (amb-bracket-range 1 4 + (lambda (v) (> v a)) bump drop))) + (emit (vector-ref st 0))))))) + ; a+b over 1<=a