From c7fb0e54224d681566addea7cb3b28667e0f6f6f Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Sat, 26 Sep 2026 11:14:09 +0700 Subject: [PATCH] Literal locals fed through do, let and if arms share one type without extra rounds, a chain past the rounds names the local to annotate, a restart's conversion fix shows the argument as written, and a name's lookup is answered from the last one under the same scope --- lib/check.ml | 121 ++++++++++++++++++++++++------ runtime/flan_rt.c | 8 +- test/programs/literal-locals.flan | 10 ++- test/programs/restarts.flan | 5 ++ test/test_acceptance.ml | 2 + test/test_flan.ml | 23 ++++++ 6 files changed, 143 insertions(+), 26 deletions(-) diff --git a/lib/check.ml b/lib/check.ml index 4f009b3d..84d38976 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -1020,7 +1020,21 @@ let bind ctx ?what ?lit name bty ~assignable = ctx.scope <- (name, { slot; bty; assignable; bwhat = what; blit = lit }) :: ctx.scope; slot -let lookup ctx name = List.assoc_opt name ctx.scope +(* The last answer for each name, with the scope it was read from. A body is + checked under one scope for long stretches and names the same local + several times per form, so compared by identity this answers most + lookups without walking a scope that, in a long [let], holds thousands of + names. *) +let lookup_cache : (string, (string * binding) list * binding option) Hashtbl.t = + Hashtbl.create 64 + +let lookup ctx name = + match Hashtbl.find_opt lookup_cache name with + | Some (sc, r) when sc == ctx.scope -> r + | _ -> + let r = List.assoc_opt name ctx.scope in + Hashtbl.replace lookup_cache name (ctx.scope, r); + r (* Capture, spec-memory.md's case 2: a body lifted into a function of its own — an [fn] literal or a handler clause — naming a local of the function it was @@ -6089,11 +6103,11 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr = integer type, since the real one is answered again per copy. A local of the same name shadows it. *) | Ast.Var name - when (not (List.mem_assoc name ctx.scope)) - && (List.mem name ctx.env.lenvars - || (match List.assoc_opt name ctx.env.subst with - | Some (Types.Len _) -> true - | _ -> false)) -> + when (List.mem name ctx.env.lenvars + || (match List.assoc_opt name ctx.env.subst with + | Some (Types.Len _) -> true + | _ -> false)) + && lookup ctx name = None -> let n = match List.assoc_opt name ctx.env.subst with | Some (Types.Len n) -> n @@ -6425,7 +6439,16 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr = let t = Printf.sprintf "%g" x in if String.exists (fun c -> c = '.' || c = 'e' || c = 'n' || c = 'i') t then t else t ^ ".0" - | _ -> spell_arg "x" a + | _ -> + (* The argument as written, when it is on one line of a file the + checker can read; otherwise an ellipsis. *) + let l = a.Ast.loc in + match Loc.source_line l with + | Some line + when l.Loc.macro = None && l.Loc.eline = l.Loc.line && l.Loc.col >= 1 + && l.Loc.ecol > l.Loc.col && l.Loc.ecol - 1 <= String.length line -> + String.sub line (l.Loc.col - 1) (l.Loc.ecol - l.Loc.col) + | _ -> spell_arg "\u{2026}" a in String.concat "\x1f" (sg :: (if fln_source loc then "i" else "p") :: List.map spell written) @@ -7420,19 +7443,37 @@ and lit_recorded ctx n = locals are merged with whatever [v] is stored into and the others are what it brings. *) and lit_parts ctx (v : Ast.expr) = - let rec go (v : Ast.expr) (vars, others) = + (* [env]: names a [let] inside [v] binds, with what they were bound to, so + (let [t a0] t) passes a0 through as (do a0) and an if's arms do. *) + let rec go env (v : Ast.expr) (vars, others) = match v.Ast.e with | Ast.Var n -> - (match lookup ctx n with - | Some { blit = Some k; _ } when lit_kind k <> Some `Box -> (k :: vars, others) - | _ -> (vars, v :: others)) + (match List.assoc_opt n env with + | Some (Some (vs, os)) -> (vs @ vars, os @ others) + | Some None -> (vars, v :: others) + | None -> + match lookup ctx n with + | Some { blit = Some k; _ } when lit_kind k <> Some `Box -> (k :: vars, others) + | _ -> (vars, v :: others)) | Ast.Int _ | Ast.Float _ | Ast.Byte _ -> (vars, others) | Ast.Call ({ Ast.e = Ast.Var ("+" | "-" | "*" | "/" | "%" | "min" | "max"); _ }, args) when args <> [] -> - List.fold_left (fun acc a -> go a acc) (vars, others) args + List.fold_left (fun acc a -> go env a acc) (vars, others) args + | Ast.Do (_ :: _ as xs) -> go env (List.nth xs (List.length xs - 1)) (vars, others) + | Ast.Let (bs, (_ :: _ as xs)) -> + let env = + List.fold_left + (fun env (b : Ast.binding) -> + (b.Ast.bname, + if b.Ast.bty = None then Some (go env b.Ast.bval ([], [])) else None) + :: env) + env bs + in + go env (List.nth xs (List.length xs - 1)) (vars, others) + | Ast.If (_, t, Some e) -> go env e (go env t (vars, others)) | _ -> (vars, v :: others) in - go v ([], []) + go [] v ([], []) (* A float literal, or an integer one past i32, anywhere in [v]'s arithmetic. *) and lit_wide_literals (v : Ast.expr) = @@ -7528,22 +7569,23 @@ and with_lits : 'a. ctx -> Loc.t -> Ast.expr list -> (unit -> 'a) -> 'a = if !lit_depth = 0 then Phys.reset lit_memo) @@ fun () -> let unsettled = Loc.diag ~kind:"check/lit-unsettled" loc "unsettled" in - (* The decisions the uses recorded so far make, and whether any moved. *) + (* The decisions the uses recorded so far make, written into + [s.decided], and the locals whose decision moved. *) let settle () = let solved = lit_solve s in - let moved = ref false in + let moved = ref [] in List.iter - (fun (k, _, r) -> + (fun (k, name, r) -> match r with | Ok t -> let kind = Option.value (lit_kind k) ~default:`Int in if not (Types.equal t (lit_guess ~subst:ctx.env.subst s k kind)) then begin - moved := true; + moved := (k, name, t) :: !moved; Phys.replace s.decided k t end | Error _ -> ()) solved; - (solved, !moved) + (solved, List.rev !moved) in let conflict solved = List.find_map @@ -7567,6 +7609,9 @@ and with_lits : 'a. ctx -> Loc.t -> Ast.expr list -> (unit -> 'a) -> 'a = incr lit_recording; (* A ref, because [trial] is monomorphic inside this recursive group. *) let answer = ref None in + (* What the settle inside the trial found, which has already written + its decisions: settling again outside would see nothing move. *) + let settled = ref None in let outcome = Fun.protect ~finally:(fun () -> decr lit_recording; s.recording <- false) @@ -7574,8 +7619,9 @@ and with_lits : 'a. ctx -> Loc.t -> Ast.expr list -> (unit -> 'a) -> 'a = trial ctx (fun () -> let r = run () in let solved, moved = settle () in + settled := Some (solved, moved); (* The guesses held: this check is the answer. *) - if moved || s.dirty || conflict solved <> None then + if moved <> [] || s.dirty || conflict solved <> None then raise (Loc.Error unsettled); answer := Some r; poison loc)) @@ -7583,11 +7629,19 @@ and with_lits : 'a. ctx -> Loc.t -> Ast.expr list -> (unit -> 'a) -> 'a = match outcome, !answer with | Ok _, Some r -> log (); remember (); r | _ -> - let solved, moved = settle () in + let solved, moved = + match !settled with Some sm -> sm | None -> settle () + in (match conflict solved with | Some (k, name, ((t1, l1), (t2, l2))) -> lit_conflict k name t1 l1 t2 l2 | None -> ()); - if moved && n < lit_rounds then round (n + 1) + if moved <> [] && n < lit_rounds then round (n + 1) + else if moved <> [] then begin + (* Still moving: a local fed through more calls than the rounds + follow. It is the local that needs its type written. *) + let k, name, t = List.hd moved in + lit_unsettled k name t + end else begin (* Nothing left to learn: checked for real, so a refusal is the ordinary one and a whole-file check goes on past it. *) @@ -7599,6 +7653,31 @@ and with_lits : 'a. ctx -> Loc.t -> Ast.expr list -> (unit -> 'a) -> 'a = round 1 end +(* A literal local whose uses kept changing its type past [lit_rounds]. *) +and lit_unsettled (k : Ast.expr) name t = + let lit = lit_spelling k in + let fix = + if fln_source k.Ast.loc then Printf.sprintf "let %s: %s = %s" name (tyname k.Ast.loc t) lit + else Printf.sprintf "(%s %s)" (tyname k.Ast.loc t) lit + in + Loc.failk "check/literal-unsettled" k.Ast.loc + "the type of %s depends on too long a chain of the values stored into it \ + to be read off them. Write the type it should have: %s" + name fix + +and lit_spelling (k : Ast.expr) = + let lit = + match k.Ast.e with + | Ast.Int n -> Int64.to_string n + | Ast.Float x -> Printf.sprintf "%g" x + | Ast.Byte b -> Printf.sprintf "\\%c" (Char.chr b) + | Ast.Call (_, [ { Ast.e = Ast.Int n; _ } ]) -> Int64.to_string (Int64.neg n) + | Ast.Call (_, [ { Ast.e = Ast.Float x; _ } ]) -> Printf.sprintf "%g" (-.x) + | _ -> "..." + in + let whole = lit <> "" && String.for_all (fun c -> (c >= '0' && c <= '9') || c = '-') lit in + if whole && lit_kind k = Some `Float then lit ^ ".0" else lit + (* Two uses of a literal local that no one type satisfies. *) and lit_conflict (k : Ast.expr) name t1 l1 t2 l2 = let lit = diff --git a/runtime/flan_rt.c b/runtime/flan_rt.c index c48f6f39..57c35edf 100644 --- a/runtime/flan_rt.c +++ b/runtime/flan_rt.c @@ -1193,10 +1193,14 @@ _Noreturn void flan_restart_args_fail(const uint8_t *loc, int64_t loclen, if (wrote < 0 || (size_t)wrote >= sizeof fix - used) { ok = 0; break; } used += (size_t)wrote; } + /* An argument the compiler could not spell is an ellipsis, and a fix with + * a hole in it is a conversion to make, not code to paste. */ + int holed = strstr(fix, "\xe2\x80\xa6") != NULL; if (ok && used > 0) - flan_say(loc, loclen, "restart %.*s takes %.*s, given %.*s. Write %s", + flan_say(loc, loclen, "restart %.*s takes %.*s, given %.*s. %s %s", (int)namelen, (const char *)name, (int)wantlen, (const char *)want, - (int)plen[0], (const char *)part[0], fix); + (int)plen[0], (const char *)part[0], + holed ? "Convert the argument with" : "Write", fix); else flan_say(loc, loclen, "restart %.*s takes %.*s, given %.*s", (int)namelen, (const char *)name, (int)wantlen, (const char *)want, (int)plen[0], diff --git a/test/programs/literal-locals.flan b/test/programs/literal-locals.flan index 69bef99a..71aefc48 100644 --- a/test/programs/literal-locals.flan +++ b/test/programs/literal-locals.flan @@ -30,10 +30,14 @@ (set a b) a)) -;; recur rebinds a loop's names the way set does. +;; Two locals fed from each other: i is counted against an i64, and acc +;; sums a literal past i32. (defn sum-to [n i64] i64 - (loop [i 0 acc 0] - (if (< i n) (recur (+ i 1) (+ acc 1000000000)) acc))) + (let [i 0 acc 0] + (while (< i n) + (set acc (+ acc 1000000000)) + (set i (+ i 1))) + acc)) ;; Inside a generic body the literal takes the type variable. (defn sum-of [xs [$t]] $t {:where (numeric? $t)} diff --git a/test/programs/restarts.flan b/test/programs/restarts.flan index b8adc4a5..cc799dc5 100644 --- a/test/programs/restarts.flan +++ b/test/programs/restarts.flan @@ -106,6 +106,10 @@ (handler-bind [(AssetMissing [c] (let [big (i64 7)] (invoke-restart 'use-value big)))] (supplied n))) +(defn doubled [n i32] i32 + (handler-bind [(AssetMissing [c] (let [big (i64 7)] (invoke-restart 'use-value (* big 2))))] + (supplied n))) + (defn main [args [str]] i32 ;; One argument selects a trap; none runs the table's case. (if (> (length args) 1) @@ -116,6 +120,7 @@ (= k 3) (print (overfull 92)) (= k 4) (print (mislaid 93)) (= k 5) (print (widened 94)) + (= k 6) (print (doubled 95)) :else (println "?")) (return 0))) diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index 311499d3..ea7a24e6 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -1402,6 +1402,8 @@ let () = "restart use-value takes (str), given (i32)"; refuses "a number of another type is refused with its conversion" "5" "restart use-value takes (i32), given (i64). Write (i32 big)"; + refuses "and the argument as it was written when it is an expression" "6" + "restart use-value takes (i32), given (i64). Write (i32 (* big 2))"; (try Sys.remove exe with Sys_error _ -> ()) in restart_mismatch (); diff --git a/test/test_flan.ml b/test/test_flan.ml index 4e7e2beb..e3b9fa9a 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -1105,6 +1105,29 @@ let () = ~needle:"1e-50 is too small for f32, which rounds it to 0" "(defn f [] f32 1e-50)"; infers "a literal past f32's range is an f64 like any other" "(+ 1.0 1e300)" "f64"; + (* Chains through a second round, and through do, let and if arms that + merge without one. *) + accepts "a literal local fed through do, however long the chain" + "(defn f [x i64] i64 (let [a0 0 a1 0 a2 0 a3 0 a4 0 a5 0 a6 0 a7 0 a8 0 a9 0 a10 0 \ + a11 0 a12 0] (set a0 x) (set a1 (do a0)) (set a2 (do a1)) (set a3 (do a2)) \ + (set a4 (do a3)) (set a5 (do a4)) (set a6 (do a5)) (set a7 (do a6)) \ + (set a8 (do a7)) (set a9 (do a8)) (set a10 (do a9)) (set a11 (do a10)) \ + (set a12 (do a11)) a12))"; + accepts "a literal local fed through a let" + "(defn f [x i64] i64 (let [a0 0 a1 0 a2 0] (set a0 x) (set a1 (let [t a0] t)) \ + (set a2 (let [t a1] t)) a2))"; + accepts "a literal local fed through both arms of an if" + "(defn f [x i64] i64 (let [a0 0 a1 0] (set a0 x) (set a1 (if true a0 a0)) a1))"; + accepts "a literal local fed through a generic call settles in rounds" + "(defn same [x $t] $t x) (defn f [x i64] i64 (let [a0 0 a1 0 a2 0] (set a0 x) \ + (set a1 (same a0)) (set a2 (same a1)) a2))"; + rejects_check "a chain the rounds cannot follow names the local to annotate" + ~needle:"the type of a7 depends on too long a chain of the values stored into \ + it to be read off them. Write the type it should have: (i64 0)" + "(defn same [x $t] $t x) (defn f [x i64] i64 (let [a0 0 a1 0 a2 0 a3 0 a4 0 a5 0 \ + a6 0 a7 0 a8 0 a9 0 a10 0] (set a0 x) (set a1 (same a0)) (set a2 (same a1)) \ + (set a3 (same a2)) (set a4 (same a3)) (set a5 (same a4)) (set a6 (same a5)) \ + (set a7 (same a6)) (set a8 (same a7)) (set a9 (same a8)) (set a10 (same a9)) a10))"; rejects_check "two uses of a literal local disagree" ~needle:"x is used as u32 and as i32, and 0 can have only one type. \ Write the one it should have: (u32 0)"