Find a span's leftover boundary through the inverse it already has
The decision used a rounded division, `total.px.div(fixed)`, where the room the children get is a floored multiply, so the boundary and the drawing it guards were two expressions for one length and disagreed at the edge of it. `room` is that length as a `Len`, `room.to_px` is the multiply, and `Holds::through` is its exact preimage -- so ask `room` whether anything is left and hand the answer back through the same expression. The three branches go with the division. They were the sign of `1 - rel`: the fixed parts growing slower than the box, faster, or exactly with it, and `through` reads that sign already. Forty lines become twelve, one `div` leaves layout, and the boundary is the drawing's own. Green on the suite, the shrinker at 400 seeds of depth 5, the oracle at 1000 seeds of depth 6 and 120 in debug, and 2000 seeds at depth 4 over all fifteen cases. `tabs`, `view`, `minimal` and `random` byte-identical.
This commit is contained in:
1 parent
a92c6acdbf
commit
53b00c68e9
1 file changed
+16
-34
+16
-34
@@ -46,43 +46,26 @@ impl Widget for Span {
|
||||
|sum, len| sum + *len,
|
||||
);
|
||||
|
||||
// What is left for the shares to divide: the box less everything
|
||||
// fixed, as a length of the box rather than a number of pixels.
|
||||
let room = Len::rel_max() - Len::from_parts(total.rel, total.px);
|
||||
// Whether anything is left over is a question in pixels: `rel(0.5)`
|
||||
// beside 300 px is full at 600 and overfull at 400. The room to
|
||||
// divide is `len * fixed - total.px`, and the length where it runs
|
||||
// out is exactly the box a parent sizing itself from this answer
|
||||
// hands back -- which is why this used to need a margin either side
|
||||
// of the boundary, and why it does not now: that box and this sum are
|
||||
// whole counts of the same step, and both routes to it land on the
|
||||
// same count. What the generated oracle checks is the consequence,
|
||||
// since which children exist at all turns on this.
|
||||
let fixed = Rel::ONE - total.rel;
|
||||
// beside 300 px is full at 600 and overfull at 400. Asked of `room`
|
||||
// itself, and answered back through the same expression, so the
|
||||
// boundary is the drawing's own and not a second way of finding it:
|
||||
// the three cases a rounded division needed -- the fixed parts
|
||||
// growing slower than the box, faster, or exactly with it -- are the
|
||||
// sign of `room.rel`, which `through` already reads. What the
|
||||
// generated oracle checks is the consequence, since which children
|
||||
// exist at all turns on this.
|
||||
let mut shares = false;
|
||||
if total.leftover > Weight::ZERO {
|
||||
let current = painter.px_len(axis);
|
||||
let holds = if fixed > Rel::ZERO {
|
||||
// The box length the fixed parts alone fill.
|
||||
let full = total.px.div(fixed);
|
||||
shares = current > full;
|
||||
match shares {
|
||||
true => Holds::from(full.next_up()..=Px::MAX),
|
||||
false => Holds::from(Px::MIN..=full),
|
||||
}
|
||||
} else if fixed < Rel::ZERO {
|
||||
// The relative parts grow faster than the box does, so here
|
||||
// a shorter box is the one that leaves room.
|
||||
let full = total.px.div(fixed);
|
||||
shares = current < full;
|
||||
match shares {
|
||||
true => Holds::from(Px::MIN..=full.next_down()),
|
||||
false => Holds::from(full..=Px::MAX),
|
||||
}
|
||||
} else {
|
||||
// The relative parts take exactly the box, whatever it is, so
|
||||
// the only room is what negative pixels leave.
|
||||
shares = total.px < Px::ZERO;
|
||||
Holds::ANY
|
||||
shares = room.to_px(painter.px_len(axis)) > Px::ZERO;
|
||||
let holds = match shares {
|
||||
true => Holds::from(Px::STEP..=Px::MAX),
|
||||
false => Holds::from(Px::MIN..=Px::ZERO),
|
||||
};
|
||||
painter.holds(axis, holds);
|
||||
painter.holds(axis, holds.through(room));
|
||||
}
|
||||
|
||||
// Across itself a span is as long as its longest child -- unless a
|
||||
@@ -99,7 +82,6 @@ impl Widget for Span {
|
||||
// row.
|
||||
let mut fixed = Len::rel_min();
|
||||
let mut taken = Weight::ZERO;
|
||||
let room = Len::rel_max() - Len::from_parts(total.rel, total.px);
|
||||
let mut start = Len::rel_min();
|
||||
let mut ortho = LayoutLen::ZERO;
|
||||
for (child, len) in self.children.iter().zip(&lens) {
|
||||
|
||||
Reference in new issue
Block a user