From 6d87c02584086cfcb8ef16b6a3d12af4248c7dd8 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Sat, 19 Sep 2026 14:24:10 +0700 Subject: [PATCH] Both backends are asked whether they store where the render said they do MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The x86 block asks the break loop's questions of an --x86 host so that the two sets of answers can be read against each other rather than merely found plausible. A store is where they could most easily differ: the place forms the walk ends at are lowered by each backend's own `place', and the two disagree about an Option — which is why what may be written is settled in session.ml above both of them and not in either. So the same slot is written, read back, and refused for a type that does not fit, on this backend too. And `Check.expressions' carries the comment that was written for the function it replaced; the one-expression entry beside it has its own line. --- lib/check.ml | 45 +++++++++++++++++++++++---------------------- test/test_dev.ml | 27 +++++++++++++++++++++++++++ 2 files changed, 50 insertions(+), 22 deletions(-) diff --git a/lib/check.ml b/lib/check.ml index 67008a4..7e2612a 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -7068,30 +7068,30 @@ let instances_since env mark = List.rev (List.filteri (fun i _ -> i < fresh) env.instances) -(* One expression, checked against a program that is already running. The - frame is empty — a REPL expression has no parameters and no enclosing - function — so the slots it needs are whatever its own [let]s allocate. +(* Expressions checked against a program that is already running, all of them + into *one* frame. It is empty to start with — a REPL expression has no + parameters and no enclosing function — so the slots it ends up with are + whatever their own [let]s allocate. - [want] is the inspector's write verb and nothing else: [C-x C-e] has no - expectation to offer, but a store into a slot of type [f32] does, and the - whole value of passing it is that [3] arrives as an [f32] rather than as an - [i32] the store would then have to be refused for. The expectation flows - through [check] the way it flows anywhere — that is what bidirectional - means — and [expect] at the end is what catches the cases that ignore it, - so the refusal is the checker's own "expected f32, found string" and not a - second sentence written here that would drift from it. *) -(* Several of them against one frame, which is what the inspector's write verb - needs and what it must not build by hand. Two expressions checked - separately each number their slots from zero, so splicing them into one - thunk would have the second one's [let] reading and writing the first - one's storage — a frame that is two frames wearing one frame's clothes. - Sharing the [ctx] is the whole of the fix, and it is a fix because there is - exactly one allocator of slot indices in this compiler and it is this - record's counter. + One frame and not one each, which is what the inspector's write verb needs + and what it must not assemble by hand. Two expressions checked separately + both number their slots from zero, so splicing them into one thunk would + have the second one's [let] reading and writing the first one's storage — a + frame that is two frames wearing one frame's clothes. Sharing the [ctx] is + the whole of the fix, and it is a fix because there is exactly one allocator + of slot indices in this compiler and it is this record's counter. - The expressions are otherwise independent: nothing binds a name for the - next one, because the list is a list of values being stored and not a - sequence. *) + They are otherwise independent: none of them binds a name for the next, + because the list is a list of values being stored and not a sequence. + + [want] is the write verb too, and [C-x C-e] passes none: a store into a + slot of type [f32] has an expectation to offer and a typed expression does + not. The whole value of passing it is that [3] arrives as an [f32] rather + than as an [i32] the store would then have to be refused for. It flows + through [check] the way an expectation flows anywhere — that is what + bidirectional means — and [expect] at the end catches the arms that ignore + it, so the refusal is the checker's own "expected f32, found string" rather + than a second sentence written here that would drift from it. *) let expressions env (es : (Types.t option * Ast.expr) list) : Tast.expr list * Types.t array * string option array = let ctx = @@ -7113,6 +7113,7 @@ let expressions env (es : (Types.t option * Ast.expr) list) : (ts, Array.of_list (List.rev ctx.slot_tys), Array.of_list (List.rev ctx.slot_names)) +(* The one-expression case, which is every caller but the write verb. *) let expression env ?want (e : Ast.expr) : Tast.expr * Types.t array * string option array = match expressions env [ (want, e) ] with diff --git a/test/test_dev.ml b/test/test_dev.ml index 905a51a..79cc888 100644 --- a/test/test_dev.ml +++ b/test/test_dev.ml @@ -4487,6 +4487,33 @@ let () = else if Wire.string_field r "value" <> Some "(Point {.x 1.5 .y 2.5})" then fail "x86 inspect of slot 2 answered %S" (Option.value ~default:"" (Wire.string_field r "value")); + (* And the write half of the same root, for the reason this whole block + exists: the two backends must answer the same. A store is where they + could most easily not — the place forms the walk ends at are lowered + by each backend's own [place], and the two disagree about an Option, + which is why what may be written is settled in [session.ml] above + both of them rather than in either. *) + let r = + request c + "(:op \"set\" :frame 0 :slot 2 :path (\"y\") :edits ((:code \"6.5\")))" + in + if status r <> "ok" then fail "x86 set: %s" (said r) + else if Wire.string_field r "value" <> Some "6.5" then + fail "x86 set of p.y answered %S" + (Option.value ~default:"" (Wire.string_field r "value")); + let r = request c "(:op \"inspect\" :frame 0 :slot 2)" in + if Wire.string_field r "value" <> Some "(Point {.x 1.5 .y 6.5})" then + fail "x86: the store did not land where the render says it did: %S" + (Option.value ~default:"" (Wire.string_field r "value")); + (* A refusal that comes from above both backends reads the same here + as it does there, which is the claim rather than the refusal. *) + let r = + request c + "(:op \"set\" :frame 0 :slot 2 :path (\"y\") :edits ((:code \"\\\"no\\\"\")))" + in + if status r <> "error" || not (contains_sub (said r) "expected f32") then + fail "x86: a value of the wrong type was not refused by the checker: %s" + (said r); (* And the globals, which are not in the frame at all -- they are found through the same descriptor's fingerprint, and a frame whose [refsig] disagreed with what the daemon recomputes would refuse