#[allow(unused_imports)]
use alloc::{boxed::Box, format, string::String, string::ToString, vec, vec::Vec};
use core::fmt::Debug;
use core::hash::Hash;

/// A concept — a type representing a kind of thing in an ontology.
///
/// Corresponds to Guarino (2009) *Formal Ontology in Information Systems*'s
/// "universal" and OWL's "class": a shared essence that instances can
/// inhabit. A concept's *variants* play the role of both finer-grained
/// sub-concepts and (in closed-world ontologies) the only individuals — there
/// is no separate runtime individual layer.
///
/// # Open-world by default
///
/// `Concept` itself makes **no** finiteness commitment: it carries only the
/// supertrait bounds (`Sized + Clone + Eq + Hash + Debug + 'static`) and a
/// lexical [`name`](Concept::name). This is the open-world case (Reiter 1978):
/// a concept may be inhabited by individuals that exist only at runtime — e.g.
/// the vertices of an ontology materialized from a loaded `.prx`, which the
/// type system cannot enumerate at compile time.
///
/// Finite enumeration lives in the [`FinitelyGenerated`] subtrait, which adds
/// `variants()`. Closed-world concepts (the macro-derived enums) implement both
/// `Concept` and `FinitelyGenerated`; open-world concepts implement only
/// `Concept`. The split lets a generic algorithm demand finite enumeration
/// exactly where it iterates (`T: FinitelyGenerated`) and stay open-world
/// everywhere else (`T: Concept`).
///
/// Can be derived for enums with unit variants — the derive emits **both**
/// `Concept` and `FinitelyGenerated`:
/// ```text
/// use pr4xis::category::{Concept, FinitelyGenerated};
///
/// #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Concept)]
/// enum Color { Red, Green, Blue }
///
/// assert_eq!(Color::variants().len(), 3);
/// ```
///
/// # Literature
///
/// - Guarino (2009) §2 — concepts as specifications of conceptualizations
/// - Masolo et al. (2003) WonderWeb D18 — DOLCE's universal/particular split
/// - Smith (2015) *Basic Formal Ontology* — continuants and occurrents
/// - ONTOLEX-Lemon (W3C 2016) — names as lexical entries
/// - Mac Lane (1971) III.5 — coproducts (sum types) and their generators
/// - Reiter (1978) *On Closed World Data Bases* — the closed/open-world split
pub trait Concept: Sized + Clone + Eq + Hash + Debug + 'static {
    /// The Lemon canonical form identifying a variant — generated by the
    /// derive macro from the variant's Rust name. Override to inject
    /// structured lexical metadata.
    fn name(&self) -> &'static str {
        ""
    }

    /// The variant's lexical grounding — its ONTOLEX-Lemon entry (label +
    /// definition/gloss + language), if the ontology declares one.
    ///
    /// This is the structured form of the identity-layer "what does this
    /// concept *mean*" that [`name`](Concept::name) only names. Per
    /// ONTOLEX-Lemon (W3C 2016) a name is a lexical entry, not a bare string;
    /// this accessor carries that entry so the gloss travels WITH the concept
    /// (e.g. into an emitted `.prx`) rather than living only in a compile-time
    /// side table.
    ///
    /// # Default: `None` (open-world)
    ///
    /// The default returns `None` — a concept need not be lexically grounded
    /// (open-world: a runtime-materialized vertex carries its gloss in its
    /// definition, not its type). The `ontology!` macro overrides this to
    /// return each concept's entry from the generated `labels` table; bare
    /// `#[derive(Concept)]` enums (no label data at the derive site) keep the
    /// default. This is identity-layer metadata, so it lives on `Concept`
    /// itself — the finite-enumeration commitment ([`variants`]) stays on
    /// [`FinitelyGenerated`].
    ///
    /// [`variants`]: FinitelyGenerated::variants
    fn lexical(&self) -> Option<crate::ontology::meta::Lexical> {
        None
    }
}

/// Marker trait for [`Concept`]s whose variants form a **finite generator
/// set** for a free monoid (equivalently, a free sum type / coproduct with
/// a finite generator family).
///
/// # Why this exists
///
/// "Finitely generated" is the standard algebraic / categorical term for
/// a structure whose elements are producible by applying operations to a
/// finite generator set. It's load-bearing across algebra and category
/// theory:
///
/// - **Lang** *Algebra* (3rd ed., Graduate Texts in Math 211, 2002) §I.2
///   — finitely generated groups / modules / algebras
/// - **Howie** *Fundamentals of Semigroup Theory* (1995) §1.2 — "a monoid
///   M is finitely generated iff there exists a finite subset S ⊂ M such
///   that every element of M can be written as a product of elements of S"
/// - **Clifford & Preston** *The Algebraic Theory of Semigroups* (1961)
///   Ch. 1 — same definition for semigroups
/// - **Mac Lane** *Categories for the Working Mathematician* (1971) VII.3
///   — free monoids and generators; III.5 — coproducts as free sum types
/// - **Adámek & Rosický** *Locally Presentable and Accessible Categories*
///   (1994) — finitely presentable / finitely generated objects
/// - **Fong & Spivak** *Seven Sketches in Compositionality* (2019) Ch. 3
///   — finitely presented categories via generators and relations
/// - **Eilenberg** *Automata, Languages, and Machines* (1974) A.III — free
///   monoids on finite alphabets, the canonical finitely-generated case
/// - **Ganter & Wille** *Formal Concept Analysis* (1999) — concepts
///   generated by (finite) attribute sets
///
/// # In pr4xis
///
/// This subtrait carries the finite enumeration: `variants()` lives here, **not**
/// on [`Concept`]. That realizes the closed/open-world split (Reiter 1978 *On
/// Closed World Data Bases*) in the type system — closed-world concepts (the
/// macro-derived enums) are `FinitelyGenerated`; open-world concepts
/// (potentially-infinite or runtime-instantiated, e.g. vertices materialized
/// from a loaded `.prx`) implement only `Concept` and therefore cannot be
/// enumerated. A generic algorithm asks for `T: FinitelyGenerated` exactly
/// where it iterates the generators, and stays open-world (`T: Concept`)
/// everywhere else.
///
/// There is deliberately **no** default `variants()`: a silently-empty
/// enumeration is a footgun (it would make every open-world concept look like
/// the empty closed-world ontology). Implementors must supply the real
/// generator set; the derive macro does so for unit enums.
pub trait FinitelyGenerated: Concept {
    /// All variants of this concept — the generators of its free sum type.
    ///
    /// Algebraically, the variants ARE the generators: a concept enum is
    /// the coproduct (Mac Lane III.5) over its variants, and `variants()`
    /// returns that finite generator set. Implementing this trait IS the
    /// finitely-generated (closed-world) commitment.
    fn variants() -> Vec<Self>;
}

/// Metadata about concept variants — generated by the derive macro
/// from `/// doc comments`. Separate from the [`Concept`] trait because
/// descriptions are metadata ABOUT the concept, not behavior OF it.
///
/// The derive macro generates a const `<TypeName>_META: &[ConceptMeta]`
/// for each concept enum. The vocabulary system reads it.
#[derive(Debug, Clone)]
pub struct ConceptMeta {
    pub name: &'static str,
    pub description: &'static str,
}

#[cfg(test)]
mod tests {
    use super::*;
    use pr4xis_derive::Concept;

    #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Concept)]
    enum TestConcept {
        A,
        B,
        C,
    }

    #[test]
    fn derive_concept_produces_all_variants() {
        let v = TestConcept::variants();
        assert_eq!(v.len(), 3);
        assert_eq!(v[0], TestConcept::A);
        assert_eq!(v[1], TestConcept::B);
        assert_eq!(v[2], TestConcept::C);
    }

    #[test]
    fn derive_concept_single_variant() {
        #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Concept)]
        enum Single {
            Only,
        }
        assert_eq!(Single::variants(), vec![Single::Only]);
    }

    #[test]
    fn derived_concept_is_finitely_generated() {
        // The derive macro emits BOTH Concept and FinitelyGenerated, so a
        // derived enum can be used where finite enumeration is required.
        fn check<T: FinitelyGenerated>() -> usize {
            T::variants().len()
        }
        assert_eq!(check::<TestConcept>(), 3);
    }
}
