//!
//! derived — the WHOLE theory autogenerated from ordinary functions. No `theory!` block at all.
//!
//! v17 derived the grid, v19 pared the `theory!` block to its floor — but a block was still written.
//! Here there is none. `#[algebra]` reads the module's operator FUNCTIONS and synthesises the entire
//! `Theory`: each function's signature gives its arity (→ fixity), its single value type (→ the
//! sort), and its name (→ the symbol); the grid is shadow-derived from the type, the observation is
//! the value itself. So the agent writes only what it MEANS — the value object and the operators —
//! and the algebra, the grid, and the discovered spec all follow.
//!
//! `Tri` is the three-element lattice (`Lo ≤ Mid ≤ Hi`). From `meet`/`join` alone the macro builds
//! `Lattice` (the theory) and `LatticeSort`, and the engine discovers the full distributive-lattice
//! spec over a grid the type generated — nothing here was declared, only defined.

use crate::algebra;

#[algebra(Lattice, "tri lattice")]
pub mod lattice {
    use crate::Shaped;

    /// A three-element lattice value object — its grid comes entirely from its `Shaped` structure.
    #[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Shaped)]
    pub enum Tri {
        Lo,
        Mid,
        Hi,
    }

    pub fn meet(a: Tri, b: Tri) -> Tri {
        a.min(b)
    }
    pub fn join(a: Tri, b: Tri) -> Tri {
        a.max(b)
    }
}

/// MULTI-SORTED: operators ranging over TWO value types. The macro synthesises a `Value` sum over
/// `Small` and `Large` and the `sort_of` that tags it — so a domain spanning several sorts (like the
/// date calculus's `Date`/`Duration`) is still just its value objects and functions. `lift` carries
/// the small lattice into the large one; the engine discovers it is a homomorphism, across the sorts.
///
/// (Names are kept clear of the crate's type-level vocabulary — `Z`, `S`, `Graded` are Peano/grading
/// types in `boundary`, and reusing them makes rustc fully-qualify paths in the compile-fail
/// `.stderr` fixtures.)
#[algebra(Tiers, "graded lattices")]
pub mod tiers {
    use crate::Shaped;

    #[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Shaped)]
    pub enum Small {
        Bot,
        Top,
    }
    #[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Shaped)]
    pub enum Large {
        One,
        Two,
        Three,
    }

    pub fn meet_small(a: Small, b: Small) -> Small {
        a.min(b)
    }
    pub fn meet_large(a: Large, b: Large) -> Large {
        a.min(b)
    }
    pub fn lift(x: Small) -> Large {
        match x {
            Small::Bot => Large::One,
            Small::Top => Large::Two,
        }
    }
}

#[cfg(test)]
mod tests {
    use super::lattice::{Lattice, LatticeSort, Tri};
    use super::tiers::Tiers;
    use crate::discover::engine::{shadow_grid, Engine, Theory};

    /// MULTI-SORT autogeneration: from two `#[derive(Shaped)]` value enums (`Lo`, `Hi`) and three
    /// functions, `#[algebra]` synthesised a TWO-SORTED `Theory` — the `Value` sum and the `sort_of`
    /// that tags it — and the engine discovers both monoids AND the cross-sort homomorphism `lift`.
    /// No `Value` enum, no `sort_of`, no `theory!` was written; the multi-sorted algebra is just the
    /// value objects and the functions.
    #[test]
    fn a_multi_sorted_theory_is_generated_and_discovered() {
        let proses: Vec<String> = Engine::<Tiers>::new()
            .discover()
            .laws
            .iter()
            .map(|l| l.prose.clone())
            .collect();
        assert_eq!(
            proses,
            vec![
                "meet_small gives the same result in either order.".to_string(),
                "With meet_small, the grouping of three values doesn't matter.".to_string(),
                "meet_small of a value with itself gives that value.".to_string(),
                "meet_large gives the same result in either order.".to_string(),
                "With meet_large, the grouping of three values doesn't matter.".to_string(),
                "meet_large of a value with itself gives that value.".to_string(),
                "lift turns meet_small into meet_large.".to_string(), // the cross-sort homomorphism
            ],
            "the generated two-sorted spec"
        );
        // the synthesised theory genuinely spans TWO sorts (the operators touch both).
        let sorts: std::collections::BTreeSet<_> = <Tiers as Theory>::operators()
            .iter()
            .flat_map(|o| o.inputs.iter().chain(std::iter::once(&o.output)).copied())
            .collect();
        assert_eq!(sorts.len(), 2, "two sorts synthesised from the value types");
    }

    /// The macro generated a real `Theory`: a marker (`Lattice`), a sort (`LatticeSort`), and the
    /// operator table — from two ordinary functions. The grid still comes from the value type's
    /// structure (no constant operator could bootstrap one), exactly as in the hand-written form.
    #[test]
    fn the_theory_is_generated_from_the_functions() {
        // two operators were read off the function signatures — both binary (arity 2), no constants.
        let ops = <Lattice as Theory>::operators();
        assert_eq!(ops.len(), 2, "meet and join");
        assert!(
            ops.iter().all(|o| o.inputs.len() == 2),
            "both binary, read from `(Tri, Tri) -> Tri`"
        );
        // the grid is type-generated and wired into `inhabitants`.
        assert_eq!(shadow_grid::<Tri>(24), vec![Tri::Lo, Tri::Mid, Tri::Hi]);
        assert_eq!(
            <Lattice as Theory>::inhabitants(LatticeSort::Only),
            vec![Tri::Lo, Tri::Mid, Tri::Hi]
        );
    }

    /// And the generated theory discovers the WHOLE distributive-lattice spec — `meet`/`join` each
    /// commutative, associative, idempotent, both distributivities and both absorptions — from two
    /// functions and a `#[derive(Shaped)]` enum. Nothing was declared; everything was defined.
    #[test]
    fn the_generated_lattice_is_discovered_hands_free() {
        let proses: Vec<String> = Engine::<Lattice>::new()
            .discover()
            .laws
            .iter()
            .map(|l| l.prose.clone())
            .collect();
        assert_eq!(
            proses,
            vec![
                "meet gives the same result in either order.".to_string(),
                "With meet, the grouping of three values doesn't matter.".to_string(),
                "meet of a value with itself gives that value.".to_string(),
                "meet distributes over join.".to_string(),
                "meet absorbs join.".to_string(),
                "join gives the same result in either order.".to_string(),
                "With join, the grouping of three values doesn't matter.".to_string(),
                "join of a value with itself gives that value.".to_string(),
                "join distributes over meet.".to_string(),
                "join absorbs meet.".to_string(),
            ],
            "the generated lattice's discovered spec"
        );
    }
}
