From 8c7ad62b449447c42c16d0d78f4b734c230654b7 Mon Sep 17 00:00:00 2001 From: giles Date: Fri, 8 May 2026 19:19:17 +0000 Subject: [PATCH] ocaml: phase 5 HM def-mut + def-rec-mut at top level (+3 tests, 454 total) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ocaml-type-of-program now handles :def-mut (sequential generalize) and :def-rec-mut (pre-bind tvs, infer rhs, unify, generalize all, infer body — same algorithm as the inline let-rec-mut version). Mutual top-level recursion now type-checks: let rec even n = ... and odd n = ...;; even 10 : Bool let rec map f xs = ... and length lst = ...;; map : ('a -> 'b) -> 'a list -> 'b list --- lib/ocaml/infer.sx | 75 ++++++++++++++++++++++++++++++++++++++++++++ lib/ocaml/test.sh | 13 ++++++++ plans/ocaml-on-sx.md | 5 +++ 3 files changed, 93 insertions(+) diff --git a/lib/ocaml/infer.sx b/lib/ocaml/infer.sx index c0f8c0f3..18582509 100644 --- a/lib/ocaml/infer.sx +++ b/lib/ocaml/infer.sx @@ -661,6 +661,81 @@ (let ((r (ocaml-infer (nth decl 1) env counter))) (set! last-type (hm-apply (get r :subst) (get r :type))))) + ((= tag "def-mut") + ;; let x = e and y = e' (top level, no rec) + (let ((bindings (nth decl 1))) + (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 counter))) + (let ((s (get r :subst)) (t (get r :type))) + (let ((env2 (hm-apply-env s env))) + (let ((scheme (hm-generalize t env2))) + (begin + (set! env (assoc env2 nm scheme)) + (set! last-type t)))))))))) + (define loop + (fn (xs) + (when (not (= xs (list))) + (begin (one (first xs)) (loop (rest xs)))))) + (loop bindings)))) + ((= tag "def-rec-mut") + ;; let rec f = ... and g = ... — mutual recursion at top level. + (let ((bindings (nth decl 1)) (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)) + (set! last-type (hm-apply s2 t)))))))))) + (define loop2 + (fn (xs) + (when (not (= xs (list))) + (begin (infer-one (first xs)) (loop2 (rest xs)))))) + (loop2 bindings) + (set! env (hm-apply-env subst env)) + (set! idx 0) + (define gen-one + (fn (b) + (let ((nm (nth b 0))) + (let ((scheme (hm-generalize + (hm-apply subst (nth tvs idx)) + env))) + (begin + (set! env (assoc env nm scheme)) + (set! idx (+ idx 1))))))) + (define loop3 + (fn (xs) + (when (not (= xs (list))) + (begin (gen-one (first xs)) (loop3 (rest xs)))))) + (loop3 bindings)))))) (else nil))))) (define loop (fn (xs) diff --git a/lib/ocaml/test.sh b/lib/ocaml/test.sh index b9ad1f6c..1bde32a3 100755 --- a/lib/ocaml/test.sh +++ b/lib/ocaml/test.sh @@ -1116,6 +1116,14 @@ cat > "$TMPFILE" << 'EPOCHS' (epoch 4103) (eval "(ocaml-run \"let r = { x = 1; y = 2 } in r.x <- r.y * 10; r.x\")") +;; ── HM top-level def-mut / def-rec-mut ──────────────────────── +(epoch 4200) +(eval "(ocaml-type-of-program \"let x = 1 and y = 2;; x + y\")") +(epoch 4201) +(eval "(ocaml-type-of-program \"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);; even 10\")") +(epoch 4202) +(eval "(ocaml-type-of-program \"let rec map f xs = match xs with | [] -> [] | h :: t -> f h :: map f t and length lst = match lst with | [] -> 0 | _ :: t -> 1 + length t;; map\")") + EPOCHS OUTPUT=$(timeout 180 "$SX_SERVER" < "$TMPFILE" 2>/dev/null) @@ -1767,6 +1775,11 @@ check 4101 "for-loop accum r.x" '15' check 4102 "r.name <- str" '"Alice"' check 4103 "r.x <- r.y * 10" '20' +# ── HM top-level def-mut / def-rec-mut ───────────────────────── +check 4200 "let-mut x+y" '"Int"' +check 4201 "let-rec-mut even 10" '"Bool"' +check 4202 "let-rec-mut map+length" 'list -> ' + 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 5deb193c..d7ccc61d 100644 --- a/plans/ocaml-on-sx.md +++ b/plans/ocaml-on-sx.md @@ -407,6 +407,11 @@ _Newest first._ binary search tree (`type 'a tree = Leaf | Node of 'a * 'a tree * 'a tree`) with insert + in-order traversal. Tests parametric ADT, recursive match, List.append, List.fold_left. +- 2026-05-08 Phase 5 — HM for top-level `let..and..` decls (+3 + tests, 454 total). `ocaml-type-of-program` now handles `:def-mut` + (sequential generalization) and `:def-rec-mut` (mutual recursion + with shared tvs) decls. Mutual `even`/`odd` and `map`/`length` + type-check at top level. - 2026-05-08 Phase 5.1 — memo_fib.ml baseline (16/16 pass). Memoized fibonacci using `Hashtbl.find_opt` + `Hashtbl.add`. fib(25) = 75025. Demonstrates mutable dict semantics through the OCaml stdlib API.