logicaffeine_compile/
lib.rs

1#![cfg_attr(docsrs, feature(doc_cfg))]
2
3//! # logicaffeine_compile
4//!
5//! The compilation pipeline for LOGOS, transforming natural language logic
6//! into executable Rust code.
7//!
8//! ## Architecture
9//!
10//! ```text
11//! LOGOS Source
12//!      │
13//!      ▼
14//! ┌─────────┐     ┌───────────┐     ┌──────────┐
15//! │  Lexer  │ ──▶ │  Parser   │ ──▶ │   AST    │
16//! └─────────┘     └───────────┘     └──────────┘
17//!                                         │
18//!      ┌──────────────────────────────────┘
19//!      ▼
20//! ┌─────────────────────────────────────────────┐
21//! │            Analysis Passes                   │
22//! │  ┌─────────┐  ┌───────────┐  ┌───────────┐ │
23//! │  │ Escape  │  │ Ownership │  │    Z3     │ │
24//! │  └─────────┘  └───────────┘  └───────────┘ │
25//! └─────────────────────────────────────────────┘
26//!      │
27//!      ▼
28//! ┌──────────┐     ┌────────────┐
29//! │ CodeGen  │ ──▶ │ Rust Code  │
30//! └──────────┘     └────────────┘
31//! ```
32//!
33//! ## Feature Flags
34//!
35//! | Feature | Description |
36//! |---------|-------------|
37//! | `codegen` | Rust code generation (default) |
38//! | `verification` | Z3-based static verification |
39//!
40//! ## Modules
41//!
42//! - [`compile`]: Top-level compilation functions
43//! - [`codegen`]: AST to Rust code generation (requires `codegen` feature)
44//! - [`analysis`]: Static analysis passes (escape, ownership, discovery)
45//! - [`extraction`]: Kernel term extraction to Rust
46//! - [`interpreter`]: Tree-walking AST interpreter
47//! - [`diagnostic`]: Rustc error translation to LOGOS-friendly messages
48//! - [`sourcemap`]: Source location mapping for diagnostics
49//! - [`loader`]: Multi-file module loading
50//! - [`ui_bridge`]: Web interface integration
51//! - `verification`: Z3-based static verification (requires `verification` feature)
52//!
53//! ## Getting Started
54//!
55//! ### Basic Compilation
56//!
57//! ```
58//! use logicaffeine_compile::compile::compile_to_rust;
59//! # use logicaffeine_compile::ParseError;
60//! # fn main() -> Result<(), ParseError> {
61//!
62//! let source = "## Main\nLet x be 5.\nShow x.";
63//! let rust_code = compile_to_rust(source)?;
64//! # Ok(())
65//! # }
66//! ```
67//!
68//! ### With Ownership Checking
69//!
70//! ```
71//! use logicaffeine_compile::compile::compile_to_rust_checked;
72//!
73//! let source = "## Main\nLet x be 5.\nGive x to y.\nShow x.";
74//! // Returns error: use-after-move detected at check-time
75//! let result = compile_to_rust_checked(source);
76//! ```
77//!
78//! ### Interpretation
79//!
80//! ```no_run
81//! use logicaffeine_compile::interpret_for_ui;
82//!
83//! # fn main() {}
84//! # async fn example() {
85//! let source = "## Main\nLet x be 5.\nShow x.";
86//! let result = interpret_for_ui(source).await;
87//! // result.lines contains ["5"]
88//! # }
89//! ```
90
91// Re-export base types
92pub use logicaffeine_base::{Arena, Interner, Symbol, SymbolEq};
93
94// Re-export language types needed for compilation
95pub use logicaffeine_language::{
96    ast, drs, error, lexer, parser, token,
97    analysis::{TypeRegistry, DiscoveryPass, PolicyRegistry, PolicyCondition},
98    arena_ctx::AstContext,
99    registry::SymbolRegistry,
100    formatter,
101    mwe,
102    Lexer, Parser, ParseError,
103};
104
105// Re-export kernel for extraction
106pub use logicaffeine_kernel as kernel;
107
108// Module loading
109pub mod loader;
110pub use loader::{Loader, ModuleSource};
111
112// Compile-time analysis
113pub mod analysis;
114
115// Code generation
116#[cfg(feature = "codegen")]
117pub mod codegen;
118
119// Compilation pipeline
120pub mod compile;
121pub use compile::{CompileOutput, CrateDependency, compile_program_full};
122
123// Diagnostics
124pub mod diagnostic;
125
126// Source mapping
127pub mod sourcemap;
128
129// Extraction (proof term extraction)
130pub mod extraction;
131
132// Optimization passes
133pub mod optimize;
134
135// Interpreter
136pub mod interpreter;
137
138// UI Bridge - high-level compilation for web interface
139pub mod ui_bridge;
140
141// Verification pass (Z3-based, requires verification feature)
142#[cfg(feature = "verification")]
143pub mod verification;
144#[cfg(feature = "verification")]
145pub use verification::VerificationPass;
146
147// Re-export UI types at crate root for convenience
148pub use ui_bridge::{
149    compile_for_ui, compile_for_proof, compile_theorem_for_ui, verify_theorem,
150    interpret_for_ui, interpret_for_ui_sync, interpret_streaming, CompileResult, ProofCompileResult, TheoremCompileResult,
151    AstNode, TokenInfo, TokenCategory,
152};
153#[cfg(feature = "codegen")]
154pub use ui_bridge::generate_rust_code;
155
156// Provide module aliases for internal code
157pub mod intern {
158    pub use logicaffeine_base::{Interner, Symbol, SymbolEq};
159}
160
161pub mod arena {
162    pub use logicaffeine_base::Arena;
163}
164
165pub mod arena_ctx {
166    pub use logicaffeine_language::arena_ctx::*;
167}
168
169pub mod registry {
170    pub use logicaffeine_language::registry::*;
171}
172
173pub mod style {
174    pub use logicaffeine_language::style::*;
175}
logicaffeine_compile/lib.rs

logicaffeine_compile/
lib.rs
