A reconsidered operand must leave nothing behind, and a literal is never reconsidered
This commit is contained in:
parent
3efa261539
commit
657f640ec7
126
lib/check.ml
126
lib/check.ml
@ -20,6 +20,19 @@
|
||||
|
||||
let fail = Loc.fail
|
||||
|
||||
(* "A literal could not be built at the type this site asked for": 300 at a u8,
|
||||
1.5 at an i32, 3000000000 at the i32 an unconstrained integer defaults to.
|
||||
|
||||
It is kinded rather than left generic because one caller has to tell this
|
||||
refusal apart from every other one. [binary] retries a refused operand
|
||||
against the other operand's type (FIX.org 2026-09-20, implicit widening),
|
||||
and it must not retry *this* one: a literal takes its width from the other
|
||||
side and always could, so a literal that does not fit is the program's
|
||||
mistake and not a pair of types that failed to meet. Without the kind the
|
||||
retry turns (+ u8-thing 300) into i32 arithmetic, which is a different
|
||||
language from the one the author decided on. *)
|
||||
let literal_at_want = "check/literal-at-want"
|
||||
|
||||
(* [List.map]'s evaluation order is unspecified, and checking allocates frame
|
||||
slots as a side effect. Left-to-right is required, not a preference: a later
|
||||
let binding sees an earlier one, and slot numbering must be reproducible. *)
|
||||
@ -2692,7 +2705,7 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
|
||||
match want with
|
||||
| Some (Types.Float k) -> k
|
||||
| Some other when other <> Types.Never ->
|
||||
fail loc "expected %s, found the float literal %g"
|
||||
Loc.failk literal_at_want loc "expected %s, found the float literal %g"
|
||||
(Types.to_string other) x
|
||||
| _ -> Types.F64
|
||||
in
|
||||
@ -3039,7 +3052,7 @@ and int_literal loc ~want ?(default = Types.I32) n =
|
||||
| Some (Types.Float k) ->
|
||||
mk loc (Types.Float k) (Tast.Float (Int64.to_float n, k))
|
||||
| Some other when other <> Types.Never ->
|
||||
fail loc "expected %s, found the integer literal %Ld"
|
||||
Loc.failk literal_at_want loc "expected %s, found the integer literal %Ld"
|
||||
(Types.to_string other) n
|
||||
| _ -> mk loc (Types.Int default) (Tast.Int (in_range loc default n, default))
|
||||
|
||||
@ -3066,7 +3079,8 @@ and in_range loc k n =
|
||||
&& Int64.compare n (Int64.shift_left 1L bits) < 0
|
||||
in
|
||||
if ok then n
|
||||
else fail loc "%Ld does not fit in %s" n (Types.ikind_name k)
|
||||
else Loc.failk literal_at_want loc "%Ld does not fit in %s" n
|
||||
(Types.ikind_name k)
|
||||
|
||||
(* The arms that are names rather than calls, and the same rule holds for them:
|
||||
each is in [builtins] below, and test_flan reads this match to check it. *)
|
||||
@ -7525,23 +7539,73 @@ and numeric_want want =
|
||||
construction: neither i32 nor u32 widens into the other, and the refusal
|
||||
says which cast to write.
|
||||
|
||||
[join_pair] is reached only when the *first* operand turned out to be the
|
||||
narrower one. The other order needs nothing here: checking y against an i64
|
||||
x already widens an i32 y inside [expect]. *)
|
||||
and join_pair ctx (a : Tast.expr) (y : Ast.expr) exn =
|
||||
(* Asking y for [a]'s type failed. Either y is genuinely wrong, or y is
|
||||
simply the wider operand and this is the one direction [expect] cannot
|
||||
serve on its own. Check y on its own terms to find out; if it decides a
|
||||
type that a widens into, a is the one that moves. Anything else re-raises
|
||||
the original refusal, so an error inside y is still reported as itself and
|
||||
no form that cannot check without an expectation — None, (zeroed) — loses
|
||||
the expectation it used to get. *)
|
||||
match check ctx y with
|
||||
| exception _ -> raise exn
|
||||
| b ->
|
||||
if Types.widens_to ~from:a.Tast.ty ~into:b.Tast.ty then
|
||||
widen a.Tast.loc b.Tast.ty a, b
|
||||
else raise exn
|
||||
The mechanism for 3 is a *trial*: ask y for [a]'s type, and if that refusal
|
||||
is the one widening was invented for, look again the other way round. Two
|
||||
things have to be true for a trial to be honest, and both are below.
|
||||
|
||||
[trial] is the first. Checking is not a function of its argument — it
|
||||
allocates frame slots and it opens scopes — so a check that is abandoned
|
||||
has to leave no trace, and [scoped] cannot help: it restores the scope on
|
||||
the way *out*, which an exception does not take. Without this a binding
|
||||
from the abandoned pass outlives it, which is visible as a name that should
|
||||
be unknown resolving anyway, and worse, as a shadow: the inner binding of
|
||||
(let [t ...] ... (let [t ...] t) ... t) survives into the outer t's slot
|
||||
with nothing ever stored in it. That is an uninitialised read, produced by
|
||||
a program the compiler accepted.
|
||||
|
||||
[literal_at_want] is the second. A trial that refused because a *literal*
|
||||
could not be built at the wanted type is not a pair of types that failed to
|
||||
meet — the literal had no type of its own to bring — so looking again would
|
||||
answer with the literal's default and quietly move (+ u8-thing 300) to i32.
|
||||
Rule 2 above is not a description of the old language kept for continuity;
|
||||
it is what the author decided, and the kind is how the trial obeys it. *)
|
||||
and trial ctx f =
|
||||
(* Everything a check writes into the context that is not the expression it
|
||||
answers. [defers] and [defer_slot] are on the list even though a [defer]
|
||||
inside an operand is already refused — [defer_ok] is cleared on entry to
|
||||
[check] — because "already impossible elsewhere" is the kind of reason
|
||||
that stops being true, and putting a field back costs nothing.
|
||||
|
||||
Only [Loc.Error] is caught. A timeout or a stack overflow is not a
|
||||
refusal to reconsider, and silently continuing past one would turn a
|
||||
resource failure into a wrong answer. *)
|
||||
let scope = ctx.scope and slots = ctx.slots in
|
||||
let slot_tys = ctx.slot_tys and slot_names = ctx.slot_names in
|
||||
let defers = ctx.defers and defer_slot = ctx.defer_slot in
|
||||
match f () with
|
||||
| r -> Ok r
|
||||
| exception Loc.Error d ->
|
||||
ctx.scope <- scope; ctx.slots <- slots;
|
||||
ctx.slot_tys <- slot_tys; ctx.slot_names <- slot_names;
|
||||
ctx.defers <- defers; ctx.defer_slot <- defer_slot;
|
||||
Error d
|
||||
|
||||
(* Whether the trial's refusal is one worth reconsidering. A literal that did
|
||||
not fit is not, and neither is a refusal a program cannot make any use of
|
||||
having a second opinion on. *)
|
||||
and reconsiderable (d : Loc.diag) = not (String.equal d.Loc.kind literal_at_want)
|
||||
|
||||
(* [a] was checked, y refused [a]'s type, and [b] is y on its own terms — held
|
||||
by the caller when it has one, taken here when it does not. If the pair has
|
||||
a join it can only be [b]'s type (had it been [a]'s, the trial would have
|
||||
passed), so [a] is the operand that moves. *)
|
||||
and join_widen (a : Tast.expr) (b : Tast.expr) =
|
||||
match Types.join a.Tast.ty b.Tast.ty with
|
||||
| Some t when not (Types.equal t a.Tast.ty) ->
|
||||
Some (widen a.Tast.loc t a, widen b.Tast.loc t b)
|
||||
| _ -> None
|
||||
|
||||
and join_pair ctx (a : Tast.expr) (y : Ast.expr) (d : Loc.diag) =
|
||||
(* Check y on its own terms to find out whether it was simply the wider
|
||||
operand. This trial is guarded too: if y cannot check without an
|
||||
expectation at all — [None], [(zeroed)] — the original refusal is the one
|
||||
reported, so no form loses the expectation it used to get. *)
|
||||
match trial ctx (fun () -> check ctx y) with
|
||||
| Error _ -> raise (Loc.Error d)
|
||||
| Ok b ->
|
||||
(match join_widen a b with
|
||||
| Some pair -> pair
|
||||
| None -> raise (Loc.Error d))
|
||||
|
||||
and binary ctx ?(dyn_ok = false) ?(join = true) name loc ~want args =
|
||||
match args with
|
||||
@ -7603,18 +7667,22 @@ and binary ctx ?(dyn_ok = false) ?(join = true) name loc ~want args =
|
||||
that has to move. Nothing is checked a third time — the own-terms [b]
|
||||
already in hand is the answer. *)
|
||||
else
|
||||
(match check ctx ~want:a.Tast.ty y with
|
||||
| b' -> a, b'
|
||||
| exception e ->
|
||||
if join && Types.widens_to ~from:a.Tast.ty ~into:b.Tast.ty then
|
||||
widen a.Tast.loc b.Tast.ty a, b
|
||||
else raise e)
|
||||
(match trial ctx (fun () -> check ctx ~want:a.Tast.ty y) with
|
||||
| Ok b' -> a, b'
|
||||
| Error d ->
|
||||
(match
|
||||
if join && reconsiderable d then join_widen a b else None
|
||||
with
|
||||
| Some pair -> pair
|
||||
| None -> raise (Loc.Error d)))
|
||||
end
|
||||
else begin
|
||||
let a = check ctx ?want x in
|
||||
match check ctx ~want:a.Tast.ty y with
|
||||
| b -> a, b
|
||||
| exception e -> if join then join_pair ctx a y e else raise e
|
||||
match trial ctx (fun () -> check ctx ~want:a.Tast.ty y) with
|
||||
| Ok b -> a, b
|
||||
| Error d ->
|
||||
if join && reconsiderable d then join_pair ctx a y d
|
||||
else raise (Loc.Error d)
|
||||
end
|
||||
| _ -> fail loc "%s takes two arguments" name
|
||||
|
||||
|
||||
@ -1208,10 +1208,12 @@ int64_t flan_dyn_need_i64(flan_dyn v) {
|
||||
}
|
||||
|
||||
/* A float, and an int is not one. Refusing the widening is the decision, not
|
||||
* an omission: typed Flan has no implicit widening anywhere — [(print-i64 x)]
|
||||
* used to force an explicit [(i64 x)] at every site — and a boundary that
|
||||
* quietly turned an int into a float would be the one place in the language
|
||||
* where a *value* changed type without anybody writing it down. The dyn
|
||||
* an omission. The typed language does widen an integer into a float, but only
|
||||
* where the float holds every value of it exactly — an i32 into an f64, never
|
||||
* an i64 (FIX.org 2026-09-20). This boundary has no such guarantee to offer:
|
||||
* the box carries one integer width and it is i64, so "an int here" means the
|
||||
* widest one, which is exactly the conversion the typed lattice refuses. The
|
||||
* dyn
|
||||
* *operators* promote, because arithmetic between a 2 and a 2.5 has an obvious
|
||||
* answer and refusing it makes dynamic code worse; the boundary into a typed
|
||||
* f64 parameter does not, because there the annotation is somebody's stated
|
||||
|
||||
@ -112,10 +112,12 @@ flan_dyn flan_dyn_vec_new(void) {
|
||||
/* ── Arithmetic ────────────────────────────────────────────────────── */
|
||||
|
||||
/* Two numbers promote to f64 when either is one, which is the rule a reader
|
||||
* expects of a dynamic language and is not the rule the typed language uses.
|
||||
* The typed language has no implicit widening at all; here there is no
|
||||
* annotation to have been written, so refusing would leave (+ 1 2.5) with no
|
||||
* spelling that works. */
|
||||
* expects of a dynamic language and is still not the rule the typed language
|
||||
* uses. The typed side widens only where nothing can be lost, and an i64 into
|
||||
* an f64 can (FIX.org 2026-09-20), so (+ i64-x 2.5) is written there and is
|
||||
* promoted here. The difference is not an oversight on either side: here there
|
||||
* is no annotation to have been written, so refusing would leave (+ 1 2.5)
|
||||
* with no spelling that works. */
|
||||
static int numeric(cell *c) { return c->tag == T_I64 || c->tag == T_F64; }
|
||||
static double as_f(cell *c) { return c->tag == T_I64 ? (double)c->u.i : c->u.f; }
|
||||
|
||||
|
||||
@ -23,59 +23,59 @@
|
||||
;;;; is built at the wanted width by the literal rule and would never reach a
|
||||
;;;; cast at all.
|
||||
|
||||
(defvar i8-neg i8 -5)
|
||||
(defvar i8-pos i8 127)
|
||||
(defvar i16-neg i16 -300)
|
||||
(defvar i32-neg i32 -2000000000)
|
||||
(defvar i32-one i32 1)
|
||||
(defvar i32-all i32 -1)
|
||||
(defvar u8-max u8 255)
|
||||
(defvar u16-max u16 65535)
|
||||
(defvar u32-big u32 4000000000)
|
||||
(defvar u32-max u32 4294967295)
|
||||
(defvar i64-big i64 5000000000)
|
||||
(defvar f32-half f32 0.5)
|
||||
(defvar w-i8neg i8 -5)
|
||||
(defvar w-i8pos i8 127)
|
||||
(defvar w-i16neg i16 -300)
|
||||
(defvar w-i32neg i32 -2000000000)
|
||||
(defvar w-i32one i32 1)
|
||||
(defvar w-i32all i32 -1)
|
||||
(defvar w-u8max u8 255)
|
||||
(defvar w-u16max u16 65535)
|
||||
(defvar w-u32big u32 4000000000)
|
||||
(defvar w-u32max u32 4294967295)
|
||||
(defvar w-i64big i64 5000000000)
|
||||
(defvar w-f32half f32 0.5)
|
||||
|
||||
;; Widening at a parameter. Each of these is a plain typed function and the
|
||||
;; call sites below hand it a narrower type with no cast written anywhere.
|
||||
(defn take-i64 [x i64] i64 x)
|
||||
(defn take-i16 [x i16] i16 x)
|
||||
(defn take-u64 [x u64] u64 x)
|
||||
(defn take-f64 [x f64] f64 x)
|
||||
(defn take-f32 [x f32] f32 x)
|
||||
(defn w-take-i64 [x i64] i64 x)
|
||||
(defn w-take-i16 [x i16] i16 x)
|
||||
(defn w-take-u64 [x u64] u64 x)
|
||||
(defn w-take-f64 [x f64] f64 x)
|
||||
(defn w-take-f32 [x f32] f32 x)
|
||||
|
||||
;; Widening at a return position: the body is an i32 and the signature is i64.
|
||||
(defn ret-widened [] i64 i32-neg)
|
||||
(defn w-ret-widened [] i64 w-i32neg)
|
||||
|
||||
;; Widening in a binary operator, both orders. The first is the direction
|
||||
;; [expect] already served; the second is the one the join rule added.
|
||||
(defn add-wide-first [] i64 (+ i64-big i32-one))
|
||||
(defn add-narrow-first [] i64 (+ i32-one i64-big))
|
||||
(defn w-add-wide-first [] i64 (+ w-i64big w-i32one))
|
||||
(defn w-add-narrow-first [] i64 (+ w-i32one w-i64big))
|
||||
|
||||
(defn main [args [string]] i32
|
||||
;; ── integer to integer ──────────────────────────────────────────
|
||||
(println (take-i64 i8-neg)) ;; -5
|
||||
(println (take-i64 i8-pos)) ;; 127
|
||||
(println (take-i64 i16-neg)) ;; -300
|
||||
(println (take-i64 i32-all)) ;; -1
|
||||
(println (take-i64 i32-neg)) ;; -2000000000
|
||||
(println (take-i16 u8-max)) ;; 255
|
||||
(println (take-i64 u8-max)) ;; 255
|
||||
(println (take-i64 u16-max)) ;; 65535
|
||||
(println (take-i64 u32-big)) ;; 4000000000
|
||||
(println (take-i64 u32-max)) ;; 4294967295
|
||||
(println (take-u64 u32-big)) ;; 4000000000
|
||||
(println (take-u64 u8-max)) ;; 255
|
||||
(println (w-take-i64 w-i8neg)) ;; -5
|
||||
(println (w-take-i64 w-i8pos)) ;; 127
|
||||
(println (w-take-i64 w-i16neg)) ;; -300
|
||||
(println (w-take-i64 w-i32all)) ;; -1
|
||||
(println (w-take-i64 w-i32neg)) ;; -2000000000
|
||||
(println (w-take-i16 w-u8max)) ;; 255
|
||||
(println (w-take-i64 w-u8max)) ;; 255
|
||||
(println (w-take-i64 w-u16max)) ;; 65535
|
||||
(println (w-take-i64 w-u32big)) ;; 4000000000
|
||||
(println (w-take-i64 w-u32max)) ;; 4294967295
|
||||
(println (w-take-u64 w-u32big)) ;; 4000000000
|
||||
(println (w-take-u64 w-u8max)) ;; 255
|
||||
|
||||
;; ── a widened return ────────────────────────────────────────────
|
||||
(println (ret-widened)) ;; -2000000000
|
||||
(println (w-ret-widened)) ;; -2000000000
|
||||
|
||||
;; ── integer to float, exact only ────────────────────────────────
|
||||
(println (take-f64 i32-neg)) ;; -2000000000.0
|
||||
(println (take-f64 u32-max)) ;; 4294967295.0
|
||||
(println (take-f64 i8-neg)) ;; -5.0
|
||||
(println (take-f32 i16-neg)) ;; -300.0
|
||||
(println (take-f32 u16-max)) ;; 65535.0
|
||||
(println (w-take-f64 w-i32neg)) ;; -2000000000.0
|
||||
(println (w-take-f64 w-u32max)) ;; 4294967295.0
|
||||
(println (w-take-f64 w-i8neg)) ;; -5.0
|
||||
(println (w-take-f32 w-i16neg)) ;; -300.0
|
||||
(println (w-take-f32 w-u16max)) ;; 65535.0
|
||||
|
||||
;; The printer answers %g, which rounds an f64 long before the bits it is
|
||||
;; carrying run out, so the exactness the int-to-float boundary is chosen for
|
||||
@ -83,27 +83,27 @@
|
||||
;; these is the difference between the widened value and the number it is
|
||||
;; supposed to be, and a conversion that lost anything answers something
|
||||
;; other than the last unit.
|
||||
(println (- (take-f64 u32-max) 4294967294.0)) ;; 1
|
||||
(println (- (take-f64 i32-neg) -1999999999.0)) ;; -1
|
||||
(println (- (take-f32 u16-max) 65534.0)) ;; 1
|
||||
(println (- (w-take-f64 w-u32max) 4294967294.0)) ;; 1
|
||||
(println (- (w-take-f64 w-i32neg) -1999999999.0)) ;; -1
|
||||
(println (- (w-take-f32 w-u16max) 65534.0)) ;; 1
|
||||
|
||||
;; ── float to float ──────────────────────────────────────────────
|
||||
(println (take-f64 f32-half)) ;; 0.5
|
||||
(println (w-take-f64 w-f32half)) ;; 0.5
|
||||
|
||||
;; ── the binary join, both operand orders ────────────────────────
|
||||
(println (add-wide-first)) ;; 5000000001
|
||||
(println (add-narrow-first)) ;; 5000000001
|
||||
(println (w-add-wide-first)) ;; 5000000001
|
||||
(println (w-add-narrow-first)) ;; 5000000001
|
||||
;; The narrower operand is the first one, and the sum is an i64 even though
|
||||
;; nothing on this line is annotated.
|
||||
(println (+ i32-neg i64-big)) ;; 3000000000
|
||||
(println (+ w-i32neg w-i64big)) ;; 3000000000
|
||||
;; A comparison joins the same way, and the widened -1 must still be -1.
|
||||
(println (< i32-all i64-big)) ;; true
|
||||
(println (< w-i32all w-i64big)) ;; true
|
||||
;; min and max over two widths answer at the wider one.
|
||||
(println (max i8-neg i16-neg)) ;; -5
|
||||
(println (min i8-neg i32-neg)) ;; -2000000000
|
||||
(println (max w-i8neg w-i16neg)) ;; -5
|
||||
(println (min w-i8neg w-i32neg)) ;; -2000000000
|
||||
;; A count narrower than the value widens to it; the value's width decides.
|
||||
(println (<< i64-big i8-pos)) ;; 0 -- masked to 127 mod 64 = 63
|
||||
(println (<< w-i64big w-i8pos)) ;; 0 -- masked to 127 mod 64 = 63
|
||||
;; An expectation reaches the operands, so this adds at i64 rather than
|
||||
;; wrapping at i32 and widening the sum afterwards.
|
||||
(println (take-i64 (+ i32-neg i32-neg))) ;; -4000000000
|
||||
(println (w-take-i64 (+ w-i32neg w-i32neg))) ;; -4000000000
|
||||
0)
|
||||
|
||||
@ -1009,6 +1009,36 @@ let () =
|
||||
accepts "an unannotated let of a u64 constant still binds a u64"
|
||||
"(defconst fnv u64 0xcbf29ce484222325) \
|
||||
(defn f [] u64 (let [h fnv] (* h 2)))";
|
||||
(* A literal that does not fit is the program's mistake, not a pair of types
|
||||
that failed to meet, so the join must not reconsider it — the operand it
|
||||
would reconsider against is the one the literal was supposed to take its
|
||||
width *from*. Both spellings: the literal written as the operand, and the
|
||||
literal buried in one. *)
|
||||
rejects_check "a literal that does not fit is still refused"
|
||||
"(defvar m u8) (defn f [] u8 (+ m 300))" ~needle:"300 does not fit in u8";
|
||||
rejects_check "and is refused inside an operand too"
|
||||
"(defvar m u8) (defn f [] u8 (+ m (+ 300 1)))"
|
||||
~needle:"300 does not fit in u8";
|
||||
rejects_check "a float literal still cannot stand where an int is wanted"
|
||||
"(defvar n i32) (defn f [] i32 (+ n 1.5))"
|
||||
~needle:"found the float literal 1.5";
|
||||
accepts "a literal that does fit still takes the operand's type"
|
||||
"(defvar m u8) (defn f [] u8 (+ m 200))";
|
||||
|
||||
(* The join reconsiders a refused operand, and a reconsidered pass must leave
|
||||
nothing behind. [scoped] cannot see to that — it puts the scope back on
|
||||
the way out, which an exception does not take — so [binary] snapshots and
|
||||
restores around each trial. Both symptoms of not doing it: a binding that
|
||||
outlives the pass that made it, and the same binding *shadowing* a live
|
||||
one, which is an uninitialised read in a program the compiler accepted. *)
|
||||
rejects_check "an abandoned trial leaves no binding behind"
|
||||
"(defvar n i32) (defvar w i64) \
|
||||
(defn f [] i32 (println (+ n (let [q w] q))) (println q) 0)"
|
||||
~needle:"unknown name q";
|
||||
accepts "and does not shadow the binding it was nested in"
|
||||
"(defvar n i32) (defvar w i64) \
|
||||
(defn f [] i32 (let [t n] (println (+ n (let [t w] t))) (println t)) 0)";
|
||||
|
||||
(* Shifts are the carve-out: the value's type decides and the count widens
|
||||
to it, never the reverse, because the result's width and the poison check
|
||||
both belong to the value. *)
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user