mk: phase 5C — nafc, negation as finite failure

(nafc g) is a three-line primitive: peek the goal's stream for one
answer; if empty, yield (unit s); else mzero. Carries the standard
miniKanren caveats — open-world unsound, diverges on infinite streams.

7 tests: failed-goal-succeeds, successful-goal-fails, double-negation,
conde-all-fail-makes-nafc-succeed, conde-any-success-makes-nafc-fail,
nafc as a guard accepting and blocking.

201/201 cumulative.

lib/apl/parser.sx

@@ -25,9 +25,8 @@
 ; Glyph classification sets
 ; ============================================================
 
-(define
-  apl-parse-op-glyphs
-  (list "/" "⌿" "\\" "⍀" "¨" "⍨" "∘" "." "⍣" "⍤" "⍥" "@"))
+(define apl-parse-op-glyphs
+  (list "/" "\\" "¨" "⍨" "∘" "." "⍣" "⍤" "⍥" "@"))
 
 (define
   apl-parse-fn-glyphs
@@ -83,48 +82,22 @@
     "⍎"
     "⍕"))
 
-(define apl-quad-fn-names (list "⎕FMT" "⎕←"))
+(define apl-quad-fn-names (list "⎕FMT"))
 
-(define apl-known-fn-names (list))
+(define
+  apl-parse-op-glyph?
+  (fn (v) (some (fn (g) (= g v)) apl-parse-op-glyphs)))
 
 ; ============================================================
 ; Token accessors
 ; ============================================================
 
-(define
-  apl-collect-fn-bindings
-  (fn
-    (stmt-groups)
-    (set! apl-known-fn-names (list))
-    (for-each
-      (fn
-        (toks)
-        (when
-          (and
-            (>= (len toks) 3)
-            (= (tok-type (nth toks 0)) :name)
-            (= (tok-type (nth toks 1)) :assign)
-            (= (tok-type (nth toks 2)) :lbrace))
-          (set!
-            apl-known-fn-names
-            (cons (tok-val (nth toks 0)) apl-known-fn-names))))
-      stmt-groups)))
-
-(define
-  apl-parse-op-glyph?
-  (fn (v) (some (fn (g) (= g v)) apl-parse-op-glyphs)))
-
 (define
   apl-parse-fn-glyph?
   (fn (v) (some (fn (g) (= g v)) apl-parse-fn-glyphs)))
 
 (define tok-type (fn (tok) (get tok :type)))
 
-; ============================================================
-; Collect trailing operators starting at index i
-; Returns {:ops (op ...) :end new-i}
-; ============================================================
-
 (define tok-val (fn (tok) (get tok :value)))
 
 (define
@@ -134,8 +107,8 @@
     (and (= (tok-type tok) :glyph) (apl-parse-op-glyph? (tok-val tok)))))
 
 ; ============================================================
-; Build a derived-fn node by chaining operators left-to-right
-; (+/¨  →  (:derived-fn "¨" (:derived-fn "/" (:fn-glyph "+"))))
+; Collect trailing operators starting at index i
+; Returns {:ops (op ...) :end new-i}
 ; ============================================================
 
 (define
@@ -146,17 +119,15 @@
       (and (= (tok-type tok) :glyph) (apl-parse-fn-glyph? (tok-val tok)))
       (and
         (= (tok-type tok) :name)
-        (or
-          (some (fn (q) (= q (tok-val tok))) apl-quad-fn-names)
-          (some (fn (q) (= q (tok-val tok))) apl-known-fn-names))))))
-
-; ============================================================
-; Find matching close bracket/paren/brace
-; Returns the index of the matching close token
-; ============================================================
+        (some (fn (q) (= q (tok-val tok))) apl-quad-fn-names)))))
 
 (define collect-ops (fn (tokens i) (collect-ops-loop tokens i (list))))
 
+; ============================================================
+; Build a derived-fn node by chaining operators left-to-right
+; (+/¨  →  (:derived-fn "¨" (:derived-fn "/" (:fn-glyph "+"))))
+; ============================================================
+
 (define
   collect-ops-loop
   (fn
@@ -172,10 +143,8 @@
           {:end i :ops acc})))))
 
 ; ============================================================
-; Segment collection: scan tokens left-to-right, building
-; a list of {:kind "val"/"fn" :node ast} segments.
-; Operators following function glyphs are merged into
-; derived-fn nodes during this pass.
+; Find matching close bracket/paren/brace
+; Returns the index of the matching close token
 ; ============================================================
 
 (define
@@ -194,20 +163,12 @@
     (find-matching-close-loop tokens start open-type close-type 1)))
 
 ; ============================================================
-; Build tree from segment list
-;
-; The segments are in left-to-right order.
-; APL evaluates right-to-left, so the LEFTMOST function is
-; the outermost (last-evaluated) node.
-;
-; Patterns:
-;   [val]              → val node
-;   [fn val ...]       → (:monad fn (build-tree rest))
-;   [val fn val ...]   → (:dyad fn val (build-tree rest))
-;   [val val ...]      → (:vec val1 val2 ...) — strand
+; Segment collection: scan tokens left-to-right, building
+; a list of {:kind "val"/"fn" :node ast} segments.
+; Operators following function glyphs are merged into
+; derived-fn nodes during this pass.
 ; ============================================================
 
-; Find the index of the first function segment (returns -1 if none)
 (define
   find-matching-close-loop
   (fn
@@ -247,9 +208,21 @@
   collect-segments
   (fn (tokens) (collect-segments-loop tokens 0 (list))))
 
-; Build an array node from 0..n value segments
-; If n=1 → return that segment's node
-; If n>1 → return (:vec node1 node2 ...)
+; ============================================================
+; Build tree from segment list
+;
+; The segments are in left-to-right order.
+; APL evaluates right-to-left, so the LEFTMOST function is
+; the outermost (last-evaluated) node.
+;
+; Patterns:
+;   [val]              → val node
+;   [fn val ...]       → (:monad fn (build-tree rest))
+;   [val fn val ...]   → (:dyad fn val (build-tree rest))
+;   [val val ...]      → (:vec val1 val2 ...) — strand
+; ============================================================
+
+; Find the index of the first function segment (returns -1 if none)
 (define
   collect-segments-loop
   (fn
@@ -269,38 +242,24 @@
             ((= tt :str)
               (collect-segments-loop tokens (+ i 1) (append acc {:kind "val" :node (list :str tv)})))
             ((= tt :name)
-              (cond
-                ((some (fn (q) (= q tv)) apl-quad-fn-names)
+              (if
+                (some (fn (q) (= q tv)) apl-quad-fn-names)
+                (let
+                  ((op-result (collect-ops tokens (+ i 1))))
                   (let
-                    ((op-result (collect-ops tokens (+ i 1))))
+                    ((ops (get op-result :ops)) (ni (get op-result :end)))
                     (let
-                      ((ops (get op-result :ops))
-                        (ni (get op-result :end)))
-                      (let
-                        ((fn-node (build-derived-fn (list :fn-glyph tv) ops)))
-                        (collect-segments-loop
-                          tokens
-                          ni
-                          (append acc {:kind "fn" :node fn-node}))))))
-                ((some (fn (q) (= q tv)) apl-known-fn-names)
-                  (let
-                    ((op-result (collect-ops tokens (+ i 1))))
-                    (let
-                      ((ops (get op-result :ops))
-                        (ni (get op-result :end)))
-                      (let
-                        ((fn-node (build-derived-fn (list :fn-name tv) ops)))
-                        (collect-segments-loop
-                          tokens
-                          ni
-                          (append acc {:kind "fn" :node fn-node}))))))
-                (else
-                  (let
-                    ((br (maybe-bracket (list :name tv) tokens (+ i 1))))
-                    (collect-segments-loop
-                      tokens
-                      (nth br 1)
-                      (append acc {:kind "val" :node (nth br 0)}))))))
+                      ((fn-node (build-derived-fn (list :fn-glyph tv) ops)))
+                      (collect-segments-loop
+                        tokens
+                        ni
+                        (append acc {:kind "fn" :node fn-node})))))
+                (let
+                  ((br (maybe-bracket (list :name tv) tokens (+ i 1))))
+                  (collect-segments-loop
+                    tokens
+                    (nth br 1)
+                    (append acc {:kind "val" :node (nth br 0)})))))
             ((= tt :lparen)
               (let
                 ((end (find-matching-close tokens (+ i 1) :lparen :rparen)))
@@ -308,23 +267,11 @@
                   ((inner-tokens (slice tokens (+ i 1) end))
                     (after (+ end 1)))
                   (let
-                    ((inner-segs (collect-segments inner-tokens)))
-                    (if
-                      (and
-                        (>= (len inner-segs) 2)
-                        (every? (fn (s) (= (get s :kind) "fn")) inner-segs))
-                      (let
-                        ((train-node (cons :train (map (fn (s) (get s :node)) inner-segs))))
-                        (collect-segments-loop
-                          tokens
-                          after
-                          (append acc {:kind "fn" :node train-node})))
-                      (let
-                        ((br (maybe-bracket (parse-apl-expr inner-tokens) tokens after)))
-                        (collect-segments-loop
-                          tokens
-                          (nth br 1)
-                          (append acc {:kind "val" :node (nth br 0)}))))))))
+                    ((br (maybe-bracket (parse-apl-expr inner-tokens) tokens after)))
+                    (collect-segments-loop
+                      tokens
+                      (nth br 1)
+                      (append acc {:kind "val" :node (nth br 0)}))))))
             ((= tt :lbrace)
               (let
                 ((end (find-matching-close tokens (+ i 1) :lbrace :rbrace)))
@@ -399,12 +346,9 @@
 
 (define find-first-fn (fn (segs) (find-first-fn-loop segs 0)))
 
-
-; ============================================================
-; Split token list on statement separators (diamond / newline)
-; Only splits at depth 0 (ignores separators inside { } or ( ) )
-; ============================================================
-
+; Build an array node from 0..n value segments
+; If n=1 → return that segment's node
+; If n>1 → return (:vec node1 node2 ...)
 (define
   find-first-fn-loop
   (fn
@@ -426,9 +370,10 @@
       (get (first segs) :node)
       (cons :vec (map (fn (s) (get s :node)) segs)))))
 
+
 ; ============================================================
-; Parse a dfn body (tokens between { and })
-; Handles guard expressions: cond : expr
+; Split token list on statement separators (diamond / newline)
+; Only splits at depth 0 (ignores separators inside { } or ( ) )
 ; ============================================================
 
 (define
@@ -463,6 +408,11 @@
   split-statements
   (fn (tokens) (split-statements-loop tokens (list) (list) 0)))
 
+; ============================================================
+; Parse a dfn body (tokens between { and })
+; Handles guard expressions: cond : expr
+; ============================================================
+
 (define
   split-statements-loop
   (fn
@@ -517,10 +467,6 @@
       ((stmt-groups (split-statements tokens)))
       (let ((stmts (map parse-dfn-stmt stmt-groups))) (cons :dfn stmts)))))
 
-; ============================================================
-; Parse a single statement (assignment or expression)
-; ============================================================
-
 (define
   parse-dfn-stmt
   (fn
@@ -537,17 +483,12 @@
             (parse-apl-expr body-tokens)))
         (parse-stmt tokens)))))
 
-; ============================================================
-; Parse an expression from a flat token list
-; ============================================================
-
 (define
   find-top-level-colon
   (fn (tokens i) (find-top-level-colon-loop tokens i 0)))
 
 ; ============================================================
-; Main entry point
-; parse-apl: string → AST
+; Parse a single statement (assignment or expression)
 ; ============================================================
 
 (define
@@ -567,6 +508,10 @@
           ((and (= tt :colon) (= depth 0)) i)
           (true (find-top-level-colon-loop tokens (+ i 1) depth)))))))
 
+; ============================================================
+; Parse an expression from a flat token list
+; ============================================================
+
 (define
   parse-stmt
   (fn
@@ -581,6 +526,11 @@
         (parse-apl-expr (slice tokens 2)))
       (parse-apl-expr tokens))))
 
+; ============================================================
+; Main entry point
+; parse-apl: string → AST
+; ============================================================
+
 (define
   parse-apl-expr
   (fn
@@ -597,52 +547,13 @@
       ((tokens (apl-tokenize src)))
       (let
         ((stmt-groups (split-statements tokens)))
-        (begin
-          (apl-collect-fn-bindings stmt-groups)
+        (if
+          (= (len stmt-groups) 0)
+          nil
           (if
-            (= (len stmt-groups) 0)
-            nil
-            (if
-              (= (len stmt-groups) 1)
-              (parse-stmt (first stmt-groups))
-              (cons :program (map parse-stmt stmt-groups)))))))))
-
-(define
-  split-bracket-loop
-  (fn
-    (tokens current acc depth)
-    (if
-      (= (len tokens) 0)
-      (append acc (list current))
-      (let
-        ((tok (first tokens)) (more (rest tokens)))
-        (let
-          ((tt (tok-type tok)))
-          (cond
-            ((or (= tt :lparen) (= tt :lbrace) (= tt :lbracket))
-              (split-bracket-loop
-                more
-                (append current (list tok))
-                acc
-                (+ depth 1)))
-            ((or (= tt :rparen) (= tt :rbrace) (= tt :rbracket))
-              (split-bracket-loop
-                more
-                (append current (list tok))
-                acc
-                (- depth 1)))
-            ((and (= tt :semi) (= depth 0))
-              (split-bracket-loop
-                more
-                (list)
-                (append acc (list current))
-                depth))
-            (else
-              (split-bracket-loop more (append current (list tok)) acc depth))))))))
-
-(define
-  split-bracket-content
-  (fn (tokens) (split-bracket-loop tokens (list) (list) 0)))
+            (= (len stmt-groups) 1)
+            (parse-stmt (first stmt-groups))
+            (cons :program (map parse-stmt stmt-groups))))))))
 
 (define
   maybe-bracket
@@ -658,17 +569,8 @@
           ((inner-tokens (slice tokens (+ after 1) end))
             (next-after (+ end 1)))
           (let
-            ((sections (split-bracket-content inner-tokens)))
-            (if
-              (= (len sections) 1)
-              (let
-                ((idx-expr (parse-apl-expr inner-tokens)))
-                (let
-                  ((indexed (list :dyad (list :fn-glyph "⌷") idx-expr val-node)))
-                  (maybe-bracket indexed tokens next-after)))
-              (let
-                ((axis-exprs (map (fn (toks) (if (= (len toks) 0) :all (parse-apl-expr toks))) sections)))
-                (let
-                  ((indexed (cons :bracket (cons val-node axis-exprs))))
-                  (maybe-bracket indexed tokens next-after)))))))
+            ((idx-expr (parse-apl-expr inner-tokens)))
+            (let
+              ((indexed (list :dyad (list :fn-glyph "⌷") idx-expr val-node)))
+              (maybe-bracket indexed tokens next-after)))))
       (list val-node after))))

lib/apl/runtime.sx

@@ -883,7 +883,7 @@
       (let
         ((sub (apl-permutations (- n 1))))
         (reduce
-          (fn (acc p) (append (apl-insert-everywhere n p) acc))
+          (fn (acc p) (append acc (apl-insert-everywhere n p)))
           (list)
           sub)))))
 
@@ -985,38 +985,6 @@
         (some (fn (c) (= c 0)) codes)
         (some (fn (c) (= c (nth e 1))) codes)))))
 
-(define
-  apl-cartesian
-  (fn
-    (lists)
-    (if
-      (= (len lists) 0)
-      (list (list))
-      (let
-        ((rest-prods (apl-cartesian (rest lists))))
-        (reduce
-          (fn (acc x) (append acc (map (fn (p) (cons x p)) rest-prods)))
-          (list)
-          (first lists))))))
-
-(define
-  apl-bracket-multi
-  (fn
-    (axes arr)
-    (let
-      ((shape (get arr :shape)) (ravel (get arr :ravel)))
-      (let
-        ((rank (len shape)) (strides (apl-strides shape)))
-        (let
-          ((axis-info (map (fn (i) (let ((a (nth axes i))) (cond ((= a nil) {:idxs (range 0 (nth shape i)) :scalar? false}) ((= (len (get a :shape)) 0) {:idxs (list (- (first (get a :ravel)) apl-io)) :scalar? true}) (else {:idxs (map (fn (x) (- x apl-io)) (get a :ravel)) :scalar? false})))) (range 0 rank))))
-          (let
-            ((cells (apl-cartesian (map (fn (a) (get a :idxs)) axis-info))))
-            (let
-              ((result-ravel (map (fn (cell) (let ((flat (reduce + 0 (map (fn (i) (* (nth cell i) (nth strides i))) (range 0 rank))))) (nth ravel flat))) cells)))
-              (let
-                ((result-shape (filter (fn (x) (>= x 0)) (map (fn (i) (let ((a (nth axis-info i))) (if (get a :scalar?) -1 (len (get a :idxs))))) (range 0 rank)))))
-                (make-array result-shape result-ravel)))))))))
-
 (define
   apl-reduce
   (fn

lib/apl/test.sh

@@ -39,7 +39,6 @@ cat > "$TMPFILE" << 'EPOCHS'
 (load "lib/apl/tests/idioms.sx")
 (load "lib/apl/tests/eval-ops.sx")
 (load "lib/apl/tests/pipeline.sx")
-(load "lib/apl/tests/programs-e2e.sx")
 (epoch 4)
 (eval "(list apl-test-pass apl-test-fail)")
 EPOCHS

lib/apl/tests/pipeline.sx

@@ -178,137 +178,3 @@
   "apl-run \"(⍳5)[3] × 7\" → 21"
   (mkrv (apl-run "(⍳5)[3] × 7"))
   (list 21))
-
-(apl-test "decimal: 3.7 → 3.7" (mkrv (apl-run "3.7")) (list 3.7))
-
-(apl-test "decimal: ¯2.5 → -2.5" (mkrv (apl-run "¯2.5")) (list -2.5))
-
-(apl-test "decimal: 1.5 + 2.5 → 4" (mkrv (apl-run "1.5 + 2.5")) (list 4))
-
-(apl-test "decimal: ⌊3.7 → 3" (mkrv (apl-run "⌊ 3.7")) (list 3))
-
-(apl-test "decimal: ⌈3.7 → 4" (mkrv (apl-run "⌈ 3.7")) (list 4))
-
-(apl-test
-  "⎕← scalar passthrough"
-  (mkrv (apl-run "⎕← 42"))
-  (list 42))
-
-(apl-test
-  "⎕← vector passthrough"
-  (mkrv (apl-run "⎕← 1 2 3"))
-  (list 1 2 3))
-
-(apl-test
-  "string: 'abc' → 3-char vector"
-  (mkrv (apl-run "'abc'"))
-  (list "a" "b" "c"))
-
-(apl-test "string: 'a' is rank-0 scalar" (mksh (apl-run "'a'")) (list))
-
-(apl-test "string: 'hello' shape (5)" (mksh (apl-run "'hello'")) (list 5))
-
-(apl-test
-  "named-fn: f ← {⍺+⍵} ⋄ 3 f 4 → 7"
-  (mkrv (apl-run "f ← {⍺+⍵} ⋄ 3 f 4"))
-  (list 7))
-
-(apl-test
-  "named-fn monadic: sq ← {⍵×⍵} ⋄ sq 7 → 49"
-  (mkrv (apl-run "sq ← {⍵×⍵} ⋄ sq 7"))
-  (list 49))
-
-(apl-test
-  "named-fn dyadic: hyp ← {((⍺×⍺)+⍵×⍵)} ⋄ 3 hyp 4 → 25"
-  (mkrv (apl-run "hyp ← {((⍺×⍺)+⍵×⍵)} ⋄ 3 hyp 4"))
-  (list 25))
-
-(apl-test
-  "named-fn: dbl ← {⍵+⍵} ⋄ dbl ⍳5"
-  (mkrv (apl-run "dbl ← {⍵+⍵} ⋄ dbl ⍳5"))
-  (list 2 4 6 8 10))
-
-(apl-test
-  "named-fn factorial via ∇ recursion"
-  (mkrv (apl-run "fact ← {0=⍵:1 ⋄ ⍵×∇⍵-1} ⋄ fact 5"))
-  (list 120))
-
-(apl-test
-  "named-fn used twice in expr: dbl ← {⍵+⍵} ⋄ (dbl 3) + dbl 4"
-  (mkrv (apl-run "dbl ← {⍵+⍵} ⋄ (dbl 3) + dbl 4"))
-  (list 14))
-
-(apl-test
-  "named-fn with vector arg: neg ← {-⍵} ⋄ neg 1 2 3"
-  (mkrv (apl-run "neg ← {-⍵} ⋄ neg 1 2 3"))
-  (list -1 -2 -3))
-
-(apl-test
-  "multi-axis: M[2;2] → center"
-  (mkrv (apl-run "M ← (3 3) ⍴ ⍳9 ⋄ M[2;2]"))
-  (list 5))
-
-(apl-test
-  "multi-axis: M[1;] → first row"
-  (mkrv (apl-run "M ← (3 3) ⍴ ⍳9 ⋄ M[1;]"))
-  (list 1 2 3))
-
-(apl-test
-  "multi-axis: M[;2] → second column"
-  (mkrv (apl-run "M ← (3 3) ⍴ ⍳9 ⋄ M[;2]"))
-  (list 2 5 8))
-
-(apl-test
-  "multi-axis: M[1 2;1 2] → 2x2 block"
-  (mkrv (apl-run "M ← (2 3) ⍴ ⍳6 ⋄ M[1 2;1 2]"))
-  (list 1 2 4 5))
-
-(apl-test
-  "multi-axis: M[1 2;1 2] shape (2 2)"
-  (mksh (apl-run "M ← (2 3) ⍴ ⍳6 ⋄ M[1 2;1 2]"))
-  (list 2 2))
-
-(apl-test
-  "multi-axis: M[;] full matrix"
-  (mkrv (apl-run "M ← (2 2) ⍴ 10 20 30 40 ⋄ M[;]"))
-  (list 10 20 30 40))
-
-(apl-test
-  "multi-axis: M[1;] shape collapsed"
-  (mksh (apl-run "M ← (3 3) ⍴ ⍳9 ⋄ M[1;]"))
-  (list 3))
-
-(apl-test
-  "multi-axis: select all rows of column 3"
-  (mkrv (apl-run "M ← (4 3) ⍴ 1 2 3 4 5 6 7 8 9 10 11 12 ⋄ M[;3]"))
-  (list 3 6 9 12))
-
-(apl-test
-  "train: mean = (+/÷≢) on 1..5"
-  (mkrv (apl-run "(+/÷≢) 1 2 3 4 5"))
-  (list 3))
-
-(apl-test
-  "train: mean of 2 4 6 8 10"
-  (mkrv (apl-run "(+/÷≢) 2 4 6 8 10"))
-  (list 6))
-
-(apl-test
-  "train 2-atop: (- ⌊) 5 → -5"
-  (mkrv (apl-run "(- ⌊) 5"))
-  (list -5))
-
-(apl-test
-  "train 3-fork dyadic: 2(+×-)5 → -21"
-  (mkrv (apl-run "2 (+ × -) 5"))
-  (list -21))
-
-(apl-test
-  "train: range = (⌈/-⌊/) on vector"
-  (mkrv (apl-run "(⌈/-⌊/) 3 1 4 1 5 9 2 6"))
-  (list 8))
-
-(apl-test
-  "train: mean of ⍳10 has shape ()"
-  (mksh (apl-run "(+/÷≢) ⍳10"))
-  (list))

lib/apl/tests/programs-e2e.sx

@@ -1,96 +0,0 @@
-; End-to-end tests of the classic-program archetypes — running APL
-; source through the full pipeline (tokenize → parse → eval-ast → runtime).
-;
-; These mirror the algorithms documented in lib/apl/tests/programs/*.apl
-; but use forms our pipeline supports today (named functions instead of
-; the inline ⍵← rebinding idiom; multi-stmt over single one-liners).
-
-(define mkrv (fn (arr) (get arr :ravel)))
-(define mksh (fn (arr) (get arr :shape)))
-
-; ---------- factorial via ∇ recursion (cf. n-queens style) ----------
-
-(apl-test
-  "e2e: factorial 5! = 120"
-  (mkrv (apl-run "fact ← {0=⍵:1 ⋄ ⍵×∇⍵-1} ⋄ fact 5"))
-  (list 120))
-
-(apl-test
-  "e2e: factorial 7! = 5040"
-  (mkrv (apl-run "fact ← {0=⍵:1 ⋄ ⍵×∇⍵-1} ⋄ fact 7"))
-  (list 5040))
-
-(apl-test
-  "e2e: factorial via ×/⍳N (no recursion)"
-  (mkrv (apl-run "fact ← {×/⍳⍵} ⋄ fact 6"))
-  (list 720))
-
-; ---------- sum / triangular numbers (sum-1..N) ----------
-
-(apl-test
-  "e2e: triangular(10) = 55"
-  (mkrv (apl-run "tri ← {+/⍳⍵} ⋄ tri 10"))
-  (list 55))
-
-(apl-test
-  "e2e: triangular(100) = 5050"
-  (mkrv (apl-run "tri ← {+/⍳⍵} ⋄ tri 100"))
-  (list 5050))
-
-; ---------- sum of squares ----------
-
-(apl-test
-  "e2e: sum-of-squares 1..5 = 55"
-  (mkrv (apl-run "ss ← {+/⍵×⍵} ⋄ ss ⍳5"))
-  (list 55))
-
-(apl-test
-  "e2e: sum-of-squares 1..10 = 385"
-  (mkrv (apl-run "ss ← {+/⍵×⍵} ⋄ ss ⍳10"))
-  (list 385))
-
-; ---------- divisor-counting (prime-sieve building blocks) ----------
-
-(apl-test
-  "e2e: divisor counts 1..5 via outer mod"
-  (mkrv (apl-run "P ← ⍳ 5 ⋄ +⌿ 0 = P ∘.| P"))
-  (list 1 2 2 3 2))
-
-(apl-test
-  "e2e: divisor counts 1..10"
-  (mkrv (apl-run "P ← ⍳ 10 ⋄ +⌿ 0 = P ∘.| P"))
-  (list 1 2 2 3 2 4 2 4 3 4))
-
-(apl-test
-  "e2e: prime-mask 1..10 (count==2)"
-  (mkrv (apl-run "P ← ⍳ 10 ⋄ 2 = +⌿ 0 = P ∘.| P"))
-  (list 0 1 1 0 1 0 1 0 0 0))
-
-; ---------- monadic primitives chained ----------
-
-(apl-test
-  "e2e: sum of |abs| = 15"
-  (mkrv (apl-run "+/|¯1 ¯2 ¯3 ¯4 ¯5"))
-  (list 15))
-
-(apl-test
-  "e2e: max of squares 1..6"
-  (mkrv (apl-run "⌈/(⍳6)×⍳6"))
-  (list 36))
-
-; ---------- nested named functions ----------
-
-(apl-test
-  "e2e: compose dbl and sq via two named fns"
-  (mkrv (apl-run "dbl ← {⍵+⍵} ⋄ sq ← {⍵×⍵} ⋄ sq dbl 3"))
-  (list 36))
-
-(apl-test
-  "e2e: max-of-two as named dyadic fn"
-  (mkrv (apl-run "mx ← {⍺⌈⍵} ⋄ 5 mx 3"))
-  (list 5))
-
-(apl-test
-  "e2e: sqrt-via-newton 1 step from 1 → 2.5"
-  (mkrv (apl-run "step ← {(⍵+⍺÷⍵)÷2} ⋄ 4 step 1"))
-  (list 2.5))

lib/apl/tests/programs.sx

@@ -252,8 +252,6 @@
 
 (apl-test "queens 7 → 40 solutions" (mkrv (apl-queens 7)) (list 40))
 
-(apl-test "queens 8 → 92 solutions" (mkrv (apl-queens 8)) (list 92))
-
 (apl-test "permutations of 3 has 6" (len (apl-permutations 3)) 6)
 
 (apl-test "permutations of 4 has 24" (len (apl-permutations 4)) 24)

lib/apl/tokenizer.sx

@@ -2,7 +2,7 @@
   (list "+" "-" "×" "÷" "*" "⍟" "⌈" "⌊" "|" "!" "?" "○" "~" "<" "≤" "=" "≥" ">" "≠"
         "≢" "≡" "∊" "∧" "∨" "⍱" "⍲" "," "⍪" "⍴" "⌽" "⊖" "⍉" "↑" "↓" "⊂" "⊃" "⊆"
         "∪" "∩" "⍳" "⍸" "⌷" "⍋" "⍒" "⊥" "⊤" "⊣" "⊢" "⍎" "⍕"
-        "⍺" "⍵" "∇" "/" "⌿" "\\" "⍀" "¨" "⍨" "∘" "." "⍣" "⍤" "⍥" "@" "¯"))
+        "⍺" "⍵" "∇" "/" "\\" "¨" "⍨" "∘" "." "⍣" "⍤" "⍥" "@" "¯"))
 
 (define apl-glyph?
   (fn (ch)
@@ -138,22 +138,12 @@
                  (begin
                    (consume! "¯")
                    (let ((digits (read-digits! "")))
-                     (if (and (< pos src-len) (= (cur-byte) ".")
-                              (< (+ pos 1) src-len) (apl-digit? (nth source (+ pos 1))))
-                       (begin (advance!)
-                              (let ((frac (read-digits! "")))
-                                (tok-push! :num (- 0 (string->number (str digits "." frac))))))
-                       (tok-push! :num (- 0 (parse-int digits 0)))))
+                     (tok-push! :num (- 0 (parse-int digits 0))))
                    (scan!)))
                 ((apl-digit? ch)
                  (begin
                    (let ((digits (read-digits! "")))
-                     (if (and (< pos src-len) (= (cur-byte) ".")
-                              (< (+ pos 1) src-len) (apl-digit? (nth source (+ pos 1))))
-                       (begin (advance!)
-                              (let ((frac (read-digits! "")))
-                                (tok-push! :num (string->number (str digits "." frac)))))
-                       (tok-push! :num (parse-int digits 0))))
+                     (tok-push! :num (parse-int digits 0)))
                    (scan!)))
                 ((= ch "'")
                  (begin
@@ -165,9 +155,7 @@
                  (let ((start pos))
                    (begin
                      (if (cur-sw? "⎕") (consume! "⎕") (advance!))
-                     (if (and (< pos src-len) (cur-sw? "←"))
-                       (consume! "←")
-                       (read-ident-cont!))
+                     (read-ident-cont!)
                      (tok-push! :name (slice source start pos))
                      (scan!))))
                 (true

lib/apl/transpile.sx

@@ -40,7 +40,6 @@
       ((= g "⍋") apl-grade-up)
       ((= g "⍒") apl-grade-down)
       ((= g "⎕FMT") apl-quad-fmt)
-      ((= g "⎕←") apl-quad-print)
       (else (error "no monadic fn for glyph")))))
 
 (define
@@ -98,15 +97,6 @@
       ((tag (first node)))
       (cond
         ((= tag :num) (apl-scalar (nth node 1)))
-        ((= tag :str)
-          (let
-            ((s (nth node 1)))
-            (if
-              (= (len s) 1)
-              (apl-scalar s)
-              (make-array
-                (list (len s))
-                (map (fn (i) (slice s i (+ i 1))) (range 0 (len s)))))))
         ((= tag :vec)
           (let
             ((items (rest node)))
@@ -149,16 +139,6 @@
                 (apl-eval-ast rhs env)))))
         ((= tag :program) (apl-eval-stmts (rest node) env))
         ((= tag :dfn) node)
-        ((= tag :bracket)
-          (let
-            ((arr-expr (nth node 1)) (axis-exprs (rest (rest node))))
-            (let
-              ((arr (apl-eval-ast arr-expr env))
-                (axes
-                  (map
-                    (fn (a) (if (= a :all) nil (apl-eval-ast a env)))
-                    axis-exprs)))
-              (apl-bracket-multi axes arr))))
         (else (error (list "apl-eval-ast: unknown node tag" tag node)))))))
 
 (define
@@ -439,36 +419,6 @@
                   ((f (apl-resolve-dyadic inner env)))
                   (fn (arr) (apl-commute f arr))))
               (else (error "apl-resolve-monadic: unsupported op")))))
-        ((= tag :fn-name)
-          (let
-            ((nm (nth fn-node 1)))
-            (let
-              ((bound (get env nm)))
-              (if
-                (and
-                  (list? bound)
-                  (> (len bound) 0)
-                  (= (first bound) :dfn))
-                (fn (arg) (apl-call-dfn-m bound arg))
-                (error "apl-resolve-monadic: name not bound to dfn")))))
-        ((= tag :train)
-          (let
-            ((fns (rest fn-node)))
-            (let
-              ((n (len fns)))
-              (cond
-                ((= n 2)
-                  (let
-                    ((g (apl-resolve-monadic (nth fns 0) env))
-                      (h (apl-resolve-monadic (nth fns 1) env)))
-                    (fn (arg) (g (h arg)))))
-                ((= n 3)
-                  (let
-                    ((f (apl-resolve-monadic (nth fns 0) env))
-                      (g (apl-resolve-dyadic (nth fns 1) env))
-                      (h (apl-resolve-monadic (nth fns 2) env)))
-                    (fn (arg) (g (f arg) (h arg)))))
-                (else (error "monadic train arity not 2 or 3"))))))
         (else (error "apl-resolve-monadic: unknown fn-node tag"))))))
 
 (define
@@ -492,18 +442,6 @@
                   ((f (apl-resolve-dyadic inner env)))
                   (fn (a b) (apl-commute-dyadic f a b))))
               (else (error "apl-resolve-dyadic: unsupported op")))))
-        ((= tag :fn-name)
-          (let
-            ((nm (nth fn-node 1)))
-            (let
-              ((bound (get env nm)))
-              (if
-                (and
-                  (list? bound)
-                  (> (len bound) 0)
-                  (= (first bound) :dfn))
-                (fn (a b) (apl-call-dfn bound a b))
-                (error "apl-resolve-dyadic: name not bound to dfn")))))
         ((= tag :outer)
           (let
             ((inner (nth fn-node 2)))
@@ -517,24 +455,6 @@
               ((f (apl-resolve-dyadic f-node env))
                 (g (apl-resolve-dyadic g-node env)))
               (fn (a b) (apl-inner f g a b)))))
-        ((= tag :train)
-          (let
-            ((fns (rest fn-node)))
-            (let
-              ((n (len fns)))
-              (cond
-                ((= n 2)
-                  (let
-                    ((g (apl-resolve-monadic (nth fns 0) env))
-                      (h (apl-resolve-dyadic (nth fns 1) env)))
-                    (fn (a b) (g (h a b)))))
-                ((= n 3)
-                  (let
-                    ((f (apl-resolve-dyadic (nth fns 0) env))
-                      (g (apl-resolve-dyadic (nth fns 1) env))
-                      (h (apl-resolve-dyadic (nth fns 2) env)))
-                    (fn (a b) (g (f a b) (h a b)))))
-                (else (error "dyadic train arity not 2 or 3"))))))
         (else (error "apl-resolve-dyadic: unknown fn-node tag"))))))
 
 (define apl-run (fn (src) (apl-eval-ast (parse-apl src) {})))

lib/datalog/builtins.sx

@@ -1,300 +0,0 @@
-;; lib/datalog/builtins.sx — comparison + arithmetic body literals.
-;;
-;; Built-in predicates filter / extend candidate substitutions during
-;; rule evaluation. They are not stored facts and do not participate in
-;; the Herbrand base.
-;;
-;;   (< a b)  (<= a b)  (> a b)  (>= a b)   ; numeric (or string) compare
-;;   (= a b)                                  ; unify (binds vars)
-;;   (!= a b)                                ; ground-only inequality
-;;   (is X expr)                              ; bind X to expr's value
-;;
-;; Arithmetic expressions are SX-list compounds:
-;;   (+ a b)  (- a b)  (* a b)  (/ a b)
-;; or numbers / variables (must be bound at evaluation time).
-
-(define
-  dl-comparison?
-  (fn
-    (lit)
-    (and
-      (list? lit)
-      (> (len lit) 0)
-      (let
-        ((rel (dl-rel-name lit)))
-        (cond
-          ((nil? rel) false)
-          (else (dl-member-string? rel (list "<" "<=" ">" ">=" "!="))))))))
-
-(define
-  dl-eq?
-  (fn
-    (lit)
-    (and
-      (list? lit)
-      (> (len lit) 0)
-      (let ((rel (dl-rel-name lit))) (and (not (nil? rel)) (= rel "=")))))) 
-
-(define
-  dl-is?
-  (fn
-    (lit)
-    (and
-      (list? lit)
-      (> (len lit) 0)
-      (let
-        ((rel (dl-rel-name lit)))
-        (and (not (nil? rel)) (= rel "is")))))) 
-
-;; Evaluate an arithmetic expression under subst. Returns the numeric
-;; result, or raises if any operand is unbound or non-numeric.
-(define
-  dl-eval-arith
-  (fn
-    (expr subst)
-    (let
-      ((w (dl-walk expr subst)))
-      (cond
-        ((number? w) w)
-        ((dl-var? w)
-          (error (str "datalog arith: unbound variable " (symbol->string w))))
-        ((list? w)
-          (let
-            ((rel (dl-rel-name w)) (args (rest w)))
-            (cond
-              ((not (= (len args) 2))
-                (error (str "datalog arith: need 2 args, got " w)))
-              (else
-                (let
-                  ((a (dl-eval-arith (first args) subst))
-                    (b (dl-eval-arith (nth args 1) subst)))
-                  (cond
-                    ((= rel "+") (+ a b))
-                    ((= rel "-") (- a b))
-                    ((= rel "*") (* a b))
-                    ((= rel "/") (/ a b))
-                    (else (error (str "datalog arith: unknown op " rel)))))))))
-        (else (error (str "datalog arith: not a number — " w)))))))
-
-(define
-  dl-eval-compare
-  (fn
-    (lit subst)
-    (let
-      ((rel (dl-rel-name lit))
-        (a (dl-walk (nth lit 1) subst))
-        (b (dl-walk (nth lit 2) subst)))
-      (cond
-        ((or (dl-var? a) (dl-var? b))
-          (error
-            (str
-              "datalog: comparison "
-              rel
-              " has unbound argument; "
-              "ensure prior body literal binds the variable")))
-        (else
-          (let
-            ((ok (cond ((= rel "<") (< a b)) ((= rel "<=") (<= a b)) ((= rel ">") (> a b)) ((= rel ">=") (>= a b)) ((= rel "!=") (not (dl-tuple-equal? a b))) (else (error (str "datalog: unknown compare " rel))))))
-            (if ok subst nil)))))))
-
-(define
-  dl-eval-eq
-  (fn
-    (lit subst)
-    (dl-unify (nth lit 1) (nth lit 2) subst)))
-
-(define
-  dl-eval-is
-  (fn
-    (lit subst)
-    (let
-      ((target (nth lit 1)) (expr (nth lit 2)))
-      (let
-        ((value (dl-eval-arith expr subst)))
-        (dl-unify target value subst)))))
-
-(define
-  dl-eval-builtin
-  (fn
-    (lit subst)
-    (cond
-      ((dl-comparison? lit) (dl-eval-compare lit subst))
-      ((dl-eq? lit) (dl-eval-eq lit subst))
-      ((dl-is? lit) (dl-eval-is lit subst))
-      (else (error (str "dl-eval-builtin: not a built-in: " lit))))))
-
-;; ── Safety analysis ──────────────────────────────────────────────
-;;
-;; Walks body literals left-to-right tracking a "bound" set. The check
-;; understands these literal kinds:
-;;
-;;   positive non-built-in    → adds its vars to bound
-;;   (is X expr)              → vars(expr) ⊆ bound, then add X (if var)
-;;   <,<=,>,>=,!=             → all vars ⊆ bound (no binding)
-;;   (= a b) where:
-;;       both non-vars        → constraint check, no binding
-;;       a var, b not         → bind a
-;;       b var, a not         → bind b
-;;       both vars            → at least one in bound; bind the other
-;;   {:neg lit}               → all vars ⊆ bound (Phase 7 enforces fully)
-;;
-;; At end, head vars (minus `_`) must be ⊆ bound.
-
-(define
-  dl-vars-not-in
-  (fn
-    (vs bound)
-    (let
-      ((out (list)))
-      (do
-        (for-each
-          (fn
-            (v)
-            (when (not (dl-member-string? v bound)) (append! out v)))
-          vs)
-        out))))
-
-(define
-  dl-rule-check-safety
-  (fn
-    (rule)
-    (let
-      ((head (get rule :head))
-        (body (get rule :body))
-        (bound (list))
-        (err nil))
-      (do
-        (define
-          dl-add-bound!
-          (fn
-            (vs)
-            (for-each
-              (fn
-                (v)
-                (when (not (dl-member-string? v bound)) (append! bound v)))
-              vs)))
-        (define
-          dl-process-eq!
-          (fn
-            (lit)
-            (let
-              ((a (nth lit 1)) (b (nth lit 2)))
-              (let
-                ((va (dl-var? a)) (vb (dl-var? b)))
-                (cond
-                  ((and (not va) (not vb)) nil)
-                  ((and va (not vb))
-                    (dl-add-bound! (list (symbol->string a))))
-                  ((and (not va) vb)
-                    (dl-add-bound! (list (symbol->string b))))
-                  (else
-                    (let
-                      ((sa (symbol->string a)) (sb (symbol->string b)))
-                      (cond
-                        ((dl-member-string? sa bound)
-                          (dl-add-bound! (list sb)))
-                        ((dl-member-string? sb bound)
-                          (dl-add-bound! (list sa)))
-                        (else
-                          (set!
-                            err
-                            (str
-                              "= between two unbound variables "
-                              (list sa sb)
-                              " — at least one must be bound by an "
-                              "earlier positive body literal")))))))))))
-        (define
-          dl-process-cmp!
-          (fn
-            (lit)
-            (let
-              ((needed (dl-vars-of (list (nth lit 1) (nth lit 2)))))
-              (let
-                ((missing (dl-vars-not-in needed bound)))
-                (when
-                  (> (len missing) 0)
-                  (set!
-                    err
-                    (str
-                      "comparison "
-                      (dl-rel-name lit)
-                      " requires bound variable(s) "
-                      missing
-                      " (must be bound by an earlier positive "
-                      "body literal)")))))))
-        (define
-          dl-process-is!
-          (fn
-            (lit)
-            (let
-              ((tgt (nth lit 1)) (expr (nth lit 2)))
-              (let
-                ((needed (dl-vars-of expr)))
-                (let
-                  ((missing (dl-vars-not-in needed bound)))
-                  (cond
-                    ((> (len missing) 0)
-                      (set!
-                        err
-                        (str
-                          "is RHS uses unbound variable(s) "
-                          missing
-                          " — bind them via a prior positive body "
-                          "literal")))
-                    (else
-                      (when
-                        (dl-var? tgt)
-                        (dl-add-bound! (list (symbol->string tgt)))))))))))
-        (define
-          dl-process-neg!
-          (fn
-            (lit)
-            (let
-              ((needed (dl-vars-of (get lit :neg))))
-              (let
-                ((missing (dl-vars-not-in needed bound)))
-                (when
-                  (> (len missing) 0)
-                  (set!
-                    err
-                    (str
-                      "negation refers to unbound variable(s) "
-                      missing
-                      " — they must be bound by an earlier "
-                      "positive body literal")))))))
-        (define
-          dl-process-lit!
-          (fn
-            (lit)
-            (when
-              (nil? err)
-              (cond
-                ((and (dict? lit) (has-key? lit :neg))
-                  (dl-process-neg! lit))
-                ((dl-eq? lit) (dl-process-eq! lit))
-                ((dl-is? lit) (dl-process-is! lit))
-                ((dl-comparison? lit) (dl-process-cmp! lit))
-                ((and (list? lit) (> (len lit) 0))
-                  (dl-add-bound! (dl-vars-of lit)))))))
-        (for-each dl-process-lit! body)
-        (when
-          (nil? err)
-          (let
-            ((head-vars (dl-vars-of head)) (missing (list)))
-            (do
-              (for-each
-                (fn
-                  (v)
-                  (when
-                    (and (not (dl-member-string? v bound)) (not (= v "_")))
-                    (append! missing v)))
-                head-vars)
-              (when
-                (> (len missing) 0)
-                (set!
-                  err
-                  (str
-                    "head variable(s) "
-                    missing
-                    " do not appear in any positive body literal"))))))
-        err))))

lib/datalog/conformance.conf

@@ -1,21 +0,0 @@
-# Datalog conformance config — sourced by lib/guest/conformance.sh.
-
-LANG_NAME=datalog
-MODE=dict
-
-PRELOADS=(
-  lib/datalog/tokenizer.sx
-  lib/datalog/parser.sx
-  lib/datalog/unify.sx
-  lib/datalog/db.sx
-  lib/datalog/builtins.sx
-  lib/datalog/eval.sx
-)
-
-SUITES=(
-  "tokenize:lib/datalog/tests/tokenize.sx:(dl-tokenize-tests-run!)"
-  "parse:lib/datalog/tests/parse.sx:(dl-parse-tests-run!)"
-  "unify:lib/datalog/tests/unify.sx:(dl-unify-tests-run!)"
-  "eval:lib/datalog/tests/eval.sx:(dl-eval-tests-run!)"
-  "builtins:lib/datalog/tests/builtins.sx:(dl-builtins-tests-run!)"
-)

lib/datalog/conformance.sh

@@ -1,3 +0,0 @@
-#!/usr/bin/env bash
-# Thin wrapper — see lib/guest/conformance.sh and lib/datalog/conformance.conf.
-exec bash "$(dirname "$0")/../guest/conformance.sh" "$(dirname "$0")/conformance.conf" "$@"

lib/datalog/db.sx

@@ -1,227 +0,0 @@
-;; lib/datalog/db.sx — Datalog database (EDB + IDB + rules) + safety hook.
-;;
-;; A db is a mutable dict:
-;;   {:facts {<rel-name-string> -> (literal ...)}
-;;    :rules ({:head literal :body (literal ...)} ...)}
-;;
-;; Facts are stored as full literals `(rel arg ... arg)` so they unify
-;; directly against rule body literals. Each relation's tuple list is
-;; deduplicated on insert.
-;;
-;; Phase 3 introduced safety analysis for head variables; Phase 4 (in
-;; lib/datalog/builtins.sx) swaps in the real `dl-rule-check-safety`,
-;; which is order-aware and understands built-in predicates.
-
-(define dl-make-db (fn () {:facts {} :rules (list)}))
-
-(define
-  dl-rel-name
-  (fn
-    (lit)
-    (cond
-      ((and (dict? lit) (has-key? lit :neg)) (dl-rel-name (get lit :neg)))
-      ((and (list? lit) (> (len lit) 0) (symbol? (first lit)))
-        (symbol->string (first lit)))
-      (else nil))))
-
-(define dl-builtin-rels (list "<" "<=" ">" ">=" "=" "!=" "is"))
-
-(define
-  dl-member-string?
-  (fn
-    (s xs)
-    (cond
-      ((= (len xs) 0) false)
-      ((= (first xs) s) true)
-      (else (dl-member-string? s (rest xs))))))
-
-(define
-  dl-builtin?
-  (fn
-    (lit)
-    (and
-      (list? lit)
-      (> (len lit) 0)
-      (let
-        ((rel (dl-rel-name lit)))
-        (cond
-          ((nil? rel) false)
-          (else (dl-member-string? rel dl-builtin-rels)))))))
-
-(define
-  dl-positive-lit?
-  (fn
-    (lit)
-    (cond
-      ((and (dict? lit) (has-key? lit :neg)) false)
-      ((dl-builtin? lit) false)
-      ((and (list? lit) (> (len lit) 0)) true)
-      (else false))))
-
-(define
-  dl-tuple-equal?
-  (fn
-    (a b)
-    (cond
-      ((and (list? a) (list? b))
-        (and (= (len a) (len b)) (dl-tuple-equal-list? a b 0)))
-      ((and (number? a) (number? b)) (= a b))
-      (else (equal? a b)))))
-
-(define
-  dl-tuple-equal-list?
-  (fn
-    (a b i)
-    (cond
-      ((>= i (len a)) true)
-      ((not (dl-tuple-equal? (nth a i) (nth b i))) false)
-      (else (dl-tuple-equal-list? a b (+ i 1))))))
-
-(define
-  dl-tuple-member?
-  (fn
-    (lit lits)
-    (cond
-      ((= (len lits) 0) false)
-      ((dl-tuple-equal? lit (first lits)) true)
-      (else (dl-tuple-member? lit (rest lits))))))
-
-(define
-  dl-ensure-rel!
-  (fn
-    (db rel-key)
-    (let
-      ((facts (get db :facts)))
-      (do
-        (when
-          (not (has-key? facts rel-key))
-          (dict-set! facts rel-key (list)))
-        (get facts rel-key)))))
-
-(define
-  dl-rel-tuples
-  (fn
-    (db rel-key)
-    (let
-      ((facts (get db :facts)))
-      (if (has-key? facts rel-key) (get facts rel-key) (list)))))
-
-(define
-  dl-add-fact!
-  (fn
-    (db lit)
-    (cond
-      ((not (and (list? lit) (> (len lit) 0)))
-        (error (str "dl-add-fact!: expected literal list, got " lit)))
-      ((not (dl-ground? lit (dl-empty-subst)))
-        (error (str "dl-add-fact!: expected ground literal, got " lit)))
-      (else
-        (let
-          ((rel-key (dl-rel-name lit)))
-          (let
-            ((tuples (dl-ensure-rel! db rel-key)))
-            (cond
-              ((dl-tuple-member? lit tuples) false)
-              (else (do (append! tuples lit) true)))))))))
-
-;; The full safety check lives in builtins.sx (it has to know which
-;; predicates are built-ins). dl-add-rule! calls it via forward
-;; reference; load builtins.sx alongside db.sx in any setup that
-;; adds rules. The fallback below is used if builtins.sx isn't loaded.
-(define
-  dl-rule-check-safety
-  (fn
-    (rule)
-    (let
-      ((head-vars (dl-vars-of (get rule :head))) (body-vars (list)))
-      (do
-        (for-each
-          (fn
-            (lit)
-            (when
-              (and
-                (list? lit)
-                (> (len lit) 0)
-                (not (and (dict? lit) (has-key? lit :neg))))
-              (for-each
-                (fn
-                  (v)
-                  (when
-                    (not (dl-member-string? v body-vars))
-                    (append! body-vars v)))
-                (dl-vars-of lit))))
-          (get rule :body))
-        (let
-          ((missing (list)))
-          (do
-            (for-each
-              (fn
-                (v)
-                (when
-                  (and
-                    (not (dl-member-string? v body-vars))
-                    (not (= v "_")))
-                  (append! missing v)))
-              head-vars)
-            (cond
-              ((> (len missing) 0)
-                (str
-                  "head variable(s) "
-                  missing
-                  " do not appear in any body literal"))
-              (else nil))))))))
-
-(define
-  dl-add-rule!
-  (fn
-    (db rule)
-    (cond
-      ((not (dict? rule))
-        (error (str "dl-add-rule!: expected rule dict, got " rule)))
-      ((not (has-key? rule :head))
-        (error (str "dl-add-rule!: rule missing :head, got " rule)))
-      (else
-        (let
-          ((err (dl-rule-check-safety rule)))
-          (cond
-            ((not (nil? err)) (error (str "dl-add-rule!: " err)))
-            (else
-              (let
-                ((rules (get db :rules)))
-                (do (append! rules rule) true)))))))))
-
-(define
-  dl-add-clause!
-  (fn
-    (db clause)
-    (cond
-      ((has-key? clause :query) false)
-      ((and (has-key? clause :body) (= (len (get clause :body)) 0))
-        (dl-add-fact! db (get clause :head)))
-      (else (dl-add-rule! db clause)))))
-
-(define
-  dl-load-program!
-  (fn
-    (db source)
-    (let
-      ((clauses (dl-parse source)))
-      (do (for-each (fn (c) (dl-add-clause! db c)) clauses) db))))
-
-(define
-  dl-program
-  (fn (source) (let ((db (dl-make-db))) (dl-load-program! db source))))
-
-(define dl-rules (fn (db) (get db :rules)))
-
-(define
-  dl-fact-count
-  (fn
-    (db)
-    (let
-      ((facts (get db :facts)) (total 0))
-      (do
-        (for-each
-          (fn (k) (set! total (+ total (len (get facts k)))))
-          (keys facts))
-        total))))

lib/datalog/eval.sx

@@ -1,147 +0,0 @@
-;; lib/datalog/eval.sx — naive bottom-up fixpoint evaluator.
-;;
-;; (dl-saturate! db) iterates rules until no new tuples are derived.
-;; The Herbrand base is finite (no function symbols) so termination is
-;; guaranteed by the language.
-;;
-;; Body literal kinds handled here:
-;;   positive (rel arg ... arg)  → match against EDB+IDB tuples (dl-match-positive)
-;;   built-in (< X Y), (is X e)  → constraint via dl-eval-builtin (Phase 4)
-;;   negation {:neg lit}         → Phase 7
-
-(define
-  dl-match-positive
-  (fn
-    (lit db subst)
-    (let
-      ((rel (dl-rel-name lit)) (results (list)))
-      (cond
-        ((nil? rel) (error (str "dl-match-positive: bad literal " lit)))
-        (else
-          (let
-            ((tuples (dl-rel-tuples db rel)))
-            (do
-              (for-each
-                (fn
-                  (tuple)
-                  (let
-                    ((s (dl-unify lit tuple subst)))
-                    (when (not (nil? s)) (append! results s))))
-                tuples)
-              results)))))))
-
-(define
-  dl-match-lit
-  (fn
-    (lit db subst)
-    (cond
-      ((and (dict? lit) (has-key? lit :neg))
-        (error "datalog: negation not yet supported (Phase 7)"))
-      ((dl-builtin? lit)
-        (let
-          ((s (dl-eval-builtin lit subst)))
-          (if (nil? s) (list) (list s))))
-      ((and (list? lit) (> (len lit) 0))
-        (dl-match-positive lit db subst))
-      (else (error (str "datalog: unknown body-literal shape: " lit))))))
-
-(define
-  dl-find-bindings
-  (fn
-    (lits db subst)
-    (cond
-      ((nil? subst) (list))
-      ((= (len lits) 0) (list subst))
-      (else
-        (let
-          ((options (dl-match-lit (first lits) db subst))
-            (results (list)))
-          (do
-            (for-each
-              (fn
-                (s)
-                (for-each
-                  (fn (s2) (append! results s2))
-                  (dl-find-bindings (rest lits) db s)))
-              options)
-            results))))))
-
-(define
-  dl-apply-rule!
-  (fn
-    (db rule)
-    (let
-      ((head (get rule :head)) (body (get rule :body)) (new? false))
-      (do
-        (for-each
-          (fn
-            (s)
-            (let
-              ((derived (dl-apply-subst head s)))
-              (when (dl-add-fact! db derived) (set! new? true))))
-          (dl-find-bindings body db (dl-empty-subst)))
-        new?))))
-
-(define
-  dl-saturate!
-  (fn
-    (db)
-    (let
-      ((changed true))
-      (do
-        (define
-          dl-sat-loop
-          (fn
-            ()
-            (when
-              changed
-              (do
-                (set! changed false)
-                (for-each
-                  (fn (r) (when (dl-apply-rule! db r) (set! changed true)))
-                  (dl-rules db))
-                (dl-sat-loop)))))
-        (dl-sat-loop)
-        db))))
-
-(define
-  dl-query
-  (fn
-    (db goal)
-    (do
-      (dl-saturate! db)
-      (let
-        ((substs (dl-find-bindings (list goal) db (dl-empty-subst)))
-          (vars (dl-vars-of goal))
-          (results (list)))
-        (do
-          (for-each
-            (fn
-              (s)
-              (let
-                ((proj (dl-project-subst s vars)))
-                (when
-                  (not (dl-tuple-member? proj results))
-                  (append! results proj))))
-            substs)
-          results)))))
-
-(define
-  dl-project-subst
-  (fn
-    (subst names)
-    (let
-      ((out {}))
-      (do
-        (for-each
-          (fn
-            (n)
-            (let
-              ((sym (string->symbol n)))
-              (let
-                ((v (dl-walk sym subst)))
-                (dict-set! out n (dl-apply-subst v subst)))))
-          names)
-        out))))
-
-(define dl-relation (fn (db name) (dl-rel-tuples db name)))

lib/datalog/parser.sx

@@ -1,242 +0,0 @@
-;; lib/datalog/parser.sx — Datalog tokens → AST
-;;
-;; Output shapes:
-;;   Literal (positive)  := (relname arg ... arg)        — SX list
-;;   Literal (negative)  := {:neg (relname arg ... arg)} — dict
-;;   Argument            := var-symbol | atom-symbol | number | string
-;;                        | (op-name arg ... arg)        — arithmetic compound
-;;   Fact                := {:head literal :body ()}
-;;   Rule                := {:head literal :body (lit ... lit)}
-;;   Query               := {:query (lit ... lit)}
-;;   Program             := list of facts / rules / queries
-;;
-;; Variables and constants are both SX symbols; the evaluator dispatches
-;; on first-char case ('A'..'Z' or '_' = variable, otherwise constant).
-;;
-;; The parser permits nested compounds in arg position to support
-;; arithmetic (e.g. (is Z (+ X Y))). Safety analysis at rule-load time
-;; rejects compounds whose head is not an arithmetic operator.
-
-(define
-  dl-pp-peek
-  (fn
-    (st)
-    (let
-      ((i (get st :idx)) (tokens (get st :tokens)))
-      (if (< i (len tokens)) (nth tokens i) {:type "eof" :value nil :pos 0}))))
-
-(define
-  dl-pp-peek2
-  (fn
-    (st)
-    (let
-      ((i (+ (get st :idx) 1)) (tokens (get st :tokens)))
-      (if (< i (len tokens)) (nth tokens i) {:type "eof" :value nil :pos 0}))))
-
-(define
-  dl-pp-advance!
-  (fn (st) (dict-set! st :idx (+ (get st :idx) 1))))
-
-(define
-  dl-pp-at?
-  (fn
-    (st type value)
-    (let
-      ((t (dl-pp-peek st)))
-      (and
-        (= (get t :type) type)
-        (or (= value nil) (= (get t :value) value))))))
-
-(define
-  dl-pp-error
-  (fn
-    (st msg)
-    (let
-      ((t (dl-pp-peek st)))
-      (error
-        (str
-          "Parse error at pos "
-          (get t :pos)
-          ": "
-          msg
-          " (got "
-          (get t :type)
-          " '"
-          (if (= (get t :value) nil) "" (get t :value))
-          "')")))))
-
-(define
-  dl-pp-expect!
-  (fn
-    (st type value)
-    (let
-      ((t (dl-pp-peek st)))
-      (if
-        (dl-pp-at? st type value)
-        (do (dl-pp-advance! st) t)
-        (dl-pp-error
-          st
-          (str "expected " type (if (= value nil) "" (str " '" value "'"))))))))
-
-;; Argument: variable, atom, number, string, or compound (relname/op + parens).
-(define
-  dl-pp-parse-arg
-  (fn
-    (st)
-    (let
-      ((t (dl-pp-peek st)))
-      (let
-        ((ty (get t :type)) (vv (get t :value)))
-        (cond
-          ((= ty "number") (do (dl-pp-advance! st) vv))
-          ((= ty "string") (do (dl-pp-advance! st) vv))
-          ((= ty "var") (do (dl-pp-advance! st) (string->symbol vv)))
-          ((or (= ty "atom") (= ty "op"))
-            (do
-              (dl-pp-advance! st)
-              (if
-                (dl-pp-at? st "punct" "(")
-                (do
-                  (dl-pp-advance! st)
-                  (let
-                    ((args (dl-pp-parse-arg-list st)))
-                    (do
-                      (dl-pp-expect! st "punct" ")")
-                      (cons (string->symbol vv) args))))
-                (string->symbol vv))))
-          (else (dl-pp-error st "expected term")))))))
-
-;; Comma-separated args inside parens.
-(define
-  dl-pp-parse-arg-list
-  (fn
-    (st)
-    (let
-      ((args (list)))
-      (do
-        (append! args (dl-pp-parse-arg st))
-        (define
-          dl-pp-arg-loop
-          (fn
-            ()
-            (when
-              (dl-pp-at? st "punct" ",")
-              (do
-                (dl-pp-advance! st)
-                (append! args (dl-pp-parse-arg st))
-                (dl-pp-arg-loop)))))
-        (dl-pp-arg-loop)
-        args))))
-
-;; A positive literal: relname (atom or op) followed by optional (args).
-(define
-  dl-pp-parse-positive
-  (fn
-    (st)
-    (let
-      ((t (dl-pp-peek st)))
-      (let
-        ((ty (get t :type)) (vv (get t :value)))
-        (if
-          (or (= ty "atom") (= ty "op"))
-          (do
-            (dl-pp-advance! st)
-            (if
-              (dl-pp-at? st "punct" "(")
-              (do
-                (dl-pp-advance! st)
-                (let
-                  ((args (dl-pp-parse-arg-list st)))
-                  (do
-                    (dl-pp-expect! st "punct" ")")
-                    (cons (string->symbol vv) args))))
-              (list (string->symbol vv))))
-          (dl-pp-error st "expected literal head"))))))
-
-;; A body literal: positive, or not(positive).
-(define
-  dl-pp-parse-body-lit
-  (fn
-    (st)
-    (let
-      ((t1 (dl-pp-peek st)) (t2 (dl-pp-peek2 st)))
-      (if
-        (and
-          (= (get t1 :type) "atom")
-          (= (get t1 :value) "not")
-          (= (get t2 :type) "punct")
-          (= (get t2 :value) "("))
-        (do
-          (dl-pp-advance! st)
-          (dl-pp-advance! st)
-          (let
-            ((inner (dl-pp-parse-positive st)))
-            (do (dl-pp-expect! st "punct" ")") {:neg inner})))
-        (dl-pp-parse-positive st)))))
-
-;; Comma-separated body literals.
-(define
-  dl-pp-parse-body
-  (fn
-    (st)
-    (let
-      ((lits (list)))
-      (do
-        (append! lits (dl-pp-parse-body-lit st))
-        (define
-          dl-pp-body-loop
-          (fn
-            ()
-            (when
-              (dl-pp-at? st "punct" ",")
-              (do
-                (dl-pp-advance! st)
-                (append! lits (dl-pp-parse-body-lit st))
-                (dl-pp-body-loop)))))
-        (dl-pp-body-loop)
-        lits))))
-
-;; Single clause: fact, rule, or query. Consumes trailing dot.
-(define
-  dl-pp-parse-clause
-  (fn
-    (st)
-    (cond
-      ((dl-pp-at? st "op" "?-")
-        (do
-          (dl-pp-advance! st)
-          (let
-            ((body (dl-pp-parse-body st)))
-            (do (dl-pp-expect! st "punct" ".") {:query body}))))
-      (else
-        (let
-          ((head (dl-pp-parse-positive st)))
-          (cond
-            ((dl-pp-at? st "op" ":-")
-              (do
-                (dl-pp-advance! st)
-                (let
-                  ((body (dl-pp-parse-body st)))
-                  (do (dl-pp-expect! st "punct" ".") {:body body :head head}))))
-            (else (do (dl-pp-expect! st "punct" ".") {:body (list) :head head}))))))))
-
-(define
-  dl-parse-program
-  (fn
-    (tokens)
-    (let
-      ((st {:tokens tokens :idx 0}) (clauses (list)))
-      (do
-        (define
-          dl-pp-prog-loop
-          (fn
-            ()
-            (when
-              (not (dl-pp-at? st "eof" nil))
-              (do
-                (append! clauses (dl-pp-parse-clause st))
-                (dl-pp-prog-loop)))))
-        (dl-pp-prog-loop)
-        clauses))))
-
-(define dl-parse (fn (src) (dl-parse-program (dl-tokenize src))))

lib/datalog/scoreboard.json

@@ -1,14 +0,0 @@
-{
-  "lang": "datalog",
-  "total_passed": 106,
-  "total_failed": 0,
-  "total": 106,
-  "suites": [
-    {"name":"tokenize","passed":26,"failed":0,"total":26},
-    {"name":"parse","passed":18,"failed":0,"total":18},
-    {"name":"unify","passed":28,"failed":0,"total":28},
-    {"name":"eval","passed":15,"failed":0,"total":15},
-    {"name":"builtins","passed":19,"failed":0,"total":19}
-  ],
-  "generated": "2026-05-07T23:50:44+00:00"
-}

lib/datalog/scoreboard.md

@@ -1,11 +0,0 @@
-# datalog scoreboard
-
-**106 / 106 passing** (0 failure(s)).
-
-| Suite | Passed | Total | Status |
-|-------|--------|-------|--------|
-| tokenize | 26 | 26 | ok |
-| parse | 18 | 18 | ok |
-| unify | 28 | 28 | ok |
-| eval | 15 | 15 | ok |
-| builtins | 19 | 19 | ok |

lib/datalog/tests/builtins.sx

@@ -1,228 +0,0 @@
-;; lib/datalog/tests/builtins.sx — comparison + arithmetic body literals.
-
-(define dl-bt-pass 0)
-(define dl-bt-fail 0)
-(define dl-bt-failures (list))
-
-(define
-  dl-bt-deep=?
-  (fn
-    (a b)
-    (cond
-      ((and (list? a) (list? b))
-        (and (= (len a) (len b)) (dl-bt-deq-l? a b 0)))
-      ((and (dict? a) (dict? b))
-        (let
-          ((ka (keys a)) (kb (keys b)))
-          (and (= (len ka) (len kb)) (dl-bt-deq-d? a b ka 0))))
-      ((and (number? a) (number? b)) (= a b))
-      (else (equal? a b)))))
-
-(define
-  dl-bt-deq-l?
-  (fn
-    (a b i)
-    (cond
-      ((>= i (len a)) true)
-      ((not (dl-bt-deep=? (nth a i) (nth b i))) false)
-      (else (dl-bt-deq-l? a b (+ i 1))))))
-
-(define
-  dl-bt-deq-d?
-  (fn
-    (a b ka i)
-    (cond
-      ((>= i (len ka)) true)
-      ((let ((k (nth ka i))) (not (dl-bt-deep=? (get a k) (get b k))))
-        false)
-      (else (dl-bt-deq-d? a b ka (+ i 1))))))
-
-(define
-  dl-bt-set=?
-  (fn
-    (a b)
-    (and (= (len a) (len b)) (dl-bt-subset? a b) (dl-bt-subset? b a))))
-
-(define
-  dl-bt-subset?
-  (fn
-    (xs ys)
-    (cond
-      ((= (len xs) 0) true)
-      ((not (dl-bt-contains? ys (first xs))) false)
-      (else (dl-bt-subset? (rest xs) ys)))))
-
-(define
-  dl-bt-contains?
-  (fn
-    (xs target)
-    (cond
-      ((= (len xs) 0) false)
-      ((dl-bt-deep=? (first xs) target) true)
-      (else (dl-bt-contains? (rest xs) target)))))
-
-(define
-  dl-bt-test-set!
-  (fn
-    (name got expected)
-    (if
-      (dl-bt-set=? got expected)
-      (set! dl-bt-pass (+ dl-bt-pass 1))
-      (do
-        (set! dl-bt-fail (+ dl-bt-fail 1))
-        (append!
-          dl-bt-failures
-          (str
-            name
-            "\n    expected (set): "
-            expected
-            "\n    got:            "
-            got))))))
-
-(define
-  dl-bt-test!
-  (fn
-    (name got expected)
-    (if
-      (dl-bt-deep=? got expected)
-      (set! dl-bt-pass (+ dl-bt-pass 1))
-      (do
-        (set! dl-bt-fail (+ dl-bt-fail 1))
-        (append!
-          dl-bt-failures
-          (str name "\n    expected: " expected "\n    got:      " got))))))
-
-(define
-  dl-bt-throws?
-  (fn
-    (thunk)
-    (let
-      ((threw false))
-      (do (guard (e (#t (set! threw true))) (thunk)) threw))))
-
-(define
-  dl-bt-run-all!
-  (fn
-    ()
-    (do
-      (dl-bt-test-set!
-        "less than filter"
-        (dl-query
-          (dl-program
-            "age(alice, 30). age(bob, 17). age(carol, 22).\n             adult(X) :- age(X, A), >=(A, 18).")
-          (list (quote adult) (quote X)))
-        (list {:X (quote alice)} {:X (quote carol)}))
-      (dl-bt-test-set!
-        "less-equal filter"
-        (dl-query
-          (dl-program
-            "n(1). n(2). n(3). n(4). n(5).\n             small(X) :- n(X), <=(X, 3).")
-          (list (quote small) (quote X)))
-        (list {:X 1} {:X 2} {:X 3}))
-      (dl-bt-test-set!
-        "not-equal filter"
-        (dl-query
-          (dl-program
-            "p(1, 2). p(2, 2). p(3, 4).\n             diff(X, Y) :- p(X, Y), !=(X, Y).")
-          (list (quote diff) (quote X) (quote Y)))
-        (list {:X 1 :Y 2} {:X 3 :Y 4}))
-      (dl-bt-test-set!
-        "is plus"
-        (dl-query
-          (dl-program
-            "n(1). n(2). n(3).\n             succ(X, Y) :- n(X), is(Y, +(X, 1)).")
-          (list (quote succ) (quote X) (quote Y)))
-        (list {:X 1 :Y 2} {:X 2 :Y 3} {:X 3 :Y 4}))
-      (dl-bt-test-set!
-        "is multiply"
-        (dl-query
-          (dl-program
-            "n(2). n(3). n(4).\n             square(X, Y) :- n(X), is(Y, *(X, X)).")
-          (list (quote square) (quote X) (quote Y)))
-        (list {:X 2 :Y 4} {:X 3 :Y 9} {:X 4 :Y 16}))
-      (dl-bt-test-set!
-        "is nested expr"
-        (dl-query
-          (dl-program
-            "n(1). n(2). n(3).\n             f(X, Y) :- n(X), is(Y, *(+(X, 1), 2)).")
-          (list (quote f) (quote X) (quote Y)))
-        (list {:X 1 :Y 4} {:X 2 :Y 6} {:X 3 :Y 8}))
-      (dl-bt-test-set!
-        "is bound LHS — equality"
-        (dl-query
-          (dl-program
-            "n(1, 2). n(2, 5). n(3, 4).\n             succ(X, Y) :- n(X, Y), is(Y, +(X, 1)).")
-          (list (quote succ) (quote X) (quote Y)))
-        (list {:X 1 :Y 2} {:X 3 :Y 4}))
-      (dl-bt-test-set!
-        "triple via is"
-        (dl-query
-          (dl-program
-            "n(1). n(2). n(3).\n             triple(X, Y) :- n(X), is(Y, *(X, 3)).")
-          (list (quote triple) (quote X) (quote Y)))
-        (list {:X 1 :Y 3} {:X 2 :Y 6} {:X 3 :Y 9}))
-      (dl-bt-test-set!
-        "= unifies var with constant"
-        (dl-query
-          (dl-program "p(a). p(b).\n             qual(X) :- p(X), =(X, a).")
-          (list (quote qual) (quote X)))
-        (list {:X (quote a)}))
-      (dl-bt-test-set!
-        "= unifies two vars (one bound)"
-        (dl-query
-          (dl-program "p(a). p(b).\n             twin(X, Y) :- p(X), =(Y, X).")
-          (list (quote twin) (quote X) (quote Y)))
-        (list {:X (quote a) :Y (quote a)} {:X (quote b) :Y (quote b)}))
-      (dl-bt-test!
-        "big count"
-        (let
-          ((db (dl-program "n(0). n(1). n(2). n(3). n(4). n(5). n(6). n(7). n(8). n(9).\n                  big(X) :- n(X), >=(X, 5).")))
-          (do (dl-saturate! db) (len (dl-relation db "big"))))
-        5)
-      (dl-bt-test!
-        "unsafe — comparison without binder"
-        (dl-bt-throws? (fn () (dl-program "p(X) :- <(X, 5).")))
-        true)
-      (dl-bt-test!
-        "unsafe — comparison both unbound"
-        (dl-bt-throws? (fn () (dl-program "p(X, Y) :- <(X, Y), q(X).")))
-        true)
-      (dl-bt-test!
-        "unsafe — is uses unbound RHS var"
-        (dl-bt-throws?
-          (fn () (dl-program "p(X, Y) :- q(X), is(Y, +(X, Z)).")))
-        true)
-      (dl-bt-test!
-        "unsafe — is on its own"
-        (dl-bt-throws? (fn () (dl-program "p(Y) :- is(Y, +(X, 1)).")))
-        true)
-      (dl-bt-test!
-        "unsafe — = between two unbound"
-        (dl-bt-throws? (fn () (dl-program "p(X, Y) :- =(X, Y).")))
-        true)
-      (dl-bt-test!
-        "safe — is binds head var"
-        (dl-bt-throws?
-          (fn () (dl-program "n(1). p(Y) :- n(X), is(Y, +(X, 1)).")))
-        false)
-      (dl-bt-test!
-        "safe — comparison after binder"
-        (dl-bt-throws?
-          (fn () (dl-program "n(1). big(X) :- n(X), >=(X, 0).")))
-        false)
-      (dl-bt-test!
-        "safe — = binds head var"
-        (dl-bt-throws?
-          (fn () (dl-program "p(a). p(b). x(Y) :- p(X), =(Y, X).")))
-        false))))
-
-(define
-  dl-builtins-tests-run!
-  (fn
-    ()
-    (do
-      (set! dl-bt-pass 0)
-      (set! dl-bt-fail 0)
-      (set! dl-bt-failures (list))
-      (dl-bt-run-all!)
-      {:failures dl-bt-failures :total (+ dl-bt-pass dl-bt-fail) :passed dl-bt-pass :failed dl-bt-fail})))

lib/datalog/tests/eval.sx

@@ -1,206 +0,0 @@
-;; lib/datalog/tests/eval.sx — naive evaluation + safety analysis tests.
-
-(define dl-et-pass 0)
-(define dl-et-fail 0)
-(define dl-et-failures (list))
-
-;; Same deep-equal helper used in other suites.
-(define
-  dl-et-deep=?
-  (fn
-    (a b)
-    (cond
-      ((and (list? a) (list? b))
-        (and (= (len a) (len b)) (dl-et-deq-l? a b 0)))
-      ((and (dict? a) (dict? b))
-        (let
-          ((ka (keys a)) (kb (keys b)))
-          (and (= (len ka) (len kb)) (dl-et-deq-d? a b ka 0))))
-      ((and (number? a) (number? b)) (= a b))
-      (else (equal? a b)))))
-
-(define
-  dl-et-deq-l?
-  (fn
-    (a b i)
-    (cond
-      ((>= i (len a)) true)
-      ((not (dl-et-deep=? (nth a i) (nth b i))) false)
-      (else (dl-et-deq-l? a b (+ i 1))))))
-
-(define
-  dl-et-deq-d?
-  (fn
-    (a b ka i)
-    (cond
-      ((>= i (len ka)) true)
-      ((let ((k (nth ka i))) (not (dl-et-deep=? (get a k) (get b k))))
-        false)
-      (else (dl-et-deq-d? a b ka (+ i 1))))))
-
-;; Set-equality on lists (order-independent, uses dl-et-deep=?).
-(define
-  dl-et-set=?
-  (fn
-    (a b)
-    (and (= (len a) (len b)) (dl-et-subset? a b) (dl-et-subset? b a))))
-
-(define
-  dl-et-subset?
-  (fn
-    (xs ys)
-    (cond
-      ((= (len xs) 0) true)
-      ((not (dl-et-contains? ys (first xs))) false)
-      (else (dl-et-subset? (rest xs) ys)))))
-
-(define
-  dl-et-contains?
-  (fn
-    (xs target)
-    (cond
-      ((= (len xs) 0) false)
-      ((dl-et-deep=? (first xs) target) true)
-      (else (dl-et-contains? (rest xs) target)))))
-
-(define
-  dl-et-test!
-  (fn
-    (name got expected)
-    (if
-      (dl-et-deep=? got expected)
-      (set! dl-et-pass (+ dl-et-pass 1))
-      (do
-        (set! dl-et-fail (+ dl-et-fail 1))
-        (append!
-          dl-et-failures
-          (str name "\n    expected: " expected "\n    got:      " got))))))
-
-(define
-  dl-et-test-set!
-  (fn
-    (name got expected)
-    (if
-      (dl-et-set=? got expected)
-      (set! dl-et-pass (+ dl-et-pass 1))
-      (do
-        (set! dl-et-fail (+ dl-et-fail 1))
-        (append!
-          dl-et-failures
-          (str
-            name
-            "\n    expected (set): "
-            expected
-            "\n    got:            "
-            got))))))
-
-(define
-  dl-et-throws?
-  (fn
-    (thunk)
-    (let
-      ((threw false))
-      (do (guard (e (#t (set! threw true))) (thunk)) threw))))
-
-(define
-  dl-et-run-all!
-  (fn
-    ()
-    (do
-      (dl-et-test-set!
-        "fact lookup any"
-        (dl-query
-          (dl-program "parent(tom, bob). parent(bob, ann).")
-          (list (quote parent) (quote X) (quote Y)))
-        (list {:X (quote tom) :Y (quote bob)} {:X (quote bob) :Y (quote ann)}))
-      (dl-et-test-set!
-        "fact lookup constant arg"
-        (dl-query
-          (dl-program "parent(tom, bob). parent(tom, liz). parent(bob, ann).")
-          (list (quote parent) (quote tom) (quote Y)))
-        (list {:Y (quote bob)} {:Y (quote liz)}))
-      (dl-et-test-set!
-        "no match"
-        (dl-query
-          (dl-program "parent(tom, bob).")
-          (list (quote parent) (quote nobody) (quote X)))
-        (list))
-      (dl-et-test-set!
-        "ancestor closure"
-        (dl-query
-          (dl-program
-            "parent(tom, bob). parent(bob, ann). parent(ann, pat).\n             ancestor(X, Y) :- parent(X, Y).\n             ancestor(X, Z) :- parent(X, Y), ancestor(Y, Z).")
-          (list (quote ancestor) (quote tom) (quote X)))
-        (list {:X (quote bob)} {:X (quote ann)} {:X (quote pat)}))
-      (dl-et-test-set!
-        "sibling"
-        (dl-query
-          (dl-program
-            "parent(tom, bob). parent(tom, liz). parent(jane, bob). parent(jane, liz).\n             sibling(X, Y) :- parent(P, X), parent(P, Y).")
-          (list (quote sibling) (quote bob) (quote Y)))
-        (list {:Y (quote bob)} {:Y (quote liz)}))
-      (dl-et-test-set!
-        "same-generation"
-        (dl-query
-          (dl-program
-            "parent(tom, bob). parent(tom, liz). parent(bob, ann). parent(liz, joe).\n             person(tom). person(bob). person(liz). person(ann). person(joe).\n             sg(X, X) :- person(X).\n             sg(X, Y) :- parent(P1, X), sg(P1, P2), parent(P2, Y).")
-          (list (quote sg) (quote ann) (quote X)))
-        (list {:X (quote ann)} {:X (quote joe)}))
-      (dl-et-test!
-        "ancestor count"
-        (let
-          ((db (dl-program "parent(a, b). parent(b, c). parent(c, d).\n                  ancestor(X, Y) :- parent(X, Y).\n                  ancestor(X, Z) :- parent(X, Y), ancestor(Y, Z).")))
-          (do (dl-saturate! db) (len (dl-relation db "ancestor"))))
-        6)
-      (dl-et-test-set!
-        "grandparent"
-        (dl-query
-          (dl-program
-            "parent(a, b). parent(b, c). parent(c, d).\n             grandparent(X, Z) :- parent(X, Y), parent(Y, Z).")
-          (list (quote grandparent) (quote X) (quote Y)))
-        (list {:X (quote a) :Y (quote c)} {:X (quote b) :Y (quote d)}))
-      (dl-et-test!
-        "no recursion infinite loop"
-        (let
-          ((db (dl-program "edge(1, 2). edge(2, 3). edge(3, 1).\n                  reach(X, Y) :- edge(X, Y).\n                  reach(X, Z) :- edge(X, Y), reach(Y, Z).")))
-          (do (dl-saturate! db) (len (dl-relation db "reach"))))
-        9)
-      (dl-et-test!
-        "unsafe head var"
-        (dl-et-throws? (fn () (dl-program "p(X, Y) :- q(X).")))
-        true)
-      (dl-et-test!
-        "unsafe — empty body"
-        (dl-et-throws? (fn () (dl-program "p(X) :- .")))
-        true)
-      (dl-et-test!
-        "underscore var ok"
-        (dl-et-throws? (fn () (dl-program "p(X, _) :- q(X).")))
-        false)
-      (dl-et-test!
-        "var only in head — unsafe"
-        (dl-et-throws? (fn () (dl-program "p(X, Y) :- q(Z).")))
-        true)
-      (dl-et-test!
-        "head var bound by body"
-        (dl-et-throws? (fn () (dl-program "p(X) :- q(X).")))
-        false)
-      (dl-et-test!
-        "head subset of body"
-        (dl-et-throws?
-          (fn
-            ()
-            (dl-program
-              "edge(a,b). edge(b,c). reach(X, Z) :- edge(X, Y), edge(Y, Z).")))
-        false))))
-
-(define
-  dl-eval-tests-run!
-  (fn
-    ()
-    (do
-      (set! dl-et-pass 0)
-      (set! dl-et-fail 0)
-      (set! dl-et-failures (list))
-      (dl-et-run-all!)
-      {:failures dl-et-failures :total (+ dl-et-pass dl-et-fail) :passed dl-et-pass :failed dl-et-fail})))

lib/datalog/tests/parse.sx

@@ -1,147 +0,0 @@
-;; lib/datalog/tests/parse.sx — parser unit tests
-;;
-;; Run via: bash lib/datalog/conformance.sh
-;; Or:      (load "lib/datalog/tokenizer.sx") (load "lib/datalog/parser.sx")
-;;          (load "lib/datalog/tests/parse.sx") (dl-parse-tests-run!)
-
-(define dl-pt-pass 0)
-(define dl-pt-fail 0)
-(define dl-pt-failures (list))
-
-;; Order-independent structural equality. Lists compared positionally,
-;; dicts as sets of (key, value) pairs. Numbers via = (so 30.0 = 30).
-(define
-  dl-deep-equal?
-  (fn
-    (a b)
-    (cond
-      ((and (list? a) (list? b))
-        (and (= (len a) (len b)) (dl-deep-equal-list? a b 0)))
-      ((and (dict? a) (dict? b))
-        (let
-          ((ka (keys a)) (kb (keys b)))
-          (and
-            (= (len ka) (len kb))
-            (dl-deep-equal-dict? a b ka 0))))
-      ((and (number? a) (number? b)) (= a b))
-      (else (equal? a b)))))
-
-(define
-  dl-deep-equal-list?
-  (fn
-    (a b i)
-    (cond
-      ((>= i (len a)) true)
-      ((not (dl-deep-equal? (nth a i) (nth b i))) false)
-      (else (dl-deep-equal-list? a b (+ i 1))))))
-
-(define
-  dl-deep-equal-dict?
-  (fn
-    (a b ka i)
-    (cond
-      ((>= i (len ka)) true)
-      ((let ((k (nth ka i))) (not (dl-deep-equal? (get a k) (get b k))))
-        false)
-      (else (dl-deep-equal-dict? a b ka (+ i 1))))))
-
-(define
-  dl-pt-test!
-  (fn
-    (name got expected)
-    (if
-      (dl-deep-equal? got expected)
-      (set! dl-pt-pass (+ dl-pt-pass 1))
-      (do
-        (set! dl-pt-fail (+ dl-pt-fail 1))
-        (append!
-          dl-pt-failures
-          (str name "\n    expected: " expected "\n    got:      " got))))))
-
-(define
-  dl-pt-throws?
-  (fn
-    (thunk)
-    (let
-      ((threw false))
-      (do (guard (e (#t (set! threw true))) (thunk)) threw))))
-
-(define
-  dl-pt-run-all!
-  (fn
-    ()
-    (do
-      (dl-pt-test! "empty program" (dl-parse "") (list))
-      (dl-pt-test! "fact" (dl-parse "parent(tom, bob).") (list {:body (list) :head (list (quote parent) (quote tom) (quote bob))}))
-      (dl-pt-test!
-        "two facts"
-        (dl-parse "parent(tom, bob). parent(bob, ann).")
-        (list {:body (list) :head (list (quote parent) (quote tom) (quote bob))} {:body (list) :head (list (quote parent) (quote bob) (quote ann))}))
-      (dl-pt-test! "zero-ary fact" (dl-parse "ready.") (list {:body (list) :head (list (quote ready))}))
-      (dl-pt-test!
-        "rule one body lit"
-        (dl-parse "ancestor(X, Y) :- parent(X, Y).")
-        (list {:body (list (list (quote parent) (quote X) (quote Y))) :head (list (quote ancestor) (quote X) (quote Y))}))
-      (dl-pt-test!
-        "recursive rule"
-        (dl-parse "ancestor(X, Z) :- parent(X, Y), ancestor(Y, Z).")
-        (list {:body (list (list (quote parent) (quote X) (quote Y)) (list (quote ancestor) (quote Y) (quote Z))) :head (list (quote ancestor) (quote X) (quote Z))}))
-      (dl-pt-test!
-        "query single"
-        (dl-parse "?- ancestor(tom, X).")
-        (list {:query (list (list (quote ancestor) (quote tom) (quote X)))}))
-      (dl-pt-test!
-        "query multi"
-        (dl-parse "?- p(X), q(X).")
-        (list {:query (list (list (quote p) (quote X)) (list (quote q) (quote X)))}))
-      (dl-pt-test!
-        "negation"
-        (dl-parse "safe(X) :- person(X), not(parent(X, _)).")
-        (list {:body (list (list (quote person) (quote X)) {:neg (list (quote parent) (quote X) (quote _))}) :head (list (quote safe) (quote X))}))
-      (dl-pt-test!
-        "number arg"
-        (dl-parse "age(alice, 30).")
-        (list {:body (list) :head (list (quote age) (quote alice) 30)}))
-      (dl-pt-test!
-        "string arg"
-        (dl-parse "label(x, \"hi\").")
-        (list {:body (list) :head (list (quote label) (quote x) "hi")}))
-      (dl-pt-test!
-        "comparison literal"
-        (dl-parse "p(X) :- <(X, 5).")
-        (list {:body (list (list (string->symbol "<") (quote X) 5)) :head (list (quote p) (quote X))}))
-      (dl-pt-test!
-        "is with arith"
-        (dl-parse "succ(X, Y) :- nat(X), is(Y, +(X, 1)).")
-        (list {:body (list (list (quote nat) (quote X)) (list (quote is) (quote Y) (list (string->symbol "+") (quote X) 1))) :head (list (quote succ) (quote X) (quote Y))}))
-      (dl-pt-test!
-        "mixed program"
-        (dl-parse "p(a). p(b). q(X) :- p(X). ?- q(Y).")
-        (list {:body (list) :head (list (quote p) (quote a))} {:body (list) :head (list (quote p) (quote b))} {:body (list (list (quote p) (quote X))) :head (list (quote q) (quote X))} {:query (list (list (quote q) (quote Y)))}))
-      (dl-pt-test!
-        "comments skipped"
-        (dl-parse "% comment\nfoo(a).\n/* block */ bar(b).")
-        (list {:body (list) :head (list (quote foo) (quote a))} {:body (list) :head (list (quote bar) (quote b))}))
-      (dl-pt-test!
-        "underscore var"
-        (dl-parse "p(X) :- q(X, _).")
-        (list {:body (list (list (quote q) (quote X) (quote _))) :head (list (quote p) (quote X))}))
-      (dl-pt-test!
-        "missing dot raises"
-        (dl-pt-throws? (fn () (dl-parse "p(a)")))
-        true)
-      (dl-pt-test!
-        "trailing comma raises"
-        (dl-pt-throws? (fn () (dl-parse "p(a,).")))
-        true))))
-
-(define
-  dl-parse-tests-run!
-  (fn
-    ()
-    (do
-      (set! dl-pt-pass 0)
-      (set! dl-pt-fail 0)
-      (set! dl-pt-failures (list))
-      (dl-pt-run-all!)
-      {:failures dl-pt-failures :total (+ dl-pt-pass dl-pt-fail) :passed dl-pt-pass :failed dl-pt-fail})))

lib/datalog/tests/tokenize.sx

@@ -1,139 +0,0 @@
-;; lib/datalog/tests/tokenize.sx — tokenizer unit tests
-;;
-;; Run via: bash lib/datalog/conformance.sh
-;; Or:      (load "lib/datalog/tokenizer.sx") (load "lib/datalog/tests/tokenize.sx")
-;;          (dl-tokenize-tests-run!)
-
-(define dl-tk-pass 0)
-(define dl-tk-fail 0)
-(define dl-tk-failures (list))
-
-(define
-  dl-tk-test!
-  (fn
-    (name got expected)
-    (if
-      (= got expected)
-      (set! dl-tk-pass (+ dl-tk-pass 1))
-      (do
-        (set! dl-tk-fail (+ dl-tk-fail 1))
-        (append!
-          dl-tk-failures
-          (str name "\n    expected: " expected "\n    got:      " got))))))
-
-(define dl-tk-types (fn (toks) (map (fn (t) (get t :type)) toks)))
-(define dl-tk-values (fn (toks) (map (fn (t) (get t :value)) toks)))
-
-(define
-  dl-tk-run-all!
-  (fn
-    ()
-    (do
-      (dl-tk-test! "empty" (dl-tk-types (dl-tokenize "")) (list "eof"))
-      (dl-tk-test!
-        "atom dot"
-        (dl-tk-types (dl-tokenize "foo."))
-        (list "atom" "punct" "eof"))
-      (dl-tk-test!
-        "atom dot value"
-        (dl-tk-values (dl-tokenize "foo."))
-        (list "foo" "." nil))
-      (dl-tk-test!
-        "var"
-        (dl-tk-types (dl-tokenize "X."))
-        (list "var" "punct" "eof"))
-      (dl-tk-test!
-        "underscore var"
-        (dl-tk-types (dl-tokenize "_x."))
-        (list "var" "punct" "eof"))
-      (dl-tk-test!
-        "integer"
-        (dl-tk-values (dl-tokenize "42"))
-        (list 42 nil))
-      (dl-tk-test!
-        "decimal"
-        (dl-tk-values (dl-tokenize "3.14"))
-        (list 3.14 nil))
-      (dl-tk-test!
-        "string"
-        (dl-tk-values (dl-tokenize "\"hello\""))
-        (list "hello" nil))
-      (dl-tk-test!
-        "quoted atom"
-        (dl-tk-types (dl-tokenize "'two words'"))
-        (list "atom" "eof"))
-      (dl-tk-test!
-        "quoted atom value"
-        (dl-tk-values (dl-tokenize "'two words'"))
-        (list "two words" nil))
-      (dl-tk-test! ":-" (dl-tk-values (dl-tokenize ":-")) (list ":-" nil))
-      (dl-tk-test! "?-" (dl-tk-values (dl-tokenize "?-")) (list "?-" nil))
-      (dl-tk-test! "<=" (dl-tk-values (dl-tokenize "<=")) (list "<=" nil))
-      (dl-tk-test! ">=" (dl-tk-values (dl-tokenize ">=")) (list ">=" nil))
-      (dl-tk-test! "!=" (dl-tk-values (dl-tokenize "!=")) (list "!=" nil))
-      (dl-tk-test!
-        "single op values"
-        (dl-tk-values (dl-tokenize "< > = + - * /"))
-        (list "<" ">" "=" "+" "-" "*" "/" nil))
-      (dl-tk-test!
-        "single op types"
-        (dl-tk-types (dl-tokenize "< > = + - * /"))
-        (list "op" "op" "op" "op" "op" "op" "op" "eof"))
-      (dl-tk-test!
-        "punct"
-        (dl-tk-values (dl-tokenize "( ) , ."))
-        (list "(" ")" "," "." nil))
-      (dl-tk-test!
-        "fact tokens"
-        (dl-tk-types (dl-tokenize "parent(tom, bob)."))
-        (list "atom" "punct" "atom" "punct" "atom" "punct" "punct" "eof"))
-      (dl-tk-test!
-        "rule shape"
-        (dl-tk-types (dl-tokenize "p(X) :- q(X)."))
-        (list
-          "atom"
-          "punct"
-          "var"
-          "punct"
-          "op"
-          "atom"
-          "punct"
-          "var"
-          "punct"
-          "punct"
-          "eof"))
-      (dl-tk-test!
-        "comparison literal"
-        (dl-tk-values (dl-tokenize "<(X, 5)"))
-        (list "<" "(" "X" "," 5 ")" nil))
-      (dl-tk-test!
-        "is form"
-        (dl-tk-values (dl-tokenize "is(Y, +(X, 1))"))
-        (list "is" "(" "Y" "," "+" "(" "X" "," 1 ")" ")" nil))
-      (dl-tk-test!
-        "line comment"
-        (dl-tk-types (dl-tokenize "% comment line\nfoo."))
-        (list "atom" "punct" "eof"))
-      (dl-tk-test!
-        "block comment"
-        (dl-tk-types (dl-tokenize "/* a\nb */ x."))
-        (list "atom" "punct" "eof"))
-      (dl-tk-test!
-        "whitespace"
-        (dl-tk-types (dl-tokenize "  foo  ,\t bar  ."))
-        (list "atom" "punct" "atom" "punct" "eof"))
-      (dl-tk-test!
-        "positions"
-        (map (fn (t) (get t :pos)) (dl-tokenize "foo bar"))
-        (list 0 4 7)))))
-
-(define
-  dl-tokenize-tests-run!
-  (fn
-    ()
-    (do
-      (set! dl-tk-pass 0)
-      (set! dl-tk-fail 0)
-      (set! dl-tk-failures (list))
-      (dl-tk-run-all!)
-      {:failures dl-tk-failures :total (+ dl-tk-pass dl-tk-fail) :passed dl-tk-pass :failed dl-tk-fail})))

lib/datalog/tests/unify.sx

@@ -1,185 +0,0 @@
-;; lib/datalog/tests/unify.sx — unification + substitution tests.
-
-(define dl-ut-pass 0)
-(define dl-ut-fail 0)
-(define dl-ut-failures (list))
-
-(define
-  dl-ut-deep-equal?
-  (fn
-    (a b)
-    (cond
-      ((and (list? a) (list? b))
-        (and (= (len a) (len b)) (dl-ut-deq-list? a b 0)))
-      ((and (dict? a) (dict? b))
-        (let
-          ((ka (keys a)) (kb (keys b)))
-          (and (= (len ka) (len kb)) (dl-ut-deq-dict? a b ka 0))))
-      ((and (number? a) (number? b)) (= a b))
-      (else (equal? a b)))))
-
-(define
-  dl-ut-deq-list?
-  (fn
-    (a b i)
-    (cond
-      ((>= i (len a)) true)
-      ((not (dl-ut-deep-equal? (nth a i) (nth b i))) false)
-      (else (dl-ut-deq-list? a b (+ i 1))))))
-
-(define
-  dl-ut-deq-dict?
-  (fn
-    (a b ka i)
-    (cond
-      ((>= i (len ka)) true)
-      ((let ((k (nth ka i))) (not (dl-ut-deep-equal? (get a k) (get b k))))
-        false)
-      (else (dl-ut-deq-dict? a b ka (+ i 1))))))
-
-(define
-  dl-ut-test!
-  (fn
-    (name got expected)
-    (if
-      (dl-ut-deep-equal? got expected)
-      (set! dl-ut-pass (+ dl-ut-pass 1))
-      (do
-        (set! dl-ut-fail (+ dl-ut-fail 1))
-        (append!
-          dl-ut-failures
-          (str name "\n    expected: " expected "\n    got:      " got))))))
-
-(define
-  dl-ut-run-all!
-  (fn
-    ()
-    (do
-      (dl-ut-test! "var? uppercase" (dl-var? (quote X)) true)
-      (dl-ut-test! "var? underscore" (dl-var? (quote _foo)) true)
-      (dl-ut-test! "var? lowercase" (dl-var? (quote tom)) false)
-      (dl-ut-test! "var? number" (dl-var? 5) false)
-      (dl-ut-test! "var? string" (dl-var? "hi") false)
-      (dl-ut-test! "var? list" (dl-var? (list 1)) false)
-      (dl-ut-test!
-        "atom-atom match"
-        (dl-unify (quote tom) (quote tom) (dl-empty-subst))
-        {})
-      (dl-ut-test!
-        "atom-atom fail"
-        (dl-unify (quote tom) (quote bob) (dl-empty-subst))
-        nil)
-      (dl-ut-test!
-        "num-num match"
-        (dl-unify 5 5 (dl-empty-subst))
-        {})
-      (dl-ut-test!
-        "num-num fail"
-        (dl-unify 5 6 (dl-empty-subst))
-        nil)
-      (dl-ut-test!
-        "string match"
-        (dl-unify "hi" "hi" (dl-empty-subst))
-        {})
-      (dl-ut-test! "string fail" (dl-unify "hi" "bye" (dl-empty-subst)) nil)
-      (dl-ut-test!
-        "var-atom binds"
-        (dl-unify (quote X) (quote tom) (dl-empty-subst))
-        {:X (quote tom)})
-      (dl-ut-test!
-        "atom-var binds"
-        (dl-unify (quote tom) (quote X) (dl-empty-subst))
-        {:X (quote tom)})
-      (dl-ut-test!
-        "var-var same"
-        (dl-unify (quote X) (quote X) (dl-empty-subst))
-        {})
-      (dl-ut-test!
-        "var-var bind"
-        (let
-          ((s (dl-unify (quote X) (quote Y) (dl-empty-subst))))
-          (dl-walk (quote X) s))
-        (quote Y))
-      (dl-ut-test!
-        "tuple match"
-        (dl-unify
-          (list (quote parent) (quote X) (quote bob))
-          (list (quote parent) (quote tom) (quote Y))
-          (dl-empty-subst))
-        {:X (quote tom) :Y (quote bob)})
-      (dl-ut-test!
-        "tuple arity mismatch"
-        (dl-unify
-          (list (quote p) (quote X))
-          (list (quote p) (quote a) (quote b))
-          (dl-empty-subst))
-        nil)
-      (dl-ut-test!
-        "tuple head mismatch"
-        (dl-unify
-          (list (quote p) (quote X))
-          (list (quote q) (quote X))
-          (dl-empty-subst))
-        nil)
-      (dl-ut-test!
-        "walk chain"
-        (let
-          ((s1 (dl-unify (quote X) (quote Y) (dl-empty-subst))))
-          (let
-            ((s2 (dl-unify (quote Y) (quote tom) s1)))
-            (dl-walk (quote X) s2)))
-        (quote tom))
-      (dl-ut-test!
-        "apply subst on tuple"
-        (let
-          ((s (dl-bind (quote X) (quote tom) (dl-empty-subst))))
-          (dl-apply-subst (list (quote parent) (quote X) (quote Y)) s))
-        (list (quote parent) (quote tom) (quote Y)))
-      (dl-ut-test!
-        "ground? all const"
-        (dl-ground?
-          (list (quote p) (quote tom) 5)
-          (dl-empty-subst))
-        true)
-      (dl-ut-test!
-        "ground? unbound var"
-        (dl-ground? (list (quote p) (quote X)) (dl-empty-subst))
-        false)
-      (dl-ut-test!
-        "ground? bound var"
-        (let
-          ((s (dl-bind (quote X) (quote tom) (dl-empty-subst))))
-          (dl-ground? (list (quote p) (quote X)) s))
-        true)
-      (dl-ut-test!
-        "ground? bare var"
-        (dl-ground? (quote X) (dl-empty-subst))
-        false)
-      (dl-ut-test!
-        "vars-of basic"
-        (dl-vars-of
-          (list (quote p) (quote X) (quote tom) (quote Y) (quote X)))
-        (list "X" "Y"))
-      (dl-ut-test!
-        "vars-of ground"
-        (dl-vars-of (list (quote p) (quote tom) (quote bob)))
-        (list))
-      (dl-ut-test!
-        "vars-of nested compound"
-        (dl-vars-of
-          (list
-            (quote is)
-            (quote Z)
-            (list (string->symbol "+") (quote X) 1)))
-        (list "Z" "X")))))
-
-(define
-  dl-unify-tests-run!
-  (fn
-    ()
-    (do
-      (set! dl-ut-pass 0)
-      (set! dl-ut-fail 0)
-      (set! dl-ut-failures (list))
-      (dl-ut-run-all!)
-      {:failures dl-ut-failures :total (+ dl-ut-pass dl-ut-fail) :passed dl-ut-pass :failed dl-ut-fail})))

lib/datalog/tokenizer.sx

@@ -1,254 +0,0 @@
-;; lib/datalog/tokenizer.sx — Datalog source → token stream
-;;
-;; Tokens: {:type T :value V :pos P}
-;; Types:
-;;   "atom"    — lowercase-start ident or quoted 'atom'
-;;   "var"     — uppercase-start or _-start ident (value is the name)
-;;   "number"  — numeric literal (decoded to number)
-;;   "string"  — "..." string literal
-;;   "punct"   — ( ) , .
-;;   "op"      — :- ?- <= >= != < > = + - * /
-;;   "eof"
-;;
-;; Datalog has no function symbols in arg position; the parser still
-;; accepts nested compounds for arithmetic ((is X (+ A B))) but safety
-;; analysis rejects non-arithmetic nesting at rule-load time.
-
-(define dl-make-token (fn (type value pos) {:type type :value value :pos pos}))
-
-(define dl-digit? (fn (c) (and (>= c "0") (<= c "9"))))
-(define dl-lower? (fn (c) (and (>= c "a") (<= c "z"))))
-(define dl-upper? (fn (c) (and (>= c "A") (<= c "Z"))))
-
-(define
-  dl-ident-char?
-  (fn (c) (or (dl-lower? c) (dl-upper? c) (dl-digit? c) (= c "_"))))
-
-(define dl-ws? (fn (c) (or (= c " ") (= c "\t") (= c "\n") (= c "\r"))))
-
-(define
-  dl-tokenize
-  (fn
-    (src)
-    (let
-      ((tokens (list)) (pos 0) (src-len (len src)))
-      (define
-        dl-peek
-        (fn
-          (offset)
-          (if (< (+ pos offset) src-len) (nth src (+ pos offset)) nil)))
-      (define cur (fn () (dl-peek 0)))
-      (define advance! (fn (n) (set! pos (+ pos n))))
-      (define
-        at?
-        (fn
-          (s)
-          (let
-            ((sl (len s)))
-            (and (<= (+ pos sl) src-len) (= (slice src pos (+ pos sl)) s)))))
-      (define
-        dl-emit!
-        (fn
-          (type value start)
-          (append! tokens (dl-make-token type value start))))
-      (define
-        skip-line-comment!
-        (fn
-          ()
-          (when
-            (and (< pos src-len) (not (= (cur) "\n")))
-            (do (advance! 1) (skip-line-comment!)))))
-      (define
-        skip-block-comment!
-        (fn
-          ()
-          (cond
-            ((>= pos src-len) nil)
-            ((and (= (cur) "*") (< (+ pos 1) src-len) (= (dl-peek 1) "/"))
-              (advance! 2))
-            (else (do (advance! 1) (skip-block-comment!))))))
-      (define
-        skip-ws!
-        (fn
-          ()
-          (cond
-            ((>= pos src-len) nil)
-            ((dl-ws? (cur)) (do (advance! 1) (skip-ws!)))
-            ((= (cur) "%")
-              (do (advance! 1) (skip-line-comment!) (skip-ws!)))
-            ((and (= (cur) "/") (< (+ pos 1) src-len) (= (dl-peek 1) "*"))
-              (do (advance! 2) (skip-block-comment!) (skip-ws!)))
-            (else nil))))
-      (define
-        read-ident
-        (fn
-          (start)
-          (do
-            (when
-              (and (< pos src-len) (dl-ident-char? (cur)))
-              (do (advance! 1) (read-ident start)))
-            (slice src start pos))))
-      (define
-        read-decimal-digits!
-        (fn
-          ()
-          (when
-            (and (< pos src-len) (dl-digit? (cur)))
-            (do (advance! 1) (read-decimal-digits!)))))
-      (define
-        read-number
-        (fn
-          (start)
-          (do
-            (read-decimal-digits!)
-            (when
-              (and
-                (< pos src-len)
-                (= (cur) ".")
-                (< (+ pos 1) src-len)
-                (dl-digit? (dl-peek 1)))
-              (do (advance! 1) (read-decimal-digits!)))
-            (parse-number (slice src start pos)))))
-      (define
-        read-quoted
-        (fn
-          (quote-char)
-          (let
-            ((chars (list)))
-            (advance! 1)
-            (define
-              loop
-              (fn
-                ()
-                (cond
-                  ((>= pos src-len) nil)
-                  ((= (cur) "\\")
-                    (do
-                      (advance! 1)
-                      (when
-                        (< pos src-len)
-                        (let
-                          ((ch (cur)))
-                          (do
-                            (cond
-                              ((= ch "n") (append! chars "\n"))
-                              ((= ch "t") (append! chars "\t"))
-                              ((= ch "r") (append! chars "\r"))
-                              ((= ch "\\") (append! chars "\\"))
-                              ((= ch "'") (append! chars "'"))
-                              ((= ch "\"") (append! chars "\""))
-                              (else (append! chars ch)))
-                            (advance! 1))))
-                      (loop)))
-                  ((= (cur) quote-char) (advance! 1))
-                  (else
-                    (do (append! chars (cur)) (advance! 1) (loop))))))
-            (loop)
-            (join "" chars))))
-      (define
-        scan!
-        (fn
-          ()
-          (do
-            (skip-ws!)
-            (when
-              (< pos src-len)
-              (let
-                ((ch (cur)) (start pos))
-                (cond
-                  ((at? ":-")
-                    (do
-                      (dl-emit! "op" ":-" start)
-                      (advance! 2)
-                      (scan!)))
-                  ((at? "?-")
-                    (do
-                      (dl-emit! "op" "?-" start)
-                      (advance! 2)
-                      (scan!)))
-                  ((at? "<=")
-                    (do
-                      (dl-emit! "op" "<=" start)
-                      (advance! 2)
-                      (scan!)))
-                  ((at? ">=")
-                    (do
-                      (dl-emit! "op" ">=" start)
-                      (advance! 2)
-                      (scan!)))
-                  ((at? "!=")
-                    (do
-                      (dl-emit! "op" "!=" start)
-                      (advance! 2)
-                      (scan!)))
-                  ((dl-digit? ch)
-                    (do
-                      (dl-emit! "number" (read-number start) start)
-                      (scan!)))
-                  ((= ch "'")
-                    (do (dl-emit! "atom" (read-quoted "'") start) (scan!)))
-                  ((= ch "\"")
-                    (do (dl-emit! "string" (read-quoted "\"") start) (scan!)))
-                  ((dl-lower? ch)
-                    (do (dl-emit! "atom" (read-ident start) start) (scan!)))
-                  ((or (dl-upper? ch) (= ch "_"))
-                    (do (dl-emit! "var" (read-ident start) start) (scan!)))
-                  ((= ch "(")
-                    (do
-                      (dl-emit! "punct" "(" start)
-                      (advance! 1)
-                      (scan!)))
-                  ((= ch ")")
-                    (do
-                      (dl-emit! "punct" ")" start)
-                      (advance! 1)
-                      (scan!)))
-                  ((= ch ",")
-                    (do
-                      (dl-emit! "punct" "," start)
-                      (advance! 1)
-                      (scan!)))
-                  ((= ch ".")
-                    (do
-                      (dl-emit! "punct" "." start)
-                      (advance! 1)
-                      (scan!)))
-                  ((= ch "<")
-                    (do
-                      (dl-emit! "op" "<" start)
-                      (advance! 1)
-                      (scan!)))
-                  ((= ch ">")
-                    (do
-                      (dl-emit! "op" ">" start)
-                      (advance! 1)
-                      (scan!)))
-                  ((= ch "=")
-                    (do
-                      (dl-emit! "op" "=" start)
-                      (advance! 1)
-                      (scan!)))
-                  ((= ch "+")
-                    (do
-                      (dl-emit! "op" "+" start)
-                      (advance! 1)
-                      (scan!)))
-                  ((= ch "-")
-                    (do
-                      (dl-emit! "op" "-" start)
-                      (advance! 1)
-                      (scan!)))
-                  ((= ch "*")
-                    (do
-                      (dl-emit! "op" "*" start)
-                      (advance! 1)
-                      (scan!)))
-                  ((= ch "/")
-                    (do
-                      (dl-emit! "op" "/" start)
-                      (advance! 1)
-                      (scan!)))
-                  (else (do (advance! 1) (scan!)))))))))
-      (scan!)
-      (dl-emit! "eof" nil pos)
-      tokens)))

lib/datalog/unify.sx

@@ -1,159 +0,0 @@
-;; lib/datalog/unify.sx — unification + substitution for Datalog terms.
-;;
-;; Term taxonomy (after parsing):
-;;   variable  — SX symbol whose first char is uppercase A–Z or '_'.
-;;   constant  — SX symbol whose first char is lowercase a–z (atom name).
-;;   number    — numeric literal.
-;;   string    — string literal.
-;;   compound  — SX list (functor arg ... arg). In core Datalog these
-;;               only appear as arithmetic expressions (see Phase 4
-;;               safety analysis); compound-against-compound unification
-;;               is supported anyway for completeness.
-;;
-;; Substitutions are immutable dicts keyed by variable name (string).
-;; A failed unification returns nil; success returns the extended subst.
-
-(define dl-empty-subst (fn () {}))
-
-(define
-  dl-var?
-  (fn
-    (term)
-    (and
-      (symbol? term)
-      (let
-        ((name (symbol->string term)))
-        (and
-          (> (len name) 0)
-          (let
-            ((c (slice name 0 1)))
-            (or (and (>= c "A") (<= c "Z")) (= c "_"))))))))
-
-;; Walk: chase variable bindings until we hit a non-variable or an unbound
-;; variable. The result is either a non-variable term or an unbound var.
-(define
-  dl-walk
-  (fn
-    (term subst)
-    (if
-      (dl-var? term)
-      (let
-        ((name (symbol->string term)))
-        (if
-          (and (dict? subst) (has-key? subst name))
-          (dl-walk (get subst name) subst)
-          term))
-      term)))
-
-;; Bind a variable symbol to a value in subst, returning a new subst.
-(define
-  dl-bind
-  (fn (var-sym value subst) (assoc subst (symbol->string var-sym) value)))
-
-(define
-  dl-unify
-  (fn
-    (t1 t2 subst)
-    (if
-      (nil? subst)
-      nil
-      (let
-        ((u1 (dl-walk t1 subst)) (u2 (dl-walk t2 subst)))
-        (cond
-          ((dl-var? u1)
-            (cond
-              ((and (dl-var? u2) (= (symbol->string u1) (symbol->string u2)))
-                subst)
-              (else (dl-bind u1 u2 subst))))
-          ((dl-var? u2) (dl-bind u2 u1 subst))
-          ((and (list? u1) (list? u2))
-            (if
-              (= (len u1) (len u2))
-              (dl-unify-list u1 u2 subst 0)
-              nil))
-          ((and (number? u1) (number? u2)) (if (= u1 u2) subst nil))
-          ((and (string? u1) (string? u2)) (if (= u1 u2) subst nil))
-          ((and (symbol? u1) (symbol? u2))
-            (if (= (symbol->string u1) (symbol->string u2)) subst nil))
-          (else nil))))))
-
-(define
-  dl-unify-list
-  (fn
-    (a b subst i)
-    (cond
-      ((nil? subst) nil)
-      ((>= i (len a)) subst)
-      (else
-        (dl-unify-list
-          a
-          b
-          (dl-unify (nth a i) (nth b i) subst)
-          (+ i 1))))))
-
-;; Apply substitution: walk the term and recurse into lists.
-(define
-  dl-apply-subst
-  (fn
-    (term subst)
-    (let
-      ((w (dl-walk term subst)))
-      (if (list? w) (map (fn (x) (dl-apply-subst x subst)) w) w))))
-
-;; Ground? — true iff no free variables remain after walking.
-(define
-  dl-ground?
-  (fn
-    (term subst)
-    (let
-      ((w (dl-walk term subst)))
-      (cond
-        ((dl-var? w) false)
-        ((list? w) (dl-ground-list? w subst 0))
-        (else true)))))
-
-(define
-  dl-ground-list?
-  (fn
-    (xs subst i)
-    (cond
-      ((>= i (len xs)) true)
-      ((not (dl-ground? (nth xs i) subst)) false)
-      (else (dl-ground-list? xs subst (+ i 1))))))
-
-;; Return the list of variable names appearing in a term (deduped, in
-;; left-to-right order). Useful for safety analysis later.
-(define
-  dl-vars-of
-  (fn (term) (let ((seen (list))) (do (dl-vars-of-aux term seen) seen))))
-
-(define
-  dl-vars-of-aux
-  (fn
-    (term acc)
-    (cond
-      ((dl-var? term)
-        (let
-          ((name (symbol->string term)))
-          (when (not (dl-member? name acc)) (append! acc name))))
-      ((list? term) (dl-vars-of-list term acc 0))
-      (else nil))))
-
-(define
-  dl-vars-of-list
-  (fn
-    (xs acc i)
-    (when
-      (< i (len xs))
-      (do
-        (dl-vars-of-aux (nth xs i) acc)
-        (dl-vars-of-list xs acc (+ i 1))))))
-
-(define
-  dl-member?
-  (fn
-    (x xs)
-    (cond
-      ((= (len xs) 0) false)
-      ((= (first xs) x) true)
-      (else (dl-member? x (rest xs))))))

lib/guest/hm.sx

@@ -1,180 +0,0 @@
-;; lib/guest/hm.sx — Hindley-Milner type-inference foundations.
-;;
-;; Builds on lib/guest/match.sx (terms + unify) and ast.sx (canonical
-;; AST shapes). This file ships the ALGEBRA — types, schemes, free
-;; type-vars, generalize / instantiate, substitution composition — so a
-;; full Algorithm W (or J) can be assembled on top either inside this
-;; file or in a host-specific consumer (haskell/infer.sx,
-;; lib/ocaml/types.sx, …).
-;;
-;; Per the brief the second consumer for this step is OCaml-on-SX
-;; Phase 5 (paired sequencing). Until that lands, the algebra is the
-;; deliverable; the host-flavoured assembly (lambda / app / let
-;; inference rules with substitution threading) lives in the host.
-;;
-;; Types
-;; -----
-;; A type is a canonical match.sx term — type variables use mk-var,
-;; type constructors use mk-ctor:
-;;   (hm-tv NAME)              type variable
-;;   (hm-arrow A B)             A -> B
-;;   (hm-con NAME ARGS)         named n-ary constructor
-;;   (hm-int) / (hm-bool) / (hm-string)   primitive constructors
-;;
-;; Schemes
-;; -------
-;;   (hm-scheme VARS TYPE)        ∀ VARS . TYPE
-;;   (hm-monotype TYPE)           empty quantifier
-;;   (hm-scheme? S) (hm-scheme-vars S) (hm-scheme-type S)
-;;
-;; Free type variables
-;; -------------------
-;;   (hm-ftv TYPE)                names occurring in TYPE
-;;   (hm-ftv-scheme S)            free names (minus quantifiers)
-;;   (hm-ftv-env ENV)             free across an env (name -> scheme)
-;;
-;; Substitution
-;; ------------
-;;   (hm-apply SUBST TYPE)        substitute through a type
-;;   (hm-apply-scheme SUBST S)    leaves bound vars alone
-;;   (hm-apply-env SUBST ENV)
-;;   (hm-compose S2 S1)           apply S1 then S2
-;;
-;; Generalize / Instantiate
-;; ------------------------
-;;   (hm-generalize TYPE ENV)      → scheme over ftv(t) - ftv(env)
-;;   (hm-instantiate SCHEME COUNTER) → fresh-var instance
-;;   (hm-fresh-tv COUNTER)         → (:var "tN"), bumps COUNTER
-;;
-;; Inference (literal only — the rest of Algorithm W lives in the host)
-;; --------------------------------------------------------------------
-;;   (hm-infer-literal EXPR)       → {:subst {} :type T}
-;;
-;; A complete Algorithm W consumes this kit by assembling lambda / app
-;; / let rules in the host language file.
-
-(define hm-tv     (fn (name) (list :var name)))
-(define hm-con    (fn (name args) (list :ctor name args)))
-(define hm-arrow  (fn (a b) (hm-con "->" (list a b))))
-(define hm-int    (fn () (hm-con "Int" (list))))
-(define hm-bool   (fn () (hm-con "Bool" (list))))
-(define hm-string (fn () (hm-con "String" (list))))
-
-(define hm-scheme        (fn (vars t) (list :scheme vars t)))
-(define hm-monotype      (fn (t) (hm-scheme (list) t)))
-(define hm-scheme?       (fn (s) (and (list? s) (not (empty? s)) (= (first s) :scheme))))
-(define hm-scheme-vars   (fn (s) (nth s 1)))
-(define hm-scheme-type   (fn (s) (nth s 2)))
-
-(define
-  hm-fresh-tv
-  (fn (counter)
-    (let ((n (first counter)))
-      (begin
-        (set-nth! counter 0 (+ n 1))
-        (hm-tv (str "t" (+ n 1)))))))
-
-(define
-  hm-ftv-acc
-  (fn (t acc)
-    (cond
-      ((is-var? t)
-        (if (some (fn (n) (= n (var-name t))) acc) acc (cons (var-name t) acc)))
-      ((is-ctor? t)
-        (let ((a acc))
-          (begin
-            (for-each (fn (x) (set! a (hm-ftv-acc x a))) (ctor-args t))
-            a)))
-      (:else acc))))
-
-(define hm-ftv (fn (t) (hm-ftv-acc t (list))))
-
-(define
-  hm-ftv-scheme
-  (fn (s)
-    (let ((qs (hm-scheme-vars s))
-          (all (hm-ftv (hm-scheme-type s))))
-      (filter (fn (n) (not (some (fn (q) (= q n)) qs))) all))))
-
-(define
-  hm-ftv-env
-  (fn (env)
-    (let ((acc (list)))
-      (begin
-        (for-each
-          (fn (k)
-            (for-each
-              (fn (n)
-                (when (not (some (fn (m) (= m n)) acc))
-                  (set! acc (cons n acc))))
-              (hm-ftv-scheme (get env k))))
-          (keys env))
-        acc))))
-
-(define hm-apply (fn (subst t) (walk* t subst)))
-
-(define
-  hm-apply-scheme
-  (fn (subst s)
-    (let ((qs (hm-scheme-vars s))
-          (d {}))
-      (begin
-        (for-each
-          (fn (k)
-            (when (not (some (fn (q) (= q k)) qs))
-              (dict-set! d k (get subst k))))
-          (keys subst))
-        (hm-scheme qs (walk* (hm-scheme-type s) d))))))
-
-(define
-  hm-apply-env
-  (fn (subst env)
-    (let ((d {}))
-      (begin
-        (for-each
-          (fn (k) (dict-set! d k (hm-apply-scheme subst (get env k))))
-          (keys env))
-        d))))
-
-(define
-  hm-compose
-  (fn (s2 s1)
-    (let ((d {}))
-      (begin
-        (for-each (fn (k) (dict-set! d k (walk* (get s1 k) s2))) (keys s1))
-        (for-each
-          (fn (k) (when (not (has-key? d k)) (dict-set! d k (get s2 k))))
-          (keys s2))
-        d))))
-
-(define
-  hm-generalize
-  (fn (t env)
-    (let ((tvars (hm-ftv t))
-          (evars (hm-ftv-env env)))
-      (let ((qs (filter (fn (n) (not (some (fn (m) (= m n)) evars))) tvars)))
-        (hm-scheme qs t)))))
-
-(define
-  hm-instantiate
-  (fn (s counter)
-    (let ((qs (hm-scheme-vars s))
-          (subst {}))
-      (begin
-        (for-each
-          (fn (q) (set! subst (assoc subst q (hm-fresh-tv counter))))
-          qs)
-        (walk* (hm-scheme-type s) subst)))))
-
-;; Literal inference — the only AST kind whose typing rule is closed
-;; in the kit. Lambda / app / let live in host code so the host's own
-;; AST conventions stay untouched.
-(define
-  hm-infer-literal
-  (fn (expr)
-    (let ((v (ast-literal-value expr)))
-      (cond
-        ((number? v)  {:subst {} :type (hm-int)})
-        ((string? v)  {:subst {} :type (hm-string)})
-        ((boolean? v) {:subst {} :type (hm-bool)})
-        (:else (error (str "hm-infer-literal: unknown kind: " v)))))))

lib/guest/layout.sx

@@ -1,145 +0,0 @@
-;; lib/guest/layout.sx — configurable off-side / layout-sensitive lexer.
-;;
-;; Inserts virtual open / close / separator tokens based on indentation.
-;; Configurable enough to encode either the Haskell 98 layout rule (let /
-;; where / do / of opens a virtual brace at the next token's column) or
-;; a Python-ish indent / dedent rule (a colon at the end of a line opens
-;; a block at the next non-blank line's column).
-;;
-;; Token shape (input + output)
-;; ----------------------------
-;; Each token is a dict {:type :value :line :col …}. The kit reads
-;; only :type / :value / :line / :col and passes everything else
-;; through. The input stream MUST be free of newline filler tokens
-;; (preprocess them away with your tokenizer) — line breaks are detected
-;; by comparing :line of consecutive tokens.
-;;
-;; Config
-;; ------
-;;   :open-keywords    list of strings; a token whose :value matches
-;;                     opens a new layout block at the next token's
-;;                     column (Haskell: let/where/do/of).
-;;   :open-trailing-fn (fn (tok) -> bool) — alternative trigger that
-;;                     fires AFTER the token is emitted. Use for
-;;                     Python-style trailing `:`.
-;;   :open-token / :close-token / :sep-token
-;;                     templates {:type :value} merged with :line and
-;;                     :col when virtual tokens are emitted.
-;;   :explicit-open?   (fn (tok) -> bool) — if the next token after a
-;;                     trigger satisfies this, suppress virtual layout
-;;                     for that block (Haskell: `{`).
-;;   :module-prelude?  if true, wrap whole input in an implicit block
-;;                     at the first token's column (Haskell yes,
-;;                     Python no).
-;;
-;; Public entry
-;; ------------
-;;   (layout-pass cfg tokens) -> tokens with virtual layout inserted.
-
-(define
-  layout-mk-virtual
-  (fn (template line col)
-    (assoc (assoc template :line line) :col col)))
-
-(define
-  layout-is-open-kw?
-  (fn (tok open-kws)
-    (and (= (get tok :type) "reserved")
-         (some (fn (k) (= k (get tok :value))) open-kws))))
-
-(define
-  layout-pass
-  (fn (cfg tokens)
-    (let ((open-kws (get cfg :open-keywords))
-          (trailing-fn (get cfg :open-trailing-fn))
-          (open-tmpl (get cfg :open-token))
-          (close-tmpl (get cfg :close-token))
-          (sep-tmpl (get cfg :sep-token))
-          (mod-prelude? (get cfg :module-prelude?))
-          (expl?-fn (get cfg :explicit-open?))
-          (out (list))
-          (stack (list))
-          (n (len tokens))
-          (i 0)
-          (prev-line -1)
-          (pending-open false)
-          (just-opened false))
-      (define
-        emit-closes-while-greater
-        (fn (col line)
-          (when (and (not (empty? stack)) (> (first stack) col))
-            (do
-              (append! out (layout-mk-virtual close-tmpl line col))
-              (set! stack (rest stack))
-              (emit-closes-while-greater col line)))))
-      (define
-        emit-pending-open
-        (fn (line col)
-          (do
-            (append! out (layout-mk-virtual open-tmpl line col))
-            (set! stack (cons col stack))
-            (set! pending-open false)
-            (set! just-opened true))))
-      (define
-        layout-step
-        (fn ()
-          (when (< i n)
-            (let ((tok (nth tokens i)))
-              (let ((line (get tok :line)) (col (get tok :col)))
-                (cond
-                  (pending-open
-                    (cond
-                      ((and (not (= expl?-fn nil)) (expl?-fn tok))
-                        (do
-                          (set! pending-open false)
-                          (append! out tok)
-                          (set! prev-line line)
-                          (set! i (+ i 1))
-                          (layout-step)))
-                      (:else
-                        (do
-                          (emit-pending-open line col)
-                          (layout-step)))))
-                  (:else
-                    (let ((on-fresh-line? (and (> prev-line 0) (> line prev-line))))
-                      (do
-                        (when on-fresh-line?
-                          (let ((stack-before stack))
-                            (begin
-                              (emit-closes-while-greater col line)
-                              (when (and (not (empty? stack))
-                                         (= (first stack) col)
-                                         (not just-opened)
-                                         ;; suppress separator if a dedent fired
-                                         ;; — the dedent is itself the separator
-                                         (= (len stack) (len stack-before)))
-                                (append! out (layout-mk-virtual sep-tmpl line col))))))
-                        (set! just-opened false)
-                        (append! out tok)
-                        (set! prev-line line)
-                        (set! i (+ i 1))
-                        (cond
-                          ((layout-is-open-kw? tok open-kws)
-                            (set! pending-open true))
-                          ((and (not (= trailing-fn nil)) (trailing-fn tok))
-                            (set! pending-open true)))
-                        (layout-step))))))))))
-      (begin
-        ;; Module prelude: implicit layout block at the first token's column.
-        (when (and mod-prelude? (> n 0))
-          (let ((tok (nth tokens 0)))
-            (do
-              (append! out (layout-mk-virtual open-tmpl (get tok :line) (get tok :col)))
-              (set! stack (cons (get tok :col) stack))
-              (set! just-opened true))))
-        (layout-step)
-        ;; EOF: close every remaining block.
-        (define close-rest
-          (fn ()
-            (when (not (empty? stack))
-              (do
-                (append! out (layout-mk-virtual close-tmpl 0 0))
-                (set! stack (rest stack))
-                (close-rest)))))
-        (close-rest)
-        out))))

lib/guest/tests/hm.sx

@@ -1,89 +0,0 @@
-;; lib/guest/tests/hm.sx — exercises lib/guest/hm.sx algebra.
-
-(define ghm-test-pass 0)
-(define ghm-test-fail 0)
-(define ghm-test-fails (list))
-
-(define
-  ghm-test
-  (fn (name actual expected)
-    (if (= actual expected)
-      (set! ghm-test-pass (+ ghm-test-pass 1))
-      (begin
-        (set! ghm-test-fail (+ ghm-test-fail 1))
-        (append! ghm-test-fails {:name name :expected expected :actual actual})))))
-
-;; ── Type constructors ─────────────────────────────────────────────
-(ghm-test "tv"           (hm-tv "a") (list :var "a"))
-(ghm-test "int"          (hm-int)    (list :ctor "Int" (list)))
-(ghm-test "arrow"        (ctor-head (hm-arrow (hm-int) (hm-bool))) "->")
-(ghm-test "arrow-args-len" (len (ctor-args (hm-arrow (hm-int) (hm-bool)))) 2)
-
-;; ── Schemes ───────────────────────────────────────────────────────
-(ghm-test "scheme-vars"  (hm-scheme-vars (hm-scheme (list "a") (hm-tv "a"))) (list "a"))
-(ghm-test "monotype-vars" (hm-scheme-vars (hm-monotype (hm-int))) (list))
-(ghm-test "scheme?-yes"  (hm-scheme? (hm-monotype (hm-int))) true)
-(ghm-test "scheme?-no"   (hm-scheme? (hm-int)) false)
-
-;; ── Fresh tyvars ──────────────────────────────────────────────────
-(ghm-test "fresh-1"
-  (let ((c (list 0))) (var-name (hm-fresh-tv c))) "t1")
-(ghm-test "fresh-bumps"
-  (let ((c (list 5))) (begin (hm-fresh-tv c) (first c))) 6)
-
-;; ── Free type variables ──────────────────────────────────────────
-(ghm-test "ftv-int"      (hm-ftv (hm-int)) (list))
-(ghm-test "ftv-tv"       (hm-ftv (hm-tv "a")) (list "a"))
-(ghm-test "ftv-arrow"
-  (len (hm-ftv (hm-arrow (hm-tv "a") (hm-arrow (hm-tv "b") (hm-tv "a"))))) 2)
-(ghm-test "ftv-scheme-quantified"
-  (hm-ftv-scheme (hm-scheme (list "a") (hm-arrow (hm-tv "a") (hm-tv "b")))) (list "b"))
-(ghm-test "ftv-env"
-  (let ((env (assoc {} "f" (hm-monotype (hm-arrow (hm-tv "x") (hm-tv "y"))))))
-    (len (hm-ftv-env env))) 2)
-
-;; ── Substitution / apply / compose ───────────────────────────────
-(ghm-test "apply-tv"
-  (hm-apply (assoc {} "a" (hm-int)) (hm-tv "a")) (hm-int))
-(ghm-test "apply-arrow"
-  (ctor-head
-    (hm-apply (assoc {} "a" (hm-int))
-              (hm-arrow (hm-tv "a") (hm-tv "b")))) "->")
-(ghm-test "compose-1-then-2"
-  (var-name
-    (hm-apply
-      (hm-compose (assoc {} "b" (hm-tv "c")) (assoc {} "a" (hm-tv "b")))
-      (hm-tv "a"))) "c")
-
-;; ── Generalize / Instantiate ─────────────────────────────────────
-;;   forall a. a -> a   instantiated twice yields fresh vars each time
-(ghm-test "generalize-id"
-  (len (hm-scheme-vars (hm-generalize (hm-arrow (hm-tv "a") (hm-tv "a")) {}))) 1)
-
-(ghm-test "generalize-skips-env"
-  ;; ftv(t)={a,b}, ftv(env)={a}, qs={b}
-  (let ((env (assoc {} "x" (hm-monotype (hm-tv "a")))))
-    (len (hm-scheme-vars
-           (hm-generalize (hm-arrow (hm-tv "a") (hm-tv "b")) env)))) 1)
-
-(ghm-test "instantiate-fresh"
-  (let ((s (hm-scheme (list "a") (hm-arrow (hm-tv "a") (hm-tv "a"))))
-        (c (list 0)))
-    (let ((t1 (hm-instantiate s c)) (t2 (hm-instantiate s c)))
-      (not (= (var-name (first (ctor-args t1)))
-              (var-name (first (ctor-args t2)))))))
-  true)
-
-;; ── Inference (literal only) ─────────────────────────────────────
-(ghm-test "infer-int"
-  (ctor-head (get (hm-infer-literal (ast-literal 42)) :type)) "Int")
-(ghm-test "infer-string"
-  (ctor-head (get (hm-infer-literal (ast-literal "hi")) :type)) "String")
-(ghm-test "infer-bool"
-  (ctor-head (get (hm-infer-literal (ast-literal true)) :type)) "Bool")
-
-(define ghm-tests-run!
-  (fn ()
-    {:passed ghm-test-pass
-     :failed ghm-test-fail
-     :total  (+ ghm-test-pass ghm-test-fail)}))

lib/guest/tests/layout.sx

@@ -1,180 +0,0 @@
-;; lib/guest/tests/layout.sx — synthetic Python-ish off-side fixture.
-;;
-;; Exercises lib/guest/layout.sx with a config different from Haskell's
-;; (no module-prelude, layout opens via trailing `:` not via reserved
-;; keyword) to prove the kit isn't Haskell-shaped.
-
-(define glayout-test-pass 0)
-(define glayout-test-fail 0)
-(define glayout-test-fails (list))
-
-(define
-  glayout-test
-  (fn (name actual expected)
-    (if (= actual expected)
-      (set! glayout-test-pass (+ glayout-test-pass 1))
-      (begin
-        (set! glayout-test-fail (+ glayout-test-fail 1))
-        (append! glayout-test-fails {:name name :expected expected :actual actual})))))
-
-;; Convenience: build a token from {type value line col}.
-(define
-  glayout-tok
-  (fn (ty val line col)
-    {:type ty :value val :line line :col col}))
-
-;; Project a token list to ((type value) ...) for compact comparison.
-(define
-  glayout-shape
-  (fn (toks)
-    (map (fn (t) (list (get t :type) (get t :value))) toks)))
-
-;; ── Haskell-flavour: keyword opens block ─────────────────────────
-(define
-  glayout-haskell-cfg
-  {:open-keywords (list "let" "where" "do" "of")
-   :open-trailing-fn nil
-   :open-token   {:type "vlbrace" :value "{"}
-   :close-token  {:type "vrbrace" :value "}"}
-   :sep-token    {:type "vsemi"   :value ";"}
-   :module-prelude? false
-   :explicit-open? (fn (tok) (= (get tok :type) "lbrace"))})
-
-;;   do
-;;     a
-;;     b
-;;   c       ← outside the do-block
-(glayout-test "haskell-do-block"
-  (glayout-shape
-    (layout-pass
-      glayout-haskell-cfg
-      (list (glayout-tok "reserved" "do" 1 1)
-            (glayout-tok "ident" "a" 2 3)
-            (glayout-tok "ident" "b" 3 3)
-            (glayout-tok "ident" "c" 4 1))))
-  (list (list "reserved" "do")
-        (list "vlbrace" "{")
-        (list "ident" "a")
-        (list "vsemi" ";")
-        (list "ident" "b")
-        (list "vrbrace" "}")
-        (list "ident" "c")))
-
-;; Explicit `{` after `do` suppresses virtual layout.
-(glayout-test "haskell-explicit-brace"
-  (glayout-shape
-    (layout-pass
-      glayout-haskell-cfg
-      (list (glayout-tok "reserved" "do" 1 1)
-            (glayout-tok "lbrace" "{" 1 4)
-            (glayout-tok "ident" "a" 1 6)
-            (glayout-tok "rbrace" "}" 1 8))))
-  (list (list "reserved" "do")
-        (list "lbrace" "{")
-        (list "ident" "a")
-        (list "rbrace" "}")))
-
-;; Single-statement do-block on the same line.
-(glayout-test "haskell-do-inline"
-  (glayout-shape
-    (layout-pass
-      glayout-haskell-cfg
-      (list (glayout-tok "reserved" "do" 1 1)
-            (glayout-tok "ident" "a" 1 4))))
-  (list (list "reserved" "do")
-        (list "vlbrace" "{")
-        (list "ident" "a")
-        (list "vrbrace" "}")))
-
-;; Module-prelude: wrap whole input in implicit layout block at first
-;; tok's column.
-(glayout-test "haskell-module-prelude"
-  (glayout-shape
-    (layout-pass
-      (assoc glayout-haskell-cfg :module-prelude? true)
-      (list (glayout-tok "ident" "x" 1 1)
-            (glayout-tok "ident" "y" 2 1)
-            (glayout-tok "ident" "z" 3 1))))
-  (list (list "vlbrace" "{")
-        (list "ident" "x")
-        (list "vsemi" ";")
-        (list "ident" "y")
-        (list "vsemi" ";")
-        (list "ident" "z")
-        (list "vrbrace" "}")))
-
-;; ── Python-flavour: trailing `:` opens block ─────────────────────
-(define
-  glayout-python-cfg
-  {:open-keywords (list)
-   :open-trailing-fn (fn (tok) (and (= (get tok :type) "punct")
-                                    (= (get tok :value) ":")))
-   :open-token   {:type "indent" :value "INDENT"}
-   :close-token  {:type "dedent" :value "DEDENT"}
-   :sep-token    {:type "newline" :value "NEWLINE"}
-   :module-prelude? false
-   :explicit-open? nil})
-
-;;   if x:
-;;       a
-;;       b
-;;   c
-(glayout-test "python-if-block"
-  (glayout-shape
-    (layout-pass
-      glayout-python-cfg
-      (list (glayout-tok "reserved" "if" 1 1)
-            (glayout-tok "ident" "x" 1 4)
-            (glayout-tok "punct" ":" 1 5)
-            (glayout-tok "ident" "a" 2 5)
-            (glayout-tok "ident" "b" 3 5)
-            (glayout-tok "ident" "c" 4 1))))
-  (list (list "reserved" "if")
-        (list "ident" "x")
-        (list "punct" ":")
-        (list "indent" "INDENT")
-        (list "ident" "a")
-        (list "newline" "NEWLINE")
-        (list "ident" "b")
-        (list "dedent" "DEDENT")
-        (list "ident" "c")))
-
-;; Nested Python-style blocks.
-;;   def f():
-;;       if x:
-;;           a
-;;       b
-(glayout-test "python-nested"
-  (glayout-shape
-    (layout-pass
-      glayout-python-cfg
-      (list (glayout-tok "reserved" "def" 1 1)
-            (glayout-tok "ident" "f" 1 5)
-            (glayout-tok "punct" "(" 1 6)
-            (glayout-tok "punct" ")" 1 7)
-            (glayout-tok "punct" ":" 1 8)
-            (glayout-tok "reserved" "if" 2 5)
-            (glayout-tok "ident" "x" 2 8)
-            (glayout-tok "punct" ":" 2 9)
-            (glayout-tok "ident" "a" 3 9)
-            (glayout-tok "ident" "b" 4 5))))
-  (list (list "reserved" "def")
-        (list "ident" "f")
-        (list "punct" "(")
-        (list "punct" ")")
-        (list "punct" ":")
-        (list "indent" "INDENT")
-        (list "reserved" "if")
-        (list "ident" "x")
-        (list "punct" ":")
-        (list "indent" "INDENT")
-        (list "ident" "a")
-        (list "dedent" "DEDENT")
-        (list "ident" "b")
-        (list "dedent" "DEDENT")))
-
-(define glayout-tests-run!
-  (fn ()
-    {:passed glayout-test-pass
-     :failed glayout-test-fail
-     :total  (+ glayout-test-pass glayout-test-fail)}))

lib/minikanren/conda.sx

@@ -0,0 +1,42 @@
+;; lib/minikanren/conda.sx — Phase 5 piece A: `conda`, the soft-cut.
+;;
+;;   (conda (g0 g ...) (h0 h ...) ...)
+;;     — first clause whose head g0 produces ANY answer wins; ALL of g0's
+;;       answers are then conj'd with the rest of that clause; later
+;;       clauses are NOT tried.
+;;     — differs from condu only in not wrapping g0 in onceo: condu
+;;       commits to the SINGLE first answer, conda lets the head's full
+;;       answer-set flow into the rest of the clause.
+;;       (Reasoned Schemer chapter 10; Byrd 5.3.)
+
+(define
+  conda-try
+  (fn
+    (clauses s)
+    (cond
+      ((empty? clauses) mzero)
+      (:else
+        (let
+          ((cl (first clauses)))
+          (let
+            ((head-goal (first cl)) (rest-goals (rest cl)))
+            (let
+              ((peek (stream-take 1 (head-goal s))))
+              (if
+                (empty? peek)
+                (conda-try (rest clauses) s)
+                (mk-bind (head-goal s) (mk-conj-list rest-goals))))))))))
+
+(defmacro
+  conda
+  (&rest clauses)
+  (quasiquote
+    (fn
+      (s)
+      (conda-try
+        (list
+          (splice-unquote
+            (map
+              (fn (cl) (quasiquote (list (splice-unquote cl))))
+              clauses)))
+        s))))

lib/minikanren/conde.sx

@@ -0,0 +1,39 @@
+;; lib/minikanren/conde.sx — Phase 2 piece C: `conde`, the canonical
+;; miniKanren and-or form, with implicit Zzz inverse-eta delay so recursive
+;; relations like appendo terminate.
+;;
+;;   (conde (g1a g1b ...) (g2a g2b ...) ...)
+;;     ≡ (mk-disj (Zzz (mk-conj g1a g1b ...))
+;;                (Zzz (mk-conj g2a g2b ...)) ...)
+;;
+;; `Zzz g` wraps a goal expression in (fn (S) (fn () (g S))) so that
+;; `g`'s body isn't constructed until the surrounding fn is applied to a
+;; substitution AND the returned thunk is forced. This is what gives
+;; miniKanren its laziness — recursive goal definitions can be `(conde
+;; ... (... (recur ...)))` without infinite descent at construction time.
+;;
+;; Hygiene: the substitution parameter is gensym'd so that user goal
+;; expressions which themselves bind `s` (e.g. `(appendo l s ls)`) keep
+;; their lexical `s` and don't accidentally reference the wrapper's
+;; substitution. Without gensym, miniKanren relations that follow the
+;; common (l s ls) parameter convention are silently miscompiled.
+
+(defmacro
+  Zzz
+  (g)
+  (let
+    ((s-sym (gensym "zzz-s-")))
+    (quasiquote
+      (fn ((unquote s-sym)) (fn () ((unquote g) (unquote s-sym)))))))
+
+(defmacro
+  conde
+  (&rest clauses)
+  (quasiquote
+    (mk-disj
+      (splice-unquote
+        (map
+          (fn
+            (clause)
+            (quasiquote (Zzz (mk-conj (splice-unquote clause)))))
+          clauses)))))

lib/minikanren/condu.sx

@@ -0,0 +1,58 @@
+;; lib/minikanren/condu.sx — Phase 2 piece D: `condu` and `onceo`.
+;;
+;; Both are commitment forms (no backtracking into discarded options):
+;;
+;;   (onceo g)        — succeeds at most once: takes the first answer
+;;                      stream-take produces from (g s).
+;;
+;;   (condu (g0 g ...) (h0 h ...) ...)
+;;                    — first clause whose head goal succeeds wins; only
+;;                      the first answer of the head is propagated to the
+;;                      rest of that clause; later clauses are not tried.
+;;                      (Reasoned Schemer chapter 10; Byrd 5.4.)
+
+(define
+  onceo
+  (fn
+    (g)
+    (fn
+      (s)
+      (let
+        ((peek (stream-take 1 (g s))))
+        (if (empty? peek) mzero (unit (first peek)))))))
+
+;; condu-try — runtime walker over a list of clauses (each clause a list of
+;; goals). Forces the head with stream-take 1; if head fails, recurse to
+;; the next clause; if head succeeds, commits its single answer through
+;; the rest of the clause.
+(define
+  condu-try
+  (fn
+    (clauses s)
+    (cond
+      ((empty? clauses) mzero)
+      (:else
+        (let
+          ((cl (first clauses)))
+          (let
+            ((head-goal (first cl)) (rest-goals (rest cl)))
+            (let
+              ((peek (stream-take 1 (head-goal s))))
+              (if
+                (empty? peek)
+                (condu-try (rest clauses) s)
+                ((mk-conj-list rest-goals) (first peek))))))))))
+
+(defmacro
+  condu
+  (&rest clauses)
+  (quasiquote
+    (fn
+      (s)
+      (condu-try
+        (list
+          (splice-unquote
+            (map
+              (fn (cl) (quasiquote (list (splice-unquote cl))))
+              clauses)))
+        s))))

lib/minikanren/fresh.sx

@@ -0,0 +1,23 @@
+;; lib/minikanren/fresh.sx — Phase 2 piece B: `fresh` for introducing
+;; logic variables inside a goal body.
+;;
+;;   (fresh (x y z) goal1 goal2 ...)
+;;     ≡ (let ((x (make-var)) (y (make-var)) (z (make-var)))
+;;         (mk-conj goal1 goal2 ...))
+;;
+;; A macro rather than a function so user-named vars are real lexical
+;; bindings — which is also what miniKanren convention expects.
+;; The empty-vars form (fresh () goal ...) is just a goal grouping.
+
+(defmacro
+  fresh
+  (vars &rest goals)
+  (quasiquote
+    (let
+      (unquote (map (fn (v) (list v (list (quote make-var)))) vars))
+      (mk-conj (splice-unquote goals)))))
+
+;; call-fresh — functional alternative for code that builds goals
+;; programmatically:
+;;   ((call-fresh (fn (x) (== x 7))) empty-s) → ({:_.N 7})
+(define call-fresh (fn (f) (fn (s) ((f (make-var)) s))))

lib/minikanren/goals.sx

@@ -0,0 +1,58 @@
+;; lib/minikanren/goals.sx — Phase 2 piece B: core goals.
+;;
+;; A goal is a function (fn (s) → stream-of-substitutions).
+;; Goals built here:
+;;   succeed         — always returns (unit s)
+;;   fail            — always returns mzero
+;;   ==              — unifies two terms; succeeds with a singleton, else fails
+;;   ==-check        — opt-in occurs-checked equality
+;;   conj2 / mk-conj — sequential conjunction of goals
+;;   disj2 / mk-disj — interleaved disjunction of goals (raw — `conde` adds
+;;                     the implicit-conj-per-clause sugar in a later commit)
+
+(define succeed (fn (s) (unit s)))
+
+(define fail (fn (s) mzero))
+
+(define
+  ==
+  (fn
+    (u v)
+    (fn
+      (s)
+      (let ((s2 (mk-unify u v s))) (if (= s2 nil) mzero (unit s2))))))
+
+(define
+  ==-check
+  (fn
+    (u v)
+    (fn
+      (s)
+      (let ((s2 (mk-unify-check u v s))) (if (= s2 nil) mzero (unit s2))))))
+
+(define conj2 (fn (g1 g2) (fn (s) (mk-bind (g1 s) g2))))
+
+(define disj2 (fn (g1 g2) (fn (s) (mk-mplus (g1 s) (g2 s)))))
+
+;; Fold goals in a list. (mk-conj-list ()) ≡ succeed; (mk-disj-list ()) ≡ fail.
+(define
+  mk-conj-list
+  (fn
+    (gs)
+    (cond
+      ((empty? gs) succeed)
+      ((empty? (rest gs)) (first gs))
+      (:else (conj2 (first gs) (mk-conj-list (rest gs)))))))
+
+(define
+  mk-disj-list
+  (fn
+    (gs)
+    (cond
+      ((empty? gs) fail)
+      ((empty? (rest gs)) (first gs))
+      (:else (disj2 (first gs) (mk-disj-list (rest gs)))))))
+
+(define mk-conj (fn (&rest gs) (mk-conj-list gs)))
+
+(define mk-disj (fn (&rest gs) (mk-disj-list gs)))

lib/minikanren/nafc.sx

@@ -0,0 +1,24 @@
+;; lib/minikanren/nafc.sx — Phase 5 piece C: negation as finite failure.
+;;
+;;   (nafc g)
+;;     succeeds (yields the input substitution) if g has zero answers
+;;     against that substitution; fails (mzero) if g has at least one.
+;;
+;; Caveat: `nafc` is unsound under the open-world assumption. It only
+;; makes sense for goals over fully-ground terms, or with the explicit
+;; understanding that adding more facts could flip the answer. Use
+;; `(project (...) ...)` to ensure the relevant vars are ground first.
+;;
+;; Caveat 2: stream-take forces g for at least one answer; if g is
+;; infinitely-ground (say, a divergent search over an unbound list),
+;; nafc itself will diverge. Standard miniKanren limitation.
+
+(define
+  nafc
+  (fn
+    (g)
+    (fn
+      (s)
+      (let
+        ((peek (stream-take 1 (g s))))
+        (if (empty? peek) (unit s) mzero)))))

lib/minikanren/peano.sx

@@ -0,0 +1,35 @@
+;; lib/minikanren/peano.sx — Peano-encoded natural-number relations.
+;;
+;; Same encoding as `lengtho`: zero is the keyword `:z`; successors are
+;; `(:s n)`. So 3 = `(:s (:s (:s :z)))`. `(:z)` and `(:s ...)` are normal
+;; SX values that unify positionally — no special primitives needed.
+;;
+;; Peano arithmetic is the canonical miniKanren way to test addition /
+;; multiplication / less-than relationally without an FD constraint store.
+;; (CLP(FD) integers come in Phase 6.)
+
+(define zeroo (fn (n) (== n :z)))
+
+(define succ-of (fn (n m) (== m (list :s n))))
+
+(define
+  pluso
+  (fn
+    (a b c)
+    (conde
+      ((== a :z) (== b c))
+      ((fresh (a-1 c-1) (== a (list :s a-1)) (== c (list :s c-1)) (pluso a-1 b c-1))))))
+
+(define minuso (fn (a b c) (pluso b c a)))
+
+(define lteo (fn (a b) (fresh (k) (pluso a k b))))
+
+(define lto (fn (a b) (fresh (sa) (succ-of a sa) (lteo sa b))))
+
+(define
+  *o
+  (fn
+    (a b c)
+    (conde
+      ((== a :z) (== c :z))
+      ((fresh (a-1 ab-1) (== a (list :s a-1)) (*o a-1 b ab-1) (pluso b ab-1 c))))))

lib/minikanren/project.sx

@@ -0,0 +1,25 @@
+;; lib/minikanren/project.sx — Phase 5 piece B: `project`.
+;;
+;;   (project (x y) g1 g2 ...)
+;;     — rebinds each named var to (mk-walk* var s) within the body's
+;;       lexical scope, then runs the conjunction of the body goals on
+;;       the same substitution. Use to escape into regular SX (arithmetic,
+;;       string ops, host predicates) when you need a ground value.
+;;
+;; If any of the projected vars is still unbound at this point, the body
+;; sees the raw `(:var NAME)` term — that is intentional and lets you
+;; mix project with `(== ground? var)` patterns or with conda guards.
+;;
+;; Hygiene: substitution parameter is gensym'd so it doesn't capture user
+;; vars (`s` is a popular relation parameter name).
+
+(defmacro
+  project
+  (vars &rest goals)
+  (let
+    ((s-sym (gensym "proj-s-")))
+    (quasiquote
+      (fn
+        ((unquote s-sym))
+        ((let (unquote (map (fn (v) (list v (list (quote mk-walk*) v s-sym))) vars)) (mk-conj (splice-unquote goals)))
+          (unquote s-sym))))))

lib/minikanren/relations.sx

@@ -0,0 +1,67 @@
+;; lib/minikanren/relations.sx — Phase 4 standard relations.
+;;
+;; Programs use native SX lists as data. Relations decompose lists via the
+;; tagged cons-cell shape `(:cons h t)` because SX has no improper pairs;
+;; the unifier treats `(:cons h t)` and the native list `(h . t)` as
+;; equivalent, and `mk-walk*` flattens cons cells back to flat lists for
+;; reification.
+
+;; --- pair / list shape relations ---
+
+(define nullo (fn (l) (== l (list))))
+
+(define pairo (fn (p) (fresh (a d) (== p (mk-cons a d)))))
+
+(define caro (fn (p a) (fresh (d) (== p (mk-cons a d)))))
+
+(define cdro (fn (p d) (fresh (a) (== p (mk-cons a d)))))
+
+(define conso (fn (a d p) (== p (mk-cons a d))))
+
+(define firsto caro)
+(define resto cdro)
+
+(define
+  listo
+  (fn (l) (conde ((nullo l)) ((fresh (a d) (conso a d l) (listo d))))))
+
+;; --- appendo: the canary ---
+;;
+;; (appendo l s ls) — `ls` is the concatenation of `l` and `s`.
+;; Runs forwards (l, s known → ls), backwards (ls known → all (l, s) pairs),
+;; and bidirectionally (mix of bound + unbound).
+
+(define
+  appendo
+  (fn
+    (l s ls)
+    (conde
+      ((nullo l) (== s ls))
+      ((fresh (a d res) (conso a d l) (conso a res ls) (appendo d s res))))))
+
+;; --- membero ---
+;; (membero x l) — x appears (at least once) in l.
+
+(define
+  membero
+  (fn
+    (x l)
+    (conde
+      ((fresh (d) (conso x d l)))
+      ((fresh (a d) (conso a d l) (membero x d))))))
+
+(define
+  reverseo
+  (fn
+    (l r)
+    (conde
+      ((nullo l) (nullo r))
+      ((fresh (a d res-rev) (conso a d l) (reverseo d res-rev) (appendo res-rev (list a) r))))))
+
+(define
+  lengtho
+  (fn
+    (l n)
+    (conde
+      ((nullo l) (== n :z))
+      ((fresh (a d n-1) (conso a d l) (== n (list :s n-1)) (lengtho d n-1))))))

lib/minikanren/run.sx

@@ -0,0 +1,56 @@
+;; lib/minikanren/run.sx — Phase 3: drive a goal + reify the query var.
+;;
+;; reify-name N        — make the canonical "_.N" reified symbol.
+;; reify-s term rs     — walk term in rs, add a mapping from each fresh
+;;                       unbound var to its _.N name (left-to-right order).
+;; reify q s           — walk* q in s, build reify-s, walk* again to
+;;                       substitute reified names in.
+;; run-n n q-name g... — defmacro: bind q-name to a fresh var, conj goals,
+;;                       take ≤ n answers from the stream, reify each
+;;                       through q-name. n = -1 takes all (used by run*).
+;; run*                — defmacro: (run* q g...) ≡ (run-n -1 q g...)
+;; run                 — defmacro: (run n q g...) ≡ (run-n n q g...)
+;;                       The two-segment form is the standard TRS API.
+
+(define reify-name (fn (n) (make-symbol (str "_." n))))
+
+(define
+  reify-s
+  (fn
+    (term rs)
+    (let
+      ((w (mk-walk term rs)))
+      (cond
+        ((is-var? w) (extend (var-name w) (reify-name (len rs)) rs))
+        ((mk-list-pair? w) (reduce (fn (acc a) (reify-s a acc)) rs w))
+        (:else rs)))))
+
+(define
+  reify
+  (fn
+    (term s)
+    (let
+      ((w (mk-walk* term s)))
+      (let ((rs (reify-s w (empty-subst)))) (mk-walk* w rs)))))
+
+(defmacro
+  run-n
+  (n q-name &rest goals)
+  (quasiquote
+    (let
+      (((unquote q-name) (make-var)))
+      (map
+        (fn (s) (reify (unquote q-name) s))
+        (stream-take
+          (unquote n)
+          ((mk-conj (splice-unquote goals)) empty-s))))))
+
+(defmacro
+  run*
+  (q-name &rest goals)
+  (quasiquote (run-n -1 (unquote q-name) (splice-unquote goals))))
+
+(defmacro
+  run
+  (n q-name &rest goals)
+  (quasiquote (run-n (unquote n) (unquote q-name) (splice-unquote goals))))

lib/minikanren/stream.sx

@@ -0,0 +1,66 @@
+;; lib/minikanren/stream.sx — Phase 2 piece A: lazy streams of substitutions.
+;;
+;; SX has no improper pairs (cons requires a list cdr), so we use a
+;; tagged stream-cell shape for mature stream elements:
+;;
+;;   stream  ::= mzero                        empty (the SX empty list)
+;;             | (:s HEAD TAIL)               mature cell, TAIL is a stream
+;;             | thunk                        (fn () ...) → stream when forced
+;;
+;; HEAD is a substitution dict. TAIL is again a stream (possibly a thunk),
+;; which is what gives us laziness — mk-mplus can return a mature head with
+;; a thunk in the tail, deferring the rest of the search.
+
+(define mzero (list))
+
+(define s-cons (fn (h t) (list :s h t)))
+
+(define
+  s-cons?
+  (fn (s) (and (list? s) (not (empty? s)) (= (first s) :s))))
+
+(define s-car (fn (s) (nth s 1)))
+(define s-cdr (fn (s) (nth s 2)))
+
+(define unit (fn (s) (s-cons s mzero)))
+
+(define stream-pause? (fn (s) (and (not (list? s)) (callable? s))))
+
+;; mk-mplus — interleave two streams. If s1 is paused we suspend and
+;; swap (Reasoned Schemer "interleave"); otherwise mature-cons head with
+;; mk-mplus of the rest.
+(define
+  mk-mplus
+  (fn
+    (s1 s2)
+    (cond
+      ((empty? s1) s2)
+      ((stream-pause? s1) (fn () (mk-mplus s2 (s1))))
+      (:else (s-cons (s-car s1) (mk-mplus (s-cdr s1) s2))))))
+
+;; mk-bind — apply goal g to every substitution in stream s, mk-mplus-ing.
+(define
+  mk-bind
+  (fn
+    (s g)
+    (cond
+      ((empty? s) mzero)
+      ((stream-pause? s) (fn () (mk-bind (s) g)))
+      (:else (mk-mplus (g (s-car s)) (mk-bind (s-cdr s) g))))))
+
+;; stream-take — force up to n results out of a (possibly lazy) stream
+;; into a flat SX list of substitutions. n = -1 means take all.
+(define
+  stream-take
+  (fn
+    (n s)
+    (cond
+      ((= n 0) (list))
+      ((empty? s) (list))
+      ((stream-pause? s) (stream-take n (s)))
+      (:else
+        (cons
+          (s-car s)
+          (stream-take
+            (if (= n -1) -1 (- n 1))
+            (s-cdr s)))))))

lib/minikanren/tests/conda.sx

@@ -0,0 +1,75 @@
+;; lib/minikanren/tests/conda.sx — Phase 5 piece A tests for `conda`.
+
+;; --- conda commits to first non-failing head, keeps ALL its answers ---
+
+(mk-test
+  "conda-first-clause-keeps-all"
+  (run*
+    q
+    (conda
+      ((mk-disj (== q 1) (== q 2)))
+      ((== q 100))))
+  (list 1 2))
+
+(mk-test
+  "conda-skips-failing-head"
+  (run*
+    q
+    (conda
+      ((== 1 2))
+      ((mk-disj (== q 10) (== q 20)))))
+  (list 10 20))
+
+(mk-test
+  "conda-all-fail"
+  (run*
+    q
+    (conda ((== 1 2)) ((== 3 4))))
+  (list))
+
+(mk-test "conda-no-clauses" (run* q (conda)) (list))
+
+;; --- conda DIFFERS from condu: conda keeps all head answers ---
+
+(mk-test
+  "conda-vs-condu-divergence"
+  (list
+    (run*
+      q
+      (conda
+        ((mk-disj (== q 1) (== q 2)))
+        ((== q 100))))
+    (run*
+      q
+      (condu
+        ((mk-disj (== q 1) (== q 2)))
+        ((== q 100)))))
+  (list (list 1 2) (list 1)))
+
+;; --- conda head's rest-goals run on every head answer ---
+
+(mk-test
+  "conda-rest-goals-run-on-all-answers"
+  (run*
+    q
+    (fresh
+      (x r)
+      (conda
+        ((mk-disj (== x 1) (== x 2))
+          (== r (list :tag x))))
+      (== q r)))
+  (list (list :tag 1) (list :tag 2)))
+
+;; --- if rest-goals fail on a head answer, that head answer is filtered;
+;;     the clause does not fall through to next clauses (per soft-cut). ---
+
+(mk-test
+  "conda-rest-fails-no-fallthrough"
+  (run*
+    q
+    (conda
+      ((mk-disj (== q 1) (== q 2)) (== q 99))
+      ((== q 200))))
+  (list))
+
+(mk-tests-run!)

lib/minikanren/tests/conde.sx

@@ -0,0 +1,89 @@
+;; lib/minikanren/tests/conde.sx — Phase 2 piece C tests for `conde`.
+;;
+;; Note on ordering: conde clauses are wrapped in Zzz (inverse-eta delay),
+;; so applying the conde goal to a substitution returns thunks. mk-mplus
+;; suspends-and-swaps when its left operand is paused, giving fair
+;; interleaving — this is exactly what makes recursive relations work,
+;; but it does mean conde answers can interleave rather than appear in
+;; strict left-to-right clause order.
+
+;; --- single-clause conde ≡ conj of clause body ---
+
+(mk-test
+  "conde-one-clause"
+  (let ((q (mk-var "q"))) (run* q (conde ((== q 7)))))
+  (list 7))
+
+(mk-test
+  "conde-one-clause-multi-goals"
+  (let
+    ((q (mk-var "q")))
+    (run* q (conde ((fresh (x) (== x 5) (== q (list x x)))))))
+  (list (list 5 5)))
+
+;; --- multi-clause: produces one row per clause (interleaved) ---
+
+(mk-test
+  "conde-three-clauses-as-set"
+  (let
+    ((qs (run* q (conde ((== q 1)) ((== q 2)) ((== q 3))))))
+    (and
+      (= (len qs) 3)
+      (and
+        (some (fn (x) (= x 1)) qs)
+        (and
+          (some (fn (x) (= x 2)) qs)
+          (some (fn (x) (= x 3)) qs)))))
+  true)
+
+(mk-test
+  "conde-mixed-success-failure-as-set"
+  (let
+    ((qs (run* q (conde ((== q "a")) ((== 1 2)) ((== q "b"))))))
+    (and
+      (= (len qs) 2)
+      (and (some (fn (x) (= x "a")) qs) (some (fn (x) (= x "b")) qs))))
+  true)
+
+;; --- conde with conjuncts inside clauses ---
+
+(mk-test
+  "conde-clause-conj-as-set"
+  (let
+    ((rows (run* q (fresh (x y) (conde ((== x 1) (== y 10)) ((== x 2) (== y 20))) (== q (list x y))))))
+    (and
+      (= (len rows) 2)
+      (and
+        (some (fn (r) (= r (list 1 10))) rows)
+        (some (fn (r) (= r (list 2 20))) rows))))
+  true)
+
+;; --- nested conde ---
+
+(mk-test
+  "conde-nested-yields-three"
+  (let
+    ((qs (run* q (conde ((conde ((== q 1)) ((== q 2)))) ((== q 3))))))
+    (and
+      (= (len qs) 3)
+      (and
+        (some (fn (x) (= x 1)) qs)
+        (and
+          (some (fn (x) (= x 2)) qs)
+          (some (fn (x) (= x 3)) qs)))))
+  true)
+
+;; --- conde all clauses fail → empty stream ---
+
+(mk-test
+  "conde-all-fail"
+  (run*
+    q
+    (conde ((== 1 2)) ((== 3 4))))
+  (list))
+
+;; --- empty conde: no clauses ⇒ fail ---
+
+(mk-test "conde-no-clauses" (run* q (conde)) (list))
+
+(mk-tests-run!)

lib/minikanren/tests/condu.sx

@@ -0,0 +1,86 @@
+;; lib/minikanren/tests/condu.sx — Phase 2 piece D tests for `onceo` and `condu`.
+
+;; --- onceo: at most one answer ---
+
+(mk-test
+  "onceo-single-success-passes-through"
+  (let
+    ((q (mk-var "q")))
+    (let
+      ((res (stream-take 5 ((onceo (== q 7)) empty-s))))
+      (map (fn (s) (mk-walk q s)) res)))
+  (list 7))
+
+(mk-test
+  "onceo-multi-success-trimmed-to-one"
+  (let
+    ((q (mk-var "q")))
+    (let
+      ((res (stream-take 5 ((onceo (mk-disj (== q 1) (== q 2) (== q 3))) empty-s))))
+      (map (fn (s) (mk-walk q s)) res)))
+  (list 1))
+
+(mk-test
+  "onceo-failure-stays-failure"
+  ((onceo (== 1 2)) empty-s)
+  (list))
+
+(mk-test
+  "onceo-conde-trimmed"
+  (let
+    ((q (mk-var "q")))
+    (let
+      ((res (stream-take 5 ((onceo (conde ((== q "a")) ((== q "b")))) empty-s))))
+      (map (fn (s) (mk-walk q s)) res)))
+  (list "a"))
+
+;; --- condu: first clause with successful head wins ---
+
+(mk-test
+  "condu-first-clause-wins"
+  (let
+    ((q (mk-var "q")))
+    (let
+      ((res (stream-take 10 ((condu ((== q 1)) ((== q 2))) empty-s))))
+      (map (fn (s) (mk-walk q s)) res)))
+  (list 1))
+
+(mk-test
+  "condu-skips-failing-head"
+  (let
+    ((q (mk-var "q")))
+    (let
+      ((res (stream-take 10 ((condu ((== 1 2)) ((== q 100)) ((== q 200))) empty-s))))
+      (map (fn (s) (mk-walk q s)) res)))
+  (list 100))
+
+(mk-test
+  "condu-all-fail-empty"
+  ((condu ((== 1 2)) ((== 3 4)))
+    empty-s)
+  (list))
+
+(mk-test "condu-empty-clauses-fail" ((condu) empty-s) (list))
+
+;; --- condu commits head's first answer; rest-goals can still backtrack
+;;     within that committed substitution but cannot revisit other heads. ---
+
+(mk-test
+  "condu-head-onceo-rest-runs"
+  (let
+    ((q (mk-var "q")) (r (mk-var "r")))
+    (let
+      ((res (stream-take 10 ((condu ((mk-disj (== q 1) (== q 2)) (== r 99))) empty-s))))
+      (map (fn (s) (list (mk-walk q s) (mk-walk r s))) res)))
+  (list (list 1 99)))
+
+(mk-test
+  "condu-rest-goals-can-fail-the-clause"
+  (let
+    ((q (mk-var "q")))
+    (let
+      ((res (stream-take 10 ((condu ((== q 1) (== 2 3)) ((== q 99))) empty-s))))
+      (map (fn (s) (mk-walk q s)) res)))
+  (list))
+
+(mk-tests-run!)

lib/minikanren/tests/fresh.sx

@@ -0,0 +1,101 @@
+;; lib/minikanren/tests/fresh.sx — Phase 2 piece B tests for `fresh`.
+
+;; --- empty fresh: pure goal grouping ---
+
+(mk-test
+  "fresh-empty-vars-equiv-conj"
+  (stream-take 5 ((fresh () (== 1 1)) empty-s))
+  (list empty-s))
+
+(mk-test
+  "fresh-empty-vars-no-goals-is-succeed"
+  (stream-take 5 ((fresh ()) empty-s))
+  (list empty-s))
+
+;; --- single var ---
+
+(mk-test
+  "fresh-one-var-bound"
+  (let
+    ((s (first (stream-take 5 ((fresh (x) (== x 7)) empty-s)))))
+    (first (vals s)))
+  7)
+
+;; --- multiple vars + multiple goals ---
+
+(mk-test
+  "fresh-two-vars-three-goals"
+  (let
+    ((q (mk-var "q"))
+      (g
+        (fresh
+          (x y)
+          (== x 10)
+          (== y 20)
+          (== q (list x y)))))
+    (mk-walk* q (first (stream-take 5 (g empty-s)))))
+  (list 10 20))
+
+(mk-test
+  "fresh-three-vars"
+  (let
+    ((q (mk-var "q"))
+      (g
+        (fresh
+          (a b c)
+          (== a 1)
+          (== b 2)
+          (== c 3)
+          (== q (list a b c)))))
+    (mk-walk* q (first (stream-take 5 (g empty-s)))))
+  (list 1 2 3))
+
+;; --- fresh interacts with disj ---
+
+(mk-test
+  "fresh-with-disj"
+  (let
+    ((q (mk-var "q")))
+    (let
+      ((g (fresh (x) (mk-disj (== x 1) (== x 2)) (== q x))))
+      (let
+        ((res (stream-take 5 (g empty-s))))
+        (map (fn (s) (mk-walk q s)) res))))
+  (list 1 2))
+
+;; --- nested fresh ---
+
+(mk-test
+  "fresh-nested"
+  (let
+    ((q (mk-var "q"))
+      (g
+        (fresh
+          (x)
+          (fresh
+            (y)
+            (== x 1)
+            (== y 2)
+            (== q (list x y))))))
+    (mk-walk* q (first (stream-take 5 (g empty-s)))))
+  (list 1 2))
+
+;; --- call-fresh (functional alternative) ---
+
+(mk-test
+  "call-fresh-binds-and-walks"
+  (let
+    ((s (first (stream-take 5 ((call-fresh (fn (x) (== x 99))) empty-s)))))
+    (first (vals s)))
+  99)
+
+(mk-test
+  "call-fresh-distinct-from-outer-vars"
+  (let
+    ((q (mk-var "q")))
+    (let
+      ((g (call-fresh (fn (x) (mk-conj (== x 5) (== q (list x x)))))))
+      (mk-walk* q (first (stream-take 5 (g empty-s))))))
+  (list 5 5))
+
+(mk-tests-run!)

lib/minikanren/tests/goals.sx

@@ -0,0 +1,260 @@
+;; lib/minikanren/tests/goals.sx — Phase 2 tests for stream.sx + goals.sx.
+;;
+;; Streams use a tagged shape internally (`(:s head tail)`) so that mature
+;; cells can have thunk tails — SX has no improper pairs. Test assertions
+;; therefore stream-take into a plain SX list, or check goal effects via
+;; mk-walk on the resulting subst, instead of inspecting raw streams.
+
+;; --- stream-take base cases (input streams use s-cons / mzero) ---
+
+(mk-test
+  "stream-take-zero-from-mature"
+  (stream-take 0 (s-cons (empty-subst) mzero))
+  (list))
+
+(mk-test "stream-take-from-mzero" (stream-take 5 mzero) (list))
+
+(mk-test
+  "stream-take-mature-pair"
+  (stream-take 5 (s-cons :a (s-cons :b mzero)))
+  (list :a :b))
+
+(mk-test
+  "stream-take-fewer-than-available"
+  (stream-take 1 (s-cons :a (s-cons :b mzero)))
+  (list :a))
+
+(mk-test
+  "stream-take-all-with-neg-1"
+  (stream-take -1 (s-cons :a (s-cons :b (s-cons :c mzero))))
+  (list :a :b :c))
+
+;; --- stream-take forces immature thunks ---
+
+(mk-test
+  "stream-take-forces-thunk"
+  (stream-take 5 (fn () (s-cons :x mzero)))
+  (list :x))
+
+(mk-test
+  "stream-take-forces-nested-thunks"
+  (stream-take 5 (fn () (fn () (s-cons :y mzero))))
+  (list :y))
+
+;; --- mk-mplus interleaves ---
+
+(mk-test
+  "mplus-empty-left"
+  (stream-take 5 (mk-mplus mzero (s-cons :r mzero)))
+  (list :r))
+
+(mk-test
+  "mplus-empty-right"
+  (stream-take 5 (mk-mplus (s-cons :l mzero) mzero))
+  (list :l))
+
+(mk-test
+  "mplus-mature-mature"
+  (stream-take
+    5
+    (mk-mplus (s-cons :a (s-cons :b mzero)) (s-cons :c (s-cons :d mzero))))
+  (list :a :b :c :d))
+
+(mk-test
+  "mplus-with-paused-left-swaps"
+  (stream-take
+    5
+    (mk-mplus
+      (fn () (s-cons :a (s-cons :b mzero)))
+      (s-cons :c (s-cons :d mzero))))
+  (list :c :d :a :b))
+
+;; --- mk-bind ---
+
+(mk-test
+  "bind-empty-stream"
+  (stream-take 5 (mk-bind mzero (fn (s) (unit s))))
+  (list))
+
+(mk-test
+  "bind-singleton-identity"
+  (stream-take
+    5
+    (mk-bind (s-cons 5 mzero) (fn (x) (unit x))))
+  (list 5))
+
+(mk-test
+  "bind-flat-multi"
+  (stream-take
+    10
+    (mk-bind
+      (s-cons 1 (s-cons 2 mzero))
+      (fn (x) (s-cons x (s-cons (* x 10) mzero)))))
+  (list 1 10 2 20))
+
+(mk-test
+  "bind-fail-prunes-some"
+  (stream-take
+    10
+    (mk-bind
+      (s-cons 1 (s-cons 2 (s-cons 3 mzero)))
+      (fn (x) (if (= x 2) mzero (unit x)))))
+  (list 1 3))
+
+;; --- core goals: succeed / fail ---
+
+(mk-test
+  "succeed-yields-singleton"
+  (stream-take 5 (succeed empty-s))
+  (list empty-s))
+
+(mk-test "fail-yields-mzero" (stream-take 5 (fail empty-s)) (list))
+
+;; --- == ---
+
+(mk-test
+  "eq-ground-success"
+  (stream-take 5 ((== 1 1) empty-s))
+  (list empty-s))
+
+(mk-test
+  "eq-ground-failure"
+  (stream-take 5 ((== 1 2) empty-s))
+  (list))
+
+(mk-test
+  "eq-binds-var"
+  (let
+    ((x (mk-var "x")))
+    (mk-walk
+      x
+      (first (stream-take 5 ((== x 7) empty-s)))))
+  7)
+
+(mk-test
+  "eq-list-success"
+  (let
+    ((x (mk-var "x")))
+    (mk-walk
+      x
+      (first
+        (stream-take
+          5
+          ((== x (list 1 2)) empty-s)))))
+  (list 1 2))
+
+(mk-test
+  "eq-list-mismatch-fails"
+  (stream-take
+    5
+    ((== (list 1 2) (list 1 3)) empty-s))
+  (list))
+
+;; --- conj2 / mk-conj ---
+
+(mk-test
+  "conj2-both-bind"
+  (let
+    ((x (mk-var "x")) (y (mk-var "y")))
+    (let
+      ((s (first (stream-take 5 ((conj2 (== x 1) (== y 2)) empty-s)))))
+      (list (mk-walk x s) (mk-walk y s))))
+  (list 1 2))
+
+(mk-test
+  "conj2-conflict-empty"
+  (let
+    ((x (mk-var "x")))
+    (stream-take
+      5
+      ((conj2 (== x 1) (== x 2)) empty-s)))
+  (list))
+
+(mk-test
+  "conj-empty-is-succeed"
+  (stream-take 5 ((mk-conj) empty-s))
+  (list empty-s))
+
+(mk-test
+  "conj-single-is-goal"
+  (let
+    ((x (mk-var "x")))
+    (mk-walk
+      x
+      (first
+        (stream-take 5 ((mk-conj (== x 99)) empty-s)))))
+  99)
+
+(mk-test
+  "conj-three-bindings"
+  (let
+    ((x (mk-var "x")) (y (mk-var "y")) (z (mk-var "z")))
+    (let
+      ((s (first (stream-take 5 ((mk-conj (== x 1) (== y 2) (== z 3)) empty-s)))))
+      (list (mk-walk x s) (mk-walk y s) (mk-walk z s))))
+  (list 1 2 3))
+
+;; --- disj2 / mk-disj ---
+
+(mk-test
+  "disj2-both-succeed"
+  (let
+    ((q (mk-var "q")))
+    (let
+      ((res (stream-take 5 ((disj2 (== q 1) (== q 2)) empty-s))))
+      (map (fn (s) (mk-walk q s)) res)))
+  (list 1 2))
+
+(mk-test
+  "disj2-fail-or-succeed"
+  (let
+    ((q (mk-var "q")))
+    (let
+      ((res (stream-take 5 ((disj2 fail (== q 5)) empty-s))))
+      (map (fn (s) (mk-walk q s)) res)))
+  (list 5))
+
+(mk-test
+  "disj-empty-is-fail"
+  (stream-take 5 ((mk-disj) empty-s))
+  (list))
+
+(mk-test
+  "disj-three-clauses"
+  (let
+    ((q (mk-var "q")))
+    (let
+      ((res (stream-take 5 ((mk-disj (== q "a") (== q "b") (== q "c")) empty-s))))
+      (map (fn (s) (mk-walk q s)) res)))
+  (list "a" "b" "c"))
+
+;; --- conj/disj nesting ---
+
+(mk-test
+  "disj-of-conj"
+  (let
+    ((x (mk-var "x")) (y (mk-var "y")))
+    (let
+      ((res (stream-take 5 ((mk-disj (mk-conj (== x 1) (== y 2)) (mk-conj (== x 3) (== y 4))) empty-s))))
+      (map (fn (s) (list (mk-walk x s) (mk-walk y s))) res)))
+  (list (list 1 2) (list 3 4)))
+
+;; --- ==-check ---
+
+(mk-test
+  "eq-check-no-occurs-fails"
+  (let
+    ((x (mk-var "x")))
+    (stream-take 5 ((==-check x (list 1 x)) empty-s)))
+  (list))
+
+(mk-test
+  "eq-check-no-occurs-non-occurring-succeeds"
+  (let
+    ((x (mk-var "x")))
+    (mk-walk
+      x
+      (first (stream-take 5 ((==-check x 5) empty-s)))))
+  5)
+
+(mk-tests-run!)

lib/minikanren/tests/nafc.sx

@@ -0,0 +1,50 @@
+;; lib/minikanren/tests/nafc.sx — Phase 5 piece C tests for `nafc`.
+
+(mk-test
+  "nafc-failed-goal-succeeds"
+  (run* q (nafc (== 1 2)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "nafc-successful-goal-fails"
+  (run* q (nafc (== 1 1)))
+  (list))
+
+(mk-test
+  "nafc-double-negation"
+  (run* q (nafc (nafc (== 1 1))))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "nafc-with-conde-no-clauses-succeed"
+  (run*
+    q
+    (nafc
+      (conde ((== 1 2)) ((== 3 4)))))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "nafc-with-conde-some-clause-succeeds-fails"
+  (run*
+    q
+    (nafc
+      (conde ((== 1 1)) ((== 3 4)))))
+  (list))
+
+;; --- composing nafc with == as a guard ---
+
+(mk-test
+  "nafc-as-guard"
+  (run*
+    q
+    (fresh (x) (== x 5) (nafc (== x 99)) (== q x)))
+  (list 5))
+
+(mk-test
+  "nafc-guard-blocking"
+  (run*
+    q
+    (fresh (x) (== x 5) (nafc (== x 5)) (== q x)))
+  (list))
+
+(mk-tests-run!)

lib/minikanren/tests/peano.sx

@@ -0,0 +1,119 @@
+;; lib/minikanren/tests/peano.sx — Peano arithmetic.
+;;
+;; Builds Peano numbers via a host-side helper so tests stay readable.
+;; (mk-nat 3) → (:s (:s (:s :z))).
+
+(define
+  mk-nat
+  (fn (n) (if (= n 0) :z (list :s (mk-nat (- n 1))))))
+
+;; --- zeroo ---
+
+(mk-test
+  "zeroo-zero-succeeds"
+  (run* q (zeroo :z))
+  (list (make-symbol "_.0")))
+(mk-test
+  "zeroo-non-zero-fails"
+  (run* q (zeroo (mk-nat 1)))
+  (list))
+
+;; --- pluso forward ---
+
+(mk-test
+  "pluso-forward-2-3"
+  (run* q (pluso (mk-nat 2) (mk-nat 3) q))
+  (list (mk-nat 5)))
+
+(mk-test "pluso-forward-zero-zero" (run* q (pluso :z :z q)) (list :z))
+
+(mk-test
+  "pluso-forward-zero-n"
+  (run* q (pluso :z (mk-nat 4) q))
+  (list (mk-nat 4)))
+
+(mk-test
+  "pluso-forward-n-zero"
+  (run* q (pluso (mk-nat 4) :z q))
+  (list (mk-nat 4)))
+
+;; --- pluso backward ---
+
+(mk-test
+  "pluso-recover-augend"
+  (run* q (pluso q (mk-nat 2) (mk-nat 5)))
+  (list (mk-nat 3)))
+
+(mk-test
+  "pluso-recover-addend"
+  (run* q (pluso (mk-nat 2) q (mk-nat 5)))
+  (list (mk-nat 3)))
+
+(mk-test
+  "pluso-enumerate-pairs-summing-to-3"
+  (run*
+    q
+    (fresh (a b) (pluso a b (mk-nat 3)) (== q (list a b))))
+  (list
+    (list :z (mk-nat 3))
+    (list (mk-nat 1) (mk-nat 2))
+    (list (mk-nat 2) (mk-nat 1))
+    (list (mk-nat 3) :z)))
+
+;; --- minuso ---
+
+(mk-test
+  "minuso-5-2-3"
+  (run* q (minuso (mk-nat 5) (mk-nat 2) q))
+  (list (mk-nat 3)))
+
+(mk-test
+  "minuso-n-n-zero"
+  (run* q (minuso (mk-nat 7) (mk-nat 7) q))
+  (list :z))
+
+;; --- *o ---
+
+(mk-test
+  "times-2-3"
+  (run* q (*o (mk-nat 2) (mk-nat 3) q))
+  (list (mk-nat 6)))
+
+(mk-test
+  "times-zero-anything-zero"
+  (run* q (*o :z (mk-nat 99) q))
+  (list :z))
+
+(mk-test
+  "times-3-4"
+  (run* q (*o (mk-nat 3) (mk-nat 4) q))
+  (list (mk-nat 12)))
+
+;; --- lteo / lto ---
+
+(mk-test
+  "lteo-success"
+  (run 1 q (lteo (mk-nat 2) (mk-nat 5)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "lteo-equal-success"
+  (run 1 q (lteo (mk-nat 3) (mk-nat 3)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "lteo-greater-fails"
+  (run* q (lteo (mk-nat 5) (mk-nat 2)))
+  (list))
+
+(mk-test
+  "lto-strict-success"
+  (run 1 q (lto (mk-nat 2) (mk-nat 5)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "lto-equal-fails"
+  (run* q (lto (mk-nat 3) (mk-nat 3)))
+  (list))
+
+(mk-tests-run!)

lib/minikanren/tests/project.sx

@@ -0,0 +1,60 @@
+;; lib/minikanren/tests/project.sx — Phase 5 piece B tests for `project`.
+
+;; --- project rebinds vars to ground values for SX use ---
+
+(mk-test
+  "project-square-via-host"
+  (run* q (fresh (n) (== n 5) (project (n) (== q (* n n)))))
+  (list 25))
+
+(mk-test
+  "project-multi-vars"
+  (run*
+    q
+    (fresh
+      (a b)
+      (== a 3)
+      (== b 4)
+      (project (a b) (== q (+ a b)))))
+  (list 7))
+
+(mk-test
+  "project-with-string-host-op"
+  (run* q (fresh (s) (== s "hello") (project (s) (== q (str s "!")))))
+  (list "hello!"))
+
+;; --- project nested inside conde ---
+
+(mk-test
+  "project-inside-conde"
+  (run*
+    q
+    (fresh
+      (n)
+      (conde ((== n 3)) ((== n 4)))
+      (project (n) (== q (* n 10)))))
+  (list 30 40))
+
+;; --- project body can be multiple goals (mk-conj'd) ---
+
+(mk-test
+  "project-multi-goal-body"
+  (run*
+    q
+    (fresh
+      (n)
+      (== n 7)
+      (project (n) (== q (+ n 1)) (== q (+ n 1)))))
+  (list 8))
+
+(mk-test
+  "project-multi-goal-body-conflict"
+  (run*
+    q
+    (fresh
+      (n)
+      (== n 7)
+      (project (n) (== q (+ n 1)) (== q (+ n 2)))))
+  (list))
+
+(mk-tests-run!)

lib/minikanren/tests/relations.sx

@@ -0,0 +1,227 @@
+;; lib/minikanren/tests/relations.sx — Phase 4 standard relations.
+;;
+;; Includes the classic miniKanren canaries: appendo forwards / backwards /
+;; bidirectionally, membero, listo enumeration.
+
+;; --- nullo / pairo ---
+
+(mk-test
+  "nullo-empty-succeeds"
+  (run* q (nullo (list)))
+  (list (make-symbol "_.0")))
+
+(mk-test "nullo-non-empty-fails" (run* q (nullo (list 1))) (list))
+
+(mk-test
+  "pairo-non-empty-succeeds"
+  (run* q (pairo (list 1 2)))
+  (list (make-symbol "_.0")))
+
+(mk-test "pairo-empty-fails" (run* q (pairo (list))) (list))
+
+;; --- caro / cdro / firsto / resto ---
+
+(mk-test
+  "caro-extracts-head"
+  (run* q (caro (list 1 2 3) q))
+  (list 1))
+
+(mk-test
+  "cdro-extracts-tail"
+  (run* q (cdro (list 1 2 3) q))
+  (list (list 2 3)))
+
+(mk-test
+  "firsto-alias-of-caro"
+  (run* q (firsto (list 10 20) q))
+  (list 10))
+
+(mk-test
+  "resto-alias-of-cdro"
+  (run* q (resto (list 10 20) q))
+  (list (list 20)))
+
+(mk-test
+  "caro-cdro-build"
+  (run*
+    q
+    (fresh
+      (h t)
+      (caro (list 1 2 3) h)
+      (cdro (list 1 2 3) t)
+      (== q (list h t))))
+  (list (list 1 (list 2 3))))
+
+;; --- conso ---
+
+(mk-test
+  "conso-forward"
+  (run* q (conso 0 (list 1 2 3) q))
+  (list (list 0 1 2 3)))
+
+(mk-test
+  "conso-extract-head"
+  (run*
+    q
+    (conso
+      q
+      (list 2 3)
+      (list 1 2 3)))
+  (list 1))
+
+(mk-test
+  "conso-extract-tail"
+  (run* q (conso 1 q (list 1 2 3)))
+  (list (list 2 3)))
+
+;; --- listo ---
+
+(mk-test
+  "listo-empty-succeeds"
+  (run* q (listo (list)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "listo-finite-list-succeeds"
+  (run* q (listo (list 1 2 3)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "listo-enumerates-shapes"
+  (run 3 q (listo q))
+  (list
+    (list)
+    (list (make-symbol "_.0"))
+    (list (make-symbol "_.0") (make-symbol "_.1"))))
+
+;; --- appendo: the canary ---
+
+(mk-test
+  "appendo-forward-simple"
+  (run*
+    q
+    (appendo (list 1 2) (list 3 4) q))
+  (list (list 1 2 3 4)))
+
+(mk-test
+  "appendo-forward-empty-l"
+  (run* q (appendo (list) (list 3 4) q))
+  (list (list 3 4)))
+
+(mk-test
+  "appendo-forward-empty-s"
+  (run* q (appendo (list 1 2) (list) q))
+  (list (list 1 2)))
+
+(mk-test
+  "appendo-recovers-tail"
+  (run*
+    q
+    (appendo
+      (list 1 2)
+      q
+      (list 1 2 3 4)))
+  (list (list 3 4)))
+
+(mk-test
+  "appendo-recovers-prefix"
+  (run*
+    q
+    (appendo
+      q
+      (list 3 4)
+      (list 1 2 3 4)))
+  (list (list 1 2)))
+
+(mk-test
+  "appendo-backward-all-splits"
+  (run*
+    q
+    (fresh
+      (l s)
+      (appendo l s (list 1 2 3))
+      (== q (list l s))))
+  (list
+    (list (list) (list 1 2 3))
+    (list (list 1) (list 2 3))
+    (list (list 1 2) (list 3))
+    (list (list 1 2 3) (list))))
+
+(mk-test
+  "appendo-empty-empty-empty"
+  (run* q (appendo (list) (list) q))
+  (list (list)))
+
+;; --- membero ---
+
+(mk-test
+  "membero-element-present"
+  (run
+    1
+    q
+    (membero 2 (list 1 2 3)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "membero-element-absent-empty"
+  (run* q (membero 99 (list 1 2 3)))
+  (list))
+
+(mk-test
+  "membero-enumerates"
+  (run* q (membero q (list "a" "b" "c")))
+  (list "a" "b" "c"))
+
+;; --- reverseo ---
+
+(mk-test
+  "reverseo-forward"
+  (run* q (reverseo (list 1 2 3) q))
+  (list (list 3 2 1)))
+
+(mk-test "reverseo-empty" (run* q (reverseo (list) q)) (list (list)))
+
+(mk-test
+  "reverseo-singleton"
+  (run* q (reverseo (list 42) q))
+  (list (list 42)))
+
+(mk-test
+  "reverseo-five"
+  (run*
+    q
+    (reverseo (list 1 2 3 4 5) q))
+  (list (list 5 4 3 2 1)))
+
+(mk-test
+  "reverseo-backward-one"
+  (run 1 q (reverseo q (list 1 2 3)))
+  (list (list 3 2 1)))
+
+(mk-test
+  "reverseo-round-trip"
+  (run*
+    q
+    (fresh (mid) (reverseo (list "a" "b" "c") mid) (reverseo mid q)))
+  (list (list "a" "b" "c")))
+
+;; --- lengtho (Peano-style) ---
+
+(mk-test "lengtho-empty-is-z" (run* q (lengtho (list) q)) (list :z))
+
+(mk-test
+  "lengtho-of-3"
+  (run* q (lengtho (list "a" "b" "c") q))
+  (list (list :s (list :s (list :s :z)))))
+
+(mk-test
+  "lengtho-empty-from-zero"
+  (run 1 q (lengtho q :z))
+  (list (list)))
+
+(mk-test
+  "lengtho-enumerates-of-length-2"
+  (run 1 q (lengtho q (list :s (list :s :z))))
+  (list (list (make-symbol "_.0") (make-symbol "_.1"))))
+
+(mk-tests-run!)

lib/minikanren/tests/run.sx

@@ -0,0 +1,114 @@
+;; lib/minikanren/tests/run.sx — Phase 3 tests for run* / run / reify.
+
+;; --- canonical TRS one-liners ---
+
+(mk-test "run*-eq-one" (run* q (== q 1)) (list 1))
+(mk-test "run*-eq-string" (run* q (== q "hello")) (list "hello"))
+(mk-test "run*-eq-symbol" (run* q (== q (quote sym))) (list (quote sym)))
+(mk-test "run*-fail-empty" (run* q (== 1 2)) (list))
+
+;; --- run with a count ---
+
+(mk-test
+  "run-3-of-many"
+  (run
+    3
+    q
+    (conde
+      ((== q 1))
+      ((== q 2))
+      ((== q 3))
+      ((== q 4))
+      ((== q 5))))
+  (list 1 2 3))
+
+(mk-test "run-zero-empty" (run 0 q (== q 1)) (list))
+
+(mk-test
+  "run-1-takes-one"
+  (run 1 q (conde ((== q "a")) ((== q "b"))))
+  (list "a"))
+
+;; --- reification: unbound vars get _.N left-to-right ---
+
+(mk-test
+  "reify-single-unbound"
+  (run* q (fresh (x) (== q x)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "reify-pair-unbound"
+  (run* q (fresh (x y) (== q (list x y))))
+  (list (list (make-symbol "_.0") (make-symbol "_.1"))))
+
+(mk-test
+  "reify-mixed-bound-unbound"
+  (run* q (fresh (x y) (== q (list 1 x 2 y))))
+  (list
+    (list 1 (make-symbol "_.0") 2 (make-symbol "_.1"))))
+
+(mk-test
+  "reify-shared-unbound-same-name"
+  (run* q (fresh (x) (== q (list x x))))
+  (list (list (make-symbol "_.0") (make-symbol "_.0"))))
+
+(mk-test
+  "reify-distinct-unbound-distinct-names"
+  (run* q (fresh (x y) (== q (list x y x y))))
+  (list
+    (list
+      (make-symbol "_.0")
+      (make-symbol "_.1")
+      (make-symbol "_.0")
+      (make-symbol "_.1"))))
+
+;; --- conde + run* ---
+
+(mk-test
+  "run*-conde-three"
+  (run*
+    q
+    (conde ((== q 1)) ((== q 2)) ((== q 3))))
+  (list 1 2 3))
+
+(mk-test
+  "run*-conde-fresh-mix"
+  (run*
+    q
+    (conde ((fresh (x) (== q (list 1 x)))) ((== q "ground"))))
+  (list (list 1 (make-symbol "_.0")) "ground"))
+
+;; --- run* + conjunction ---
+
+(mk-test
+  "run*-conj-binds-q"
+  (run* q (fresh (x) (== x 5) (== q (list x x))))
+  (list (list 5 5)))
+
+;; --- run* + condu ---
+
+(mk-test
+  "run*-condu-first-wins"
+  (run* q (condu ((== q 1)) ((== q 2))))
+  (list 1))
+
+(mk-test
+  "run*-onceo-trim"
+  (run* q (onceo (conde ((== q "a")) ((== q "b")))))
+  (list "a"))
+
+;; --- multi-goal run ---
+
+(mk-test
+  "run*-three-goals"
+  (run*
+    q
+    (fresh
+      (x y z)
+      (== x 1)
+      (== y 2)
+      (== z 3)
+      (== q (list x y z))))
+  (list (list 1 2 3)))
+
+(mk-tests-run!)

lib/minikanren/tests/unify.sx

@@ -0,0 +1,293 @@
+;; lib/minikanren/tests/unify.sx — Phase 1 tests for unify.sx.
+;;
+;; Loads into a session that already has lib/guest/match.sx and
+;; lib/minikanren/unify.sx defined. Tests are top-level forms.
+;; Call (mk-tests-run!) afterwards to get the totals.
+;;
+;; Note: SX dict equality is reference-based, so tests check the *effect*
+;; of a unification (success/failure flag, or walked bindings) rather than
+;; the raw substitution dict.
+
+(define mk-test-pass 0)
+(define mk-test-fail 0)
+(define mk-test-fails (list))
+
+(define
+  mk-test
+  (fn
+    (name actual expected)
+    (if
+      (= actual expected)
+      (set! mk-test-pass (+ mk-test-pass 1))
+      (begin
+        (set! mk-test-fail (+ mk-test-fail 1))
+        (append! mk-test-fails {:name name :expected expected :actual actual})))))
+
+(define mk-tests-run! (fn () {:total (+ mk-test-pass mk-test-fail) :passed mk-test-pass :failed mk-test-fail :fails mk-test-fails}))
+
+(define mk-unified? (fn (s) (if (= s nil) false true)))
+
+;; --- fresh variable construction ---
+
+(mk-test
+  "make-var-distinct"
+  (let ((a (make-var)) (b (make-var))) (= (var-name a) (var-name b)))
+  false)
+
+(mk-test "make-var-is-var" (mk-var? (make-var)) true)
+(mk-test "var?-num" (mk-var? 5) false)
+(mk-test "var?-list" (mk-var? (list 1 2)) false)
+(mk-test "var?-string" (mk-var? "hi") false)
+(mk-test "var?-empty" (mk-var? (list)) false)
+(mk-test "var?-bool" (mk-var? true) false)
+
+;; --- empty substitution ---
+
+(mk-test "empty-s-walk-num" (mk-walk 5 empty-s) 5)
+(mk-test "empty-s-walk-str" (mk-walk "x" empty-s) "x")
+(mk-test
+  "empty-s-walk-list"
+  (mk-walk (list 1 2) empty-s)
+  (list 1 2))
+(mk-test
+  "empty-s-walk-unbound-var"
+  (let ((x (make-var))) (= (mk-walk x empty-s) x))
+  true)
+
+;; --- walk: top-level chain resolution ---
+
+(mk-test
+  "walk-direct-binding"
+  (mk-walk (mk-var "x") (extend "x" 7 empty-s))
+  7)
+
+(mk-test
+  "walk-two-step-chain"
+  (mk-walk
+    (mk-var "x")
+    (extend "x" (mk-var "y") (extend "y" 9 empty-s)))
+  9)
+
+(mk-test
+  "walk-three-step-chain"
+  (mk-walk
+    (mk-var "a")
+    (extend
+      "a"
+      (mk-var "b")
+      (extend "b" (mk-var "c") (extend "c" 42 empty-s))))
+  42)
+
+(mk-test
+  "walk-stops-at-list"
+  (mk-walk (list 1 (mk-var "x")) (extend "x" 5 empty-s))
+  (list 1 (mk-var "x")))
+
+;; --- walk*: deep walk into lists ---
+
+(mk-test
+  "walk*-flat-list-with-vars"
+  (mk-walk*
+    (list (mk-var "x") 2 (mk-var "y"))
+    (extend "x" 1 (extend "y" 3 empty-s)))
+  (list 1 2 3))
+
+(mk-test
+  "walk*-nested-list"
+  (mk-walk*
+    (list 1 (mk-var "x") (list 2 (mk-var "y")))
+    (extend "x" 5 (extend "y" 6 empty-s)))
+  (list 1 5 (list 2 6)))
+
+(mk-test
+  "walk*-unbound-stays-var"
+  (let
+    ((x (mk-var "x")))
+    (= (mk-walk* (list 1 x) empty-s) (list 1 x)))
+  true)
+
+(mk-test "walk*-atom" (mk-walk* 5 empty-s) 5)
+
+;; --- unify atoms (success / failure semantics, not dict shape) ---
+
+(mk-test
+  "unify-num-eq-succeeds"
+  (mk-unified? (mk-unify 5 5 empty-s))
+  true)
+(mk-test "unify-num-neq-fails" (mk-unify 5 6 empty-s) nil)
+(mk-test
+  "unify-str-eq-succeeds"
+  (mk-unified? (mk-unify "a" "a" empty-s))
+  true)
+(mk-test "unify-str-neq-fails" (mk-unify "a" "b" empty-s) nil)
+(mk-test
+  "unify-bool-eq-succeeds"
+  (mk-unified? (mk-unify true true empty-s))
+  true)
+(mk-test "unify-bool-neq-fails" (mk-unify true false empty-s) nil)
+(mk-test
+  "unify-nil-eq-succeeds"
+  (mk-unified? (mk-unify nil nil empty-s))
+  true)
+(mk-test
+  "unify-empty-list-succeeds"
+  (mk-unified? (mk-unify (list) (list) empty-s))
+  true)
+
+;; --- unify var with anything (walk to verify binding) ---
+
+(mk-test
+  "unify-var-num-binds"
+  (mk-walk (mk-var "x") (mk-unify (mk-var "x") 5 empty-s))
+  5)
+
+(mk-test
+  "unify-num-var-binds"
+  (mk-walk (mk-var "x") (mk-unify 5 (mk-var "x") empty-s))
+  5)
+
+(mk-test
+  "unify-var-list-binds"
+  (mk-walk
+    (mk-var "x")
+    (mk-unify (mk-var "x") (list 1 2) empty-s))
+  (list 1 2))
+
+(mk-test
+  "unify-var-var-same-no-extend"
+  (mk-unified? (mk-unify (mk-var "x") (mk-var "x") empty-s))
+  true)
+
+(mk-test
+  "unify-var-var-different-walks-equal"
+  (let
+    ((s (mk-unify (mk-var "x") (mk-var "y") empty-s)))
+    (= (mk-walk (mk-var "x") s) (mk-walk (mk-var "y") s)))
+  true)
+
+;; --- unify lists positionally ---
+
+(mk-test
+  "unify-list-equal-succeeds"
+  (mk-unified?
+    (mk-unify
+      (list 1 2 3)
+      (list 1 2 3)
+      empty-s))
+  true)
+
+(mk-test
+  "unify-list-different-length-fails-1"
+  (mk-unify
+    (list 1 2)
+    (list 1 2 3)
+    empty-s)
+  nil)
+
+(mk-test
+  "unify-list-different-length-fails-2"
+  (mk-unify
+    (list 1 2 3)
+    (list 1 2)
+    empty-s)
+  nil)
+
+(mk-test
+  "unify-list-mismatch-fails"
+  (mk-unify
+    (list 1 2)
+    (list 1 3)
+    empty-s)
+  nil)
+
+(mk-test
+  "unify-list-vs-atom-fails"
+  (mk-unify (list 1 2) 5 empty-s)
+  nil)
+
+(mk-test
+  "unify-empty-vs-non-empty-fails"
+  (mk-unify (list) (list 1) empty-s)
+  nil)
+
+(mk-test
+  "unify-list-with-vars-walks"
+  (mk-walk*
+    (list (mk-var "x") (mk-var "y"))
+    (mk-unify
+      (list (mk-var "x") (mk-var "y"))
+      (list 1 2)
+      empty-s))
+  (list 1 2))
+
+(mk-test
+  "unify-nested-lists-with-vars-walks"
+  (mk-walk*
+    (list (mk-var "x") (list (mk-var "y") 3))
+    (mk-unify
+      (list (mk-var "x") (list (mk-var "y") 3))
+      (list 1 (list 2 3))
+      empty-s))
+  (list 1 (list 2 3)))
+
+;; --- unify chained substitutions ---
+
+(mk-test
+  "unify-chain-var-var-then-atom"
+  (let
+    ((x (mk-var "x")) (y (mk-var "y")))
+    (let
+      ((s1 (mk-unify x y empty-s)))
+      (mk-walk x (mk-unify y 7 s1))))
+  7)
+
+(mk-test
+  "unify-already-bound-consistent"
+  (let
+    ((s (extend "x" 5 empty-s)))
+    (mk-unified? (mk-unify (mk-var "x") 5 s)))
+  true)
+
+(mk-test
+  "unify-already-bound-conflict-fails"
+  (let
+    ((s (extend "x" 5 empty-s)))
+    (mk-unify (mk-var "x") 6 s))
+  nil)
+
+;; --- occurs check (opt-in) ---
+
+(mk-test
+  "unify-no-occurs-default-succeeds"
+  (let
+    ((x (mk-var "x")))
+    (mk-unified? (mk-unify x (list 1 x) empty-s)))
+  true)
+
+(mk-test
+  "unify-occurs-direct-fails"
+  (let ((x (mk-var "x"))) (mk-unify-check x (list 1 x) empty-s))
+  nil)
+
+(mk-test
+  "unify-occurs-nested-fails"
+  (let
+    ((x (mk-var "x")))
+    (mk-unify-check x (list 1 (list 2 x)) empty-s))
+  nil)
+
+(mk-test
+  "unify-occurs-non-occurring-succeeds"
+  (let
+    ((x (mk-var "x")))
+    (mk-unified? (mk-unify-check x 5 empty-s)))
+  true)
+
+(mk-test
+  "unify-occurs-via-chain-fails"
+  (let
+    ((x (mk-var "x")) (y (mk-var "y")))
+    (let ((s (extend "y" (list x) empty-s))) (mk-unify-check x y s)))
+  nil)
+
+(mk-tests-run!)

lib/minikanren/unify.sx

@@ -0,0 +1,82 @@
+;; lib/minikanren/unify.sx — Phase 1 + cons-cell extension.
+;;
+;; miniKanren-on-SX, built on lib/guest/match.sx. The kit ships the heavy
+;; lifting (walk-with, unify-with, occurs-with, extend, empty-subst,
+;; mk-var/is-var?/var-name); this file supplies a miniKanren-shaped cfg
+;; and a thin public API.
+;;
+;; Term shapes:
+;;   logic var   : (:var NAME)              — kit's mk-var
+;;   cons cell   : (:cons HEAD TAIL)        — for relational programming
+;;                 (built by mk-cons; lets relations decompose lists by
+;;                 head/tail without proper improper pairs in the host)
+;;   native list : SX list (a b c)          — also unifies pair-style:
+;;                 args = (head, tail) so (1 2 3) ≡ (:cons 1 (:cons 2 (:cons 3 ())))
+;;   atom        : number / string / symbol / boolean / nil / ()
+;;
+;; Substitution: SX dict mapping VAR-NAME → term. Empty = (empty-subst).
+
+(define mk-cons (fn (h t) (list :cons h t)))
+
+(define
+  mk-cons-cell?
+  (fn (t) (and (list? t) (not (empty? t)) (= (first t) :cons))))
+
+(define mk-cons-head (fn (t) (nth t 1)))
+(define mk-cons-tail (fn (t) (nth t 2)))
+
+(define
+  mk-list-pair?
+  (fn (t) (and (list? t) (not (empty? t)) (not (is-var? t)))))
+
+(define mk-list-pair-head (fn (t) :pair))
+
+(define
+  mk-list-pair-args
+  (fn
+    (t)
+    (cond
+      ((mk-cons-cell? t) (list (mk-cons-head t) (mk-cons-tail t)))
+      (:else (list (first t) (rest t))))))
+
+(define mk-cfg {:ctor-head mk-list-pair-head :var? is-var? :ctor? mk-list-pair? :occurs-check? false :var-name var-name :ctor-args mk-list-pair-args})
+
+(define mk-cfg-occurs {:ctor-head mk-list-pair-head :var? is-var? :ctor? mk-list-pair? :occurs-check? true :var-name var-name :ctor-args mk-list-pair-args})
+
+(define empty-s (empty-subst))
+
+(define mk-fresh-counter 0)
+
+(define
+  make-var
+  (fn
+    ()
+    (begin
+      (set! mk-fresh-counter (+ mk-fresh-counter 1))
+      (mk-var (str "_." mk-fresh-counter)))))
+
+(define mk-var? is-var?)
+
+(define mk-walk (fn (t s) (walk-with mk-cfg t s)))
+
+(define
+  mk-walk*
+  (fn
+    (t s)
+    (let
+      ((w (mk-walk t s)))
+      (cond
+        ((mk-cons-cell? w)
+          (let
+            ((h (mk-walk* (mk-cons-head w) s))
+              (tl (mk-walk* (mk-cons-tail w) s)))
+            (cond
+              ((empty? tl) (list h))
+              ((mk-cons-cell? tl) tl)
+              ((list? tl) (cons h tl))
+              (:else (mk-cons h tl)))))
+        ((mk-list-pair? w) (map (fn (a) (mk-walk* a s)) w))
+        (:else w)))))
+
+(define mk-unify (fn (u v s) (unify-with mk-cfg u v s)))
+(define mk-unify-check (fn (u v s) (unify-with mk-cfg-occurs u v s)))

plans/apl-on-sx.md

@@ -135,48 +135,6 @@ and tightens loose ends.
   on error switches to the trap branch.  Define `apl-throw` and a small
   set of error codes; use `try`/`catch` from the host.
 
-### Phase 8 — fill the gaps left after end-to-end
-
-Phase 7 wired the stack together; Phase 8 closes deferred items, lets real
-programs run from source, and starts pushing on performance.
-
-- [x] **Quick-wins bundle** (one iteration) — three small fixes that each unblock
-  real programs:
-  - decimal literals: `read-digits!` consumes one trailing `.` plus more digits
-    so `3.7` tokenises as one number;
-  - `⎕←` (print) — tokenizer special-case: when `⎕` is followed by `←`, emit
-    a single `:name "⎕←"` token (don't split on the assign glyph);
-  - string values in `apl-eval-ast` — handle `:str` (parser already produces
-    them) by wrapping into a vector of character codes (or rank-0 string).
-- [x] **Named function definitions** — `f ← {⍺+⍵} ⋄ 1 f 2` and `2 f 3`.
-  - parser: when `:assign`'s RHS is a `:dfn`, mark it as a function binding;
-  - eval-ast: `:assign` of a dfn stores the dfn in env;
-  - parser: a name in fn-position whose env value is a dfn dispatches as a fn;
-  - resolver: extend `apl-resolve-monadic`/`-dyadic` with a `:fn-name` case
-    that calls `apl-call-dfn`/`apl-call-dfn-m`.
-- [x] **Multi-axis bracket indexing** — `A[I;J]` and `A[;J]` and `A[I;]`.
-  - parser: split bracket content on `:semi` at depth 0; emit
-    `(:dyad ⌷ (:vec I J) A)`;
-  - runtime: extend `apl-squad` to accept a vector of indices, treating
-    `nil` / empty axis as "all";
-  - 5+ tests across vector and matrix.
-- [x] **`.apl` files as actual tests** — `lib/apl/tests/programs/*.apl` are
-  currently documentation. Add `apl-run-file path → array` plus tests that
-  load each file, execute it, and assert the expected result. Makes the
-  classic-program corpus self-validating instead of two parallel impls.
-  _(Embedded source-string approach: tests/programs-e2e.sx runs the same
-  algorithms as the .apl docs through the full pipeline. The original
-  one-liners (e.g. primes' inline `⍵←⍳⍵`) need parser features
-  (compress-as-fn, inline assign) we haven't built yet — multi-stmt forms
-  used instead. Slurp/read-file primitive missing in OCaml SX runtime.)_
-- [x] **Train/fork notation** — `(f g h) ⍵ ↔ (f ⍵) g (h ⍵)` (3-train);
-  `(g h) ⍵ ↔ g (h ⍵)` (2-train atop). Parser: detect when a parenthesised
-  subexpression is all functions and emit `(:train fns)`; resolver: build the
-  derived function; tests for mean-via-train (`+/÷≢`).
-- [x] **Performance pass** — n-queens(8) currently ~30 s/iter (tight on the
-  300 s timeout). Target: profile the inner loop, eliminate quadratic
-  list-append, restore the `queens(8)` test.
-
 ## SX primitive baseline
 
 Use vectors for arrays; numeric tower + rationals for numbers; ADTs for tagged data;
@@ -191,13 +149,6 @@ data; format for string templating.
 
 _Newest first._
 
-- 2026-05-07: Phase 8 step 6 — perf: swapped (append acc xs) → (append xs acc) in apl-permutations to make permutation generation linear instead of quadratic; q(7) 32s→12s; q(8)=92 test restored within 300s timeout; **Phase 8 complete, all unchecked items ticked**; 497/497
-- 2026-05-07: Phase 8 step 5 — train/fork notation. Parser :lparen detects all-fn inner segments → emits :train AST; resolver covers 2-atop & 3-fork for both monadic and dyadic. `(+/÷≢) 1..5 → 3` (mean), `(- ⌊) 5 → -5` (atop), `2(+×-)5 → -21` (dyadic fork), `(⌈/-⌊/) → 8` (range); +6 tests; 496/496
-- 2026-05-07: Phase 8 step 4 — programs-e2e.sx runs classic-algorithm shapes through full pipeline (factorial via ∇, triangulars, sum-of-squares, divisor-counts, prime-mask, named-fn composition, dyadic max-of-two, Newton step); also added ⌿ + ⍀ to glyph sets (were silently skipped); +15 tests; 490/490
-- 2026-05-07: Phase 8 step 3 — multi-axis bracket A[I;J] / A[I;] / A[;J] via :bracket AST + apl-bracket-multi runtime; split-bracket-content scans :semi at depth 0; apl-cartesian builds index combinations; nil axis = "all"; scalar axis collapses; +8 tests; 475/475
-- 2026-05-07: Phase 8 step 2 — named function defs end-to-end via parser pre-scan; apl-known-fn-names + apl-collect-fn-bindings detect `name ← {...}` patterns; collect-segments-loop emits :fn-name for known names; resolver looks up env for :fn-name; supports recursion (∇ in named dfn); +7 tests including fact via ∇; 467/467
-- 2026-05-07: Phase 8 step 1 — quick-wins bundle: decimal literals (3.7, ¯2.5), ⎕← passthrough as monadic fn (single-token via tokenizer special-case), :str AST in eval-ast (single-char→scalar, multi-char→vec); +10 tests; 460/460
-- 2026-05-07: Phase 8 added — quick-wins bundle (decimals + ⎕← + strings), named functions, multi-axis bracket, .apl-files-as-tests, trains, perf
 - 2026-05-07: Phase 7 step 6 — :Trap exception machinery via R7RS guard; apl-throw raises tagged error, apl-trap-matches? checks codes (0=catch-all), :trap clause in apl-tradfn-eval-stmt wraps try-block with guard; :throw AST for testing; **Phase 7 complete, all unchecked plan items done**; +5 tests; 450/450
 - 2026-05-07: Phase 7 step 5 — idiom corpus 34→64 (+30 source-string idioms via apl-run); also fixed tokenizer + parser to recognize ≢ and ≡ glyphs (were silently skipped); 445/445
 - 2026-05-07: Phase 7 step 4 — bracket indexing `A[I]` desugared to `(:dyad ⌷ I A)` via maybe-bracket helper, wired into :name + :lparen branches of collect-segments-loop; multi-axis (A[I;J]) deferred (semicolon split); +7 tests; 415/415

plans/datalog-on-sx.md

@@ -58,108 +58,50 @@ Key differences from Prolog:
 ## Roadmap
 
 ### Phase 1 — tokenizer + parser
-- [x] Tokenizer: atoms (lowercase/quoted), variables (uppercase/`_`), numbers, strings,
-      punct (`( )`, `,`, `.`), operators (`:-`, `?-`, `<=`, `>=`, `!=`, `<`, `>`, `=`,
-      `+`, `-`, `*`, `/`), comments (`%`, `/* */`)
-      Note: no function symbol syntax (no nested `f(...)` in arg position) — but the
-      parser permits nested compounds for arithmetic; safety analysis (Phase 3) rejects
-      non-arithmetic nesting.
-- [x] Parser:
+- [ ] Tokenizer: atoms (lowercase/quoted), variables (uppercase/`_`), numbers, strings,
+      operators (`:- `, `?-`, `,`, `.`), comments (`%`, `/* */`)
+      Note: no function symbol syntax (no nested `f(...)` in arg position).
+- [ ] Parser:
       - Facts: `parent(tom, bob).` → `{:head (parent tom bob) :body ()}`
       - Rules: `ancestor(X,Z) :- parent(X,Y), ancestor(Y,Z).`
               → `{:head (ancestor X Z) :body ((parent X Y) (ancestor Y Z))}`
-      - Queries: `?- ancestor(tom, X).` → `{:query ((ancestor tom X))}`
-        (`:query` value is always a list of literals; `?- p, q.` → `{:query ((p) (q))}`)
+      - Queries: `?- ancestor(tom, X).` → `{:query (ancestor tom X)}`
       - Negation: `not(parent(X,Y))` in body position → `{:neg (parent X Y)}`
-- [x] Tests in `lib/datalog/tests/parse.sx` (18) and `lib/datalog/tests/tokenize.sx` (26).
-      Conformance harness: `bash lib/datalog/conformance.sh` → 44 / 44 passing.
+- [ ] Tests in `lib/datalog/tests/parse.sx`
 
 ### Phase 2 — unification + substitution
-- [x] Ported (not shared) from `lib/prolog/` — term walk, no occurs check.
-- [x] `dl-unify t1 t2 subst` → extended subst dict, or `nil` on failure.
-- [x] `dl-walk`, `dl-bind`, `dl-apply-subst`, `dl-ground?`, `dl-vars-of`.
-- [x] Substitutions are immutable dicts keyed by variable name (string).
-      Lists/tuples unify element-wise (used for arithmetic compounds too).
-- [x] Tests in `lib/datalog/tests/unify.sx` (28). 72 / 72 conformance.
+- [ ] Share or port unification from `lib/prolog/` — term walk, occurs check off by default
+- [ ] `dl-unify` `t1` `t2` `subst` → extended subst or nil (no function symbols means simpler)
+- [ ] `dl-ground?` `term` → bool — all variables bound in substitution
+- [ ] Tests: atom/atom, var/atom, var/var, list args
 
-### Phase 3 — extensional DB + naive evaluation + safety analysis
-- [x] EDB+IDB combined: `{:facts {<rel-name-string> -> (literal ...)}}` —
-      relations indexed by name; tuples stored as full literals so they
-      unify directly. Dedup on insert via `dl-tuple-equal?`.
-- [x] `dl-add-fact! db lit` (rejects non-ground) and `dl-add-rule! db rule`
-      (rejects unsafe). `dl-program source` parses + loads in one step.
-- [x] Naive evaluation `dl-saturate! db`: iterate rules until no new tuples.
-      `dl-find-bindings` recursively joins body literals; `dl-match-positive`
-      unifies a literal against every tuple in the relation.
-- [x] `dl-query db goal` → list of substitutions over `goal`'s vars,
-      deduplicated. `dl-relation db name` for derived tuples.
-- [x] Safety analysis at `dl-add-rule!` time: every head variable except
-      `_` must appear in some positive body literal. Built-ins and negated
-      literals do not satisfy safety. Helpers `dl-positive-body-vars`,
-      `dl-rule-unsafe-head-vars` exposed for later phases.
-- [x] Negation and arithmetic built-ins error cleanly at saturate time
-      (Phase 4 / Phase 7 will swap in real semantics).
-- [x] Tests in `lib/datalog/tests/eval.sx` (15): transitive closure,
-      sibling, same-generation, grandparent, cyclic graph reach, six
-      safety cases. 87 / 87 conformance.
+### Phase 3 — extensional DB + naive evaluation
+- [ ] EDB: `{:relation-name → set-of-ground-tuples}` using SX sets (Phase 18 of primitives)
+- [ ] `dl-add-fact!` `db` `relation` `args` → add ground tuple
+- [ ] `dl-add-rule!` `db` `head` `body` → add rule clause
+- [ ] Naive evaluation: iterate rules until fixpoint
+      For each rule, for each combination of body tuples that unify, derive head tuple.
+      Repeat until no new tuples added.
+- [ ] `dl-query` `db` `goal` → list of substitutions satisfying goal against derived DB
+- [ ] Tests: transitive closure (ancestor), sibling, same-generation — classic Datalog programs
 
-### Phase 4 — built-in predicates + body arithmetic
-Almost every real query needs `<`, `=`, simple arithmetic, and string
-comparisons in body position. These are not EDB lookups — they're
-constraints that filter bindings.
-- [x] Recognise built-in predicates in body: `(< X Y)`, `(<= X Y)`, `(> X Y)`,
-      `(>= X Y)`, `(= X Y)`, `(!= X Y)` and arithmetic forms `(is Z (+ X Y))`,
-      `(is Z (- X Y))`, `(is Z (* X Y))`, `(is Z (/ X Y))`. Live in
-      `lib/datalog/builtins.sx`.
-- [x] `dl-eval-builtin` dispatches; `dl-eval-arith` recursively evaluates
-      `(+ a b)` etc. with full nesting. `=` unifies; `!=` rejects equal
-      ground terms.
-- [x] Order-aware safety analysis (`dl-rule-check-safety`): walks body
-      left-to-right tracking which vars are bound. `is`'s RHS vars must
-      be already bound; LHS becomes bound. Comparisons require both
-      sides bound. `=` is special-cased — at least one side bound binds
-      the other. Negation vars must be bound (will be enforced fully in
-      Phase 7).
-- [x] Wired through SX numeric primitives — no separate number tower.
-- [x] Tests in `lib/datalog/tests/builtins.sx` (19): range filters,
-      arithmetic derivations, equality binding, eight safety violations
-      and three safe-shape tests. Conformance 106 / 106.
-
-### Phase 5 — semi-naive evaluation (performance)
+### Phase 4 — semi-naive evaluation (performance)
 - [ ] Delta sets: track newly derived tuples per iteration
 - [ ] Semi-naive rule: only join against delta tuples from last iteration, not full relation
 - [ ] Significant speedup for recursive rules — avoids re-deriving known tuples
+- [ ] `dl-stratify` `db` → dependency graph + SCC analysis → stratum ordering
 - [ ] Tests: verify semi-naive produces same results as naive; benchmark on large ancestor chain
 
-### Phase 6 — magic sets (goal-directed bottom-up, opt-in)
-Naive bottom-up derives **all** consequences before answering. Magic sets
-rewrite the program so the fixpoint only derives tuples relevant to the
-goal — a major perf win for "what's reachable from node X" queries on
-large graphs.
-- [ ] Adornments: annotate rule predicates with bound (`b`) / free (`f`)
-      patterns based on how they're called.
-- [ ] Magic transformation: for each adorned predicate, generate a
-      `magic_<pred>` relation and rewrite rule bodies to filter through it.
-- [ ] Sideways information passing strategy (SIPS): left-to-right by
-      default; pluggable.
-- [ ] Optional pass — `(dl-set-strategy! db :magic)`; default semi-naive.
-- [ ] Tests: equivalence vs naive on small inputs; perf win on a 10k-node
-      reachability query from a single root.
-
-### Phase 7 — stratified negation
+### Phase 5 — stratified negation
 - [ ] Dependency graph analysis: which relations depend on which (positively or negatively)
 - [ ] Stratification check: error if negation is in a cycle (non-stratifiable program)
-- [ ] `dl-stratify db` → SCC analysis → stratum ordering
-- [ ] Evaluation: process strata in order — lower stratum fully computed
-      before using its complement in a higher stratum
-- [ ] `not(P)` in rule body: at evaluation time, check P is NOT in the
-      derived EDB
-- [ ] Safety extension: head vars in negative literals must also appear in
-      some positive body literal of the same rule
-- [ ] Tests: non-member (`not(member(X,L))`), colored-graph
-      (`not(same-color(X,Y))`), stratification error detection
+- [ ] Evaluation: process strata in order — lower stratum fully computed before using its
+      complement in a higher stratum
+- [ ] `not(P)` in rule body: at evaluation time, check P is NOT in the derived EDB
+- [ ] Tests: non-member (`not(member(X,L))`), colored-graph (`not(same-color(X,Y))`),
+      stratification error detection
 
-### Phase 8 — aggregation (Datalog+)
+### Phase 6 — aggregation (Datalog+)
 - [ ] `count(X, Goal)` → number of distinct X satisfying Goal
 - [ ] `sum(X, Goal)` → sum of X values satisfying Goal
 - [ ] `min(X, Goal)` / `max(X, Goal)` → min/max of X satisfying Goal
@@ -167,7 +109,7 @@ large graphs.
 - [ ] Aggregation breaks stratification — evaluate in a separate post-fixpoint pass
 - [ ] Tests: social network statistics, grade aggregation, inventory sums
 
-### Phase 9 — SX embedding API
+### Phase 7 — SX embedding API
 - [ ] `(dl-program facts rules)` → database from SX data directly (no parsing required)
       ```
       (dl-program
@@ -181,7 +123,7 @@ large graphs.
 - [ ] Integration demo: federation graph query — `(ancestor actor1 actor2)` over
       rose-ash ActivityPub follow relationships
 
-### Phase 10 — Datalog as a query language for rose-ash
+### Phase 8 — Datalog as a query language for rose-ash
 - [ ] Schema: map SQLAlchemy model relationships to Datalog EDB facts
       (e.g. `(follows user1 user2)`, `(authored user post)`, `(tagged post tag)`)
 - [ ] Loader: `dl-load-from-db!` — query PostgreSQL, populate Datalog EDB
@@ -200,42 +142,4 @@ _(none yet)_
 
 _Newest first._
 
-- 2026-05-07 — Phase 4 done. `lib/datalog/builtins.sx` (~280 LOC) adds
-  `(< X Y)`, `(<= X Y)`, `(> X Y)`, `(>= X Y)`, `(= X Y)`, `(!= X Y)`,
-  and `(is X expr)` with `+ - * /`. `dl-eval-builtin` dispatches;
-  `dl-eval-arith` recursively evaluates nested compounds. Safety
-  check is now order-aware — it walks body literals left-to-right
-  tracking the bound set, requires comparison/`is` inputs to be
-  already bound, and special-cases `=` (binds the var-side; both
-  sides must include at least one bound to bind the other). Phase 3's
-  simple safety check stays in db.sx as a forward-reference fallback;
-  builtins.sx redefines `dl-rule-check-safety` to the comprehensive
-  version. eval.sx's `dl-match-lit` now dispatches built-ins through
-  `dl-eval-builtin`. 19 builtins tests; conformance 106 / 106.
-
-- 2026-05-07 — Phase 3 done. `lib/datalog/db.sx` (~250 LOC) holds facts
-  indexed by relation name plus the rules list, with `dl-add-fact!` /
-  `dl-add-rule!` (rejects non-ground facts and unsafe rules);
-  `lib/datalog/eval.sx` (~150 LOC) implements the naive bottom-up
-  fixpoint via `dl-find-bindings`/`dl-match-positive`/`dl-saturate!`
-  and `dl-query` (deduped projected substitutions). Safety analysis
-  rejects unsafe head vars at load time. Negation and arithmetic
-  built-ins raise clean errors (lifted in later phases). 15 eval
-  tests cover transitive closure, sibling, same-generation, cyclic
-  graph reach, and six safety violations. Conformance 87 / 87.
-
-- 2026-05-07 — Phase 2 done. `lib/datalog/unify.sx` (~140 LOC):
-  `dl-var?` (case + underscore), `dl-walk`, `dl-bind`, `dl-unify` (returns
-  extended dict subst or `nil`), `dl-apply-subst`, `dl-ground?`, `dl-vars-of`.
-  Substitutions are immutable dicts; `assoc` builds extended copies. 28
-  unify tests; conformance now 72 / 72.
-
-- 2026-05-07 — Phase 1 done. `lib/datalog/tokenizer.sx` (~190 LOC) emits
-  `{:type :value :pos}` tokens; `lib/datalog/parser.sx` (~150 LOC) produces
-  `{:head … :body …}` / `{:query …}` clauses, with nested compounds
-  permitted for arithmetic and `not(...)` desugared to `{:neg …}`. 44 / 44
-  via `bash lib/datalog/conformance.sh` (26 tokenize + 18 parse). Local
-  helpers namespace-prefixed (`dl-emit!`, `dl-peek`) after a host-primitive
-  shadow clash. Test harness uses a custom `dl-deep-equal?` that handles
-  out-of-order dict keys and number repr (`equal?` fails on dict key order
-  and on `30` vs `30.0`).
+_(awaiting phase 1)_

plans/lib-guest.md

@@ -158,8 +158,8 @@ Extract from `haskell/infer.sx`. Algorithm W or J, generalisation, instantiation
 | 4 — pratt.sx (lua + prolog) | [done] | da27958d | Extracted operator-table format + lookup only — climbing loops stay per-language because lua and prolog use opposite prec conventions. lua/parser.sx: 18-clause cond → 15-entry table. prolog/parser.sx: pl-op-find deleted, pl-op-lookup wraps pratt-op-lookup. lua 185/185, prolog 590/590 — both = baseline. |
 | 5 — ast.sx (lua + prolog) | [partial — pending real consumers] | a774cd26 | Kit + 33 self-tests shipped (10 canonical kinds, predicates, accessors). Step is "Optional" per brief; lua/prolog parsers untouched (185/185 + 590/590). Datalog-on-sx will be the natural first real consumer; lua/prolog converters can land later. |
 | 6 — match.sx (haskell + prolog) | [partial — kit shipped; ports deferred] | 863e9d93 | Pure-functional unify + match kit (canonical wire format + cfg-driven adapters) + 25 self-tests. Existing prolog/haskell engines untouched (structurally divergent — mutating-symmetric vs pure-asymmetric — would risk 746 passing tests under brief's revert-on-regression rule). Real consumer is minikraken/datalog work in flight. |
-| 7 — layout.sx (haskell + synthetic) | [partial — haskell port deferred] | d75c61d4 | Configurable kit (haskell-style keyword-opens + python-style trailing-`:`-opens) + 6 self-tests covering both flavours. Synthetic Python-ish fixture passes; haskell/layout.sx untouched (kit not yet a drop-in for Haskell 98 Note 5 etc.; haskell still 156/156 baseline). |
-| 8 — hm.sx (haskell + TBD) | [partial — algebra shipped; assembly deferred] | ab2c40c1 | HM foundations: types/schemes/ftv/apply/compose/generalize/instantiate/fresh-tv on top of match.sx unify, plus literal inference rule. 24/24 self-tests. Algorithm W lambda/app/let assembly deferred to host code — paired sequencing per brief: lib/ocaml/types.sx (OCaml-on-SX Phase 5) + haskell/infer.sx port. Haskell still 156/156 baseline. |
+| 7 — layout.sx (haskell + synthetic) | [in-progress] | — | — |
+| 8 — hm.sx (haskell + TBD) | [ ] | — | — |
 
 ---
 

plans/minikanren-on-sx.md

@@ -50,63 +50,87 @@ Key semantic mappings:
 ## Roadmap
 
 ### Phase 1 — variables + unification
-- [ ] `make-var` → fresh logic variable (unique mutable box)
-- [ ] `var?` `v` → bool — is this a logic variable?
-- [ ] `walk` `term` `subst` → follow substitution chain to ground term or unbound var
-- [ ] `walk*` `term` `subst` → deep walk (recurse into lists/dicts)
-- [ ] `unify` `u` `v` `subst` → extended substitution or `#f` (failure)
+- [x] `make-var` → fresh logic variable (unique mutable box)
+- [x] `var?` `v` → bool — is this a logic variable?
+- [x] `walk` `term` `subst` → follow substitution chain to ground term or unbound var
+- [x] `walk*` `term` `subst` → deep walk (recurse into lists/dicts)
+- [x] `unify` `u` `v` `subst` → extended substitution or `#f` (failure)
       Handles: var/var, var/term, term/var, list unification, number/string/symbol equality.
       No occurs check by default; `unify-check` with occurs check as opt-in.
-- [ ] Empty substitution `empty-s` = `(list)` (empty assoc list)
-- [ ] Tests in `lib/minikanren/tests/unify.sx`: ground terms, vars, lists, failure, occurs
+- [x] Empty substitution `empty-s` (dict-based via kit's `empty-subst` — assoc list was a sketch; kit ships dict, kept it)
+- [x] Tests in `lib/minikanren/tests/unify.sx`: ground terms, vars, lists, failure, occurs
 
 ### Phase 2 — streams + goals
-- [ ] Stream type: `mzero` (empty stream = `nil`), `unit s` (singleton = `(list s)`),
-      `mplus` (interleave two streams), `bind` (apply goal to stream)
-- [ ] Lazy streams via `delay`/`force` — mature pairs for depth-first, immature for lazy
-- [ ] `==` goal: `(fn (s) (let ((s2 (unify u v s))) (if s2 (unit s2) mzero)))`
-- [ ] `succeed` / `fail` — trivial goals
-- [ ] `fresh` — `(fn (f) (fn (s) ((f (make-var)) s)))` — introduces one var; `fresh*` for many
-- [ ] `conde` — interleaving disjunction of goal lists
-- [ ] `condu` — committed choice (soft-cut): only explores first successful clause
-- [ ] `onceo` — succeeds at most once
-- [ ] Tests: basic goal composition, backtracking, interleaving
+- [x] Stream type: `mzero` (empty), `unit s` (singleton), `mk-mplus` (interleave),
+      `mk-bind` (apply goal to stream). Names mk-prefixed because SX has a host
+      `bind` primitive that silently shadows user defines.
+- [x] Lazy streams via thunks: a paused stream is a zero-arg fn; mk-mplus suspends
+      and swaps when its left operand is paused, giving fair interleaving.
+- [x] `==` goal: `(fn (s) (let ((s2 (mk-unify u v s))) (if s2 (unit s2) mzero)))`
+- [x] `==-check` — opt-in occurs-checked equality goal
+- [x] `succeed` / `fail` — trivial goals
+- [x] `conj2` / `mk-conj` (variadic) — sequential conjunction
+- [x] `disj2` / `mk-disj` (variadic) — interleaved disjunction (raw — `conde`
+      adds the implicit-conj-per-clause sugar later)
+- [x] `fresh` — introduces logic variables inside a goal body. Implemented as a
+      defmacro: `(fresh (x y) g1 g2 ...)` ⇒ `(let ((x (make-var)) (y (make-var)))
+      (mk-conj g1 g2 ...))`. Also `call-fresh` for programmatic goal building.
+- [x] `conde` — sugar over disj+conj, one row per clause; defmacro that
+      wraps each clause body in `mk-conj` and folds via `mk-disj`. Notes:
+      with eager streams ordering is left-clause-first DFS; true interleaving
+      requires paused thunks (Phase 4 recursive relations).
+- [x] `condu` — committed choice. defmacro folding clauses into a runtime
+      `condu-try` walker; first clause whose head goal yields a non-empty
+      stream commits its first answer, rest-goals run on that single subst.
+- [x] `onceo` — `(stream-take 1 (g s))`; trims a goal's stream to ≤1 answer.
+- [x] Tests: basic goal composition, backtracking, interleaving (110 cumulative)
 
 ### Phase 3 — run + reification
-- [ ] `run*` `goal` → list of all answers (reified)
-- [ ] `run n` `goal` → list of first n answers
-- [ ] `reify` `term` `subst` → replace unbound vars with `_0`, `_1`, ... names
-- [ ] `reify-s` → builds reification substitution for naming unbound vars consistently
-- [ ] `fresh` with multiple variables: `(fresh (x y z) goal)` sugar
-- [ ] Query variable conventions: `q` as canonical query variable
-- [ ] Tests: classic miniKanren programs — `(run* q (== q 1))` → `(1)`,
+- [x] `run*` `goal` → list of all answers (reified). defmacro: bind q-name as
+      fresh var, conj goals, take all from stream, reify each.
+- [x] `run n` `goal` → list of first n answers (defmacro; n = -1 means all)
+- [x] `reify` `term` `subst` → walk* + build reification subst + walk* again
+- [x] `reify-s` → maps each unbound var (in left-to-right walk order) to a
+      `_.N` symbol via `(make-symbol (str "_." n))`
+- [x] `fresh` with multiple variables — already shipped Phase 2B.
+- [x] Query variable conventions: `q` as canonical query variable (matches TRS)
+- [x] Tests: classic miniKanren programs — `(run* q (== q 1))` → `(1)`,
       `(run* q (conde ((== q 1)) ((== q 2))))` → `(1 2)`,
-      Peano arithmetic, `appendo` preview
+      `(run* q (fresh (x y) (== q (list x y))))` → `((_.0 _.1))`. Peano +
+      `appendo` deferred to Phase 4.
 
 ### Phase 4 — standard relations
-- [ ] `appendo` `l` `s` `ls` — list append, runs forwards and backwards
-- [ ] `membero` `x` `l` — x is a member of l
-- [ ] `listo` `l` — l is a proper list
-- [ ] `nullo` `l` — l is empty
-- [ ] `pairo` `p` — p is a pair (cons cell)
-- [ ] `caro` `p` `a` — car of pair
-- [ ] `cdro` `p` `d` — cdr of pair
-- [ ] `conso` `a` `d` `p` — cons
-- [ ] `firsto` / `resto` — aliases for caro/cdro
-- [ ] `reverseo` `l` `r` — reverse of list
-- [ ] `flatteno` `l` `f` — flatten nested lists
-- [ ] `permuteo` `l` `p` — permutation of list
-- [ ] `lengtho` `l` `n` — length as a relation (Peano or integer)
-- [ ] Tests: run each relation forwards and backwards; generate from partial inputs
+- [x] `appendo` `l` `s` `ls` — list append, runs forwards AND backwards.
+      Canary green: `(run* q (appendo (1 2) (3 4) q))` → `((1 2 3 4))`;
+      `(run* q (fresh (l s) (appendo l s (1 2 3)) (== q (list l s))))` →
+      all four splits.
+- [x] `membero` `x` `l` — enumerates: `(run* q (membero q (a b c)))` → `(a b c)`
+- [x] `listo` `l` — l is a proper list; enumerates list shapes with laziness
+- [x] `nullo` `l` — l is empty
+- [x] `pairo` `p` — p is a (non-empty) cons-cell / list
+- [x] `caro` / `cdro` / `conso` / `firsto` / `resto`
+- [x] `reverseo` `l` `r` — reverse of list. Forward is fast; backward is `run 1`-clean,
+      `run*` diverges due to interleaved unbounded list search (canonical TRS issue).
+- [ ] `flatteno` `l` `f` — flatten nested lists (deferred — needs atom predicate)
+- [ ] `permuteo` `l` `p` — permutation of list (deferred to Phase 5 with `matche`)
+- [x] `lengtho` `l` `n` — length as a relation, Peano-encoded:
+      `:z` / `(:s :z)` / `(:s (:s :z))` ... matches TRS. Forward is direct;
+      backward enumerates lists of a given length.
+- [x] Tests: run each relation forwards and backwards (so far 25 in
+      `tests/relations.sx`; reverseo/flatteno/permuteo/lengtho deferred)
 
 ### Phase 5 — `project` + `matche` + negation
-- [ ] `project` `(x ...) body` — access reified values of logic vars inside a goal;
-      escapes to ground values for arithmetic or string ops
+- [x] `project` `(x ...) body` — defmacro: rebinds named vars to `(mk-walk* var s)`
+      in the body's lexical scope, then runs `(mk-conj body...)` on the same
+      substitution. Hygienic via gensym'd `s`-param. (`Phase 5 piece B`)
 - [ ] `matche` — pattern matching over logic terms (extension from core.logic)
       `(matche l ((head . tail) goal) (() goal))`
-- [ ] `conda` — soft-cut disjunction (like Prolog `->`)
-- [ ] `condu` — committed choice (already in phase 2; refine semantics here)
-- [ ] `nafc` — negation as finite failure with constraint
+- [x] `conda` — soft-cut: first non-failing head wins; ALL of head's answers
+      flow through rest-goals; later clauses not tried (`Phase 5 piece A`)
+- [x] `condu` — committed choice (Phase 2)
+- [x] `nafc` — negation as finite failure: `(nafc g)` yields the input subst
+      iff g has zero answers. Standard caveats apply (open-world unsoundness;
+      diverges if g is infinite). `Phase 5 piece C`.
 - [ ] Tests: Zebra puzzle, N-queens, Sudoku via `project`, family relations via `matche`
 
 ### Phase 6 — arithmetic constraints CLP(FD)
@@ -135,4 +159,72 @@ _(none yet)_
 
 _Newest first._
 
-_(awaiting phase 1)_
+- **2026-05-07** — **Phase 5 piece C — nafc**: `lib/minikanren/nafc.sx`. Three-line
+  primitive: stream-take 1; if empty, `(unit s)`, else `mzero`. 7 tests including
+  double-negation and use as a guard. 201/201 cumulative.
+- **2026-05-07** — **Phase 5 piece B — project**: `lib/minikanren/project.sx` —
+  defmacro that walks each named var, rebinds them, and runs the body's mk-conj.
+  Demonstrated escape into host arithmetic / string ops (`(* n n)`, `(str s "!")`).
+  Hygienic gensym'd s-param. 6 new tests, 194/194 cumulative.
+- **2026-05-07** — **Peano arithmetic** (`lib/minikanren/peano.sx`): zeroo, pluso,
+  minuso, lteo, lto, *o on Peano-encoded naturals (`:z` / `(:s n)`). pluso runs
+  forward, backward, and enumerates: `(run* q (fresh (a b) (pluso a b 3)
+  (== q (list a b))))` → all 4 pairs summing to 3. *o uses repeated pluso —
+  works for small inputs, slower for larger. 19 new tests, 188/188 cumulative.
+- **2026-05-07** — **Phase 5 piece A — conda**: soft-cut. Mirrors `condu` minus
+  the `onceo` on the head: all head answers are conjuncted through the rest of
+  the chosen clause. 7 new tests including the conda-vs-condu divergence test.
+  169/169 cumulative.
+- **2026-05-07** — **Phase 4 piece B — reverseo + lengtho**: reverseo runs forward
+  cleanly and `run 1`-cleanly backward; lengtho uses Peano-encoded lengths so it
+  works as a true relation in both directions (tests use the encoding directly).
+  10 new tests, 162/162 cumulative.
+- **2026-05-07** — **Phase 4 piece A — appendo canary green**: cons-cell support
+  in `unify.sx` + `(:s head tail)` lazy stream refactor in `stream.sx` + hygienic
+  `Zzz` (gensym'd subst-name) wrapping each `conde` clause + `lib/minikanren/
+  relations.sx` with `nullo` / `pairo` / `caro` / `cdro` / `conso` / `firsto` /
+  `resto` / `listo` / `appendo` / `membero`. 25 new tests in `tests/relations.sx`,
+  152/152 cumulative.
+  - **Three deep fixes shipped together**, all required to make `appendo`
+    terminate in both directions:
+    1. SX has no improper pairs, so a stream cell of mature subst + thunk
+       tail can't use `cons` — moved to a `(:s head tail)` tagged shape.
+    2. `(Zzz g)` wrapped its inner fn in a parameter named `s`, capturing
+       the user goal's own `s` binding (the `(appendo l s ls)` convention).
+       Replaced with `(gensym "zzz-s-")` for hygiene.
+    3. SX cons cells `(:cons h t)` for relational decomposition (so
+       `(conso a d l)` can split a list by head/tail without proper
+       improper pairs); `mk-walk*` re-flattens cons cells back to native
+       lists for clean reification output.
+- **2026-05-07** — **Phase 3 done** (run + reification): `lib/minikanren/run.sx` (~28 lines).
+  `reify`/`reify-s`/`reify-name` for canonical `_.N` rendering of unbound vars in
+  left-to-right occurrence order; `run*` / `run` / `run-n` defmacros. 18 new tests
+  in `tests/run.sx`, including the **first classic miniKanren tests green**:
+  `(run* q (== q 1))` → `(1)`; `(run* q (fresh (x y) (== q (list x y))))` →
+  `((_.0 _.1))`. 128/128 cumulative.
+- **2026-05-07** — **Phase 2 piece D + done** (`condu` / `onceo`): `lib/minikanren/condu.sx`.
+  Both are commitment forms: `onceo` is `(stream-take 1 ...)`; `condu` walks clauses
+  and commits the first one whose head produces an answer. 10 tests in `tests/condu.sx`,
+  110/110 cumulative. Phase 2 complete — ready for Phase 3 (run + reification).
+- **2026-05-07** — **Phase 2 piece C** (`conde`): `lib/minikanren/conde.sx` — single
+  defmacro folding clauses through `mk-disj` with internal `mk-conj`. 9 tests in
+  `tests/conde.sx`, 100/100 cumulative. Confirmed eager DFS ordering for ==-only
+  streams; true interleaving is a Phase 4 concern (paused thunks under recursion).
+- **2026-05-07** — **Phase 2 piece B** (`fresh`): `lib/minikanren/fresh.sx` (~10 lines).
+  defmacro form for nice user-facing syntax + `call-fresh` for programmatic use.
+  9 new tests in `tests/fresh.sx`, 91/91 cumulative.
+- **2026-05-07** — **Phase 2 piece A** (streams + ==/conj/disj): `lib/minikanren/stream.sx`
+  (mzero/unit/mk-mplus/mk-bind/stream-take, ~25 lines of code) + `lib/minikanren/goals.sx`
+  (succeed/fail/==/==-check/conj2/disj2/mk-conj/mk-disj, ~30 lines). Found and noted
+  a host-primitive name clash: `bind` is built in and silently shadows user defines —
+  must use `mk-bind`/`mk-mplus` etc. throughout. 34 tests in `tests/goals.sx`,
+  82/82 cumulative all green. fresh/conde/condu/onceo still pending.
+- **2026-05-07** — **Phase 1 done**: `lib/minikanren/unify.sx` (53 lines, ~22 lines of actual code) +
+  `lib/minikanren/tests/unify.sx` (48 tests, all green). Kit consumption: `walk-with`,
+  `unify-with`, `occurs-with`, `extend`, `empty-subst`, `mk-var`, `is-var?`, `var-name`
+  all supplied by `lib/guest/match.sx`. Local additions: a miniKanren-flavoured cfg
+  (treats native SX lists as cons-pairs via `:ctor-head = :pair`, occurs-check off),
+  `make-var` fresh-counter, deep `mk-walk*` (kit's `walk*` only recurses into `:ctor`
+  form, not native lists), and `mk-unify` / `mk-unify-check` thin wrappers. The kit
+  earns its keep ~3× over by line count — confirms lib-guest match kit is reusable
+  for logic-language hosts as designed.