Cairn · module

Cairn.Layout.VList

lean/Cairn/Layout/VList.lean

Virtual lists: what the layout does with them

Cairn.VList proves which rows a virtual list builds and that, in the heights it lays out by, each row starts where the one before ends (Model.top_succ). This file proves the layout's side: a column with no gap, justified to the start, as every VList.node box is (node_eq), lays its children one under the other, each starting where the one before it ends, the first at the top of its content box less the offset, whatever the children's heights.

  • Stacked: rects one under the other from y, with no gaps and no overlaps.
  • arrange_stacked: such a box's laid children are Stacked from its content top less the offset.
  • vlist_stacked: so are a laid VList.node's: the spacer for the rows above, the rows in key order, and the spacer for the rows below.

Imports Cairn.Layout.Proofs, Cairn.VList

Order

Definitions 2

def

Cairn.Layout.Stacked

lean/Cairn/Layout/VList.lean:23
Stacked : List Rect → Int → Prop

rs lie one under the other from y: the first starts at y, each next one where the one before it ends.

def

Cairn.Layout.VList_checks.knownAt3

lean/Cairn/Layout/VList.lean:91
knownAt3 : VList.Known

Theorems 4

theorem

Cairn.Layout.Line.go_stacked

provedlean/Cairn/Layout/VList.lean:27
go_stacked (ln : Line) (hz : ln.horiz = false)
  (hs : ∀ (i : Nat), ln.spacing i = 0) (items : List Item) (i j : Nat) (pos : Int) :
  Stacked (ln.go i j pos items) pos
theorem

Cairn.Layout.stacked_map

provedlean/Cairn/Layout/VList.lean:34
stacked_map (o : Int) (rs : List Rect) (y : Int) :
  Stacked rs y →
    Stacked (List.map (fun q => { x := q.x, y := q.y - o, w := q.w, h := q.h }) rs) (y - o)
theorem

Cairn.Layout.arrange_stacked

provedlean/Cairn/Layout/VList.lean:46
arrange_stacked (m : TextMetrics) (c r : Rect) {st : Style}
  (ctl : Option Control) (sz : Size) (kids : List Sized) {o : Int} (ho : st.scroll = some o)
  (hcol : st.axis = Axis.column) (hgap : st.gap = 0) (hj : st.justify = Align.start) :
  Stacked (List.map Laid.rect (arrange m c r (Sized.box st ctl sz kids)).children)
    ((r.inset st.padding).y - o)

One under the other. A column scroll box with no gap, justified to the start and scrolled by o, lays its children one under the other: the first at the top of its content box less o, each next where the one before it ends.

theorem

Cairn.Layout.vlist_stacked

provedlean/Cairn/Layout/VList.lean:63
vlist_stacked (m : TextMetrics) (c r : Rect) (aw : Int) (v : VList) (ui : UI)
  (keys : Array Nat) (row : Nat → Node) :
  ∃ st,
    st.rows = some (v.infoOf ui keys) ∧
      st.scroll = some (ui.scrollOf v.ref) ∧
        v.node ui keys row =
            Node.box st none
              (VList.spacer ((v.infoOf ui keys).modelOf.top (v.infoOf ui keys).first) ::
                  VList.rowNodes keys row (v.infoOf ui keys).first
                    (v.infoOf ui keys).last ++
                [VList.spacer
                    ((v.infoOf ui keys).modelOf.top (v.infoOf ui keys).modelOf.count -
                      (v.infoOf ui keys).modelOf.top (v.infoOf ui keys).last)]) ∧
          Stacked
            (List.map Laid.rect
              (arrange m c r (measure m aw (v.node ui keys row))).children)
            ((r.inset st.padding).y - ui.scrollOf v.ref)

A virtual list's rows, laid. However tall its rows turn out, a laid VList.node puts the spacer for the rows above, the rows in key order and the spacer below one under the other, from the top of its content box less the runtime's offset: no gaps, no overlaps.