Cairn.UI.Hit
lean/Cairn/UI/Hit.lean
Hit testing over a laid-out tree.
Paint order is pre-order: a node paints before its children, and children paint in list order,
so later entries are on top. Every node that paints (a box with a background, border or
control, every text run and every field) leaves a hit entry: its visible rect
(rect.inter clip) and its owner, the nearest control at or above it. A point hits the
topmost entry that contains it, and the hit goes to that entry's owner. So a label inside a
button routes to the button, and an opaque panel painted over a button blocks it.
Imports Cairn.UI.Node
Structures 3
Target : Type
A control-bearing node of a laid tree, with its control pulled out.
Hit : Type
LayoutFacts (laid : Laid) (t : Target) : Prop
The facts about a laid tree the pressable theorem needs, for one control t: its visible
rect is nonempty, and a pointer at the centre of that rect reaches it. Layout (workstream B)
proves its trees satisfy these for every control of an enabled move at sizes at or above the
minimum.
nonempty : t.visible.nonempty
reaches : Reaches laid t t.visible.center
Definitions 19
ref (t : Target) : ControlRef
visible (t : Target) : Rect
isField (t : Target) : Bool
focusable (t : Target) : Bool
Fields always take focus; other controls do unless their role is static.
paints (style : Style) (control : Option Control) : Bool
Whether a box leaves a hit entry. Unpainted, control-less boxes are layout only.
hitsOf (o : Option Target) : Laid → List Hit
Hit entries in paint order; o is the owner inherited from the ancestors.
hitsList (o : Option Target) : List Laid → List Hit
targetsOf : Laid → List Target
Every control in the tree, in paint order.
targetsList : List Laid → List Target
hits (laid : Laid) : List Hit
targets (laid : Laid) : List Target
refs (laid : Laid) : List ControlRef
The refs of every control in the tree, in paint order.
present (laid : Laid) (r : ControlRef) : Bool
r names a control in laid.
focusableIn (laid : Laid) (r : ControlRef) : Bool
r names a focusable control in laid.
find (laid : Laid) (r : ControlRef) : Option Target
The first control in paint order with this ref.
hitTarget (laid : Laid) (p : Point) : Option Target
The control a point hits: the owner of the topmost hit entry containing it.
hitTest (laid : Laid) (p : Point) : Option Control
hitRef (laid : Laid) (p : Point) : Option ControlRef
Reaches (laid : Laid) (t : Target) (p : Point) : Prop
t is what a pointer at p reaches: t's own hit entry contains p, and everything
painted after it that also contains p belongs to t (its label, its icon).
Theorems 16
hitsOf_owner (o : Option Target) (l : Laid) (h : Hit) : h ∈ hitsOf o l → h.owner = o ∨ ∃ t, t ∈ targetsOf l ∧ h.owner = some t
hitsList_owner (o : Option Target) (ls : List Laid) (h : Hit) : h ∈ hitsList o ls → h.owner = o ∨ ∃ t, t ∈ targetsList ls ∧ h.owner = some t
targetsOf_control (l : Laid) (t : Target) : t ∈ targetsOf l → t.node.control? = some t.control
targetsList_control (ls : List Laid) (t : Target) : t ∈ targetsList ls → t.node.control? = some t.control
hits_owner_mem {laid : Laid} {h : Hit} {t : Target} (hm : h ∈ hits laid)
(ho : h.owner = some t) : t ∈ targets laidEvery owner of a hit entry is a control of the tree.
hitTarget_mem {laid : Laid} {p : Point} {t : Target}
(h : hitTarget laid p = some t) : t ∈ targets laidThe hit test only ever answers with a control of the tree.
mem_refs {laid : Laid} {t : Target} (h : t ∈ targets laid) : t.ref ∈ refs laid
present_iff {laid : Laid} {r : ControlRef} :
present laid r = true ↔ r ∈ refs laid
find_mem {laid : Laid} {r : ControlRef} {t : Target}
(h : find laid r = some t) : t ∈ targets laid ∧ t.ref = r
hitRef_present {laid : Laid} {p : Point} {r : ControlRef}
(h : hitRef laid p = some r) : r ∈ refs laid
contains_center {r : Rect} (h : r.nonempty) : r.contains r.center = true
find?_reverse_split {α : Type} {q : α → Bool} {pre post : List α} {a : α}
(ha : q a = true) :
∃ b, List.find? q (pre ++ a :: post).reverse = some b ∧ (b = a ∨ b ∈ post ∧ q b = true)The last element satisfying q in pre ++ a :: post is a or comes after it.
hitTarget_of_reaches {laid : Laid} {t : Target} {p : Point}
(h : Reaches laid t p) : hitTarget laid p = some tHit-test level pressability at a point.
reaches_mem {laid : Laid} {t : Target} {p : Point} (h : Reaches laid t p) :
t ∈ targets laid
hitTest_center {laid : Laid} {t : Target} (h : LayoutFacts laid t) :
hitTest laid t.visible.center = some t.controlPressable, hit-test level. Under the layout facts, hit testing at the centre of a control's visible rect returns that control.
contains_center {laid : Laid} {t : Target}
(h : LayoutFacts laid t) : t.visible.contains t.visible.center = true
Instances 2
instInhabitedTarget : Inhabited Target
instInhabitedHit : Inhabited Hit