From ff0679cbb15f8e616afd438aebeeefefe49c14de Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Fri, 25 Sep 2026 22:14:06 +0700 Subject: [PATCH] An if's else arm is checked once and brought to the join, an abandoned check undoes only what it wrote, and an arm refused at the join says why at its value --- lib/check.ml | 234 ++++++++++++++++++++++++++++------------------ test/test_flan.ml | 63 +++++++++++++ 2 files changed, 206 insertions(+), 91 deletions(-) diff --git a/lib/check.ml b/lib/check.ml index bbc78dd1..0defb97b 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -34,6 +34,12 @@ let fail = Loc.fail language from the one the author decided on. *) let literal_at_want = "check/literal-at-want" +(* A refusal that is two types failing to meet, a literal's included: what + an arm checked at another arm's type says when the two simply differ. *) +let is_mismatch (d : Loc.diag) = + String.equal d.Loc.kind "check/type-mismatch" + || String.equal d.Loc.kind literal_at_want + (* [List.map]'s evaluation order is unspecified, and checking allocates frame slots as a side effect. Left-to-right is required, not a preference: a later let binding sees an earlier one, and slot numbering must be reproducible. *) @@ -121,6 +127,35 @@ type gstruct = { program asks for the copy itself. *) let struct_apps : (string, string * Types.t list) Hashtbl.t = Hashtbl.create 16 +(* The undo journal a check that may be abandoned writes into: every table + write a body's check makes goes through [jreplace]/[jremove]/[jset], which + note how to take it back while a [snapshot_env] is open. So abandoning a + check costs what it wrote, not the size of the tables it could have. *) +let journal : (unit -> unit) list ref = ref [] +let journal_open = ref 0 + +let jot undo = if !journal_open > 0 then journal := undo :: !journal + +let jreplace tbl k v = + (if !journal_open > 0 then + let old = Hashtbl.find_opt tbl k in + jot (fun () -> + match old with + | Some o -> Hashtbl.replace tbl k o + | None -> Hashtbl.remove tbl k)); + Hashtbl.replace tbl k v + +let jremove tbl k = + (if !journal_open > 0 then + match Hashtbl.find_opt tbl k with + | Some o -> jot (fun () -> Hashtbl.replace tbl k o) + | None -> ()); + Hashtbl.remove tbl k + +let jset r v = + (if !journal_open > 0 then let old = !r in jot (fun () -> r := old)); + r := v + (* The length every length variable has inside a generic body's abstract pass. Large so that no constant index into such an array is refused as out of bounds there, and within i32 so that [(length a)] is an ordinary index. @@ -364,25 +399,25 @@ let new_env () = { guard_next = false; } -(* Everything checking may write into [env], taken so that a check which is - abandoned — a trial, a probe, a return type read and thrown away, a - tolerated body — can be undone as one piece. Partial undo is the bug this +(* A check that may be abandoned — a trial, a probe, a return type read and + thrown away, a tolerated body — opens one of these: [undo] puts back + everything it wrote into [env], [keep] closes it and leaves the writes, + which an enclosing one can still undo. Partial undo is the bug this exists for: rewinding [lifted] and not the generic cache left a copy made during a trial with the lambda it lifted gone, which is a link error. So the whole record is named, closed with warning 9: a new field stops this compiling until it is decided here. - Taken on every trial, so it copies only what a body's check writes: the - struct table and its locations (a generic struct's copy, a closure's - environment), the struct-copy tables, and the generic cache, whose copies' - entries in [fns] are the only ones a body adds. The rest is written by the - declaration passes alone, before any body is checked, and is marked so. *) -let snapshot_env env : unit -> unit = - let[@warning "+9"] { structs; locs; copies; insts; lifted; instances; - tyvars; subst; tvpreds; chain; deferred; lenvars; - len_placeholder; schain; in_field; recovering; - recovered; poison; speculating; guard_next; - fns = _ (* through [insts], below *); + The tables a body's check writes go through the journal ([jreplace]); + the lists and flags are held here, which costs nothing; the rest is + written by the declaration passes alone, before any body is checked. *) +let snapshot_env env : (unit -> unit) * (unit -> unit) = + let[@warning "+9"] { lifted; instances; tyvars; subst; tvpreds; chain; + deferred; lenvars; len_placeholder; schain; in_field; + recovering; recovered; poison; speculating; + guard_next; + (* Journaled at their writes. *) + structs = _; locs = _; copies = _; insts = _; fns = _; (* Declaration passes only. *) datas = _; unions = _; cases = _; aliases = _; consts = _; enums = _; parents = _; externs = _; @@ -391,29 +426,22 @@ let snapshot_env env : unit -> unit = generics = _; gsigs = _; refused_generics = _; gstructs = _; broken = _; glens = _; classes = _; tracks = _; inferred = _; infer_failed = _ } = env in - let keep t = - let c = Hashtbl.copy t in - fun () -> Hashtbl.reset t; Hashtbl.iter (Hashtbl.add t) c + incr journal_open; + let mark = !journal in + let close () = + decr journal_open; + if !journal_open = 0 then journal := [] in - let tables = [ keep structs; keep locs; keep copies; keep struct_apps ] in - let cache = Hashtbl.fold (fun g r acc -> (g, r, !r) :: acc) insts [] in - fun () -> - List.iter (fun undo -> undo ()) tables; - (* A copy made since goes from [fns] with its cache entry. *) - Hashtbl.filter_map_inplace - (fun g r -> - match List.find_opt (fun (h, _, _) -> String.equal g h) cache with - | None -> - List.iter (fun (_, _, sym) -> Hashtbl.remove env.fns sym) !r; - None - | Some (_, _, before) -> - List.iter - (fun ((_, _, sym) as e) -> - if not (List.memq e before) then Hashtbl.remove env.fns sym) - !r; - r := before; - Some r) - insts; + let undo () = + let rec back l = + if l != mark then + match l with + | u :: rest -> u (); back rest + | [] -> () + in + back !journal; + journal := mark; + close (); env.lifted <- lifted; env.instances <- instances; env.tyvars <- tyvars; env.subst <- subst; env.tvpreds <- tvpreds; env.chain <- chain; env.deferred <- deferred; env.lenvars <- lenvars; @@ -421,6 +449,8 @@ let snapshot_env env : unit -> unit = env.in_field <- in_field; env.recovering <- recovering; env.recovered <- recovered; env.poison <- poison; env.speculating <- speculating; env.guard_next <- guard_next + in + (undo, close) (* A refusal [collect] can go on past: kept while a whole-file check is collecting, in the order found, and raised otherwise. *) @@ -1469,7 +1499,7 @@ let struct_app g args = args) in if not (Hashtbl.mem struct_apps key) then begin - Hashtbl.replace struct_apps key (g, args); + jreplace struct_apps key (g, args); Hashtbl.replace Types.display key (Printf.sprintf "(%s %s)" g (String.concat " " (List.map Types.to_string args))) @@ -1710,8 +1740,8 @@ and struct_copy ?(at_definition = false) env loc name targs = let key = struct_app name targs in if Hashtbl.mem env.copies key then key else if Hashtbl.mem env.broken name then begin - Hashtbl.replace env.copies key (List.exists generic_arg targs); - Hashtbl.replace env.structs key { Tast.sname = key; fields = [] }; + jreplace env.copies key (List.exists generic_arg targs); + jreplace env.structs key { Tast.sname = key; fields = [] }; key end else begin @@ -1745,9 +1775,9 @@ and struct_copy ?(at_definition = false) env loc name targs = let generic = List.exists generic_arg targs in (* In before its fields, so a field that names the same copy through a pointer — [(defstruct Node [next (Ptr (Node $t))])] — finds it. *) - Hashtbl.replace env.copies key generic; - Hashtbl.replace env.structs key { Tast.sname = key; fields = [] }; - Hashtbl.replace env.locs key g.gloc; + jreplace env.copies key generic; + jreplace env.structs key { Tast.sname = key; fields = [] }; + jreplace env.locs key g.gloc; let saved = (env.subst, env.tyvars, env.lenvars, env.tvpreds, env.len_placeholder, env.in_field, env.schain) @@ -1775,13 +1805,13 @@ and struct_copy ?(at_definition = false) env loc name targs = with | fields -> restore (); - Hashtbl.replace env.structs key { Tast.sname = key; fields }; + jreplace env.structs key { Tast.sname = key; fields }; finite_from env key; key | exception e -> restore (); - Hashtbl.remove env.copies key; - Hashtbl.remove env.structs key; + jremove env.copies key; + jremove env.structs key; (* A field refused inside the template says nothing about which use asked for this copy; the note names it, one per level of copies. *) (match e with @@ -3011,7 +3041,7 @@ let close_over ~fname (octx : ctx) (fctx : ctx) loc = (fun (n, ((b : binding), _)) -> { Tast.fname = n; fty = b.bty }) caught in - Hashtbl.replace fctx.env.structs ename { Tast.sname = ename; fields }; + jreplace fctx.env.structs ename { Tast.sname = ename; fields }; let ety = Types.Named ename in let eslot = fresh_slot fctx (Types.Ptr (Types.Mut, ety)) in let binds = @@ -7367,47 +7397,42 @@ and check_if_once ctx ~tail ?want loc c t e = is checked once; a refused one re-checks each level below the refusal once more, the square of its depth. *) (* The else arm on its own terms, when nothing is wanted: the two arms - meet at [arm_join], so the order they are written in decides nothing. - Kept when it has the then arm's type, or when the then arm is the one - that moves; when the else arm moves it is checked again below at the - then arm's type, so its literals are typed there as before. *) + meet at [arm_join], so the order they are written in decides nothing, + and both are brought to the join as checked — the arm is never checked + twice, which in a chain of ifs would be twice per level. *) let joined = if want <> None || free_join || t.Tast.ty = Types.Never || t.Tast.ty = Types.Bool || and_sentinel e || lone_literal e then None else - (* A trial not kept leaves nothing: [trial] puts the context and - the environment back when it raises. *) - let not_kept = "check/arm-not-kept" in let alone () = branch ctx (fun () -> in_tail (fun () -> check ctx e)) in - match - trial ctx (fun () -> - let v = alone () in - match arm_join t.Tast.ty v.Tast.ty with - | Some j when Types.equal v.Tast.ty j -> v - | _ -> raise (Loc.Error (Loc.diag ~kind:not_kept v.Tast.loc ""))) - with - | Ok v -> Some (v.Tast.ty, v) - | Error d when String.equal d.Loc.kind not_kept -> None - | Error _ -> - (* Refused on its own terms. If the then arm's type is what it - needed — [nil], a bare struct — the arm is checked at it below; - if it is refused there too, its own error is the real one, so it - is checked for real on its own terms and nothing is invented - about a type it was never going to have. *) + match trial ctx alone with + | Ok v -> + (match arm_join t.Tast.ty v.Tast.ty with + | Some j -> Some (j, expect ctx v.Tast.loc ~want:(Some j) v) + (* No join: the refusal [if] gives its else arm. *) + | None -> + Some (t.Tast.ty, expect ctx v.Tast.loc ~want:(Some t.Tast.ty) v)) + | Error own -> + (* Refused on its own terms. The then arm's type may be what it + needed — [nil], a bare struct — and it is checked at it below, + whose refusal is then the one said. Only when that refusal is a + mismatch and the arm's own is not — an unknown name, say — is + the arm's own error the real one, so nothing is invented about a + type it was never going to have. *) (match trial ctx (fun () -> branch ctx (fun () -> in_tail (fun () -> check ctx ~want:t.Tast.ty e))) with - | Ok _ -> None - | Error _ -> + | Error d + when is_mismatch d && not (is_mismatch own) -> let v = alone () in (match arm_join t.Tast.ty v.Tast.ty with | Some j -> Some (j, expect ctx v.Tast.loc ~want:(Some j) v) | None -> - fail loc "the branches of this if have different types: %s and %s" - (Types.to_string t.Tast.ty) (Types.to_string v.Tast.ty))) + Some (t.Tast.ty, expect ctx v.Tast.loc ~want:(Some t.Tast.ty) v)) + | _ -> None) in match joined with | Some (j, v) -> @@ -8878,12 +8903,16 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms = let at w () = block ctx ?want:w a.Ast.aloc a.Ast.body in match trial ctx (at None) with | Ok b -> b - | Error _ -> - (* Refused on its own terms: the join is what it needed, - or, refused there too, its own error is the real one. *) + | Error own -> + (* Refused on its own terms: the join may be what it + needed, and its refusal at the join is then the one + said — unless that refusal is a mismatch and the arm's + own is not, when the arm's own error is the real one. *) (match trial ctx (at !want) with - | Ok _ -> at !want () - | Error _ -> at None ()) + | Error d + when is_mismatch d && not (is_mismatch own) -> + at None () + | _ -> at !want ()) else block ctx ?want:!want a.Ast.aloc a.Ast.body in (if body.Tast.ty <> Types.Never then @@ -8900,11 +8929,32 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms = let checked = match free, !want with | true, Some j -> + (* Said at the arm's value, its last form, as a refusal checked at the + join would have been — not at its pattern. *) + let rec value (x : Ast.expr) = + match x.Ast.e with + | Ast.Do (_ :: _ as xs) | Ast.Let (_, (_ :: _ as xs)) -> + value (List.hd (List.rev xs)) + | _ -> x.Ast.loc + in + let value_loc i = + let (a : Ast.arm), _, _ = List.nth resolved i in + match List.rev a.Ast.body with + | x :: _ -> value x + | [] -> a.Ast.aloc + in + (* Each arm refused on its own, so every arm that cannot meet the join + is said, as each would be checked at it. *) List.map (fun (i, (arm : Tast.arm)) -> match arm.Tast.abody with | [ b ] when not (Types.equal b.Tast.ty j || b.Tast.ty = Types.Never) -> - (i, { arm with Tast.abody = [ expect ctx b.Tast.loc ~want:(Some j) b ] }) + let at = value_loc i in + let b = + try expect ctx at ~want:(Some j) b + with Loc.Error d -> refuse_or_poison ctx.env at d + in + (i, { arm with Tast.abody = [ b ] }) | _ -> (i, arm)) checked | _ -> checked @@ -13346,7 +13396,7 @@ and instantiate env loc gname vars subst cparams cret = let cache = match Hashtbl.find_opt env.insts gname with | Some r -> r - | None -> let r = ref [] in Hashtbl.replace env.insts gname r; r + | None -> let r = ref [] in jreplace env.insts gname r; r in let same (ps, r, _) = List.length ps = List.length cparams @@ -13392,8 +13442,8 @@ and instantiate env loc gname vars subst cparams cret = (* The entry goes in *before* the body is checked, which is what makes a recursive generic function terminate: the call to itself at the same types finds this and does not generate a second copy. *) - cache := (cparams, cret, sym) :: !cache; - Hashtbl.replace env.fns sym (cparams, cret); + jset cache ((cparams, cret, sym) :: !cache); + jreplace env.fns sym (cparams, cret); let saved_subst = env.subst and saved_vars = env.tyvars and saved_preds = env.tvpreds and saved_chain = env.chain in (* Inside the copy there are no variables left: [resolve_name] answers @@ -13481,8 +13531,8 @@ and instantiate env loc gname vars subst cparams cret = (* A copy whose body did not check is not a copy. Both entries go back out, so a second call at the same types is the same refusal again rather than a cache hit on a function that does not exist. *) - cache := List.filter (fun (_, _, s) -> s <> sym) !cache; - Hashtbl.remove env.fns sym; + jset cache (List.filter (fun (_, _, s) -> s <> sym) !cache); + jremove env.fns sym; raise e in env.instances <- tfn :: env.instances; @@ -13583,9 +13633,9 @@ and trial ctx f = outer_what; caught; place_ok; envslot; parent = _; in_frames; loops; tail; in_defer; owner = _ } = ctx in - let undo = snapshot_env ctx.env in + let undo, keep = snapshot_env ctx.env in match speculate ctx.env f with - | r -> Ok r + | r -> keep (); Ok r | exception Loc.Error d -> undo (); ctx.slots <- slots; ctx.slot_tys <- slot_tys; @@ -13596,6 +13646,7 @@ and trial ctx f = ctx.caught <- caught; ctx.place_ok <- place_ok; ctx.envslot <- envslot; ctx.loops <- loops; ctx.tail <- tail; ctx.in_defer <- in_defer; Error d + | exception e -> keep (); raise e (* Whether the trial's refusal is one worth reconsidering. A literal that did not fit is not, and neither is a refusal a program cannot make any use of @@ -15147,9 +15198,9 @@ and check_generic env (fn : Ast.fn) = [env.tvpreds] whether the variable was declared to support it, and every instantiation asks the concrete type the same question again. *) env.tvpreds <- fn.Ast.fwhere; - Hashtbl.replace env.fns fn.Ast.name (params, ret); + jreplace env.fns fn.Ast.name (params, ret); let finish () = - Hashtbl.remove env.fns fn.Ast.name; + jremove env.fns fn.Ast.name; env.lifted <- saved_lifted; env.tyvars <- saved_vars; env.tvpreds <- saved_preds; @@ -15186,7 +15237,7 @@ and read_return env (fn : Ast.fn) params = (* One check of the body against [ret], thrown away with everything it wrote into [env] ([snapshot_env]); pass two checks it again for real. *) let attempt ret = - let undo = snapshot_env env in + let undo, _ = snapshot_env env in let seen = !infer_seen in infer_seen := []; let restore () = undo (); infer_seen := seen in @@ -16538,16 +16589,17 @@ let build_program ~keep_going ?tolerate ?previous (decls : Ast.decl list) : ([snapshot_env]): a copy it asked for would otherwise stay cached, and the next body asking for it would be handed the name of a copy the program does not have. *) - let undo = snapshot_env env in + let undo, keep = snapshot_env env in (match f () with - | x -> x + | x -> keep (); x | exception ((Loc.Error d | Loc.Errors (d :: _)) as e) -> if ok env name d then begin undo (); tolerated := name :: !tolerated; None end - else raise e) + else (keep (); raise e) + | exception e -> keep (); raise e) in let decls, prelude_warnings = shadow_prelude (Parse.program (Prelude.forms ())) decls diff --git a/test/test_flan.ml b/test/test_flan.ml index 3bb133a9..9ff4d3de 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -7862,6 +7862,69 @@ let () = incr failures; Printf.printf "FAIL an else arm's own error alone: %d errors\n" n end); + (* An arm that needs the other's type, and is refused at it too, says why + at that type — not that it has no type on its own. *) + rejects_check "a bare struct else arm with an unknown name in it" + ~needle:"unknown name q2" + "(defstruct P [x i32 y i32])\n\ + (defn b3 [c bool p P] i32 (let [v (if c p {.x q2 .y 2})] (.y v)))\n\ + (defn main [] i32 0)"; + rejects_check "a bare struct match arm with an unknown name in it" + ~needle:"unknown name q2" + "(defstruct P [x i32 y i32])\n\ + (defn a3 [o (Option i32) p P] i32 \ + (let [v (match o (Some q) p None {.x q2 .y 2})] (.y v)))\n\ + (defn main [] i32 0)"; + (* A match arm that does not meet the others is refused at its value. *) + (match + checked + "(defn m4 [o (Option i32) x i8] i32 \ + (let [v (match o (Some q) x None (do (println \"a\") \"lit\"))] 0))\n\ + (defn main [] i32 0)" + with + | _ -> check "a match arm of another type is refused" false + | exception Loc.Error { Loc.dloc; dmsg; _ } -> + check "a match arm of another type is refused at its value" + (dloc.Loc.col = 87 && contains dmsg "expected i8, found string")); + (* Nested arms that meet at a wider type are checked once each, not once + per level above them. *) + (let nest kind depth = + let rec go k e = + if k = 0 then e + else + go (k - 1) + (match kind with + | `If -> Printf.sprintf "(if c a (+ (idg b) (i32 %s)))" e + | `Match -> + Printf.sprintf "(match o (Some q) a None (+ (idg b) (i32 %s)))" e) + in + go depth "(i32 b)" + in + let structs = + String.concat "" + (List.init 300 (Printf.sprintf "(defstruct S%d [a i32 b i64])\n")) + in + List.iter + (fun (kind, sg, what) -> + let src = + "(defn idg [x $t] $t x)\n" ^ structs + ^ "(defn f " ^ sg ^ " i64 (let [v " ^ nest kind 20 ^ "] v))\n\ + (defn g " ^ sg ^ " _ " ^ nest kind 20 ^ ")" + in + let t0 = Unix.gettimeofday () in + match checked src with + | p -> + check (what ^ " twenty deep checks fast") + (Unix.gettimeofday () -. t0 < 3.0); + check (what ^ " twenty deep meets at i64") + (List.exists + (fun (f : Tast.fn) -> + f.Tast.name = "g" && Types.equal f.Tast.ret (Types.Int Types.I64)) + p.Tast.fns) + | exception Loc.Error { Loc.dmsg; _ } -> + check (what ^ " twenty deep checks: " ^ dmsg) false) + [ (`If, "[c bool a i64 b i32]", "an if"); + (`Match, "[o (Option i32) a i64 b i32]", "a match") ]); rejects_check "an else arm's own error is the one reported" ~needle:"unknown function nope2" "(defn g [c bool a i32 b i64] i64 (let [v (if c a (+ b (nope2 1)))] v))\n\