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