karpal-std 0.5.0

// Standard prelude for the Karpal ecosystem.
//
// Re-exports the most commonly used types and traits from
// `karpal-core`, `karpal-profunctor`, and `karpal-optics`.

/// Prelude module — `use karpal_std::prelude::*` to import everything.
pub mod prelude {
    // HKT encoding
    pub use karpal_core::hkt::{
        EnvF, HKT, HKT2, IdentityF, NonEmptyVec, NonEmptyVecF, OptionF, ReaderF, ResultBF, ResultF,
        StoreF, TracedF, TupleF, VecF,
    };

    // Functor hierarchy
    pub use karpal_core::{
        Alt, Alternative, Applicative, Apply, Chain, Functor, FunctorFilter, Monad,
    };

    // Foldable / Traversable
    pub use karpal_core::{Foldable, Traversable};

    // Comonad hierarchy
    pub use karpal_core::{Comonad, ComonadEnv, ComonadStore, ComonadTraced, Extend};

    // Bifunctor, Selective, NaturalTransformation, DinaturalTransformation
    pub use karpal_core::{Bifunctor, DinaturalTransformation, NaturalTransformation, Selective};

    // Invariant
    pub use karpal_core::Invariant;

    // Contravariant hierarchy
    pub use karpal_core::{Conclude, Contravariant, Decide, Divide, Divisible, PredicateF};

    // Plus
    pub use karpal_core::Plus;

    // Algebraic typeclasses
    pub use karpal_core::{Monoid, Semigroup};

    // Newtype wrappers
    pub use karpal_core::{First, Last, Max, Min, Product, Sum};

    // Adjunctions & advanced category theory
    pub use karpal_core::{
        Adjunction, Coend, ComposeF, ContAdj, ContF, ContravariantAdjunction, CurryAdj, End,
        IdentityAdj, ProfunctorAdjunction, ProfunctorFunctor, ProfunctorIdentityAdj,
        ProfunctorIdentityF,
    };

    // Abstract algebra
    pub use karpal_algebra::{
        AbelianGroup, BoundedLattice, Field, Group, Lattice, Module, Ring, Semiring, VectorSpace,
    };

    // Profunctor
    pub use karpal_profunctor::{Choice, FnP, ForgetF, Profunctor, Strong, TaggedF, Traversing};

    // Optics
    pub use karpal_optics::fold::{ComposedFold, Fold};
    pub use karpal_optics::getter::{ComposedGetter, Getter};
    pub use karpal_optics::iso::{Iso, SimpleIso};
    pub use karpal_optics::lens::{ComposedLens, Lens, SimpleLens};
    pub use karpal_optics::optic::Optic;
    pub use karpal_optics::review::Review;
    pub use karpal_optics::setter::{Setter, SimpleSetter};
    pub use karpal_optics::traversal::{ComposedTraversal, SimpleTraversal, Traversal};
    pub use karpal_optics::{Prism, SimplePrism};

    // Arrow hierarchy
    pub use karpal_arrow::{
        Arrow, ArrowApply, ArrowChoice, ArrowLoop, ArrowPlus, ArrowZero, Category, CokleisliF, FnA,
        KleisliF, Semigroupoid,
    };

    // Arrow macros
    pub use karpal_arrow::{impl_cokleisli, impl_cokleisli_env};

    // Free constructions
    pub use karpal_free::{
        Codensity, CodensityF, Cofree, CofreeF, Coyoneda, CoyonedaF, Day, DayF, Density, DensityF,
        Free, FreeAlt, FreeAltF, FreeAp, FreeApF, FreeF, Freer, FreerF, Lan, LanF, Ran, RanMapped,
        Yoneda, YonedaF,
    };

    // Recursion schemes
    pub use karpal_recursion::{
        Either, Fix, FixF, Mu, Nu, ana, apo, cata, chrono, futu, histo, hylo, para, zygo,
    };

    // Effect system / Monad transformers
    pub use karpal_effect::{
        ApplicativeSt, ChainSt, ExceptTF, FunctorSt, MonadTrans, ReaderTF, StateTF, WriterTF,
    };

    // Proof system / Algebraic witnesses
    pub use karpal_proof::{
        And,
        Implies,
        IsAbelianGroup,
        // Property markers
        IsAssociative,
        IsBoundedLattice,
        IsCommutative,
        IsField,
        IsGroup,
        IsLattice,
        IsLawfulFunctor,
        IsLawfulMonad,
        IsMonoid,
        IsRing,
        IsSemiring,
        Justifies,
        NonEmpty,
        Positive,
        Property,
        Proven,
        Rewrite,
        // Derive macros
        VerifyCommutative,
        VerifyGroup,
        VerifyLattice,
        VerifyMonoid,
        VerifyRing,
        VerifySemigroup,
        VerifySemiring,
    };

    // External verification / proof obligations
    pub use karpal_verify::{
        AlgebraicSignature, ArtifactBatch, ArtifactLayout, ArtifactRecord, BinarySymbol,
        Certificate, Certified, CommandKind, ConstantSymbol, DEFAULT_REPORT_STEM, Declaration,
        DryRunner, ExecutionResult, ExecutionStatus, InvocationPlan, Lean4, LeanAlias,
        LeanCertificate, LeanConfig, LeanDiagnostic, LeanDriver, LeanExport, LeanImport,
        LeanOutput, LeanPrelude, LeanProject, LeanTheorem, LocalProcessRunner, ModuleReport,
        Obligation, ObligationBundle, ObligationReport, Origin, ProofDialect, ReportFiles,
        SmtCertificate, SmtConfig, SmtLib2, SmtOutput, Sort, Term, UnarySymbol,
        VerificationBackend, VerificationOutput, VerificationPolicy, VerificationReport,
        VerificationSession, VerificationTier, VerifierRunner, dry_run_bundle_artifacts,
        dry_run_report, execute_report, export_lean_bundle, export_lean_bundle_structured,
        export_lean_bundle_structured_with_prelude, export_lean_bundle_with_prelude,
        export_module_with_prelude, export_smt_batch, export_smt_bundle, export_with_prelude,
        parse_lean_output, parse_smt_output, parse_smt_status, verify_bundle,
        verify_bundle_with_ci_outputs, write_bundle_artifacts,
    };

    // Monoidal categories and string diagrams
    pub use karpal_diagram::{
        Braiding,
        // Phase 13 coherence types
        ByNormalization,
        ByYanking,
        CoherenceCertificate,
        Diagram,
        DiagramKind,
        HexagonIdentity,
        NormalizationRule,
        NormalizationTrace,
        PentagonIdentity,
        SvgRenderer,
        Symmetry,
        Tensor,
        TextRenderer,
        Trace,
        TriangleIdentity,
        coherence_certificates,
        equivalent_proved,
        prove_yanking,
    };
    pub use karpal_schubert_types::verification::{schubert_bundle, verify_schubert};
    pub use karpal_schubert_types::{
        Intersection, IntersectionKind, SchubertProven, SchubertType, SchubertTyped,
        check_intersection, compose_checks,
    }; // Phase 14
    #[cfg(feature = "amari")]
    pub use karpal_verify::{
        AmariMonteCarloVerifier, AmariObligationKind, AmariSmtProofObligation,
        AmariStatisticalProperty, AmariVerificationResult, StatisticalBound,
        StatisticalVerification, ThreeTierObligationReport, ThreeTierVerificationReport,
        classify_tier, concentration_obligation_for, ensures_expected,
        expected_value_obligation_for, postcondition_obligation_for, precondition_obligation_for,
        prob_ensures, prob_requires, three_tier_report, verify_rare_event,
    };

    // Macros
    pub use karpal_core::{ado_, do_};
}

// Crate re-exports for qualified access
pub use karpal_algebra;
pub use karpal_arrow;
pub use karpal_core;
pub use karpal_diagram;
pub use karpal_effect;
pub use karpal_free;
pub use karpal_optics;
pub use karpal_profunctor;
pub use karpal_proof;
pub use karpal_recursion;
pub use karpal_schubert_types;
pub use karpal_verify;

// Macro re-exports
pub use karpal_core::ado_;
pub use karpal_core::do_;

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

    #[test]
    fn prelude_hkt_accessible() {
        let _: <OptionF as HKT>::Of<i32> = Some(42);
        let _: <VecF as HKT>::Of<i32> = vec![1, 2, 3];
        let _: <ResultF<String> as HKT>::Of<i32> = Ok(42);
    }

    #[test]
    fn prelude_functor_accessible() {
        let result = <OptionF as Functor>::fmap(Some(1), |x| x + 1);
        assert_eq!(result, Some(2));
    }

    #[test]
    fn prelude_lens_accessible() {
        let lens: SimpleLens<(i32, i32), i32> = Lens::new(|p: &(i32, i32)| p.0, |p, x| (x, p.1));
        assert_eq!(lens.get(&(1, 2)), 1);
    }

    #[test]
    fn prelude_prism_accessible() {
        let prism: SimplePrism<Option<i32>, i32> = Prism::new(
            |s| match s {
                Some(v) => Ok(v),
                None => Err(None),
            },
            Some,
        );
        assert_eq!(prism.preview(&Some(42)), Some(42));
        assert_eq!(prism.preview(&None), None);
    }

    #[test]
    fn prelude_profunctor_accessible() {
        let f: <FnP as HKT2>::P<i32, i32> = Box::new(|x| x + 1);
        assert_eq!(f(1), 2);
    }

    #[test]
    fn prelude_arrow_accessible() {
        let double = <FnA as Arrow>::arr(|x: i32| x * 2);
        let inc = <FnA as Arrow>::arr(|x: i32| x + 1);
        let composed = <FnA as Semigroupoid>::compose(inc, double);
        assert_eq!(composed(5), 11); // (5 * 2) + 1
    }

    #[test]
    fn prelude_verify_accessible() {
        let obligation = Obligation::associativity(
            "sum_assoc",
            Origin::new("karpal-core", "Semigroup for i32"),
            Sort::Int,
            "combine",
        );
        let exported = SmtLib2::export(&obligation);
        assert!(exported.contains("check-sat"));
    }

    #[test]
    fn prelude_diagram_accessible() {
        let trace = Diagram::identity(1)
            .then(Diagram::box_("double", 1, 1))
            .normalize_with_trace();
        assert_eq!(trace.normalized, Diagram::box_("double", 1, 1));
        assert!(trace.applied(NormalizationRule::ElideIdentitySequenceStage));
    }

    #[test]
    fn prelude_schubert_accessible() {
        let sigma_1 = SchubertType::new(vec![1], (2, 4)).expect("σ₁");
        let result = check_intersection(&sigma_1, &sigma_1);
        assert_eq!(result.kind(), IntersectionKind::Positive);
    }
}