From 0405666b1f4fa2237cb783acc1c9e1f4e39ffba5 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Sun, 13 Sep 2026 09:32:58 +0700 Subject: [PATCH] The two cases the tests did not cover, and one leak of a permission MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A type-changing (map f) is the case into's single shadowed element name would break if the shadowing were a trick rather than the language's rule; it is not, because each stage is a fresh slot at its own type, and into.flan now runs an i32 source into a (Vec f32) to say so. A move-only accumulator carried round by recur is the shape BUILT.md pitches the form on and was untested. It works, and recur.flan now carries a Vec three times round and answers with it. block's empty-body arm returned before the loop that distributes the tail, so (do) in a tail position left ctx.tail set for whatever was checked next. Latent rather than live — every consumer sets it immediately before use, and the leaking form is always Unit-typed — but it is one line to close and the invariant is easier to state closed. Also the PORTING.md line listing loop/recur among the things with no customer: it was built, and the half of that finding that still stands is tail calls, which were not. --- BUILT.md | 7 ++++++- NEXT.md | 4 +++- lib/check.ml | 4 +++- test/programs/into.flan | 13 +++++++++++++ test/programs/recur.flan | 12 ++++++++++++ test/test_acceptance.ml | 4 ++-- 6 files changed, 39 insertions(+), 5 deletions(-) diff --git a/BUILT.md b/BUILT.md index 14eeaa8..a1e79bf 100644 --- a/BUILT.md +++ b/BUILT.md @@ -3058,7 +3058,9 @@ is. So `into` collects, and a reducing macro of the same shape is a separate for in that position should borrow — `into.flan`'s does — and the day `drop` exists this stops being a question. - **One element name throughout**, shadowed by each `(map f)` stage: `(let [x (f x)] ...)`. A `let` binding's value is checked before its name is bound, so the initialiser reads the outer `x` — that is the language's rule, not an - accident, and `bind`'s `x~2` debug suffix exists precisely so a debugger does not lie about which is which. + accident, and `bind`'s `x~2` debug suffix exists precisely so a debugger does not lie about which is which. A + **type-changing** `map` is the case this most plausibly breaks and it does not: each stage is a fresh slot at the + stage's own type, and `into.flan` runs an `i32` source into a `(Vec f32)` to say so. ### What the prelude's macro limits cost, exactly @@ -3111,6 +3113,9 @@ it: the machinery was already there, and the question `recur` asks — *may this - **`recur` rebinds every name at once.** The new values go into temporaries and are written afterwards, so `(recur y x)` swaps. Interleaved writes would give `y y`, and `recur.flan` asserts the swap for exactly that reason. +- **A move-only accumulator goes round.** `(loop [acc (vec-new i32) i 0] ... (recur acc (+ i 1)))` is the shape the + form exists for, and it is the one the move tracker had to be taught about (below). `recur.flan` carries a `Vec` + round three iterations and answers with it. `tast.ml` said a `While` the checker *invents* contains no jumps, because the depths would be minted against a stack it is not on. `check_loop`'s `While` is the exception, and it is the exception because it is pushed on `ctx.loops` diff --git a/NEXT.md b/NEXT.md index ede707f..52b0df8 100644 --- a/NEXT.md +++ b/NEXT.md @@ -115,7 +115,9 @@ abandoned frame leaving half-written state behind; rollback is what finishes tha **What `PORTING.md` says NOT to build, with evidence:** escaping closures (one capture site, fixed by one parameter), `Handle`/pools, `Result`/`try`, `handler-case`, `loop`/`recur` and tail calls, user allocators, structural typing — **none has a customer in that code**. (`Handle` and the pool were built anyway, and on the other reason: they are the -gate on classes. The finding stands and is why they were built small — see [`BUILT.md`](BUILT.md).) And **generics is not the blocker** there either: the element-changing maps are +gate on classes. The finding stands and is why they were built small — see [`BUILT.md`](BUILT.md). `loop`/`recur` was +built too, and the finding stands there as well: what it is not is **tail calls**, which are still not built and still +have no customer.) And **generics is not the blocker** there either: the element-changing maps are five-line load-time loops. That last one hangs on a design decision the report states flatly — whether the game's state holds fixed arrays or `Vec`s. diff --git a/lib/check.ml b/lib/check.ml index 3c3ff75..ef3a16e 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -1367,7 +1367,9 @@ and borrowed ctx (a : Ast.expr) f = [let] is the case the relaxation exists for. *) and block ctx ?want ?(defer_ok = false) loc body = match body with - | [] -> expect loc ~want (unit_at loc) + (* Withdrawn here too. An empty body has no last form to be the tail, so + leaving the permission set would hand it to whatever is checked next. *) + | [] -> ctx.tail <- false; expect loc ~want (unit_at loc) | _ -> (* A block's tail is its last form and nothing else. Callers that must not pass one on need do nothing: [check] withdrew it before they were diff --git a/test/programs/into.flan b/test/programs/into.flan index 3714892..3374f21 100644 --- a/test/programs/into.flan +++ b/test/programs/into.flan @@ -35,6 +35,9 @@ (set builds (+ builds 1)) (slice xs 0 (len xs))) +(defn wide [x i32] f32 (f32 x)) +(defn bigf? [x f32] bool (> x 2.5)) + (defn show [v [i32]] () (dotimes [i (len v)] (print (at v i)) (print " ")) (println "")) @@ -71,6 +74,16 @@ (free v) (free src)) + ;; A type-changing map: the chain's element name is rebound at the new type + ;; by each stage, and the push sees the destination's element type. One name, + ;; shadowed — a let binding's value is checked before its name is bound, so + ;; each stage reads the stage before it. + (let [xs [1 2 3 4] + v (into xs (vec-new f32) (map wide) (filter bigf?))] + (dotimes [i (len v)] (print (at v i)) (print " ")) + (println "") ; 3 4 + (free v)) + ;; A source that is a call is bound once, so it is made once however many ;; elements come out of it. (let [xs [1 2 3 4] diff --git a/test/programs/recur.flan b/test/programs/recur.flan index e25daf0..7bc54aa 100644 --- a/test/programs/recur.flan +++ b/test/programs/recur.flan @@ -81,6 +81,18 @@ (recur (+ i 1) (+ acc hit)))))) (println "") ; 4 + ;; A move-only accumulator, carried round by recur and answered with. This + ;; is the shape the form exists for: no mutable local, no sentinel flag, and + ;; the Vec is the loop's value. recur writes every name on the way round, so + ;; the "moves a value bound outside the loop" rule is not about acc. + (let [v (loop [acc (vec-new i32) i 0] + (if (= i 3) + acc + (do (push acc i) (recur acc (+ i 1)))))] + (dotimes [i (len v)] (print (at v i))) + (println "") ; 012 + (free v)) + ;; A match arm is a tail too. (print (loop [i 0 acc 0] (match (step i) diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index e00fd4f..65b8dac 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -131,13 +131,13 @@ let () = rather than running out of stack. The swap line is the other — recur rebinds every name at once, and interleaved writes would print 1. *) outputs "loop and recur" "programs/recur.flan" - "10\n2\n21\n8\n10000000\n64\n012\n0\n4\n6\n"; + "10\n2\n21\n8\n10000000\n64\n012\n0\n4\n012\n6\n"; (* into. The count of pulls is the assertion a unit test cannot make: one pass, one call per element per stage it reaches, and no intermediate collection anywhere. The two show lines either side of it are the same source transformed in two orders, which have to differ. *) outputs "into" "programs/into.flan" - "7 8 9 \n2 4 6 8 10 12 \n4 8 12 \n21\n6 2 4 \n3 1 2 \n2 4 \n1\n"; + "7 8 9 \n2 4 6 8 10 12 \n4 8 12 \n21\n6 2 4 \n3 1 2 \n3 4 \n2 4 \n1\n"; (* The prelude's slice algorithms. Every assertion here is over an input a wrong implementation fails: unsorted with duplicates, negatives and an odd length; a reverse-sorted slice; and a sort of a subslice whose