The cast that opens a box, pinned on both backends
This commit is contained in:
parent
10610fb76b
commit
a45e3806af
@ -3730,6 +3730,83 @@ level "1"
|
|||||||
some_nil ~opt:"-O0" ();
|
some_nil ~opt:"-O0" ();
|
||||||
some_nil ~x86:true ();
|
some_nil ~x86:true ();
|
||||||
|
|
||||||
|
(* A numeric cast opening a dyn box — FIX.org 2026-09-20.
|
||||||
|
programs/dyn-cast.flan is one program because the three behaviours are
|
||||||
|
one story told in order: the same-kind casts print, the cross-kind ones
|
||||||
|
print and warn, and the non-numeric box ends the process. The trap is
|
||||||
|
last for the reason [dyn_boundary]'s is — one program, one ending.
|
||||||
|
|
||||||
|
Three things are asserted, and the third is the one that needed the
|
||||||
|
work. First, the numbers: the same-kind casts are pure unboxes, and the
|
||||||
|
cross-kind ones convert the way the same cast converts a typed operand,
|
||||||
|
so (f64 int-box) is 7 and (i64 float-box) is 2 — the truncation toward
|
||||||
|
zero (i64 2.5) already does, not a rounding this feature invented.
|
||||||
|
|
||||||
|
Second, the trap. A bool box is refused by [flan_dyn_cast_kind], which
|
||||||
|
is the decision to mirror the typed parameter boundary rather than to
|
||||||
|
invent a rule: a dyn holding true does not satisfy an i64 parameter
|
||||||
|
today either.
|
||||||
|
|
||||||
|
Third, ONCE PER SITE. The two cross-kind casts in the middle sit inside
|
||||||
|
a [dotimes] that runs eight times, so a per-value warning would put
|
||||||
|
sixteen lines on stderr; what is counted here is three — one for each
|
||||||
|
of the program's three cross-kind cast *sites*, the third being the
|
||||||
|
(f32 int-box) after the loop. That count is the whole reason the
|
||||||
|
runtime carries a table of sites at all: these casts live in frame
|
||||||
|
loops, sand.flan's at 120fps, and a flood is not a diagnostic.
|
||||||
|
|
||||||
|
[run] merges stderr into stdout, so the warnings and the numbers come
|
||||||
|
back in one string and the count is a count over it. *)
|
||||||
|
let dyn_cast_out = "7\n7\n7\n7\n2.5\n2.5\n" in
|
||||||
|
let dyn_cast ?opt ?x86 () =
|
||||||
|
let exe = compile ?opt ?x86 "programs/dyn-cast.flan" in
|
||||||
|
let code, text = run exe None in
|
||||||
|
let name =
|
||||||
|
"dyn: a numeric cast opens the box, and warns once per site"
|
||||||
|
^ (match opt with Some o -> ", " ^ o | None -> "")
|
||||||
|
^ (match x86 with Some true -> ", --x86" | _ -> "")
|
||||||
|
in
|
||||||
|
(* Occurrences of the warning's stable half. Counted rather than
|
||||||
|
matched, because what is being pinned is a number and not a
|
||||||
|
sentence. *)
|
||||||
|
let needle = "warned once for this site" in
|
||||||
|
let warnings =
|
||||||
|
let n = String.length needle and m = String.length text in
|
||||||
|
let c = ref 0 in
|
||||||
|
for i = 0 to m - n do
|
||||||
|
if String.sub text i n = needle then incr c
|
||||||
|
done;
|
||||||
|
!c
|
||||||
|
in
|
||||||
|
if code <> 134
|
||||||
|
|| not (contains text dyn_cast_out)
|
||||||
|
(* The two cross-kind conversions, by their values: 7 -> 7.0 and
|
||||||
|
2.5 -> 2, eight times each. *)
|
||||||
|
|| not (contains text "7\n2\n7\n2\n")
|
||||||
|
|| warnings <> 3
|
||||||
|
|| not (contains text "found a dyn holding an int, and converted it to f64")
|
||||||
|
|| not (contains text "found a dyn holding a float, and converted it to i64")
|
||||||
|
|| not (contains text "found a dyn holding an int, and converted it to f32")
|
||||||
|
(* The non-numeric box, in the runtime's own words. *)
|
||||||
|
|| not (contains text "bool, and a number was wanted")
|
||||||
|
then begin
|
||||||
|
incr failures;
|
||||||
|
Printf.printf
|
||||||
|
"FAIL %s\n got: %S (exit %d, %d warnings)\n wanted: %S, \
|
||||||
|
three warnings, then a trap (exit 134)\n"
|
||||||
|
name text code warnings dyn_cast_out
|
||||||
|
end;
|
||||||
|
(try Sys.remove exe with Sys_error _ -> ())
|
||||||
|
in
|
||||||
|
dyn_cast ();
|
||||||
|
dyn_cast ~opt:"-O0" ();
|
||||||
|
(* The dev daemon's default backend. The parity rule (FIX.org, "x86 tracks
|
||||||
|
LLVM -O0") is what this row is: the same numbers, the same three
|
||||||
|
warnings and the same trap, which is only true because the conversion
|
||||||
|
on each arm is the [Cast] node both backends already lowered rather
|
||||||
|
than arithmetic this feature wrote twice. *)
|
||||||
|
dyn_cast ~x86:true ();
|
||||||
|
|
||||||
(* ── Typed containers into dyn as views, M2 item 3 ────────────────
|
(* ── Typed containers into dyn as views, M2 item 3 ────────────────
|
||||||
programs/dyn-view.flan takes its mode from argv, the way bounds.flan
|
programs/dyn-view.flan takes its mode from argv, the way bounds.flan
|
||||||
does, because a survey and a trap cannot share a process: mode 0 is
|
does, because a survey and a trap cannot share a process: mode 0 is
|
||||||
|
|||||||
@ -1429,6 +1429,36 @@ let () =
|
|||||||
(defn main [] i32\n\
|
(defn main [] i32\n\
|
||||||
\ (match (unbox-opt (box-it 42)) (Some x) (if (= x 42) 0 1) None 1))";
|
\ (match (unbox-opt (box-it 42)) (Some x) (if (= x 42) 0 1) None 1))";
|
||||||
|
|
||||||
|
(* A numeric cast opens a dyn box — FIX.org 2026-09-20. The checker's half
|
||||||
|
is small: every cast name the language has admits a dyn operand now, and
|
||||||
|
that is what these rows are. What the cast then *does* is a run-time
|
||||||
|
question and lives in test_acceptance.ml's dyn-cast rows — the same split
|
||||||
|
as the typed boundary, whose refusal is here and whose trap is there. *)
|
||||||
|
accepts "every numeric cast takes a dyn"
|
||||||
|
"(defn d [] dyn 7)\n\
|
||||||
|
(defn main [] i32\n\
|
||||||
|
\ (do (i64 (d)) (i32 (d)) (i16 (d)) (i8 (d))\n\
|
||||||
|
\ (u64 (d)) (u32 (d)) (u16 (d)) (u8 (d))\n\
|
||||||
|
\ (f64 (d)) (f32 (d))\n\
|
||||||
|
\ 0))";
|
||||||
|
(* And a cast the checker could already see was wrong is wrong for the same
|
||||||
|
reason it was: dyn is admitted by name, not by the numeric test going
|
||||||
|
soft. A string is not a number and never reaches a runtime tag. *)
|
||||||
|
rejects_check "a cast still refuses a non-numeric typed operand"
|
||||||
|
"(defn main [] i32 (i64 \"hi\"))"
|
||||||
|
~needle:"converts a number";
|
||||||
|
(* The *generic* cast — [($t x)] in a body whose signature says
|
||||||
|
[{:where (numeric? $t)}] — is a separate arm in the checker and did not
|
||||||
|
grow a dyn case. It did not need one: the operand's type there is what
|
||||||
|
the bound admits, and [numeric?] does not admit dyn, so a dyn cannot
|
||||||
|
reach that arm to begin with. The refusal is the bound's, at the call
|
||||||
|
that would have instantiated it. *)
|
||||||
|
rejects_check "a generic cast's operand is still what its bound admits"
|
||||||
|
"(defn conv [x $t] $t {:where (numeric? $t)} (t x))\n\
|
||||||
|
(defn d [] dyn 7)\n\
|
||||||
|
(defn main [] i32 (i32 (conv (d))))"
|
||||||
|
~needle:"numeric?";
|
||||||
|
|
||||||
(* The map operations ride the words the typed map already owns: get, put,
|
(* The map operations ride the words the typed map already owns: get, put,
|
||||||
len, has-key? — one question, one word, on both sides. has-key? on a
|
len, has-key? — one question, one word, on both sides. has-key? on a
|
||||||
typed map still checks against its K. *)
|
typed map still checks against its K. *)
|
||||||
@ -1893,8 +1923,16 @@ let () =
|
|||||||
keyword-specific one. *)
|
keyword-specific one. *)
|
||||||
rejects_check "a keyword needs an enum"
|
rejects_check "a keyword needs an enum"
|
||||||
"(defn g [x i32] ()) (defn f [] () (g :space))" ~needle:"is expected here";
|
"(defn g [x i32] ()) (defn f [] () (g :space))" ~needle:"is expected here";
|
||||||
rejects_check "a keyword with no expectation converts as dyn"
|
(* This row used to be a rejection, and the sentence it wanted was the cast
|
||||||
"(defn f [] () (print (i64 :space)))" ~needle:"found dyn";
|
arm's "converts a number, found dyn". FIX.org 2026-09-20 took that
|
||||||
|
refusal away on purpose: a numeric cast opens a dyn box, so [(i64 d)]
|
||||||
|
compiles for every dyn [d] and the question of what the box holds moved
|
||||||
|
to run time. A keyword's box holds no number and traps there —
|
||||||
|
[flan_dyn_cast_kind]'s sentence, the same one a bool's box gets, pinned
|
||||||
|
in test_acceptance.ml's dyn-cast rows. What is left here is that the
|
||||||
|
program is now well-typed, which is the change. *)
|
||||||
|
accepts "a keyword is dyn, and a numeric cast on it is a run-time question"
|
||||||
|
"(defn f [] () (print (i64 :space)))";
|
||||||
rejects_check "a keyword that is not a member"
|
rejects_check "a keyword that is not a member"
|
||||||
"(defenum Key [space 32]) (defn g [k Key] ()) (defn f [] () (g :spcae))"
|
"(defenum Key [space 32]) (defn g [k Key] ()) (defn f [] () (g :spcae))"
|
||||||
~needle:"has no member :spcae";
|
~needle:"has no member :spcae";
|
||||||
|
|||||||
Loading…
x
Reference in New Issue
Block a user