ocaml: phase 5 HM let-mut / let-rec-mut (+3 tests, 442 total)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 30s

ocaml-infer-let-mut: each rhs inferred in parent env, generalized
sequentially before adding to body env.

ocaml-infer-let-rec-mut: pre-bind all names with fresh tvs; infer
each rhs against the joint env, unify each with its tv, then
generalize all and infer body.

Mutual recursion now type-checks:
  let rec even n = if n = 0 then true else odd (n - 1)
  and odd n = if n = 0 then false else even (n - 1)
  in even   : Int -> Bool
This commit is contained in:
2026-05-08 17:28:27 +00:00
parent 4909ebe2ad
commit cabf5dc9c3
3 changed files with 111 additions and 0 deletions

View File

@@ -166,6 +166,94 @@
(let ((s2 (get r2 :subst)) (t2 (get r2 :type)))
{:subst (hm-compose s2 s1) :type t2}))))))))))
;; let x = e1 and y = e2 in body — non-rec multi-binding; each rhs is
;; inferred against the parent env, then generalized and added to body env.
(define ocaml-infer-let-mut
(fn (bindings body env counter)
(let ((subst {}) (env-cur env))
(begin
(define one
(fn (b)
(let ((nm (nth b 0)) (ps (nth b 1)) (rh (nth b 2)))
(let ((rhs-expr (cond
((= (len ps) 0) rh)
(else (list :fun ps rh)))))
(let ((r (ocaml-infer rhs-expr env-cur counter)))
(let ((s (get r :subst)) (t (get r :type)))
(let ((env-after (hm-apply-env s env-cur)))
(let ((scheme (hm-generalize t env-after)))
(begin
(set! subst (hm-compose s subst))
(set! env-cur (assoc env-after nm scheme)))))))))))
(define loop
(fn (xs)
(when (not (= xs (list)))
(begin (one (first xs)) (loop (rest xs))))))
(loop bindings)
(let ((rb (ocaml-infer body env-cur counter)))
(let ((sb (get rb :subst)) (tb (get rb :type)))
{:subst (hm-compose sb subst) :type tb}))))))
;; let rec f = ... and g = ... in body — mutually recursive multi-binding.
;; Pre-bind all names with fresh tvs, infer rhs in joint env, unify with
;; tvs, generalize, infer body.
(define ocaml-infer-let-rec-mut
(fn (bindings body env counter)
(let ((tvs (list)) (env-rec env))
(begin
(define alloc
(fn (xs)
(when (not (= xs (list)))
(let ((b (first xs)))
(let ((nm (nth b 0)) (tv (hm-fresh-tv counter)))
(begin
(append! tvs tv)
(set! env-rec (assoc env-rec nm (hm-monotype tv)))
(alloc (rest xs))))))))
(alloc bindings)
(let ((subst {}) (idx 0))
(begin
(define infer-one
(fn (b)
(let ((ps (nth b 1)) (rh (nth b 2)))
(let ((rhs-expr (cond
((= (len ps) 0) rh)
(else (list :fun ps rh)))))
(let ((r (ocaml-infer rhs-expr env-rec counter)))
(let ((s (get r :subst)) (t (get r :type)))
(let ((s2 (ocaml-hm-unify
(hm-apply s (nth tvs idx))
t
(hm-compose s subst))))
(begin
(set! subst s2)
(set! idx (+ idx 1))))))))))
(define loop
(fn (xs)
(when (not (= xs (list)))
(begin (infer-one (first xs)) (loop (rest xs))))))
(loop bindings)
(let ((env-final (hm-apply-env subst env)))
(begin
(set! idx 0)
(define gen-one
(fn (b)
(let ((nm (nth b 0)))
(let ((scheme (hm-generalize
(hm-apply subst (nth tvs idx))
env-final)))
(begin
(set! env-final (assoc env-final nm scheme))
(set! idx (+ idx 1)))))))
(define loop2
(fn (xs)
(when (not (= xs (list)))
(begin (gen-one (first xs)) (loop2 (rest xs))))))
(loop2 bindings)
(let ((rb (ocaml-infer body env-final counter)))
(let ((sb (get rb :subst)) (tb (get rb :type)))
{:subst (hm-compose sb subst) :type tb}))))))))))
;; let-rec name params = rhs in body — bind name to a fresh tv before
;; inferring rhs, then unify the inferred rhs type with the tv. This
;; lets rhs reference name (recursive call). Generalize after.
@@ -491,6 +579,10 @@
(nth expr 3) (nth expr 4) env counter))
((= tag "let-rec") (ocaml-infer-let-rec (nth expr 1) (nth expr 2)
(nth expr 3) (nth expr 4) env counter))
((= tag "let-mut")
(ocaml-infer-let-mut (nth expr 1) (nth expr 2) env counter))
((= tag "let-rec-mut")
(ocaml-infer-let-rec-mut (nth expr 1) (nth expr 2) env counter))
((= tag "if") (ocaml-infer-if (nth expr 1) (nth expr 2)
(nth expr 3) env counter))
((= tag "tuple") (ocaml-infer-tuple (rest expr) env counter))

View File

@@ -1084,6 +1084,14 @@ cat > "$TMPFILE" << 'EPOCHS'
(epoch 3708)
(eval "(ocaml-run \"Bytes.concat \\\"-\\\" [\\\"a\\\";\\\"b\\\";\\\"c\\\"]\")")
;; ── HM let-mut / let-rec-mut ──────────────────────────────────
(epoch 3800)
(eval "(ocaml-type-of \"let x = 1 and y = 2 in x + y\")")
(epoch 3801)
(eval "(ocaml-type-of \"let rec even n = if n = 0 then true else odd (n - 1) and odd n = if n = 0 then false else even (n - 1) in even\")")
(epoch 3802)
(eval "(ocaml-type-of \"let f x = x + 1 and g x = x * 2 in f 1 + g 2\")")
EPOCHS
OUTPUT=$(timeout 180 "$SX_SERVER" < "$TMPFILE" 2>/dev/null)
@@ -1715,6 +1723,11 @@ check 3706 "Result.fold Ok" '50'
check 3707 "Bytes.length" '5'
check 3708 "Bytes.concat" '"a-b-c"'
# ── HM let-mut / let-rec-mut ───────────────────────────────────
check 3800 "let-mut x+y : Int" '"Int"'
check 3801 "let-rec-mut even" '"Int -> Bool"'
check 3802 "let-mut f and g" '"Int"'
TOTAL=$((PASS + FAIL))
if [ $FAIL -eq 0 ]; then
echo "ok $PASS/$TOTAL OCaml-on-SX tests passed"

View File

@@ -399,6 +399,12 @@ _Newest first._
recognise `!` as the prefix-deref of an application argument, so
`String.concat "" (List.rev !b)` parses as `(... (deref b))`. Buffer
uses a ref holding a string list; contents reverses and concats.
- 2026-05-08 Phase 5 — HM let-mut / let-rec-mut inference (+3 tests,
442 total). `ocaml-infer-let-mut` infers each rhs in the parent env
and generalizes sequentially; `ocaml-infer-let-rec-mut` pre-binds
all names with fresh tvs, infers each rhs against the joint env,
unifies, generalizes, then infers body. Mutual recursion works:
`let rec even n = ... and odd n = ... in even : Int -> Bool`.
- 2026-05-08 Phase 6 — Option/Result/Bytes extensions (+9 tests, 439
total). Option: join, to_result, some, none. Result: value, iter,
fold. Bytes: length, get, of_string, to_string, concat, sub (thin