From a029afc127966f66da8d8fc1989638ba2641208c Mon Sep 17 00:00:00 2001 From: Dmitri Sotnikov Date: Mon, 15 Jun 2026 21:43:15 +0000 Subject: [PATCH] Fold type predicates on proven types (jolt-wcw) (#129) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit When the collection-type inference proves an argument's type, number?/ string?/keyword?/record?/nil?/some? fold to a compile-time boolean. A const-fold now runs after inference so a folded predicate propagates and collapses any if it gates to the taken branch. Sound by construction: only a provable answer folds, and only when the argument is side-effect-free (a const or local) so dropping its evaluation is a no-op. Unknown types (:any/:truthy) and impure args keep the call. vector?/set?/map? are left out — the :vec tag conflates a real vector with a range/seq, so vector? could be wrong. 50M-iter loop, same shape isolated with a carry-only control: number? call+ branch 5080ms, predicate folded 1365ms — matching the 1417ms control floor, so the 3.7x is entirely the eliminated call+branch. Co-authored-by: Yogthos --- jolt-core/jolt/passes.clj | 4 +- jolt-core/jolt/passes/types.clj | 43 +++++++++++++++ test/integration/predicate-fold-test.janet | 61 ++++++++++++++++++++++ 3 files changed, 107 insertions(+), 1 deletion(-) create mode 100644 test/integration/predicate-fold-test.janet diff --git a/jolt-core/jolt/passes.clj b/jolt-core/jolt/passes.clj index 80a1270..a1e4ba3 100644 --- a/jolt-core/jolt/passes.clj +++ b/jolt-core/jolt/passes.clj @@ -39,5 +39,7 @@ (if (and @dirty (< i 8)) (recur (inc i) n2) n2)))] - (run-inference opt)) + ;; a final const-fold after inference propagates any predicate folded to a + ;; constant (jolt-wcw), collapsing the `if` it gates to the taken branch. + (const-fold (run-inference opt))) (const-fold node))) diff --git a/jolt-core/jolt/passes/types.clj b/jolt-core/jolt/passes/types.clj index 94752fc..68a31bd 100644 --- a/jolt-core/jolt/passes/types.clj +++ b/jolt-core/jolt/passes/types.clj @@ -249,6 +249,38 @@ :else :any)) :else :any))) +;; Predicate folding (jolt-wcw): a type predicate whose argument's type is +;; PROVEN folds to a compile-time boolean. Only the precise tags are folded — +;; :num/:str/:kw mean exactly that scalar, and a record carries its defrecord +;; :type tag. NOT folded: vector?/set?/map?, because the :vec tag conflates a +;; real vector with a range/seq (so vector? could be wrong) — left for when the +;; lattice distinguishes them. :any and :truthy carry no structural info (a +;; value known only non-nil could be any concrete type), so every predicate is +;; unknown on them. nil?/some? fold because every concrete type here is +;; provably non-nil. +(def ^:private fold-preds + #{"number?" "string?" "keyword?" "record?" "nil?" "some?"}) +(defn- record-t? [t] (and (struct-type? t) (some? (get t :type)))) +(defn- pred-on [pname t] + (cond + (or (= t :any) (= t :truthy)) 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))] + (if (and (seq vs) (not (nil? (first vs))) (apply = vs)) (first vs) nil)) + :else + (case pname + "number?" (= t :num) + "string?" (= t :str) + "keyword?" (= t :kw) + "record?" (record-t? t) + "nil?" false + "some?" true + nil))) +;; Side-effect-free node whose evaluation can be dropped when its predicate +;; folds away (a wider purity analysis can broaden this later). +(defn- pure-node? [n] (let [op (get n :op)] (or (= op :const) (= op :local)))) + (declare infer) ;; HOFs that apply their fn arg to the ELEMENTS of a collection (jolt-d6u, @@ -355,6 +387,17 @@ args (get node :args) n (count args)] (cond + ;; predicate folding (jolt-wcw): a type predicate over a single, + ;; side-effect-free argument whose type PROVES the answer becomes a + ;; boolean constant — eliminating the call, and (once const-fold runs + ;; after inference) collapsing any `if` it gates. Falls through to the + ;; normal call path when the answer isn't provable or the arg is impure. + (and iscall-var (contains? fold-preds cn) (= n 1)) + (let [ar (infer (nth args 0) tenv) + v (pred-on cn (nth ar 0))] + (if (and (not (nil? v)) (pure-node? (nth ar 1))) + [:any {:op :const :val v}] + [(call-ret-type fnode) (assoc node :args [(nth ar 1)])])) ;; (:k m) / (:k m default): the result is m's field type, and if m is a ;; struct the subject is tagged so the back end drops the guard — this ;; types nested access end to end (RFC 0005). diff --git a/test/integration/predicate-fold-test.janet b/test/integration/predicate-fold-test.janet new file mode 100644 index 0000000..d0bf618 --- /dev/null +++ b/test/integration/predicate-fold-test.janet @@ -0,0 +1,61 @@ +# Predicate folding from inference (jolt-wcw): when the collection-type +# inference PROVES the argument's type, a type predicate (number?/string?/ +# keyword?/nil?/some?/record?) folds to a compile-time boolean constant, which +# the trailing const-fold then propagates — collapsing any `if` it gates to the +# taken branch. Sound: only a provable answer folds, and only when the argument +# is side-effect-free (a local or const), so dropping its evaluation is a no-op. +# Mirrors type-infer-test.janet's harness (count a marker in the emitted IR to +# prove the optimization fired, then evaluate to prove it stayed correct). +(import ../../src/jolt/api :as api) +(import ../../src/jolt/backend :as backend) +(import ../../src/jolt/reader :as reader) + +(print "Predicate folding (jolt-wcw)...") + +(os/setenv "JOLT_DIRECT_LINK" "1") +(def ctx (api/init {:compile? true})) +(api/eval-string ctx "(ns pf)") + +(defn code [src] + (string/format "%p" (backend/emit-ir ctx (backend/analyze-form ctx (reader/parse-string src))))) +(defn occurs [src needle] (length (string/find-all needle (code src)))) +(defn ev [src] (api/eval-string ctx src)) + +# --- the predicate call is gone where the type is proven -------------------- +(assert (= 0 (occurs "(fn [] (let [x (+ 1 2)] (number? x)))" "number?")) + "number? on proven :num -> folded, call eliminated") +(assert (= 0 (occurs "(fn [] (let [x \"hi\"] (string? x)))" "string?")) + "string? on proven :str -> folded") +(assert (= 0 (occurs "(fn [] (let [x :k] (keyword? x)))" "keyword?")) + "keyword? on proven :kw -> folded") +(assert (= 0 (occurs "(fn [] (let [x (+ 1 2)] (nil? x)))" "nil?")) + "nil? on a provably non-nil value -> folded") + +# --- the folded constant collapses an if it gates -------------------------- +# the dead branch's literal (200) must be gone after dead-branch removal +(assert (= 0 (occurs "(fn [] (let [x (+ 1 2)] (if (number? x) 100 200)))" "200")) + "true predicate folds the if to its then-branch (dead 200 dropped)") +(assert (= 0 (occurs "(fn [] (let [x (+ 1 2)] (if (string? x) 100 200)))" "100")) + "false predicate folds the if to its else-branch (dead 100 dropped)") + +# --- sound fallback: unknown type or impure arg keeps the call ------------- +# a param is :any (Phase 0 doesn't type it) -> no fold +(assert (= 1 (occurs "(fn [m] (number? m))" "number?")) + "unknown-type arg keeps the predicate call") +# arg type is proven :num but the arg has side effects (a call) -> must NOT +# drop its evaluation, so the predicate is left in place +(assert (>= (occurs "(fn [g] (number? (+ (g) 1)))" "number?") 1) + "impure arg (even with proven type) keeps the predicate call") + +# --- correctness: folded path evaluates to the dispatched path ------------- +(assert (= true (ev "((fn [] (let [x (+ 1 2)] (number? x))))")) "number? true value") +(assert (= false (ev "((fn [] (let [x \"hi\"] (number? x))))")) "number? false value") +(assert (= true (ev "((fn [] (let [x :k] (keyword? x))))")) "keyword? true value") +(assert (= false (ev "((fn [] (let [x 5] (nil? x))))")) "nil? false value") +(assert (= true (ev "((fn [] (let [x 5] (some? x))))")) "some? true value") +(assert (= :yes (ev "((fn [] (let [x 5] (if (number? x) :yes :no))))")) "gated if takes proven branch") +(assert (= :no (ev "((fn [] (let [x 5] (if (string? x) :yes :no))))")) "gated if drops false branch") +# impure arg still runs its side effect and returns the right answer +(assert (= 6 (ev "((fn [g] (if (number? (+ (g) 1)) (+ (g) 5) 0)) (fn [] 1))")) "impure-arg predicate stays correct") + +(print "Predicate folding (jolt-wcw) passed!")