diff --git a/docs/rfc/0004-type-hints.md b/docs/rfc/0004-type-hints.md new file mode 100644 index 0000000..4c84837 --- /dev/null +++ b/docs/rfc/0004-type-hints.md @@ -0,0 +1,128 @@ +# RFC 0004: Type hints and keyword-lookup specialization + +Status: accepted (design note) + +This note describes how Jolt treats Clojure type hints, and the one place it +uses them: a `^:struct` or `^Record` hint on a local lets a constant-keyword +lookup skip its runtime representation guard. It records the rationale, the +soundness contract, the checked mode for catching inaccurate hints, and the +measured effect, so later work does not relitigate it. + +## Background: why the lookup carries a guard + +A Jolt map value has several runtime representations (see RFC on collections and +`src/jolt/core.janet`): a Janet struct for a small all-scalar-key literal map, a +persistent hash map (a table tagged `:jolt/type :jolt/phm`) when a key is a +collection or a value is nil, plus sorted maps, transients, and record/deftype +instances. A record instance is a Janet table tagged `:jolt/deftype` but, like a +struct, it carries no `:jolt/type`, so a raw Janet `(get inst :field)` reads its +fields directly. + +A constant-keyword lookup `(:k m)` compiles to a guarded form: + +```janet +(if (get m :jolt/type) (core-get m k) (get m k)) +``` + +The guard is one opcode. A non-nil `:jolt/type` routes phm/sorted/transient/ +lazy-seq values to `core-get`'s full semantics; everything else (structs, +records, nil, scalars) takes the bare Janet `get`, which matches `core-get` for +keyword keys. The guard is correct and cheap, but on a struct it is a second +`get`: profiling the ray tracer (a naive all-maps program) found keyword lookups +are about half of a render, and the guard is the only avoidable part of each +one. A bare get is roughly 20ns where the guarded form is roughly 36ns. + +Dropping the guard is only safe when the subject is known to be a plain +struct/record rather than a tagged collection. Jolt does not infer that +inter-procedurally (it would be unsound across a dynamic language's call +boundaries). A type hint supplies the same fact soundly, as a programmer +assertion. + +## What the hints mean + +Two hints on a local resolve to the "plain struct/record" assertion, which we +call the `:struct` hint internally: + +- `^:struct` — the value is a plain struct or record map. There is no Clojure + keyword with this meaning (Clojure's type hints are class names), so this is a + Jolt-specific metadata flag, analogous to `^:dynamic`. +- `^Name` where `Name` is a `defrecord`/`deftype`. Both forms define a `->Name` + positional constructor, so the analyzer treats a tag whose `->Name` resolves + as a record type. Record instances are raw-get-safe, so the lookup drops the + guard. A `^String`, `^long`, or any other non-record tag is not a record and + is ignored, exactly as before. + +Every other hint parses and is inert, matching Clojure (S12b in the reader +spec). A hint never changes a program's result; it only permits an +optimization. + +## How it flows + +The reader already keeps `^hint` metadata on the binding symbol and is otherwise +transparent (`reader.janet`, `meta-form->map`). The change threads that fact to +the lookup site: + +1. The analyzer (`jolt-core/jolt/analyzer.clj`) records a `:struct` hint per + local in its env when a param or `let` binding carries `^:struct` or a + record-type tag, and attaches `:hint :struct` to that local's `:local` IR + node. Resolving a record-type tag uses a new host contract function + `record-type?` (`src/jolt/host_iface.janet`), which checks for the `->Name` + constructor. +2. The back end (`emit-kw-lookup` in `src/jolt/backend.janet`) emits the bare get + when the lookup subject is a `:local` carrying the hint, and the guarded form + otherwise. The unhinted path is byte-identical to before. +3. The inline pass (`jolt-core/jolt/passes.clj`) propagates the hint: when it + binds a non-trivial call argument to a fresh local, it carries the called + function's parameter hint onto that local, so lookups inside the spliced body + keep the bare path. Without this, inlining a hinted function would erase the + benefit, because the hinted parameter is replaced by an unhinted temporary. + +The same machinery covers both `(:k m)` and `(get m :k [default])` when the key +is a constant keyword. A `get` with a variable, numeric, or string key falls +through to `core-get` unchanged. + +## Soundness and the checked mode + +An accurate hint is correctness-preserving by construction: for a struct or +record the bare get equals the guarded result. An inaccurate hint (asserting +`^:struct` for a value that is actually a phm) makes the raw get return the wrong +thing. This is the same contract as a wrong Clojure `^String`, except that a +wrong Jolt hint fails silently rather than throwing. + +To make a lie visible without taxing the fast path, `JOLT_CHECK_HINTS=1` keeps +the guard but throws on the tagged arm with a message naming the local and key: + +``` +type hint violated on `m`: (:a m) — value carries :jolt/type +(a phm/sorted/transient/lazy-seq), not the plain struct/record the +^:struct/^Record hint asserts +``` + +This is a development aid, off by default, with zero cost to normal builds (the +flag is read when the lookup is compiled, and the bare get is emitted when it is +off). The flag is part of the image-cache fingerprint. + +## Coverage + +Type hints parse in every position Clojure accepts them and are inert except for +the optimization above. This matches Clojure's "parse and otherwise do nothing" +model, with the difference that Clojure additionally uses hints to avoid +reflection and select primitive arithmetic, which do not apply to a Janet host. + +## Measured effect + +On the ray tracer (`~/src/examples/ray-tracer`, all values are `{:r :g :b}`-style +maps), with inlining on and the hot parameters hinted, a render goes from 13.3s +to 10.9s, about 1.22x, taking it to roughly 7.8x the JVM from 9.4x after the +inline pass. A seeded render produces an identical pixel checksum hinted and +unhinted, confirming the hints are correctness-preserving on the full pipeline. + +## Status and non-goals + +Implemented. Not pursued: inter-procedural shape inference (unsound in a dynamic +language without a guard, which costs as much as the one being removed) and a +shape-based "hidden class" representation (profiling showed allocation is about +1% of the workload, so a cheaper allocation would not help, and an escaping-map +lookup through a runtime shape check costs about the same as the guard it would +replace). The hint is the sound, opt-in lever on the part of the cost that can +move. diff --git a/docs/rfc/0005-structural-type-inference.md b/docs/rfc/0005-structural-type-inference.md new file mode 100644 index 0000000..635e15c --- /dev/null +++ b/docs/rfc/0005-structural-type-inference.md @@ -0,0 +1,245 @@ +# RFC 0005 — Structural collection-type inference + +- **Status**: Implemented (jolt-5uj). Ray tracer 12.8s to 11.0s hint-free, + matching the explicit `^:struct` version; render checksum unchanged. +- **Champions**: jolt maintainers +- **Created**: 2026-06-13 + +## Summary + +Replace jolt's ad-hoc inference lattice with a single recursive **structural +type**, so that the type of a value mirrors the tree shape of the data it +describes. A struct-map carries its field types, a vector its element type, a +function its parameter and return types, recursively. A keyword lookup returns +the looked-up field's type, so nested access like `(:r (:direction ray))` is +typed end to end. This unifies the two facts the current inference tracks +inconsistently (a vector's element type, but not a map's field types), subsumes +the existing inference phases (jolt-99x Phases 0 to 3) as special cases, and +closes the remaining ray-tracer gap without a hint. The system is a +soft-typing-style inference: it never rejects a program, it assigns a concrete +type only when it can prove one, and it falls back to `:any` (and the existing +runtime guard) everywhere else. + +## Motivation + +The inference added in jolt-99x specializes a collection access (drops the +`:jolt/type` guard, emits `pv-count`, and so on) when it can prove the +collection's type. It works, it is sound, and it is fully dynamic-fallback +safe. But its type lattice grew ad hoc: + +- `:struct-map` means "a raw-get-safe map" but carries **no field types**. +- `{:vec ELEM}` carries its **element type**. + +These are the same idea applied to two kinds of child in the data tree, but +only one is tracked. The cost is concrete: in the ray tracer a lookup result +like `(:direction ray)` is typed `:any`, so `(:r (:direction ray))` keeps its +guard, and the `vec3` functions (called all day with such values) cannot be +typed, so the inference reaches only about 3% where the explicit `^:struct` +hint reaches 22%. The hint wins precisely because it asserts the field/param +shape the inference fails to derive. + +The fix is to make the type a structural tree, tagged as precisely as provable. +Then `:struct` tracking and field tracking are one mechanism, the special cases +collapse into one signature table, and nested access is typed by construction. + +## The type lattice + +A type `T` is one of: + +- A scalar tag: `:num`, `:str`, `:kw`, `:bool`, `:char`. (Optionally a coarser + `:nonnil` for "provably not nil and not false", which is what the struct-vs-phm + decision needs; see below.) +- `:nil`. +- `{:struct {field -> T}}` — a raw-get-safe map (Janet struct or record) whose + field `k` has type `(fields k)` or `:any` if absent. The degenerate + `{:struct {}}` is "a struct, fields unknown" and replaces today's + `:struct-map`. +- `{:vec T}` — a vector whose elements have type `T`. +- `{:set T}` — a set of `T`. +- `:phm` — a persistent hash map (NOT raw-get-safe; distinct from `:struct`). +- `{:fn {:params [T...] :ret T}}` — a function (optional precision; the current + flat param/return inference is the zero-arity-detail version of this). +- `:any` — the top. Anything not provably more specific. +- `:bottom` (represented as the absence of a type / `nil` internally) — the + identity for join, used to seed the fixpoint. + +Types are immutable values comparable by structural equality, exactly like the +current `{:vec ELEM}` representation, so they flow across the portable +inference and the Janet orchestrator unchanged. + +### Join (least upper bound) + +``` +join(T, T) = T +join(bottom, T) = T +join({:struct a}, {:struct b}) = {:struct {k -> join(a[k]?:any, b[k]?:any) for k in keys(a) ∪ keys(b)}} +join({:vec a}, {:vec b}) = {:vec join(a, b)} +join({:set a}, {:set b}) = {:set join(a, b)} +join(_, _) = :any ; different constructors +``` + +Two struct types join field-wise; a field present in only one side becomes +`:any` in the result (it might be absent, so a lookup of it is not provably +typed). This is the standard record lattice. + +### Termination: depth cap + +Structural types of recursive data (a tree node that contains a tree node, a +cons cell) would be infinite. To keep types finite and the inter-procedural +fixpoint terminating, structural types are **depth-capped**: beyond a small +depth `D` (proposed `D = 4`) a child type is `:any`. Construction and join both +truncate at `D`. With the cap the lattice has finite height, so the monotone +fixpoint converges. The ray tracer's shapes (vec3 inside ray inside hit-info) +are depth 2 to 3, well inside the cap. + +## Inference rules + +Inference is a forward pass producing `[type node']` for each IR node (the +existing shape), threaded with a local type environment and the +inter-procedural state from Phase 1. The rules are uniform over the structural +type: + +- **Literals.** `{:k v ...}` with constant scalar keys and struct-safe values + builds `{:struct {:k type(v) ...}}`; otherwise `:phm`. `[a b ...]` builds + `{:vec (join type(a) type(b) ...)}`. `#{...}` builds `{:set ...}`. Scalars + build their scalar tag. (The struct-vs-phm condition is the same as the back + end's: scalar keys, and every value provably non-nil and non-false.) +- **Lookup returns the field type.** `(:k m)` / `(get m :k)` where + `m : {:struct fs}` returns `(fs :k)` or `:any`. This is the single rule that + makes nesting work and that unifies field tracking with `:struct` tracking. +- **Indexing returns the element type.** `(nth v i)` / `(v i)` where + `v : {:vec T}` returns `T`. `(first v)` / `(peek v)` likewise. +- **Flow.** `let`/`loop` bind init types; `if` joins the branch types; `do` + takes the tail type. (As today.) +- **Calls use signatures.** Every call result type comes from the callee's + signature: core fns from a fixed signature table (below), user fns from the + inter-procedural fixpoint's inferred signature. + +The Phase 1 inter-procedural fixpoint, recompile, escape gate, and closed-world +assumption (RFC to follow / jolt-767) are unchanged. They now propagate +structural types instead of flat tags. + +## Core function signatures + +The current special cases (`truthy-ret-fns`, `vector-ret-fns`, `elem-fns`, +`hof-table`, and the `conj`/`range`/`reduce`/`mapv` branches) collapse into one +table of **type schemes**, possibly parametric: + +``` +inc, dec, +, -, *, /, mod, ... : (... :num) -> :num +count : (Coll) -> :num +nth : ∀T. ({:vec T}, :num) -> T (3-arg adds a default: -> join(T, default)) +get : ∀T. ({:struct fs}, :k) -> (fs :k) ; const key +first,peek : ∀T. ({:vec T}) -> T +conj : ∀T. ({:vec T}, x) -> {:vec join(T, type(x))} +assoc : ({:struct fs}, :k, v) -> {:struct (assoc fs :k type(v))} ; const key +vec, mapv : ... -> {:vec ...} +range : (...) -> {:vec :num} +rand-nth : ∀T. ({:vec T}) -> T +map, filter, mapv, filterv, reduce, ... ; see HOFs +``` + +Parametric schemes (the `∀T`) are where polymorphism actually matters, and they +give the element/field propagation for free. **Higher-order functions are just +schemes whose parameter is itself a function type**: `reduce`'s scheme says its +function argument is `(Acc, Elem) -> Acc` applied to the collection's element +type, so the closure's element parameter is typed by applying the scheme, +replacing the hand-written `hof-table`. + +## Hints as seeds + +`^:struct x` seeds `x : {:struct {}}` (a struct, fields unknown) at a unit +boundary the inference cannot see across. A future extension could allow a shape +hint `^{:r :num :g :num :b :num}` to seed field types, but once inference is +structural this is rarely needed; the hint stays the escape hatch for genuinely +dynamic boundaries, exactly as today. + +## Soundness + +Unchanged in spirit from the current system: a concrete type is assigned only +when proven (a literal genuinely has those fields; a fn provably returns that +shape), and everything unprovable is `:any`, which keeps the dynamic guard. A +wrong specialization is therefore impossible. The inter-procedural part keeps +the closed-world (optimization-mode) assumption already adopted, which is sound +under whole-program / source-distribution compilation. + +## Relationship to Hindley-Milner and soft typing + +This is HM-shaped with two deliberate departures, which is the textbook +definition of **soft typing** (Wright and Cartwright, "A Practical Soft Type +System for Scheme", 1997 — HM extended with union types and a dynamic type). + +Taken from HM: + +- The **structural type language** (records, vectors, functions as type + constructors). This is the "tree of types". +- **Constraint propagation** and **type schemes** for the core library (the + `∀T` signatures). That parametric polymorphism is exactly what HM provides, + and it is where it matters (generic collection functions like `nth`, + `reduce`, `map`). + +Changed, on purpose: + +- Replace "unify or **fail**" with "**join over a lattice whose top is `:any`**". + The inference never rejects a program; an unprovable spot becomes `:any` and + keeps the runtime guard. This is the "fall back to dynamic when in doubt" + policy made principled. +- **Monovariant** for user functions (the inter-procedural fixpoint plus + inlining cover the practical polymorphism); parametric schemes are kept only + for core functions. + +So: HM structural types and constraint propagation and core-fn schemes, solved +by lattice join with a dynamic top instead of unification-or-fail. Other AOT +inferencers for dynamic languages do the whole-program version of the same +thing (RPython's annotator, Crystal's global inference, Shed Skin), all with a +union/dynamic fallback. + +## Implementation and migration + +This is a refactor that **simplifies** the current code: it deletes the ad-hoc +tag soup and the per-op special cases and replaces them with one recursive type +plus a signature table. + +1. Define the structural type, `join`, the depth cap, and the predicates + (`struct-safe?`, `field-type`, `elem-type`) in `jolt.passes`. +2. Rewrite `infer` so each op produces/consumes structural types: literals + build shapes; `(:k m)` returns the field type; calls consult the signature + table. +3. Move the core-fn knowledge into a signature table (subsumes the existing + tables and HOF handling). +4. The back end keeps reading the use-site type to specialize (guard drop for + `{:struct}`, `pv-count`/`pv-nth` for `{:vec}`), now uniformly. +5. Keep the Phase 1 fixpoint, recompile, escape gate, and triggering as is; they + propagate structural types. + +The phases land incrementally behind the same optimization-mode gate, each +verified against conformance (three modes), the full test gate, and the +ray-tracer benchmark, exactly as the current phases were. + +## Design problems and open questions + +- **Recursion / termination.** Handled by the depth cap (`D = 4`). Open + question: is a fixed cap better than proper recursive (mu) types? A cap is + simpler and sound; mu-types are more precise but add complexity. Proposed: + start with the cap. +- **Compile-time cost.** Structural types are larger and the fixpoint does more + work. Mitigations: the depth cap bounds type size; inference runs only in + optimization mode; the fixpoint iteration count stays bounded. Needs + measurement on a large namespace (clojure.core itself) to confirm acceptable. +- **Heterogeneous data.** `[1 "a"]` joins to `{:vec :any}`; a map whose field + varies across branches joins that field to `:any`. Correct degradation, not a + problem, but worth stating. +- **Non-constant keys.** `(assoc m k v)` / `(:k m)` with a non-constant `k` + cannot track a specific field; the result degrades to `{:struct {}}` or + `:phm` as appropriate. Field tracking only applies to constant scalar keys. +- **`false`/`nil` field values.** A map literal is `{:struct ...}` only when + every value is provably non-nil and non-false (the back end stores such maps + as a phm). The `:nonnil` tag (or a per-type "provably truthy" predicate) is + what the literal rule needs; this must be carried correctly or struct + inference is unsound. +- **Function-type precision.** `{:fn ...}` is optional. The current flat + param/return inference is enough for the collection-specialization goal; + full function types matter more for the type-checker (RFC 0006) and could be + deferred. +- **Closed-world boundary.** Inherited from Phase 1: param/return inference + assumes the compiled unit is the whole program. Documented there; unchanged. diff --git a/docs/rfc/0006-success-type-checking.md b/docs/rfc/0006-success-type-checking.md new file mode 100644 index 0000000..fd6fbd8 --- /dev/null +++ b/docs/rfc/0006-success-type-checking.md @@ -0,0 +1,232 @@ +# RFC 0006 — Compile-time detection of provably-wrong code (success typing) + +- **Status**: Implemented. Core-fn error domains (arithmetic on non-numbers, + count/first/rest/next/seq/nth on non-seqable scalars), `JOLT_TYPE_CHECK= + off|warn|error`. Follow-ups landed: bounded scalar **unions** (jolt-pz5) so a + use is reported only when every member is in the error domain; **user-fn + error domains** behind `JOLT_TYPE_CHECK_USER` (jolt-zo1, closed-world); + precise **file:line:col** locations (jolt-fqy). The checker is now one + inference walk (folded into `infer`), and is **on by default in direct-link + builds** — where it piggybacks on the specialization inference for ~free — + and opt-in (`JOLT_TYPE_CHECK`) in plain builds. +- **Champions**: jolt maintainers +- **Created**: 2026-06-13 +- **Depends on**: RFC 0005 (structural collection-type inference) + +## Summary + +Reuse the structural type inference of RFC 0005 as a **loose type checker**: at +compile time, flag code that is *provably* wrong, accept everything that is +merely ambiguous, and never produce a false positive. Concretely, when an +expression's inferred type is concrete and the operation applied to it would +throw at runtime for that type (for example passing a string where a function +only ever operates on numbers), report a clear compile-time error pointing at +the offending form, with the inferred type and what was expected. When the type +is `:any`, a union that includes a valid case, or beyond the inference's depth +cap, accept it silently. This is **success typing** (the discipline behind +Erlang's Dialyzer), applied to jolt for free on top of the inference we already +need for optimization. + +## Motivation + +Once the compiler tracks concrete types for many values (RFC 0005), it can see +some programs that cannot possibly be correct: `(inc "x")`, `(first 5)`, +`(count :k)`, `(/ 1 "two")`. Today these compile and fail at runtime, often far +from the cause. Reporting them at compile time, with a precise location and +message, turns a class of runtime crashes into immediate, actionable feedback, +at no extra inference cost. + +The design constraint the user set is the right one and is exactly success +typing's contract: **accept ambiguous cases, reject only provably-wrong ones.** +A checker that never lies about errors is one developers trust and that does not +get in the way of correct-but-untypeable dynamic code. + +## Principle: success typing, never a false positive + +Success typing (Lindahl and Sagonas, "Practical Type Inference Based on Success +Typings", 2006; the basis of Dialyzer) inverts the usual type-checker stance. +A normal checker accepts only what it can prove correct and rejects the rest +(false positives on dynamic code). A success typer accepts everything that +*could* be correct and rejects only what *cannot* be correct under any +execution. It is sound for **rejection**: if it reports an error, the code is +genuinely wrong. It is intentionally incomplete: it misses errors it cannot +prove. That is the correct trade for a dynamic language, and it matches the +user's "accept ambiguous, reject provably wrong". + +Mapped onto jolt: + +- The inference assigns a value a concrete type only when it can prove it + (RFC 0005). Unprovable is `:any`. +- A use site is reported **iff** the argument's inferred type is concrete and + lies entirely outside the operation's accepted domain, where the operation + *throws* on that domain (not merely returns a benign default). +- `:any`, a depth-capped child, or a union that includes an accepted type is + **never** reported. + +## What "provably wrong" means + +The checker needs, per operation it understands, an **error domain**: the set +of argument types for which the operation throws at runtime. This is narrower +than "the types it is documented to accept", because Clojure is lenient in many +places and flagging a benign case would be a false positive: + +- `(get 5 :k)` returns `nil`, it does not throw. NOT reported. +- `(:k 5)` returns `nil`. NOT reported. +- `(count 5)` throws ("count not supported on number"). Reported when the + argument is provably a non-countable scalar. +- `(first 5)` throws (not seqable). Reported for a provably non-seqable scalar. +- `(inc "x")`, `(+ 1 "x")` throw. Reported when an argument is provably a + non-number (`:str`, `:kw`, `:struct`, `:vec`, ...). +- `(nth 5 0)` throws. Reported for a provably non-indexable scalar. + +So the checker ships a curated table of the clearest throwing operations with +their error domains. It starts small (arithmetic on non-numbers, seq/`count`/ +`nth`/`first` on non-seqables) and grows conservatively. Anything not in the +table is not checked, which is safe (no false positive). + +A use site is reported only when: + +1. the argument's inferred type `T` is concrete (not `:any`, not a union that + includes an accepted type, not truncated by the depth cap), and +2. `T` is in the operation's error domain (the operation provably throws on `T`). + +## Examples + +```clojure +(inc "x") ; ERROR: inc expects a number, got a string +(let [n "x"] (inc n)) ; ERROR: same, n inferred :str +(count :foo) ; ERROR: count not supported on :kw +(first 42) ; ERROR: 42 is not seqable +(:k 5) ; accepted (returns nil, not an error) +(inc (rand-nth coll)) ; accepted if the element type is :any/unknown +(inc (if c 1 "x")) ; accepted: union {:num, :str} includes :num (ambiguous) +(defn f [n] (inc n)) ... ; if f is ALWAYS called with strings in-unit, ERROR at the call; + ; if its callers are unknown/varied, accepted +``` + +## Error reporting + +A reported error includes: + +- the source location (`file:line:col`) of the offending form; +- the operation and the parameter position; +- the inferred type of the argument, rendered readably (`:str`, + `{:struct {:r :num}}`, `{:vec :any}`); +- what the operation requires (`a number`, `a seqable`). + +Example: + +``` +type error scene.clj:42:18: `inc` requires a number, but argument 1 is a string +``` + +Errors are attributed to the form the user wrote. For macro-expanded code, the +checker reports at the original form's recorded position (the loader already +tracks `:error-pos`), never at synthesized internals. + +## Strictness levels + +`JOLT_TYPE_CHECK` controls behavior: + +- **off** — no checking. +- **warn** — report to stderr, do not fail compilation. **The default in + direct-link builds**, where checking rides the specialization inference for + ~free; opt-in elsewhere. +- **error** — fail compilation on a provable type error. Opt-in for CI / strict + builds. + +When `JOLT_TYPE_CHECK` is unset, checking is **on (`warn`) in direct-link +builds** and **off in plain REPL/dev builds** (where it would cost a standalone +inference pass, ~2.6× compile). `JOLT_TYPE_CHECK_USER` additionally enables +reporting against inferred user-function domains (closed-world; see below). + +Because the checker only fires on provable errors, even `error` mode cannot +break a correct program: a correct program has no provable type errors to +report. (A correct-but-untypeable program is simply not reported, since its +types degrade to `:any`.) + +## Soundness of rejection (no false positives) + +The whole value of this feature is that a reported error is real. The +guarantees: + +- The inference assigns concrete types only when provable (RFC 0005). So a + concrete `T` at a use site is a genuine lower bound on what flows there in the + analyzed world. +- The error-domain table lists only operations that genuinely throw on the + listed types, verified against the runtime. +- Ambiguity is always accepted: `:any`, unions containing an accepted type, and + depth-capped children are never reported. + +Two boundaries need care and bound where the checker is allowed to fire: + +- **Closed-world / redefinition.** Inter-procedural argument types assume the + compiled unit is the whole program (inherited from RFC 0005). For the checker, + this means a reported error on a *user* function's parameter is only as sound + as that assumption. The conservative initial policy: only report against + **core-function** error domains (stable, not redefinable) and against types + derived without crossing an open boundary. Reporting against inferred user-fn + signatures is a later, opt-in escalation. +- **Macros / generated code.** Check post-expansion IR but report at the user's + source location, and suppress reports inside expansions the user did not + write (or attribute them to the macro call site). + +## Relationship to other systems + +- **Dialyzer / success typing** (Erlang): the direct model — sound for + rejection, no false positives, accepts the ambiguous. +- **Typed Clojure / core.typed**: opt-in *sound* gradual typing that rejects + what it cannot prove correct; the opposite trade (false positives on dynamic + code), which is why we do not follow it. +- **clj-kondo**: a popular Clojure linter that flags some obvious type misuses + syntactically; this RFC subsumes the type-driven subset with inference-backed + precision and no false positives. + +## Implementation + +The checker is a thin pass over the same inference results: + +1. After (or during) inference, walk the IR. At each call to an operation in + the error-domain table, look at the inferred type of each checked argument. +2. If concrete and in the error domain, record a diagnostic with location, the + inferred type, and the expected domain. +3. Emit diagnostics per the strictness level. + +It adds no new inference; it consumes RFC 0005's types and a small curated +table. It can ship after RFC 0005 lands, starting in `warn` mode with the +smallest high-confidence table (arithmetic and seq/count/nth/first), and grow. + +## Design problems and open questions + +- **Curating the error domain.** The table must list only genuinely-throwing + cases. Getting it wrong (listing a lenient op) yields false positives, which + destroys trust. Mitigation: start tiny, test each entry against the runtime, + grow slowly. Open question: derive the table from the same machinery the + runtime uses, to avoid drift? +- **Unions.** *Resolved (jolt-pz5).* The lattice has a bounded scalar union + `{:union #{T...}}` (cap 4); differing if-branches form a union instead of + collapsing to `:any`, and a use is reported only when *every* member is in the + error domain. Unions are opaque to structural specialization, so codegen is + unchanged. +- **User-function signatures.** *Resolved (jolt-zo1), opt-in.* Behind + `JOLT_TYPE_CHECK_USER`: the checker re-checks a registered non-redefinable + user fn's body with one parameter bound to its concrete argument type; a + diagnostic the all-`:any` body did not have means that argument is provably + wrong. Monotonic, so still no false positives; closed-world, hence opt-in. +- **Negative/never types.** *Resolved (jolt-wwy).* Calling a provably + non-callable value (`:num`/`:str` — keywords/maps/vectors/sets are IFn) is + reported at the default level; wrong-arity to a registered single-fixed-arity + user fn is reported under the `JOLT_TYPE_CHECK_USER` opt-in. A union callee is + flagged only when every member is non-callable. +- **Position vs intent.** *Resolved (jolt-fqy).* The reader records each list + form's absolute offset (identity-keyed, so positions survive macroexpansion + exactly when the user's sub-form is spliced through); the analyzer stamps it + onto `:invoke` nodes, the checker carries it into each diagnostic, and the + back end renders `file:line:col`. Inlining/scalar-replace preserve it via + `assoc`. +- **Interaction with the optimization gate.** *Resolved (jolt audit).* The + checker is one inference walk folded into `infer`. In direct-link builds it + piggybacks on the specialization inference that already runs (~free, default + on); in plain builds it runs as a standalone pass only when `JOLT_TYPE_CHECK` + is set. "Run inference for checking" and "specialize from inference" are the + same walk now, gated by a `checking?` flag. diff --git a/docs/spec/02-reader.md b/docs/spec/02-reader.md index 67e4500..7d9962b 100644 --- a/docs/spec/02-reader.md +++ b/docs/spec/02-reader.md @@ -83,6 +83,16 @@ checks → UNVERIFIED (rows to add). - S12a. `^:kw form` ≡ `^{:kw true} form`; `^Sym form` ≡ `^{:tag Sym} form`; `^"str"` ≡ `^{:tag "str"} form`. Multiple `^` stack, rightmost innermost, merged left-over-right. +- S12b. Type hints are semantically transparent: a hint MUST NOT change a + program's result. Hints parse in every position they do in Clojure (params, + `let` bindings, `def` names, return position, arbitrary forms) and are + otherwise inert. As a non-normative optimization, jolt recognizes two hints + on a local as an assertion that a constant-keyword lookup may skip its + runtime representation guard: `^:struct` (a plain struct/record map) and + `^Name` where `Name` is a `defrecord`/`deftype`. The assertion is the + programmer's (an inaccurate hint yields a wrong lookup, like a wrong Clojure + `^String`); `JOLT_CHECK_HINTS=1` turns a violated hint into an error at no + cost to unchecked builds. See RFC 0004. - S13a. `#'ns/sym` MUST denote the same var as `(var ns/sym)`: `(= (var clojure.core/str) #'clojure.core/str)` is true. diff --git a/jolt-core/jolt/analyzer.clj b/jolt-core/jolt/analyzer.clj index 8840292..f56ee38 100644 --- a/jolt-core/jolt/analyzer.clj +++ b/jolt-core/jolt/analyzer.clj @@ -22,7 +22,8 @@ form-literal? form-elements form-vec-items form-map-pairs form-set-items form-special? compile-ns form-macro? form-expand-1 resolve-global - form-sym-meta host-intern! form-syntax-quote-lower]])) + form-sym-meta host-intern! form-syntax-quote-lower + record-type? form-position]])) (declare analyze) @@ -39,11 +40,27 @@ (swap! gensym-counter inc) (str "_r$" prefix n))) -(defn- empty-env [] {:locals #{}}) +(defn- empty-env [] {:locals #{} :hints {}}) (defn- local? [env nm] (contains? (:locals env) nm)) (defn- add-locals [env names] (update env :locals #(reduce conj % names))) (defn- with-recur [env name] (assoc env :recur name)) +;; Type hints (jolt-94n). The reader keeps ^hint metadata on the binding symbol. +;; Two hints resolve to the :struct fast path (a constant-keyword lookup skips +;; the :jolt/type guard and emits a bare get): ^:struct (a plain struct/record +;; map) and ^TypeName where TypeName is a defrecord/deftype (its instances are +;; tagged :jolt/deftype, not :jolt/type, so a raw get is correct). Every other +;; hint (^String, ^long, ...) parses and is ignored, as before. +(defn- hint-of [ctx sym] + (let [m (form-sym-meta sym)] + (cond + (nil? m) nil + (get m :struct) :struct + :else (let [t (get m :tag)] + (when (and t (record-type? ctx t)) :struct))))) +(defn- add-hint [env nm h] + (if h (assoc env :hints (assoc (:hints env) nm h)) env)) + (defn- analyze-seq [ctx forms env] (let [v (mapv #(analyze ctx % env) forms) n (count v)] @@ -59,23 +76,28 @@ (when-not (form-sym? bsym) (uncompilable "destructuring binding")) (let [nm (form-sym-name bsym) init (analyze ctx (nth bvec (inc i)) env)] - (recur (+ i 2) (add-locals env [nm]) (conj pairs [nm init])))) + (recur (+ i 2) (add-hint (add-locals env [nm]) nm (hint-of ctx bsym)) + (conj pairs [nm init])))) [pairs env]))) -(defn- parse-params [pvec] - (loop [i 0 fixed [] rest-name nil] +(defn- parse-params [ctx pvec] + ;; :hints is a vector of [name hint] pairs (vector, not a map, so the caller + ;; folds it with a plain reduce — no reduce-over-map in the kernel subset). + (loop [i 0 fixed [] rest-name nil hints []] (if (< i (count pvec)) (let [p (nth pvec i)] (when-not (form-sym? p) (uncompilable "destructuring fn param")) (if (= "&" (form-sym-name p)) (let [r (nth pvec (inc i))] (when-not (form-sym? r) (uncompilable "destructuring fn rest")) - (recur (+ i 2) fixed (form-sym-name r))) - (recur (inc i) (conj fixed (form-sym-name p)) rest-name))) - {:fixed fixed :rest rest-name}))) + (recur (+ i 2) fixed (form-sym-name r) hints)) + (let [nm (form-sym-name p) h (hint-of ctx p)] + (recur (inc i) (conj fixed nm) rest-name + (if h (conj hints [nm h]) hints))))) + {:fixed fixed :rest rest-name :hints hints}))) (defn- analyze-arity [ctx pvec body env fn-name] - (let [pp (parse-params (vec (form-vec-items pvec))) + (let [pp (parse-params ctx (vec (form-vec-items pvec))) fixed (:fixed pp) rst (:rest pp) ;; Always a recur target, variadic included: the back end gives the rest @@ -88,7 +110,8 @@ ;; keeps recur targets unique per compilation unit. rname (gen-name (str (compile-ns ctx) "/" (or fn-name "fn") "--")) names (cond-> (vec fixed) rst (conj rst) fn-name (conj fn-name)) - env* (-> (add-locals env names) (with-recur rname)) + env0 (-> (add-locals env names) (with-recur rname)) + env* (reduce (fn [e pr] (add-hint e (nth pr 0) (nth pr 1))) env0 (:hints pp)) arity {:params fixed :recur-name rname :body (analyze-seq ctx body env*)}] ;; :rest only when variadic — an absent :rest reads back nil, same as before, @@ -190,7 +213,8 @@ (defn- analyze-symbol [ctx form env] (let [nm (form-sym-name form) ns (form-sym-ns form)] (cond - (and (nil? ns) (local? env nm)) (local nm) + (and (nil? ns) (local? env nm)) + (let [h (get (:hints env) nm)] (if h (assoc (local nm) :hint h) (local nm))) ns (let [r (resolve-global ctx form)] (if (= :var (:kind r)) (var-ref (:ns r) (:name r)) @@ -226,8 +250,13 @@ (and (form-sym? head) (not shadowed) (form-macro? ctx head)) (analyze ctx (form-expand-1 ctx form) env) :else - (invoke (analyze ctx head env) - (mapv #(analyze ctx % env) (rest items)))))))) + ;; stamp the list form's source offset onto the :invoke (jolt-fqy) + ;; so the success checker can report file:line:col. nil when the + ;; reader did not record it (synthetic/macro-built forms). + (let [n (invoke (analyze ctx head env) + (mapv #(analyze ctx % env) (rest items))) + p (form-position form)] + (if p (assoc n :pos p) n))))))) (defn analyze ([ctx form] (analyze ctx form (empty-env))) diff --git a/jolt-core/jolt/passes.clj b/jolt-core/jolt/passes.clj index 1173088..fc6199b 100644 --- a/jolt-core/jolt/passes.clj +++ b/jolt-core/jolt/passes.clj @@ -178,7 +178,15 @@ (let [op (get node :op)] (cond (= op :local) (let [r (get env (get node :name))] - (if r r node)) + ;; carry the param's ^:struct hint onto a let-bound fresh + ;; local, so lookups inside the inlined body keep the bare + ;; (no-guard) path (jolt-dad). The param hint asserts the + ;; arg is a struct; inlining doesn't change that contract. + (if r + (if (and (= :local (get r :op)) (get node :hint) (not (get r :hint))) + (assoc r :hint (get node :hint)) + r) + node)) (= op :if) (assoc node :test (subst (get node :test) env) :then (subst (get node :then) env) @@ -698,18 +706,679 @@ :finally (when (get node :finally) (scalar-replace (get node :finally)))) :else node))) +;; --------------------------------------------------------------------------- +;; Collection-type inference (jolt-99x), Phase 0: intra-procedural. A forward, +;; soft-typing-style pass (simplified HM: monovariant, never-fails, lattice top +;; = :any) that types expressions from literals/arithmetic and flows the type +;; through let bindings and if-joins. Where a keyword-lookup subject is PROVEN a +;; plain struct map it sets :hint :struct (the same channel a manual hint uses, +;; so the back end drops the guard); where the type is :any it leaves the +;; dynamic guard in place. Sound by construction: a concrete type is assigned +;; only when proven, so a wrong bare get is impossible. +;; +;; Recursive STRUCTURAL types (RFC 0005). A type mirrors the data tree: +;; compound: {:struct {field -> T}} (raw-get-safe map, field types) +;; {:vec T} (vector of T) +;; {:set T} (set of T) +;; scalar: :num :str :kw :truthy (all provably non-nil/non-false) +;; :phm (persistent hash map; NOT raw-get-safe) +;; :any (top), nil (bottom, identity for join). +;; Compound types are small jolt maps, so they compare by value on both the +;; Clojure and the Janet (orchestrator) side. struct/vec/set use distinct keys so +;; a type is recognised by which key it carries. +;; (get t :KEY) is nil for a keyword type and the child for a compound, so a +;; compound is detected by some? — no map?/contains? needed. +(defn- velem [t] (get t :vec)) +(defn- selem [t] (get t :set)) +(defn- sfields [t] (get t :struct)) +(defn- vec-type? [t] (some? (velem t))) +(defn- set-type? [t] (some? (selem t))) +(defn- struct-type? [t] (some? (sfields t))) +(defn- mk-vec [t] {:vec (if t t :any)}) +(defn- mk-set [t] {:set (if t t :any)}) +(defn- mk-struct [fs] {:struct fs}) + +;; Bounded union types (RFC 0006 / jolt-pz5). A union {:union #{T...}} records +;; that a value is provably one of a small, fixed set of SCALAR types — what +;; differing if-branches used to collapse to :any. It exists so the success +;; checker can reject a use where EVERY member is in the op's error domain +;; ((inc (if c "a" :k))) while still accepting one where any member is valid +;; ((inc (if c 1 "x"))). Scalars only, capped cardinality: the member space is +;; the five scalar tags, so the lattice stays finite and the inter-procedural +;; fixpoint terminates. A union is opaque to every STRUCTURAL predicate +;; (struct-type?/vec-type?/set-type? key on :struct/:vec/:set, which a union +;; lacks), so specialization treats it exactly like :any — codegen is +;; unchanged; only the checker reads inside it. +(def ^:private union-cap 4) +(defn- scalar-t? [t] (or (= t :num) (= t :str) (= t :kw) (= t :truthy) (= t :phm))) +(defn- union-type? [t] (some? (get t :union))) +(defn- umembers [t] (get t :union)) +(defn- union-of + "Normalize a seq of member types into a lattice value: flatten nested unions, + keep only scalars (any non-scalar member collapses the whole thing to :any, + the conservative top), then return the lone member if one, {:union #{...}} + for 2..cap distinct scalars, or :any past the cap." + [ts] + (let [flat (reduce (fn [acc t] + (if (union-type? t) + (reduce conj acc (umembers t)) + (conj acc t))) + #{} ts)] + (cond + (not (every? scalar-t? flat)) :any + (= 0 (count flat)) :any + (= 1 (count flat)) (first flat) + (> (count flat) union-cap) :any + :else {:union flat}))) + +(declare join-t) +(defn- merge-fields + "Per-field join of two field maps (a key in only one side joins with :any)." + [fa fb] + (let [m1 (reduce (fn [m k] (assoc m k (join-t (get fa k :any) (get fb k :any)))) {} (keys fa))] + (reduce (fn [m k] (if (get m k) m (assoc m k (join-t (get fa k :any) (get fb k :any))))) m1 (keys fb)))) +(defn- join-t [a b] + (cond + (= a b) a + (nil? a) b + (nil? b) a + (and (struct-type? a) (struct-type? b)) (mk-struct (merge-fields (sfields a) (sfields b))) + (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 + ;; (or scalar unions); anything compound on either side stays :any (jolt-pz5) + :else (let [ma (cond (union-type? a) (umembers a) (scalar-t? a) #{a} :else nil) + mb (cond (union-type? b) (umembers b) (scalar-t? b) #{b} :else nil)] + (if (and ma mb) (union-of (reduce conj ma mb)) :any)))) +(defn- join [a b] (join-t a b)) +;; depth cap (RFC 0005): truncate a type below depth d to :any, so recursive data +;; can't make an infinite type and the inter-procedural fixpoint stays finite. +(def ^:private type-depth 4) +(defn- cap [t d] + (cond + (<= d 0) (if (or (struct-type? t) (vec-type? t) (set-type? t)) :any t) + (struct-type? t) (mk-struct (reduce (fn [m k] (assoc m k (cap (get (sfields t) k) (dec d)))) + {} (keys (sfields t)))) + (vec-type? t) (mk-vec (cap (velem t) (dec d))) + (set-type? t) (mk-set (cap (selem t) (dec d))) + :else t)) +;; raw-get-safe (a Janet 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)) +;; tag a node (any expression, not just a :local) so the back end can specialize +;; a lookup whose SUBJECT is that node — this is what makes nested access work: +;; (:direction ray) is tagged struct, so (:r (:direction ray)) drops its guard. +(defn- mark-hint [node h] (assoc node :hint h)) +;; a value provably neither nil nor false — the back end only builds a struct +;; (vs a phm) when every value is non-nil/non-false, so a map literal is a struct +;; only when all its values have such a type. Collections are non-nil. +(defn- truthy-type? [t] + (or (= t :num) (= t :str) (= t :kw) (= t :truthy) (= t :phm) + (struct-type? t) (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). +(def ^:private num-ret-fns + #{"+" "-" "*" "/" "inc" "dec" "mod" "rem" "quot" "min" "max" "abs" + "bit-and" "bit-or" "bit-xor" "count"}) +(def ^:private vector-ret-fns #{"vec" "vector" "mapv" "filterv" "subvec"}) + +;; Inter-procedural state (jolt-767, Phase 1). The Janet orchestrator (backend +;; infer-unit!) drives a whole-unit fixpoint: before typing a fn body it installs +;; the current return-type estimates of all unit fns here, and after typing it +;; reads back the call sites this body made (callee + inferred arg types) to +;; propagate into callee param types. Both are plain module state, like `dirty`. +(def ^:private rtenv-box (atom {})) ;; "ns/name" -> inferred return type +(def ^:private calls-box (atom [])) ;; collected [ "ns/name" [arg-types...] ] +(def ^:private escapes-box (atom #{})) ;; var-keys used as a VALUE (not a call head) +(def ^:private diag-box (atom [])) ;; success-type-check diagnostics (RFC 0006) +;; jolt-d6u: a var reference's VALUE type — a fn var is :truthy (non-nil), a def +;; var carries its inferred init type (e.g. a color table -> {:vec :struct-map}). +;; The orchestrator populates this from sealed (opt-mode) cell roots + def inits. +(def ^:private vtype-box (atom {})) ;; "ns/name" -> value type + +;; User-function error domains (jolt-zo1), opt-in. As the checker walks defs it +;; registers each non-redefinable single-fixed-arity user fn's {:params :body} +;; here, keyed "ns/name". At a later call site (strict mode only) the body is +;; re-checked with ONE parameter bound to its concrete argument type — if that +;; alone produces a diagnostic the all-:any body did not, that argument is +;; provably wrong and the CALL is reported. Module state, like rtenv-box: a def +;; must precede its call (the same closed-world ordering RFC 0005 assumes). +(def ^:private user-sig-box (atom {})) ;; "ns/name" -> {:params [..] :body ir} +(def ^:private checking-box (atom #{})) ;; keys mid-recheck — cycle guard +(def ^:private strict-box (atom false)) ;; report against user-fn domains? +;; 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 +;; checks, instead of a separate check-walk that re-inferred every subtree +;; (quadratic in nesting). Off during the optimization fixpoint so it doesn't +;; emit intermediate diagnostics; on only inside check-form. +(def ^:private checking? (atom false)) + +;; fns that RETURN an element of their (first) collection arg, so a lookup on the +;; 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) + +(defn- var-key [fnode] (str (get fnode :ns) "/" (get fnode :name))) + +(defn- call-ret-type [fnode] + (let [op (get fnode :op)] + (cond + ;; a user fn whose return type the fixpoint has estimated + (= op :var) (let [r (get @rtenv-box (var-key fnode))] + (if r r (let [nm (and (= "clojure.core" (get fnode :ns)) (get fnode :name))] + (cond (nil? nm) :any + (contains? num-ret-fns nm) :num + (contains? vector-ret-fns nm) (mk-vec :any) + :else :any)))) + (= op :host) (let [nm (get fnode :name)] + (cond (contains? num-ret-fns nm) :num + (contains? vector-ret-fns nm) (mk-vec :any) + :else :any)) + :else :any))) + +(declare infer) + +;; HOFs that apply their fn arg to the ELEMENTS of a collection (jolt-d6u, +;; Phase 3). :epos is which param of the fn receives an element. reduce is +;; handled separately (its arity changes the coll position, and its closure +;; also takes an accumulator). +(def ^:private hof-table + {"map" {:epos 0} "mapv" {:epos 0} "filter" {:epos 0} "filterv" {:epos 0} + "keep" {:epos 0} "remove" {:epos 0} "run!" {:epos 0} "mapcat" {:epos 0}}) + +(defn- infer-fn-seeded + "Infer a fn-literal passed to a HOF, seeding the given params to element/accum + types (seeds: param-index -> type), other params :any, captured locals from + tenv. Returns [ret-type node'] — ret is the lub of arity tail types, used to + type the HOF result (e.g. reduce's accumulator, mapv's element)." + [node seeds tenv] + (let [res (mapv (fn [a] + (let [params (get a :params) + pe (reduce (fn [e i] + (assoc e (nth params i) + (let [s (get seeds i)] (if s s :any)))) + tenv (range (count params))) + pe (if (get a :rest) (assoc pe (get a :rest) :any) pe) + br (infer (get a :body) pe)] + [(nth br 0) (assoc a :body (nth br 1))])) + (get node :arities)) + rets (mapv (fn [r] (nth r 0)) res) + ret (if (empty? rets) :any (reduce join (first rets) (rest rets)))] + [ret (assoc node :arities (mapv (fn [r] (nth r 1)) res))])) + +(defn- infer + "Returns [type node'] — the inferred type of node and node with struct-safe + :local references annotated :hint :struct. tenv maps in-scope local names to + inferred types." + [node tenv] + (let [op (get node :op)] + (cond + (= op :const) + [(let [v (get node :val)] + (cond (number? v) :num + (string? v) :str + (keyword? v) :kw + (or (nil? v) (= false v)) :any ; nil/false are not struct-eligible + :else :truthy)) ; true, char, ... -> non-nil + node] + (= op :local) + (let [t (get tenv (get node :name))] + [(if t t :any) + (cond + (struct-safe? t) (assoc node :hint :struct) + (vec-type? t) (assoc node :hint :vector) + :else node)]) + (= op :map) + (let [pairs (get node :pairs) + res (mapv (fn [pr] + (let [kr (infer (nth pr 0) tenv) + vr (infer (nth pr 1) tenv)] + [(nth kr 1) (nth vr 1) (nth vr 0) (get (nth pr 0) :val)])) + pairs) + struct? (and (> (count res) 0) + (every? (fn [pr] (scalar-const? (nth pr 0))) pairs) + (every? (fn [r] (truthy-type? (nth r 2))) res)) + t (if struct? + (cap (mk-struct (reduce (fn [m r] (assoc m (nth r 3) (nth r 2))) {} res)) type-depth) + :any)] + [t (assoc node :pairs (mapv (fn [r] [(nth r 0) (nth r 1)]) res))]) + (= op :vector) + (let [irs (mapv (fn [x] (infer x tenv)) (get node :items)) + ets (mapv (fn [r] (nth r 0)) irs) + el (if (empty? ets) :any (reduce join (first ets) (rest ets)))] + [(cap (mk-vec el) type-depth) (assoc node :items (mapv (fn [r] (nth r 1)) irs))]) + (= op :set) + (let [irs (mapv (fn [x] (infer x tenv)) (get node :items)) + ets (mapv (fn [r] (nth r 0)) irs) + 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) + thn (infer (get node :then) tenv) + els (infer (get node :else) tenv)] + [(join (nth thn 0) (nth els 0)) + (assoc node :test (nth tr 1) :then (nth thn 1) :else (nth els 1))]) + (= op :do) + (let [stmts (mapv (fn [s] (nth (infer s tenv) 1)) (get node :statements)) + r (infer (get node :ret) tenv)] + [(nth r 0) (assoc node :statements stmts :ret (nth r 1))]) + (= op :throw) + [:any (assoc node :expr (nth (infer (get node :expr) tenv) 1))] + ;; a :var reached HERE is in value position (an arg, a let init, ...), not + ;; a call head — so the fn it names escapes and its params can't be inferred. + ;; Its VALUE type comes from vtype-box (a fn is :truthy, a def carries its + ;; inferred type); unknown -> :any. + (= op :var) (do (swap! escapes-box conj (var-key node)) + [(let [vt (get @vtype-box (var-key node))] (if vt vt :any)) node]) + (= op :invoke) + (let [fnode (get node :fn) + iscall-var (= :var (get fnode :op)) + cn (when (and iscall-var (= "clojure.core" (get fnode :ns))) (get fnode :name)) + args (get node :args) + n (count args)] + (cond + ;; (: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). + (and (= :const (get fnode :op)) (keyword? (get fnode :val)) (>= n 1) (<= n 2)) + (let [mr (infer (nth args 0) tenv) + mt (nth mr 0) + msub (if (struct-safe? mt) (mark-hint (nth mr 1) :struct) (nth mr 1)) + ft (field-type mt (get fnode :val)) + dr (when (= n 2) (infer (nth args 1) tenv))] + [(if dr (join ft (nth dr 0)) ft) + (assoc node :args (if dr [msub (nth dr 1)] [msub]))]) + ;; (get m :k [default]): same, when the key is a constant keyword. + (and (or (and (= :var (get fnode :op)) (= "clojure.core" (get fnode :ns)) (= "get" (get fnode :name))) + (and (= :host (get fnode :op)) (= "get" (get fnode :name)))) + (>= n 2) (= :const (get (nth args 1) :op)) (keyword? (get (nth args 1) :val))) + (let [mr (infer (nth args 0) tenv) + mt (nth mr 0) + msub (if (struct-safe? mt) (mark-hint (nth mr 1) :struct) (nth mr 1)) + kr (infer (nth args 1) tenv) + ft (field-type mt (get (nth args 1) :val)) + dr (when (= n 3) (infer (nth args 2) tenv))] + [(if dr (join ft (nth dr 0)) ft) + (assoc node :args (if dr [msub (nth kr 1) (nth dr 1)] [msub (nth kr 1)]))]) + ;; reduce over a typed vector with a fn-literal (jolt-d6u): seed the + ;; closure's accumulator (param 0) to the init type and its element + ;; (param 1) to the vector's element type, so its body — and any calls + ;; it makes — see those types. + (and (= cn "reduce") (>= n 2) (= :fn (get (nth args 0) :op))) + (let [three (>= n 3) + coll-r (infer (nth args (if three 2 1)) tenv) + init-r (when three (infer (nth args 1) tenv)) + et (let [ct (nth coll-r 0)] (if (vec-type? ct) (velem ct) :any)) + init-t (if init-r (nth init-r 0) :any) + fn-r (infer-fn-seeded (nth args 0) {0 init-t 1 et} tenv)] + [(join init-t (nth fn-r 0)) + (assoc node :args (if three + [(nth fn-r 1) (nth init-r 1) (nth coll-r 1)] + [(nth fn-r 1) (nth coll-r 1)]))]) + ;; map/mapv/filter/... over a typed vector with a fn-literal: seed the + ;; fn's element param; mapv/filterv produce a typed vector. + (and cn (get hof-table cn) (>= n 2) (= :fn (get (nth args 0) :op))) + (let [coll-r (infer (nth args 1) tenv) + et (let [ct (nth coll-r 0)] (if (vec-type? ct) (velem ct) :any)) + fn-r (infer-fn-seeded (nth args 0) {(get (get hof-table cn) :epos) et} tenv) + rt (cond (= cn "mapv") (mk-vec (nth fn-r 0)) + (= cn "filterv") (mk-vec et) + :else :any)] + [rt (assoc node :args [(nth fn-r 1) (nth coll-r 1)])]) + ;; conj/into: track the element type of a vector being grown. + (and (or (= cn "conj") (= cn "into")) (>= n 1)) + (let [ares (mapv (fn [a] (infer a tenv)) args) + base (nth (nth ares 0) 0) + rest-ts (mapv (fn [r] (nth r 0)) (rest ares)) + rt (cond + (and (= cn "conj") (vec-type? base)) + (mk-vec (reduce join (velem base) rest-ts)) + (and (= cn "into") (vec-type? base) (= 2 n) (vec-type? (nth rest-ts 0))) + (mk-vec (join (velem base) (velem (nth rest-ts 0)))) + :else (call-ret-type fnode))] + [rt (assoc node :args (mapv (fn [r] (nth r 1)) ares))]) + ;; everything else: type args, collect the call (var callee), use the + ;; declared/estimated return type. range produces a numeric vector. + :else + (let [fr (when (not iscall-var) (infer fnode tenv)) + fnode' (if iscall-var fnode (nth fr 1)) + ;; the callee's value type: a var's from vtype-box (a fn is + ;; :truthy, a def carries its inferred type), else the inferred + ;; type of the callee expression (jolt-wwy) + callee-t (if iscall-var (get @vtype-box (var-key fnode)) (nth fr 0)) + ares (mapv (fn [a] (infer a tenv)) args)] + (when iscall-var + (swap! calls-box conj [(var-key fnode) (mapv (fn [r] (nth r 0)) ares)])) + ;; success-type check at this call, reusing the arg types just + ;; computed (jolt audit): core error domains always, user-fn domains + ;; in strict mode. The arg subtrees are inferred exactly once. + (when @checking? + (let [ats (mapv (fn [r] (nth r 0)) ares) pos (get node :pos)] + (when cn (check-invoke cn args ats pos)) + ;; calling a provably non-function (jolt-wwy) + (when (not-callable? callee-t) + (swap! diag-box conj + {:op :call :type (type-name callee-t) :pos pos + :msg (str "cannot call " (type-name callee-t) " as a function")})) + (when (and @strict-box iscall-var) + (let [k (var-key fnode) usig (get @user-sig-box k)] + (when usig (check-user-call k usig ats pos)))))) + [(cond + (= cn "range") (mk-vec :num) + ;; element-returning fn over a typed vector -> the element type + (and cn (contains? elem-fns cn) (> n 0)) + (let [a0 (nth (nth ares 0) 0)] (if (vec-type? a0) (velem a0) :any)) + :else (call-ret-type fnode)) + (assoc node :fn fnode' :args (mapv (fn [r] (nth r 1)) ares))]))) + (= op :let) + (let [res (reduce (fn [acc b] + (let [te (nth acc 0) binds (nth acc 1) + ir (infer (nth b 1) te)] + [(assoc te (nth b 0) (nth ir 0)) (conj binds [(nth b 0) (nth ir 1)])])) + [tenv []] (get node :bindings)) + br (infer (get node :body) (nth res 0))] + [(nth br 0) (assoc node :bindings (nth res 1) :body (nth br 1))]) + (= op :loop) + ;; conservative + sound: loop bindings join across recur, which we don't + ;; track in Phase 0, so they stay :any. Still descend to annotate any + ;; known-type lookups inside the body. + [:any (assoc node + :bindings (mapv (fn [b] [(nth b 0) (nth (infer (nth b 1) tenv) 1)]) (get node :bindings)) + :body (nth (infer (get node :body) tenv) 1))] + (= op :recur) + [:any (assoc node :args (mapv (fn [a] (nth (infer a tenv) 1)) (get node :args)))] + (= op :fn) + ;; a closure inherits the enclosing tenv so CAPTURED locals keep their + ;; types (e.g. a reduce closure that calls (f captured-struct ...)); its own + ;; params/rest shadow to :any (unknown until Phase 1 types them via callers). + [:any (assoc node :arities + (mapv (fn [a] + (let [pe (reduce (fn [e p] (assoc e p :any)) tenv (get a :params)) + pe (if (get a :rest) (assoc pe (get a :rest) :any) pe)] + (assoc a :body (nth (infer (get a :body) pe) 1)))) + (get node :arities)))] + (= op :def) + (do (when @checking? (register-user-fn! node)) + [:any (assoc node :init (nth (infer (get node :init) tenv) 1))]) + (= op :try) + [:any (assoc node + :body (nth (infer (get node :body) tenv) 1) + :catch-body (when (get node :catch-body) (nth (infer (get node :catch-body) tenv) 1)) + :finally (when (get node :finally) (nth (infer (get node :finally) tenv) 1)))] + :else [:any node]))) + +(defn- infer-top [node] (nth (infer node {}) 1)) + +;; --------------------------------------------------------------------------- +;; Success-type checking (RFC 0006). Reuse the inference above as a loose type +;; checker: flag a core-fn call ONLY when an argument's inferred type is +;; concrete AND lies in that op's error domain (the op provably throws on it). +;; Everything ambiguous — :any, :truthy (true/char/...), :nil — is accepted, so +;; 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 (jolt-pz5) — 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 (jolt-wwy): 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. arg-types is the vector of inferred argument types; pos is + the call form's source offset (jolt-fqy), carried into each diagnostic." + [cn args arg-types pos] + (cond + (contains? num-ops cn) + (reduce (fn [_ i] + (let [t (nth arg-types i)] + (when (not-number? t) + (swap! diag-box 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! diag-box 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 (jolt-zo1), opt-in -------------------------- +(defn- all-any-env + "tenv binding every param name to :any (the all-ambiguous baseline)." + [params] + (reduce (fn [e p] (assoc e p :any)) {} params)) + +(defn- isolated-diag-count + "Count of diagnostics typing body under tenv produces, with the shared + diag-box saved and restored so this probe never leaks into the real report. + Runs the same checking inference as check-form (checking? is already on)." + [body tenv] + (let [saved @diag-box] + (reset! diag-box []) + (infer body tenv) + (let [n (count @diag-box)] + (reset! diag-box saved) + n))) + +(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] + (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! user-sig-box 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 + arg count always throws, jolt-wwy) or an argument whose concrete type the body + rejects. For the latter, re-check the body with ONLY that parameter bound to + its arg type (others :any); a diagnostic the all-:any body did not already + have means the argument alone is provably wrong. Monotonic — binding a + concrete type can only ADD error-domain hits — so no false positive. + Cycle-guarded so mutually recursive fns terminate." + [key sig arg-types pos] + (when (not (contains? @checking-box key)) + (let [prev @checking-box] + (reset! checking-box (conj prev key)) + (let [params (:params sig) + body (:body sig) + npar (count params) + nargs (count arg-types)] + (if (not= npar nargs) + ;; arity is provably wrong regardless of types — report and stop (the + ;; per-arg type re-check would bind params positionally, meaningless + ;; under a mismatch) + (swap! diag-box conj + {:op :user-call :type :arity :pos pos + :msg (str "wrong number of args (" nargs ") passed to `" + (:name sig) "` (expected " npar ")")}) + (let [base (isolated-diag-count body (all-any-env params))] + (reduce + (fn [_ i] + (let [at (nth arg-types i)] + (when (and (not= at :any) (not= at :truthy)) + (let [pe (assoc (all-any-env params) (nth params i) at)] + (when (> (isolated-diag-count body pe) base) + (swap! diag-box conj + {:op :user-call :argpos i :type (type-name at) :pos pos + :msg (str "argument " (inc i) " to `" (:name sig) + "` is " (type-name at) + ", which its body provably rejects")}))))) + nil) + nil (range npar))))) + (reset! checking-box prev)))) + +;; --- Inter-procedural driver API (jolt-767) consumed by the back end -------- +(defn set-rtenv! + "Install the current return-type estimates (a map \"ns/name\" -> type) used to + type call results during the fixpoint." + [m] (reset! rtenv-box m)) + +(defn set-vtypes! + "Install var VALUE types (a map \"ns/name\" -> type): fn vars are :truthy + (non-nil), def vars carry their inferred init type (jolt-d6u)." + [m] (reset! vtype-box m)) + +(defn join-types + "Public structural join (lub), used by the orchestrator's fixpoint so param/ + return types join field-wise/element-wise instead of collapsing to :any." + [a b] (join-t a b)) + +(defn reset-escapes! [] (reset! escapes-box #{})) +(defn collected-escapes [] (vec @escapes-box)) + +(defn check-form + "Success-type check a single analyzed form (RFC 0006). Returns a vector of + diagnostics [{:op :argpos :type :msg} ...] for provably-wrong calls; empty + when nothing is provably wrong. Runs independently of specialization so it is + usable in normal builds (the decoupled checking path). + + With strict? true, also reports calls to registered user functions whose + concrete argument types provably make the body throw (jolt-zo1, opt-in, + closed-world). user-sig-box accumulates registered defs across forms, so a + def must precede its call — the same ordering RFC 0005 already assumes." + ([node] (check-form node false)) + ([node strict?] + (reset! strict-box (if strict? true false)) + (reset! checking-box #{}) + (reset! diag-box []) + ;; the check IS the inference: one walk that types and emits diagnostics + ;; (jolt audit). checking? gates emission so the optimization fixpoint, which + ;; also calls infer, stays silent. + (reset! checking? true) + (infer node {}) + (reset! checking? false) + (reset! strict-box false) + (vec @diag-box))) + +(defn infer-body + "Type `body` under tenv (local-name -> type). Returns [ret-type node' calls], + where calls is the [[\"ns/name\" [arg-types...]] ...] this body invokes (for + propagating into callee param types). Also accumulates escapes (read with + collected-escapes after a full sweep)." + [body tenv] + (reset! calls-box []) + (let [r (infer body tenv)] + [(nth r 0) (nth r 1) @calls-box])) + +(defn reinfer-def + "Re-run inference on a stashed :def's fn arity bodies with param types seeded + (ptmap: param-name -> type), returning the def with annotated bodies. The back + end emits the result directly (no further passes), so the param-typed lookups + keep their specialization. Used by the inter-procedural recompile." + [def-node ptmap] + (let [fnode (get def-node :init)] + (if (= :fn (get fnode :op)) + (assoc def-node :init + (assoc fnode :arities + (mapv (fn [a] (assoc a :body (nth (infer (get a :body) ptmap) 1))) + (get fnode :arities)))) + def-node))) + +;; Piggyback checking (jolt audit). In direct-link mode infer-top already runs +;; one inference pass for specialization; turning checking? on during it makes +;; the success checker nearly free there (no extra traversal — just the +;; per-call error-domain predicates). The back end sets the mode before +;; run-passes and reads take-diags! after. It checks the POST-optimization IR, +;; which matches what the optimized program actually evaluates (scalar-replace +;; only drops provably-pure code, an accepted opt-mode divergence). +(def ^:private check-mode-box (atom {:on false :strict false})) +(defn set-check-mode! + "Enable/disable checking during the next run-passes inference (direct-link)." + [on strict?] (reset! check-mode-box {:on (if on true false) :strict (if strict? true false)})) +(defn take-diags! + "Diagnostics accumulated by the last checking run-passes; clears the buffer." + [] (let [d (vec @diag-box)] (reset! diag-box []) d)) + (defn run-passes "All passes, in order. The back end applies this to every analyzed form. When inlining is enabled for the unit (user code under direct-linking, jolt-87f), run inline + flatten + scalar-replace + const-fold to a capped fixpoint — inlining exposes map literals to lookups, scalar-replace collapses them, which - may expose more. Otherwise (core + bootstrap) just const-fold, as before." + may expose more — then a collection-type inference pass (jolt-99x) that + auto-drops the lookup guard where the type is proven. Otherwise (core + + bootstrap) just const-fold, as before." [node ctx] (if (inline-enabled? ctx) - (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 8)) - (recur (inc i) n2) - n2))) + (let [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 8)) + (recur (inc i) n2) + n2)))] + ;; specialization inference, optionally also emitting success diagnostics + (if (get @check-mode-box :on) + (do (reset! diag-box []) + (reset! checking-box #{}) + (reset! strict-box (get @check-mode-box :strict)) + (reset! checking? true) + (let [r (infer-top opt)] + (reset! checking? false) + (reset! strict-box false) + r)) + (infer-top opt))) (const-fold node))) diff --git a/src/jolt/api.janet b/src/jolt/api.janet index b4c9e8f..e935f3a 100644 --- a/src/jolt/api.janet +++ b/src/jolt/api.janet @@ -189,6 +189,10 @@ # — that would be circular — so it reads this hook). Without it, required # namespaces ran interpreted-only. (put (ctx :env) :toplevel-eval eval-toplevel) + # Inter-procedural type-inference hook (jolt-767): the evaluator calls this + # after a unit finishes loading (optimization mode only). Installed here to + # avoid an evaluator->backend circular import. + (put (ctx :env) :infer-unit! backend/infer-unit!) # Stateful primitives as ctx-capturing clojure.core fns (protocol-dispatch, # register-method, …) — so the protocol macros compile to plain invokes. Must # precede the overlay (its defprotocol/extend-type expansions call these). @@ -296,7 +300,7 @@ # Opts land in the key via their printed form; an opt that prints unstably # (e.g. a closure in :namespaces) just degrades to a cache miss, never to a # wrong hit. Runtime knobs that shape the ctx outside opts ride along too. - (def key (string/format "%q|%q|%q|%q|%q|%q|%q|%q|%q" + (def key (string/format "%q|%q|%q|%q|%q|%q|%q|%q|%q|%q" (string janet/version "-" janet/build) opts (os/getenv "JOLT_PATH") @@ -305,7 +309,8 @@ (os/getenv "JOLT_FEATURES") (os/getenv "JOLT_INTERPRET_MACROS") (os/getenv "JOLT_DIRECT_LINK") - (os/getenv "JOLT_NO_IR_PASSES"))) + (os/getenv "JOLT_NO_IR_PASSES") + (os/getenv "JOLT_CHECK_HINTS"))) (string dir "/jolt-ctx-" (band h 0x7FFFFFFF) "-" len "-" (band (hash key) 0x7FFFFFFF) ".jimg")) (defn init-cached @@ -364,5 +369,12 @@ Returns the result of the last form evaluated." [ctx s &opt file] (default file "") + # record form positions so the checker can report file:line:col (jolt-fqy). + # The checker is on when JOLT_TYPE_CHECK selects it, OR by default in + # direct-link builds (where it piggybacks on inference for free). + (when (or (checker-enabled?) (get (ctx :env) :inline?)) + (track-positions! true) + (put (ctx :env) :tc-source s) + (put (ctx :env) :tc-file file)) (eval-forms-positioned ctx (parse-all-positioned s file) file)) diff --git a/src/jolt/backend.janet b/src/jolt/backend.janet index ab2bd62..91de6d8 100644 --- a/src/jolt/backend.janet +++ b/src/jolt/backend.janet @@ -13,6 +13,7 @@ (use ./evaluator) (import ./reader :as r) (import ./phm :as phm) +(import ./pv :as pv) # The IR is portable data; reading its representation is a host-layer concern. # Most nodes are Janet structs (raw-readable), but a node carrying a nil-valued @@ -72,13 +73,21 @@ (when (get (ctx :env) :inline?) (def init (norm-node (node :init))) (def meta (node :meta)) - (when (and (= :fn (init :op)) - (not (and meta (or (get meta :redef) (get meta :dynamic))))) - (def arities (vview (init :arities))) - (when (= 1 (length arities)) - (def ar (norm-node (in arities 0))) - (unless (ar :rest) - (put cell :inline-ir {:params (ar :params) :body (ar :body)})))))) + (def redefable (and meta (or (get meta :redef) (get meta :dynamic)))) + (cond + redefable nil + (= :fn (init :op)) + (let [arities (vview (init :arities))] + (when (= 1 (length arities)) + (def ar (norm-node (in arities 0))) + (unless (ar :rest) + (put cell :inline-ir {:params (ar :params) :body (ar :body)}) + # jolt-767: stash the whole (post-pass) :def IR so the inter-procedural + # pass can re-infer its body with discovered param types and re-emit it. + (put cell :infer-ir node)))) + # a non-fn def: stash so the pass can infer its VALUE type (jolt-d6u), e.g. + # a color table used via rand-nth — its element type flows to lookups. + true (put cell :infer-ir node)))) # Var late-binding: reads go through `(var-get cell)` with the cell embedded as a # constant, so compiled code sees redefinition (Janet early-binds plain symbols) @@ -304,10 +313,69 @@ (var- fp-counter 0) (defn- jsym [] (symbol "_fp$" (++ fp-counter))) +# Is fnode a reference to clojure.core/get (or a host `get`)? Used to give +# (get m :kw [d]) the same inlined keyword-lookup treatment as (:kw m [d]). +(defn- get-head? [fnode] + (case (fnode :op) + :var (and (= "clojure.core" (fnode :ns)) (= "get" (fnode :name))) + :host (= "get" (fnode :name)) + false)) + +# Is fnode a reference to clojure.core/ (or host )? +(defn- core-head? [fnode name] + (case (fnode :op) + :var (and (= "clojure.core" (fnode :ns)) (= name (fnode :name))) + :host (= name (fnode :name)) + false)) + +# Is this IR node a :local the inference proved to be a vector ({:vec ...})? +(defn- vec-hinted? [n] (and (= :local (n :op)) (= :vector (n :hint)))) + +# Shared emit for a constant-keyword map lookup — both (:kw m [d]) and +# (get m :kw [d]). subj-node is the subject's IR node (carries the type hint), +# m-expr its emitted form, k the keyword, d-expr the emitted default or nil. +# - unhinted: GUARDED — (if (get m :jolt/type) (core-get …) (bare get)). The +# guard (one opcode) routes tagged reps (phm/sorted/transient/lazy-seq) to +# core-get; a plain struct/record (no :jolt/type) takes the bare get, which +# matches core-get for keyword keys. +# - ^:struct / ^Record hinted subject: skip the guard, bare get (~20 vs ~36ns). +# - hinted + JOLT_CHECK_HINTS: keep the guard but THROW on the tagged arm, so a +# lying hint surfaces a clear error (dev aid; off by default, no perf cost). +(defn- emit-kw-lookup [subj-node m-expr k d-expr] + # the subject is a struct (raw-get-safe) when hinted so — by an explicit + # ^:struct/^Record hint on a local, OR by inference tagging ANY subject + # expression it proved to be a struct (jolt-d6u/RFC 0005), which is what lets + # nested access like (:r (:direction ray)) drop its guard. + (def hinted (and subj-node (= :struct (subj-node :hint)))) + (def checked (and hinted (os/getenv "JOLT_CHECK_HINTS"))) + (def m (if (symbol? m-expr) m-expr (jsym))) + (def wrap (fn [body] (if (symbol? m-expr) body ['let [m m-expr] body]))) + (def err (when checked + ['error (string "type hint violated on `" (subj-node :name) "`: (" + k " " (subj-node :name) ") — value carries :jolt/type " + "(a phm/sorted/transient/lazy-seq), not the plain " + "struct/record the ^:struct/^Record hint asserts")])) + (if (nil? d-expr) + (let [fast ['get m k]] + (wrap (cond + checked ['if ['get m :jolt/type] err fast] + hinted fast + ['if ['get m :jolt/type] (tuple core-get m k) fast]))) + (let [d (if (symbol? d-expr) d-expr (jsym)) + v (jsym) + fast ['let [v ['get m k]] ['if ['nil? v] d v]] + body (cond + checked ['if ['get m :jolt/type] err fast] + hinted fast + ['if ['get m :jolt/type] (tuple core-get m k d) fast]) + body (if (symbol? d-expr) body ['let [d d-expr] body])] + (wrap body)))) + (defn- emit-invoke [ctx node] (def fnode (norm-node (node :fn))) (def args (map |(emit ctx $) (vview (node :args)))) (def nop (native-op fnode (length args))) + (def argnodes (vview (node :args))) (cond nop (case nop '++ ['+ (in args 0) 1] @@ -326,27 +394,30 @@ # records with direct field keys, nil, janet arrays, scalars) gets janet # `get` semantics, which match core-get for keyword keys. Structs never # store nil values (nil values force the phm rep), so present-but-nil - # can't be confused with missing on the fast arm. + # can't be confused with missing on the fast arm. A ^:struct/^Record hint on + # the subject skips the guard entirely (jolt-94n; see emit-kw-lookup). (and (= :const (fnode :op)) (keyword? (fnode :val)) (>= 2 (length args) 1)) - (let [k (fnode :val) - m-expr (in args 0) - # when the subject is already a janet symbol (a local), read it - # directly — the guard + lookup both reference it, and locals are - # immutable reads, so no rebinding let is needed (saves a binding - # per lookup in exactly the hottest shape, (:k local)) - m (if (symbol? m-expr) m-expr (jsym)) - wrap (fn [body] (if (symbol? m-expr) body ['let [m m-expr] body]))] - (if (= 1 (length args)) - (wrap ['if ['get m :jolt/type] (tuple core-get m k) ['get m k]]) - (let [d-expr (in args 1) - d (if (symbol? d-expr) d-expr (jsym)) - v (jsym) - body ['if ['get m :jolt/type] - (tuple core-get m k d) - ['let [v ['get m k]] ['if ['nil? v] d v]]] - body (if (symbol? d-expr) body ['let [d d-expr] body])] - (wrap body)))) + (emit-kw-lookup (norm-node (in argnodes 0)) (in args 0) (fnode :val) + (when (= 2 (length args)) (in args 1))) + # (get m :kw) / (get m :kw default) — same inlined keyword lookup as (:kw m), + # so an explicit get with a constant keyword gets the guard fast path and the + # ^:struct/^Record hint (jolt-94n). Only when the key is a constant keyword; + # a variable/number/string key falls through to core-get below. + (and (get-head? fnode) (>= (length args) 2) (<= (length args) 3) + (let [a1 (norm-node (in argnodes 1))] (and (= :const (a1 :op)) (keyword? (a1 :val))))) + (emit-kw-lookup (norm-node (in argnodes 0)) (in args 0) + ((norm-node (in argnodes 1)) :val) + (when (= 3 (length args)) (in args 2))) + # (count v) on an inferred vector -> pv-count, skipping core-count's dispatch + # chain (jolt-d6u, Phase 2). Sound: a {:vec ...}-typed value is a pvec. + (and (core-head? fnode "count") (= 1 (length args)) (vec-hinted? (norm-node (in argnodes 0)))) + (tuple pv/pv-count (in args 0)) + # (nth v i default) on an inferred vector -> pv-nth. Only the 3-ARG form: the + # 2-arg nth ERRORS on out-of-bounds where pv-nth returns nil, so specializing + # it would change semantics; the 3-arg default matches pv-nth exactly. + (and (core-head? fnode "nth") (= 3 (length args)) (vec-hinted? (norm-node (in argnodes 0)))) + (tuple pv/pv-nth (in args 0) (in args 1) (in args 2)) (direct-call? ctx fnode) (tuple (emit ctx fnode) ;args) # Local callee (closure param, let-bound fn, defn self-name): inline the # function check so the overwhelmingly-common function case is a direct @@ -542,6 +613,47 @@ [ctx] (build-compiler! ctx)) +(defn- report-diags! + "Render and emit success-type diagnostics (RFC 0006) at the given strictness: + `warn` prints to stderr, `error` throws (failing this form's compilation). + file:line:col when the diagnostic carries an offset and the source is on the + env (jolt-fqy); else the ns." + [ctx diags strictness ns] + (def src (get (ctx :env) :tc-source)) + (def file (or (get (ctx :env) :tc-file) (and ns (string ns)))) + (each d diags + (def off (get d :pos)) + (def loc + (if (and off src) + (let [lc (r/line-col src off)] + (string (or file "?") ":" (in lc 0) ":" (in lc 1))) + (string "in " (if ns (string ns) "?")))) + (def msg (string "type error " loc ": " (get d :msg))) + (if (= strictness "error") + (error msg) + (eprint " " msg)))) + +(defn type-check! + "Decoupled success-type check (RFC 0006): run jolt.passes/check-form as its OWN + inference pass over `ir` and report. Used in NON-direct-link builds, where the + optimization inference doesn't run — so checking costs a separate pass. (In + direct-link builds checking piggybacks on run-passes' inference instead, near + free; see analyze-form.) Protected so a checker bug never breaks compilation. + + JOLT_TYPE_CHECK_USER (an orthogonal opt-in knob, jolt-zo1) additionally + reports calls to user functions whose concrete argument types provably make + the body throw — sound only under the closed-world assumption, hence opt-in." + [ctx ir strictness ns] + (def cf (ns-find (ctx-find-ns ctx "jolt.passes") "check-form")) + (when cf + (def uenv (os/getenv "JOLT_TYPE_CHECK_USER")) + (def strict? (and uenv (not= uenv "0") (not= uenv "off"))) + (def r (protect ((var-get cf) ir strict?))) + (when (r 0) + (def diags (if (pv/pvec? (r 1)) (pv/pv->array (r 1)) (r 1))) + (when (and diags (> (length diags) 0)) + (report-diags! ctx diags strictness ns))))) + (defn analyze-form "Run the portable Clojure analyzer (jolt.analyzer/analyze) on a reader form, returning host-neutral IR." @@ -574,14 +686,44 @@ # Resolved lazily; absent during the pre-passes bootstrap window. (def pv (unless (= "1" (os/getenv "JOLT_NO_IR_PASSES")) (ns-find (ctx-find-ns ctx "jolt.passes") "run-passes"))) - (if pv - (let [pr (protect ((var-get pv) (r 1) ctx))] - # the pass runs interpreted; a throw inside it unwinds past the - # interpreter's ns restores — put the compile ns back either way, or - # the REST of this compilation resolves in jolt.passes - (ctx-set-current-ns ctx saved-ns) - (if (pr 0) (pr 1) (r 1))) - (r 1))) + # Success-type checking level (RFC 0006). JOLT_TYPE_CHECK wins when set; + # otherwise it defaults to `warn` in direct-link builds — where the + # optimization inference already runs, so checking piggybacks on it for nearly + # free — and stays OFF for plain REPL/dev builds (no inference -> no free ride; + # opt in with JOLT_TYPE_CHECK there). (jolt audit) + (def tc (os/getenv "JOLT_TYPE_CHECK")) + (def tc-off (or (= tc "off") (= tc "0"))) + (def direct-link? (if (get (ctx :env) :inline?) true false)) + (def level (cond tc-off nil tc tc direct-link? "warn" true nil)) + (def uenv (os/getenv "JOLT_TYPE_CHECK_USER")) + (def strict? (and uenv (not= uenv "0") (not= uenv "off") true)) + # piggyback: check DURING run-passes' inference (direct-link, the cheap path) + (def piggyback? (and level direct-link? pv true)) + (def scm (and piggyback? (ns-find (ctx-find-ns ctx "jolt.passes") "set-check-mode!"))) + (when scm ((var-get scm) true strict?)) + (def result + (if pv + (let [pr (protect ((var-get pv) (r 1) ctx))] + # the pass runs interpreted; a throw inside it unwinds past the + # interpreter's ns restores — put the compile ns back either way, or + # the REST of this compilation resolves in jolt.passes + (ctx-set-current-ns ctx saved-ns) + (if (pr 0) (pr 1) (r 1))) + (r 1))) + (when scm ((var-get scm) false false)) + (cond + # direct-link: collect the diagnostics infer-top emitted and report them + piggyback? + (let [td (ns-find (ctx-find-ns ctx "jolt.passes") "take-diags!")] + (when td + (def raw ((var-get td))) + (def diags (if (pv/pvec? raw) (pv/pv->array raw) raw)) + (when (and diags (> (length diags) 0)) + (report-diags! ctx diags level saved-ns)))) + # plain build with checking explicitly requested: a separate inference pass + (and level (not direct-link?)) + (type-check! ctx (r 1) level saved-ns)) + result) # The analyzer's deliberate punt signal — (uncompilable why) throws the string # "jolt/uncompilable: ". Anything else escaping the compile step is an @@ -706,6 +848,157 @@ (++ n)))) n) +# Inter-procedural collection-type inference + recompile (jolt-767, Phase 1), +# closed-world / optimization mode. After a unit loads, every single-fixed-arity +# fn stashed a post-pass :def IR (:infer-ir). We: +# 1. run a whole-unit fixpoint: a fn's param types = lub of its in-unit +# call-site arg types (computed by jolt.passes/infer-body); a fn whose var +# escapes as a VALUE keeps :any params (its callers aren't all visible). +# 2. re-infer + re-emit each fn body with its param types seeded, so +# param-dependent lookups specialize (drop the :jolt/type guard). +# Recompiled bodies are semantically identical to the guarded ones, so this is +# correct regardless of recompile order; order only affects how far a direct- +# linked call propagates the faster callee. +(defn- itype-join [a b] + (cond + (nil? a) b + (nil? b) a + (= a b) a + # compound vector types {:vec ELEM} join element-wise (jolt-d6u) + (and (struct? a) (struct? b) (in a :vec) (in b :vec)) + (struct :vec (itype-join (in a :vec) (in b :vec))) + :any)) + +(defn infer-unit! + [ctx ns-name] + (def pns (ctx-find-ns ctx "jolt.passes")) + (def f-set-rtenv (and pns (ns-find pns "set-rtenv!"))) + (def f-set-vtypes (and pns (ns-find pns "set-vtypes!"))) + (def f-join (and pns (ns-find pns "join-types"))) + (def f-infer-body (and pns (ns-find pns "infer-body"))) + (def f-reinfer (and pns (ns-find pns "reinfer-def"))) + (def f-reset-esc (and pns (ns-find pns "reset-escapes!"))) + (def f-get-esc (and pns (ns-find pns "collected-escapes"))) + (def ns (ctx-find-ns ctx ns-name)) + (def report @{}) + (when (and ns f-set-rtenv f-set-vtypes f-join f-infer-body f-reinfer f-reset-esc f-get-esc) + # gather single-fixed-arity fns AND non-fn defs that stashed a :def IR + (def fns @[]) + (def defs @[]) + (def by-key @{}) + (def vtypes @{}) # var VALUE types: fns -> :truthy (non-nil), defs -> inferred + (each nm (keys (ns :mappings)) + (def v (get (ns :mappings) nm)) + (when (and (table? v) (get v :infer-ir)) + (def d (norm-node (get v :infer-ir))) + (def init (norm-node (d :init))) + (def key (string ns-name "/" nm)) + (if (= :fn (init :op)) + (let [ars (vview (init :arities))] + (when (= 1 (length ars)) + (def ar (norm-node (in ars 0))) + (unless (ar :rest) + (def pv (vview (ar :params))) + (def rec @{:key key :cell v :def d :params (ar :params) :body (ar :body) + :np (length pv) :pt (array/new-filled (length pv)) :ret nil}) + (array/push fns rec) + (put by-key key rec) + # a fn value is non-nil -> :truthy (sealed root in opt mode) + (put vtypes key :truthy)))) + # non-fn def: its value type is inferred from its init (jolt-d6u) + (array/push defs @{:key key :init (d :init) :vt nil})))) + (when (or (> (length fns) 0) (> (length defs) 0)) + ((var-get f-reset-esc)) + # --- param/return/value-type fixpoint (chaotic iteration to LEAST fixpoint) --- + # Param types are RECOMPUTED FRESH each iteration, not accumulated: :any is + # the lattice top, so a join with an early-iteration :any (a caller whose own + # params weren't typed yet) would poison the result permanently. Recomputing + # from the current state lets a param refine as its callers' types improve. + (var prev-rt @{}) + (var changed true) (var iter 0) + (while (and changed (< iter 16)) + ((var-get f-set-rtenv) prev-rt) + ((var-get f-set-vtypes) vtypes) + # type every fn body once under current param types; stash ret + calls + (each f fns + (def tenv @{}) + (def pv (vview (f :params))) + (for i 0 (f :np) (when (in (f :pt) i) (put tenv (in pv i) (in (f :pt) i)))) + (def res (vview ((var-get f-infer-body) (f :body) tenv))) + (put f :tret (in res 0)) + (put f :tcalls (in res 2))) + # infer each def's VALUE type from its init + (each dv defs + (put dv :tvt (in (vview ((var-get f-infer-body) (dv :init) @{})) 0))) + # recompute param types FRESH (start at bottom = nil) from this round's calls + (def newpt @{}) + (each f fns (put newpt (f :key) (array/new-filled (f :np)))) + (each f fns + (each c (vview (f :tcalls)) + (def cv (vview c)) + (def npa (get newpt (in cv 0))) + (when npa + (def callee (get by-key (in cv 0))) + (def ats (vview (in cv 1))) + (def lim (min (length ats) (callee :np))) + (for i 0 lim (put npa i ((var-get f-join) (in npa i) (in ats i))))))) + # commit + detect change + (set changed false) + (def nrt @{}) + (each f fns + (def np (get newpt (f :key))) + (for i 0 (f :np) (when (not= (in np i) (in (f :pt) i)) (set changed true))) + (when (not= (f :tret) (f :ret)) (set changed true)) + (put f :pt np) + (put f :ret (f :tret)) + (when (f :tret) (put nrt (f :key) (f :tret)))) + (each dv defs + (when (not= (dv :tvt) (dv :vt)) (set changed true)) + (put dv :vt (dv :tvt)) + (when (dv :tvt) (put vtypes (dv :key) (dv :tvt)))) + (set prev-rt nrt) + (++ iter)) + # --- escaped fns: var used as a value -> params untrustworthy -> skip --- + (def esc @{}) + (each k (vview ((var-get f-get-esc))) (put esc k true)) + # install the FINAL return + value types so reinfer-def sees them + (def final-rt @{}) + (each f fns (when (f :ret) (put final-rt (f :key) (f :ret)))) + ((var-get f-set-rtenv) final-rt) + ((var-get f-set-vtypes) vtypes) + # --- re-emit the WHOLE unit, callees first (jolt-d6u) ------------------- + # Re-inference alone only rebinds a fn's own var, but the hot path runs + # through callee bodies INLINED / direct-linked into callers at first + # compile. Re-emitting in callee-first (reverse-topological) order makes + # each caller re-embed its now-recompiled callees, and re-infers its body + # (typing locals via return inference) — so the specialization propagates, + # and a call site compiled AFTER this pass (the -e entry) links the whole + # recompiled chain. Every fn is re-emitted, not just those with concrete + # params, so the embedding refreshes even where a fn gained no param type. + (def order @[]) + (def seen @{}) + (defn visit [k] + (unless (get seen k) + (put seen k true) + (def f (get by-key k)) + (when f + (each c (vview (f :tcalls)) (visit (in (vview c) 0))) + (array/push order f)))) + (each f fns (visit (f :key))) + (each f order + (put report (f :key) (f :pt)) + (def ptmap @{}) + # escaped fn: its param types are untrustworthy (callers not all visible), + # so re-emit it WITHOUT seeding params (still re-embeds recompiled callees). + (unless (get esc (f :key)) + (def pv (vview (f :params))) + (for i 0 (f :np) + (def t (in (f :pt) i)) + (when (and t (not= t :any)) (put ptmap (in pv i) t)))) + (def def2 ((var-get f-reinfer) (f :def) ptmap)) + (protect (eval (emit-ir ctx def2) (ctx-janet-env ctx)))))) + report) + (defn ensure-macros-compiled! "Called once the overlay is fully loaded (api/load-core-overlay!): ensure the analyzer is built, then run the staged macro-recompile pass so the early diff --git a/src/jolt/evaluator.janet b/src/jolt/evaluator.janet index 096501e..ff68c25 100644 --- a/src/jolt/evaluator.janet +++ b/src/jolt/evaluator.janet @@ -375,6 +375,18 @@ [ctx src &opt file] (default file "") (def toplevel (get (ctx :env) :toplevel-eval)) + # a require runs nested inside an outer file's eval; save/restore the outer + # checker source so its later forms still convert offsets correctly (jolt-fqy) + (def checking (or (checker-enabled?) (get (ctx :env) :inline?))) + (def saved-src (and checking (get (ctx :env) :tc-source))) + (def saved-file (and checking (get (ctx :env) :tc-file))) + (when checking + (track-positions! true) + (put (ctx :env) :tc-source src) + (put (ctx :env) :tc-file file)) + (defer (when checking + (put (ctx :env) :tc-source saved-src) + (put (ctx :env) :tc-file saved-file)) (each [f line] (parse-all-positioned src file) (try (if toplevel (toplevel ctx f) (eval-form ctx @{} f)) @@ -388,7 +400,7 @@ (when (nil? (get env :error-loading)) (put env :error-loading @[])) (def chain (get env :error-loading)) (when (not= (last chain) file) (array/push chain file)) - (propagate err fib))))) + (propagate err fib)))))) (defn- maybe-require-ns "If namespace ns-name isn't populated yet, load its source — from a file on the @@ -421,6 +433,14 @@ (if path (load-ns-source ctx (slurp path) path) (load-ns-source ctx embedded (string ns-name " (stdlib)"))) + # Inter-procedural collection-type inference (jolt-767): once the whole + # unit is loaded, run the closed-world fixpoint + recompile so param- + # dependent lookups specialize. Only in optimization mode; best-effort + # (a failure here must not break loading). Hook installed by the api to + # avoid an evaluator->backend circular import. + (when (get (ctx :env) :inline?) + (when-let [iu (get (ctx :env) :infer-unit!)] + (protect (iu ctx ns-name)))) # Record load order for tooling (uberscript): a dependency finishes # loading before its requirer, so this is topological. Skip the # baked-in stdlib — it's part of the runtime, not something to bundle. diff --git a/src/jolt/host_iface.janet b/src/jolt/host_iface.janet index 55a05d3..2bcf20e 100644 --- a/src/jolt/host_iface.janet +++ b/src/jolt/host_iface.janet @@ -194,6 +194,10 @@ # with it would recurse forever. (defn h-ref-get [tab key] (get tab key)) +# Absolute source offset of a list FORM (jolt-fqy), or nil. The analyzer stamps +# it onto :invoke nodes so the success checker can report file:line:col. +(defn h-form-position [form] (rdr/form-pos form)) + # --------------------------------------------------------------------------- # Inline registry (jolt-87f, Route 1 AOT escape analysis). The inline pass # (jolt.passes) is portable Clojure and can't read Janet var cells, so it asks @@ -219,6 +223,18 @@ (not (let [m (cell :meta)] (and m (get m :redef))))) (cell :inline-ir)))) +# Is `name` (a bare type-name string, e.g. "Vec3") a defrecord/deftype? Both +# expand to define a ->Name positional constructor var (30-macros.clj), so its +# presence is the marker. Lets the analyzer resolve a ^Record type hint to the +# struct fast path: record instances are tables tagged :jolt/deftype (NOT +# :jolt/type), so a raw keyword get is correct for them (jolt-94n). +(defn h-record-type? [ctx name] + (def ctor (string "->" name)) + (def cns (ctx-find-ns ctx (h-current-ns ctx))) + (if (or (and cns (ns-find cns ctor)) + (ns-find (ctx-find-ns ctx "clojure.core") ctor)) + true false)) + (def- exports {"form-sym?" h-sym? "form-sym-name" h-sym-name "form-sym-ns" h-sym-ns "ref-put!" h-ref-put! @@ -233,7 +249,8 @@ "form-expand-1" h-expand-1 "resolve-global" h-resolve-global "form-syntax-quote-lower" h-syntax-quote-lower "host-intern!" h-intern! - "inline-enabled?" h-inline-enabled? "inline-ir" h-inline-ir}) + "inline-enabled?" h-inline-enabled? "inline-ir" h-inline-ir + "record-type?" h-record-type? "form-position" h-form-position}) (defn install! [ctx] (def ns (ctx-find-ns ctx "jolt.host")) diff --git a/src/jolt/loader.janet b/src/jolt/loader.janet index 70a76b6..7c82476 100644 --- a/src/jolt/loader.janet +++ b/src/jolt/loader.janet @@ -112,6 +112,10 @@ (load-ns ctx filepath) → namespace symbol string" [ctx filepath] (def source (slurp filepath)) + (when (or (checker-enabled?) (get (ctx :env) :inline?)) + (track-positions! true) + (put (ctx :env) :tc-source source) + (put (ctx :env) :tc-file filepath)) (def pairs (parse-all-positioned source filepath)) (var ns-name nil) (each [form _] pairs diff --git a/src/jolt/main.janet b/src/jolt/main.janet index af7527c..602bdff 100644 --- a/src/jolt/main.janet +++ b/src/jolt/main.janet @@ -259,18 +259,24 @@ [msg] (def msg (string msg)) (cond - # janet polymorphic arithmetic: could not find method :+ for 1 or :r+ for "a" + # janet polymorphic arithmetic. Binary: "could not find method :+ for 1 or + # :r+ for "a"". Unary (inc/dec/-): "could not find method :+ for "x"" — no + # "or :r" clause, so orpos is nil; handle both without crashing the reporter. (string/has-prefix? "could not find method :" msg) (let [rest* (string/slice msg (length "could not find method :")) sp (string/find " " rest*) op (string/slice rest* 0 sp) tail (string/slice rest* (+ sp (length " for "))) - orpos (string/find " or :r" tail) - a (string/slice tail 0 orpos) - forpos (string/find " for " tail (+ orpos 1)) - b (string/slice tail (+ forpos 5))] - (string "Cannot " (get op-words op op) " " a " and " b - " — " op " expects numbers")) + orpos (string/find " or :r" tail)] + (if (nil? orpos) + # unary form: one operand + (string "Cannot " (get op-words op op) " " tail + " — " op " expects numbers") + (let [a (string/slice tail 0 orpos) + forpos (string/find " for " tail (+ orpos 1)) + b (string/slice tail (+ forpos 5))] + (string "Cannot " (get op-words op op) " " a " and " b + " — " op " expects numbers")))) # janet fixed-arity: called with 2 arguments, expected 1 (and (string/has-prefix? " called with " msg)) (let [nm-end (string/find ">" msg) diff --git a/src/jolt/reader.janet b/src/jolt/reader.janet index 7b01ec9..a6220f7 100644 --- a/src/jolt/reader.janet +++ b/src/jolt/reader.janet @@ -14,6 +14,41 @@ # Forward declaration for mutual recursion (var read-form nil) +# Source-position tracking for the success checker (jolt-fqy). When enabled, the +# reader records each LIST form's absolute start offset (lists are the forms that +# become :invoke nodes — what the checker reports on). Off by default: a flag +# check per list is the only cost when the checker isn't running. Keyed by form +# IDENTITY (lists are fresh arrays, never interned), so a position survives +# macroexpansion exactly when the user's own sub-form is spliced through, and is +# absent for macro-synthesized structure — which is what we want (fall back to +# the call site). Not cleared between parses: nested parses (a require mid-load) +# would otherwise drop an outer file's positions; the table is bounded by forms +# compiled this process and only populated when the checker is on. +(def form-pos-table @{}) +(var track-positions false) +(var pos-base 0) # absolute offset of the slice read-form currently sees + +(defn track-positions! + "Enable/disable list-form position recording (jolt-fqy)." + [on] (set track-positions on)) + +(defn set-pos-base! + "Tell the reader the absolute offset of the slice it is about to read, so + recorded list positions are absolute (parse-all-positioned reads a shrinking + remainder)." + [b] (set pos-base b)) + +(defn form-pos + "Absolute start offset recorded for a list form, or nil." + [form] (get form-pos-table form)) + +(defn checker-enabled? + "True when JOLT_TYPE_CHECK selects a non-off level — the loaders use this to + decide whether to record form positions for the checker (jolt-fqy)." + [] + (def tc (os/getenv "JOLT_TYPE_CHECK")) + (if (and tc (not= tc "off") (not= tc "0")) true false)) + (def whitespace-chars " \t\n\r,") (defn whitespace? [c] @@ -624,7 +659,9 @@ # list (= c 40) - (read-list s pos) + (let [r (read-list s pos)] + (when track-positions (put form-pos-table (in r 0) (+ pos-base pos))) + r) # unmatched closing delimiters (= c 41) @@ -726,6 +763,9 @@ (or (= c (chr " ")) (= c (chr "\t")) (= c (chr "\r")) (= c (chr ","))) (++ i) (= c (chr ";")) (while (and (< i n) (not= (in s i) (chr "\n"))) (++ i)) (set scanning false))) + # list-form positions recorded during this parse-next are relative to s; + # tell the reader the slice base so they land absolute (jolt-fqy) + (when track-positions (set-pos-base! (- (length source) (length s)))) (def [form rest*] (try (parse-next s) ([err fib] diff --git a/test/integration/cli-test.janet b/test/integration/cli-test.janet index eef40aa..184d1b9 100644 --- a/test/integration/cli-test.janet +++ b/test/integration/cli-test.janet @@ -45,6 +45,12 @@ (check "arith error message rewritten" (run-err "-e" `(+ 1 "a")`) (has `Cannot add 1 and "a"`)) +# unary arithmetic (inc/dec) on a non-number: the host error has no "or :r" +# clause, which used to crash the rewriter itself — handle it (jolt audit) +(check "unary arith error does not crash the rewriter" + (run-err "-e" `(inc "x")`) + (fn [s] (and (string/find "expects numbers" s) + (nil? (string/find "could not find method" s))))) (check "arity error names the fn" (run-err "-e" "(defn afn [x] x) (afn 1 2)") (has "Wrong number of args (2) passed to: user/afn")) @@ -112,6 +118,51 @@ r) (has "could not find method")) +# --- success checker default-on in direct-link, off in plain builds ---------- +# A provably-wrong defn (never called, so no runtime error): the checker is the +# only thing that can flag it. Plain build = silent (no dev regression); +# direct-link build = warns by default (free piggyback on inference). +(def tcw (string (or (os/getenv "TMPDIR") "/tmp") "/jolt-tcwarn-" (os/time) ".clj")) +(spit tcw "(ns tcw)\n\n(defn unused [s]\n (inc \"definitely-not-a-number\"))\n") +(check "plain build does not run the checker (no regression)" + (run-err tcw) + (fn [s] (nil? (string/find "type error" s)))) +(check "direct-link build warns by default (free checking)" + (do (os/setenv "JOLT_DIRECT_LINK" "1") + (def r (run-err tcw)) + (os/setenv "JOLT_DIRECT_LINK" nil) + r) + (fn [s] (and (string/find "type error" s) + (string/find "requires a number" s)))) +(check "JOLT_TYPE_CHECK=off disables it even in direct-link" + (do (os/setenv "JOLT_DIRECT_LINK" "1") + (os/setenv "JOLT_TYPE_CHECK" "off") + (def r (run-err tcw)) + (os/setenv "JOLT_DIRECT_LINK" nil) + (os/setenv "JOLT_TYPE_CHECK" nil) + r) + (fn [s] (nil? (string/find "type error" s)))) +# negative/never types (jolt-wwy): calling a non-function is reported by default +# in direct-link; wrong-arity to a user fn under the JOLT_TYPE_CHECK_USER opt-in +(def tcn (string (or (os/getenv "TMPDIR") "/tmp") "/jolt-tcneg-" (os/time) ".clj")) +(spit tcn "(ns tcn)\n\n(defn nope []\n (let [n 5] (n 1)))\n") +(check "direct-link reports calling a number as a function" + (do (os/setenv "JOLT_DIRECT_LINK" "1") + (def r (run-err tcn)) + (os/setenv "JOLT_DIRECT_LINK" nil) + r) + (has "cannot call a number as a function")) +(def tca (string (or (os/getenv "TMPDIR") "/tmp") "/jolt-tcarity-" (os/time) ".clj")) +(spit tca "(ns tca)\n\n(defn f [x y] (+ x y))\n(defn g [] (f 1))\n") +(check "JOLT_TYPE_CHECK_USER reports wrong arity to a user fn" + (do (os/setenv "JOLT_DIRECT_LINK" "1") + (os/setenv "JOLT_TYPE_CHECK_USER" "1") + (def r (run-err tca)) + (os/setenv "JOLT_DIRECT_LINK" nil) + (os/setenv "JOLT_TYPE_CHECK_USER" nil) + r) + (has "wrong number of args (1) passed to `f` (expected 2)")) + (if (> fails 0) (error (string "cli-test: " fails " failing check(s)")) (print "\nAll CLI tests passed!")) diff --git a/test/integration/struct-hint-test.janet b/test/integration/struct-hint-test.janet new file mode 100644 index 0000000..f91ffa0 --- /dev/null +++ b/test/integration/struct-hint-test.janet @@ -0,0 +1,79 @@ +# Type hints driving keyword-lookup specialization (jolt-94n). A local hinted +# ^:struct (a plain struct/record map) or ^Record (a defrecord/deftype) lets a +# constant-keyword lookup skip the :jolt/type guard and emit a bare get +# (~20ns vs ~36ns), the way Clojure type hints let the compiler specialize. +# Covers both (:k m) and (get m :k), hint propagation through inlining, the +# ^Record path, the JOLT_CHECK_HINTS dev aid, and that accurate hints preserve +# results. An inaccurate hint is a programmer error (like a wrong ^String): the +# raw get returns the wrong value, surfaced only under JOLT_CHECK_HINTS. +(import ../../src/jolt/api :as api) +(import ../../src/jolt/backend :as backend) +(import ../../src/jolt/reader :as reader) + +(print "Type hints (jolt-94n)...") + +(os/setenv "JOLT_DIRECT_LINK" "1") # inline on, so hint-through-inline is exercised +(def ctx (api/init {:compile? true})) +(api/eval-string ctx "(ns sh)") +(api/eval-string ctx "(defrecord Vec3r [r g b])") +(each s ["(defn v3 [r g b] {:r r :g g :b b})" + "(defn dot [^:struct l ^:struct r] (+ (+ (* (:r l) (:r r)) (* (:g l) (:g r))) (* (:b l) (:b r))))" + "(defn sub [^:struct l ^:struct r] {:r (- (:r l) (:r r)) :g (- (:g l) (:g r)) :b (- (:b l) (:b r))})" + "(defn lensq [^:struct v] (dot v v))"] + (api/eval-string ctx s)) + +(defn guards [src] + (def code (string/format "%p" (backend/emit-ir ctx (backend/analyze-form ctx (reader/parse-string src))))) + (length (string/find-all ":jolt/type" code))) + +# --- guard removal ---------------------------------------------------------- +(assert (= 1 (guards "(fn [v] (:r v))")) "unhinted (:r v) keeps the guard") +(assert (= 0 (guards "(fn [^:struct v] (:r v))")) "^:struct (:r v) drops the guard") +(assert (= 0 (guards "(fn [^Vec3r v] (:r v))")) "^Record (:r v) drops the guard") +(assert (= 1 (guards "(fn [^String v] (:r v))")) "^String (not a record) still guards") +(assert (= 0 (guards "(fn [^:struct v] (+ (+ (:r v) (:g v)) (:b v)))")) "all three hinted lookups bare") +(assert (= 0 (guards "(fn [^:struct v] (lensq v))")) "hint survives through an inlined call") +# hints work on let bindings too, not just params (init is a plain local here, +# so the only candidate guard is the hinted (:r v)) +(assert (= 0 (guards "(fn [^:struct s] (let [^:struct v s] (:r v)))")) "^:struct on a let binding drops the guard") +(assert (= 1 (guards "(fn [s] (let [v s] (:r v)))")) "unhinted let binding keeps the guard") +# (get m :k) gets the same treatment as (:k m) +(assert (= 1 (guards "(fn [m] (get m :k))")) "unhinted (get m :k) is guarded-inline") +(assert (= 0 (guards "(fn [^:struct m] (get m :k))")) "^:struct (get m :k) drops the guard") +(assert (= 0 (guards "(fn [^Vec3r m] (get m :k 0))")) "^Record (get m :k d) drops the guard") +# a variable (non-constant) key isn't a keyword literal, so the inline doesn't +# fire — it falls through to core-get, which still indexes correctly. +(assert (= 2 (api/eval-string ctx "((fn [m kk] (get m kk)) {:a 2} :a)")) "variable-key get via core-get") +(assert (= 10 (api/eval-string ctx "((fn [m i] (get m i)) [10 20] 0)")) "variable-key get indexes a vector") + +# --- correctness (accurate hints preserve results) -------------------------- +(assert (= 32 (api/eval-string ctx "(dot (v3 1 2 3) (v3 4 5 6))")) "hinted dot value") +(assert (= 14 (api/eval-string ctx "(lensq (v3 1 2 3))")) "hinted lensq (inline-flow) value") +(assert (= 7 (api/eval-string ctx "(:r (sub (v3 9 8 7) (v3 2 0 0)))")) "hinted sub field") +(api/eval-string ctx "(defn hit [^:struct ray ^:struct c] (lensq (sub (:origin ray) c)))") +(assert (= 48 (api/eval-string ctx "(hit {:origin (v3 5 5 5) :direction (v3 0 0 0)} (v3 1 1 1))")) + "hinted value through nested inline reads correctly") +(assert (= nil (api/eval-string ctx "((fn [^:struct m] (:absent m)) (v3 1 2 3))")) "hinted struct miss -> nil") +(assert (= 9 (api/eval-string ctx "((fn [^:struct m] (get m :absent 9)) (v3 1 2 3))")) "hinted get default") +# field access on a real record instance through a ^Record hint +(api/eval-string ctx "(defn vr-x [^Vec3r v] (:r v))") +(assert (= 5 (api/eval-string ctx "(vr-x (->Vec3r 5 6 7))")) "record field via ^Record hint") +# (get m :k) on assorted reps still matches core-get semantics (unhinted path) +(assert (= 2 (api/eval-string ctx "(get {:a 2} :a)")) "get struct present") +(assert (= nil (api/eval-string ctx "(get {:a 2} :z)")) "get struct miss") +(assert (= 1 (api/eval-string ctx "(get (hash-map :a 1 :x nil) :a)")) "get phm present") +(assert (= nil (api/eval-string ctx "(get (hash-map :a 1 :x nil) :x)")) "get phm nil value") +(assert (= 7 (api/eval-string ctx "(get (sorted-map :a 7) :a)")) "get sorted present") + +# --- checked mode: a lying hint throws (separate ctx with the flag on) ------- +(os/setenv "JOLT_CHECK_HINTS" "1") +(def cctx (api/init {:compile? true})) +(api/eval-string cctx "(ns ck)") +(api/eval-string cctx "(defn rd [^:struct m] (:a m))") +(assert (= 1 (api/eval-string cctx "(rd {:a 1 :b 2})")) "checked mode: accurate hint still works") +(let [r (protect (api/eval-string cctx "(rd (hash-map :a 1 :x nil))"))] + (assert (not (r 0)) "checked mode: lying ^:struct hint throws") + (assert (string/find "type hint violated" (string (r 1))) "checked-mode error is meaningful")) +(os/setenv "JOLT_CHECK_HINTS" nil) + +(print "Type hints passed!") diff --git a/test/integration/type-check-test.janet b/test/integration/type-check-test.janet new file mode 100644 index 0000000..5580a24 --- /dev/null +++ b/test/integration/type-check-test.janet @@ -0,0 +1,137 @@ +# Success-type checking (RFC 0006, jolt-y3b). The structural inference of +# RFC 0005, reused as a loose checker: flag a core-fn call ONLY when an argument +# is PROVABLY the wrong type (concrete and in the op's throwing error domain). +# Ambiguous cases (:any, unions, :truthy) are accepted — no false positives. +(import ../../src/jolt/api :as api) +(import ../../src/jolt/backend :as backend) +(import ../../src/jolt/types :as types) +(import ../../src/jolt/reader :as reader) + +(print "Success-type checking (jolt-y3b)...") + +(os/setenv "JOLT_DIRECT_LINK" "1") +(reader/track-positions! true) # record form positions (jolt-fqy) +(def ctx (api/init {:compile? true})) +(def pns (types/ctx-find-ns ctx "jolt.passes")) +(def check (types/var-get (types/ns-find pns "check-form"))) + +# diagnostics (a Janet tuple of diag structs) for a source form +(defn diags [src] + (api/normalize-pvecs (check (backend/analyze-form ctx (reader/parse-string src))))) +(defn nd [src] (length (diags src))) +# strict mode (jolt-zo1): also report provably-wrong calls to user fns +(defn nds [src] + (length (api/normalize-pvecs + (check (backend/analyze-form ctx (reader/parse-string src)) true)))) + +# --- provably wrong: REPORTED ------------------------------------------------ +(assert (= 1 (nd "(inc \"x\")")) "inc on a string") +(assert (= 1 (nd "(+ 1 \"x\")")) "+ with a string arg") +(assert (= 1 (nd "(count :foo)")) "count of a keyword") +(assert (= 1 (nd "(count 5)")) "count of a number") +(assert (= 1 (nd "(first 42)")) "first of a number") +(assert (= 1 (nd "(nth :k 0)")) "nth of a keyword") +(assert (= 1 (nd "(let [n \"x\"] (inc n))")) "inc on a let-bound string") +(assert (= 1 (nd "(inc (count :k))")) "inner count of keyword reported (inc of :num is fine)") + +# --- ambiguous / lenient: ACCEPTED (no false positive) ----------------------- +(assert (= 0 (nd "(:k 5)")) "keyword lookup on a number returns nil, not an error") +(assert (= 0 (nd "(get 5 :k)")) "get on a number returns nil, not an error") +(assert (= 0 (nd "(fn [x] (inc x))")) "inc on an unknown (:any) param accepted") +(assert (= 0 (nd "(fn [c] (inc (if c 1 \"x\")))")) "inc on a {:num | :str} branch -> :any, accepted") +(assert (= 0 (nd "(count \"ab\")")) "count of a string is fine") +(assert (= 0 (nd "(count [1 2 3])")) "count of a vector is fine") +(assert (= 0 (nd "(first [1 2 3])")) "first of a vector is fine") +(assert (= 0 (nd "(inc (count [1 2 3]))")) "count of vector + inc of :num both fine") +(assert (= 0 (nd "(inc (first [1 2 3]))")) "first of vector -> :num, inc fine") + +# --- calling a non-function (jolt-wwy): :num and :str are not callable -------- +(assert (= 1 (nd "(5 1)")) "calling a number is reported") +(assert (= 1 (nd "(\"hi\" 0)")) "calling a string is reported") +(assert (= 1 (nd "((+ 1 2) :k)")) "calling an arithmetic result (a :num) is reported") +(assert (= 1 (nd "(let [n 5] (n 1))")) "calling a let-bound number is reported") +(assert (= 1 (nd "(let [s \"x\"] (s 0))")) "calling a let-bound string is reported") +# (a var holding a number, e.g. (def nn 5) (nn 1), is caught in direct-link +# mode via vtype-box; the standalone checker has no var value types) +# callable values: keyword/map/vector/set as IFn — NOT reported +(assert (= 0 (nd "(:k {:k 1})")) "keyword call is fine") +(assert (= 0 (nd "({:a 1} :a)")) "map call is fine") +(assert (= 0 (nd "([10 20] 1)")) "vector call is fine") +(assert (= 0 (nd "(#{1 2} 1)")) "set call is fine") +(assert (= 0 (nd "(fn [c] ((if c 1 :k) 0))")) "union {:num | :kw} callee accepted (:kw is callable)") +(assert (= 0 (nd "(fn [f] (f 1))")) "calling an unknown (:any) param accepted") +(assert (= 1 (nd "(fn [c] ((if c 1 \"x\") 0))")) "union {:num | :str} callee — both non-callable — reported") + +# --- bounded unions (jolt-pz5): report only when EVERY member is in the error +# domain; accept when any member is valid. Differing branches used to collapse +# to :any (accepted); now they form {:union #{...}} and are checked per-member. +(assert (= 1 (nd "(fn [c] (inc (if c \"a\" :k)))")) + "inc of {:str | :kw} — every member non-number — reported") +(assert (= 0 (nd "(fn [c] (inc (if c 1 \"x\")))")) + "inc of {:num | :str} — :num is fine — still accepted") +(assert (= 1 (nd "(fn [c] (count (if c :k 5)))")) + "count of {:kw | :num} — both non-seqable — reported") +(assert (= 0 (nd "(fn [c] (count (if c :k \"ab\")))")) + "count of {:kw | :str} — :str is seqable — accepted") +(assert (= 1 (nd "(fn [c] (inc (if c \"a\" (if c :k :j))))")) + "inc of nested all-non-number union reported") +(assert (= 0 (nd "(fn [c] (inc (if c \"a\" (if c :k 1))))")) + "inc of union with a buried :num member accepted") +# a union is opaque to structural specialization — it keeps the dynamic guard, +# exactly like :any, so a keyword lookup over it is never mis-specialized. +(assert (= 0 (nd "(fn [c] (:r (if c {:r 1} {:g 2})))")) + "keyword lookup over a struct union is accepted (no false positive)") + +# --- user-function error domains (jolt-zo1), opt-in strict mode -------------- +# A call passing a provably-wrong type to a user fn whose body requires +# otherwise is reported ONLY in strict mode; the default level never fires on +# user fns (closed-world soundness boundary). +(assert (= 0 (nd "(do (defn ufa [x] (+ x 1)) (ufa \"s\"))")) + "user-fn wrong call NOT reported at the default level") +(assert (= 1 (nds "(do (defn ufa [x] (+ x 1)) (ufa \"s\"))")) + "strict: arithmetic fn called with a string is reported") +(assert (= 0 (nds "(do (defn ufb [x] (+ x 1)) (ufb 5))")) + "strict: same fn called with a number is accepted") +(assert (= 0 (nds "(do (defn ufc [x] (:k x)) (ufc \"s\"))")) + "strict: a body that uses the param leniently is not reported") +# cross-form: a def registered by an earlier check is visible to a later call +(nds "(defn ufd [x] (count x))") +(assert (= 1 (nds "(ufd 42)")) + "strict: cross-form call to a seq-only fn with a number is reported") +(assert (= 0 (nds "(do (defn ^:redef ufe [x] (+ x 1)) (ufe \"s\"))")) + "strict: a ^:redef fn is not a stable requirement, not reported") +(assert (= 1 (nds "(do (defn ufrec [x] (ufrec (+ x 1))) (ufrec \"s\"))")) + "strict: self-recursion terminates (cycle guard) and the (+ x 1) on a string is reported once") +# wrong arity to a user fn (jolt-wwy), strict mode: the registered fixed arity +# makes a mismatched call provably throw, regardless of argument types +(assert (= 1 (nds "(do (defn uar [x y] (+ x y)) (uar 1))")) + "strict: 2-arg fn called with 1 arg is reported") +(assert (= 1 (nds "(do (defn uar2 [x] x) (uar2 1 2 3))")) + "strict: 1-arg fn called with 3 args is reported") +(assert (= 0 (nds "(do (defn uar3 [x y] (+ x y)) (uar3 1 2))")) + "strict: correct arity accepted") +(assert (= 0 (nd "(do (defn uar4 [x y] (+ x y)) (uar4 1))")) + "default level does NOT report user-fn arity (closed-world, opt-in)") +(assert (= 0 (nds "(do (defn ^:redef uar5 [x y] (+ x y)) (uar5 1))")) + "strict: ^:redef fn arity not checked (could be redefined)") + +# --- the diagnostic carries op + type + a message ---------------------------- +(def one (in (diags "(inc \"x\")") 0)) +(assert (= "inc" (get one :op)) "diagnostic names the op") +(assert (string/find "number" (get one :msg)) "message says a number is required") +# --- the diagnostic carries the offending form's source offset (jolt-fqy) ----- +(assert (= 0 (get one :pos)) "diagnostic carries :pos (offset 0 for a single form)") +(def nested (in (diags "(do 1 2 (inc :k))") 0)) +(assert (= 8 (get nested :pos)) + "the inner (inc :k) form is positioned at its own offset, not the do's") + +# --- end-to-end: strictness drives compilation (decoupled from :inline?) ----- +# error mode aborts a provably-wrong form's compilation; a correct form compiles. +(os/setenv "JOLT_TYPE_CHECK" "error") +(assert (not (first (protect (api/eval-string ctx "(count :nope)")))) + "error mode aborts a provably-wrong form") +(assert (first (protect (api/eval-string ctx "(count [1 2 3])"))) + "error mode accepts a correct form") +(os/setenv "JOLT_TYPE_CHECK" "off") + +(print "Success-type checking passed!") diff --git a/test/integration/type-infer-phase1-test.janet b/test/integration/type-infer-phase1-test.janet new file mode 100644 index 0000000..e60fbc1 --- /dev/null +++ b/test/integration/type-infer-phase1-test.janet @@ -0,0 +1,55 @@ +# Inter-procedural collection-type inference, Phase 1 (jolt-767): closed-world. +# A whole-unit fixpoint propagates collection types through the call graph — a +# fn's param types become the lub of its in-unit call-site arg types — so a +# param that always receives a struct map gets typed and its lookups specialize, +# with no hint. Fns whose var escapes as a value keep :any params (their callers +# aren't all visible). Sound under source distribution + whole-program compile. +(import ../../src/jolt/api :as api) +(import ../../src/jolt/backend :as backend) +(import ../../src/jolt/types :as types) +(import ../../src/jolt/reader :as reader) + +(print "Type inference Phase 1 (jolt-767)...") + +(os/setenv "JOLT_DIRECT_LINK" "1") +(def ctx (api/init {:compile? true})) +(api/eval-string ctx "(ns p1)") +# closed-world unit. mk is small (inlined away). rd is RECURSIVE, so it survives +# inlining and is called via its var — exactly the shape (big/recursive fn with +# escaping-from-the-caller params) that inter-procedural inference targets. Its +# param v flows from mk's struct-map literal (after mk inlines into drv). +(each s ["(defn mk [a b] {:r a :g b})" + "(defn rd [v n] (if (< n 1) (:r v) (rd v (dec n))))" + "(defn drv [] (rd (mk 1 2) 3))" + # esc's var is used as a VALUE (passed to mapv) -> params must stay :any + "(defn esc [w] (:r w))" + "(defn use-esc [xs] (mapv esc xs))"] + (api/eval-string ctx s)) + +(def report (backend/infer-unit! ctx "p1")) + +# --- the fixpoint computed the right param types ----------------------------- +# rd's param v flows from mk's struct result (mk inlines to a struct literal in +# drv) and stays struct across the recursive self-call -> a {:struct ...} type +(defn struct-type? [t] (truthy? (get t :struct))) +(assert (struct-type? (in (get report "p1/rd") 0)) (string "rd param v: " (in (get report "p1/rd") 0))) +# esc escaped (passed to mapv) -> param stays unknown (:any / nil), NOT struct +(assert (not (struct-type? (in (get report "p1/esc") 0))) "escaping fn param not inferred struct") + +# --- the seeded re-inference drops the guard for a struct param -------------- +# (on a FRESH analysis, since infer-unit! re-stashes the already-specialized body) +(def pns (types/ctx-find-ns ctx "jolt.passes")) +(def reinfer (types/ns-find pns "reinfer-def")) +(def rd-def (backend/analyze-form ctx (reader/parse-string "(defn rdx [v n] (if (< n 1) (:r v) (rdx v (dec n))))"))) +(defn guards-seeded [ptmap] + (length (string/find-all ":jolt/type" (string/format "%p" (backend/emit-ir ctx ((types/var-get reinfer) rd-def ptmap)))))) +(assert (= 0 (guards-seeded @{"v" {:struct {}}})) "struct param -> bare lookup") +(assert (= 1 (guards-seeded @{})) "no param type -> guard kept") + +# --- correctness: recompiled unit still computes the same -------------------- +(assert (= 1 (api/eval-string ctx "(p1/drv)")) "drv correct after recompile") +(assert (= 7 (api/eval-string ctx "(p1/rd {:r 7 :g 8} 0)")) "rd correct on a struct") +(assert (= nil (api/eval-string ctx "(p1/rd (hash-map :r nil) 0)")) "rd correct on a phm (key present, nil)") +(assert (deep= [1 1] (api/normalize-pvecs (api/eval-string ctx "(p1/use-esc [{:r 1} {:r 1}])"))) "escaping fn still correct") + +(print "Type inference Phase 1 passed!") diff --git a/test/integration/type-infer-phase2-test.janet b/test/integration/type-infer-phase2-test.janet new file mode 100644 index 0000000..94c8aeb --- /dev/null +++ b/test/integration/type-infer-phase2-test.janet @@ -0,0 +1,24 @@ +# Vector op specialization, Phase 2 (jolt-d6u): a value the inference proved to +# be a vector ({:vec ...}) gets count -> pv-count (skip core-count's dispatch) +# and 3-arg nth -> pv-nth. 2-arg nth is NOT specialized: it errors on +# out-of-bounds where pv-nth returns nil. +(import ../../src/jolt/api :as api) +(import ../../src/jolt/backend :as backend) +(import ../../src/jolt/types :as types) +(import ../../src/jolt/reader :as reader) +(print "Type inference Phase 2 (vector ops)...") +(os/setenv "JOLT_DIRECT_LINK" "1") +(def ctx (api/init {:compile? true})) +(api/eval-string ctx "(ns p2)") +(def reinfer (types/var-get (types/ns-find (types/ctx-find-ns ctx "jolt.passes") "reinfer-def"))) +(defn estr [src ptmap] + (string/format "%p" (backend/emit-ir ctx (reinfer (backend/analyze-form ctx (reader/parse-string src)) ptmap)))) +(assert (string/find "pv-count" (estr "(defn f [v] (count v))" @{"v" {:vec :any}})) "count on vector -> pv-count") +(assert (not (string/find "pv-count" (estr "(defn f [v] (count v))" @{}))) "count on unknown not specialized") +(assert (string/find "pv-nth" (estr "(defn f [v i] (nth v i 0))" @{"v" {:vec :any}})) "3-arg nth on vector -> pv-nth") +(assert (not (string/find "pv-nth" (estr "(defn f [v i] (nth v i))" @{"v" {:vec :any}}))) "2-arg nth NOT specialized") +# correctness +(assert (= 3 (api/eval-string ctx "(count [1 2 3])")) "count value") +(assert (= 2 (api/eval-string ctx "(nth [1 2 3] 1 9)")) "nth 3-arg in-bounds") +(assert (= 9 (api/eval-string ctx "(nth [1 2 3] 5 9)")) "nth 3-arg default") +(print "Type inference Phase 2 passed!") diff --git a/test/integration/type-infer-phase3-test.janet b/test/integration/type-infer-phase3-test.janet new file mode 100644 index 0000000..e9dc1c5 --- /dev/null +++ b/test/integration/type-infer-phase3-test.janet @@ -0,0 +1,41 @@ +# Collection-element types + HOF awareness, Phase 3 (jolt-d6u). A vector carries +# its element type ({:vec ELEM}); a reduce/map/filter closure over it gets that +# element type on its element param. So a lookup inside a reduce closure over a +# vector-of-structs specializes — no hint — WHEN the element type is provable. +(import ../../src/jolt/api :as api) +(import ../../src/jolt/backend :as backend) +(import ../../src/jolt/types :as types) +(import ../../src/jolt/reader :as reader) + +(print "Type inference Phase 3 (jolt-d6u)...") + +(os/setenv "JOLT_DIRECT_LINK" "1") +(def ctx (api/init {:compile? true})) +(api/eval-string ctx "(ns p3)") +(def pns (types/ctx-find-ns ctx "jolt.passes")) +(def reinfer (types/var-get (types/ns-find pns "reinfer-def"))) +# helper: analyze a defn, reinfer with seeded param types, count guards +(defn guards [src ptmap] + (def d (backend/analyze-form ctx (reader/parse-string src))) + (length (string/find-all ":jolt/type" (string/format "%p" (backend/emit-ir ctx (reinfer d ptmap)))))) + +# a reduce closure's element param gets the vector's element type +(def red "(defn f [coll] (reduce (fn [acc h] (+ acc (:r h))) 0 coll))") +(assert (= 0 (guards red @{"coll" {:vec {:struct {}}}})) "reduce element typed -> bare lookup in closure") +(assert (= 1 (guards red @{"coll" {:vec :any}})) "reduce over vector of unknown -> guard kept") +(assert (= 1 (guards red @{})) "untyped coll -> guard kept") + +# mapv over a vector-of-structs types the closure element too +(def mp "(defn g [coll] (mapv (fn [h] (:r h)) coll))") +(assert (= 0 (guards mp @{"coll" {:vec {:struct {}}}})) "mapv element typed -> bare lookup") +(assert (= 1 (guards mp @{"coll" {:vec :any}})) "mapv over unknown element -> guard") + +# element type is DERIVED, not just seeded: a vector literal of structs, reduced +(def derived "(defn h2 [] (reduce (fn [acc x] (+ acc (:r x))) 0 [{:r 1 :g 2} {:r 3 :g 4}]))") +(assert (= 0 (guards derived @{})) "vector literal of structs -> element struct -> bare lookup") + +# correctness: the specialized closures compute the same +(assert (= 4 (api/eval-string ctx "((fn [coll] (reduce (fn [acc h] (+ acc (:r h))) 0 coll)) [{:r 1} {:r 3}])")) "reduce value") +(assert (= 4 (api/eval-string ctx "(reduce (fn [acc x] (+ acc (:r x))) 0 [{:r 1 :g 2} {:r 3 :g 4}])")) "derived value") + +(print "Type inference Phase 3 passed!") diff --git a/test/integration/type-infer-test.janet b/test/integration/type-infer-test.janet new file mode 100644 index 0000000..016500a --- /dev/null +++ b/test/integration/type-infer-test.janet @@ -0,0 +1,54 @@ +# Static collection-type inference, Phase 0 (jolt-6sr): intra-procedural. +# The pass infers an expression's collection type from literals/arithmetic and +# flows it through let bindings and if-joins. Where a keyword-lookup subject is +# PROVEN to be a plain struct map it auto-drops the :jolt/type guard (the +# inference output is the same ^:struct channel as a manual hint); where the +# type is unknown it stays :any and keeps the dynamic guard (sound fallback). +# +# Note: Route 1 scalar-replacement already eliminates NON-escaping let-bound +# maps outright, so these cases force the map to ESCAPE (pass it to `sink`) to +# isolate what inference adds — typing a map that survives and is then looked up. +(import ../../src/jolt/api :as api) +(import ../../src/jolt/backend :as backend) +(import ../../src/jolt/reader :as reader) + +(print "Type inference Phase 0 (jolt-6sr)...") + +(os/setenv "JOLT_DIRECT_LINK" "1") +(def ctx (api/init {:compile? true})) +(api/eval-string ctx "(ns ti)") + +(defn guards [src] + (length (string/find-all ":jolt/type" + (string/format "%p" (backend/emit-ir ctx (backend/analyze-form ctx (reader/parse-string src))))))) +(defn ev [src] (api/eval-string ctx src)) + +# --- guard auto-removal where the type is proven, no hint ------------------- +# escaping struct-map literal (scalar keys, truthy values) is proven struct +(assert (= 0 (guards "(fn [sink] (let [v {:r 1 :g 2 :b 3}] (sink v) (:r v)))")) "inferred struct-map literal -> bare lookup") +# arithmetic values are provably non-nil/non-false -> still a struct +(assert (= 0 (guards "(fn [sink a b] (let [v {:r (+ a 1) :g (* b 2) :b 7}] (sink v) (:r v)))")) "arithmetic-valued map inferred struct") +# the inferred type flows through a rebinding +(assert (= 0 (guards "(fn [sink] (let [v {:r 1 :g 2} w v] (sink w) (:r w)))")) "inferred type flows through a rebinding") +# both if-branches struct -> join is struct +(assert (= 0 (guards "(fn [sink c] (let [v (if c {:a 1} {:a 2})] (sink v) (:a v)))")) "if-join of two struct literals stays struct") + +# --- sound fallback to the guard where the type is NOT proven --------------- +# a param is unknown (Phase 1 handles params) -> guard kept, exactly as today +(assert (= 1 (guards "(fn [m] (:r m))")) "unknown param keeps the guard") +# a value that could be nil/false makes the literal maybe-phm -> :any -> guard +(assert (= 1 (guards "(fn [sink x] (let [v {:r x}] (sink v) (:r v)))")) "maybe-nil value -> not proven struct -> guard") +# join of a struct and a phm is :any -> guard +(assert (>= (guards "(fn [sink c] (let [v (if c {:a 1} (hash-map :a nil))] (sink v) (:a v)))") 1) "struct/phm join -> :any -> guard") + +# --- correctness: every shape evaluates to the same as the guarded path ----- +(def snk "(fn [_] nil)") +(assert (= 1 (ev (string "((fn [sink] (let [v {:r 1 :g 2 :b 3}] (sink v) (:r v))) " snk ")"))) "struct literal value") +(assert (= 6 (ev (string "((fn [sink a] (let [v {:r (+ a 1)}] (sink v) (:r v))) " snk " 5)"))) "arithmetic-valued struct") +(assert (= 2 (ev (string "((fn [sink] (let [v {:r 1 :g 2} w v] (sink w) (:g w))) " snk ")"))) "flowed type value") +(assert (= 1 (ev (string "((fn [sink c] (let [v (if c {:a 1} {:a 2})] (sink v) (:a v))) " snk " true)"))) "if-join value") +(assert (= nil (ev (string "((fn [sink x] (let [v {:r x}] (sink v) (:r v))) " snk " nil)"))) "maybe-nil map reads correctly (nil)") +(assert (= nil (ev (string "((fn [sink c] (let [v (if c {:a 1} (hash-map :a nil))] (sink v) (:a v))) " snk " false)"))) "phm branch reads nil correctly") +(assert (= 1 (ev (string "((fn [sink c] (let [v (if c {:a 1} (hash-map :a nil))] (sink v) (:a v))) " snk " true)"))) "struct branch reads correctly") + +(print "Type inference Phase 0 passed!")