minerva 0.2.0

extern crate alloc;

use alloc::collections::BTreeSet;
use alloc::vec::Vec;
use core::marker::PhantomData;

use super::{DotSet, VersionVector};

mod peek;
mod scoped;

pub use peek::ScopedPeek;
pub use scoped::Scoped;

/// A restriction scope: an invariant lifetime brand tied to one sub-roster,
/// inside which restricted evidence may be compared, and outside of which the
/// comparison does not typecheck.
///
/// A scope is opened by [`with_scope`], which mints a fresh, invariant lifetime
/// `'brand` and hands the body a `Scope<'brand>`. Restricting a vector or a
/// have-set through the scope yields a [`Scoped`] value carrying that same
/// brand, so two values born under different scopes never unify: comparing
/// evidence restricted under different rosters is a compile error, not a
/// discipline the caller must remember.
///
/// The brand is the type-level form of PRD 0013's *created-order hazard*.
/// Restriction preserves order but does not reflect it, so an order verdict on
/// restrictions is order *over the roster*, never order tout court; a caller
/// that compares restrictions from two different rosters and acts as if the
/// verdict were global has fabricated a happens-before out of forgetting. The
/// scope makes that fabrication uncompilable rather than merely documented.
pub struct Scope<'brand> {
    /// The scope's sub-roster, ascending and deduplicated. Restriction into
    /// the scope reads exactly these stations.
    roster: BTreeSet<u32>,
    /// The invariant lifetime brand. `fn(&'brand ()) -> &'brand ()` places
    /// `'brand` in both argument and return position, so the parameter is
    /// invariant and two scopes' brands never unify.
    _brand: PhantomData<fn(&'brand ()) -> &'brand ()>,
}

/// Opens a restriction scope over `roster` and runs `body` inside it.
///
/// The brand is fresh and invariant per invocation: the `for<'brand>` bound
/// forces `body` to accept *any* lifetime the caller of `with_scope` picks, so
/// the concrete `'brand` cannot be named outside and two scopes' values never
/// unify. Comparing evidence restricted under different rosters is therefore a
/// compile error. A [`Scoped`] value also cannot be returned out of `body`
/// while still branded, because its type mentions `'brand`; the lawful exit is
/// [`Scoped::forget`], which drops the brand and hands back a plain value.
///
/// # Type-level proof obligations
///
/// Two scopes' values do not unify, so a cross-scope comparison fails to
/// compile:
///
/// ```compile_fail
/// use minerva::metis::{with_scope, VersionVector};
///
/// let a = VersionVector::new();
/// let b = VersionVector::new();
/// with_scope([1u32], |outer| {
///     let ra = outer.restrict(&a);
///     with_scope([1u32], |inner| {
///         let rb = inner.restrict(&b);
///         // `ra` is branded by `outer`, `rb` by `inner`: the brands are
///         // distinct invariant lifetimes, so this does not typecheck.
///         let _ = ra.happens_before(&rb);
///     });
/// });
/// ```
///
/// A branded value cannot escape its scope: the brand cannot outlive the body:
///
/// ```compile_fail
/// use minerva::metis::{with_scope, Scoped, VersionVector};
///
/// let v = VersionVector::new();
/// // The return type would have to mention the scope's `'brand`, which is
/// // not nameable outside, so this does not typecheck.
/// let escaped: Scoped<'_, VersionVector> =
///     with_scope([1u32], |scope| scope.restrict(&v));
/// let _ = escaped;
/// ```
///
/// Escaping is lawful only after [`Scoped::forget`], which drops the brand:
///
/// ```
/// use minerva::metis::{with_scope, VersionVector};
///
/// let v = VersionVector::new();
/// let forgotten: VersionVector = with_scope([1u32], |scope| scope.restrict(&v).forget());
/// assert_eq!(forgotten, VersionVector::new());
/// ```
///
/// # The intended flow
///
/// Open a scope, restrict two vectors, read a scoped order verdict (sound over
/// the roster), read the concurrency verdict that lawfully escapes unbranded,
/// then forget deliberately when leaving:
///
/// ```
/// use minerva::metis::{with_scope, VersionVector};
///
/// let mut a = VersionVector::new();
/// a.observe(1, 3);
/// a.observe(2, 1);
/// let mut b = VersionVector::new();
/// b.observe(1, 1);
/// b.observe(2, 4);
/// // Globally concurrent: each leads the other on a station.
/// assert!(a.concurrent(&b));
///
/// let (ordered_in_scope, concurrent_globally, forgotten) = with_scope([1u32], |scope| {
///     let ra = scope.restrict(&a);
///     let rb = scope.restrict(&b);
///     // Over station 1 alone, `b` precedes `a`: a verdict sound only here.
///     let ordered = rb.happens_before(&ra);
///     // Concurrency reflects globally, so this bool lawfully leaves the scope.
///     let concurrent = ra.concurrent_globally(&rb);
///     // Leaving forgets where the verdict was valid; the name is the warning.
///     (ordered, concurrent, ra.forget())
/// });
///
/// assert!(ordered_in_scope); // order over the roster, never order tout court
/// assert!(!concurrent_globally); // these restrictions are ordered, not concurrent
/// assert_eq!(forgotten, a.restrict([1u32]));
/// ```
pub fn with_scope<R>(
    roster: impl IntoIterator<Item = u32>,
    body: impl for<'brand> FnOnce(Scope<'brand>) -> R,
) -> R {
    let scope = Scope {
        roster: roster.into_iter().collect(),
        _brand: PhantomData,
    };
    body(scope)
}

impl<'brand> Scope<'brand> {
    /// The scope's roster, ascending.
    pub fn roster(&self) -> impl Iterator<Item = u32> + '_ {
        self.roster.iter().copied()
    }

    /// Restriction into the scope: brands [`VersionVector::restrict`] over this
    /// scope's roster. One of the three constructors of [`Scoped`] values,
    /// with [`restrict_dots`](Self::restrict_dots) and
    /// [`restrict_all`](Self::restrict_all).
    #[must_use]
    pub fn restrict(&self, vector: &VersionVector) -> Scoped<'brand, VersionVector> {
        Scoped {
            value: vector.restrict(self.roster.iter().copied()),
            _brand: PhantomData,
        }
    }

    /// Restriction into the scope: brands [`DotSet::restrict`] over this
    /// scope's roster. One of the three constructors of [`Scoped`] values,
    /// with [`restrict`](Self::restrict) and
    /// [`restrict_all`](Self::restrict_all).
    #[must_use]
    pub fn restrict_dots(&self, dots: &DotSet) -> Scoped<'brand, DotSet> {
        Scoped {
            value: dots.restrict(self.roster.iter().copied()),
            _brand: PhantomData,
        }
    }

    /// Restricts a batch of vectors into the scope, each branded, so multi-step
    /// scoped work stops hand-rolling the restrict loop.
    ///
    /// Every element is [`restrict`](Self::restrict)ed over the same roster and
    /// carries the same `'brand`, so the whole batch unifies with each other and
    /// with any single [`restrict`](Self::restrict) from the same scope, and none
    /// of it escapes without a deliberate [`Scoped::forget`]. Order is preserved:
    /// the `i`th output is the `i`th input restricted.
    #[must_use]
    pub fn restrict_all<'a>(
        &self,
        vectors: impl IntoIterator<Item = &'a VersionVector>,
    ) -> Vec<Scoped<'brand, VersionVector>> {
        vectors.into_iter().map(|v| self.restrict(v)).collect()
    }
}