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    #[cfg(feature = "amari")]
146    pub use karpal_verify::{
147        AmariMonteCarloVerifier, AmariObligationKind, AmariSmtProofObligation,
148        AmariStatisticalProperty, AmariVerificationResult, StatisticalBound,
149        StatisticalVerification, ThreeTierObligationReport, ThreeTierVerificationReport,
150        classify_tier, concentration_obligation_for, ensures_expected,
151        expected_value_obligation_for, postcondition_obligation_for, precondition_obligation_for,
152        prob_ensures, prob_requires, three_tier_report, verify_rare_event,
153    };
154
155    // Macros
156    pub use karpal_core::{ado_, do_};
157}
158
159// Crate re-exports for qualified access
160pub use karpal_algebra;
161pub use karpal_arrow;
162pub use karpal_core;
163pub use karpal_effect;
164pub use karpal_free;
165pub use karpal_optics;
166pub use karpal_profunctor;
167pub use karpal_proof;
168pub use karpal_recursion;
169pub use karpal_verify;
170
171// Macro re-exports
172pub use karpal_core::ado_;
173pub use karpal_core::do_;
174
175#[cfg(test)]
176mod tests {
177    use super::prelude::*;
178
179    #[test]
180    fn prelude_hkt_accessible() {
181        let _: <OptionF as HKT>::Of<i32> = Some(42);
182        let _: <VecF as HKT>::Of<i32> = vec![1, 2, 3];
183        let _: <ResultF<String> as HKT>::Of<i32> = Ok(42);
184    }
185
186    #[test]
187    fn prelude_functor_accessible() {
188        let result = <OptionF as Functor>::fmap(Some(1), |x| x + 1);
189        assert_eq!(result, Some(2));
190    }
191
192    #[test]
193    fn prelude_lens_accessible() {
194        let lens: SimpleLens<(i32, i32), i32> = Lens::new(|p: &(i32, i32)| p.0, |p, x| (x, p.1));
195        assert_eq!(lens.get(&(1, 2)), 1);
196    }
197
198    #[test]
199    fn prelude_prism_accessible() {
200        let prism: SimplePrism<Option<i32>, i32> = Prism::new(
201            |s| match s {
202                Some(v) => Ok(v),
203                None => Err(None),
204            },
205            Some,
206        );
207        assert_eq!(prism.preview(&Some(42)), Some(42));
208        assert_eq!(prism.preview(&None), None);
209    }
210
211    #[test]
212    fn prelude_profunctor_accessible() {
213        let f: <FnP as HKT2>::P<i32, i32> = Box::new(|x| x + 1);
214        assert_eq!(f(1), 2);
215    }
216
217    #[test]
218    fn prelude_arrow_accessible() {
219        let double = <FnA as Arrow>::arr(|x: i32| x * 2);
220        let inc = <FnA as Arrow>::arr(|x: i32| x + 1);
221        let composed = <FnA as Semigroupoid>::compose(inc, double);
222        assert_eq!(composed(5), 11); // (5 * 2) + 1
223    }
224
225    #[test]
226    fn prelude_verify_accessible() {
227        let obligation = Obligation::associativity(
228            "sum_assoc",
229            Origin::new("karpal-core", "Semigroup for i32"),
230            Sort::Int,
231            "combine",
232        );
233        let exported = SmtLib2::export(&obligation);
234        assert!(exported.contains("check-sat"));
235    }
236}
karpal_std/lib.rs

karpal_std/
lib.rs
