Skip to main content

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}