logicaffeine_compile/
lib.rs

1#![cfg_attr(docsrs, feature(doc_cfg))]
2#![doc = include_str!("../README.md")]
3
4// Re-export base types
5pub use logicaffeine_base::{Arena, Interner, Symbol, SymbolEq};
6
7// Re-export language types needed for compilation
8pub use logicaffeine_language::{
9    ast, drs, error, lexer, optimization, parser, token,
10    analysis::{TypeRegistry, DiscoveryPass, PolicyRegistry, PolicyCondition},
11    arena_ctx::AstContext,
12    registry::SymbolRegistry,
13    formatter,
14    mwe,
15    Lexer, Parser, ParseError,
16};
17
18// Re-export kernel for extraction
19pub use logicaffeine_kernel as kernel;
20
21// Module loading
22pub mod loader;
23pub use loader::{Loader, ModuleSource};
24
25// Compile-time analysis
26pub mod analysis;
27
28// Concurrency determinacy model + classifier (Phase 0 of work/FINISH_INTERPRETER.md).
29// Pure AST analysis — independent of the codegen feature.
30pub mod concurrency;
31
32// Code generation
33#[cfg(feature = "codegen")]
34pub mod codegen;
35
36// Counted-loop recognition shared by the for-range peephole and the unroller.
37// Gated with codegen because it reuses the peephole's pure-AST guard helpers;
38// the only consumer is the AOT (Rust-emitting) pipeline.
39#[cfg(feature = "codegen")]
40pub(crate) mod loop_shape;
41
42// C code generation (benchmark-only subset)
43#[cfg(feature = "codegen")]
44pub mod codegen_c;
45
46// SVA/PSL code generation for hardware verification
47pub mod codegen_sva;
48
49// Compilation pipeline
50pub mod compile;
51pub use compile::{CompileOutput, CrateDependency, classify_source, compile_program_full, compile_program_full_deterministic, compile_program_full_with_proven, compile_to_rust, compile_to_rust_deterministic, compile_to_rust_with_proven, first_parallel_block_independent, send_check_source};
52
53// Diagnostics
54pub mod diagnostic;
55
56// Source mapping
57pub mod sourcemap;
58
59// Extraction (proof term extraction)
60pub mod extraction;
61
62// Optimization passes
63pub mod optimize;
64
65// Interpreter
66pub mod interpreter;
67
68// Tail-call recognition shared by all three execution tiers (tree-walker, VM,
69// AOT) so "a self-tail-call runs in constant stack" is one definition, not three.
70pub(crate) mod tail_call;
71
72// Type-directed division resolution: rewrites `Divide → ExactDivide` where a `/`'s
73// result flows into a `Rational` context (the default stays floor — zero breakage).
74pub(crate) mod resolve_division;
75
76// Shared semantics kernel — ONE implementation of value semantics used by the
77// tree-walker, the bytecode VM, and (later) the JIT slow paths.
78pub mod semantics;
79
80// Register bytecode VM (fast portable interpreter — WASM engine + JIT substrate).
81pub mod vm;
82
83// The Studio bytecode debugger (step / breakpoints / time-travel). Zero production
84// cost — nothing here is on the execution path.
85pub mod debug;
86
87// UI Bridge - high-level compilation for web interface
88pub mod ui_bridge;
89
90// The replay-based interactive session behind `largo repl`.
91pub mod repl;
92pub use repl::{ReplOutcome, ReplSession};
93
94#[cfg(feature = "verification")]
95pub mod defeasible;
96
97// Verification pass (Z3-based, requires verification feature)
98#[cfg(feature = "verification")]
99pub mod verification;
100#[cfg(feature = "verification")]
101pub use verification::VerificationPass;
102
103// Re-export UI types at crate root for convenience
104pub use ui_bridge::{
105    answer_question, compile_for_ui, compile_for_proof, compile_theorem_for_ui,
106    grounded_grid_problem, solve_grid, SolvedGrid, GridColumn,
107    prove_theorem_trace, theorem_proof_exprs, theorem_dependency_graph, verify_theorem, TheoremTrace,
108    interpret_for_ui, interpret_for_ui_with_args, interpret_for_ui_sync,
109    interpret_for_ui_sync_with_args, interpret_for_ui_baseline,
110    interpret_for_ui_baseline_with_args, interpret_for_ui_baseline_sync_with_args,
111    interpret_streaming, interpret_streaming_with_vfs, interpret_streaming_with_vfs_observer,
112    ObserverCallback, run_vm_concurrent, run_vm_net_async,
113    run_vm_concurrent_seeded, run_treewalker_concurrent_seeded,
114    CompileResult, ProofCompileResult,
115    TheoremCompileResult, AstNode, TokenInfo, TokenCategory,
116    extract_math_rust, extract_math_rust_from_source, extract_logic_rust, parse_math_statements,
117    extract_math_module, extract_math_module_from_source, extract_logic_module, partition_mixed,
118};
119
120// The work-stealing M:N driver is native-only (no OS threads on wasm32).
121#[cfg(not(target_arch = "wasm32"))]
122pub use ui_bridge::run_vm_workstealing_seeded;
123#[cfg(feature = "codegen")]
124pub use ui_bridge::{generate_rust_code, generate_rust_code_with_proven};
125#[cfg(feature = "verification")]
126pub use ui_bridge::{
127    check_theorem_defeasible, check_theorem_defeasible_consistent,
128    check_theorem_premises_consistent, check_theorem_smt,
129};
130
131// Provide module aliases for internal code
132pub mod intern {
133    pub use logicaffeine_base::{Interner, Symbol, SymbolEq};
134}
135
136pub mod arena {
137    pub use logicaffeine_base::Arena;
138}
139
140pub mod arena_ctx {
141    pub use logicaffeine_language::arena_ctx::*;
142}
143
144pub mod registry {
145    pub use logicaffeine_language::registry::*;
146}
147
148pub mod style {
149    pub use logicaffeine_language::style::*;
150}
logicaffeine_compile/lib.rs

logicaffeine_compile/
lib.rs
