From cabf5dc9c324068c724619fe7049b26e5540db23 Mon Sep 17 00:00:00 2001 From: giles Date: Fri, 8 May 2026 17:28:27 +0000 Subject: [PATCH] ocaml: phase 5 HM let-mut / let-rec-mut (+3 tests, 442 total) 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 --- lib/ocaml/infer.sx | 92 ++++++++++++++++++++++++++++++++++++++++++++ lib/ocaml/test.sh | 13 +++++++ plans/ocaml-on-sx.md | 6 +++ 3 files changed, 111 insertions(+) diff --git a/lib/ocaml/infer.sx b/lib/ocaml/infer.sx index 84beebf2..c0f8c0f3 100644 --- a/lib/ocaml/infer.sx +++ b/lib/ocaml/infer.sx @@ -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)) diff --git a/lib/ocaml/test.sh b/lib/ocaml/test.sh index 404b707b..c7345ac0 100755 --- a/lib/ocaml/test.sh +++ b/lib/ocaml/test.sh @@ -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" diff --git a/plans/ocaml-on-sx.md b/plans/ocaml-on-sx.md index 742efe40..07a57fac 100644 --- a/plans/ocaml-on-sx.md +++ b/plans/ocaml-on-sx.md @@ -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