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

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> {
    pub file: &'a [u8],
    pub version: u8,
    pub num_sorts: u8,
    pub num_terms: u32,
    pub num_theorems: u32,
    pub sorts: &'a [u8],
    pub terms: &'a [u8],
    pub theorems: &'a [u8],
    pub proofs: &'a [u8],
    pub sort_index: &'a [u8],
    pub term_index: &'a [u8],
    pub theorem_index: &'a [u8],
}

impl<'a> Mmb<'a> {
    pub fn from(file: &'a [u8]) -> Option<Mmb<'a>> {
        parser::parse(file).map(|x| x.1).ok()
    }

    pub fn visit_sort_index<V: index::Visitor>(&self, visitor: &mut V) {
        parser::parse_index(self.file, self.sort_index, self.num_sorts as usize, visitor).unwrap();
    }

    pub fn visit_term_index<V: index::Visitor>(&self, visitor: &mut V) {
        parser::parse_index(self.file, self.term_index, self.num_terms as usize, visitor).unwrap();
    }

    pub fn visit_theorem_index<V: index::Visitor>(&self, visitor: &mut V) {
        parser::parse_index(
            self.file,
            self.theorem_index,
            self.num_theorems as usize,
            visitor,
        )
        .unwrap();
    }

    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(())
    }
}