typed-rust: f64 math — float literals, exact->inexact, log2, float division
ober
3de8612b022371fb35ca9c88d7188ec564077daa
--- a/docs/jerboa-to-rust.md +++ b/docs/jerboa-to-rust.md @@ -96,6 +96,14 @@ Landed: is `(Bytes -> String)` and lowers to lossy decode `String::from_utf8_lossy(&(buf)).into_owned()` (matches the String input ABI, never panics). Both borrow rather than move their source. +- `f64` math: float literals lower to `<n>f64` (the `flonum?` check precedes + `integer?`, so `4.0` stays a Float, not a Nat); `exact->inexact` widens any + numeric operand with an `as f64` cast; `log2` lowers to `f64::log2`; and + `+`/`-`/`*`/`/` on Float operands are native f64 ops (the result type follows + `merge-numeric-types`, so any Float operand makes the expression Float). This + is enough to compute a Shannon-entropy term `-p*log2(p)`; see + `tests/fixtures/typed/rust-float.ss`. The f64 return ABI is wired through the + generated FFI wrapper. - `for/fold` over a single `in-range` clause with one accumulator lowers to a native Rust `for` loop: `{ let mut acc = init; for i in (start)..(end) { acc = body; } acc }`. The accumulator type is pinned by its initial value and the --- a/docs/typed-jerboa.md +++ b/docs/typed-jerboa.md @@ -237,7 +237,10 @@ Current landing: Jerboa — see `tests/fixtures/typed/rust-ct-equal.ss`. `make-bytevector` is checked as `(Nat -> Bytes)` / `(Nat Nat -> Bytes)` (fill defaults to `0`) and lowers to a fresh owned `vec![(fill) as u8; (size) as usize]`; in-place - mutation is still future work. `string->utf8` + mutation is still future work. Float (`f64`) math is supported: float + literals, `exact->inexact` (numeric→Float `as f64` cast), `log2`, and + `+`/`-`/`*`/`/` over Float operands — enough for a Shannon-entropy term + `-p*log2(p)` (`tests/fixtures/typed/rust-float.ss`). `string->utf8` (`String -> Bytes`) and `utf8->string` (`Bytes -> String`) cross the text/binary boundary, lowering to `as_bytes().to_vec()` and a lossy `from_utf8_lossy` decode, so a constant-time auth-token comparison ports too --- a/lib/jerboa/typed/checker.ss +++ b/lib/jerboa/typed/checker.ss @@ -371,7 +371,12 @@ 'string->utf8 '())) (cons 'utf8->string (make-typed-call-sig (list 'Bytes) 'String '() - 'utf8->string '())))) + 'utf8->string '())) + ;; base-2 logarithm on a float (the entropy/log-likelihood primitive); + ;; callers cast integers up with exact->inexact first. + (cons 'log2 + (make-typed-call-sig (list 'Float) 'Float '() + 'log2 '())))) (def (field-types fields) (map typed-field-type fields)) @@ -1277,6 +1282,25 @@ (append acc-errors start-errors end-errors body-errors range-errors invariant-errors)))))))]))) + (def (infer-to-float args env type-names expr) + ;; (exact->inexact n): widen any numeric operand to Float. Custom inference + ;; (not a fixed signature) because the operand may be Nat, Int, or Fixnum. + (if (not (= (length args) 1)) + (values #f + (list (error-at expr 'bad-primitive-arity + "exact->inexact needs exactly one operand" + expr))) + (let-values ([(arg-ir errors) (infer-expression (car args) env type-names)]) + (let* ([operand-errors + (operand-type-errors 'numeric (list (ir-type arg-ir)) + (list expr) expr)] + [ok? (and arg-ir (null? errors) (null? operand-errors))]) + (values + (and ok? + (make-typed-ir-call 'Float (expr-source expr) + 'exact->inexact 'exact->inexact (list arg-ir) '())) + (append errors operand-errors)))))) + (def (infer-make-bytevector args env type-names expr) ;; (make-bytevector size) or (make-bytevector size fill). Size and fill are ;; numeric; the result is a fresh Bytes buffer. A missing fill defaults to a @@ -1591,6 +1615,10 @@ (values (make-typed-ir-lit 'String src value) '())] [(bytevector? value) (values (make-typed-ir-lit 'Bytes src value) '())] + ;; check flonum? before integer?: in Chez (integer? 3.0) is #t, so an + ;; integer-valued flonum like 4.0 must still type as Float, not Nat. + [(flonum? value) + (values (make-typed-ir-lit 'Float src value) '())] [(integer? value) (values (make-typed-ir-lit (if (>= value 0) 'Nat 'Int) src value) @@ -1638,6 +1666,8 @@ (infer-for-fold args env type-names expr)] [(make-bytevector) (infer-make-bytevector args env type-names expr)] + [(exact->inexact) + (infer-to-float args env type-names expr)] [(option-some) (infer-option-some args env type-names expr)] [(option-none) --- a/lib/jerboa/typed/core.ss +++ b/lib/jerboa/typed/core.ss @@ -115,6 +115,8 @@ string->utf8 utf8->string make-bytevector + exact->inexact + log2 debug-string record-ctor record-pred --- a/lib/jerboa/typed/rust.ss +++ b/lib/jerboa/typed/rust.ss @@ -1314,6 +1314,18 @@ (emit-expression (car args)) ") as usize]")) + ;; (exact->inexact n) -> widen a numeric value to f64 with an `as` cast. + (def (emit-to-float args) + (unless (= (length args) 1) + (error 'typed-rust "exact->inexact expects one operand" args)) + (string-append "((" (emit-expression (car args) ) ") as f64)")) + + ;; (log2 x) -> f64::log2; the checker requires a Float operand. + (def (emit-log2 args) + (unless (= (length args) 1) + (error 'typed-rust "log2 expects one operand" args)) + (string-append "((" (emit-expression (car args)) ").log2())")) + ;; borrow the String's bytes and copy into an owned Vec<u8> (no move, so the ;; source String stays usable under the Clone-heavy ownership model) (def (emit-string->utf8 args) @@ -1558,6 +1570,8 @@ [(string->utf8) (emit-string->utf8 args)] [(utf8->string) (emit-utf8->string args)] [(make-bytevector) (emit-make-bytevector args)] + [(exact->inexact) (emit-to-float args)] + [(log2) (emit-log2 args)] [(debug-string) (emit-debug-string args)] [(record-ctor) (let ([record (lookup-name (ir-call-info-ref ir 'record) @@ -1636,6 +1650,11 @@ "u8") out)))) "]"))] + ;; flonum? before integer?: (integer? 4.0) is #t in Chez, but a Float + ;; literal must emit an f64. number->string keeps the decimal point + ;; (4.0 -> "4.0"), so "<n>f64" is always a valid Rust float literal. + [(flonum? expr) + (string-append (number->string expr) "f64")] [(integer? expr) (if (>= expr 0) (string-append (number->string expr) "u64") new file mode 100644 --- /dev/null +++ b/tests/fixtures/typed/rust-float.ss @@ -0,0 +1,19 @@ +(typed-library (sample typed float-math) + (export half widen neg-log2 entropy-term) + + ;; a bare Float literal (integer-valued and fractional both stay f64) + (def (half) : Float 0.5) + + ;; widen any numeric count up to Float + (def (widen (n : Nat)) : Float + (exact->inexact n)) + + ;; -log2(p): the per-symbol "surprise" used in Shannon entropy + (def (neg-log2 (p : Float)) : Float + (- 0.0 (log2 p))) + + ;; one Shannon entropy term -p*log2(p) for a symbol seen c of n times. + ;; Float division and the int->float casts are the point of the fixture. + (def (entropy-term (c : Nat) (n : Nat)) : Float + (let ((p (/ (exact->inexact c) (exact->inexact n)))) + (- 0.0 (* p (log2 p)))))) --- a/tests/test-typed-checker.ss +++ b/tests/test-typed-checker.ss @@ -715,6 +715,52 @@ (make-bytevector n b b)))) '(bad-primitive-arity)) +(test "float literal types as Float and returns from a def" + (error-kinds + '(typed-library (body float-lit) + (export f) + (def (f) : Float 0.5))) + '()) + +(test "integer-valued float literal still types as Float, not Nat" + (error-kinds + '(typed-library (body float-int-valued) + (export f) + (def (f) : Float 4.0))) + '()) + +(test "exact->inexact widens a Nat to Float" + (error-kinds + '(typed-library (body to-float) + (export f) + (def (f (n : Nat)) : Float + (exact->inexact n)))) + '()) + +(test "log2 returns Float and accepts a Float operand" + (error-kinds + '(typed-library (body log2-ok) + (export f) + (def (f (p : Float)) : Float + (log2 p)))) + '()) + +(test "log2 rejects a non-Float operand" + (error-kinds + '(typed-library (body log2-bad) + (export f) + (def (f (n : Nat)) : Float + (log2 n)))) + '(argument-type-mismatch)) + +(test "float arithmetic (division of casts) types as Float" + (error-kinds + '(typed-library (body float-div) + (export f) + (def (f (c : Nat) (n : Nat)) : Float + (/ (exact->inexact c) (exact->inexact n))))) + '()) + (test "record constructor and accessor calls" (error-kinds '(typed-library (body record-ok) --- a/tests/test-typed-rust.ss +++ b/tests/test-typed-rust.ss @@ -233,6 +233,21 @@ (define mkbv-rust (typed-library-form->rust-string mkbv-form)) +;; f64 math: float literals, the exact->inexact widening cast, log2, and float +;; division/mul/sub -- the building blocks of Shannon entropy scoring. +(define float-form + '(typed-library (sample typed float-math) + (export half widen entropy-term) + (def (half) : Float 0.5) + (def (widen (n : Nat)) : Float + (exact->inexact n)) + (def (entropy-term (c : Nat) (n : Nat)) : Float + (let ((p (/ (exact->inexact c) (exact->inexact n)))) + (- 0.0 (* p (log2 p))))))) + +(define float-rust + (typed-library-form->rust-string float-form)) + (define return-form '(typed-library (sample typed return-values) (export greeting echo-text echo-bytes) @@ -530,6 +545,16 @@ (substring? mkbv-rust "(vec![(255u64) as u8; (n) as usize]).len() as u64")) #t) +(test "rust lowers f64 math: float literal, cast, log2, division" + (and (substring? float-rust "pub fn half() -> f64") + (substring? float-rust "0.5f64") + (substring? float-rust "pub fn widen(n: u64) -> f64") + (substring? float-rust "((n) as f64)") + ;; the entropy term: p = (c as f64)/(n as f64), then -(p * p.log2()) + (substring? float-rust "(((c) as f64) / ((n) as f64))") + (substring? float-rust "(0.0f64 - (p * ((p).log2())))")) + #t) + (test "rust emits handle registry for record and variant ABI" (and (substring? handle-rust "fn jt_store_handle<T: Any + Send>(value: T) -> u64") (substring? handle-rust "fn jt_clone_handle<T: Any + Clone>(id: u64) -> Option<T>")