Cairn.VList
lean/Cairn/VList.lean
Virtual lists: lay out only the rows on screen
A VList is a scroll box over a list the view names in full (every row's key) but builds only
in part: the rows that meet the viewport, plus overscan points above and below, with a spacer
for the rest above and one for the rest below (docs/layout.md, "Virtual lists").
- Heights are never measured off screen. A row's height is known once it has been laid; until
then it is the list's estimate (given, or the mean of the first heights laid at its width, kept until the width changes). The runtime records
the real heights from every layout (
record, called byRuntime.fixUI), keyed by row key and forgotten when the list's width changes, andsettleruns the view again when they change. - The anchor. The runtime also records the first row showing and where its top was. When the
heights above it change, or rows are inserted above it, the offset moves by as much as its top
did, so it stays where it was on screen. When the clamp keeps the offset from moving that far,
the row is held, and put back once the clamp allows, until the batch's frame is shown
(
anchorAt).
The heights a view lays out by are a Model: the known rows, sorted by index, and the estimate
for the rest. Model.top and Model.height are the specification (sums over the rows); the view
computes them with topF and heightF (a binary search and a prefix sum, so a frame costs the
same whatever the list's length), and topF_eq and heightF_eq prove them equal.
Theorems, for every model:
window_iff: the rows laid are exactly those whose extent[top, top + height)meets[lo, hi)(the viewport, widened by the overscan);window_count: there are at most(hi − lo) / m + 2of them, for anymno larger than any row's height (minHeight_le), whatever the list's length;top_succ: each row starts where the one before it ends (the layout's side,Cairn.Layout.VList, shows the laid rows do too);record_keeps: a correction keeps the anchor's on-screen position, unless the clamp moves it;top_eq_of_below: a change wholly below a row doesn't move its top, so it moves no offset;record_holds,record_returns: when the clamp moves it, the row is held at its place, and the next record the clamp allows puts it back there.
Imports Cairn.App
Structures 3
Model : Type
The heights a list is laid out by: count rows, the known ones (rows, sorted by index:
model_sorted) at their height, the others at est.
Good (M : Model) : Prop
The model is sorted, and its heights are positive.
sorted : Sorted M.rows.toList
pos : 0 ≤ M.height i
VList : Type
A virtual list (docs/layout.md, "Virtual lists"): a scroll box whose offset the runtime owns
(ref, usually a place claim's ref, as with UI.scrolling), holding only the rows that meet its
viewport and overscan points above and below it.
ref : ControlRef
estimate : Option NatA row's height until it is laid; none: the mean of the heights known so far.
overscan : NatPoints laid above and below the viewport, so a small scroll shows rows already laid.
style : Style
The box's own style: its size, padding, background. Its axis, gap, justify and scroll are the list's.
Definitions 44
search (p : Nat → Bool) (lo hi : Nat) : Nat
The least i in [lo, hi) where p holds, or hi: binary search, for a p that stays
true once it is (search_spec).
Mono (p : Nat → Bool) : Prop
p stays true once it is.
corrBelow (est : Nat) : List Row → Nat → Int
The corrections height − est of the rows with index below i.
corrAt (est : Nat) : List Row → Nat → Int
The corrections of the rows with index i (one at most, in a sorted list).
corrAll (est : Nat) : List Row → Int
The corrections of every row.
Sorted (l : List Row) : Prop
Rows sorted by index, each index once.
top (M : Model) (i : Nat) : Int
Row i's top in the list's content: the heights of the rows above it.
height (M : Model) (i : Nat) : Int
Row i's height: its known height, or the estimate.
minHeight (M : Model) : Nat
The least height in a model: the estimate's and every known row's.
prefixes (est : Nat) : List Row → Int → List Int
acc then the running sums of the rows' corrections: entry m is acc plus the first
m rows' corrections.
pre (M : Model) : Array Int
The prefix sums of the known rows' corrections (prefixes).
atOrBelow (M : Model) (i m : Nat) : Bool
Known row m lies at or below row i (or there is none).
topF (M : Model) (pre : Array Int) (i : Nat) : Int
heightF (M : Model) (i : Nat) : Int
Row i's height, fast (heightF_eq).
firstF (M : Model) (pre : Array Int) (lo : Int) : Nat
The first row laid: the least row whose bottom is below lo.
lastF (M : Model) (pre : Array Int) (first : Nat) (hi : Int) : Nat
One past the last row laid: from first, the least row whose top is at or below hi.
window (M : Model) (lo hi : Int) : Nat × Nat
The rows laid for the content span [lo, hi): indices [first, last).
keep (keys : Array Nat) : List Row → Nat → List Row
The rows of l that can be trusted for keys: in increasing index order from next, each at
an index whose key it is, each at least a point tall. Others are dropped.
byKey (rows : List Row) : Array Row
Rows sorted by key, for looking keys up (indexOf).
lookup (sorted : Array Row) (k : Nat) : Option Row
The known row with key k in sorted (sorted by key), by binary search.
relocate (keys : Array Nat) (known : Known) : List Row
known's rows moved to the indices keys gives their keys. Usually nothing moves (the same
keys) or every row moves by the same amount (rows inserted at the head); otherwise each key is
looked up.
align (keys : Array Nat) (known : Known) : Array Row
The known rows for these keys, sorted by index (model_sorted): what the runtime knew,
moved to where their keys are now.
defaultEstimate : NatA row's height when nothing is known and no estimate is given.
mean (rows : Array Row) : Nat
The mean of the rows' heights; 0 when there are none.
estOf (guess : Option Nat) (stored : Nat) (rows : Array Row) : Nat
The estimate: the given one, else the one the runtime keeps (Known.est), else the mean of
the known heights; at least a point.
model (keys : Array Nat) (known : Known) (guess : Option Nat) : Model
The model a view lays keys out by, from what the runtime knows.
spacer (h : Int) : Node
An empty box of height h: what stands for the rows not laid.
viewportOf (ui : UI) (k : Known) : Int
The viewport the window is computed for: the box's length when it was last laid, else the window's height (more than enough).
rowNodes (keys : Array Nat) (row : Nat → Node) (first last : Nat) : List Node
The rows [first, last), each built from its key.
modelOf (info : Info) : Model
The model a laid list was laid out by.
infoOf (v : VList) (ui : UI) (keys : Array Nat) : Info
What node lays a list out by: the model, and the rows [first, last) it builds.
node (v : VList) (ui : UI) (keys : Array Nat) (row : Nat → Node) : Node
A virtual list's box. keys names every row, in order (keep the array in the app's state,
so the view doesn't rebuild it every frame); row builds the row with a given key. Only the rows
that meet the viewport, widened by the overscan, are built, between a spacer for the rows above
and one for the rows below, at the heights the runtime knows (model).
span (info : Info) (o : Int) : Int × Int
The span of content node laid rows for: the offset less the overscan, to the offset plus the
viewport and the overscan.
clampTo (x lim : Int) : Int
x within [0, lim] (lim floored at 0), as the runtime clamps offsets.
laidRows (info : Info) (kids : List Laid) : List Row
The rows a laid list laid, with their heights: its children past the top spacer.
go (info : Info) : Nat → List Laid → List Row
keepSpan : NatHow many rows either side of those laid the runtime keeps the heights of. Further rows go back to the estimate (the anchor keeps the rows on screen still when they do), so what the runtime keeps, and what a frame costs, stays bounded however long the list and however much of it has been scrolled through (bench/vlist.md).
merged (info : Info) (width : Int) (kids : List Laid) : Array Row
What is known after a layout: the heights known before within keepSpan rows of those laid
(none if the width changed), with the rows just laid at the heights they were laid at.
keptEst (info : Info) (width : Int) (rows : Array Row) : Nat
The estimate kept after a layout: the one kept before, unless the width changed; else the mean of the heights now known.
after (info : Info) (width : Int) (kids : List Laid) : Model
The model after a layout.
keepRow (info : Info) (rows : Array Row) (o : Int) : Option (Nat × Int)
The row to keep still, as its index in the new model and its top before: the anchor, if the
offset is where it was recorded (nothing scrolled since) and its key is still known; otherwise
the first row showing at the laid offset o, in the heights it was laid by.
corrected (M' : Model) (keepAt : Option (Nat × Int)) (o lim : Int) : Int
The corrected offset: o moved by as much as the kept row's top moved, clamped.
anchorAt (info : Info) (M' : Model) (keepAt : Option (Nat × Int)) (o o' : Int) : Option Anchor
The anchor recorded after a correction to o': the first row showing at o', if it was
laid, else the kept row. But when the clamp moved the offset (the kept row isn't where it was on
screen), the kept row, held: top + hold is where its top would be had the offset moved freely
(o' + (t − o)), so a later layout in the same batch that can (a longer list, a larger limit)
moves the offset to put it back (record_holds, record_returns). The hold lasts until the
batch's frame is shown (Runtime.steps, Known.letGo): then the row is kept where it shows.
record (info : Info) (r : Rect) (pad : Insets) (o lim : Int) (kids : List Laid) : Known × Int
The runtime's record of a laid list (Runtime.fixUI): the box at r with padding pad,
laid at offset o with children kids, whose offset may go up to lim. Returns what is now
known (the heights laid, the box's length, the anchor) and the corrected offset.
Theorems 39
search_spec (p : Nat → Bool) (hp : Mono p) (lo hi : Nat) (hle : lo ≤ hi) : lo ≤ search p lo hi ∧ search p lo hi ≤ hi ∧ (∀ (i : Nat), lo ≤ i → i < search p lo hi → p i = false) ∧ (search p lo hi < hi → p (search p lo hi) = true)
corrBelow_succ (est : Nat) (l : List Row) (i : Nat) : corrBelow est l (i + 1) = corrBelow est l i + corrAt est l i
top_zero (M : Model) : M.top 0 = 0
top_succ (M : Model) (i : Nat) : M.top (i + 1) = M.top i + M.height i
Adjacent. Each row starts where the one before it ends: no gaps, no overlaps.
corrAt_none (est : Nat) (l : List Row) (i : Nat) (h : ∀ (r : Row), r ∈ l → r.index ≠ i) : corrAt est l i = 0
corrAt_mem (est : Nat) (l : List Row) (hs : Sorted l) {r : Row} (hr : r ∈ l) : corrAt est l r.index = ↑r.height - ↑est
height_eq (M : Model) (hs : Sorted M.rows.toList) (i : Nat) : (∀ (r : Row), r ∈ M.rows.toList → r.index = i → M.height i = ↑r.height) ∧ ((∀ (r : Row), r ∈ M.rows.toList → r.index ≠ i) → M.height i = ↑M.est)
A row's height in a sorted model: its known height if it is known, else the estimate.
height_ge (M : Model) (hs : Sorted M.rows.toList) {m : Nat} (he : m ≤ M.est) (hr : ∀ (r : Row), r ∈ M.rows.toList → m ≤ r.height) (i : Nat) : ↑m ≤ M.height i
Heights are at least m when the estimate and every known height are.
foldl_min_le (l : List Row) (a : Nat) : List.foldl (fun a r => min a r.height) a l ≤ a ∧ ∀ (r : Row), r ∈ l → List.foldl (fun a r => min a r.height) a l ≤ r.height
foldl_min_ge (l : List Row) (a m : Nat) (ha : m ≤ a) (hl : ∀ (r : Row), r ∈ l → m ≤ r.height) : m ≤ List.foldl (fun a r => min a r.height) a l
minHeight_le (M : Model) (hs : Sorted M.rows.toList) (i : Nat) : ↑M.minHeight ≤ M.height i
minHeight is no larger than any row's height.
top_mono (M : Model) (hh : ∀ (i : Nat), 0 ≤ M.height i) {i j : Nat} (hij : i ≤ j) : M.top i ≤ M.top j
top_sub_ge (M : Model) {m : Int} (hh : ∀ (i : Nat), m ≤ M.height i) {i j : Nat} (hij : i ≤ j) : ↑(j - i) * m ≤ M.top j - M.top i
j − i rows of at least m points each take at least (j − i)·m points.
top_eq_of_below (M M' : Model) (i : Nat) (h : ∀ (j : Nat), j < i → M.height j = M'.height j) : M.top i = M'.top i
A change wholly below a row doesn't move its top. Two models that agree on the heights
of every row above row i put it at the same place (so a correction there moves no offset).
prefixes_get (est : Nat) (l : List Row) (acc : Int) (m : Nat) (hm : m ≤ l.length) : (prefixes est l acc)[m]? = some (acc + corrAll est (List.take m l))
atOrBelow_mono (M : Model) (hs : Sorted M.rows.toList) (i : Nat) : Mono (M.atOrBelow i)
below_spec (M : Model) (hs : Sorted M.rows.toList) (i : Nat) : M.below i ≤ M.rows.size ∧ (∀ (m : Nat) (h : m < M.rows.size), m < M.below i → M.rows[m].index < i) ∧ ∀ (m : Nat) (h : m < M.rows.size), M.below i ≤ m → i ≤ M.rows[m].index
corrBelow_append (est : Nat) (a b : List Row) (i : Nat) : corrBelow est (a ++ b) i = corrBelow est a i + corrBelow est b i
corrBelow_all_lt (est : Nat) (l : List Row) (i : Nat) (h : ∀ (r : Row), r ∈ l → r.index < i) : corrBelow est l i = corrAll est l
corrBelow_all_ge (est : Nat) (l : List Row) (i : Nat) (h : ∀ (r : Row), r ∈ l → i ≤ r.index) : corrBelow est l i = 0
topF_eq (M : Model) (hs : Sorted M.rows.toList) (i : Nat) : M.topF M.pre i = M.top i
The fast top is the top.
heightF_eq (M : Model) (hs : Sorted M.rows.toList) (i : Nat) : M.heightF i = M.height i
The fast height is the height.
window_spec (M : Model) (hM : M.Good) (lo hi : Int) : (M.window lo hi).fst ≤ (M.window lo hi).snd ∧ (M.window lo hi).snd ≤ M.count ∧ (∀ (i : Nat), i < (M.window lo hi).fst → M.top (i + 1) ≤ lo) ∧ ((M.window lo hi).fst < M.count → lo < M.top ((M.window lo hi).fst + 1)) ∧ (∀ (i : Nat), (M.window lo hi).fst ≤ i → i < (M.window lo hi).snd → M.top i < hi) ∧ ((M.window lo hi).snd < M.count → hi ≤ M.top (M.window lo hi).snd)
window_iff (M : Model) (hM : M.Good) (lo hi : Int) {i : Nat} (hi' : i < M.count) : (M.window lo hi).fst ≤ i ∧ i < (M.window lo hi).snd ↔ lo < M.top i + M.height i ∧ M.top i < hi
Exactly the rows that meet the span. A row is laid if and only if its extent
[top, top + height) meets [lo, hi).
window_count (M : Model) (hM : M.Good) {m : Int} (hm : 0 < m) (hh : ∀ (i : Nat), m ≤ M.height i) (lo hi : Int) (hlh : lo ≤ hi) : ↑((M.window lo hi).snd - (M.window lo hi).fst) ≤ (hi - lo) / m + 2
Bounded by the viewport, not the list. With every row at least m > 0 points tall, at
most (hi − lo) / m + 2 rows are laid: the ones wholly inside the span, and one at each end.
keep_spec (keys : Array Nat) (l : List Row) (next : Nat) : Sorted (keep keys l next) ∧ ∀ (r : Row), r ∈ keep keys l next → next ≤ r.index ∧ keys[r.index]? = some r.key ∧ 1 ≤ r.height
align_spec (keys : Array Nat) (known : Known) : Sorted (align keys known).toList ∧ ∀ (r : Row), r ∈ (align keys known).toList → keys[r.index]? = some r.key ∧ 1 ≤ r.height
model_good (keys : Array Nat) (known : Known) (guess : Option Nat) : (model keys known guess).Good ∧ ∀ (i : Nat), 1 ≤ (model keys known guess).height i
A view's model is sorted, and every height in it is at least a point (so window_iff
and window_count apply, with m = 1, or minHeight).
model_rows_lt (keys : Array Nat) (known : Known) (guess : Option Nat) (r : Row) : r ∈ (model keys known guess).rows.toList → r.index < (model keys known guess).count
Known rows lie in the list: each index is below the row count.
infoOf_model (v : VList) (ui : UI) (keys : Array Nat) : (v.infoOf ui keys).modelOf = model keys (ui.listOf v.ref) v.estimate
infoOf_window (v : VList) (ui : UI) (keys : Array Nat) : ((v.infoOf ui keys).first, (v.infoOf ui keys).last) = (v.infoOf ui keys).modelOf.window (ui.scrollOf v.ref - ↑v.overscan) (ui.scrollOf v.ref + (v.infoOf ui keys).viewport + ↑v.overscan)
infoOf_viewport (v : VList) (ui : UI) (keys : Array Nat) : 0 ≤ (v.infoOf ui keys).viewport
minHeight_pos (keys : Array Nat) (known : Known) (guess : Option Nat) : 1 ≤ (model keys known guess).minHeight
node_eq (v : VList) (ui : UI) (keys : Array Nat) (row : Nat → Node) : ∃ st, st.scroll = some (ui.scrollOf v.ref) ∧ st.axis = Axis.column ∧ st.gap = 0 ∧ st.justify = Align.start ∧ st.scrollRef = some v.ref ∧ st.rows = some (v.infoOf ui keys) ∧ v.node ui keys row = Node.box st none (spacer ((v.infoOf ui keys).modelOf.top (v.infoOf ui keys).first) :: rowNodes keys row (v.infoOf ui keys).first (v.infoOf ui keys).last ++ [spacer ((v.infoOf ui keys).modelOf.top (v.infoOf ui keys).modelOf.count - (v.infoOf ui keys).modelOf.top (v.infoOf ui keys).last)])
The box node builds: a column scroll box with no gap, scrolled by the runtime's offset,
holding a spacer as tall as the rows above first, the rows [first, last) in key order, and a
spacer as tall as the rows from last on, all in the heights of the model it lays out by.
node_rows (v : VList) (ui : UI) (keys : Array Nat) : have info := v.infoOf ui keys; have lo := ui.scrollOf v.ref - ↑v.overscan; have hi := ui.scrollOf v.ref + info.viewport + ↑v.overscan; (∀ (i : Nat), i < keys.size → (info.first ≤ i ∧ i < info.last ↔ lo < info.modelOf.top i + info.modelOf.height i ∧ info.modelOf.top i < hi)) ∧ 0 ≤ info.viewport ∧ ↑(info.last - info.first) ≤ (info.viewport + 2 * ↑v.overscan) / ↑info.modelOf.minHeight + 2
Exactly the rows meeting the viewport, and only so many. A virtual list builds row i
(of its keys) if and only if the row's extent in the heights it lays out by meets the viewport
widened by the overscan; and it builds at most (viewport + 2·overscan) / minHeight + 2 rows,
whatever the list's length.
record_keeps (info : Info) (r : Rect) (pad : Insets) (o lim : Int) (kids : List Laid) {i : Nat} {t : Int} (hk : keepRow info (after info (r.w - pad.left - pad.right) kids).rows o = some (i, t)) (hc : 0 ≤ o + ((after info (r.w - pad.left - pad.right) kids).topF (after info (r.w - pad.left - pad.right) kids).pre i - t) ∧ o + ((after info (r.w - pad.left - pad.right) kids).topF (after info (r.w - pad.left - pad.right) kids).pre i - t) ≤ lim) : (after info (r.w - pad.left - pad.right) kids).topF (after info (r.w - pad.left - pad.right) kids).pre i - (record info r pad o lim kids).snd = t - o
The anchor stays still. When the runtime keeps a row still (the anchor, or the row
showing at the laid offset), the corrected offset moves by exactly as much as that row's top
moved, so the row is where it was on screen (its top less the offset is unchanged), unless the
clamp moved it. This holds whatever changed: rows inserted or removed above it, heights
corrected above it or the estimate changing; a change wholly below it moves nothing
(top_eq_of_below).
keepRow_anchor (info : Info) (rows : Array Row) (o : Int) {a : Anchor} (ha : info.known.anchor = some a) (ho : a.offset = o) {r : Row} (hr : Array.find? (fun x => x.key == a.key) rows = some r) : keepRow info rows o = some (r.index, a.top + a.hold)
When the anchor is kept, it is the anchor recorded at this offset: the row the reader was at, wherever its key has moved.
record_holds (info : Info) (r : Rect) (pad : Insets) (o lim : Int) (kids : List Laid) {i : Nat} {t : Int} (hk : keepRow info (after info (r.w - pad.left - pad.right) kids).rows o = some (i, t)) (hc : (record info r pad o lim kids).snd ≠ o + ((after info (r.w - pad.left - pad.right) kids).topF (after info (r.w - pad.left - pad.right) kids).pre i - t)) : ∃ a, (record info r pad o lim kids).fst.anchor = some a ∧ a.key = info.keys[i]?.getD 0 ∧ a.offset = (record info r pad o lim kids).snd ∧ a.top + a.hold = (record info r pad o lim kids).snd + (t - o)
A clamped row is held, not dropped. When the clamp keeps the offset from moving as far
as the kept row's top moved (rows inserted above it at the end of a short list, say), the anchor
recorded is that row, held at its top had the offset moved freely: its place on screen before,
t − o, from the corrected offset.
record_returns (info : Info) (r : Rect) (pad : Insets) (o' lim : Int) (kids : List Laid) {a : Anchor} {o t : Int} (ha : info.known.anchor = some a) (hao : a.offset = o') (hat : a.top + a.hold = o' + (t - o)) {row : Row} (hr : Array.find? (fun x => x.key == a.key) (after info (r.w - pad.left - pad.right) kids).rows = some row) (hc : 0 ≤ o' + ((after info (r.w - pad.left - pad.right) kids).topF (after info (r.w - pad.left - pad.right) kids).pre row.index - (a.top + a.hold)) ∧ o' + ((after info (r.w - pad.left - pad.right) kids).topF (after info (r.w - pad.left - pad.right) kids).pre row.index - (a.top + a.hold)) ≤ lim) : (after info (r.w - pad.left - pad.right) kids).topF (after info (r.w - pad.left - pad.right) kids).pre row.index - (record info r pad o' lim kids).snd = t - o
And put back once the clamp allows. The next record of the list, laid at the offset a
held anchor was recorded at, with the row's key still known, keeps the row where it was before
the clamp held it, t − o into the box, unless the clamp moves the offset again. With
record_holds: a row inserted or grown above the first row showing moves nothing on screen once
the list is long enough to let it, within the batch.
Instances 3
instInhabitedModel : Inhabited Model
instReprModel : Repr Model
instInhabitedVList : Inhabited VList
Searching
Heights: the specification
Heights: the fast path
The view needs a row's top for a handful of rows per frame. topF finds how many known rows lie
above it by binary search and adds their corrections from a prefix sum (Model.pre, built once
per frame), so it costs O(log known) whatever the list's length.