karpal_std/
lib.rs

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

karpal_std/
lib.rs
