Cairn · module

Cairn.Frame.Menu

lean/Cairn/Frame/Menu.lean

Frame.ofMenu: a status item's menu description becomes the flat list of menu records the frame carries (docs/frame.md, "Menu records"), parents before children, as the accessibility list is.

Theorems: controls_ofMenu (the records' controls are exactly the description's actionable items, in order: what the host's NSMenu is built from is what the presence and enablement proofs are about), enabled_ofMenu (likewise for the enabled ones) and parent_lt_ofMenu (every parent index points at an earlier record, and at a submenu).

Imports Cairn.Frame

Order

Definitions 9

def

Cairn.Frame.menuRecord

lean/Cairn/Frame/Menu.lean:21
menuRecord (parent : Option Nat) : MenuItem → MenuRecord

The record for one item, without its children.

def

Cairn.Frame.menuOf

lean/Cairn/Frame/Menu.lean:31
menuOf (parent : Option Nat) (acc : Array MenuRecord) :
  MenuItem → Array MenuRecord

Append the records of an item (and, for a submenu, its children) to acc.

def

Cairn.Frame.menuAll

lean/Cairn/Frame/Menu.lean:36
menuAll (parent : Option Nat) (acc : Array MenuRecord) :
  List MenuItem → Array MenuRecord
def

Cairn.Frame.ofMenu

lean/Cairn/Frame/Menu.lean:42
ofMenu (items : List MenuItem) : Array MenuRecord

A menu description, flattened.

def

Cairn.Frame.ofStatus

lean/Cairn/Frame/Menu.lean:45
ofStatus (it : StatusItem) : StatusFrame

What a status item puts on the frame.

def

Cairn.Frame.MenuRecord.ctl

lean/Cairn/Frame/Menu.lean:50
ctl (r : MenuRecord) : Option ControlRef

The control of an actionable record.

def

Cairn.Frame.MenuRecord.enabledCtl

lean/Cairn/Frame/Menu.lean:53
enabledCtl (r : MenuRecord) : Option ControlRef

The control of an enabled actionable record.

def

Cairn.Frame.MenuParentsOk

lean/Cairn/Frame/Menu.lean:136
MenuParentsOk (ms : Array MenuRecord) : Prop

Every record's parent is an earlier record, and a submenu.

def

Cairn.Frame.MenuParentBelow

lean/Cairn/Frame/Menu.lean:139
MenuParentBelow (ms : Array MenuRecord) (parent : Option Nat) : Prop

Theorems 14

theorem

Cairn.Frame.menuOf_controls

provedlean/Cairn/Frame/Menu.lean:59
menuOf_controls (parent : Option Nat) (acc : Array MenuRecord) (m : MenuItem) :
  List.filterMap MenuRecord.ctl (menuOf parent acc m).toList =
    List.filterMap MenuRecord.ctl acc.toList ++ m.refsOf
theorem

Cairn.Frame.menuAll_controls

provedlean/Cairn/Frame/Menu.lean:77
menuAll_controls (parent : Option Nat) (acc : Array MenuRecord)
  (ms : List MenuItem) :
  List.filterMap MenuRecord.ctl (menuAll parent acc ms).toList =
    List.filterMap MenuRecord.ctl acc.toList ++ MenuItem.refs ms
theorem

Cairn.Frame.controls_ofMenu

provedlean/Cairn/Frame/Menu.lean:89
controls_ofMenu (items : List MenuItem) :
  List.filterMap MenuRecord.ctl (ofMenu items).toList = MenuItem.refs items

The menu on the frame is the menu described. The controls of the frame's menu records are exactly the description's actionable items, in order.

theorem

Cairn.Frame.menuOf_enabled

provedlean/Cairn/Frame/Menu.lean:94
menuOf_enabled (parent : Option Nat) (acc : Array MenuRecord) (m : MenuItem) :
  List.filterMap MenuRecord.enabledCtl (menuOf parent acc m).toList =
    List.filterMap MenuRecord.enabledCtl acc.toList ++ m.enabledRefsOf
theorem

Cairn.Frame.menuAll_enabled

provedlean/Cairn/Frame/Menu.lean:117
menuAll_enabled (parent : Option Nat) (acc : Array MenuRecord)
  (ms : List MenuItem) :
  List.filterMap MenuRecord.enabledCtl (menuAll parent acc ms).toList =
    List.filterMap MenuRecord.enabledCtl acc.toList ++ MenuItem.enabledRefs ms
theorem

Cairn.Frame.enabled_ofMenu

provedlean/Cairn/Frame/Menu.lean:129
enabled_ofMenu (items : List MenuItem) :
  List.filterMap MenuRecord.enabledCtl (ofMenu items).toList = MenuItem.enabledRefs items

The enabled records' controls are exactly the description's enabled items: what the host greys out is what Lean will refuse (Runtime.menu_select_stale).

theorem

Cairn.Frame.MenuParentBelow.push

provedlean/Cairn/Frame/Menu.lean:142
push {ms : Array MenuRecord} {parent : Option Nat}
  (h : MenuParentBelow ms parent) (x : MenuRecord) : MenuParentBelow (ms.push x) parent
theorem

Cairn.Frame.MenuParentsOk.push

provedlean/Cairn/Frame/Menu.lean:148
push {ms : Array MenuRecord} {x : MenuRecord}
  (h : MenuParentsOk ms) (hx : MenuParentBelow ms x.parent) : MenuParentsOk (ms.push x)
theorem

Cairn.Frame.menuOf_prefix

provedlean/Cairn/Frame/Menu.lean:164
menuOf_prefix (parent : Option Nat) (acc : Array MenuRecord) (m : MenuItem) :
  ∃ hs, ∀ (i : Nat) (hi : i < acc.size), (menuOf parent acc m)[i] = acc[i]
theorem

Cairn.Frame.menuAll_prefix

provedlean/Cairn/Frame/Menu.lean:178
menuAll_prefix (parent : Option Nat) (acc : Array MenuRecord)
  (ms : List MenuItem) :
  ∃ hs, ∀ (i : Nat) (hi : i < acc.size), (menuAll parent acc ms)[i] = acc[i]
theorem

Cairn.Frame.MenuParentBelow.mono

provedlean/Cairn/Frame/Menu.lean:191
mono {ms ms' : Array MenuRecord} {parent : Option Nat}
  (h : MenuParentBelow ms parent) (hs : ms.size ≤ ms'.size)
  (he : ∀ (i : Nat) (hi : i < ms.size), ms'[i] = ms[i]) : MenuParentBelow ms' parent
theorem

Cairn.Frame.menuOf_parents

provedlean/Cairn/Frame/Menu.lean:200
menuOf_parents (parent : Option Nat) (acc : Array MenuRecord) (m : MenuItem)
  (h : MenuParentsOk acc) (hp : MenuParentBelow acc parent) :
  MenuParentsOk (menuOf parent acc m)
theorem

Cairn.Frame.menuAll_parents

provedlean/Cairn/Frame/Menu.lean:217
menuAll_parents (parent : Option Nat) (acc : Array MenuRecord)
  (ms : List MenuItem) (h : MenuParentsOk acc) (hp : MenuParentBelow acc parent) :
  MenuParentsOk (menuAll parent acc ms)
theorem

Cairn.Frame.parent_lt_ofMenu

provedlean/Cairn/Frame/Menu.lean:230
parent_lt_ofMenu (items : List MenuItem) : MenuParentsOk (ofMenu items)

Parents first. Every menu record's parent is an earlier record and a submenu, so the host builds the NSMenu tree in one pass.