simon/jolt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Memoize the success checker's per-fn body re-inference

Browse source 
check-user-call rebuilt the all-:any env once per parameter (O(params^2)) and
re-inferred a callee body at every call site. Build the env once and memoize each
probe by [key i argtype] (and the baseline by [:base key]), cleared per form in
check-form. The global type-env is stable within a form's check and the probe's
calls/escapes side effects aren't read there, so a skipped repeat is observably
identical. (The inline-side re-walk the audit flagged is moot: hc-inline-ir is a
no-op on Chez, so try-inline never reaches body-size/body-closed?.)
This commit is contained in:
Yogthos 2026-06-23 01:54:39 -04:00
parent b8492ad81a
commit 0db08e7571
2 changed files with 137 additions and 116 deletions
Download patch file Download diff file Expand all files Collapse all files

228
host/chez/seed/image.ss
View file

File diff suppressed because one or more lines are too long

25
jolt-core/jolt/passes/types.clj
View file

@ -216,6 +216,12 @@
(def ^:private map-shapes-box (atom false)) (def ^:private map-shapes-box (atom false))
(def ^:private checking-box (atom #{})) ;; keys mid-recheck — cycle guard (def ^:private checking-box (atom #{})) ;; keys mid-recheck — cycle guard
(def ^:private strict-box (atom false)) ;; report against user-fn domains? (def ^:private strict-box (atom false)) ;; report against user-fn domains?
;; Memo for check-user-call's per-fn body re-inference: [:base key] -> baseline
;; diag count, [:arg key i argtype] -> does binding param i to argtype add a
;; diagnostic. Cleared per form (check-form) — the global type-env is stable within
;; one form's check, and isolated-diag-count's calls/escapes side effects are not
;; read there, so skipping a repeat probe is observably identical.
(def ^:private diag-memo-box (atom {}))
;; When true, `infer` emits success-type diagnostics as it types (jolt audit). ;; When true, `infer` emits success-type diagnostics as it types (jolt audit).
;; The checker IS the inference walk now — one O(n) pass that both types and ;; The checker IS the inference walk now — one O(n) pass that both types and
;; checks, instead of a separate check-walk that re-inferred every subtree ;; checks, instead of a separate check-walk that re-inferred every subtree
@ -699,13 +705,25 @@
{:op :user-call :type :arity :pos pos {:op :user-call :type :arity :pos pos
:msg (str "wrong number of args (" nargs ") passed to `" :msg (str "wrong number of args (" nargs ") passed to `"
(:name sig) "` (expected " npar ")")}) (:name sig) "` (expected " npar ")")})
(let [base (isolated-diag-count body (all-any-env params))] ;; all-any-env is built once (was rebuilt per param), and each probe is
;; memoized by [key i argtype] so the same fn re-checked across call
;; sites in this form re-infers its body at most once per (param, type).
(let [base-env (all-any-env params)
base (let [bk [:base key]]
(if (contains? @diag-memo-box bk)
(get @diag-memo-box bk)
(let [b (isolated-diag-count body base-env)]
(swap! diag-memo-box assoc bk b) b)))]
(reduce (reduce
(fn [_ i] (fn [_ i]
(let [at (nth arg-types i)] (let [at (nth arg-types i)]
(when (and (not= at :any) (not= at :truthy)) (when (and (not= at :any) (not= at :truthy))
(let [pe (assoc (all-any-env params) (nth params i) at)] (let [mk [:arg key i at]
(when (> (isolated-diag-count body pe) base) rejects (if (contains? @diag-memo-box mk)
(get @diag-memo-box mk)
(let [r (> (isolated-diag-count body (assoc base-env (nth params i) at)) base)]
(swap! diag-memo-box assoc mk r) r))]
(when rejects
(swap! diag-box conj (swap! diag-box conj
{:op :user-call :argpos i :type (type-name at) :pos pos {:op :user-call :argpos i :type (type-name at) :pos pos
:msg (str "argument " (inc i) " to `" (:name sig) :msg (str "argument " (inc i) " to `" (:name sig)
@ -755,6 +773,7 @@
(reset! strict-box (if strict? true false)) (reset! strict-box (if strict? true false))
(reset! checking-box #{}) (reset! checking-box #{})
(reset! diag-box []) (reset! diag-box [])
(reset! diag-memo-box {})
;; the check IS the inference: one walk that types and emits diagnostics ;; the check IS the inference: one walk that types and emits diagnostics
;; (jolt audit). checking? gates emission so the optimization fixpoint, which ;; (jolt audit). checking? gates emission so the optimization fixpoint, which
;; also calls infer, stays silent. ;; also calls infer, stays silent.