Cairn · module
Cairn.Layout.Grid
lean/Cairn/Layout/Grid.lean
Grids: the theorems
About Cairn.Grid (Cairn/UI/Grid.lean), for every box size and every number of cards. The
first four are about the arithmetic alone and are proved in Cairn/UI/Grid.lean itself, which
apps link, so a claim can cite them; the last three are about the layout pass and are here.
- Columns (
columns_pos,columns_fits,le_columns,not_fits_succ): at least one, and the most cards of the minimum width that fit with their gaps. When one fits, every card is at least that wide unless the rows had to shrink to fit the height (minW_le_widthShare). - Aspect (
cardH_aspect): a card's height is its width at the aspect ratio plus the caption whenever the box is tall enough for the captions. - Inside (
cell_inside): every card's rect is inside the box. - Reading order (
cell_before): a later card is in a lower row, or in the same row to the right; so no two cards overlap (cell_disjoint,rects_pairwise). - Layout (
cells_rects): laid out by the ordinary pass,Grid.node's cells land exactly onGrid.rects, wherever the parent puts the grid; its controls are the cards' in the order of the items, at every size (node_controls). - Hit testing (
hitTarget_cell): a point in cardi's rect hits what cardialone would hit: no other card can take it.
Imports Cairn.UI.Grid, Cairn.Layout.Rigid
Order
Definitions 3
cellItem (w h : Nat) : Layout.Item
What a cell offers its row: fixed on both axes at the card's size.
rowRect (g : Grid) (x y : Int) (W H n q : Nat) : Rect
Where row q goes, for a grid whose rect starts at (x, y).
cells (l : Laid) : List Laid
The cells of a laid-out grid: its rows' children, in order.
Theorems 27
chunksAux_flatten {α : Type} (c : Nat) (hc : 1 ≤ c) (fuel : Nat) (xs : List α) :
xs.length ≤ fuel → (chunksAux c fuel xs).flatten = xs
chunks_flatten {α : Type} (c : Nat) (hc : 1 ≤ c) (xs : List α) :
(chunks c xs).flatten = xsChunks keep the order: the rows, read one after another, are the items.
go_uniform (ln : Layout.Line) (it : Layout.Item) (a b gap : Nat) (hsp : ∀ (i : Nat), ln.spacing i = ↑gap) (hm : Layout.Item.mainSizing ln.horiz it = Sizing.fixed a) (hc : Layout.Item.crossSizing ln.horiz it = Sizing.fixed b) (hal : ln.align = Align.start) (its : List Layout.Item) : (∀ (x : Layout.Item), x ∈ its → x = it) → ∀ (i j : Nat) (pos : Int), ln.go i j pos its = List.map (fun q => Layout.mkRect ln.horiz (pos + ↑(q * (a + gap))) (↑a) ln.c0 ↑b) (List.range its.length)
A line of identical items, each fixed on both axes, with constant spacing and start
alignment: item q starts q pitches along.
lineRects_uniform (hz : Bool) (st : Style) (content : Rect) (items : List Layout.Item) (it : Layout.Item) (a b : Nat) (hj : st.justify = Align.start) (hal : st.align = Align.start) (hm : Layout.Item.mainSizing hz it = Sizing.fixed a) (hc : Layout.Item.crossSizing hz it = Sizing.fixed b) (hx : ∀ (x : Layout.Item), x ∈ items → x = it) : Layout.lineRects hz st content items = List.map (fun q => Layout.mkRect hz ((if hz = true then content.x else content.y) + ↑(q * (a + st.gap))) (↑a) (if hz = true then content.y else content.x) ↑b) (List.range items.length)
arrangeList_zipWith (m : TextMetrics) (c : Rect) (rs : List Rect) (ss : List Layout.Sized) : rs.length = ss.length → Layout.arrangeList m c rs ss = List.zipWith (Layout.arrange m c) rs ss
cellNode_item (m : TextMetrics) (aw : Int) (w h : Nat) (k : Node) : (Layout.measure m aw (cellNode w h k)).item = cellItem w h
rowNode_item (g : Grid) (m : TextMetrics) (aw : Int) (W H n : Nat) (cells : List Node) : (Layout.measure m aw (g.rowNode W H n cells)).item = cellItem (g.usedW W H n) (g.cardH W H n)
row_rects (g : Grid) (m : TextMetrics) (aw : Int) (clip : Rect) (x y : Int) (W H n q : Nat) (row : List Node) (hrow : ∀ (k : Node), k ∈ row → ∃ c, k = cellNode (g.cardW W H n) (g.cardH W H n) c) (hlen : row.length ≤ g.columns W) : List.map Laid.rect (Layout.arrange m clip (g.rowRect x y W H n q) (Layout.measure m aw (g.rowNode W H n row))).children = List.map (g.cell x y W H n) (List.range' (q * g.columns W) row.length)
A row of at most columns cells, laid out at row q's rect: its cells land on
cell (q * columns + k).
chunksAux_length_le {α : Type} (c : Nat) (hc : 1 ≤ c) (fuel : Nat)
(xs row : List α) :
row ∈ chunksAux c fuel xs → row.length ≤ c ∧ ∀ (k : α), k ∈ row → k ∈ xs
rows_rects (g : Grid) (m : TextMetrics) (aw : Int) (clip : Rect) (x y : Int) (W H n fuel : Nat) (ys : List Node) (q0 : Nat) : ys.length ≤ fuel → (∀ (k : Node), k ∈ ys → ∃ c, k = cellNode (g.cardW W H n) (g.cardH W H n) c) → List.flatMap (fun l => List.map Laid.rect l.children) (List.zipWith (fun q row => Layout.arrange m clip (g.rowRect x y W H n q) (Layout.measure m aw (g.rowNode W H n row))) (List.range' q0 (chunksAux (g.columns W) fuel ys).length) (chunksAux (g.columns W) fuel ys)) = List.map (g.cell x y W H n) (List.range' (q0 * g.columns W) ys.length)
Rows laid out from row q0 on: their cells land on cell (q0 * columns) onward.
chunks_mem {α : Type} (c : Nat) (hc : 1 ≤ c) (xs row : List α)
(h : row ∈ chunks c xs) : row.length ≤ c ∧ ∀ (k : α), k ∈ row → k ∈ xs
node_children (g : Grid) {α : Type} (m : TextMetrics) (aw : Int) (clip r : Rect) (W H : Nat) (card : Nat → Nat → α → Node) (xs : List α) : (Layout.arrange m clip r (Layout.measure m aw (g.node W H card xs))).children = List.zipWith (fun q row => Layout.arrange m clip (g.rowRect r.x r.y W H xs.length q) (Layout.measure m (Layout.innerAvail (g.style W H xs.length) aw) (g.rowNode W H xs.length row))) (List.range' 0 (chunks (g.columns W) (List.map (fun x => cellNode (g.cardW W H xs.length) (g.cardH W H xs.length) (card (g.cardW W H xs.length) (g.cardH W H xs.length) x)) xs)).length) (chunks (g.columns W) (List.map (fun x => cellNode (g.cardW W H xs.length) (g.cardH W H xs.length) (card (g.cardW W H xs.length) (g.cardH W H xs.length) x)) xs))
The grid laid out in r: its children are its rows, each laid out at its row's rect.
cells_rects (g : Grid) {α : Type} (m : TextMetrics) (aw : Int) (clip r : Rect) (W H : Nat) (card : Nat → Nat → α → Node) (xs : List α) : List.map Laid.rect (cells (Layout.arrange m clip r (Layout.measure m aw (g.node W H card xs)))) = g.rects r.x r.y W H xs.length
The cells land on Grid.rects. Laid out by the ordinary layout pass, wherever its
parent puts it, the grid's cells are exactly rects at the grid's origin, in order.
flatMap_flatten' {α β : Type} (f : α → List β) (L : List (List α)) :
List.flatMap f L.flatten = List.flatMap (fun l => List.flatMap f l) L
flatMap_congr' {α β : Type} {f g : α → List β} {l : List α} :
(∀ (x : α), x ∈ l → f x = g x) → List.flatMap f l = List.flatMap g l
controlsList_eq (ks : List Node) : Node.controlsList ks = List.flatMap Node.controls ks
node_controls (g : Grid) {α : Type} (W H : Nat) (card : Nat → Nat → α → Node) (xs : List α) : (g.node W H card xs).controls = List.flatMap (fun x => (card (g.cardW W H xs.length) (g.cardH W H xs.length) x).controls) xs
Stable order: the grid's controls are its cards' controls, in the order of the items, whatever the box's size; resizing moves cards but never reorders them.
mem_zipWith' {α β γ : Type} {f : α → β → γ} {c : γ} {as : List α} {bs : List β} :
c ∈ List.zipWith f as bs → ∃ a, a ∈ as ∧ ∃ b, b ∈ bs ∧ c = f a b
mem_arrangeList' (m : TextMetrics) (c : Rect) {rs : List Rect} {ss : List Layout.Sized} {x : Laid} : x ∈ Layout.arrangeList m c rs ss → ∃ r s, s ∈ ss ∧ x = Layout.arrange m c r s
hitsList_eq (o : Option Runtime.Target) (ls : List Laid) : Runtime.hitsList o ls = List.flatMap (Runtime.hitsOf o) ls
arrange_clipWithin (m : TextMetrics) (C : Rect) (s : Layout.Sized) (r : Rect) : Laid.Everywhere (fun l => ∀ (p : Point), l.clip.contains p = true → C.contains p = true) (Layout.arrange m C r s)
Every clip in a laid-out subtree lies within the clip it was laid out in.
hits_within {C : Rect} {l : Laid}
(hE :
Laid.Everywhere (fun l => ∀ (p : Point), l.clip.contains p = true → C.contains p = true)
l)
(o : Option Runtime.Target) (e : Runtime.Hit) (p : Point) :
e ∈ Runtime.hitsOf o l → e.visible.contains p = true → C.contains p = trueA hit entry of such a subtree contains only points of that clip.
cellNode_hits (m : TextMetrics) (aw : Int) (clip q : Rect) (w h : Nat) (k : Node) (e : Runtime.Hit) (p : Point) : e ∈ Runtime.hitsOf none (Layout.arrange m clip q (Layout.measure m aw (cellNode w h k))) → e.visible.contains p = true → q.contains p = true
A cell's hit entries contain only points of its rect: it clips its card.
node_hits (g : Grid) {α : Type} (m : TextMetrics) (aw : Int) (clip r : Rect) (W H : Nat) (card : Nat → Nat → α → Node) (xs : List α) : have l := Layout.arrange m clip r (Layout.measure m aw (g.node W H card xs)); Runtime.hitsOf none l = List.flatMap (Runtime.hitsOf none) (cells l) ∧ ∀ (k : Laid), k ∈ cells l → ∀ (e : Runtime.Hit) (p : Point), e ∈ Runtime.hitsOf none k → e.visible.contains p = true → k.rect.contains p = true
The grid's hit entries are its cells', in order: the grid and its rows paint nothing.
find?_flatMap_only {β : Type} (Ls : List β) (f : β → List Runtime.Hit)
(q : Runtime.Hit → Bool) (i : Nat) (hi : i < Ls.length)
(h :
∀ (j : Nat) (hj : j < Ls.length),
j ≠ i → ∀ (e : Runtime.Hit), e ∈ f Ls[j] → q e = false) :
List.find? q (List.flatMap f Ls).reverse = List.find? q (f Ls[i]).reverseIf only the i-th list's entries can satisfy q, the topmost of the concatenation that
does is the i-th's.
cells_length (g : Grid) {α : Type} (m : TextMetrics) (aw : Int) (clip r : Rect) (W H : Nat) (card : Nat → Nat → α → Node) (xs : List α) : (cells (Layout.arrange m clip r (Layout.measure m aw (g.node W H card xs)))).length = xs.length
hitTarget_cell (g : Grid) {α : Type} (m : TextMetrics) (aw : Int) (clip r : Rect) (W H : Nat) (card : Nat → Nat → α → Node) (xs : List α) (i : Nat) (hi : i < xs.length) (p : Point) (hp : (g.cell r.x r.y W H xs.length i).contains p = true) : ∃ k, (cells (Layout.arrange m clip r (Layout.measure m aw (g.node W H card xs))))[i]? = some k ∧ k.rect = g.cell r.x r.y W H xs.length i ∧ Runtime.hitTarget (Layout.arrange m clip r (Layout.measure m aw (g.node W H card xs))) p = Runtime.hitTarget k p
Hit testing finds the cell's controls. A point in card i's rect hits exactly what
card i's cell alone would hit: no other card can take it, and it answers with a control of
that cell or nothing.