Compare commits
5 Commits
loops/kern
...
lib/tcl/up
| Author | SHA1 | Date | |
|---|---|---|---|
| 24d8e362d5 | |||
| 0fbfce949b | |||
| ef0a24f0db | |||
| 30a7dd2108 | |||
| b9d63112e6 |
@@ -1279,7 +1279,7 @@ let run_foundation_tests () =
|
|||||||
assert_true "sx_truthy \"\"" (Bool (sx_truthy (String "")));
|
assert_true "sx_truthy \"\"" (Bool (sx_truthy (String "")));
|
||||||
assert_eq "not truthy nil" (Bool false) (Bool (sx_truthy Nil));
|
assert_eq "not truthy nil" (Bool false) (Bool (sx_truthy Nil));
|
||||||
assert_eq "not truthy false" (Bool false) (Bool (sx_truthy (Bool false)));
|
assert_eq "not truthy false" (Bool false) (Bool (sx_truthy (Bool false)));
|
||||||
let l = { l_params = ["x"]; l_body = Symbol "x"; l_closure = Sx_types.make_env (); l_name = None; l_compiled = None } in
|
let l = { l_params = ["x"]; l_body = Symbol "x"; l_closure = Sx_types.make_env (); l_name = None; l_compiled = None; l_call_count = 0 } in
|
||||||
assert_true "is_lambda" (Bool (Sx_types.is_lambda (Lambda l)));
|
assert_true "is_lambda" (Bool (Sx_types.is_lambda (Lambda l)));
|
||||||
ignore (Sx_types.set_lambda_name (Lambda l) "my-fn");
|
ignore (Sx_types.set_lambda_name (Lambda l) "my-fn");
|
||||||
assert_eq "lambda name mutated" (String "my-fn") (lambda_name (Lambda l))
|
assert_eq "lambda name mutated" (String "my-fn") (lambda_name (Lambda l))
|
||||||
|
|||||||
@@ -4109,4 +4109,25 @@ let () =
|
|||||||
| k :: v :: rest -> ignore (env_bind child (value_to_string k) v); add_bindings rest
|
| k :: v :: rest -> ignore (env_bind child (value_to_string k) v); add_bindings rest
|
||||||
| [_] -> raise (Eval_error "env-extend: odd number of key-val pairs") in
|
| [_] -> raise (Eval_error "env-extend: odd number of key-val pairs") in
|
||||||
add_bindings pairs;
|
add_bindings pairs;
|
||||||
Env child)
|
Env child);
|
||||||
|
|
||||||
|
(* JIT cache control & observability — backed by refs in sx_types.ml to
|
||||||
|
avoid creating a sx_primitives → sx_vm dependency cycle. sx_vm reads
|
||||||
|
these refs to decide when to JIT. *)
|
||||||
|
register "jit-stats" (fun _args ->
|
||||||
|
let d = Hashtbl.create 8 in
|
||||||
|
Hashtbl.replace d "threshold" (Number (float_of_int !Sx_types.jit_threshold));
|
||||||
|
Hashtbl.replace d "compiled" (Number (float_of_int !Sx_types.jit_compiled_count));
|
||||||
|
Hashtbl.replace d "compile-failed" (Number (float_of_int !Sx_types.jit_skipped_count));
|
||||||
|
Hashtbl.replace d "below-threshold" (Number (float_of_int !Sx_types.jit_threshold_skipped_count));
|
||||||
|
Dict d);
|
||||||
|
register "jit-set-threshold!" (fun args ->
|
||||||
|
match args with
|
||||||
|
| [Number n] -> Sx_types.jit_threshold := int_of_float n; Nil
|
||||||
|
| [Integer n] -> Sx_types.jit_threshold := n; Nil
|
||||||
|
| _ -> raise (Eval_error "jit-set-threshold!: (n) where n is integer"));
|
||||||
|
register "jit-reset-counters!" (fun _args ->
|
||||||
|
Sx_types.jit_compiled_count := 0;
|
||||||
|
Sx_types.jit_skipped_count := 0;
|
||||||
|
Sx_types.jit_threshold_skipped_count := 0;
|
||||||
|
Nil)
|
||||||
|
|||||||
@@ -138,6 +138,7 @@ and lambda = {
|
|||||||
l_closure : env;
|
l_closure : env;
|
||||||
mutable l_name : string option;
|
mutable l_name : string option;
|
||||||
mutable l_compiled : vm_closure option; (** Lazy JIT cache *)
|
mutable l_compiled : vm_closure option; (** Lazy JIT cache *)
|
||||||
|
mutable l_call_count : int; (** Tiered-compilation counter — JIT after threshold calls *)
|
||||||
}
|
}
|
||||||
|
|
||||||
and component = {
|
and component = {
|
||||||
@@ -449,7 +450,20 @@ let make_lambda params body closure =
|
|||||||
| List items -> List.map value_to_string items
|
| List items -> List.map value_to_string items
|
||||||
| _ -> value_to_string_list params
|
| _ -> value_to_string_list params
|
||||||
in
|
in
|
||||||
Lambda { l_params = ps; l_body = body; l_closure = unwrap_env_val closure; l_name = None; l_compiled = None }
|
Lambda { l_params = ps; l_body = body; l_closure = unwrap_env_val closure; l_name = None; l_compiled = None; l_call_count = 0 }
|
||||||
|
|
||||||
|
(** {1 JIT cache control}
|
||||||
|
|
||||||
|
Tiered compilation: only JIT a lambda after it's been called [jit_threshold]
|
||||||
|
times. This filters out one-shot lambdas (test harness, dynamic eval, REPLs)
|
||||||
|
so they never enter the JIT cache. Counters are exposed to SX as [(jit-stats)].
|
||||||
|
|
||||||
|
These live here (in sx_types) rather than sx_vm so [sx_primitives] can read
|
||||||
|
them without creating a sx_primitives → sx_vm dependency cycle. *)
|
||||||
|
let jit_threshold = ref 4
|
||||||
|
let jit_compiled_count = ref 0
|
||||||
|
let jit_skipped_count = ref 0
|
||||||
|
let jit_threshold_skipped_count = ref 0
|
||||||
|
|
||||||
let make_component name params has_children body closure affinity =
|
let make_component name params has_children body closure affinity =
|
||||||
let n = value_to_string name in
|
let n = value_to_string name in
|
||||||
|
|||||||
@@ -57,6 +57,9 @@ let () = Sx_types._convert_vm_suspension := (fun exn ->
|
|||||||
let jit_compile_ref : (lambda -> (string, value) Hashtbl.t -> vm_closure option) ref =
|
let jit_compile_ref : (lambda -> (string, value) Hashtbl.t -> vm_closure option) ref =
|
||||||
ref (fun _ _ -> None)
|
ref (fun _ _ -> None)
|
||||||
|
|
||||||
|
(* JIT threshold and counters live in Sx_types so primitives can read them
|
||||||
|
without creating a sx_primitives → sx_vm dependency cycle. *)
|
||||||
|
|
||||||
(** Sentinel closure indicating JIT compilation was attempted and failed.
|
(** Sentinel closure indicating JIT compilation was attempted and failed.
|
||||||
Prevents retrying compilation on every call. *)
|
Prevents retrying compilation on every call. *)
|
||||||
let jit_failed_sentinel = {
|
let jit_failed_sentinel = {
|
||||||
@@ -364,13 +367,21 @@ and vm_call vm f args =
|
|||||||
| None ->
|
| None ->
|
||||||
if l.l_name <> None
|
if l.l_name <> None
|
||||||
then begin
|
then begin
|
||||||
l.l_compiled <- Some jit_failed_sentinel;
|
l.l_call_count <- l.l_call_count + 1;
|
||||||
match !jit_compile_ref l vm.globals with
|
if l.l_call_count >= !Sx_types.jit_threshold then begin
|
||||||
| Some cl ->
|
l.l_compiled <- Some jit_failed_sentinel;
|
||||||
l.l_compiled <- Some cl;
|
match !jit_compile_ref l vm.globals with
|
||||||
push_closure_frame vm cl args
|
| Some cl ->
|
||||||
| None ->
|
incr Sx_types.jit_compiled_count;
|
||||||
|
l.l_compiled <- Some cl;
|
||||||
|
push_closure_frame vm cl args
|
||||||
|
| None ->
|
||||||
|
incr Sx_types.jit_skipped_count;
|
||||||
|
push vm (cek_call_or_suspend vm f (List args))
|
||||||
|
end else begin
|
||||||
|
incr Sx_types.jit_threshold_skipped_count;
|
||||||
push vm (cek_call_or_suspend vm f (List args))
|
push vm (cek_call_or_suspend vm f (List args))
|
||||||
|
end
|
||||||
end
|
end
|
||||||
else
|
else
|
||||||
push vm (cek_call_or_suspend vm f (List args)))
|
push vm (cek_call_or_suspend vm f (List args)))
|
||||||
|
|||||||
@@ -164,13 +164,22 @@ gets the same API for free.
|
|||||||
|
|
||||||
## Rollout
|
## Rollout
|
||||||
|
|
||||||
**Phase 1: Tiered compilation (1-2 days)**
|
**Phase 1: Tiered compilation — IMPLEMENTED (commit b9d63112)**
|
||||||
- Add `l_call_count` to lambda type
|
- ✅ `l_call_count : int` field on lambda type (sx_types.ml)
|
||||||
- Wire counter increment in `cek_call_or_suspend`
|
- ✅ Counter increment + threshold check in cek_call_or_suspend Lambda case (sx_vm.ml)
|
||||||
- Add `jit-set-threshold!` primitive
|
- ✅ Module-level refs in sx_types: `jit_threshold` (default 4), `jit_compiled_count`,
|
||||||
- Default threshold = 1 (no change in behavior)
|
`jit_skipped_count`, `jit_threshold_skipped_count`. Refs live in sx_types so
|
||||||
- Bump default to 4 once test suite confirms stability
|
sx_primitives can read them without creating an import cycle.
|
||||||
- Verify: HS conformance full-suite run completes without JIT saturation
|
- ✅ Primitives: `jit-stats`, `jit-set-threshold!`, `jit-reset-counters!` (sx_primitives.ml)
|
||||||
|
- Verified: 4771/1111 OCaml run_tests, identical to baseline — no regressions.
|
||||||
|
|
||||||
|
**WASM rollout note:** The native binary has Phase 1 active. The browser
|
||||||
|
WASM (`shared/static/wasm/sx_browser.bc.js`) needs to be rebuilt, but the
|
||||||
|
new build uses a different value-wrapping ABI ({_type, __sx_handle} for
|
||||||
|
numbers) incompatible with the current test runner (`tests/hs-run-filtered.js`).
|
||||||
|
For now the test tree pins the pre-rewrite WASM. Resolving the ABI gap
|
||||||
|
is a separate task — either update the test runner to unwrap, or expose
|
||||||
|
a value-marshalling helper from the kernel.
|
||||||
|
|
||||||
**Phase 2: LRU cache (3-5 days)**
|
**Phase 2: LRU cache (3-5 days)**
|
||||||
- Extract `Lambda.l_compiled` into central `sx_jit_cache.ml`
|
- Extract `Lambda.l_compiled` into central `sx_jit_cache.ml`
|
||||||
|
|||||||
133
plans/lib-guest-reflective.md
Normal file
133
plans/lib-guest-reflective.md
Normal file
@@ -0,0 +1,133 @@
|
|||||||
|
# lib/guest/reflective/ — first extraction kit, driven by Tcl uplevel as second consumer
|
||||||
|
|
||||||
|
The `kernel-on-sx` loop accumulated six proposed `lib/guest/reflective/` files (`env.sx`, `combiner.sx`, `evaluator.sx`, `hygiene.sx`, `quoting.sx`, `short-circuit.sx`) but extraction was blocked on the two-consumer rule. This plan opens that block by selecting Tcl's `uplevel`/`upvar` machinery as the second consumer for the **`env.sx`** file specifically — the highest-fit candidate.
|
||||||
|
|
||||||
|
Why Tcl/uplevel for *env*: both Kernel and Tcl implement first-class scope chains with recursive parent-walking lookup, and both expose those scopes to user code (Kernel via `get-current-environment`; Tcl via `uplevel`/`upvar`). The first extraction is the smallest plausible kit that both can credibly use.
|
||||||
|
|
||||||
|
Why not the whole set in one go: the other five files (`combiner.sx`, `evaluator.sx`, `hygiene.sx`, `quoting.sx`, `short-circuit.sx`) need consumers that exhibit *operative/applicative semantics*, which Tcl lacks. They stay deferred until a Scheme or Maru port lands.
|
||||||
|
|
||||||
|
## Discovery — current state, head-to-head
|
||||||
|
|
||||||
|
```
|
||||||
|
Kernel env Tcl frame
|
||||||
|
─────────────────────────────────────────────────────────────────────
|
||||||
|
shape {:knl-tag :env {:level N
|
||||||
|
:bindings DICT :locals DICT
|
||||||
|
:parent ENV-OR-NIL} :parent FRAME-OR-NIL}
|
||||||
|
|
||||||
|
update model MUTABLE (dict-set!) FUNCTIONAL (assoc returns new)
|
||||||
|
|
||||||
|
scope chain parent pointer parent pointer
|
||||||
|
+ explicit :frame-stack
|
||||||
|
on the interp
|
||||||
|
|
||||||
|
construction (kernel-make-env) (make-frame LEVEL PARENT)
|
||||||
|
(kernel-extend-env P)
|
||||||
|
|
||||||
|
lookup (kernel-env-lookup E N) (frame-lookup F N)
|
||||||
|
— raises on miss — returns nil on miss
|
||||||
|
|
||||||
|
bind (kernel-env-bind! E N V) (frame-set-top F N V)
|
||||||
|
— mutates — returns new frame
|
||||||
|
|
||||||
|
presence (kernel-env-has? E N) (frame-lookup F N) then nil-check
|
||||||
|
|
||||||
|
call-stack walk (nothing — only single chain) (tcl-frame-nth STACK LEVEL)
|
||||||
|
— indexes into :frame-stack
|
||||||
|
|
||||||
|
variable alias (nothing) (upvar-alias? V)
|
||||||
|
— alias dict points at
|
||||||
|
level + name in another frame
|
||||||
|
```
|
||||||
|
|
||||||
|
## The genuine overlap
|
||||||
|
|
||||||
|
The recursive parent-walk is identical in spirit. Both languages need:
|
||||||
|
|
||||||
|
1. A scope type with a *bindings dict* and *parent pointer*.
|
||||||
|
2. A *lookup* that walks parents until a hit (or nil/raise on miss).
|
||||||
|
3. A way to *extend* — push a fresh child frame.
|
||||||
|
4. A way to *write a binding* in a chosen frame.
|
||||||
|
|
||||||
|
The genuine divergence is *mutable vs functional update*. Tcl can't switch to mutable bindings without changing `frame-set-top`'s call sites (which return new interp state); Kernel can't switch to functional without rewriting `$define!` semantics (which mutates the dyn-env in place).
|
||||||
|
|
||||||
|
## The proposed API — adapter-driven, like `match.sx`
|
||||||
|
|
||||||
|
`lib/guest/match.sx` solves the same shape-divergence problem with a `cfg` adapter dict: the kit operates on a generic term representation, consumers pass callbacks that bridge their shape to it. The pattern works because the *algorithms* are language-agnostic; only the *data layout* differs.
|
||||||
|
|
||||||
|
`lib/guest/reflective/env.sx` should follow the same pattern.
|
||||||
|
|
||||||
|
```lisp
|
||||||
|
;; Canonical wire shape (default):
|
||||||
|
;; {:refl-tag :env :bindings DICT :parent ENV-OR-NIL}
|
||||||
|
;;
|
||||||
|
;; Adapter cfg keys (for consumers with their own shape):
|
||||||
|
;; :bindings-of — fn (scope) → DICT ; access bindings dict
|
||||||
|
;; :parent-of — fn (scope) → SCOPE-OR-NIL
|
||||||
|
;; :extend — fn (scope) → SCOPE ; child of scope
|
||||||
|
;; :bind! — fn (scope name val) → scope ; functional-or-mutable
|
||||||
|
;;
|
||||||
|
;; Default cfg (refl-default-cfg) implements the canonical wire shape
|
||||||
|
;; with MUTABLE bindings (dict-set!). Tcl provides its own cfg with
|
||||||
|
;; functional bindings and the level field preserved.
|
||||||
|
|
||||||
|
(refl-make-env) ;; canonical, mutable
|
||||||
|
(refl-extend-env PARENT)
|
||||||
|
(refl-env-bind! ENV NAME VAL) ;; mutates; returns ENV
|
||||||
|
(refl-env-has? ENV NAME)
|
||||||
|
(refl-env-lookup ENV NAME) ;; raises on miss
|
||||||
|
(refl-env-lookup-or-nil ENV NAME) ;; for guests that prefer nil
|
||||||
|
|
||||||
|
;; With explicit cfg — for consumers with their own shape:
|
||||||
|
(refl-env-lookup-with CFG SCOPE NAME)
|
||||||
|
(refl-env-bind!-with CFG SCOPE NAME VAL)
|
||||||
|
(refl-env-extend-with CFG SCOPE)
|
||||||
|
```
|
||||||
|
|
||||||
|
The two consumer migrations:
|
||||||
|
|
||||||
|
- **Kernel**: drops `kernel-make-env`, `kernel-extend-env`, `kernel-env-bind!`, `kernel-env-has?`, `kernel-env-lookup`. Replaces with `refl-*` calls on the canonical shape. Rename `:knl-tag` → `:refl-tag`. No semantic change.
|
||||||
|
- **Tcl**: keeps its `{:level :locals :parent}` shape but defines a Tcl-cfg adapter. `frame-lookup` becomes `(refl-env-lookup-with tcl-frame-cfg frame name)`. `frame-set-top` stays where it is — Tcl needs functional updates for the assoc-back-to-interp chain. The kit accommodates both, just like `match.sx` accommodates miniKanren's wire shape and Haskell's term shape.
|
||||||
|
|
||||||
|
## Roadmap
|
||||||
|
|
||||||
|
### Phase 1 — Skeleton + Kernel migration
|
||||||
|
|
||||||
|
- [ ] Create `lib/guest/reflective/env.sx` with the canonical wire shape and mutable defaults.
|
||||||
|
- [ ] Migrate `lib/kernel/eval.sx` to use `refl-make-env` / `refl-extend-env` / `refl-env-*`. Rename `:knl-tag` → `:refl-tag` in env values only (operatives/applicatives keep their own tags for now).
|
||||||
|
- [ ] All 322 Kernel tests must stay green.
|
||||||
|
|
||||||
|
### Phase 2 — Tcl adapter
|
||||||
|
|
||||||
|
- [ ] Add `tcl-frame-cfg` in `lib/tcl/runtime.sx`. Wire it through `frame-lookup` and `tcl-frame-nth` callers via `refl-env-lookup-with`. Keep Tcl's level/locals/parent shape unchanged.
|
||||||
|
- [ ] Tcl test suite (must not regress).
|
||||||
|
|
||||||
|
### Phase 3 — Documentation + cross-reference
|
||||||
|
|
||||||
|
- [ ] Update `plans/kernel-on-sx.md` to mark Phase 7's *env.sx* extraction as DONE (one of six). Keep the other five blocked.
|
||||||
|
- [ ] Add `lib/guest/reflective/env.sx` header docstring listing both consumers and pointing at this plan.
|
||||||
|
|
||||||
|
### Phase 4 — Quick wins identified along the way
|
||||||
|
|
||||||
|
- [ ] Tcl's `tcl-frame-nth` (index into call stack by level) is the start of a *stack-frame protocol* — separate from the scope-chain protocol. Tcl needs it; Kernel doesn't. Document as "language-specific extension on top of the shared kit"; consider extracting later if a third consumer (Scheme `call-with-values`, CL `compiler-let`) needs frame-level indexing.
|
||||||
|
|
||||||
|
## Non-goals
|
||||||
|
|
||||||
|
- **Do not extract `combiner.sx`, `evaluator.sx`, `hygiene.sx`, `quoting.sx`, or `short-circuit.sx`** in this branch. Tcl doesn't have operatives/applicatives; the two-consumer rule isn't satisfied for those files. They stay documented-only in `plans/kernel-on-sx.md` until a Scheme/Maru/CL-fexpr consumer arrives.
|
||||||
|
- **Do not change Tcl's update model to mutable**. The functional `frame-set-top` is structural — it's how Tcl threads the interp through `tcl-var-set`/`tcl-var-get`. Don't break it.
|
||||||
|
- **Do not unify the env-lookup error semantics**. Kernel raises; Tcl returns nil. The kit offers both (`refl-env-lookup` and `refl-env-lookup-or-nil`) and consumers pick.
|
||||||
|
|
||||||
|
## Validation criteria
|
||||||
|
|
||||||
|
The extraction is real iff:
|
||||||
|
|
||||||
|
1. Both consumers compile and pass their full test suites unchanged.
|
||||||
|
2. The shared `env.sx` file is ≥80 LoC (substantial enough to be worth sharing) and ≤200 LoC (small enough that the cfg adapter pattern doesn't become its own framework).
|
||||||
|
3. A third consumer in the future can adopt the kit by writing only the cfg dict — no algorithm changes to `env.sx`.
|
||||||
|
|
||||||
|
## References
|
||||||
|
|
||||||
|
- `plans/kernel-on-sx.md` — the kernel-on-sx loop's chisel notes; the six candidate API surfaces are documented there.
|
||||||
|
- `lib/guest/match.sx` — precedent for the adapter-cfg extraction pattern.
|
||||||
|
- `lib/tcl/runtime.sx` lines 5–22 (`make-frame`, `frame-lookup`, `frame-set-top`) — the Tcl consumer's current implementation.
|
||||||
|
- `lib/kernel/eval.sx` lines 39–82 (env block) — the Kernel consumer's current implementation.
|
||||||
216
plans/minikanren-deferred.md
Normal file
216
plans/minikanren-deferred.md
Normal file
@@ -0,0 +1,216 @@
|
|||||||
|
# miniKanren-on-SX: deferred work
|
||||||
|
|
||||||
|
The main plan (`plans/minikanren-on-sx.md`) carries Phases 1–7 through the
|
||||||
|
naive-tabling milestone. This file collects the four pieces left on the
|
||||||
|
shelf, with enough scope and design notes to drive a follow-up loop.
|
||||||
|
|
||||||
|
Branch convention: keep the same `loops/minikanren` worktree; commit and
|
||||||
|
push to `origin/loops/minikanren`. Squash-merge to `architecture` only
|
||||||
|
when each numbered piece is shipped + tests green.
|
||||||
|
|
||||||
|
Cumulative test count snapshot at squash-merge: **644** across
|
||||||
|
**71 test files**. Every change below should grow the number, not break
|
||||||
|
existing tests.
|
||||||
|
|
||||||
|
## The four pieces
|
||||||
|
|
||||||
|
### Piece A — Phase 7 SLG (cyclic patho, mutual recursion, fixed-point iteration)
|
||||||
|
|
||||||
|
**Problem.** Naive tabling drains the answer stream eagerly, then caches.
|
||||||
|
Recursive tabled calls with the SAME ground key see an empty cache (the
|
||||||
|
in-progress entry never exists), so they recurse and the host
|
||||||
|
overflows. Fibonacci works only because each recursive call has a
|
||||||
|
*different* key; cyclic `patho` and any genuinely self-recursive tabled
|
||||||
|
predicate diverge.
|
||||||
|
|
||||||
|
**Approach** — a small subset of SLG / OLDT resolution, enough to handle
|
||||||
|
the demos in the brief.
|
||||||
|
|
||||||
|
1. **In-progress sentinel.** When a tabled call `T(args)` starts, store
|
||||||
|
`(:in-progress nil)` under its key. Recursive calls into `T(args)`
|
||||||
|
from inside its own computation see the sentinel and return only
|
||||||
|
the answers accumulated so far (initially empty).
|
||||||
|
2. **Answer accumulator.** As each new answer is found, push it into
|
||||||
|
the cache entry: `(:in-progress accumulated-answers)`. After a
|
||||||
|
cycling caller returns, the outer continuation can re-consult the
|
||||||
|
updated cache.
|
||||||
|
3. **Fixed-point iteration.** The driver repeatedly re-runs the goal
|
||||||
|
until no new answers appear in a full pass, then transitions the
|
||||||
|
cache from `:in-progress` to `:done`.
|
||||||
|
4. **Subgoal table.** Track (subgoal, last-seen-cache-version) per
|
||||||
|
subscriber so each consumer only re-reads what it hasn't seen.
|
||||||
|
|
||||||
|
**Suggested artefacts.**
|
||||||
|
- `lib/minikanren/tabling-slg.sx` — new module with `table-slg-2`
|
||||||
|
(parallel to `table-2` from naive tabling). Keep `table-2` working
|
||||||
|
unchanged so Fibonacci/Ackermann don't regress.
|
||||||
|
- `lib/minikanren/tests/cyclic-graph-tabled.sx` — the canonical demo:
|
||||||
|
two-cycle `patho` from a→b→a→b plus a→b→c. With SLG, `(run* q
|
||||||
|
(tab-patho :a :c q))` returns the single shortest path, not divergence.
|
||||||
|
- `lib/minikanren/tests/mutual-recursion.sx` — even/odd via mutual
|
||||||
|
recursion (`even-o n` ↔ `odd-o (n-1)`), tabled at both names.
|
||||||
|
|
||||||
|
**Reference reading.**
|
||||||
|
- TRS chapter on tabling.
|
||||||
|
- "Tabled Logic Programming" — Sagonas & Swift (the XSB / SLG paper).
|
||||||
|
- core.logic's `tabled` macro for an SX-dialect-friendly precedent.
|
||||||
|
|
||||||
|
**Risk.** This is the brief's "research-grade complexity, not a
|
||||||
|
one-iteration item". Plan for 4–6 commits: in-progress sentinel,
|
||||||
|
answer accumulator, fixed-point driver, then one demo per commit.
|
||||||
|
|
||||||
|
### Piece B — Phase 6 polish: bounds-consistency for `fd-plus` / `fd-times`
|
||||||
|
|
||||||
|
**Problem.** Current `fd-plus-prop` and `fd-times-prop` propagate only
|
||||||
|
when two of three operands walk to ground numbers. When all three are
|
||||||
|
domain-bounded vars, the propagator returns `s` unchanged — search has
|
||||||
|
to label down to ground before any narrowing happens.
|
||||||
|
|
||||||
|
**Approach** — narrow domains via interval reasoning even when no operand
|
||||||
|
is ground.
|
||||||
|
|
||||||
|
For `(fd-plus x y z)` with bounded x, y, z:
|
||||||
|
- `x ∈ [z.min − y.max .. z.max − y.min]`
|
||||||
|
- `y ∈ [z.min − x.max .. z.max − x.min]`
|
||||||
|
- `z ∈ [x.min + y.min .. x.max + y.max]`
|
||||||
|
|
||||||
|
For `(fd-times x y z)`: same shape, but with multiplication; need to
|
||||||
|
handle sign cases (negative domain ranges) and the divisor-when-not-zero
|
||||||
|
constraint already in place.
|
||||||
|
|
||||||
|
**Suggested artefacts.**
|
||||||
|
- Patch `fd-plus-prop` and `fd-times-prop` in `lib/minikanren/clpfd.sx`
|
||||||
|
with new `:else` branches that compute new domain bounds and call
|
||||||
|
`fd-set-domain` for each var.
|
||||||
|
- New tests in `lib/minikanren/tests/clpfd-plus.sx` /
|
||||||
|
`clpfd-times.sx` exercising the all-domain case: two domain-bounded
|
||||||
|
vars in the body of a goal, with no labelling, after which their
|
||||||
|
domains have narrowed.
|
||||||
|
- A demo: cryptarithmetic puzzle (see Piece D) using bounds
|
||||||
|
consistency to avoid labelling explosion.
|
||||||
|
|
||||||
|
**Risk.** Low. The math is well-known; just careful min/max arithmetic
|
||||||
|
and watch for edge cases (empty domain after narrowing).
|
||||||
|
|
||||||
|
### Piece C — `=/=` disequality with constraint store
|
||||||
|
|
||||||
|
**Problem.** `nafc` is sound only on ground args; `fd-neq` only on FD
|
||||||
|
domains. There is no general-purpose Prolog-style structural
|
||||||
|
disequality `=/=` that works on logic terms.
|
||||||
|
|
||||||
|
**Approach.** Generalise the FD constraint store to a uniform
|
||||||
|
"constraint store" that carries:
|
||||||
|
- domain map (existing)
|
||||||
|
- *pending disequalities* — a list of `(u v)` pairs that must remain
|
||||||
|
non-unifiable under any future extension.
|
||||||
|
|
||||||
|
After every `==` / `mk-unify`, re-check each pending disequality:
|
||||||
|
- If `(u v)` are now unifiable, fail.
|
||||||
|
- If they're now structurally distinct (no shared substitution can
|
||||||
|
unify), drop from the store (the constraint is satisfied).
|
||||||
|
- Otherwise leave in store.
|
||||||
|
|
||||||
|
**Where it bites.** The kernel currently uses `mk-unify` everywhere.
|
||||||
|
Either:
|
||||||
|
1. Replace `mk-unify` with a constraint-aware wrapper everywhere
|
||||||
|
(intrusive, but principled).
|
||||||
|
2. Keep `mk-unify` for goals that don't use `=/=`, and provide a
|
||||||
|
parallel `==-cs` / `=/=-cs` pair plus an alternative `run*-cs`
|
||||||
|
driver that fires the constraint check after each binding.
|
||||||
|
|
||||||
|
Option 2 mirrors the `fd-fire-store` pattern and stays out of the
|
||||||
|
common path.
|
||||||
|
|
||||||
|
**Suggested artefacts.**
|
||||||
|
- `lib/minikanren/diseq.sx` — disequality store on top of the
|
||||||
|
existing `_fd` reserved key (re-using the constraint list, just
|
||||||
|
with disequality-shaped closures instead of FD propagators).
|
||||||
|
- `=/=` goal that posts a disequality and immediately checks it.
|
||||||
|
- `=/=-test` integration: rewrite a few Phase 5 puzzles using `=/=`
|
||||||
|
instead of `nafc + ==`.
|
||||||
|
- Tests covering: ground-pair fail, partial-pair satisfied later by
|
||||||
|
binding, partial-pair *contradicted* later by binding.
|
||||||
|
|
||||||
|
**Risk.** Medium. The hard cases are *eventual* unifiability — a
|
||||||
|
disequality `(=/= (cons a 1) (cons 2 b))` should hold until both `a`
|
||||||
|
gets bound to `2` and `b` gets bound to `1`. Implementations like
|
||||||
|
core.logic's encode this as a list of "violating bindings" the
|
||||||
|
disequality remembers.
|
||||||
|
|
||||||
|
### Piece D — Bigger CLP(FD) demos: send-more-money + Sudoku 4×4
|
||||||
|
|
||||||
|
**Problem.** The current N-queens demo only verifies the constraint
|
||||||
|
chain end-to-end. The brief's full Phase 6 list includes
|
||||||
|
"send-more-money, N-queens with CLP(FD), map coloring,
|
||||||
|
cryptarithmetic" — most of which exercise *more* than just `fd-neq +
|
||||||
|
fd-distinct`.
|
||||||
|
|
||||||
|
**Approach.** Two concrete puzzles that both stress
|
||||||
|
bounds-consistency (Piece B) once it lands:
|
||||||
|
|
||||||
|
#### send-more-money
|
||||||
|
|
||||||
|
```
|
||||||
|
S E N D
|
||||||
|
+ M O R E
|
||||||
|
---------
|
||||||
|
M O N E Y
|
||||||
|
```
|
||||||
|
|
||||||
|
8 distinct digits ∈ {0..9}, S ≠ 0, M ≠ 0. Encoded as a sum-of-digits
|
||||||
|
equation using `fd-plus` + carry chains.
|
||||||
|
|
||||||
|
Without Piece B (bounds-consistency), the search labels every digit
|
||||||
|
combination upfront — slow but tractable on a fast machine. With
|
||||||
|
Piece B, the impossible high-digit cases prune early.
|
||||||
|
|
||||||
|
Test: a single solution `(9 5 6 7 1 0 8 2)`.
|
||||||
|
|
||||||
|
#### Sudoku 4×4
|
||||||
|
|
||||||
|
Easier than 9×9 but exercises the full pattern:
|
||||||
|
- 16 cells, each ∈ {1..4}
|
||||||
|
- 4 rows, 4 cols, 4 2×2 boxes — 12 `fd-distinct` constraints
|
||||||
|
- Some cells fixed as clues
|
||||||
|
|
||||||
|
A small solver should handle 4×4 in well under a second once
|
||||||
|
bounds-consistency narrows columns / boxes after each label step.
|
||||||
|
|
||||||
|
**Suggested artefacts.**
|
||||||
|
- `lib/minikanren/tests/send-more-money.sx` — single-solution test.
|
||||||
|
- `lib/minikanren/tests/sudoku-4x4.sx` — at least three cluesets:
|
||||||
|
unique solution, multiple solutions, no solution.
|
||||||
|
- Optional: `lib/minikanren/sudoku.sx` with a parameterised
|
||||||
|
`sudoku-n` for both 4×4 and a 9×9 stress test.
|
||||||
|
|
||||||
|
**Risk.** Low–medium for 4×4 + send-more-money once Piece B lands.
|
||||||
|
9×9 Sudoku is a stretch; treat it as a stretch goal once the smaller
|
||||||
|
demos are green.
|
||||||
|
|
||||||
|
## Suggested ordering
|
||||||
|
|
||||||
|
1. **Piece B first** (bounds-consistency for `fd-plus` / `fd-times`).
|
||||||
|
Self-contained, low-risk, and unlocks Piece D's harder puzzles.
|
||||||
|
2. **Piece D** (the two demos). Validates Piece B with concrete
|
||||||
|
puzzles. Doubles as the brief's missing canary tests.
|
||||||
|
3. **Piece C** (`=/=`). Independent track; once shipped, refactor the
|
||||||
|
pet/diff puzzles in Phase 5 to use it instead of nafc.
|
||||||
|
4. **Piece A** (SLG tabling). Last because it's the highest-risk
|
||||||
|
piece; do it when the rest of the library is stable so regressions
|
||||||
|
are easy to spot.
|
||||||
|
|
||||||
|
## Operating ground rules (carry over from the original brief)
|
||||||
|
|
||||||
|
- **Scope:** `lib/minikanren/**` and the two plan files (this one and
|
||||||
|
the original).
|
||||||
|
- **Commit cadence:** one feature per commit. Short factual messages
|
||||||
|
(`mk: piece B — bounds-consistency for fd-plus`).
|
||||||
|
- **Plan updates:** tick boxes here as pieces land; mirror status in
|
||||||
|
`plans/minikanren-on-sx.md` Roadmap.
|
||||||
|
- **Test discipline:** every commit ends with the cumulative count
|
||||||
|
green. No-regression rule from the original brief still applies.
|
||||||
|
- **`sx-tree` MCP only** for `.sx` edits. `sx_validate` after every
|
||||||
|
structural edit.
|
||||||
|
- **Pushing:** `origin/loops/minikanren` only. Never `main`. Squash to
|
||||||
|
`architecture` only with explicit user permission, as we did for
|
||||||
|
the v1 merge.
|
||||||
Reference in New Issue
Block a user