Oak Lean Parser

High-performance incremental Lean parser for the oak ecosystem with flexible configuration, optimized for theorem proving and formal verification.

🎯 Overview

Oak Lean is a robust parser for Lean theorem prover, designed to handle complete Lean syntax including modern features. Built on the solid foundation of oak-core, it provides both high-level convenience and detailed AST generation for theorem proving and formal verification.

✨ Features

Complete Lean Syntax: Supports all Lean features including modern specifications
Full AST Generation: Generates comprehensive Abstract Syntax Trees
Lexer Support: Built-in tokenization with proper span information
Error Recovery: Graceful handling of syntax errors with detailed diagnostics

🚀 Quick Start

Basic example:

use oak_lean::{Parser, LeanLanguage, SourceText};

fn main() -> Result<(), Box<dyn std::error::Error>> {
    let parser = Parser::new();
    let source = SourceText::new(r#"
def factorial : ℕ → ℕ
| 0 := 1
| (n + 1) := (n + 1) * factorial n

theorem factorial_pos (n : ℕ) : factorial n > 0 :=
begin
    induction n with n ih,
    { simp [factorial] },
    { simp [factorial, ih, mul_pos] }
end
    "#);
    
    let result = parser.parse(&source);
    println!("Parsed Lean successfully.");
    Ok(())
}

📋 Parsing Examples

Definition Parsing

use oak_lean::{Parser, LeanLanguage, SourceText};

let parser = Parser::new();
let source = SourceText::new(r#"
def is_even (n : ℕ) := ∃ k, n = 2 * k

theorem even_plus_even_is_even (m n : ℕ) 
    (h₁ : is_even m) (h₂ : is_even n) : is_even (m + n) :=
begin
    cases h₁ with k hk,
    cases h₂ with l hl,
    use k + l,
    rw [hk, hl],
    ring,
end
"#);

let result = parser.parse(&source);
println!("Definition parsed successfully.");

Inductive Type Parsing

use oak_lean::{Parser, LeanLanguage, SourceText};

let parser = Parser::new();
let source = SourceText::new(r#"
inductive tree (α : Type)
| leaf : tree
| node : α → tree → tree → tree
"#);

let result = parser.parse(&source);
println!("Inductive type parsed successfully.");

🔧 Advanced Features

Token-Level Parsing

use oak_lean::{Parser, LeanLanguage, SourceText};

let parser = Parser::new();
let source = SourceText::new("def hello := \"world\"");
let result = parser.parse(&source);
println!("Token parsing completed.");

Error Handling

use oak_lean::{Parser, LeanLanguage, SourceText};

let parser = Parser::new();
let source = SourceText::new(r#"
def broken_function
    println("Hello")
    // Missing function parameters and return type
"#);

let result = parser.parse(&source);
if let Some(errors) = result.result.err() {
    println!("Parse errors found: {:?}", errors);
} else {
    println!("Parsed successfully.");
}

🏗️ AST Structure

The parser generates a comprehensive AST with the following main structures:

LeanProgram: Root container for Lean programs
Definition: Lean function and constant definitions
Theorem: Lean theorem statements and proofs
Inductive: Lean inductive type definitions
Structure: Lean structure/record definitions
Expression: Lean expressions and terms
TacticBlock: Lean tactic proof blocks

📊 Performance

Streaming: Parse large Lean files without loading entirely into memory
Incremental: Re-parse only changed sections
Memory Efficient: Smart AST node allocation
Fast Recovery: Quick error recovery for better IDE integration

🔗 Integration

Oak Lean integrates seamlessly with:

Theorem Proving: Lean code analysis and verification
Formal Verification: Processing and transforming Lean proofs
IDE Support: Language server protocol compatibility
Code Generation: Generating code from Lean AST
Documentation: Generating documentation from Lean code

📚 Examples

Check out the examples directory for comprehensive examples:

Complete Lean program parsing
Definition and theorem analysis
Proof transformation
Integration with development workflows

🤝 Contributing

Contributions are welcome!

Please feel free to submit pull requests at the project repository or open issues.

oak-lean 0.0.0