Tuple type (hm-con "*" TYPES); list type (hm-con "list" (TYPE)).
ocaml-infer-tuple threads substitution through each item left-to-right.
ocaml-infer-list unifies all items with a fresh 'a (giving 'a list for
empty []).
Pretty-printer renders 'Int * Int' for tuples and 'Int list' for lists,
matching standard OCaml notation.
Examples:
fun x y -> (x, y) : 'a -> 'b -> 'a * 'b
fun x -> [x; x] : 'a -> 'a list
[] : 'a list
Per ES, ToPrimitive only accepts strings/numbers/booleans/null
/undefined as primitives — objects AND functions trigger the next
step. Was treating function returns from toString/valueOf as
primitives (recursing to extract a string), so toString returning
a function didn't fall through to valueOf. Widened the dict-only
check to (or (= type "dict") (js-function? result)) in both
js-to-string and js-to-number ToPrimitive paths.
built-ins/String: 85/99 → 86/99. conformance.sh: 148/148.
List: concat/flatten, init, find/find_opt, partition, mapi/iteri,
assoc/assoc_opt. Option: iter/fold/to_list. Result: get_ok/get_error/
map_error/to_option.
Fixed skip-to-boundary! in parser to track let..in / begin..end /
struct..end / for/while..done nesting via a depth counter — without
this, nested-let inside a top-level decl body trips over the
decl-boundary detector. Stdlib functions like List.init / mapi / iteri
use begin..end to make their nested-let intent explicit.
exception NAME [of TYPE] parses to (:exception-def NAME [ARG-SRC]).
Runtime is a no-op: raise/match already work on tagged ctor values, so
'exception E of int;; try raise (E 5) with | E n -> n' end-to-end with
zero new eval logic.
Parser: type [PARAMS] NAME = | Ctor [of T1 [* T2]*] | ...
- PARAMS: optional 'a or ('a, 'b) tyvar list
- AST: (:type-def NAME PARAMS CTORS) with each CTOR (NAME ARG-SOURCES)
- Argument types captured as raw source strings (treated opaquely at
runtime since ctor dispatch is dynamic)
Runtime is a no-op — constructors and pattern matching already work
dynamically. Phase 5 will use these decls to register ctor types for
HM checking.
(take-while-o pred l result): take elements from l while pred holds,
stopping at the first element that fails. (drop-while-o pred l result):
drop matching elements, return the rest including the first non-match.
Together: (take-while p l) ⊕ (drop-while p l) = l, verified by an
end-to-end roundtrip test.
8 new tests, 546/546 cumulative.
(arith-progo start step len result): result is the list
(start, start+step, ..., start+(len-1)*step). Length 0 yields the
empty list. Negative steps and zero step are supported.
Useful for FD-style domain construction:
(arith-progo 1 1 9 dom) -> (1 2 3 4 5 6 7 8 9)
6 new tests, 538/538 cumulative.
Walks the list with a recursive count. On a head match, recurse and
add 1 via pluso-i; on no match (nafc), recurse forwarding the count.
Empty list yields 0.
6 new tests, 532/532 cumulative.
Pattern parser top wraps cons-pat with 'as ident' -> (:pas PAT NAME).
Match clause parser consumes optional 'when GUARD-EXPR' before -> and
emits (:case-when PAT GUARD BODY) instead of :case.
Eval: :pas matches inner pattern then binds the alias name; case-when
checks the guard after a successful match and falls through to the next
clause if the guard is false.
Or-patterns deferred — ambiguous with clause separator without
parens-only support.
Walks the list; if the head appears in the tail (membero), drop it and
recurse; otherwise keep it and recurse. Result preserves only the
*last* occurrence of each value.
Caveat: with input like (1 1 1) the membero check succeeds with
multiplicity, so multiple (1) answers may emerge — each is shape-
identical, but the test deliberately checks every-result-is-(1) rather
than asserting answer count.
5 new tests, 526/526 cumulative.
Demonstrates conda for first-match-wins dispatch over a set of rewrite
rules: 0+x = x, x+0 = x, 0*y = 0, x*0 = 0, 1*x = x, x*1 = x, default
unchanged.
Six rules + a fall-through default, all wrapped in a single conda. The
first clause whose head succeeds commits to that rewrite. The fall-
through default ensures the relation always succeeds with at least the
unchanged input.
6 new tests, 521/521 cumulative.
(flat-mapo rel l result): each element x of l is mapped to a list via
rel x list-from-x, and all such lists are concatenated to form result.
(flat-mapo (fn (x r) (== r (list x x))) (list 1 2 3) q)
-> ((1 1 2 2 3 3))
5 new tests, 515/515 cumulative.
(enumerate-i l result): result is l with each element paired with its
0-based index. (enumerate-from-i n l result): same but starts at n.
(enumerate-i (list :a :b :c) q) -> (((0 :a) (1 :b) (2 :c)))
5 new tests, 501/501 cumulative.
(partitiono pred l yes no) — yes is the elements of l where pred
succeeds; no is the rest. Conde dispatches on each element via the
predicate goal vs nafc-of-the-predicate, threading the head through
the matching output list.
Composes with intarith / membero / etc. for any predicate-shaped goal:
(partitiono (fn (x) (lto-i x 5)) (list 1 7 2 8 3) yes no)
yes -> (1 2 3); no -> (7 8)
5 new tests, 496/496 cumulative.
Composes two appendos: (appendo a b mid) ∧ (appendo mid c r). Runs
forward (concatenate three known lists) and backward (recover any of
the three from the other two and the result).
5 new tests, 491/491 cumulative.
Drop-in fast replacement for Peano lengtho when the count fits in a
host integer. Two conde clauses: empty list -> 0; recurse, n = 1 +
length(tail). Uses pluso-i so the length walks to a native int.
5 new tests, 486/486 cumulative.
Sum and product over a list of ground integers via fold + intarith.
Empty list yields the identity (0 for sum, 1 for product). Recurse
combines the head with the recursively-computed tail value via
pluso-i / *o-i.
9 new tests, 481/481 cumulative.
Two conde clauses each: singleton -> the element; multi -> compare head
against the recursive min/max of the tail and pick. Uses lteo-i / lto-i
for the comparisons, so the input must be ground integers.
mino + maxo can run together: (fresh (mn mx) (mino l mn) (maxo l mx)
(== q (list mn mx))) recovers both.
9 new tests, 472/472 cumulative.
Three conde clauses: empty list / singleton list / two-or-more (where
the first two satisfy lteo-i and the rest is recursively sorted). Uses
ground-only integer comparison (intarith), so the input list must
walk to ground integers.
7 new tests, 463/463 cumulative.
Recursive: empty l1 trivially holds; otherwise the head is in l2 (via
membero) and the tail is a subset. Duplicates in l1 are allowed since
each is independently checked.
7 new tests, 456/456 cumulative.
Two hardcoded paths returned the native marker regardless of user
override: js-invoke-function-method and the lambda branch of
js-to-string. Both now look up Function.prototype.toString via
js-dict-get-walk and invoke it on the function, falling back to
the native marker only if no override exists.
built-ins/String: 84/99 → 85/99. conformance.sh: 148/148.
Mitigation for the cyclic-graph divergence (see tests/cyclic-graph.sx).
Threads a `visited` accumulator through the recursion; each candidate
next-step is gated by `nafc (membero z visited)`. Terminates on graphs
with cycles, no Phase-7 tabling required for the simple acyclic-path
query.
Demonstrates a viable alternative to tabling for the common case where
the user wants finite path enumeration over a graph with cycles.
3 new tests, 449/449 cumulative.
Three conde clauses: empty list -> empty result; head matches x ->
skip and recurse; head differs (nafc-gated) -> keep and recurse.
Distinct from rembero, which removes only the first occurrence.
5 new tests, 446/446 cumulative.
Demo of matche dispatch + conde + recursion for tree traversal:
(matche tree
((:leaf x) (== v x))
((:node l r) (conde ((btree-walko l v)) ((btree-walko r v)))))
Test tree ((1 2) (3 (4 5))) yields all 5 leaves under run*. Also tests
membership (run 1) and absence.
4 new tests, 441/441 cumulative.
Four conso calls express the (a b . rest) -> (b a . rest) rewrite as a
purely relational constraint. Self-inverse on length-2+ lists; runs
forward (swap given input) and backward (recover original from the
swapped form). Fails on lists shorter than 2.
6 new tests, 437/437 cumulative.
(pairlisto l1 l2 pairs): pairs is the zipped list of pairs (l1[i] l2[i]).
Recurses on both l1 and l2 in lockstep, building pairs in parallel.
Runs forward, can recover l1 given l2 and pairs, can recover l2 given
l1 and pairs. Different-length lists fail.
5 new tests, 431/431 cumulative.
(iterate-no rel n x result) holds when applying the 2-arg relation rel
n times (Peano n) starting from x produces result. Base case: zero
iterations means result equals x. Recursive case: rel x mid, then
iterate-no n-1 from mid.
Generalises common chains:
succ iteration: (iterate-no succ-rel n :z q) -> n in Peano
list growth: (iterate-no cons-rel n () q) -> n-element list
4 new tests, 426/426 cumulative.
rev-acco is the standard tail-recursive reverse with an accumulator;
rev-2o starts the accumulator at the empty list. Faster than the
appendo-driven reverseo for forward queries because there is no nested
appendo per element.
Trade-off: rev-acco is asymmetric. The accumulator's initial-empty
cannot be enumerated backwards the way reverseo does, so reverseo is
still the right choice when both directions matter.
A test verifies rev-2o and reverseo agree on forward queries.
6 new tests, 422/422 cumulative.
Classic miniKanren relation. (selecto x rest l) holds when l contains
x at any position with `rest` being everything else. Direct base case
(l = (x . rest)) plus the skip-head recursion that threads the head
through to the result rest.
Run modes: enumerate every (x, rest) split; recover rest given an
element; recover an element given the rest; (and ground/all combinations).
6 new tests, 411/411 cumulative.
Composes two appendos: l = front ++ s ++ back, equivalently
(appendo front-and-s back l) and (appendo front s front-and-s).
Goal order matters: doing the (appendo ground:l) split first makes the
search finitary; the second appendo is then deterministic given
front-and-s and ground s. Reversing the order causes divergence on
failing inputs (the front search becomes unbounded).
7 new tests, 405/405 cumulative.
Two-line definitions over appendo:
(prefixo p l) ≡ ∃rest. (appendo p rest l)
(suffixo s l) ≡ ∃front. (appendo front s l)
Both enumerate all prefixes/suffixes when called with a fresh first
arg, and serve as decision relations when called with both grounded.
9 new tests, 398/398 cumulative.
Two-line definition: a list is a palindrome iff it equals its reverse.
Direct composition of reverseo + ==.
7 new tests: empty / singleton / equal pair / unequal pair /
5-element-yes / 5-element-no / strings.
389/389 cumulative.
Mirrors the structure all-distincto already uses internally: walk the
list, ensure each element is not equal to x via nafc, recurse on tail.
Useful as a constraint-style filter:
(membero x (list 1 2 3 4 5))
(not-membero x (list 2 4))
-> x in {1, 3, 5}
4 new tests, 382/382 cumulative.
repeato: produces (or recognizes) a list of n copies of a value, with n
Peano-encoded. Runs forward, backward (recover the count from a uniform
list), and bidirectionally.
concato: fold-appendo over a list-of-lists. (concato (list (list 1 2)
(list) (list 3 4 5)) q) -> ((1 2 3 4 5)).
10 new tests, 378/378 cumulative.
(tako n l prefix) — prefix is the first n elements of l.
(dropo n l suffix) — suffix is l after dropping the first n.
Both use a Peano natural for the count. Round-trip holds:
(tako n l) ⊕ (dropo n l) = l (verified by an end-to-end test)
9 new tests, 368/368 cumulative.
eveno: zero, or (s (s m)) when m is even.
oddo: one, or (s (s m)) when m is odd.
Both run forward (predicate test on a Peano number) and backward
(enumerate even / odd numbers). The two are mutually exclusive — no
number satisfies both.
12 new tests, 359/359 cumulative.
(defrel (NAME ARGS...) (CLAUSE1 ...) (CLAUSE2 ...) ...) expands to
(define NAME (fn (ARGS...) (conde (CLAUSE1 ...) (CLAUSE2 ...) ...))).
Mirrors Prolog's `name(Args) :- goals.` shape. Inherits the Zzz-on-each-
clause laziness from conde, so user relations defined via defrel
terminate on partial answers without needing manual delay. Tests
redefine membero / listo / pluso through defrel and verify equivalence.
3 new tests, 347/347 cumulative.
Per ES, Boolean.prototype is a Boolean wrapper around false,
Number.prototype wraps 0, String.prototype wraps "". So
Boolean.prototype == false (loose-eq unwraps), and
Object.prototype.toString.call(Number.prototype) ===
"[object Number]". Set __js_*_value__ on each in post-init.
built-ins/Boolean: 23/27 → 24/27, String: 80/99 → 84/99.
conformance.sh: 148/148.
lasto: x is the final element of l. Direct base case (l = (x)) plus
recurse-on-cdr.
init-o: init is l without its last element. Base case for singleton:
(== init ()). Otherwise recurse, threading the head through to the
init result via conso.
Together with appendo, the round-trip init append (list last) = l
holds, which is exercised by an end-to-end test.
8 new tests, 344/344 cumulative.
tests/rdb.sx shows the library as a small Datalog engine over fact
tables. Each table is an SX list of tuples, wrapped by a relation that
does (membero (list ...) table). Queries compose selection, projection,
and joins entirely in run* / fresh / conde / membero / intarith / nafc.
Five queries: dept filter, salary > threshold, employee-project join,
intersection (engineers on a specific project), anyone on multiple
distinct projects.
5 new tests, 336/336 cumulative.
Demonstrates the naive-patho behaviour on a 2-cycle (a <-> b, plus
b -> c). Without Phase-7 tabling, the search produces ever-longer
paths: (a b), (a b a b), (a b a b a b), ... `run 5` truncates to a
finite prefix; `run*` diverges. Documenting this as a regression-style
test gives Phase 7 a concrete starting point.
3 new tests, 331/331 cumulative.
