ocaml: phase 5 HM ctor inference for option/result (+7 tests, 351 total)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 26s
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 26s
ocaml-hm-ctor-env registers None/Some : 'a -> 'a option, Ok/Error :
'a -> ('a, 'b) result. :con NAME instantiates the scheme; :pcon NAME
ARG-PATS walks arg patterns through the constructor's arrow type,
unifying each.
Pretty-printer renders 'Int option' and '(Int, 'b) result'.
Examples now infer:
fun x -> Some x : 'a -> 'a option
match Some 5 with | None -> 0 | Some n -> n : Int
fun o -> match o with | None -> 0 | Some n -> n : Int option -> Int
Ok 1 : (Int, 'b) result
Error "oops" : ('a, String) result
User type-defs would extend the registry — pending.
This commit is contained in:
@@ -22,6 +22,21 @@
|
||||
|
||||
(define ocaml-hm-empty-subst (fn () {}))
|
||||
|
||||
;; A registry of constructor types so :con / :pcon can be inferred.
|
||||
;; OCaml's stdlib ctors are seeded here; user type-defs would extend
|
||||
;; this in a future iteration.
|
||||
(define ocaml-hm-ctor-env
|
||||
(fn ()
|
||||
(let ((a (hm-tv "a")) (b (hm-tv "b")))
|
||||
(let ((opt-of-a (hm-con "option" (list a)))
|
||||
(res-of-ab (hm-con "result" (list a b))))
|
||||
{"None" (hm-scheme (list "a") opt-of-a)
|
||||
"Some" (hm-scheme (list "a") (hm-arrow a opt-of-a))
|
||||
"Ok" (hm-scheme (list "a" "b") (hm-arrow a res-of-ab))
|
||||
"Error" (hm-scheme (list "a" "b") (hm-arrow b res-of-ab))
|
||||
"true" (hm-monotype (hm-bool))
|
||||
"false" (hm-monotype (hm-bool))}))))
|
||||
|
||||
(define ocaml-hm-builtin-env
|
||||
(fn ()
|
||||
(let ((int-int-int (hm-arrow (hm-int) (hm-arrow (hm-int) (hm-int))))
|
||||
@@ -176,6 +191,42 @@
|
||||
;; Constructor patterns aren't supported here yet (need a type-def
|
||||
;; registry) — :pcon falls through to a fresh tv so they don't break
|
||||
;; inference of mixed clauses.
|
||||
(define ocaml-infer-pcon
|
||||
(fn (name arg-pats env counter)
|
||||
(cond
|
||||
((has-key? ocaml-hm-ctors name)
|
||||
(let ((ctor-type (hm-instantiate (get ocaml-hm-ctors name) counter))
|
||||
(env-cur env) (subst {}))
|
||||
(let ((cur-type (list nil)))
|
||||
(begin
|
||||
(set-nth! cur-type 0 ctor-type)
|
||||
(define loop
|
||||
(fn (xs)
|
||||
(when (not (= xs (list)))
|
||||
(let ((rp (ocaml-infer-pat (first xs) env-cur counter)))
|
||||
(let ((arg-tv (hm-fresh-tv counter))
|
||||
(res-tv (hm-fresh-tv counter)))
|
||||
(let ((s1 (ocaml-hm-unify
|
||||
(nth cur-type 0)
|
||||
(hm-arrow arg-tv res-tv)
|
||||
(hm-compose (get rp :subst) subst))))
|
||||
(let ((s2 (ocaml-hm-unify
|
||||
(hm-apply s1 arg-tv)
|
||||
(hm-apply s1 (get rp :type))
|
||||
s1)))
|
||||
(begin
|
||||
(set! subst s2)
|
||||
(set-nth! cur-type 0 (hm-apply s2 res-tv))
|
||||
(set! env-cur (get rp :env))
|
||||
(loop (rest xs))))))))))
|
||||
(loop arg-pats)
|
||||
{:type (hm-apply subst (nth cur-type 0))
|
||||
:env env-cur
|
||||
:subst subst}))))
|
||||
(else
|
||||
(let ((tv (hm-fresh-tv counter)))
|
||||
{:type tv :env env :subst {}})))))
|
||||
|
||||
(define ocaml-infer-pat
|
||||
(fn (pat env counter)
|
||||
(let ((tag (nth pat 0)))
|
||||
@@ -241,8 +292,9 @@
|
||||
{:type (get rp :type)
|
||||
:env (assoc (get rp :env) alias (hm-monotype (get rp :type)))
|
||||
:subst (get rp :subst)})))
|
||||
((= tag "pcon")
|
||||
(ocaml-infer-pcon (nth pat 1) (rest (rest pat)) env counter))
|
||||
(else
|
||||
;; :pcon and others — fall through to a fresh tv (sound but loose).
|
||||
(let ((tv (hm-fresh-tv counter)))
|
||||
{:type tv :env env :subst {}}))))))
|
||||
|
||||
@@ -302,10 +354,22 @@
|
||||
{:subst subst
|
||||
:type (ocaml-hm-list (hm-apply subst elem-tv))}))))))
|
||||
|
||||
(define ocaml-hm-ctors (ocaml-hm-ctor-env))
|
||||
|
||||
(set! ocaml-infer
|
||||
(fn (expr env counter)
|
||||
(let ((tag (nth expr 0)))
|
||||
(cond
|
||||
((= tag "con")
|
||||
;; (:con NAME) — look up constructor type, instantiate fresh.
|
||||
(let ((name (nth expr 1)))
|
||||
(cond
|
||||
((has-key? ocaml-hm-ctors name)
|
||||
{:subst {}
|
||||
:type (hm-instantiate (get ocaml-hm-ctors name) counter)})
|
||||
(else
|
||||
;; Unknown ctor — treat as a fresh polymorphic type.
|
||||
{:subst {} :type (hm-fresh-tv counter)}))))
|
||||
((= tag "int") {:subst {} :type (hm-int)})
|
||||
((= tag "float") {:subst {} :type (hm-int)}) ;; treat float as int for now
|
||||
((= tag "string") {:subst {} :type (hm-string)})
|
||||
@@ -371,5 +435,12 @@
|
||||
((= head "list")
|
||||
(let ((elem (ocaml-hm-format-type (nth args 0))))
|
||||
(str elem " list")))
|
||||
((= head "option")
|
||||
(let ((elem (ocaml-hm-format-type (nth args 0))))
|
||||
(str elem " option")))
|
||||
((= head "result")
|
||||
(let ((a (ocaml-hm-format-type (nth args 0)))
|
||||
(b (ocaml-hm-format-type (nth args 1))))
|
||||
(str "(" a ", " b ") result")))
|
||||
(else head))))
|
||||
(else (str t)))))
|
||||
|
||||
Reference in New Issue
Block a user