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

Hintless whole-program double inference (#230)

Browse source 
The closed-world fixpoint (#226) flowed record types across fn boundaries; this
adds a numeric refinement so a hintless fn whose every call site passes a flonum
has its param unboxed to fl-ops, no ^double hint needed.

Lattice gains :double, a flonum refinement of :num: two doubles join to :double,
a double joined with anything else widens to :num — so a param is :double only
when every contributing value is a flonum, which is what makes the fl-op sound.
infer types a flonum literal and flonum arithmetic (+ - * / min max inc dec over
double/int-literal operands) as :double, and the fixpoint joins those across call
sites and return types like any other lattice value.

The bridge to the existing hint-directed pass is a synthetic [param :double]
nhint: wp-infer! stashes the :double params separately from the structural seeds,
and run-passes injects them as nhints before numeric/annotate, so the fl-op
emission and the exact->inexact entry coercion (a no-op on a proven flonum) apply
unchanged.

Sound subset only: :double, never :long — an untyped integer can be a bignum and
fx-ops would overflow/diverge from jolt's arbitrary precision. So an integer
caller leaves a param generic; an escaped fn (unknown callers) keeps :any.

run-numwp.ss gate: cross-fn :double propagation incl. through a flonum-returning
helper, the integer-caller and escape negatives, and the full run-passes path
emitting fl* + entry coercion. make test / shakesmoke green, selfhost holds, 0
new divergences.

Co-authored-by: Yogthos <yogthos@gmail.com>
This commit is contained in:
Dmitri Sotnikov 2026-06-26 14:18:10 +00:00 • committed by GitHub
parent e6e3612332
commit 8ae45057d6
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
6 changed files with 453 additions and 268 deletions
Download patch file Download diff file Expand all files Collapse all files

11
Makefile
View file

@ -4,7 +4,7 @@
# build step. `make test` is the full gate. `make remint` rebuilds the seed after a
# source change.
.PHONY: test ci values corpus unit smoke buildsmoke selfhost sci certify ffi transient infer wp devirt fieldread directlink numeric inline shakesmoke remint
.PHONY: test ci values corpus unit smoke buildsmoke selfhost sci certify ffi transient infer wp devirt fieldread numwp directlink numeric inline shakesmoke remint
# Full gate (dev machine). Includes the self-host byte-fixpoint, which only holds
# on the same Chez that minted the seed.
@ -15,7 +15,7 @@ test: selfhost ci
# lockfile) — it RUNS correctly on any Chez, but `selfhost` rebuilds it and a
# different Chez version may emit byte-different (gensym/order) output, so the
# byte-fixpoint is a dev-machine check, not a CI one (jolt-8479).
ci: values corpus unit smoke buildsmoke sci ffi transient infer wp devirt fieldread directlink numeric inline certify
ci: values corpus unit smoke buildsmoke sci ffi transient infer wp devirt fieldread numwp directlink numeric inline certify
@echo "OK: CI gates passed"
# Self-host fixpoint: bootstrap.ss rebuild == checked-in seed.
@ -79,6 +79,13 @@ devirt:
fieldread:
@chez --script host/chez/run-fieldread.ss
# Hintless whole-program double inference: a fn whose every call site passes a
# flonum has its param typed :double by the closed-world fixpoint and unboxed to
# fl-ops with no ^double hint; an integer caller leaves it generic, an escaped fn
# keeps :any.
numwp:
@chez --script host/chez/run-numwp.ss
# Direct-linking emission: a closed-world build binds top-level app defs to jv$
# Scheme bindings and routes app->app calls/refs to them, skipping var-deref +
# jolt-invoke; ^:dynamic/^:redef and nested defs opt out.