Cairn.Layout.Facts
lean/Cairn/Layout/Facts.lean
What layout guarantees
The vocabulary for the layout theorems: controls of a tree, a predicate holding at every node
(Laid.Everywhere), the local facts layout establishes at each node, and Facts, the package
the runtime's pressability proof consumes. The theorems are in Cairn.Layout.Proofs.
Imports Cairn.Layout.Core
Structures 1
Facts (m : TextMetrics) (window : Size) (n : Node) (l : Laid) : Prop
Everything layout m window n guarantees about its result l. The runtime's pressability
theorem takes these as hypotheses; Cairn.Layout.facts proves them for every view, window and
valid metrics.
controls : l.controls = n.controls
No control is lost, invented or reordered.
rootClip : l.clip = windowRect window
The root paints within the window.
rootOrigin : l.rect.x = 0 ∧ l.rect.y = 0
The root sits at the origin.
childClips : Laid.Everywhere ChildClips l
clipInside : Laid.Everywhere ClipInside l
rectNonneg : Laid.Everywhere RectNonneg l
siblingsDisjoint : Laid.Everywhere SiblingsDisjoint l
fillExact : Laid.Everywhere FillExact l
childrenInside : Laid.Everywhere ChildrenInside l
clipContained : Laid.Everywhere ClipContained l
caretPlaced : Laid.Everywhere (CaretPlaced m) l
Inductive types 1
Everywhere (P : Laid → Prop) : Laid → Prop
P holds at l and at every node below it.
Definitions 18
controls : Node → List Control
The controls of a view, in paint order (a node before its children, children in order).
controlsList : List Node → List Control
scrolls : Node → Bool
Whether a view has a scroll box anywhere in it.
scrollsList : List Node → Bool
controls : Laid → List Control
The controls of a laid-out tree, in paint order.
controlsList : List Laid → List Control
children : Laid → List Laid
sizings : Laid → Sizing × Sizing
Sizing on each axis (text always hugs).
innerClip : Laid → Rect
The clip a node hands its children: its own, cut down to its rect if it clips.
ChildClips (l : Laid) : Prop
Each child's clip is exactly the clip its parent hands down: the parent's clip, intersected with the parent's rect when the parent clips.
ClipInside (l : Laid) : Prop
The node's clip has non-negative size and contains each child's clip.
RectNonneg (l : Laid) : Prop
The node's rect has non-negative size.
SiblingsDisjoint : Laid → Prop
In a row or column, earlier children end before later ones begin on the main axis, so distinct children's rects are disjoint.
padMain (horiz : Bool) (p : Insets) : Int
Padding along the main axis.
FillExact : Laid → Prop
Fill exactness: in a row or column, if some child fills the main axis and the other children, gaps and padding fit, then children, gaps and padding span the parent exactly. Each child is described by its main-axis sizing and length.
ChildrenInside : Laid → Prop
Children that fit stay inside: in a box that doesn't scroll, if every child's rect is no
larger than the content box and, in a row or column, the children plus gaps fit along the main
axis, then every child's rect is inside the content box. Together with SiblingsDisjoint, this
means nothing in one child's subtree can cover another child, as long as the view fits. (A scroll
box's children are moved by its offset, so they can be anywhere; its clip holds them instead:
ClipContained.)
ClipContained : Laid → Prop
A box that clips (Style.clips, so every scroll box) holds everything below it: every
nonempty visible part (rect ∩ clip) of every node under it is inside its rect.
CaretPlaced (m : TextMetrics) : Laid → Prop
Field geometry: the caret sits at the text origin plus the caret's offset, within the text's extent, is one point wide and a line high, and is inside the content box horizontally whenever the content box is at least one point wide (the text scrolls to keep it there). The selection is empty when collapsed and otherwise runs between the offsets of its ends.
Theorems 2
here {P : Laid → Prop} {l : Laid} : Everywhere P l → P l
child {P : Laid → Prop} {l k : Laid} :
Everywhere P l → k ∈ l.children → Everywhere P k