-- allium: 1
-- bDS Project Management
-- Scope: core (Wave 1)
-- Distilled from: src/main/engine/ProjectEngine.ts, schema.ts

surface ProjectControlSurface {
    facing _: ProjectOperator

    provides:
        CreateProjectRequested(name, data_path)
        OpenProjectRequested(folder_path)
        SetActiveProjectRequested(project)
        DeleteProjectRequested(project)
}

entity Project {
    name: String
    slug: String
    description: String?
    data_path: String?
    is_active: Boolean
    created_at: Timestamp
    updated_at: Timestamp

    -- Relationships
    posts: Post with project = this
    media: Media with project = this
    tags: Tag with project = this

    -- Derived
    --
    -- data_path is the project folder: the directory that CONTAINS
    -- meta/project.json. It is DISCOVERED from the project.json location at
    -- load time and is never written into project.json itself — so the folder
    -- can be moved/renamed freely. The current location is remembered only as a
    -- machine-local pointer (a project registry under private_dir), never
    -- embedded in the portable project. See DataPathNotPersistedInProjectJson.
    public_dir: data_path
        -- All user-owned, portable, webserver-bound content lives here, under
        -- the project folder:
        --   posts (.md), media + thumbnails, templates/, scripts/,
        --   meta/ (project.json, categories.json, category-meta.json,
        --   publishing.json), tags.json, menu.opml, and generated html/ output.
        -- See PublicContentLivesInProjectFolder.
    private_dir: String
        -- The OS per-user app-data directory. Holds app-internal,
        -- machine-specific, regenerable artifacts ONLY — never inside the repo
        -- or the project folder:
        --   the SQLite database, the per-project embeddings index
        --   (projects/{id}/embeddings.usearch + .meta.json sidecar), the
        --   downloaded embedding-model cache, the project registry, and
        --   window/UI state.
        -- OS-specific base (resolved via :filename.basedir, app name "bds"):
        --   macOS:   ~/Library/Application Support/bds   (:user_config)
        --   Linux:   $XDG_CONFIG_HOME/bds  (default ~/.config/bds)
        --   Windows: %APPDATA%\\bds
        -- See PrivateArtifactsLiveInOsAppDir.
}

surface ProjectSurface {
    context project: Project

    exposes:
        project.name
        project.slug
        project.description when project.description != null
        project.data_path when project.data_path != null
        project.is_active
        project.created_at
        project.updated_at
        project.posts.count
        project.media.count
        project.tags.count
        project.public_dir
        project.private_dir
}

invariant SingleActiveProject {
    -- Exactly one project is active at any time
    let active = Projects where is_active
    active.count = 1
}

invariant UniqueProjectSlug {
    for a in Projects:
        for b in Projects:
            a != b implies a.slug != b.slug
}

rule CreateProject {
    when: CreateProjectRequested(name, data_path)
    let slug = slugify(name)
    ensures: Project.created(
        name: name,
        slug: slug,
        data_path: data_path,
        is_active: false
    )
    @guidance
        -- data_path is the chosen project folder. CreateProject writes
        -- meta/project.json into {data_path}/meta/ but never records data_path
        -- inside it (DataPathNotPersistedInProjectJson). The default project's
        -- folder is created at a per-user default content location on first
        -- launch — never inside the application repo or private_dir.
}

rule DiscoverProjectDataPath {
    -- Opening or loading a project folder deduces its data_path from the
    -- on-disk location of meta/project.json rather than from any stored value,
    -- keeping projects movable (DataPathNotPersistedInProjectJson).
    when: OpenProjectRequested(folder_path)
        -- folder_path contains meta/project.json
    let project = Projects where data_path = folder_path
    ensures: project.data_path = folder_path
}

invariant ProjectTemplatesDirectoryReservedForUserTemplates {
    -- The project templates directory stores only user-managed templates.
    -- Creating a project does not populate public_dir/templates with bundled defaults.
}

invariant PublicContentLivesInProjectFolder {
    -- Every file the user owns or that must be served by the webserver lives
    -- under public_dir (= the project folder containing meta/project.json):
    -- posts, media + thumbnails, templates, scripts, the meta/ JSON files,
    -- tags.json, menu.opml, and the generated html/ output. None of this
    -- content is ever written to private_dir or into the application repo.
}

invariant PrivateArtifactsLiveInOsAppDir {
    -- App-internal, machine-specific, regenerable artifacts — the SQLite
    -- database, the per-project embeddings index and its sidecar, the
    -- model cache, the project registry, and window/UI state — live ONLY
    -- under private_dir (the OS per-user app-data directory). They are never
    -- written into a project folder (public_dir) or into the application repo.
    -- A regenerable artifact (e.g. the embeddings index) may be rebuilt from
    -- the database when absent.
}

invariant DataPathNotPersistedInProjectJson {
    -- meta/project.json never stores its own path or data_path. A project's
    -- location is determined solely by where its meta/project.json file sits,
    -- so the folder can be moved or renamed without editing any file. The app
    -- remembers the current location as a machine-local pointer in private_dir.
}

rule SetActiveProject {
    when: SetActiveProjectRequested(project)
    let previous = Projects where is_active = true
    ensures:
        for p in previous:
            p.is_active = false
    ensures: project.is_active = true
}

rule DeleteProject {
    when: DeleteProjectRequested(project)
    requires: project.id != "default"
        -- The default project (id='default') cannot be deleted
    requires: project.is_active = false
        -- The currently active project cannot be deleted
    ensures: not exists project
    @guidance
        -- deleteProjectWithData removes DB rows + internal directory
        -- but preserves external data at custom data_path
}

config {
    default_project_id: String = "default"
    default_project_name: String = "My Blog"
}

invariant DefaultProjectExists {
    -- A project with id='default' always exists
    -- It is created on first launch if missing
    exists p in Projects where p.id = "default"
}