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;
114
115// Diagnostics
116pub mod diagnostic;
117
118// Source mapping
119pub mod sourcemap;
120
121// Extraction (proof term extraction)
122pub mod extraction;
123
124// Interpreter
125pub mod interpreter;
126
127// UI Bridge - high-level compilation for web interface
128pub mod ui_bridge;
129
130// Verification pass (Z3-based, requires verification feature)
131#[cfg(feature = "verification")]
132pub mod verification;
133#[cfg(feature = "verification")]
134pub use verification::VerificationPass;
135
136// Re-export UI types at crate root for convenience
137pub use ui_bridge::{
138    compile_for_ui, compile_for_proof, compile_theorem_for_ui, verify_theorem,
139    interpret_for_ui, CompileResult, ProofCompileResult, TheoremCompileResult,
140    AstNode, TokenInfo, TokenCategory,
141};
142#[cfg(feature = "codegen")]
143pub use ui_bridge::generate_rust_code;
144
145// Provide module aliases for internal code
146pub mod intern {
147    pub use logicaffeine_base::{Interner, Symbol, SymbolEq};
148}
149
150pub mod arena {
151    pub use logicaffeine_base::Arena;
152}
153
154pub mod arena_ctx {
155    pub use logicaffeine_language::arena_ctx::*;
156}
157
158pub mod registry {
159    pub use logicaffeine_language::registry::*;
160}
161
162pub mod style {
163    pub use logicaffeine_language::style::*;
164}
logicaffeine_compile/lib.rs

logicaffeine_compile/
lib.rs
