Cairn.Layout.Rigid
lean/Cairn/Layout/Rigid.lean
Rigid views: pressable at every size they fit, for every state
Layout/Check.lean proves a view pressable by evaluating its layout, which works for one
concrete state, window and set of metrics. An app with a list of any length needs the same
fact for all of them. This file gives a structural condition, FitsIn n w h, under which a
view laid out in a w × h rect satisfies every per-node condition of Pressable and every
control has a nonempty rect, for all text metrics.
The idea: in a rigid view every box and field is fixed or fill on both axes, never
hug, so no rect depends on how wide a string is. Text appears only inside boxes that clip
and hold nothing but text (Fits exempts those: the text may overflow, the clip contains it).
Then each child's size is known from its parent's alone:
- on the cross axis,
fixed ngetsnandfillgets the content box's length; - on the main axis,
fixed ngetsn, andfillgets a share of the leftover space, at least⌊leftover / fills⌋(fillShare_ge).
FitsIn asks, node by node, that the fixed children and gaps fit, that each child fits at the
size it will get, and that controls have positive size. fitsIn_arrange proves the rest;
hitTest_center_of_fitsIn turns it into "hit testing at the centre of every control returns
that control". Positions never appear, so a list of k identical rows is handled by one
argument about one row.
Imports Cairn.Layout.Check
Inductive types 1
FitsIn : Node → Int → Int → Prop
FitsIn n w h: laid out in a w × h rect, n and everything below it fit, and its
controls have positive size. Three shapes:
- wrapped text (a clipping column of lines, with no controls);
- a field of positive size;
- a box that clips and holds only text (a label: the text may overflow; the clip holds it);
- a row or column whose children are all
fixedorfillon both axes, whose fixed main-axis lengths and gaps fit its content box, whose fixed cross-axis lengths fit too, and whose every child fits at the size it will get. Afillchild on the main axis must fit at every length from⌊leftover / fills⌋up. A box with a control has no controls below it.
para {ts : TextStyle} {wr : Wrap} {s : String} {w h : Int} :
FitsIn (Node.para ts wr s) w hWrapped text always fits: it is a clipping column of text with no controls.
field {st : Style} {ts : TextStyle} {c : Control} {v : FieldView}
{w h : Int} : 0 < w → 0 < h → FitsIn (Node.field st ts c v) w hclipped {st : Style} {ctl : Option Control} {kids : List Node}
{w h : Int} :
st.clip = true →
(∀ (k : Node), k ∈ kids → k.isText = true) →
(ctl.isSome = true → 0 < w ∧ 0 < h) → FitsIn (Node.box st ctl kids) w hline {st : Style} {ctl : Option Control} {kids : List Node}
{w h : Int} :
st.axis ≠ Axis.stack →
PadOk st.padding →
0 ≤ contentW st w →
0 ≤ contentH st h →
(ctl.isSome = true → 0 < w ∧ 0 < h ∧ Node.controlsList kids = []) →
(st.scroll = none →
lineBase (Axis.horiz st.axis) st.gap kids ≤
mainIn (Axis.horiz st.axis) st w h) →
(∀ (k : Node),
k ∈ kids →
(nodeSizings k).fst.isHug = false ∧
(nodeSizings k).snd.isHug = false ∧
fixedOf (crossSz (Axis.horiz st.axis) k) ≤
crossIn (Axis.horiz st.axis) st w h) →
(∀ (k : Node),
k ∈ kids →
∀ (len : Int),
(mainSz (Axis.horiz st.axis) k = Sizing.fill →
(mainIn (Axis.horiz st.axis) st w h -
lineBase (Axis.horiz st.axis) st.gap kids) /
↑(lineFills (Axis.horiz st.axis) kids) ≤
len) →
(∀ (n : Nat),
mainSz (Axis.horiz st.axis) k = Sizing.fixed n → len = ↑n) →
FitsIn k
(wOf (Axis.horiz st.axis) len
(lenIn (crossSz (Axis.horiz st.axis) k)
(crossIn (Axis.horiz st.axis) st w h)))
(hOf (Axis.horiz st.axis) len
(lenIn (crossSz (Axis.horiz st.axis) k)
(crossIn (Axis.horiz st.axis) st w h)))) →
FitsIn (Node.box st ctl kids) w hDefinitions 19
nodeSizings : Node → Sizing × Sizing
A node's sizing on each axis (text hugs).
isText : Node → Bool
isHug : Sizing → Bool
lenIn (s : Sizing) (offer : Int) : Int
The length a non-hug sizing gets when its parent offers offer.
fixedOf (s : Sizing) : Int
What a sizing asks for before leftover space is shared (fill asks for nothing).
mainSz (horiz : Bool) (k : Node) : Sizing
crossSz (horiz : Bool) (k : Node) : Sizing
lineBase (horiz : Bool) (gap : Nat) (kids : List Node) : Int
The fixed main-axis lengths of a line's children, plus its gaps.
lineFills (horiz : Bool) (kids : List Node) : Nat
How many of a line's children fill the main axis.
PadOk (p : Insets) : Prop
contentW (st : Style) (w : Int) : Int
contentH (st : Style) (h : Int) : Int
mainIn (horiz : Bool) (st : Style) (w h : Int) : Int
crossIn (horiz : Bool) (st : Style) (w h : Int) : Int
wOf (horiz : Bool) (main cross : Int) : Int
Width and height from main- and cross-axis lengths.
hOf (horiz : Bool) (main cross : Int) : Int
NodeOk (l : Laid) : Prop
What Pressable asks at each node.
exampleRow (i : Nat) (label : String) : Node
exampleList (labels : List String) : Node
Theorems 27
le_sum_of_mem {l : List Int} (h : ∀ (x : Int), x ∈ l → 0 ≤ x) {x : Int}
(hx : x ∈ l) : x ≤ l.sum
measure_sizings (m : TextMetrics) (aw : Int) (n : Node) : (measure m aw n).sizings = nodeSizings n
measureList_eq_map (m : TextMetrics) (aw : Int) (ks : List Node) : measureList m aw ks = List.map (measure m aw) ks
mem_arrangeList (m : TextMetrics) (aw : Int) (c : Rect) (rs : List Rect) (ks : List Node) : rs.length = ks.length → ∀ (k' : Laid), k' ∈ arrangeList m c rs (List.map (measure m aw) ks) → ∃ p, p ∈ ks.zip rs ∧ k' = arrange m c p.snd (measure m aw p.fst)
With one rect per child, each laid-out child is its node arranged in its rect.
go_lens (ln : Line) (its : List Item) (i j : Nat) (pos : Int) (p : Item × Rect) : p ∈ its.zip (ln.go i j pos its) → (∃ j', mainOf ln.horiz p.snd = mainSize ln.horiz ln.L ln.f j' p.fst) ∧ crossOf ln.horiz p.snd = (crossPlace ln.align ln.c0 ln.cc (Item.crossSizing ln.horiz p.fst) (Item.crossPref ln.horiz p.fst) p.fst.stretch).snd
The main- and cross-axis lengths Line.go gives each item.
item_sizing (m : TextMetrics) (aw : Int) (h : Bool) (k : Node) : Item.mainSizing h (measure m aw k).item = mainSz h k ∧ Item.crossSizing h (measure m aw k).item = crossSz h k
A rigid child's item: its sizings are its node's.
mainSize_fill {h : Bool} {L : Int} {f j : Nat} {it : Item}
(hs : Item.mainSizing h it = Sizing.fill) : mainSize h L f j it = fillShare L f j
mainSize_fixed {h : Bool} {L : Int} {f j n : Nat} {it : Item}
(hs : Item.mainSizing h it = Sizing.fixed n) : mainSize h L f j it = ↑n
crossPlace_len (al : Align) (c0 cc : Int) (s : Sizing) (p : Int) (b : Bool) (hh : s.isHug = false) : (crossPlace al c0 cc s p b).snd = lenIn s cc
baseSum_rigid (h : Bool) (m : TextMetrics) (aw : Int) (ks : List Node) : (∀ (k : Node), k ∈ ks → (mainSz h k).isHug = false) → baseSum h (List.map (fun k => (measure m aw k).item) ks) = (List.map (fun k => fixedOf (mainSz h k)) ks).sum
fillCount_eq (h : Bool) (m : TextMetrics) (aw : Int) (ks : List Node) : fillCount h (List.map (fun k => (measure m aw k).item) ks) = lineFills h ks
mainSz_hug (h : Bool) (k : Node) (h1 : (nodeSizings k).fst.isHug = false) (h2 : (nodeSizings k).snd.isHug = false) : (mainSz h k).isHug = false ∧ (crossSz h k).isHug = false
childRects_line (st : Style) (r : Rect) (items : List Item) (hax : st.axis ≠ Axis.stack) : childRects st r items = scrolled st (lineRects (Axis.horiz st.axis) st (r.inset st.padding) items)
rect_wh (h : Bool) (q : Rect) : q.w = wOf h (mainOf h q) (crossOf h q) ∧ q.h = hOf h (mainOf h q) (crossOf h q)
mainOf_content (h : Bool) (st : Style) (r : Rect) : mainOf h (r.inset st.padding) = mainIn h st r.w r.h ∧ crossOf h (r.inset st.padding) = crossIn h st r.w r.h
text_ok (m : TextMetrics) (aw : Int) (c r : Rect) {k : Node} (hk : k.isText = true) : Laid.Everywhere NodeOk (arrange m c r (measure m aw k)) ∧ (arrange m c r (measure m aw k)).isText = true ∧ (arrange m c r (measure m aw k)).controls = []
controlsList_nil_of {ls : List Laid}
(h : ∀ (l : Laid), l ∈ ls → l.controls = []) : Laid.controlsList ls = []
mem_targetsList {t : Runtime.Target} {ls : List Laid} :
t ∈ Runtime.targetsList ls → ∃ l, l ∈ ls ∧ t ∈ Runtime.targetsOf l
arrangeList_texts (m : TextMetrics) (c : Rect) (rs : List Rect) (ss : List Sized) : (∀ (s : Sized), s ∈ ss → ∃ ts str sz, s = Sized.text ts str sz) → ∀ (k : Laid), k ∈ arrangeList m c rs ss → Laid.Everywhere NodeOk k ∧ k.isText = true ∧ k.controls = []
Arranged lines of text are text with nothing below them.
para_ok (m : TextMetrics) (ts : TextStyle) (wr : Wrap) (s : String) (aw : Int) (c r : Rect) : Laid.Everywhere NodeOk (arrange m c r (measure m aw (Node.para ts wr s))) ∧ ∀ (t : Runtime.Target), t ∈ Runtime.targetsOf (arrange m c r (measure m aw (Node.para ts wr s))) → t.node.rect.nonempty
Wrapped text lays out as a clipping column of text: it meets Pressable's conditions and
has no controls.
fitsIn_arrange (m : TextMetrics) {n : Node} {w h : Int} (hf : FitsIn n w h) (aw : Int) (c r : Rect) : r.w = w → r.h = h → Laid.Everywhere NodeOk (arrange m c r (measure m aw n)) ∧ ∀ (t : Runtime.Target), t ∈ Runtime.targetsOf (arrange m c r (measure m aw n)) → t.node.rect.nonempty
Rigid views lay out pressably. If n fits in w × h, then laid out in any rect of that
size, with any clip and any text metrics, every node meets Pressable's per-node conditions
and every control's rect is nonempty.
pressable_of_fitsIn {m : TextMetrics} {w : Size} {st : Style}
{ctl : Option Control} {kids : List Node} (hw : st.width = Sizing.fill)
(hh : st.height = Sizing.fill)
(hf : FitsIn (Node.box st ctl kids) (max 0 w.w) (max 0 w.h)) :
Pressable w (layout m w (Node.box st ctl kids))A rigid root that fills the window and fits in it lays out pressable.
hitTest_center_of_fitsIn {m : TextMetrics} {w : Size} {st : Style}
{ctl : Option Control} {kids : List Node} (hw : st.width = Sizing.fill)
(hh : st.height = Sizing.fill)
(hf : FitsIn (Node.box st ctl kids) (max 0 w.w) (max 0 w.h)) (t : Runtime.Target) :
t ∈ Runtime.targets (layout m w (Node.box st ctl kids)) →
t.visible.nonempty →
Runtime.hitTest (layout m w (Node.box st ctl kids)) t.visible.center = some t.controlPressable, for a rigid root. If the root fills the window and fits in it, every control
of the laid-out view with a visible part is pressable at that part's centre, for every text
metrics. (Outside a scroll box the visible part is the whole rect: visible_eq_rect.)
hitTest_center_of_fitsIn_flat {m : TextMetrics} {w : Size} {st : Style}
{ctl : Option Control} {kids : List Node} (hw : st.width = Sizing.fill)
(hh : st.height = Sizing.fill)
(hf : FitsIn (Node.box st ctl kids) (max 0 w.w) (max 0 w.h))
(hs : (Node.box st ctl kids).scrolls = false) (t : Runtime.Target) :
t ∈ Runtime.targets (layout m w (Node.box st ctl kids)) →
Runtime.hitTest (layout m w (Node.box st ctl kids)) t.visible.center = some t.controlPressable, for a rigid root without scroll boxes: then every control is visible whole, so every control of the laid-out view is pressable at its centre, for every text metrics.
exampleList_fitsIn (labels : List String) {w h : Int} (hw : 0 < w) (hh : 44 * ↑labels.length ≤ h) : FitsIn (exampleList labels) w h
exampleList_pressable (m : TextMetrics) (labels : List String) (w : Size) (hw : 0 < w.w) (hh : 44 * ↑labels.length ≤ w.h) (t : Runtime.Target) : t ∈ Runtime.targets (layout m w (exampleList labels)) → Runtime.hitTest (layout m w (exampleList labels)) t.visible.center = some t.control
Every button in a list of any length is pressable at its centre, with any metrics.
The condition
Arithmetic
Measure and arrange, for rigid children
The theorem
Example: a list of any length
A column of k buttons, each a clipped 44-point row holding a label. Every button is pressable
at its centre, for every text metrics, whenever the window is wider than zero and at least
44 * k tall. The proof never looks at a particular k or a particular label.