Merge: a while condition joins the loop's move regime
This commit is contained in:
commit
47cb46aa00
42
lib/check.ml
42
lib/check.ml
@ -1686,7 +1686,25 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
|
|||||||
| Ast.Let (bs, body) -> check_let ctx ~tail ?want ~defer_ok loc bs body
|
| Ast.Let (bs, body) -> check_let ctx ~tail ?want ~defer_ok loc bs body
|
||||||
| Ast.If (c, t, e') -> check_if ctx ~tail ?want loc c t e'
|
| Ast.If (c, t, e') -> check_if ctx ~tail ?want loc c t e'
|
||||||
| Ast.While (label, c, body) ->
|
| Ast.While (label, c, body) ->
|
||||||
|
(* The condition is part of the loop even though it is written outside the
|
||||||
|
braces: emit puts it in the header block, so it is re-evaluated at the
|
||||||
|
top of every trip, and a condition that gives a value away frees it once
|
||||||
|
per trip. So it is held to the loop's rule on moves and to nothing else
|
||||||
|
the loop changes: it stays outside [in_loop], because a [break] in a
|
||||||
|
condition still means the enclosing loop and a [defer] there is still
|
||||||
|
the outer block's, but its moves are diffed against the same dead set.
|
||||||
|
[dotimes]' count and a [loop]'s initial values are checked outside this
|
||||||
|
regime on purpose: they are evaluated exactly once, before the first
|
||||||
|
trip, so giving one away there is no more than giving it away before
|
||||||
|
the loop. *)
|
||||||
|
let before = ctx.dead in
|
||||||
|
let outer = List.map (fun (_, b) -> b.slot) ctx.scope in
|
||||||
let c = check ctx ~want:Types.Bool c in
|
let c = check ctx ~want:Types.Bool c in
|
||||||
|
moved_across_iterations ctx ~before ~outer
|
||||||
|
"this while condition moves a value that was bound outside the loop, and \
|
||||||
|
the condition is evaluated again at the top of every trip, so the second \
|
||||||
|
one would use what the first gave away. Move it out of the loop, or \
|
||||||
|
test something the loop does not give away";
|
||||||
let body = in_loop ctx ?label (fun () ->
|
let body = in_loop ctx ?label (fun () ->
|
||||||
scoped ctx (fun () -> map_lr (fun b -> check ctx b) body))
|
scoped ctx (fun () -> map_lr (fun b -> check ctx b) body))
|
||||||
in
|
in
|
||||||
@ -2431,15 +2449,25 @@ and in_loop ctx ?label ?entry ?(fresh = []) f =
|
|||||||
let r = f () in
|
let r = f () in
|
||||||
ctx.defer_block <- blocker;
|
ctx.defer_block <- blocker;
|
||||||
ctx.loops <- loops;
|
ctx.loops <- loops;
|
||||||
|
moved_across_iterations ctx ~before ~outer:outer_slots
|
||||||
|
"this moves a value that was bound outside the loop, so the next \
|
||||||
|
iteration would use what this one gave away. Move it out of the loop, \
|
||||||
|
or bind a fresh value inside it";
|
||||||
|
r
|
||||||
|
|
||||||
|
(* The rule a loop adds to the move checker, in one place because two forms
|
||||||
|
need it and they need it for the same reason. Everything that runs more
|
||||||
|
than once runs against the dead set it left behind last time: a slot that
|
||||||
|
was live on the way in and is dead on the way out was given away by code
|
||||||
|
that is about to run again, and the second run would be using what the
|
||||||
|
first one released. Slots bound inside the repeated region are not in
|
||||||
|
[outer] and are not the question — they are born again every trip. *)
|
||||||
|
and moved_across_iterations ctx ~before ~outer why =
|
||||||
List.iter
|
List.iter
|
||||||
(fun (slot, where) ->
|
(fun (slot, where) ->
|
||||||
if (not (List.mem_assoc slot before)) && List.mem slot outer_slots then
|
if (not (List.mem_assoc slot before)) && List.mem slot outer then
|
||||||
fail where
|
fail where "%s" why)
|
||||||
"this moves a value that was bound outside the loop, so the next \
|
ctx.dead
|
||||||
iteration would use what this one gave away. Move it out of the \
|
|
||||||
loop, or bind a fresh value inside it")
|
|
||||||
ctx.dead;
|
|
||||||
r
|
|
||||||
|
|
||||||
(* Which loop a [break] or a [continue] means, as a count of loops outwards
|
(* Which loop a [break] or a [continue] means, as a count of loops outwards
|
||||||
from the innermost — which is what [Tast.Break] carries and what [emit]
|
from the innermost — which is what [Tast.Break] carries and what [emit]
|
||||||
|
|||||||
@ -1198,6 +1198,16 @@ let () =
|
|||||||
rejects_check "a labelled break may not leave a loop"
|
rejects_check "a labelled break may not leave a loop"
|
||||||
"(defn f [] () (while :o true (loop [i 0] (break :o))))"
|
"(defn f [] () (while :o true (loop [i 0] (break :o))))"
|
||||||
~needle:"no value to give";
|
~needle:"no value to give";
|
||||||
|
(* A while's condition runs once per trip, so it lives under the same rule
|
||||||
|
as the body: what it gives away, it gives away again next time round.
|
||||||
|
Before this was checked the program below compiled and aborted in free(). *)
|
||||||
|
rejects_check "a while condition may not move what the loop is standing on"
|
||||||
|
"(defn eat [v (Vec i32)] bool (do (free v) true)) \
|
||||||
|
(defn f [] () (let [v (vec-new i32)] (while (eat v) (break))))"
|
||||||
|
~needle:"evaluated again at the top of every trip";
|
||||||
|
accepts "a condition that only looks at what it tests is fine"
|
||||||
|
"(defn f [] () (let [v (vec-new i32) n 0] \
|
||||||
|
(while (and (< n 10) (> (len v) 0)) (set n (+ n 1))) (free v)))";
|
||||||
rejects_check "loop takes no label"
|
rejects_check "loop takes no label"
|
||||||
"(defn f [] () (loop :o [i 0] (recur i)))" ~needle:"loop takes no label";
|
"(defn f [] () (loop :o [i 0] (recur i)))" ~needle:"loop takes no label";
|
||||||
rejects_check "a loop binding is a plain name"
|
rejects_check "a loop binding is a plain name"
|
||||||
|
|||||||
Loading…
x
Reference in New Issue
Block a user