coop/rose-ash
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

ocaml: phase 5 HM def-mut + def-rec-mut at top level (+3 tests, 454 total)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 25s
Details

Browse Source 
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
This commit is contained in:
giles
2026-05-08 19:19:17 +00:00
parent fff8fe2dc8
commit 8c7ad62b44
3 changed files with 93 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

75
lib/ocaml/infer.sx
View File

@@ -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)