Split the success-checker out of types.clj
types.clj held the inferencer, the success-type checker, and the driver in one 716-line namespace. Move the self-contained checker into jolt.passes.types.check: the error-domain predicates (not-number?/not-seqable?/not-callable?), the op tables, type-name, check-invoke, and the user-fn registry. These are pure over inferred types and the run's env cells, with no inference, so a check-rule edit can no longer perturb the inferencer. The infer-coupled probes stay in types.clj — isolated-diag-count and check-user-call re-run inference, so moving them would make check depend on the inferencer and reintroduce the cycle. Verbatim move; new ns wired into ei-compiler-ns-files; seed re-minted to the byte-fixpoint.
This commit is contained in:
Yogthos
parent
59e231e40d
commit
70d52ae704
4 changed files with 197 additions and 184 deletions
|
|
@ -130,6 +130,7 @@
|
|||
(cons "jolt.passes.numeric" "jolt-core/jolt/passes/numeric.clj")
|
||||
(cons "jolt.passes.inline" "jolt-core/jolt/passes/inline.clj")
|
||||
(cons "jolt.passes.types.lattice" "jolt-core/jolt/passes/types/lattice.clj")
|
||||
(cons "jolt.passes.types.check" "jolt-core/jolt/passes/types/check.clj")
|
||||
(cons "jolt.passes.types" "jolt-core/jolt/passes/types.clj")
|
||||
(cons "jolt.passes" "jolt-core/jolt/passes.clj")))
|
||||
|
||||
|
|
|
|||
File diff suppressed because one or more lines are too long
|
|
@ -6,6 +6,8 @@
|
|||
propagate param types across a unit / the whole program. Weakly coupled to the
|
||||
IR-rewriting passes — shares the const-shape predicates (jolt.passes.fold)."
|
||||
(:require [jolt.passes.fold :refer [scalar-const? kw-callee? get-callee?]]
|
||||
[jolt.passes.types.check :refer
|
||||
[not-callable? type-name check-invoke register-user-fn!]]
|
||||
[jolt.passes.types.lattice :refer
|
||||
[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
|
||||
|
|
@ -82,8 +84,9 @@
|
|||
;; result of (rand-nth coll-of-structs) etc. types as the element.
|
||||
(def ^:private elem-fns #{"rand-nth" "first" "peek" "last" "nth" "fnext" "second"})
|
||||
|
||||
;; the checker's emission points, defined after infer but referenced from it
|
||||
(declare check-invoke check-user-call register-user-fn! not-callable? type-name)
|
||||
;; defined after infer but referenced from it (the rest of the checker lives in
|
||||
;; jolt.passes.types.check, required above)
|
||||
(declare check-user-call)
|
||||
|
||||
(defn- var-key [fnode] (str (get fnode :ns) "/" (get fnode :name)))
|
||||
|
||||
|
|
@ -463,81 +466,6 @@
|
|||
;; there are no false positives. The table is curated to genuinely-throwing
|
||||
;; cases; lenient ops ((get 5 :k) -> nil, (:k 5) -> nil) are NOT listed.
|
||||
|
||||
;; concrete non-numbers: arithmetic provably throws on these. A union is in the
|
||||
;; error domain only when EVERY member is — if any member is an
|
||||
;; accepted type the call is accepted (no false positive).
|
||||
(defn- not-number? [t]
|
||||
(if (union-type? t)
|
||||
(every? not-number? (umembers t))
|
||||
(or (= t :str) (= t :kw) (= t :phm)
|
||||
(struct-type? t) (vec-type? t) (set-type? t))))
|
||||
|
||||
;; concrete non-seqable scalars: seq/count/first/nth provably throw on these.
|
||||
;; (Strings and collections ARE seqable/countable; :truthy is ambiguous; :nil
|
||||
;; and :any are accepted.) A union throws only when every member does.
|
||||
(defn- not-seqable? [t]
|
||||
(if (union-type? t)
|
||||
(every? not-seqable? (umembers t))
|
||||
(or (= t :num) (= t :kw))))
|
||||
|
||||
;; concrete non-callable values: calling them throws "Cannot call X
|
||||
;; as a function". Only :num and :str — keywords/maps/vectors/sets are IFn,
|
||||
;; :truthy/:any/:nil are ambiguous (accepted). A union is non-callable only when
|
||||
;; every member is.
|
||||
(defn- not-callable? [t]
|
||||
(if (union-type? t)
|
||||
(every? not-callable? (umembers t))
|
||||
(or (= t :num) (= t :str))))
|
||||
|
||||
;; arithmetic / numeric ops: EVERY argument must be a number.
|
||||
(def ^:private num-ops
|
||||
#{"+" "-" "*" "/" "inc" "dec" "mod" "rem" "quot" "min" "max" "abs"
|
||||
"bit-and" "bit-or" "bit-xor" "bit-not" "bit-shift-left" "bit-shift-right"})
|
||||
;; seq/count/index ops: argument 0 must be seqable/countable.
|
||||
(def ^:private seq-ops #{"count" "first" "rest" "next" "seq" "nth"})
|
||||
|
||||
(defn- type-name
|
||||
"Render an inferred type for an error message."
|
||||
[t]
|
||||
(cond (union-type? t)
|
||||
(reduce (fn [s m] (if (= s "") (type-name m) (str s " or " (type-name m))))
|
||||
"" (umembers t))
|
||||
(struct-type? t) "a map"
|
||||
(vec-type? t) "a vector"
|
||||
(set-type? t) "a set"
|
||||
(= t :str) "a string"
|
||||
(= t :kw) "a keyword"
|
||||
(= t :num) "a number"
|
||||
(= t :phm) "a map"
|
||||
:else (str t)))
|
||||
|
||||
(defn- check-invoke
|
||||
"If node is a core-op call whose argument type is provably in the error domain,
|
||||
conj a diagnostic into env's diags cell. arg-types is the vector of inferred
|
||||
argument types; pos is the call form's source offset, carried into each
|
||||
diagnostic."
|
||||
[cn args arg-types pos env]
|
||||
(cond
|
||||
(contains? num-ops cn)
|
||||
(reduce (fn [_ i]
|
||||
(let [t (nth arg-types i)]
|
||||
(when (not-number? t)
|
||||
(swap! (get env :diags) conj
|
||||
{:op cn :argpos i :type (type-name t) :pos pos
|
||||
:msg (str "`" cn "` requires a number, but argument "
|
||||
(inc i) " is " (type-name t))})))
|
||||
nil)
|
||||
nil (range (count args)))
|
||||
(and (contains? seq-ops cn) (> (count args) 0))
|
||||
(let [t (nth arg-types 0)]
|
||||
(when (not-seqable? t)
|
||||
(swap! (get env :diags) conj
|
||||
{:op cn :argpos 0 :type (type-name t) :pos pos
|
||||
:msg (str "`" cn "` requires "
|
||||
(if (= cn "count") "a countable collection" "a seqable")
|
||||
", but argument 1 is " (type-name t))})))
|
||||
:else nil))
|
||||
|
||||
;; --- user-function error domains, opt-in -------------------------------------
|
||||
(defn- all-any-env
|
||||
"tenv binding every param name to :any (the all-ambiguous baseline)."
|
||||
|
|
@ -554,24 +482,6 @@
|
|||
(infer body tenv sub)
|
||||
(count @(get sub :diags))))
|
||||
|
||||
(defn- register-user-fn!
|
||||
"Record a (def name (fn [params] body)) — single fixed arity, not redefinable —
|
||||
for later user-fn call checking. Redefinable/dynamic and multi/variadic fns are
|
||||
skipped (their body is not a stable requirement)."
|
||||
[node env]
|
||||
(let [init (get node :init)
|
||||
m (get node :meta)
|
||||
redefable (and m (or (get m :redef) (get m :dynamic)))]
|
||||
(when (and (not redefable) (= :fn (get init :op)))
|
||||
(let [arities (get init :arities)]
|
||||
(when (= 1 (count arities))
|
||||
(let [ar (first arities)]
|
||||
(when (not (get ar :rest))
|
||||
(swap! (get env :user-sigs) assoc
|
||||
(str (get node :ns) "/" (get node :name))
|
||||
{:name (get node :name)
|
||||
:params (get ar :params) :body (get ar :body)}))))))))
|
||||
|
||||
(defn- check-user-call
|
||||
"Strict mode: report a call to a registered user fn that provably throws —
|
||||
either a WRONG ARITY (the registered fn has one fixed arity, so a different
|
||||
|
|
|
|||
102
jolt-core/jolt/passes/types/check.clj
Normal file
102
jolt-core/jolt/passes/types/check.clj
Normal file
|
|
@ -0,0 +1,102 @@
|
|||
(ns jolt.passes.types.check
|
||||
"Success-type error domains (RFC 0006): the curated tables of which concrete
|
||||
types each core op provably throws on, the diagnostic emitter, and the user-fn
|
||||
signature registry. Pure over inferred types plus the run's `env` cells — no
|
||||
inference — so the inferencer (jolt.passes.types) and these rules can't perturb
|
||||
each other. The inferencer calls these during its walk; the infer-coupled user
|
||||
call probes (re-inference) stay in the inferencer."
|
||||
(:require [jolt.passes.types.lattice :refer
|
||||
[union-type? umembers struct-type? vec-type? set-type?]]))
|
||||
|
||||
;; concrete non-numbers: arithmetic provably throws on these. A union is in the
|
||||
;; error domain only when EVERY member is — if any member is an
|
||||
;; accepted type the call is accepted (no false positive).
|
||||
(defn- not-number? [t]
|
||||
(if (union-type? t)
|
||||
(every? not-number? (umembers t))
|
||||
(or (= t :str) (= t :kw) (= t :phm)
|
||||
(struct-type? t) (vec-type? t) (set-type? t))))
|
||||
|
||||
;; concrete non-seqable scalars: seq/count/first/nth provably throw on these.
|
||||
;; (Strings and collections ARE seqable/countable; :truthy is ambiguous; :nil
|
||||
;; and :any are accepted.) A union throws only when every member does.
|
||||
(defn- not-seqable? [t]
|
||||
(if (union-type? t)
|
||||
(every? not-seqable? (umembers t))
|
||||
(or (= t :num) (= t :kw))))
|
||||
|
||||
;; concrete non-callable values: calling them throws "Cannot call X
|
||||
;; as a function". Only :num and :str — keywords/maps/vectors/sets are IFn,
|
||||
;; :truthy/:any/:nil are ambiguous (accepted). A union is non-callable only when
|
||||
;; every member is.
|
||||
(defn not-callable? [t]
|
||||
(if (union-type? t)
|
||||
(every? not-callable? (umembers t))
|
||||
(or (= t :num) (= t :str))))
|
||||
|
||||
;; arithmetic / numeric ops: EVERY argument must be a number.
|
||||
(def ^:private num-ops
|
||||
#{"+" "-" "*" "/" "inc" "dec" "mod" "rem" "quot" "min" "max" "abs"
|
||||
"bit-and" "bit-or" "bit-xor" "bit-not" "bit-shift-left" "bit-shift-right"})
|
||||
;; seq/count/index ops: argument 0 must be seqable/countable.
|
||||
(def ^:private seq-ops #{"count" "first" "rest" "next" "seq" "nth"})
|
||||
|
||||
(defn type-name
|
||||
"Render an inferred type for an error message."
|
||||
[t]
|
||||
(cond (union-type? t)
|
||||
(reduce (fn [s m] (if (= s "") (type-name m) (str s " or " (type-name m))))
|
||||
"" (umembers t))
|
||||
(struct-type? t) "a map"
|
||||
(vec-type? t) "a vector"
|
||||
(set-type? t) "a set"
|
||||
(= t :str) "a string"
|
||||
(= t :kw) "a keyword"
|
||||
(= t :num) "a number"
|
||||
(= t :phm) "a map"
|
||||
:else (str t)))
|
||||
|
||||
(defn check-invoke
|
||||
"If node is a core-op call whose argument type is provably in the error domain,
|
||||
conj a diagnostic into env's diags cell. arg-types is the vector of inferred
|
||||
argument types; pos is the call form's source offset, carried into each
|
||||
diagnostic."
|
||||
[cn args arg-types pos env]
|
||||
(cond
|
||||
(contains? num-ops cn)
|
||||
(reduce (fn [_ i]
|
||||
(let [t (nth arg-types i)]
|
||||
(when (not-number? t)
|
||||
(swap! (get env :diags) conj
|
||||
{:op cn :argpos i :type (type-name t) :pos pos
|
||||
:msg (str "`" cn "` requires a number, but argument "
|
||||
(inc i) " is " (type-name t))})))
|
||||
nil)
|
||||
nil (range (count args)))
|
||||
(and (contains? seq-ops cn) (> (count args) 0))
|
||||
(let [t (nth arg-types 0)]
|
||||
(when (not-seqable? t)
|
||||
(swap! (get env :diags) conj
|
||||
{:op cn :argpos 0 :type (type-name t) :pos pos
|
||||
:msg (str "`" cn "` requires "
|
||||
(if (= cn "count") "a countable collection" "a seqable")
|
||||
", but argument 1 is " (type-name t))})))
|
||||
:else nil))
|
||||
|
||||
(defn register-user-fn!
|
||||
"Record a (def name (fn [params] body)) — single fixed arity, not redefinable —
|
||||
for later user-fn call checking. Redefinable/dynamic and multi/variadic fns are
|
||||
skipped (their body is not a stable requirement)."
|
||||
[node env]
|
||||
(let [init (get node :init)
|
||||
m (get node :meta)
|
||||
redefable (and m (or (get m :redef) (get m :dynamic)))]
|
||||
(when (and (not redefable) (= :fn (get init :op)))
|
||||
(let [arities (get init :arities)]
|
||||
(when (= 1 (count arities))
|
||||
(let [ar (first arities)]
|
||||
(when (not (get ar :rest))
|
||||
(swap! (get env :user-sigs) assoc
|
||||
(str (get node :ns) "/" (get node :name))
|
||||
{:name (get node :name)
|
||||
:params (get ar :params) :body (get ar :body)}))))))))
|
||||
Loading…
Add table
Add a link
Reference in a new issue