mmb_parser/
lib.rs

1pub use mmb_types::opcode;
2mod error;
3pub mod index;
4mod parser;
5pub mod visitor;
6
7pub use visitor::{ProofStream, UnifyStream, Visitor};
8
9#[derive(Debug)]
10pub struct Mmb<'a> {
11    file: &'a [u8],
12    version: u8,
13    num_sorts: u8,
14    num_terms: u32,
15    num_theorems: u32,
16    sorts: &'a [u8],
17    terms: &'a [u8],
18    theorems: &'a [u8],
19    proofs: &'a [u8],
20    index: Option<index::Index<'a>>,
21}
22
23impl<'a> Mmb<'a> {
24    /// Build a `Mmb` struct by parsing the file header
25    pub fn from(file: &'a [u8]) -> Option<Mmb<'a>> {
26        let file = parser::parse(file);
27        let x = file.unwrap();
28        Some(x.1)
29    }
30
31    /// Return the slice containing the entire file
32    pub fn file(&self) -> &[u8] {
33        self.file
34    }
35
36    /// Return the version of the proof file format
37    pub fn version(&self) -> u8 {
38        self.version
39    }
40
41    /// Return the number of sorts in the sort table
42    pub fn num_sorts(&self) -> u8 {
43        self.num_sorts
44    }
45
46    /// Return the number of terms in the term table
47    pub fn num_terms(&self) -> u32 {
48        self.num_terms
49    }
50
51    /// Return the number of theorems in the theorem table
52    pub fn num_theorems(&self) -> u32 {
53        self.num_theorems
54    }
55
56    /// Return the slice containing the sort table
57    pub fn sorts(&self) -> &[u8] {
58        self.sorts
59    }
60
61    /// Return the slice containing the term table
62    pub fn terms(&self) -> &[u8] {
63        self.terms
64    }
65
66    /// Return the slice containing the theorem table
67    pub fn theorems(&self) -> &[u8] {
68        self.theorems
69    }
70
71    /// Return the slice containing the proof section
72    pub fn proofs(&self) -> &[u8] {
73        self.proofs
74    }
75
76    /// Return a reference to the optional index section
77    pub fn index(&self) -> Option<&index::Index> {
78        self.index.as_ref()
79    }
80
81    pub fn visit<V: Visitor<'a>>(
82        &self,
83        visitor: &mut V,
84    ) -> Result<(), nom::Err<error::ParseError>> {
85        let (_, _) = parser::parse_sorts(self.sorts, self.num_sorts, visitor)?;
86        let (_, _) = parser::scan_statement_stream(self.proofs, visitor)?;
87        let (_, _) = parser::parse_terms(self.file, self.terms, self.num_terms as usize, visitor)?;
88        let (_, _) = parser::parse_theorems(
89            self.file,
90            self.theorems,
91            self.num_theorems as usize,
92            visitor,
93        )?;
94
95        Ok(())
96    }
97}
mmb_parser/lib.rs

mmb_parser/
lib.rs
