oak-vampire 0.0.0

Vampire theorem prover language parser with support for automated theorem proving and first-order logic.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159

# Oak Vampire Parser


[![Crates.io](https://img.shields.io/crates/v/oak-vampire.svg)](https://crates.io/crates/oak-vampire)
[![Documentation](https://docs.rs/oak-vampire/badge.svg)](https://docs.rs/oak-vampire)

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:

```rust,no_run
use oak_vampire::{VampireLexer, VampireLanguage};
use oak_core::{Lexer, SourceText};

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 output = lexer.lex(&source);
println!("Parsed Vampire problem successfully.");
```

## 📋 Parsing Examples


### Problem Parsing

```rust,no_run
use oak_vampire::{VampireLexer, VampireLanguage, ast::ValkyrieModule};
use oak_core::{Lexer, SourceText};

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 output = lexer.lex(&source);
println!("Tokens: {}", output.result.map_or(0, |tokens| tokens.len()));
```

### Formula Parsing

```rust,no_run
use oak_vampire::{VampireLexer, VampireLanguage, ast::ValkyrieInstruction};
use oak_core::{Lexer, SourceText};

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 output = lexer.lex(source);
println!("Formula tokens: {}", output.result.map_or(0, |tokens| tokens.len()));
```

## 🔧 Advanced Features


### Token-Level Parsing

```rust,no_run
use oak_vampire::{VampireLexer, VampireLanguage};
use oak_core::{Lexer, SourceText};

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

### Error Handling

```rust,no_run
use oak_vampire::{VampireLexer, VampireLanguage};
use oak_core::{Lexer, SourceText};

let language = VampireLanguage::default();
let lexer = VampireLexer::new(&language);
let invalid_code = "fof(invalid syntax here";
let source = SourceText::new(invalid_code);
let output = lexer.lex(source);

if let Some(errors) = output.errors {
    for error in errors {
        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](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](https://github.com/ygg-lang/oaks/tree/dev/examples/oak-vampire) or open [issues](https://github.com/ygg-lang/oaks/issues).