Oak Vampire Parser

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

🎯 Overview

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

✨ Features

Complete Vampire Syntax: Supports all Vampire 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_vampire::{VampireLexer, VampireLanguage};
use oak_core::{Lexer, source::SourceText, ParseSession};

let language = VampireLanguage::default();
let lexer = VampireLexer::new(&language);
let vampire_code = r#"
fof(ax1, axiom, (
    ! [A] : ( human(A) => mortal(A) )).

fof(ax2, axiom, (
    human(socrates) )).

fof(conj, conjecture, (
    mortal(socrates) )).
    "#;
    
let source = SourceText::new(vampire_code);
let mut session = ParseSession::<VampireLanguage>::default();
let output = lexer.lex(&source, &[], &mut session);
println!("Parsed Vampire problem successfully.");

📋 Parsing Examples

Problem Parsing

use oak_vampire::{VampireLexer, VampireLanguage};
use oak_core::{Lexer, source::SourceText, ParseSession};

let language = VampireLanguage::default();
let lexer = VampireLexer::new(&language);
let vampire_code = r#"
fof(commutativity, axiom, (
    ! [X, Y] : ( X + Y = Y + X ) )).

fof(associativity, axiom, (
    ! [X, Y, Z] : ( (X + Y) + Z = X + (Y + Z) ) )).

fof(goal, conjecture, (
    ! [A, B, C] : ( A + (B + C) = (C + A) + B ) )).
"#;

let source = SourceText::new(vampire_code);
let mut session = ParseSession::<VampireLanguage>::default();
let output = lexer.lex(&source, &[], &mut session);
println!("Tokens: {}", output.result.map_or(0, |tokens| tokens.len()));

Formula Parsing

use oak_vampire::{VampireLexer, VampireLanguage};
use oak_core::{Lexer, source::SourceText, ParseSession};

let language = VampireLanguage::default();
let lexer = VampireLexer::new(&language);
let formula_code = r#"
! [X, Y] : ( parent(X, Y) => ( ancestor(X, Y) & ~ sibling(X, Y) ) )
"#;

let source = SourceText::new(formula_code);
let mut session = ParseSession::<VampireLanguage>::default();
let output = lexer.lex(&source, &[], &mut session);
println!("Formula tokens: {}", output.result.map_or(0, |tokens| tokens.len()));

🔧 Advanced Features

Token-Level Parsing

use oak_vampire::{VampireLexer, VampireLanguage};
use oak_core::{Lexer, source::SourceText, ParseSession};

let language = VampireLanguage::default();
let lexer = VampireLexer::new(&language);
let source = SourceText::new("fof(ax1, axiom, ( human(socrates) )).");
let mut session = ParseSession::<VampireLanguage>::default();
let output = lexer.lex(&source, &[], &mut session);
println!("Tokens: {}", output.result.map_or(0, |tokens| tokens.len()));

Error Handling

use oak_vampire::{VampireLexer, VampireLanguage};
use oak_core::{Lexer, SourceText, ParseSession};

let language = VampireLanguage::default();
let lexer = VampireLexer::new(&language);
let invalid_code = "fof(invalid syntax here";
let source = SourceText::new(invalid_code);
let mut session = ParseSession::<VampireLanguage>::default();
let output = lexer.lex(&source, &[], &mut session);

if !output.diagnostics.is_empty() {
    for error in output.diagnostics {
        println!("Error: {:?}", error);
    }
}

🏗️ AST Structure

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

Problem: Root container for Vampire problems
Formula: Logical formulas with quantifiers and connectives
Term: Function symbols and variables
Clause: Disjunctions of literals
Literal: Atomic formulas and their negations
Quantifier: Universal and existential quantifiers

📊 Performance

Streaming: Parse large Vampire 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 of vampire integrates seamlessly with:

Theorem Provers: Build automated reasoning systems
Formal Verification: Verify software and hardware correctness
IDE Support: Language server protocol compatibility for Vampire
Educational Tools: Build logic and proof assistants
Research Tools: Support academic research in automated reasoning

📚 Examples

Check out the examples directory for comprehensive examples:

Complete Vampire problem parsing
Formula analysis and transformation
Proof extraction and validation
Integration with development workflows

🤝 Contributing

Contributions are welcome!

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

oak-vampire 0.0.1