A dyn operand in a fold's first pair keeps the form dyn at a typed want, so only the answer is opened and every position gives the same result.

This commit is contained in:
Joseph Ferano 2026-09-26 17:30:44 +07:00
parent e85ca2c431
commit c60cc33b95
3 changed files with 43 additions and 5 deletions

View File

@ -17212,8 +17212,17 @@ and binary_pair ctx ~dyn_ok ~join ~char_ok loc ~want (x : Ast.expr) (y : Ast.exp
let needs_want (f : Ast.expr) =
is_literal f || (match f.Ast.e with Ast.Kw _ -> true | _ -> false)
in
(* A dyn the want opened is put back: beside a dyn a typed operand gives
dyn (rule 117), so the pair is the dyn runtime's and only its answer
is opened at the want. Opening the operand first made (+ p 1 1) at an
i32 want an i32 add that wraps, where (+ 1 1 p) was a dyn add whose
answer traps at the i32. *)
let reopen (v : Tast.expr) =
if not dyn_ok then v
else match opened_dyn ~box:(to_dyn ctx) v with Some d -> d | None -> v
in
if y_decides then begin
let b = check ctx ?want y in
let b = reopen (check ctx ?want y) in
(* An integer literal before a char, under [+] or [-], is an integer:
the pair is char arithmetic ([char_step]). *)
let a =
@ -17240,7 +17249,7 @@ and binary_pair ctx ~dyn_ok ~join ~char_ok loc ~want (x : Ast.expr) (y : Ast.exp
what [needs_want] settles — a literal still gets the first operand's
type, so [(+ x 1)] over a dyn x goes on building an i64 one. *)
else if dyn_ok && not (needs_want y) then begin
let a = check ctx ?want x in
let a = reopen (check ctx ?want x) in
(* y at [a]'s type first, and on its own terms only if that is
refused: checking it both ways every time made a chain of these
nested in their second operands twice as slow per level. A dyn
@ -17289,7 +17298,7 @@ and binary_pair ctx ~dyn_ok ~join ~char_ok loc ~want (x : Ast.expr) (y : Ast.exp
| None -> raise (Loc.Error d)))
end
else begin
let a = check ctx ?want x in
let a = reopen (check ctx ?want x) in
match trial_at ctx y a.Tast.ty with
| Ok b -> a, b
| Error d ->

View File

@ -60,5 +60,22 @@
(let [r (the i32 0)]
(when (= a "nil-want-first") (set r (+ (the dyn nil) 1 2)))
(when (= a "nil-want-last") (set r (+ 1 2 (the dyn nil))))
(set r (+ r (at-i32 a)))
(println r)))))
0)
;; A dyn beside typed operands at an i32 want: the whole form is dyn, and only
;; its answer is opened at i32, so every position wraps nowhere and traps alike.
(defn at-i32 [a str] i32
(let [big (the dyn 2147483647)
none (the dyn nil)]
(cond
(= a "big-first") (+ big 1 1)
(= a "big-mid") (+ 1 big 1)
(= a "big-last") (+ 1 1 big)
(= a "big-pair") (+ 1 big)
(= a "big-shift") (<< big 1)
(= a "i32-nil-first") (+ none 1 1)
(= a "i32-nil-mid") (+ 1 none 1)
(= a "i32-nil-last") (+ 1 1 none)
:else 0)))

View File

@ -5686,6 +5686,8 @@ level "1"
"programs/dyn-crossing.flan" crossing_out;
let too_big = "dyn: this u64 is 18446744073709551615, above the largest \
dyn int (9223372036854775807), so it has no dyn value" in
let too_wide n =
"dyn: an i32 is wanted here, and the int " ^ n ^ " is outside an i32's range" in
let crossing_traps =
[ "u64", "51:36", too_big;
"u64-max", "52:40", too_big;
@ -5695,8 +5697,18 @@ level "1"
"nil-less", "56:41", "dyn <: int and nil";
"nil-min", "57:40", "dyn min: int and nil";
"nil-bits", "58:41", "dyn bit-or: int and nil";
"nil-want-first", "61:50", "dyn: an i32 is wanted here, and this is nil";
"nil-want-last", "62:46", "dyn +: int and nil, and it takes two numbers — (+ 3 nil)" ]
"nil-want-first", "61:47", "dyn +: nil and int, and it takes two numbers — (+ nil 1)";
"nil-want-last", "62:46", "dyn +: int and nil, and it takes two numbers — (+ 3 nil)";
(* At an i32 want the form is dyn in every position and only its
answer is opened: no position wraps. *)
"big-first", "73:25", too_wide "2147483649";
"big-mid", "74:23", too_wide "2147483649";
"big-last", "75:24", too_wide "2147483649";
"big-pair", "76:24", too_wide "2147483648";
"big-shift", "77:25", too_wide "4294967294";
"i32-nil-first", "78:29", "dyn +: nil and int, and it takes two numbers — (+ nil 1)";
"i32-nil-mid", "79:27", "dyn +: int and nil, and it takes two numbers — (+ 1 nil)";
"i32-nil-last", "80:28", "dyn +: int and nil, and it takes two numbers — (+ 2 nil)" ]
in
List.iter
(fun x86 ->