From c60cc33b9516f8f2c1a9c4dece82cc2c6d7aefcd Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Sat, 26 Sep 2026 17:30:44 +0700 Subject: [PATCH] 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. --- lib/check.ml | 15 ++++++++++++--- test/programs/dyn-crossing.flan | 17 +++++++++++++++++ test/test_acceptance.ml | 16 ++++++++++++++-- 3 files changed, 43 insertions(+), 5 deletions(-) diff --git a/lib/check.ml b/lib/check.ml index c6acece6..84dd80ba 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -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 -> diff --git a/test/programs/dyn-crossing.flan b/test/programs/dyn-crossing.flan index 4b80b47c..def9fecb 100644 --- a/test/programs/dyn-crossing.flan +++ b/test/programs/dyn-crossing.flan @@ -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))) diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index 045f1acd..c10ec35e 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -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 ->