From b8e68a48f7ce4a80ca2cae056292a2bc5935424e Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Sat, 26 Sep 2026 17:45:44 +0700 Subject: [PATCH] A literal local read at T? takes T, None may come first in an if, an Option around an array of Options takes a literal, and a literal refused at T? names the Option. --- lib/check.ml | 55 +++++++++++++++++++++++++++++--------- test/programs/autowrap.fln | 29 ++++++++++++++++++++ test/test_acceptance.ml | 3 ++- test/test_flan.ml | 3 +++ 4 files changed, 77 insertions(+), 13 deletions(-) diff --git a/lib/check.ml b/lib/check.ml index 38a04523..d1816a4a 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -3234,6 +3234,10 @@ let rec literal_arith (e : Ast.expr) : int64 option = over literals alone. *) let lone_literal (e : Ast.expr) = is_literal e || literal_arith e <> None +(* Set for one [check_value] entry: the literal is checked at the Option + itself, not wrapped, so a refusal names the Option (decision 138). *) +let skip_wrap = ref false + (* [None] as written, which has no type until an Option is asked of it. *) let is_none_lit (e : Ast.expr) = match e.Ast.e with Ast.Var "None" -> true | _ -> false @@ -3822,6 +3826,12 @@ let lit_admits kind (t : Types.t) = | `Box, t -> not (Types.equal t Types.Dyn) | _ -> false +(* What a use at [t] says about a literal local: an (Option T) wanted of it + says T, since the local is built at T and then wrapped (decision 138), so + [let w: i64? = x] makes [x] the i64 [let w: i64 = x] does. *) +let rec lit_payload (t : Types.t) = + match t with Types.Option p -> lit_payload p | t -> t + (* The rounds a session may take before its last guesses are checked as they stand. Merging makes two the usual count; the bound only stops a pathological program from looping. *) @@ -6128,19 +6138,26 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr = ctx.tail <- false; let used = ctx.used || List.memq e ctx.kept in ctx.used <- false; + let skipping = !skip_wrap in + skip_wrap := false; match e.Ast.e with (* A literal where an (Option T) is wanted is built at T and then wrapped (decision 138): [s = -1] over an [i64?] is [Some] of an i64 -1. It has no type until one is asked of it, so it is asked the payload's, rather than being built at a default and wrapped at the wrong width. *) | Ast.Int _ | Ast.UInt _ | Ast.Float _ | Ast.Byte _ | Ast.Call _ | Ast.Arr (_ :: _) - when (match want with Some (Types.Option _) -> true | _ -> false) + when (match want with Some (Types.Option _) -> not skipping | _ -> false) && (lone_literal e || (match e.Ast.e with Ast.Arr _ -> true | _ -> false)) -> let w = Option.get want in let t = match w with Types.Option t -> t | _ -> assert false in - let v = check ctx ~want:t e in - if Types.fits ~expected:t ~actual:v.Tast.ty then mk loc w (Tast.Some_ v) - else expect ctx loc ~want v + (match trial ctx (fun () -> check ctx ~want:t e) with + | Ok v when Types.fits ~expected:t ~actual:v.Tast.ty -> mk loc w (Tast.Some_ v) + | Ok v -> expect ctx loc ~want v + (* Refused at T: checked again at the Option as it was before 138, so + the refusal names what was wanted, [str?], and not only its payload. *) + | Error _ -> + skip_wrap := true; + check ctx ?want e) (* A negative literal in a generic body, at an instantiation that made it unsigned. The cast the ordinary refusal names would be wrong at every other type the function is called at, so the fix is one that needs no @@ -6991,18 +7008,19 @@ and var ctx ?(qualified = false) loc ~want name = | Some ({ blit = Some key; _ } as b) when (match ctx.lits, want with | Some s, Some t -> + let t = lit_payload t in s.recording && not !lit_quiet && (Types.equal t Types.Dyn || lit_admits (Option.value (lit_kind key) ~default:`Int) t) | _ -> false) -> - let s = Option.get ctx.lits and t = Option.get want in + let s = Option.get ctx.lits and t = lit_payload (Option.get want) in let operand = List.memq loc !lit_operand_locs in let c = if operand || Types.equal t Types.Dyn then Hint else Up in lit_add s key (c, t, loc); (try expect ctx loc ~want (mk loc b.bty (Tast.Local b.slot)) with Loc.Error _ when lit_kind key <> Some `Box && not operand -> s.dirty <- true; - mk loc t (Tast.Local b.slot)) + expect ctx loc ~want (mk loc t (Tast.Local b.slot))) | Some b -> expect ctx loc ~want (local_of loc b) (* A local of the enclosing function, in a body that was lifted out of it: @@ -8655,8 +8673,11 @@ and check_if_once ctx ~tail ~used ?want loc c t e = let t = branch ctx (fun () -> in_tail (fun () -> check ctx ?want t)) in let e = branch ctx (fun () -> in_tail (fun () -> check ctx ?want e)) in mk loc t.Tast.ty (Tast.If (c, t, e)) - | Some e when want = None && (adapts t || is_none_lit t) - && not (adapts e || is_none_lit e) + | Some e when want = None + && ((adapts t && not (adapts e || is_none_lit e)) + (* [if c then None else 5]: the else arm decides T, and + None meets it at T? below, as the other order does. *) + || (is_none_lit t && not (is_none_lit e))) && not (and_sentinel e) -> (* A literal has no type of its own until something asks, so with no expectation the other arm decides: [(if c 4000000 n)] over an i64 [n] @@ -9841,10 +9862,20 @@ and check_the ctx ~want loc (t : Ast.texpr) (v : Ast.expr) = not agree among themselves — [[1, None]] — is built at the annotation when every element fits it, as [x: [2 i32?] = [1, None]] (decision 138). Nothing is converted: the literal is built at T. *) - && not (match v.Ast.e, ty with - | Ast.Arr _, (Types.Array (_, Types.Option _) | Types.Slice (_, Types.Option _)) -> - probe ctx loc (fun () -> ignore (check ctx ~want:ty v)) <> None - | _ -> false) + && not (let rec holds_option = function + | Types.Option _ -> true + | Types.Array (_, t) | Types.Slice (_, t) -> holds_option t + | _ -> false + in + let rec elems_option = function + | Types.Array (_, t) | Types.Slice (_, t) -> holds_option t + | Types.Option t -> elems_option t + | _ -> false + in + match v.Ast.e with + | Ast.Arr _ when elems_option ty -> + probe ctx loc (fun () -> ignore (check ctx ~want:ty v)) <> None + | _ -> false) then begin let tn = tyname loc ty in let numeric = match ty with Types.Int _ | Types.Float _ -> true | _ -> false in diff --git a/test/programs/autowrap.fln b/test/programs/autowrap.fln index 7b839efb..0db6c6ea 100644 --- a/test/programs/autowrap.fln +++ b/test/programs/autowrap.fln @@ -38,6 +38,8 @@ fn arms(k: i32, x: i32) -> i32? 4 -> x _ -> 0 +fn big(x: i64?) -> i64 = x ?? 0 + fn chain(a: bool, b: bool, opt: i32?) -> Option(i32?) if a 1 @@ -93,6 +95,33 @@ fn main() println(two(kk)) ;; generics println(first(9), first(Some(8)), wrap(3) ?? 0, through(5)) + ;; a literal local takes the payload's type from an Option use, as it + ;; takes T from a T use: each pair prints the same + let la = 4 + let wa: i64? = la + let lb = 4 + let wb: i64 = lb + println(la * 1000000000, lb * 1000000000, wa ?? 0, wb) + let lc = 4 + println(big(lc), lc * 1000000000) + let lf = 7 + let wf: f64? = lf + let lg = 7 + let wg: f64 = lg + println(lf / 2, lg / 2, wf ?? 0.0, wg) + let lu = 200 + let wu: u8? = lu + let lv = 200 + let wv: u8 = lv + println(wu ?? 0, wv) + ;; None first in an if, as in a match + let e1 = if x > 1 then None else 5 + let e2 = if x > 1 then 5 else None + println(e1 ?? -1, e2 ?? -1) + ;; an Option around an array of Options + let ao: [2 i32?]? = [1, None] + let ai = ao! + println(ai[0] ?? 0, ai[1] ?? 0) ;; a narrowed name still takes a payload value let o: i32? = Some(1) if o? diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index 7504b036..09dfbad6 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -2277,7 +2277,8 @@ let () = (* A T where a T? is wanted is Some of it (decision 138). *) ("autowrap.fln", "-1\n5 4 2\n7 8 -1\n3 4\n7\n1 0 4\n5\n2 6 0\n2 -1 -1 2\n4\n-1 3 0\n\ - some some some none\nsome some some none none\nsome some\n9 8 3 5\n10\n"); + some some some none\nsome some some none none\nsome some\n9 8 3 5\n\ + 4000000000 4000000000 4 4\n4 4000000000\n3.5 3.5 7 7\n200 200\n-1 5\n1 0\n10\n"); (* x? tests and narrows, e? as g names what it found (decision 133). *) ("presence.fln", "true false true\n6\n-1\n3\n101 209 0\n11\n42\n2\nabsent\n6\nfalse true\n3\n6\n15\n"); ("presence-dyn.fln", "true false\n103 209 0\nno pet\nann\n3 2\n") ]; (* The pipe (decision 137): chains, multi-line, qualified, dyn, and the diff --git a/test/test_flan.ml b/test/test_flan.ml index b7298b55..0889c686 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -8412,6 +8412,9 @@ let () = rejects_check "a payload that does not fit is refused at the Option" ~needle:"expected (Option i32), found str" "(defn f [] (Option i32) \"no\")\n(defn main [] ())"; + rejects_check "a literal that does not fit is refused at the Option" + ~needle:"expected (Option string), found the integer literal 5" + "(defn f [] (Option string) 5)\n(defn main [] ())"; rejects_check "a narrowing is not wrapped" ~needle:"expected (Option i32), found i64" "(defn f [x i64] (Option i32) x)\n(defn main [] ())"; rejects_check "no wrap inside a container" ~needle:"expected (Vec (Option i32)), found (Vec i32)"