karpal_std/
lib.rs

1// Copyright (C) 2026 Industrial Algebra
2// SPDX-License-Identifier: Apache-2.0
3
4// Standard prelude for the Karpal ecosystem.
5//
6// Re-exports the most commonly used types and traits from
7// `karpal-core`, `karpal-profunctor`, and `karpal-optics`.
8
9/// Prelude module — `use karpal_std::prelude::*` to import everything.
10pub mod prelude {
11    // HKT encoding
12    pub use karpal_core::hkt::{
13        EnvF, HKT, HKT2, IdentityF, NonEmptyVec, NonEmptyVecF, OptionF, ReaderF, ResultBF, ResultF,
14        StoreF, TracedF, TupleF, VecF,
15    };
16
17    // Functor hierarchy
18    pub use karpal_core::{
19        Alt, Alternative, Applicative, Apply, Chain, Functor, FunctorFilter, Monad,
20    };
21
22    // Foldable / Traversable
23    pub use karpal_core::{Foldable, Traversable};
24
25    // Comonad hierarchy
26    pub use karpal_core::{Comonad, ComonadEnv, ComonadStore, ComonadTraced, Extend};
27
28    // Bifunctor, Selective, NaturalTransformation, DinaturalTransformation
29    pub use karpal_core::{Bifunctor, DinaturalTransformation, NaturalTransformation, Selective};
30
31    // Invariant
32    pub use karpal_core::Invariant;
33
34    // Contravariant hierarchy
35    pub use karpal_core::{Conclude, Contravariant, Decide, Divide, Divisible, PredicateF};
36
37    // Plus
38    pub use karpal_core::Plus;
39
40    // Algebraic typeclasses
41    pub use karpal_core::{Monoid, Semigroup};
42
43    // Newtype wrappers
44    pub use karpal_core::{First, Last, Max, Min, Product, Sum};
45
46    // Adjunctions & advanced category theory
47    pub use karpal_core::{
48        Adjunction, Coend, ComposeF, ContAdj, ContF, ContravariantAdjunction, CurryAdj, End,
49        IdentityAdj, ProfunctorAdjunction, ProfunctorFunctor, ProfunctorIdentityAdj,
50        ProfunctorIdentityF,
51    };
52
53    // Abstract algebra
54    pub use karpal_algebra::{
55        AbelianGroup, BoundedLattice, Field, Group, Lattice, Module, Ring, Semiring, VectorSpace,
56    };
57
58    // Profunctor
59    pub use karpal_profunctor::{Choice, FnP, ForgetF, Profunctor, Strong, TaggedF, Traversing};
60
61    // Optics
62    pub use karpal_optics::fold::{ComposedFold, Fold};
63    pub use karpal_optics::getter::{ComposedGetter, Getter};
64    pub use karpal_optics::iso::{Iso, SimpleIso};
65    pub use karpal_optics::lens::{ComposedLens, Lens, SimpleLens};
66    pub use karpal_optics::optic::Optic;
67    pub use karpal_optics::review::Review;
68    pub use karpal_optics::setter::{Setter, SimpleSetter};
69    pub use karpal_optics::traversal::{ComposedTraversal, SimpleTraversal, Traversal};
70    pub use karpal_optics::{Prism, SimplePrism};
71
72    // Arrow hierarchy
73    pub use karpal_arrow::{
74        Arrow, ArrowApply, ArrowChoice, ArrowLoop, ArrowPlus, ArrowZero, Category, CokleisliF, FnA,
75        KleisliF, Semigroupoid,
76    };
77
78    // Arrow macros
79    pub use karpal_arrow::{impl_cokleisli, impl_cokleisli_env};
80
81    // Free constructions
82    pub use karpal_free::{
83        Codensity, CodensityF, Cofree, CofreeF, Coyoneda, CoyonedaF, Day, DayF, Density, DensityF,
84        Free, FreeAlt, FreeAltF, FreeAp, FreeApF, FreeF, Freer, FreerF, Lan, LanF, Ran, RanMapped,
85        Yoneda, YonedaF,
86    };
87
88    // Recursion schemes
89    pub use karpal_recursion::{
90        Either, Fix, FixF, Mu, Nu, ana, apo, cata, chrono, futu, histo, hylo, para, zygo,
91    };
92
93    // Effect system / Monad transformers
94    pub use karpal_effect::{
95        ApplicativeSt, ChainSt, ExceptTF, FunctorSt, MonadTrans, ReaderTF, StateTF, WriterTF,
96    };
97
98    // Proof system / Algebraic witnesses
99    pub use karpal_proof::{
100        And,
101        Implies,
102        IsAbelianGroup,
103        // Property markers
104        IsAssociative,
105        IsBoundedLattice,
106        IsCommutative,
107        IsField,
108        IsGroup,
109        IsLattice,
110        IsLawfulFunctor,
111        IsLawfulMonad,
112        IsMonoid,
113        IsRing,
114        IsSemiring,
115        Justifies,
116        NonEmpty,
117        Positive,
118        Property,
119        Proven,
120        Rewrite,
121        // Derive macros
122        VerifyCommutative,
123        VerifyGroup,
124        VerifyLattice,
125        VerifyMonoid,
126        VerifyRing,
127        VerifySemigroup,
128        VerifySemiring,
129    };
130
131    // External verification / proof obligations
132    pub use karpal_verify::{
133        AlgebraicSignature, ArtifactBatch, ArtifactLayout, ArtifactRecord, BinarySymbol,
134        Certificate, Certified, CommandKind, ConstantSymbol, DEFAULT_REPORT_STEM, Declaration,
135        DryRunner, ExecutionResult, ExecutionStatus, InvocationPlan, Lean4, LeanAlias,
136        LeanCertificate, LeanConfig, LeanDiagnostic, LeanDriver, LeanExport, LeanImport,
137        LeanOutput, LeanPrelude, LeanProject, LeanTheorem, LocalProcessRunner, ModuleReport,
138        Obligation, ObligationBundle, ObligationReport, Origin, ProofDialect, ReportFiles,
139        SmtCertificate, SmtConfig, SmtLib2, SmtOutput, Sort, Term, UnarySymbol,
140        VerificationBackend, VerificationOutput, VerificationPolicy, VerificationReport,
141        VerificationSession, VerificationTier, VerifierRunner, dry_run_bundle_artifacts,
142        dry_run_report, execute_report, export_lean_bundle, export_lean_bundle_structured,
143        export_lean_bundle_structured_with_prelude, export_lean_bundle_with_prelude,
144        export_module_with_prelude, export_smt_batch, export_smt_bundle, export_with_prelude,
145        parse_lean_output, parse_smt_output, parse_smt_status, verify_bundle,
146        verify_bundle_with_ci_outputs, write_bundle_artifacts,
147    };
148
149    // Monoidal categories and string diagrams
150    pub use karpal_diagram::{
151        Braiding,
152        // Phase 13 coherence types
153        ByNormalization,
154        ByYanking,
155        CoherenceCertificate,
156        Diagram,
157        DiagramKind,
158        HexagonIdentity,
159        NormalizationRule,
160        NormalizationTrace,
161        PentagonIdentity,
162        SvgRenderer,
163        Symmetry,
164        Tensor,
165        TextRenderer,
166        Trace,
167        TriangleIdentity,
168        coherence_certificates,
169        equivalent_proved,
170        prove_yanking,
171    };
172    pub use karpal_higher::{
173        Bicategory, BicategoryPentagonIdentity, BicategoryTriangleIdentity, EnrichedCategory,
174        FFunctor, FMonad, IdentityFFunctor, InterchangeIdentity, TwoCategory,
175    }; // Phase 15
176    pub use karpal_schubert_types::verification::{schubert_bundle, verify_schubert};
177    pub use karpal_schubert_types::{
178        Intersection, IntersectionKind, SchubertProven, SchubertType, SchubertTyped,
179        check_intersection, compose_checks,
180    }; // Phase 14
181    #[cfg(feature = "amari")]
182    pub use karpal_verify::{
183        AmariMonteCarloVerifier, AmariObligationKind, AmariSmtProofObligation,
184        AmariStatisticalProperty, AmariVerificationResult, StatisticalBound,
185        StatisticalVerification, ThreeTierObligationReport, ThreeTierVerificationReport,
186        classify_tier, concentration_obligation_for, ensures_expected,
187        expected_value_obligation_for, postcondition_obligation_for, precondition_obligation_for,
188        prob_ensures, prob_requires, three_tier_report, verify_rare_event,
189    };
190
191    // Macros
192    pub use karpal_core::{ado_, do_};
193}
194
195// Crate re-exports for qualified access
196pub use karpal_algebra;
197pub use karpal_arrow;
198pub use karpal_core;
199pub use karpal_diagram;
200pub use karpal_effect;
201pub use karpal_free;
202pub use karpal_higher;
203pub use karpal_optics;
204pub use karpal_profunctor;
205pub use karpal_proof;
206pub use karpal_recursion;
207pub use karpal_schubert_types;
208pub use karpal_verify;
209
210// Macro re-exports
211pub use karpal_core::ado_;
212pub use karpal_core::do_;
213
214#[cfg(test)]
215mod tests {
216    use super::prelude::*;
217
218    #[test]
219    fn prelude_hkt_accessible() {
220        let _: <OptionF as HKT>::Of<i32> = Some(42);
221        let _: <VecF as HKT>::Of<i32> = vec![1, 2, 3];
222        let _: <ResultF<String> as HKT>::Of<i32> = Ok(42);
223    }
224
225    #[test]
226    fn prelude_functor_accessible() {
227        let result = <OptionF as Functor>::fmap(Some(1), |x| x + 1);
228        assert_eq!(result, Some(2));
229    }
230
231    #[test]
232    fn prelude_lens_accessible() {
233        let lens: SimpleLens<(i32, i32), i32> = Lens::new(|p: &(i32, i32)| p.0, |p, x| (x, p.1));
234        assert_eq!(lens.get(&(1, 2)), 1);
235    }
236
237    #[test]
238    fn prelude_prism_accessible() {
239        let prism: SimplePrism<Option<i32>, i32> = Prism::new(
240            |s| match s {
241                Some(v) => Ok(v),
242                None => Err(None),
243            },
244            Some,
245        );
246        assert_eq!(prism.preview(&Some(42)), Some(42));
247        assert_eq!(prism.preview(&None), None);
248    }
249
250    #[test]
251    fn prelude_profunctor_accessible() {
252        let f: <FnP as HKT2>::P<i32, i32> = Box::new(|x| x + 1);
253        assert_eq!(f(1), 2);
254    }
255
256    #[test]
257    fn prelude_arrow_accessible() {
258        let double = <FnA as Arrow>::arr(|x: i32| x * 2);
259        let inc = <FnA as Arrow>::arr(|x: i32| x + 1);
260        let composed = <FnA as Semigroupoid>::compose(inc, double);
261        assert_eq!(composed(5), 11); // (5 * 2) + 1
262    }
263
264    #[test]
265    fn prelude_verify_accessible() {
266        let obligation = Obligation::associativity(
267            "sum_assoc",
268            Origin::new("karpal-core", "Semigroup for i32"),
269            Sort::Int,
270            "combine",
271        );
272        let exported = SmtLib2::export(&obligation);
273        assert!(exported.contains("check-sat"));
274    }
275
276    #[test]
277    fn prelude_diagram_accessible() {
278        let trace = Diagram::identity(1)
279            .then(Diagram::box_("double", 1, 1))
280            .normalize_with_trace();
281        assert_eq!(trace.normalized, Diagram::box_("double", 1, 1));
282        assert!(trace.applied(NormalizationRule::ElideIdentitySequenceStage));
283    }
284
285    #[test]
286    fn prelude_schubert_accessible() {
287        let sigma_1 = SchubertType::new(vec![1], (2, 4)).expect("σ₁");
288        let result = check_intersection(&sigma_1, &sigma_1);
289        assert_eq!(result.kind(), IntersectionKind::Positive);
290    }
291}
karpal_std/lib.rs

karpal_std/
lib.rs
