Cairn.Layout.Bridge
lean/Cairn/Layout/Bridge.lean
From layout facts to the runtime's LayoutFacts
The runtime's pressable theorems (Cairn.Runtime.hitTest_center, click_center_presses) take
Cairn.Runtime.LayoutFacts laid t: the control's visible rect is nonempty and a pointer at its
centre reaches it. This file proves that every control of layout m w n satisfies it, given
four conditions an app can check about its view (Pressable):
- It fits. In every container, padding is non-negative, each child is no larger than the
content box, and in a row or column the children plus gaps fit along the main axis
(
Fits). This is where the minimum window size comes in. A box that clips and holds only text is exempt: its text may overflow (a long title, a label under unusual metrics), but the clip keeps everything it paints inside its rect, and text has no controls. - The root is inside the window.
- Stacks keep controls on top. In a stack, only the last child may contain controls
(
StackTop): earlier children are backgrounds that later ones paint over. - Controls are leaves for hit testing. A box with a control has no controls below it
(
ControlLeaf), so a label inside a button routes to the button.
Then every control whose rect is nonempty is pressable at its centre
(layoutFacts_of_pressable), and indeed at every point of its visible rect
(reaches_of_pressable).
Imports Cairn.Layout.Proofs, Cairn.UI.Hit
Structures 1
Pressable (w : Size) (l : Laid) : Prop
What an app shows about its laid-out view so that every control in it is pressable.
rootInside : l.rect.inside (windowRect w)
fits : Laid.Everywhere Fits l
stackTop : Laid.Everywhere StackTop l
controlLeaf : Laid.Everywhere ControlLeaf l
Definitions 9
isText : Laid → Bool
Fits : Laid → Prop
The children of this container fit in its content box, and its padding is non-negative; or it clips and its children are text, which may overflow it; or it scrolls, its padding is non-negative and its children fit across its axis (along it they may run past the box: the scroll box clips them).
StackTop : Laid → Prop
In a stack, only the last child may contain controls.
ControlLeaf : Laid → Prop
A box with a control has no controls below it.
Good (l : Laid) : Prop
Everything the argument uses at one node.
ReachesIn (hs : List Runtime.Hit) (t : Runtime.Target) (p : Point) : Prop
Reaches, for any list of hit entries.
NoScroll : Laid → Prop
A box that doesn't scroll (text and fields never do).
scrolls : Sized → Bool
Whether a measured view has a scroll box anywhere in it.
scrollsList : List Sized → Bool
Theorems 43
contains_iff (r : Rect) (p : Point) : r.contains p = true ↔ r.x ≤ p.x ∧ p.x < r.x + r.w ∧ r.y ≤ p.y ∧ p.y < r.y + r.h
inter_contains_left {a b : Rect} {p : Point}
(h : (a.inter b).contains p = true) : a.contains p = true
inter_contains_right {a b : Rect} {p : Point}
(h : (a.inter b).contains p = true) : b.contains p = true
contains_of_inside {r o : Rect} {p : Point} (hi : r.inside o)
(h : r.contains p = true) : o.contains p = true
inset_inside (r : Rect) {i : Insets} (ht : 0 ≤ i.top) (hr : 0 ≤ i.right) (hb : 0 ≤ i.bottom) (hl : 0 ≤ i.left) : (r.inset i).inside r
inside_inter {r a b : Rect} (ha : r.inside a) (hb : r.inside b) :
r.inside (a.inter b)
inter_of_inside {r c : Rect} (h : r.inside c) (hw : 0 ≤ r.w)
(hh : 0 ≤ r.h) : r.inter c = r
disjoint_contains {a b : Rect} {p : Point} (hd : a.disjoint b)
(ha : a.contains p = true) (hb : b.contains p = true) : False
hitsList_append (o : Option Runtime.Target) (a b : List Laid) : Runtime.hitsList o (a ++ b) = Runtime.hitsList o a ++ Runtime.hitsList o b
mem_hitsList {o : Option Runtime.Target} {h : Runtime.Hit} {ls : List Laid} :
h ∈ Runtime.hitsList o ls → ∃ k, k ∈ ls ∧ h ∈ Runtime.hitsOf o k
mem_targetsList_split {t : Runtime.Target} {ls : List Laid} :
t ∈ Runtime.targetsList ls → ∃ pre k post, ls = pre ++ k :: post ∧ t ∈ Runtime.targetsOf k
targetsOf_controls (l : Laid) : List.map (fun x => x.control) (Runtime.targetsOf l) = l.controls
targetsList_controls (ls : List Laid) : List.map (fun x => x.control) (Runtime.targetsList ls) = Laid.controlsList ls
targetsOf_eq_nil {l : Laid} (h : l.controls = []) : Runtime.targetsOf l = []
targetsList_eq_nil {ls : List Laid} (h : Laid.controlsList ls = []) :
Runtime.targetsList ls = []
mem_targetsOf_box {t : Runtime.Target} {r c : Rect} {st : Style}
{ctl : Option Control} {kids : List Laid}
(ht : t ∈ Runtime.targetsOf (Laid.box r c st ctl kids)) :
(∃ k, ctl = some k ∧ t = { node := Laid.box r c st ctl kids, control := k }) ∨
t ∈ Runtime.targetsList kids
target {P : Laid → Prop} {l : Laid} (hE : Everywhere P l)
(t : Runtime.Target) : t ∈ Runtime.targetsOf l → P t.nodeA fact holding everywhere holds at every control's node.
child_inside {r c : Rect} {st : Style} {ctl : Option Control}
{kids : List Laid} (hG : Good (Laid.box r c st ctl kids)) (hs : st.scroll = none)
{k : Laid} (hk : k ∈ kids) (hnt : k.isText = false) : k.rect.inside rIn a container that fits and doesn't scroll (and isn't a clipped box of text), each child's rect is inside the container's rect.
child_clip {r c : Rect} {st : Style} {ctl : Option Control}
{kids : List Laid} (hG : Good (Laid.box r c st ctl kids)) (hclips : st.clips = true)
{k : Laid} (hk : k ∈ kids) : k.clip = c.inter rThe clip a clipping box hands its children is its own clip cut down to its rect.
text_hit {r c : Rect} {st : Style} {ctl : Option Control}
{kids : List Laid} (hG : Good (Laid.box r c st ctl kids)) (hs : st.scroll = none)
{k : Laid} (hk : k ∈ kids) (ht : k.isText = true) {o : Option Runtime.Target}
{h : Runtime.Hit} {p : Point} (hh : h ∈ Runtime.hitsOf o k)
(hc : h.visible.contains p = true) : r.contains p = trueA text child's hits are inside its parent's rect when the parent fits or clips.
hits_in_clip {l : Laid} (hE : Laid.Everywhere ClipInside l)
(o : Option Runtime.Target) (h : Runtime.Hit) (p : Point) :
h ∈ Runtime.hitsOf o l → h.visible.contains p = true → l.clip.contains p = trueEvery hit entry in a subtree that contains p lies inside the subtree's root clip.
clipInside {l : Laid} (hE : Everywhere Layout.Good l) :
Everywhere Layout.ClipInside l
hits_inside {l : Laid} (hE : Laid.Everywhere Good l)
(o : Option Runtime.Target) (h : Runtime.Hit) (p : Point) :
h ∈ Runtime.hitsOf o l → h.visible.contains p = true → l.rect.contains p = trueEvery hit entry in a subtree that contains p lies inside the subtree's root rect.
mem_dropLast {α : Type} {pre post : List α} {k k' : α} (h : k' ∈ post) :
k ∈ (pre ++ k :: post).dropLast
reachesIn_of_good {l : Laid} (hE : Laid.Everywhere Good l)
(o : Option Runtime.Target) (t : Runtime.Target) (p : Point) :
t ∈ Runtime.targetsOf l → t.visible.contains p = true → ReachesIn (Runtime.hitsOf o l) t pIn a tree where every node is Good, a pointer anywhere in a control's visible rect reaches
that control.
paraLines_scrolls (m : TextMetrics) (ts : TextStyle) (wr : Wrap) (aw : Int) (s : String) : Sized.scrollsList (paraLines m ts wr aw s) = false
measure_scrolls (m : TextMetrics) (aw : Int) (n : Node) : (measure m aw n).scrolls = n.scrolls
measureList_scrolls (m : TextMetrics) (aw : Int) (ns : List Node) : Sized.scrollsList (measureList m aw ns) = Node.scrollsList ns
arrange_noScroll (m : TextMetrics) (s : Sized) : s.scrolls = false → ∀ (c r : Rect), Laid.Everywhere NoScroll (arrange m c r s)
arrangeList_noScroll (m : TextMetrics) (ss : List Sized) : Sized.scrollsList ss = false → ∀ (c : Rect) (rs : List Rect) (k : Laid), k ∈ arrangeList m c rs ss → Laid.Everywhere NoScroll k
scrollsList_of_forall {ks : List Node} :
(∀ (k : Node), k ∈ ks → k.scrolls = false) → Node.scrollsList ks = false
layout_noScroll (m : TextMetrics) (w : Size) {n : Node} (h : n.scrolls = false) : Laid.Everywhere NoScroll (layout m w n)
A view without scroll boxes lays out without them.
rect_inside_clip {l : Laid} (hE : Laid.Everywhere Good l)
(hns : Laid.Everywhere NoScroll l) :
l.rect.inside l.clip →
∀ (t : Runtime.Target), t ∈ Runtime.targetsOf l → t.node.rect.inside t.node.clipIn a tree where every node is Good, no box scrolls and the root is inside its clip, each
control's rect is inside its clip. (Under a scroll box a control can be anywhere: only its
visible part counts.)
contains_inter {a b : Rect} {p : Point} (ha : a.contains p = true)
(hb : b.contains p = true) : (a.inter b).contains p = true
nonempty_of_contains {r : Rect} {p : Point} (h : r.contains p = true) :
r.nonempty
hits_owner_visible {l : Laid} (hE : Laid.Everywhere Good l)
(o : Option Runtime.Target) (h : Runtime.Hit) (p : Point) :
h ∈ Runtime.hitsOf o l →
h.visible.contains p = true →
h.owner = o ∨ ∃ t, h.owner = some t ∧ t.visible.contains p = trueEvery hit entry in a subtree that contains p belongs to the owner handed down, or to a
control whose visible part contains p.
hitTarget_visible {l : Laid} (hE : Laid.Everywhere Good l) {p : Point}
{t : Runtime.Target} (h : Runtime.hitTarget l p = some t) : t.visible.contains p = trueIn a tree where every node is Good, the hit test answers only with a control whose visible
part contains the point.
layout_good {m : TextMetrics} {w : Size} {n : Node}
(hp : Pressable w (layout m w n)) : Laid.Everywhere Good (layout m w n)
reaches_of_pressable {m : TextMetrics} {w : Size} {n : Node}
(hp : Pressable w (layout m w n)) {t : Runtime.Target}
(ht : t ∈ Runtime.targets (layout m w n)) {p : Point} (hc : t.visible.contains p = true) :
Runtime.Reaches (layout m w n) t pReaching, from layout. If the view is Pressable, a pointer at any point of a control's
visible rect reaches that control.
layoutFacts_of_pressable {m : TextMetrics} {w : Size} {n : Node}
(hp : Pressable w (layout m w n)) {t : Runtime.Target}
(ht : t ∈ Runtime.targets (layout m w n)) (hne : t.visible.nonempty) :
Runtime.LayoutFacts (layout m w n) tThe bridge. If the view is Pressable, every control whose visible part (rect ∩ clip)
is nonempty satisfies the runtime's LayoutFacts: a pointer at the centre of its visible part
reaches it. So Cairn.Runtime.hitTest_center and click_center_presses apply. A control under
a scroll box may be partly or wholly scrolled out: it is pressed at the centre of what shows.
hitTest_center_of_pressable {m : TextMetrics} {w : Size} {n : Node}
(hp : Pressable w (layout m w n)) {t : Runtime.Target}
(ht : t ∈ Runtime.targets (layout m w n)) (hne : t.visible.nonempty) :
Runtime.hitTest (layout m w n) t.visible.center = some t.controlAnd so hit testing at the centre of such a control's visible part returns it.
visible_eq_rect {m : TextMetrics} {w : Size} {n : Node}
(hp : Pressable w (layout m w n)) (hns : Laid.Everywhere NoScroll (layout m w n))
{t : Runtime.Target} (ht : t ∈ Runtime.targets (layout m w n)) : t.visible = t.node.rectWithout scroll boxes, a control's visible part is its whole rect: the root is in the window and every child is inside its parent.