Whole-program param-type inference (closed world) (#226)
Re-derive each app fn's param types from its call sites under --opt, so a record type flows across fn boundaries: a ctor's return reaches a callee param, and a typed vector's element reaches a HOF closure's param. The back end can then bare-index field reads and devirtualize protocol calls at those sites (it reads the resulting :hint/:devirt annotations; consuming them is separate work). This rebuilds the inter-procedural driver the Janet host had — the API (infer-body/reinfer-def) survived the rehost but nothing drove it, and the record-shapes/protocol-methods registries were empty stubs. - records.ss: populate record-shapes (ctor key -> fields/tags/type, resolving nested record field tags) and protocol-methods (method var -> [proto method]) registries at deftype/defprotocol load time; jolt.host accessors materialize them. - passes/types.clj: wp-infer! runs a closed-world fixpoint joining call-site arg types into callee params; reinfer-def re-seeds each def at emit. Self- recursive calls and fn-level recur are collected so a recursive fn's params are constrained by its recursion, not just external callers — else a param the recursion widens (e.g. binary-trees check-tree, whose untagged child can be nil) would be unsoundly typed non-nil. A fn used in value position keeps :any params (callers unknown). Megamorphic sites join to :any. - build.ss: analyze all app forms and run the fixpoint before per-form emit. - run-wp.ss: gate (cross-fn propagation, escape soundness, self-recursion). make test / shakesmoke green, 0 new divergences, selfhost holds. Co-authored-by: Yogthos <yogthos@gmail.com>
This commit is contained in:
parent
32ef74b9b0
commit
09712ec575
8 changed files with 622 additions and 270 deletions
|
|
@ -13,7 +13,7 @@
|
|||
:refer, so jolt.passes stays the only namespace the back end imports.
|
||||
|
||||
Portable Clojure: kernel-tier fns + seed primitives only."
|
||||
(:require [jolt.host :refer [inline-enabled? record-shapes stash-inline!]]
|
||||
(:require [jolt.host :refer [inline-enabled? record-shapes protocol-methods stash-inline!]]
|
||||
[jolt.passes.fold :refer [const-fold]]
|
||||
[jolt.passes.numeric :as numeric]
|
||||
[jolt.passes.inline :refer [inline-node flatten-lets scalar-replace dirty set-rec-shapes!]]
|
||||
|
|
@ -22,6 +22,7 @@
|
|||
set-rtenv! set-vtypes! join-types
|
||||
set-record-shapes! set-map-shapes! set-protocol-methods!
|
||||
reset-escapes! collected-escapes
|
||||
wp-infer! param-seeds-for
|
||||
set-check-mode! take-diags!]]))
|
||||
|
||||
;; Cap on inline -> flatten -> scalar-replace -> const-fold iterations. Each pass
|
||||
|
|
@ -62,13 +63,18 @@
|
|||
;; `this`) to bare field reads per-form, not only under whole-program.
|
||||
;; Same shapes the inline pass uses.
|
||||
_ (set-record-shapes! (record-shapes ctx))
|
||||
_ (set-protocol-methods! (protocol-methods ctx)) ;; devirtualization
|
||||
opt (loop [i 0 n (const-fold node)]
|
||||
(reset! dirty false)
|
||||
(let [n2 (const-fold (scalar-replace (flatten-lets (inline-node n ctx))))]
|
||||
(if (and @dirty (< i inline-fixpoint-cap))
|
||||
(recur (inc i) n2)
|
||||
n2)))]
|
||||
n2)))
|
||||
;; a top-level def whose params the whole-program fixpoint typed gets
|
||||
;; reinferred with those seeds (record types flow in from its callers);
|
||||
;; everything else takes the ordinary per-form inference.
|
||||
seeds (when (= :def (:op opt)) (param-seeds-for (str (:ns opt) "/" (:name opt))))]
|
||||
;; a final const-fold after inference propagates any predicate folded to a
|
||||
;; constant, collapsing the `if` it gates to the taken branch.
|
||||
(const-fold (run-inference opt)))
|
||||
(const-fold (if seeds (reinfer-def opt seeds) (run-inference opt))))
|
||||
(const-fold node))))
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue