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
pub use mmb_types::opcode;
mod error;
pub mod index;
mod parser;
pub mod visitor;
pub use visitor::{ProofStream, UnifyStream, Visitor};
#[derive(Debug)]
pub struct Mmb<'a> {
file: &'a [u8],
version: u8,
num_sorts: u8,
num_terms: u32,
num_theorems: u32,
sorts: &'a [u8],
terms: &'a [u8],
theorems: &'a [u8],
proofs: &'a [u8],
index: Option<index::Index<'a>>,
}
impl<'a> Mmb<'a> {
pub fn from(file: &'a [u8]) -> Option<Mmb<'a>> {
parser::parse(file).map(|x| x.1).ok()
}
pub fn file(&self) -> &[u8] {
self.file
}
pub fn version(&self) -> u8 {
self.version
}
pub fn num_sorts(&self) -> u8 {
self.num_sorts
}
pub fn num_terms(&self) -> u32 {
self.num_terms
}
pub fn num_theorems(&self) -> u32 {
self.num_theorems
}
pub fn sorts(&self) -> &[u8] {
self.sorts
}
pub fn terms(&self) -> &[u8] {
self.terms
}
pub fn theorems(&self) -> &[u8] {
self.theorems
}
pub fn proofs(&self) -> &[u8] {
self.proofs
}
pub fn index(&self) -> Option<&index::Index> {
self.index.as_ref()
}
pub fn visit<V: Visitor<'a>>(
&self,
visitor: &mut V,
) -> Result<(), nom::Err<error::ParseError>> {
let (_, _) = parser::parse_sorts(self.sorts, self.num_sorts, visitor)?;
let (_, _) = parser::scan_statement_stream(self.proofs, visitor)?;
let (_, _) = parser::parse_terms(self.file, self.terms, self.num_terms as usize, visitor)?;
let (_, _) = parser::parse_theorems(
self.file,
self.theorems,
self.num_theorems as usize,
visitor,
)?;
Ok(())
}
}