Nilable record types + flow-sensitive nil narrowing (#235)
A record-or-nil (a protocol method whose impls return a record in one branch and nil in another, or an `if` over a ctor and nil) now types as a NILABLE record instead of widening to :any. A nilable record still bare-indexes its field reads (jrec-field-at falls back to jolt-get on nil), but some?/nil? do NOT fold on it, so a runtime guard is preserved — and inside (if (some? x) ..) / (if x ..) the then- branch narrows x to the non-nil record, so its reads bare-index AND unbox there. This is what lets the bounced ray type without a hint: scatter returns ScatterResult-or-nil (Metal absorbs some rays), and the consumer reads (:ray scattered) only under (if (some? scattered) ..). The narrowing proves scattered non-nil there. lattice: :nil type; :nil ∨ struct -> nilable struct, ∨ anything else -> :any; nilability is contagious through a struct join, which also now preserves :type when both sides agree (needed so a record ∨ its nilable self stays that record). truthy-type?/field-type/pred-on treat a nilable struct as maybe-nil. types: nil literal -> :nil; an `if` whose test is (some? x)/(nil? x)/x narrows the nilable local x in the proven branch. Ray tracer with NO hints: 38.4s -> 23.9s (~1.6x) — hit-sphere now types fully (0 jolt-get, 57 jrec-field-at, 38 fl-ops), identical to the hand-hinted build. run-narrow.ss gate, incl. the load-bearing check that the nil case still takes the else branch (the guard is not folded away). make test / shakesmoke green, selfhost holds, 0 new divergences. Co-authored-by: Yogthos <yogthos@gmail.com>
This commit is contained in:
parent
f124701393
commit
f920ff6ea2
5 changed files with 420 additions and 280 deletions
10
Makefile
10
Makefile
|
|
@ -4,7 +4,7 @@
|
|||
# build step. `make test` is the full gate. `make remint` rebuilds the seed after a
|
||||
# source change.
|
||||
|
||||
.PHONY: test ci values corpus unit smoke buildsmoke selfhost sci certify ffi transient infer wp devirt fieldread numwp fieldnum protoret directlink numeric inline shakesmoke remint
|
||||
.PHONY: test ci values corpus unit smoke buildsmoke selfhost sci certify ffi transient infer wp devirt fieldread numwp fieldnum protoret narrow directlink numeric inline shakesmoke remint
|
||||
|
||||
# Full gate (dev machine). Includes the self-host byte-fixpoint, which only holds
|
||||
# on the same Chez that minted the seed.
|
||||
|
|
@ -15,7 +15,7 @@ test: selfhost ci
|
|||
# lockfile) — it RUNS correctly on any Chez, but `selfhost` rebuilds it and a
|
||||
# different Chez version may emit byte-different (gensym/order) output, so the
|
||||
# byte-fixpoint is a dev-machine check, not a CI one (jolt-8479).
|
||||
ci: values corpus unit smoke buildsmoke sci ffi transient infer wp devirt fieldread numwp fieldnum protoret directlink numeric inline certify
|
||||
ci: values corpus unit smoke buildsmoke sci ffi transient infer wp devirt fieldread numwp fieldnum protoret narrow directlink numeric inline certify
|
||||
@echo "OK: CI gates passed"
|
||||
|
||||
# Self-host fixpoint: bootstrap.ss rebuild == checked-in seed.
|
||||
|
|
@ -98,6 +98,12 @@ fieldnum:
|
|||
protoret:
|
||||
@chez --script host/chez/run-protoret.ss
|
||||
|
||||
# Nilable record types + flow-sensitive narrowing: a record-or-nil types as a nilable
|
||||
# record (some?/nil? don't fold, so a runtime guard stays); inside (if (some? x) ..)
|
||||
# the then-branch narrows x to non-nil, so its field reads bare-index and unbox.
|
||||
narrow:
|
||||
@chez --script host/chez/run-narrow.ss
|
||||
|
||||
# Direct-linking emission: a closed-world build binds top-level app defs to jv$
|
||||
# Scheme bindings and routes app->app calls/refs to them, skipping var-deref +
|
||||
# jolt-invoke; ^:dynamic/^:redef and nested defs opt out.
|
||||
|
|
|
|||
76
host/chez/run-narrow.ss
Normal file
76
host/chez/run-narrow.ss
Normal file
|
|
@ -0,0 +1,76 @@
|
|||
;; run-narrow.ss — nilable record types + flow-sensitive some?/nil? narrowing.
|
||||
;;
|
||||
;; A protocol method (or `if`) returning a record-or-nil types as a NILABLE record:
|
||||
;; some?/nil? do NOT fold on it (it might be nil), so a runtime guard stays. Inside
|
||||
;; (if (some? x) ..) / (if x ..) the then-branch narrows x to the non-nil record, so
|
||||
;; its field reads bare-index and unbox. This is the ray tracer's
|
||||
;; (let [scattered (scatter ..)] (if (some? scattered) (.. (:ray scattered) ..))).
|
||||
;;
|
||||
;; The load-bearing soundness check: the nil case must still take the else branch —
|
||||
;; narrowing must NOT fold the guard away (else a real nil reaches the bare read).
|
||||
;;
|
||||
;; chez --script host/chez/run-narrow.ss
|
||||
(import (chezscheme))
|
||||
(load "host/chez/rt.ss")
|
||||
(set-chez-ns! "clojure.core")
|
||||
(load "host/chez/seed/prelude.ss")
|
||||
(load "host/chez/post-prelude.ss")
|
||||
(set-chez-ns! "user")
|
||||
(load "host/chez/host-contract.ss")
|
||||
(load "host/chez/seed/image.ss")
|
||||
(load "host/chez/compile-eval.ss")
|
||||
|
||||
(define analyze (var-deref "jolt.analyzer" "analyze"))
|
||||
(define set-record-shapes! (var-deref "jolt.passes.types" "set-record-shapes!"))
|
||||
(define set-protocol-methods! (var-deref "jolt.passes.types" "set-protocol-methods!"))
|
||||
(define wp-infer! (var-deref "jolt.passes.types" "wp-infer!"))
|
||||
(define run-passes (var-deref "jolt.passes" "run-passes"))
|
||||
(define emit (var-deref "jolt.backend-scheme" "emit"))
|
||||
(define (anode src) (analyze (make-analyze-ctx "user") (jolt-ce-read src)))
|
||||
(define (evals src) (jolt-compile-eval (string-append "(do " src ")") "user"))
|
||||
(define (built scm) (eval (read (open-input-string scm)) (interaction-environment)))
|
||||
(define (sub? s t)(let((n(string-length s))(m(string-length t)))(let loop((i 0))(cond((>(+ i m)n)#f)((string=?(substring s i(+ i m))t)#t)(else(loop(+ i 1)))))))
|
||||
(define fails 0) (define total 0)
|
||||
(define (check label actual expected)
|
||||
(set! total (+ total 1))
|
||||
(unless (equal? actual expected)
|
||||
(set! fails (+ fails 1))
|
||||
(printf " FAIL ~a: got ~s expected ~s\n" label actual expected)))
|
||||
|
||||
(evals "(defrecord R [^double k])")
|
||||
(evals "(defprotocol P (m [x]))")
|
||||
(evals "(defrecord A [v] P (m [x] (->R 1.0)))")
|
||||
(evals "(defrecord B [v] P (m [x] (if (< (:v x) 0) (->R 2.0) nil)))") ; B.m returns R-or-nil
|
||||
(set-record-shapes! (chez-record-shapes-map))
|
||||
(set-protocol-methods! (chez-protocol-methods-map))
|
||||
(set-optimize! #t)
|
||||
(define na (anode "(defrecord A [v] P (m [x] (->R 1.0)))"))
|
||||
(define nb (anode "(defrecord B [v] P (m [x] (if (< (:v x) 0) (->R 2.0) nil)))"))
|
||||
;; guarded read: inside (some? s), s narrows to non-nil R -> (:k s) bare-indexes + unboxes
|
||||
(define f (anode "(def f (fn [a] (let [s (m a)] (if (some? s) (* (:k s) 2.0) 0.0))))"))
|
||||
(wp-infer! (jolt-vector na nb f))
|
||||
(define fe (emit (run-passes f (make-analyze-ctx "user"))))
|
||||
(check "guarded nullable read bare-indexes" (sub? fe "jrec-field-at") #t)
|
||||
(check "guarded nullable read unboxes to fl*" (sub? fe "fl*") #t)
|
||||
|
||||
;; CORRECTNESS + the load-bearing soundness check: the nil case must take the else
|
||||
;; branch (the guard is preserved), not run the bare read on nil.
|
||||
(built fe)
|
||||
(define ff (var-deref "user" "f"))
|
||||
(check "non-nil (A.m -> R 1.0)" (jolt-invoke ff (evals "(->A 5)")) 2.0)
|
||||
(check "non-nil (B.m v<0 -> R 2.0)" (jolt-invoke ff (evals "(->B -5)")) 4.0)
|
||||
(check "nil case takes else (guard preserved, no crash)"
|
||||
(jolt-invoke ff (evals "(->B 5)")) 0.0)
|
||||
|
||||
;; an UNGUARDED nullable read must stay safe: jrec-field-at falls back to jolt-get on
|
||||
;; nil. (Its result type is conservative — no unbox — so this just checks no crash.)
|
||||
(define g (anode "(def g (fn [a] (let [s (m a)] (:k s))))"))
|
||||
(define ge (emit (run-passes g (make-analyze-ctx "user"))))
|
||||
(built ge)
|
||||
(define gg (var-deref "user" "g"))
|
||||
(check "unguarded nullable read on nil returns nil" (jolt-nil? (jolt-invoke gg (evals "(->B 5)"))) #t)
|
||||
(check "unguarded nullable read on non-nil returns the field" (jolt-invoke gg (evals "(->A 5)")) 1.0)
|
||||
|
||||
(if (= fails 0)
|
||||
(begin (printf "narrow gate: ~a/~a passed\n" total total) (exit 0))
|
||||
(begin (printf "narrow gate: ~a/~a passed (~a failed)\n" (- total fails) total fails) (exit 1)))
|
||||
File diff suppressed because one or more lines are too long
|
|
@ -13,7 +13,7 @@
|
|||
[velem selem sfields vec-type? set-type? struct-type? mk-vec mk-set
|
||||
mk-struct union-cap scalar-t? union-type? umembers union-of merge-fields
|
||||
join-t join type-depth cap struct-safe? field-type shape-order type-shape
|
||||
mark-struct truthy-type? num-ret-fns vector-ret-fns]]))
|
||||
mark-struct truthy-type? num-ret-fns vector-ret-fns nilable? strip-nilable]]))
|
||||
|
||||
;; --- engine state ------------------------------------------------------------
|
||||
;; The walk threads an immutable `env` (mk-env) instead of reading scattered
|
||||
|
|
@ -143,6 +143,9 @@
|
|||
(defn- pred-on [pname t]
|
||||
(cond
|
||||
(or (= t :any) (= t :truthy)) nil
|
||||
;; a nilable struct might be nil — nil?/some?/record? can't be proven, so the
|
||||
;; runtime guard must stay (this is what makes the narrowing sound).
|
||||
(nilable? t) nil
|
||||
;; a bounded scalar union folds only when every member agrees
|
||||
(union-type? t)
|
||||
(let [vs (map (fn [m] (pred-on pname m)) (umembers t))]
|
||||
|
|
@ -160,6 +163,28 @@
|
|||
;; folds away (a wider purity analysis can broaden this later).
|
||||
(defn- pure-node? [n] (let [op (get n :op)] (or (= op :const) (= op :local))))
|
||||
|
||||
;; Flow-sensitive nil narrowing: in (if (some? x) ..) / (if x ..) / (if (nil? x) ..)
|
||||
;; a nilable-struct local x is proven non-nil in one branch, so its field reads
|
||||
;; bare-index and unbox there. Only a nilable local narrows — nothing else changes.
|
||||
(defn- test-local [test pred-name]
|
||||
(when (= :invoke (get test :op))
|
||||
(let [f (get test :fn) args (get test :args)]
|
||||
(when (and (= :var (get f :op)) (= "clojure.core" (get f :ns))
|
||||
(= pred-name (get f :name))
|
||||
(= 1 (count args)) (= :local (get (nth args 0) :op)))
|
||||
(get (nth args 0) :name)))))
|
||||
(defn- narrow-nonnil [tenv nm]
|
||||
(let [t (get tenv nm)] (if (nilable? t) (assoc tenv nm (strip-nilable t)) tenv)))
|
||||
;; [then-tenv else-tenv] for an `if` whose test narrows a nilable local.
|
||||
(defn- if-narrow [test tenv]
|
||||
(let [somev (test-local test "some?")
|
||||
nilv (test-local test "nil?")]
|
||||
(cond
|
||||
(= :local (get test :op)) [(narrow-nonnil tenv (get test :name)) tenv]
|
||||
somev [(narrow-nonnil tenv somev) tenv]
|
||||
nilv [tenv (narrow-nonnil tenv nilv)]
|
||||
:else [tenv tenv])))
|
||||
|
||||
(declare infer)
|
||||
|
||||
;; infer (and infer-fn-seeded) return a [type node'] tuple — the result type plus
|
||||
|
|
@ -423,7 +448,8 @@
|
|||
(number? v) :num
|
||||
(string? v) :str
|
||||
(keyword? v) :kw
|
||||
(or (nil? v) (= false v)) :any ; nil/false are not struct-eligible
|
||||
(nil? v) :nil ; a record|nil branch types as a nilable record
|
||||
(= false v) :any ; false is not struct-eligible
|
||||
:else :truthy)) ; true, char, ... -> non-nil
|
||||
node]
|
||||
(= op :local)
|
||||
|
|
@ -463,9 +489,11 @@
|
|||
el (if (empty? ets) :any (reduce join (first ets) (rest ets)))]
|
||||
[(cap (mk-set el) type-depth) (assoc node :items (mapv (fn [r] (nth r 1)) irs))])
|
||||
(= op :if)
|
||||
(let [tr (infer (get node :test) tenv env)
|
||||
thn (infer (get node :then) tenv env)
|
||||
els (infer (get node :else) tenv env)]
|
||||
(let [test (get node :test)
|
||||
tr (infer test tenv env)
|
||||
nr (if-narrow test tenv) ; narrow a nilable local in the proven branch
|
||||
thn (infer (get node :then) (nth nr 0) env)
|
||||
els (infer (get node :else) (nth nr 1) env)]
|
||||
[(join (nth thn 0) (nth els 0))
|
||||
(assoc node :test (nth tr 1) :then (nth thn 1) :else (nth els 1))])
|
||||
(= op :do)
|
||||
|
|
|
|||
|
|
@ -79,6 +79,15 @@
|
|||
(= a b) a
|
||||
(nil? a) b
|
||||
(nil? b) a
|
||||
;; :nil is the type of a literal nil. With a struct it forms a NILABLE struct —
|
||||
;; field reads still bare-index (jrec-field-at falls back to jolt-get on nil), but
|
||||
;; some?/nil? won't fold and a guard narrows it back to non-nil. With anything
|
||||
;; else it widens to :any (nil is not a safe scalar/vec — no fl/fx, no bare elem).
|
||||
(or (= a :nil) (= b :nil))
|
||||
(let [o (if (= a :nil) b a)]
|
||||
(cond (= o :nil) :nil
|
||||
(struct-type? o) (assoc o :nilable true)
|
||||
:else :any))
|
||||
;; :double is a flonum refinement of :num: two doubles stay :double (caught by
|
||||
;; = above), but a double joined with anything else loses the flonum guarantee
|
||||
;; and widens to :num before joining — so a param is :double only when EVERY
|
||||
|
|
@ -86,13 +95,18 @@
|
|||
(or (= a :double) (= b :double))
|
||||
(join-t (if (= a :double) :num a) (if (= b :double) :num b))
|
||||
(and (struct-type? a) (struct-type? b))
|
||||
(let [merged (mk-struct (merge-fields (sfields a) (sfields b)))]
|
||||
;; joining two values of the SAME complete shape preserves it — the
|
||||
;; merged struct has the same key set. Different shapes
|
||||
(let [merged (mk-struct (merge-fields (sfields a) (sfields b)))
|
||||
;; joining two values of the SAME complete shape / record type preserves
|
||||
;; it — the merged struct has the same key set. Different shapes/types
|
||||
;; (or an incomplete side) drop it, as the layout is no longer proven.
|
||||
(if (and (get a :shape) (= (get a :shape) (get b :shape)))
|
||||
(assoc merged :shape (get a :shape))
|
||||
merged))
|
||||
merged (if (and (get a :shape) (= (get a :shape) (get b :shape)))
|
||||
(assoc merged :shape (get a :shape)) merged)
|
||||
merged (if (and (get a :type) (= (get a :type) (get b :type)))
|
||||
(assoc merged :type (get a :type)) merged)
|
||||
;; nilability is contagious: a nilable side makes the join nilable.
|
||||
merged (if (or (get a :nilable) (get b :nilable))
|
||||
(assoc merged :nilable true) merged)]
|
||||
merged)
|
||||
(and (vec-type? a) (vec-type? b)) (mk-vec (join-t (velem a) (velem b)))
|
||||
(and (set-type? a) (set-type? b)) (mk-set (join-t (selem a) (selem b)))
|
||||
;; differing kinds: form a scalar union when both sides reduce to scalars
|
||||
|
|
@ -127,7 +141,12 @@
|
|||
;; raw-get-safe (a struct / record): a struct type. The field type of key
|
||||
;; k, if known, else :any.
|
||||
(defn struct-safe? [t] (struct-type? t))
|
||||
(defn field-type [t k] (if (struct-type? t) (get (sfields t) k :any) :any))
|
||||
;; a nilable struct yields :any for every field (the whole value might be nil, so a
|
||||
;; field read can be nil) — conservative + sound. A guard narrows it to non-nil first
|
||||
;; (strip-nilable), after which the real field types flow.
|
||||
(defn field-type [t k] (if (and (struct-type? t) (not (get t :nilable))) (get (sfields t) k :any) :any))
|
||||
(defn nilable? [t] (and (map? t) (get t :nilable) true))
|
||||
(defn strip-nilable [t] (if (and (map? t) (get t :nilable)) (dissoc t :nilable) t))
|
||||
;; Shape (hidden class). A struct type built from a map LITERAL carries
|
||||
;; its complete layout — :shape, the canonical (str-sorted) key vector. The back
|
||||
;; end represents such a map as a shape tuple and reads a field by bare index.
|
||||
|
|
@ -152,7 +171,8 @@
|
|||
;; only when all its values have such a type. Collections are non-nil.
|
||||
(defn truthy-type? [t]
|
||||
(or (= t :num) (= t :double) (= t :str) (= t :kw) (= t :truthy) (= t :phm)
|
||||
(struct-type? t) (vec-type? t) (set-type? t)))
|
||||
(and (struct-type? t) (not (get t :nilable))) ; a nilable struct may be nil
|
||||
(vec-type? t) (set-type? t)))
|
||||
|
||||
;; core fns whose result is a number (so it is non-nil/non-false and, for the
|
||||
;; success-type checker, provably numeric).
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue