oxilean_std/
lib.rs

1//! # OxiLean Standard Library — Core Data Types & Theorems
2//!
3//! The standard library provides essential types, type classes, and theorems for OxiLean programs.
4//! It is written in OxiLean itself and loaded into the kernel environment at startup.
5//!
6//! ## Architecture Overview
7//!
8//! The standard library is organized into logical categories:
9//! - Primitive Types: `nat`, `bool`, `char`, `int`, `string`, `list`, `array`, `option`, `result`
10//! - Type Classes: `Eq`, `Ord`, `Show`, `Repr`, `Functor`, `Monad`, `Monoid`, `Decidable`
11//! - Core Theorems: equality, logic, arithmetic, order
12//! - Utilities: tactic lemmas, decision procedures, parsing combinators
13//!
14//! ## Environment Building
15//!
16//! Loading happens via `build_*_env` functions:
17//!
18//! ```ignore
19//! let env = Environment::new();
20//! let env = build_nat_env(env)?;
21//! let env = build_list_env(env)?;
22//! let env = build_eq_env(env)?;
23//! ```
24//!
25//! See `registry` module for module metadata and dependency graph.
26
27#![allow(missing_docs)]
28#![warn(clippy::all)]
29#![allow(clippy::module_inception)]
30#![allow(mixed_script_confusables)]
31#![allow(clippy::type_complexity)]
32#![allow(clippy::needless_range_loop)]
33#![allow(clippy::map_unwrap_or)]
34#![allow(clippy::collapsible_if)]
35#![allow(clippy::collapsible_else_if)]
36#![allow(clippy::should_implement_trait)]
37#![allow(clippy::vec_box)]
38#![allow(clippy::ptr_arg)]
39#![allow(clippy::redundant_field_names)]
40#![allow(clippy::redundant_closure)]
41#![allow(clippy::int_plus_one)]
42#![allow(clippy::implicit_saturating_sub)]
43#![allow(clippy::assign_op_pattern)]
44#![allow(clippy::clone_on_copy)]
45#![allow(clippy::useless_let_if_seq)]
46#![allow(clippy::identity_op)]
47#![allow(clippy::if_same_then_else)]
48#![allow(clippy::doc_lazy_continuation)]
49#![allow(clippy::cast_lossless)]
50#![allow(clippy::manual_range_contains)]
51#![allow(clippy::option_if_let_else)]
52#![allow(clippy::unnecessary_unwrap)]
53#![allow(clippy::missing_panics_doc)]
54#![allow(clippy::missing_errors_doc)]
55#![allow(clippy::must_use_candidate)]
56#![allow(clippy::return_self_not_must_use)]
57#![allow(clippy::items_after_statements)]
58#![allow(clippy::too_many_lines)]
59#![allow(clippy::similar_names)]
60#![allow(clippy::cast_possible_truncation)]
61#![allow(clippy::cast_sign_loss)]
62#![allow(clippy::cast_precision_loss)]
63#![allow(clippy::float_cmp)]
64#![allow(clippy::match_same_arms)]
65#![allow(clippy::single_match_else)]
66#![allow(clippy::wildcard_imports)]
67#![allow(clippy::struct_excessive_bools)]
68#![allow(clippy::module_name_repetitions)]
69#![allow(clippy::unused_self)]
70#![allow(clippy::unnecessary_wraps)]
71#![allow(clippy::use_self)]
72#![allow(clippy::default_trait_access)]
73#![allow(clippy::uninlined_format_args)]
74#![allow(clippy::vec_init_then_push)]
75#![allow(clippy::box_collection)]
76#![allow(clippy::iter_nth_zero)]
77#![allow(clippy::new_without_default)]
78#![allow(clippy::useless_conversion)]
79#![allow(suspicious_double_ref_op)]
80#![allow(clippy::needless_pass_by_value)]
81#![allow(clippy::inline_always)]
82#![allow(dead_code)]
83#![allow(unused_assignments)]
84#![allow(clippy::unnecessary_map_or)]
85#![allow(clippy::extra_unused_lifetimes)]
86#![allow(clippy::needless_lifetimes)]
87#![allow(clippy::borrow_as_ptr)]
88#![allow(clippy::used_underscore_binding)]
89#![allow(clippy::manual_let_else)]
90#![allow(clippy::empty_line_after_doc_comments)]
91#![allow(clippy::useless_format)]
92#![allow(clippy::option_option)]
93#![allow(clippy::large_enum_variant)]
94#![allow(clippy::enum_variant_names)]
95#![allow(clippy::single_char_lifetime_names)]
96#![allow(clippy::needless_update)]
97#![allow(clippy::match_wildcard_for_single_variants)]
98#![allow(clippy::missing_fields_in_debug)]
99#![allow(clippy::expect_used)]
100#![allow(clippy::panic)]
101#![allow(clippy::unwrap_used)]
102#![allow(clippy::explicit_deref_methods)]
103#![allow(clippy::suspicious_arithmetic_impl)]
104#![allow(clippy::suspicious_op_assign_impl)]
105#![allow(clippy::duplicated_attributes)]
106#![allow(clippy::match_like_matches_macro)]
107#![allow(clippy::manual_clamp)]
108#![allow(clippy::too_many_arguments)]
109#![allow(clippy::borrowed_box)]
110#![allow(clippy::nonminimal_bool)]
111#![allow(clippy::option_map_or_none)]
112#![allow(clippy::collapsible_match)]
113#![allow(clippy::map_clone)]
114#![allow(clippy::unnecessary_cast)]
115#![allow(unused_imports)]
116
117// ── Standard library modules ──────────────────────────────────────────────────
118
119pub mod abstract_algebra_adv;
120pub mod abstract_interpretation;
121pub mod abstract_rewriting;
122pub mod algebra;
123pub mod algebraic_combinatorics;
124pub mod algebraic_effects;
125pub mod algebraic_geometry;
126pub mod algebraic_k_theory;
127pub mod algebraic_number_theory;
128pub mod algebraic_topology;
129pub mod analytic_number_theory;
130pub mod arithmetic_geometry;
131pub mod array;
132pub mod automata_theory;
133pub mod bitvec;
134pub mod bool;
135pub mod category_theory;
136pub mod category_theory_ext;
137pub mod certified_algorithms;
138pub mod chaos_theory;
139pub mod char;
140pub mod chromatic_homotopy;
141pub mod coding_theory;
142pub mod coinduction;
143pub mod combinatorial_game_theory;
144pub mod combinatorial_optimization;
145pub mod combinatorics;
146pub mod combinatory_logic;
147pub mod complex;
148pub mod complexity;
149pub mod computability_theory;
150pub mod computational_geometry;
151pub mod concurrency_theory;
152pub mod constructive_mathematics;
153pub mod control_theory;
154pub mod convex_geometry;
155pub mod convex_optimization;
156pub mod cryptographic_protocols;
157pub mod cryptography;
158pub mod data_structures;
159pub mod decidable;
160pub mod denotational_semantics;
161pub mod dependent_type_theory;
162pub mod derived_algebraic_geometry;
163pub mod descriptive_set_theory;
164pub mod differential_equations;
165pub mod differential_geometry;
166pub mod diophantine_geometry;
167pub mod domain_theory;
168pub mod either;
169pub mod elliptic_curves;
170pub mod env_builder;
171pub mod eq;
172pub mod ergodic_theory;
173pub mod fin;
174pub mod forcing_theory;
175pub mod formal_languages;
176pub mod formal_verification;
177pub mod functional_analysis;
178pub mod functional_calculus;
179pub mod functional_programming;
180pub mod functor;
181pub mod fuzzy_logic;
182pub mod game_theory;
183pub mod game_theory_ext;
184pub mod geometric_group_theory;
185pub mod geometric_topology;
186pub mod graph;
187pub mod graph_algorithms;
188pub mod groebner_bases;
189pub mod group_theory;
190pub mod hashmap;
191pub mod hashset;
192pub mod higher_category_theory;
193pub mod homological_algebra;
194pub mod homological_computations;
195pub mod homotopy_theory;
196pub mod homotopy_type_theory;
197pub mod hybrid_systems;
198pub mod information_geometry;
199pub mod information_theory;
200pub mod information_theory_ext;
201pub mod int;
202pub mod io;
203pub mod iwasawa_theory;
204pub mod k_theory;
205pub mod lattice_theory;
206pub mod lazy;
207pub mod lie_theory;
208pub mod linear_algebra;
209pub mod linear_logic;
210pub mod linear_programming;
211pub mod list;
212pub mod logic;
213pub mod machine_learning;
214pub mod mathematical_physics;
215pub mod measure_theory;
216pub mod model_checking;
217pub mod model_theory;
218pub mod monad;
219pub mod motivic_cohomology;
220pub mod nat;
221pub mod noncommutative_geometry;
222pub mod nonlinear_dynamics;
223pub mod number_theory;
224pub mod numerical_analysis;
225pub mod numerical_linear_algebra;
226pub mod operations_research;
227pub mod operator_algebras;
228pub mod optimal_transport;
229pub mod option;
230pub mod ord;
231pub mod order;
232pub mod order_topology;
233pub mod ordering;
234pub mod padic_analysis;
235pub mod padic_hodge_theory;
236pub mod parametricity;
237pub mod parsec;
238pub mod pde_theory;
239pub mod persistent_data_structures;
240pub mod point_set_topology;
241pub mod probability;
242pub mod prod;
243pub mod proof_mining;
244pub mod proof_theory;
245pub mod prop;
246pub mod quantum_computing;
247pub mod quantum_field_theory;
248pub mod quantum_information;
249pub mod quotient_types;
250pub mod ramsey_theory;
251pub mod random_matrix_theory;
252pub mod range;
253pub mod rbtree;
254pub mod real;
255pub mod repr;
256pub mod representation_theory;
257pub mod result;
258pub mod reverse_mathematics;
259pub mod set;
260pub mod set_theory_zfc;
261pub mod show;
262pub mod sigma;
263pub mod social_choice_theory;
264pub mod spectral_graph_theory;
265pub mod spectral_theory;
266pub mod statistical_learning;
267pub mod statistical_mechanics;
268pub mod stochastic_control;
269pub mod stochastic_processes;
270pub mod stream;
271pub mod string;
272pub mod sum;
273pub mod symplectic_geometry;
274pub mod tactic_lemmas;
275pub mod tauberian_theory;
276pub mod term_rewriting;
277pub mod thunk;
278pub mod topological_data_analysis;
279pub mod topology;
280pub mod topology_ext;
281pub mod topos_theory;
282pub mod tropical_geometry;
283pub mod type_theory;
284pub mod universal_algebra;
285pub mod variational_calculus;
286pub mod vec;
287pub mod wellfounded;
288
289// Extended modules
290pub mod abstract_algebra_advanced;
291pub mod approximation_algorithms;
292pub mod bayesian_networks;
293pub mod bioinformatics;
294pub mod birational_geometry;
295pub mod categorical_logic;
296pub mod coalgebra_theory;
297pub mod compiler_theory;
298pub mod convex_analysis;
299pub mod cubical_type_theory;
300pub mod differential_privacy;
301pub mod distributed_systems_theory;
302pub mod finite_element_method;
303pub mod formal_argumentation;
304pub mod formal_epistemology;
305pub mod geometric_measure_theory;
306pub mod harmonic_analysis;
307pub mod information_theoretic_security;
308pub mod intersection_theory;
309pub mod knot_theory;
310pub mod lambda_calculus;
311pub mod linear_temporal_logic;
312pub mod logic_programming;
313pub mod low_dimensional_topology;
314pub mod mathematical_ecology;
315pub mod mechanism_design;
316pub mod modal_logic;
317pub mod modular_forms;
318pub mod network_theory;
319pub mod nonstandard_analysis;
320pub mod observational_type_theory;
321pub mod optimization_theory;
322pub mod parameterized_complexity;
323pub mod point_free_topology;
324pub mod post_quantum_crypto;
325pub mod probabilistic_programming;
326pub mod program_extraction;
327pub mod program_logics;
328pub mod program_synthesis;
329pub mod quantum_error_correction;
330pub mod rough_set_theory;
331pub mod session_types;
332pub mod sheaf_theory;
333pub mod spectral_methods;
334pub mod static_analysis;
335pub mod string_theory_basics;
336pub mod surreal_numbers;
337pub mod systems_biology;
338pub mod temporal_logic;
339pub mod topological_quantum_computation;
340pub mod type_directed_search;
341pub mod type_inference_algorithms;
342pub mod type_theory_advanced;
343pub mod variational_analysis;
344pub mod zero_knowledge_proofs;
345
346// ── Registry and utilities sub-modules ───────────────────────────────────────
347pub mod registry;
348pub mod std_utilities;
349
350// ── Re-exports of build_*_env functions ──────────────────────────────────────
351
352pub use algebra::build_algebra_env;
353pub use array::build_array_env;
354pub use bitvec::build_bitvec_env;
355pub use bool::build_bool_env;
356pub use category_theory::build_category_theory_env;
357pub use char::build_char_env;
358pub use decidable::build_decidable_env;
359pub use either::build_either_env;
360pub use eq::build_eq_env;
361pub use fin::build_fin_env;
362pub use functor::build_functor_env;
363pub use group_theory::build_group_theory_env;
364pub use hashmap::build_hashmap_env;
365pub use hashset::build_hashset_env;
366pub use int::build_int_env;
367pub use io::build_io_env;
368pub use lazy::build_lazy_env;
369pub use list::build_list_env;
370pub use logic::build_logic_env;
371pub use monad::build_monad_env;
372pub use nat::build_nat_env;
373pub use option::build_option_env;
374pub use ord::build_ord_env;
375pub use order::build_order_env;
376pub use ordering::build_ordering_env;
377pub use parsec::build_parsec_env;
378pub use prod::build_prod_env;
379pub use prop::build_prop_env;
380pub use quotient_types::build_quotient_types_env;
381pub use range::build_range_env;
382pub use rbtree::build_rbtree_env;
383pub use real::build_real_env;
384pub use repr::build_repr_env;
385pub use result::build_result_env;
386pub use set::build_set_env;
387pub use show::build_show_env;
388pub use sigma::build_sigma_env;
389pub use stream::build_stream_env;
390pub use string::build_string_env;
391pub use sum::build_sum_env;
392pub use tactic_lemmas::build_tactic_lemmas_env;
393pub use thunk::build_thunk_env;
394pub use topology::build_topology_env;
395pub use vec::build_vec_env;
396pub use wellfounded::build_wellfounded_env;
397
398// ── Re-exports from registry ─────────────────────────────────────────────────
399
400pub use registry::{
401    all_modules, all_theorems, count_default_modules, count_total_modules, default_modules,
402    dependents_of, direct_deps, entries_in_module, find_module, lookup_std_entry, module_category,
403    modules_for_phase, topological_sort_modules, BuildPhase, ModuleDep, StdCategory, StdEntry,
404    StdFeatures, StdLibStats, StdModuleEntry, StdVersion, CORE_DEPS, STD_KNOWN_ENTRIES,
405    STD_MODULE_REGISTRY, STD_VERSION,
406};
407
408// ── Re-exports from std_utilities ────────────────────────────────────────────
409
410pub use std_utilities::{
411    BitSet64, Counter, Diagnostic, DiagnosticBag, DiagnosticLevel, DirectedGraph, FreshNameGen,
412    Located, MinHeap, MultiMap, NameTable, ScopeTable, Span, StringSet, Trie,
413};
oxilean_std/lib.rs

oxilean_std/
lib.rs
