Crate logicaffeine_compile 

logicaffeine_compile

The compilation pipeline for LOGOS, transforming natural language logic into executable Rust code.

Architecture

LOGOS Source
     │
     ▼
┌─────────┐     ┌───────────┐     ┌──────────┐
│  Lexer  │ ──▶ │  Parser   │ ──▶ │   AST    │
└─────────┘     └───────────┘     └──────────┘
                                        │
     ┌──────────────────────────────────┘
     ▼
┌─────────────────────────────────────────────┐
│            Analysis Passes                   │
│  ┌─────────┐  ┌───────────┐  ┌───────────┐ │
│  │ Escape  │  │ Ownership │  │    Z3     │ │
│  └─────────┘  └───────────┘  └───────────┘ │
└─────────────────────────────────────────────┘
     │
     ▼
┌──────────┐     ┌────────────┐
│ CodeGen  │ ──▶ │ Rust Code  │
└──────────┘     └────────────┘

Feature Flags

Feature	Description
codegen	Rust code generation (default)
verification	Z3-based static verification

Modules

• compile: Top-level compilation functions
• codegen: AST to Rust code generation (requires codegen feature)
• analysis: Static analysis passes (escape, ownership, discovery)
• extraction: Kernel term extraction to Rust
• interpreter: Tree-walking AST interpreter
• diagnostic: Rustc error translation to LOGOS-friendly messages
• sourcemap: Source location mapping for diagnostics
• loader: Multi-file module loading
• ui_bridge: Web interface integration
• verification: Z3-based static verification (requires verification feature)

Getting Started

Basic Compilation

use logicaffeine_compile::compile::compile_to_rust;

let source = "## Main\nLet x be 5.\nShow x.";
let rust_code = compile_to_rust(source)?;

With Ownership Checking

use logicaffeine_compile::compile::compile_to_rust_checked;

let source = "## Main\nLet x be 5.\nGive x to y.\nShow x.";
// Returns error: use-after-move detected at check-time
let result = compile_to_rust_checked(source);

Interpretation

use logicaffeine_compile::interpret_for_ui;

let source = "## Main\nLet x be 5.\nShow x.";
let result = interpret_for_ui(source).await;
// result.lines contains ["5"]

Re-exports

pub use loader::Loader;

pub use loader::ModuleSource;

pub use compile::CompileOutput;

pub use compile::CrateDependency;

pub use compile::compile_program_full;

pub use ui_bridge::compile_for_ui;

pub use ui_bridge::compile_for_proof;

pub use ui_bridge::compile_theorem_for_ui;

pub use ui_bridge::verify_theorem;

pub use ui_bridge::interpret_for_ui;

pub use ui_bridge::interpret_for_ui_sync;

pub use ui_bridge::interpret_streaming;

pub use ui_bridge::CompileResult;

pub use ui_bridge::ProofCompileResult;

pub use ui_bridge::TheoremCompileResult;

pub use ui_bridge::AstNode;

pub use ui_bridge::TokenInfo;

pub use ui_bridge::TokenCategory;

pub use ui_bridge::generate_rust_code;codegen

pub use logicaffeine_kernel as kernel;

Modules

analysis

Compile-time analysis passes for the LOGOS compilation pipeline.

arena

arena_ctx

ast

Abstract Syntax Tree types for both logical expressions and imperative statements.

codegencodegen

Code generation from LOGOS AST to Rust source code.

compile

LOGOS Compilation Pipeline

diagnostic

Diagnostic bridge for translating Rust errors to LOGOS.

drs

Discourse Representation Structure (DRS) for anaphora resolution and scope tracking.

error

Error types and display formatting for parse errors.

extraction

Program extraction from kernel terms to Rust.

formatter

Output formatters for logical expressions.

intern

interpreter

Tree-walking interpreter for LOGOS imperative code.

lexer

Two-stage lexer for LOGOS natural language input.

loader

Module loader for multi-file LOGOS projects.

mwe

Multi-Word Expression (MWE) processing.

optimize

parser

Recursive descent parser for natural language to first-order logic.

registry

sourcemap

Source map for the diagnostic bridge.

style

token

Token types for the LOGOS lexer and parser.

ui_bridge

UI bridge for web interface integration.

Structs

Arena

A bump allocator for stable, arena-allocated references.

AstContext

Collection of typed arenas for AST allocation during parsing.

DiscoveryPass

Discovery pass that scans tokens before main parsing to build a TypeRegistry.

Interner

A string interner providing O(1) equality comparison via Symbol handles.

Lexer

ParseError

A parse error with location information.

Parser

Recursive descent parser for natural language to first-order logic.

PolicyRegistry

Registry for security policies defined in ## Policy blocks.

Symbol

A lightweight handle to an interned string.

SymbolRegistry

Registry for mapping words to FOL variable names.

TypeRegistry

Enums

PolicyCondition

Condition in a policy definition. Represents the predicate logic for security rules.

Traits

SymbolEq

Convenience trait for comparing a Symbol to a string literal.