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//! ```ignore
58//! use logicaffeine_compile::compile::compile_to_rust;
59//!
60//! let source = "## Main\nLet x be 5.\nShow x to show.";
61//! let rust_code = compile_to_rust(source)?;
62//! ```
63//!
64//! ### With Ownership Checking
65//!
66//! ```ignore
67//! use logicaffeine_compile::compile::compile_to_rust_checked;
68//!
69//! let source = "## Main\nLet x be 5.\nGive x to show.\nShow x to show.";
70//! // Returns error: use-after-move detected at check-time
71//! let result = compile_to_rust_checked(source);
72//! ```
73//!
74//! ### Interpretation
75//!
76//! ```ignore
77//! use logicaffeine_compile::interpret_for_ui;
78//!
79//! let source = "## Main\nLet x be 5.\nShow x to show.";
80//! let result = interpret_for_ui(source).await;
81//! // result.lines contains ["5"]
82//! ```
83
84// Re-export base types
85pub use logicaffeine_base::{Arena, Interner, Symbol, SymbolEq};
86
87// Re-export language types needed for compilation
88pub use logicaffeine_language::{
89 ast, drs, error, lexer, parser, token,
90 analysis::{TypeRegistry, DiscoveryPass, PolicyRegistry, PolicyCondition},
91 arena_ctx::AstContext,
92 registry::SymbolRegistry,
93 formatter,
94 mwe,
95 Lexer, Parser, ParseError,
96};
97
98// Re-export kernel for extraction
99pub use logicaffeine_kernel as kernel;
100
101// Module loading
102pub mod loader;
103pub use loader::{Loader, ModuleSource};
104
105// Compile-time analysis
106pub mod analysis;
107
108// Code generation
109#[cfg(feature = "codegen")]
110pub mod codegen;
111
112// Compilation pipeline
113pub mod compile;
114pub use compile::{CompileOutput, CrateDependency};
115
116// Diagnostics
117pub mod diagnostic;
118
119// Source mapping
120pub mod sourcemap;
121
122// Extraction (proof term extraction)
123pub mod extraction;
124
125// Interpreter
126pub mod interpreter;
127
128// UI Bridge - high-level compilation for web interface
129pub mod ui_bridge;
130
131// Verification pass (Z3-based, requires verification feature)
132#[cfg(feature = "verification")]
133pub mod verification;
134#[cfg(feature = "verification")]
135pub use verification::VerificationPass;
136
137// Re-export UI types at crate root for convenience
138pub use ui_bridge::{
139 compile_for_ui, compile_for_proof, compile_theorem_for_ui, verify_theorem,
140 interpret_for_ui, interpret_streaming, CompileResult, ProofCompileResult, TheoremCompileResult,
141 AstNode, TokenInfo, TokenCategory,
142};
143#[cfg(feature = "codegen")]
144pub use ui_bridge::generate_rust_code;
145
146// Provide module aliases for internal code
147pub mod intern {
148 pub use logicaffeine_base::{Interner, Symbol, SymbolEq};
149}
150
151pub mod arena {
152 pub use logicaffeine_base::Arena;
153}
154
155pub mod arena_ctx {
156 pub use logicaffeine_language::arena_ctx::*;
157}
158
159pub mod registry {
160 pub use logicaffeine_language::registry::*;
161}
162
163pub mod style {
164 pub use logicaffeine_language::style::*;
165}