-- allium: 1
-- bDS Navigation Menu
-- Scope: core (read for rendering), extension Bucket F (menu editor UI)
-- File-only model: no DB table. Loaded from meta/menu.opml into a
-- transient value, mutated in memory, written back to OPML on save.

surface MenuManagementSurface {
    facing _: MenuOperator

    provides:
        MenuLoadRequested(project_id)
        UpdateMenuRequested(items)
        SyncMenuFromFilesystemRequested(project_id)
}

surface MenuEditorSurface {
    facing _: MenuOperator

    provides:
        MenuEditorOpened(project_id)
        MenuEntryDraftRequested(menu, selected_item, kind)
        MenuEntryDraftCompleted(menu, selection_or_label)
        MenuEntryDraftCancelled(menu)
        MenuTreeEditRequested(menu, selected_item, operation, target_item, drop_position)
        UpdateMenuRequested(items)

    @guarantee EntryCreation
        -- A new page/category draft is inserted directly after the selected
        -- item, or as the first child when a submenu is selected. A page draft
        -- can select an existing page; submitting free text instead creates a
        -- submenu. A category draft can select an existing category or create
        -- a new category from non-empty free text. Cancelling removes the draft.

    @guarantee TreeEditing
        -- Entries may move among siblings, indent only beneath a preceding
        -- submenu, unindent to immediately after their parent, or be dragged
        -- before/after an entry or inside a submenu. A drop onto itself, one of
        -- its descendants, or inside a non-submenu has no effect.

    @guarantee HomeProtection
        -- The canonical Home entry cannot be moved, indented, unindented,
        -- deleted, or dragged. Those actions are unavailable while it is
        -- selected and remain no-ops if invoked indirectly.

    @guarantee SaveFeedback
        -- Save persists the current normalized tree through UpdateMenu and
        -- informs the operator that the blog menu was saved.
}

value MenuItem {
    kind: page | submenu | category_archive | home
    label: String
    slug: String?                   -- pageSlug for page/home, categoryName for category_archive
    children: List<MenuItem>?       -- present only for submenu kind
}

value Menu {
    items: List<MenuItem>

    -- Derived
    home_entry: items.first         -- always home after normalization
}

surface MenuSurface {
    context menu: Menu

    exposes:
        menu.items.count
        menu.home_entry.label
}

invariant HomeAlwaysFirst {
    -- Normalization guarantees home is always the first item.
    -- UpdateMenu strips any home entries from input, then prepends one.
    for menu in Menus:
        menu.items.first.kind = home
}

invariant MenuPersistedAsOpml {
    -- meta/menu.opml is the sole persistent store (no DB table).
    -- OPML outline attributes: text (label), type (kind),
    --   pageSlug (slug for page/home), categoryName (slug for category_archive).
    -- Nested <outline> elements represent submenu children.
    -- The head title is the project name. dateCreated and dateModified both use
    -- the project's updated timestamp, falling back to created timestamp.
    -- Empty outlines have one space before '/>' and the document ends in one
    -- newline, matching bDS2's canonical serializer.
    parse_opml(read_file("meta/menu.opml")) = menu.items
}

rule LoadMenu {
    when: MenuLoadRequested(project_id)
    -- Reads meta/menu.opml; if file missing, returns default (home-only) menu.
    -- Normalizes: strips home entries from body, prepends canonical home.
    ensures: MenuLoaded(project_id, normalize(parse_opml_or_empty(project_id)))
}

rule UpdateMenu {
    when: UpdateMenuRequested(items)
    -- Normalizes Home entry: strips all home items, prepends canonical home.
    -- Writes normalized menu back to meta/menu.opml.
    let without_home = items where kind != home
    ensures: MenuFileWritten(normalize(without_home))
}

rule SyncMenuFromFilesystem {
    when: SyncMenuFromFilesystemRequested(project_id)
    -- Reloads menu from OPML, normalizes, writes back (round-trip repair).
    ensures: MenuLoaded(project_id, _)
    ensures: MenuFileWritten(_)
}

rule OpenMenuEditor {
    when: MenuEditorOpened(project_id)
    ensures: MenuLoaded(project_id, _)
    ensures: MenuEditorReady(project_id)
}

rule StartMenuEntryDraft {
    when: MenuEntryDraftRequested(menu, selected_item, kind)
    requires: kind = page or kind = category_archive
    ensures: MenuDraftInserted(menu, selected_item, kind)
}

rule CompleteMenuEntryDraft {
    when: MenuEntryDraftCompleted(menu, selection_or_label)
    ensures: MenuDraftResolved(menu, selection_or_label)
}

rule CancelMenuEntryDraft {
    when: MenuEntryDraftCancelled(menu)
    ensures: MenuDraftRemoved(menu)
}

rule EditMenuTree {
    when: MenuTreeEditRequested(menu, selected_item, operation, target_item, drop_position)
    ensures: MenuTreePreviewUpdated(menu)
}