Pin the latch to the continue path, and the clause barrier to its reason
A dotimes whose every iteration continues still counts to its trip count. The existing case fails by hanging if the latch is wrong; this one fails by counting wrong, which is the off-by-one the four-block layout could have. A restart-case clause was made a barrier on reasoning alone and nothing observed it. Now something does. And say what a labelled continue means, which is the half that is not obvious: it advances the named loop's counter and skips the rest of its body, not just the rest of the innermost one.
This commit is contained in:
parent
008165335d
commit
3f097de522
5
BUILT.md
5
BUILT.md
@ -2490,6 +2490,11 @@ header would have jumped straight past it: the counter would never advance and t
|
||||
the latch, `continue` branches to the latch block rather than to the header, and a `while` has an empty latch that
|
||||
every optimiser folds away. `emit_while` emits four blocks instead of three.
|
||||
|
||||
A **labelled** `continue` is the half worth stating outright: `(continue :rows)` branches to the *named* loop's latch,
|
||||
so that loop's counter advances and the rest of its body is skipped along with the rest of every loop inside it. It is
|
||||
"start the next iteration of `:rows`", not "skip the rest of this innermost body". `loops.flan` asserts exactly that —
|
||||
an outer `dotimes` whose tail never prints while its counter still runs out.
|
||||
|
||||
`Tast.Break` and `Tast.Continue` carry a **relative depth** — how many loops out the target is, innermost first —
|
||||
rather than a name or an id, because that is exactly what a backend already has. `emit` keeps one entry per `While`
|
||||
it is inside, the same shape and for the same reason as `pads`, and indexes it. The invariant this rests on: the
|
||||
|
||||
@ -39,6 +39,15 @@
|
||||
(set sum (+ sum k)))
|
||||
(print sum) (println "")) ; 0 + 1 + 3 + 4 = 8
|
||||
|
||||
;; Every iteration continues, and the count is still the trip count: the
|
||||
;; latch is on the continue path and not merely reachable from the body. The
|
||||
;; case above would hang if it were not; this one would count wrong.
|
||||
(let [c 0]
|
||||
(dotimes [m 3]
|
||||
(set c (+ c 1))
|
||||
(continue))
|
||||
(print c) (println "")) ; 3
|
||||
|
||||
;; A labelled break leaves the named loop. Without the label it would leave
|
||||
;; the inner one and the outer would run all three times: 0 1 0 1 0 1.
|
||||
(dotimes :outer [a 3]
|
||||
|
||||
@ -125,7 +125,7 @@ let () =
|
||||
latch, and folded onto the body a continue would jump past it — so the
|
||||
watchdog above is what turns that failure back into a report. *)
|
||||
outputs "break and continue" "programs/loops.flan"
|
||||
"4\n9\n8\n0\n1\n0\n0\n0\n3\n6\nhit\nhit\n2\n";
|
||||
"4\n9\n8\n3\n0\n1\n0\n0\n0\n3\n6\nhit\nhit\n2\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
|
||||
|
||||
@ -853,6 +853,11 @@ let () =
|
||||
rejects_check "break may not leave a restart-case"
|
||||
"(defn f [] (while true (restart-case (break) (go [] (println \"\")))))"
|
||||
~needle:"a restart-case";
|
||||
(* A clause is a barrier for the same reason the body is: it runs after a
|
||||
transfer landed, with the form's frames still to be popped. *)
|
||||
rejects_check "break may not leave a restart-case from a clause"
|
||||
"(defn f [] (while true (restart-case (println \"\") (go [] (break)))))"
|
||||
~needle:"a restart-case";
|
||||
accepts "a loop inside a handler-bind may break out of itself"
|
||||
"(defstruct C [n i32]) (defn f [] (handler-bind [(C [c] 0)] (while true (break))))";
|
||||
rejects_check "break may not leave a handler-bind"
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user