Joseph Ferano
cdda829835
A narrower scalar at a $t a slice already fixed widens into the fixed type — the same cast a monomorphic parameter applies — where the old rule refused both directions. One accepts pin, one runtime line in int-generic.flan, and the web page's predicate table catches up: five predicates, integer? at the head, and the entailment chain grown one link.
113 lines
3.8 KiB
Plaintext
113 lines
3.8 KiB
Plaintext
;;;; integer?, end to end: the bound numeric? was one type too wide for.
|
|
;;;;
|
|
;;;; Three families in here, in order. The collapsed abs — one written body
|
|
;;;; under {:where (integer? $t)} where abs-i32 and abs-i64 used to be, pinned
|
|
;;;; at six widths, at both signed minimums (the answer is itself, because the
|
|
;;;; negation wraps — what every two's-complement abs does), and beside the
|
|
;;;; libm float pair it deliberately does not shadow: (abs-f64 -0.0) is 0
|
|
;;;; because fabs clears the sign bit, which no integer body spells. Then the
|
|
;;;; operations only integer? admits in a generic body — bit-and, bit-or,
|
|
;;;; bit-xor, the shifts, and % — at several widths each. Then the join:
|
|
;;;; mixed widths at one $t resolve to the wider type in either argument
|
|
;;;; order (FIX.org 2026-09-20), so both orders print the same number from
|
|
;;;; the same copy.
|
|
|
|
(defvar i32min i32 -2147483648)
|
|
(defvar i64min i64 -9223372036854775808)
|
|
|
|
;; The low n bits, which needs a shift, a bit-and and the literal 1 — every
|
|
;; one of them admitted by integer? and none by anything weaker.
|
|
(defn low-bits [x $t n $t] $t
|
|
{:where (integer? $t)}
|
|
(bit-and x (- (<< 1 n) 1)))
|
|
|
|
;; Truncated %, the semantics everywhere in the language, in a generic body.
|
|
(defn even? [x $t] bool
|
|
{:where (integer? $t)}
|
|
(= (% x 2) 0))
|
|
|
|
;; xor and or, and the shift right.
|
|
(defn toggle [x $t m $t] $t
|
|
{:where (integer? $t)}
|
|
(bit-xor x m))
|
|
|
|
(defn with-flag [x $t f $t] $t
|
|
{:where (integer? $t)}
|
|
(bit-or x f))
|
|
|
|
(defn halve [x $t] $t
|
|
{:where (integer? $t)}
|
|
(>> x 1))
|
|
|
|
;; The untyped literal at a bounded variable: admitted under integer? by the
|
|
;; same arm that admits it under numeric?, ranged per copy.
|
|
(defn plus-300 [x $t] $t
|
|
{:where (integer? $t)}
|
|
(+ x 300))
|
|
|
|
;; The join family. eq2? is the pair the refusal used to be pinned on.
|
|
(defn eq2? [a $t b $t] bool
|
|
{:where (equal? $t)}
|
|
(= a b))
|
|
|
|
(defn tri [a $t b $t c $t] $t
|
|
{:where (numeric? $t)}
|
|
(+ a (+ b c)))
|
|
|
|
(defn main [] ()
|
|
;; abs, one body, six widths.
|
|
(println (abs (i8 -7)))
|
|
(println (abs -7))
|
|
(println (abs (i64 -7)))
|
|
(println (abs (u8 7)))
|
|
(println (abs (u32 7)))
|
|
(println (abs (u64 7)))
|
|
;; The signed minimums answer themselves: the negation wraps, and saturating
|
|
;; quietly would be the wrong answer this file exists to refuse.
|
|
(println (abs i32min))
|
|
(println (abs i64min))
|
|
;; The float abs stays libm's: a sign-bit clear, so -0.0 comes back 0.
|
|
(println (abs-f64 -0.0))
|
|
(println (abs-f32 -0.0))
|
|
(println (abs-f64 -1.5))
|
|
(println (abs-f32 -2.5))
|
|
|
|
;; The integer?-only operations, per width.
|
|
(println (low-bits 255 3))
|
|
(println (low-bits (u16 65535) (u16 4)))
|
|
(println (low-bits (i64 1023) (i64 5)))
|
|
(println (even? 4))
|
|
(println (even? (u8 3)))
|
|
(println (even? (i64 -2)))
|
|
(println (toggle (u8 255) (u8 15)))
|
|
(println (with-flag 8 1))
|
|
(println (halve (u64 10)))
|
|
(println (halve (i64 -4)))
|
|
(println (plus-300 1))
|
|
(println (plus-300 (i64 1)))
|
|
|
|
;; The join: both orders, one copy, one answer.
|
|
(let [a (i8 3)
|
|
b (i64 3)]
|
|
(println (eq2? a b))
|
|
(println (eq2? b a)))
|
|
(let [x (u32 1)
|
|
y (i32 2)
|
|
z (i64 3)]
|
|
;; u32 and i32 meet at no type of their own; all three meet at the i64,
|
|
;; wherever it stands in the argument list.
|
|
(println (tri x y z))
|
|
(println (tri z y x)))
|
|
;; A literal beside a wider variable joins too: 4 arrives as an i32 and the
|
|
;; copy is i64's.
|
|
(let [w (i64 38)]
|
|
(println (tri w 3 1)))
|
|
;; And the one direction a container-bound variable does admit: the slice
|
|
;; fixed $t at i32 exactly, and a narrower scalar widens *into* that — the
|
|
;; same conversion a monomorphic i32 parameter would apply. (The reverse,
|
|
;; an i64 scalar against this slice, stays refused; the checker pins it.)
|
|
(let [ns [5 3 9 1]]
|
|
(match (index-of (slice ns 0 4) (i16 9))
|
|
(Some i) (println i)
|
|
_ (println -1))))
|