diff --git a/lib/check.ml b/lib/check.ml index 8e45ace2..8acb0110 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -4147,9 +4147,31 @@ let tracked_call loc env name (tr : Shim.track) ret (args : Tast.expr list) = checked in and its diagnostic, for as long as the outermost call is on the stack — see [check_truthy]. Physical identity on both, since a generic's body is the same syntax checked again at another type. *) -let truthy_failed : (Ast.expr * ctx * Loc.diag) list ref = ref [] +let truthy_failed : + (Ast.expr * (string * binding) list * Types.t * Loc.diag) list ref = ref [] + +(* Whether two scopes bind the same names at the same types, which is what a + refusal under them can depend on — the slots are fresh on every pass. A + memo keyed on less would replay a refusal after a retry changed a type. *) +let same_scope (a : (string * binding) list) (b : (string * binding) list) = + a == b + || List.equal + (fun (n, (x : binding)) (m, (y : binding)) -> + String.equal n m && Types.equal x.bty y.bty) + a b let truthy_depth = ref 0 +(* The same for an [if], keyed on its condition and the expectation: + an [if] whose else arm is tried on its own terms first (see [check_if]) + would otherwise be re-checked, refused, by the trial of every [if] above + it — the square of a refused or/and chain's length. *) +let if_failed : + (Loc.t, + Ast.expr * ((string * binding) list * Types.t) * Types.t option * Loc.diag) + Hashtbl.t = + Hashtbl.create 16 +let if_depth = ref 0 + (* A Vec or a Map parameter is a copy of the caller's header — Odin's rule — so growing it reallocates a block only this function's copy points at, and @@ -6000,10 +6022,13 @@ and check_recur ctx ~tail loc args = accident. *) and check_truthy ctx c = match - List.find_opt (fun (n, cx, _) -> n == c && cx == ctx) !truthy_failed + List.find_opt + (fun (n, sc, r, _) -> n == c && r == ctx.ret && same_scope sc ctx.scope) + !truthy_failed with - | Some (_, _, d) -> raise (Loc.Error d) + | Some (_, _, _, d) -> raise (Loc.Error d) | None -> + let scope = ctx.scope in incr truthy_depth; Fun.protect ~finally:(fun () -> @@ -6012,7 +6037,7 @@ and check_truthy ctx c = (fun () -> try check_truthy_once ctx c with Loc.Error d as ex -> - truthy_failed := (c, ctx, d) :: !truthy_failed; + truthy_failed := (c, scope, ctx.ret, d) :: !truthy_failed; raise ex) and check_truthy_once ctx c = @@ -6064,6 +6089,27 @@ and check_truthy_once ctx c = | exception Loc.Error _ -> check ctx ~want:Types.Bool c and check_if ctx ?(tail = false) ?want loc c t e = + match + List.find_opt + (fun (n, (sc, r), w, _) -> + n == c && r == ctx.ret && w = want && same_scope sc ctx.scope) + (Hashtbl.find_all if_failed c.Ast.loc) + with + | Some (_, _, _, d) -> raise (Loc.Error d) + | None -> + let scope = ctx.scope in + incr if_depth; + Fun.protect + ~finally:(fun () -> + decr if_depth; + if !if_depth = 0 then Hashtbl.reset if_failed) + (fun () -> + try check_if_once ctx ~tail ?want loc c t e + with Loc.Error d as ex -> + Hashtbl.add if_failed c.Ast.loc (c, (scope, ctx.ret), want, d); + raise ex) + +and check_if_once ctx ~tail ?want loc c t e = let c = check_truthy ctx c in (* Both arms are the tail, and a one-armed [if] counts: [(when c (recur ...))] is how nearly every loop is written, and the branch is still the last diff --git a/test/test_flan.ml b/test/test_flan.ml index 6150470e..2b529fc2 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -5691,14 +5691,33 @@ let () = let rec nest k e = if k = 0 then e else nest (k - 1) ("(not " ^ e ^ ")") in "(defn g [x i32] bool " ^ nest 200 "x" ^ ")" in - match Watchdog.within 5 (fun () -> checked deep) with + let t0 = Unix.gettimeofday () in + match checked deep with | _ -> check "a deep not nest over an i32 is refused" false - | exception Watchdog.Timeout -> - check "a deep not nest over an i32 fails fast" false | exception Loc.Error { Loc.dmsg; _ } -> + check "a deep not nest over an i32 fails fast" + (Unix.gettimeofday () -. t0 < 3.0); check "a deep not nest keeps the one-level message" (dmsg = "a condition is a bool or a dyn, and this is i32 — test it, as \ (!= x 0)")); + (* A long or chain refused at its last operand, with nothing expected of it. + Each if tries its else arm on its own terms before checking it at bool, + and a refused if is answered from memory, so a thousand operands fail + at once rather than in the square of that. *) + (let deep = + "(defn g [x i32] bool (let [b (or " + ^ String.concat " " (List.init 1000 (Printf.sprintf "(= x %d)")) + ^ " 5)] b))" + in + (* Timed rather than under [Watchdog.within]: a catch-all inside the + checker can swallow the alarm's exception. *) + let t0 = Unix.gettimeofday () in + match checked deep with + | _ -> check "a refused or chain is refused" false + | exception Loc.Error { Loc.dmsg; _ } -> + check "a refused or chain fails fast" (Unix.gettimeofday () -. t0 < 3.0); + check "a refused or chain keeps the one-operand message" + (dmsg = "expected bool, found the integer literal 5")); (* A literal still names itself: that message knows something the rule does not, so the re-check's answer is kept wherever it is more specific. *) rejects_check "a literal condition keeps its own message"