Add inference gate (jolt.passes.types)
The corpus/unit gates compile through run-passes' const-fold-only branch, so the type-inference walk runs only under jolt build --opt — buildsmoke hit one trivial app and checked stdout. run-infer.ss drives the pass directly: analyze a source string, then call check-form / infer-body / the set-*! registries and assert diagnostic counts and collected calls/escapes. Wired into make ci. Gives the inference pass real behavior coverage so refactoring its internal state is gate-validatable. jolt-ogib.10 groundwork.
This commit is contained in:
Yogthos
parent
e434356590
commit
9c5e46e91b
2 changed files with 100 additions and 2 deletions
10
Makefile
10
Makefile
|
|
@ -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 remint
|
||||
.PHONY: test ci values corpus unit smoke buildsmoke selfhost sci certify ffi transient infer 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 certify
|
||||
ci: values corpus unit smoke buildsmoke sci ffi transient infer certify
|
||||
@echo "OK: CI gates passed"
|
||||
|
||||
# Self-host fixpoint: bootstrap.ss rebuild == checked-in seed.
|
||||
|
|
@ -55,6 +55,12 @@ ffi:
|
|||
transient:
|
||||
@chez --script test/chez/transient-test.ss
|
||||
|
||||
# Inference / success-type checking: drive jolt.passes.types directly and assert
|
||||
# diagnostic counts + collected calls/escapes (the optimization pass the other
|
||||
# gates don't exercise).
|
||||
infer:
|
||||
@chez --script host/chez/run-infer.ss
|
||||
|
||||
# JVM oracle: certify the corpus against reference Clojure. Skips if clojure absent.
|
||||
certify:
|
||||
@if command -v clojure >/dev/null 2>&1; then \
|
||||
|
|
|
|||
92
host/chez/run-infer.ss
Normal file
92
host/chez/run-infer.ss
Normal file
|
|
@ -0,0 +1,92 @@
|
|||
;; run-infer.ss — inference / success-type-checking gate (jolt.passes.types).
|
||||
;;
|
||||
;; The corpus and unit gates compile through run-passes' const-fold-only branch,
|
||||
;; so the inference walk (jolt.passes.types) runs only under `jolt build --opt` —
|
||||
;; buildsmoke exercises it on one trivial app and asserts stdout only. This gate
|
||||
;; drives the pass DIRECTLY: analyze a source string to IR, then call the public
|
||||
;; checker/driver entry points (check-form, infer-body, the set-*! registries) and
|
||||
;; assert their observable output (diagnostic counts, collected calls/escapes). It
|
||||
;; pins the behavior the inference walk's internal state produces, so a refactor of
|
||||
;; that state is gate-validatable.
|
||||
;;
|
||||
;; chez --script host/chez/run-infer.ss
|
||||
(import (chezscheme))
|
||||
|
||||
(load "host/chez/rt.ss")
|
||||
(set-chez-ns! "clojure.core")
|
||||
(load "host/chez/seed/prelude.ss")
|
||||
(load "host/chez/post-prelude.ss")
|
||||
(set-chez-ns! "user")
|
||||
(load "host/chez/host-contract.ss")
|
||||
(load "host/chez/seed/image.ss")
|
||||
(load "host/chez/compile-eval.ss")
|
||||
|
||||
(define analyze (var-deref "jolt.analyzer" "analyze"))
|
||||
(define check-form (var-deref "jolt.passes.types" "check-form"))
|
||||
(define infer-body (var-deref "jolt.passes.types" "infer-body"))
|
||||
(define reset-escapes! (var-deref "jolt.passes.types" "reset-escapes!"))
|
||||
(define collected-escapes (var-deref "jolt.passes.types" "collected-escapes"))
|
||||
(define set-record-shapes! (var-deref "jolt.passes.types" "set-record-shapes!"))
|
||||
(define set-vtypes! (var-deref "jolt.passes.types" "set-vtypes!"))
|
||||
|
||||
;; analyze a source string to its IR node (fresh ctx, ns "user", no passes).
|
||||
(define (anode src) (analyze (make-analyze-ctx "user") (jolt-ce-read src)))
|
||||
;; number of success-type diagnostics check-form produces for src.
|
||||
(define (diags src strict?) (jolt-count (check-form (anode src) strict?)))
|
||||
|
||||
(define fails 0)
|
||||
(define total 0)
|
||||
(define (check label actual expected)
|
||||
(set! total (+ total 1))
|
||||
(unless (equal? actual expected)
|
||||
(set! fails (+ fails 1))
|
||||
(printf " FAIL ~a: got ~s expected ~s\n" label actual expected)))
|
||||
|
||||
;; --- core error-domain checking (strict not required) -----------------------
|
||||
(check "num-op on keyword" (diags "(+ 1 :k)" #f) 1)
|
||||
(check "num-op all numbers" (diags "(+ 1 2)" #f) 0)
|
||||
(check "count on number" (diags "(count 5)" #f) 1)
|
||||
(check "count on vector" (diags "(count [1 2])" #f) 0)
|
||||
(check "lenient (:k 5)" (diags "(:k 5)" #f) 0)
|
||||
(check "call a number" (diags "(5 1)" #f) 1)
|
||||
(check "nested count return type" (diags "(+ 1 (count :k))" #f) 1)
|
||||
|
||||
;; --- walk arms thread the type env ------------------------------------------
|
||||
(check "let binds kw" (diags "(let [x :k] (+ x 1))" #f) 1)
|
||||
(check "let binds ok" (diags "(let [x 1] (+ x 1))" #f) 0)
|
||||
(check "if then branch error" (diags "(if true (+ 1 :k) 2)" #f) 1)
|
||||
(check "do statement error" (diags "(do (+ 1 :k) 2)" #f) 1)
|
||||
(check "mapv seeds element type" (diags "(mapv (fn [x] (+ x 1)) [:a :b])" #f) 1)
|
||||
(check "mapv ok element type" (diags "(mapv (fn [x] (+ x 1)) [1 2])" #f) 0)
|
||||
(check "reduce seeds element" (diags "(reduce (fn [acc x] (+ acc x)) 0 [:a])" #f) 1)
|
||||
|
||||
;; --- strict user-function domains (checking-box / diag-memo / user-sig) ------
|
||||
(check "user wrong arg type" (diags "(do (defn f [x] (+ x 1)) (f :k))" #t) 1)
|
||||
(check "user wrong arity" (diags "(do (defn g [x] x) (g 1 2))" #t) 1)
|
||||
(check "user call ok" (diags "(do (defn h [x] (+ x 1)) (h 3))" #t) 0)
|
||||
(check "user domains off w/o strict" (diags "(do (defn f [x] (+ x 1)) (f :k))" #f) 0)
|
||||
;; recursive user fn terminates (cycle guard) and still flags the bad arg
|
||||
(check "user recursive terminates"
|
||||
(diags "(do (defn rf [x] (+ x (rf x))) (rf :k))" #t) 1)
|
||||
|
||||
;; --- infer-body collects calls + escapes ------------------------------------
|
||||
(reset-escapes!)
|
||||
(let ((r (infer-body (anode "(do (foo 1) (bar 2) (map inc [1]))") (jolt-hash-map))))
|
||||
(check "infer-body calls" (jolt-count (jolt-nth r 2)) 3) ; foo, bar, map
|
||||
(check "infer-body escapes" (jolt-count (collected-escapes)) 1)) ; inc (value position)
|
||||
|
||||
;; --- the record-shapes registry feeds call-result types --------------------
|
||||
;; without shapes a (->P …) call result is :any (accepted); with the registry it
|
||||
;; types as a struct, so an arithmetic op over it is provably not-a-number.
|
||||
(check "ctor result :any w/o shapes" (diags "(+ (->P 1) 1)" #f) 0)
|
||||
(set-record-shapes!
|
||||
(jolt-hash-map "user/->P"
|
||||
(jolt-hash-map (keyword #f "fields") (jolt-vector (keyword #f "x"))
|
||||
(keyword #f "tags") (jolt-vector jolt-nil)
|
||||
(keyword #f "type") "user.P")))
|
||||
(check "ctor result struct w/ shapes" (diags "(+ (->P 1) 1)" #f) 1)
|
||||
(set-record-shapes! (jolt-hash-map))
|
||||
|
||||
(if (= fails 0)
|
||||
(begin (printf "infer gate: ~a/~a passed\n" total total) (exit 0))
|
||||
(begin (printf "infer gate: ~a/~a passed (~a failed)\n" (- total fails) total fails) (exit 1)))
|
||||
Loading…
Add table
Add a link
Reference in a new issue