mmb_parser/
index.rs

1/// Index
2/// The index contains information about items in the proof file that are useful
3/// for printing and debugging purposes.
4///
5/// The index is a collection of tables that in turn contain domain specific
6/// data. Because the index is designed to be extensible, each table entry is
7/// identified by an id that determines how the data should be interpreted.
8#[derive(Debug)]
9pub struct Index<'a> {
10    pub(crate) file: &'a [u8],
11
12    pub(crate) num_sorts: u8,
13    pub(crate) num_terms: u32,
14    pub(crate) num_theorems: u32,
15
16    /// The number of table entries in the index
17    pub(crate) num_entries: u64,
18
19    /// The slice containing the table entries.
20    pub(crate) entries: &'a [u8],
21}
22
23use crate::parser;
24
25pub use self::name_table::NameTable;
26
27pub mod name_table;
28
29impl<'a> Index<'a> {
30    /// Returns an iterator over all table entries in the index.
31    pub fn iter(&self) -> EntryIterator<'a> {
32        EntryIterator {
33            entries: self.entries,
34        }
35    }
36}
37
38impl<'a> IntoIterator for Index<'a> {
39    type Item = Entry;
40    type IntoIter = EntryIterator<'a>;
41
42    fn into_iter(self) -> Self::IntoIter {
43        self.iter()
44    }
45}
46
47impl<'a> IntoIterator for &Index<'a> {
48    type Item = Entry;
49    type IntoIter = EntryIterator<'a>;
50
51    fn into_iter(self) -> Self::IntoIter {
52        self.iter()
53    }
54}
55
56/// An iterator over table entries in the index.
57pub struct EntryIterator<'a> {
58    entries: &'a [u8],
59}
60
61/// A table entry in the index.
62#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
63pub struct Entry {
64    pub(crate) id: u32,
65    pub(crate) ptr: u64,
66}
67
68const NAME_TABLE_ID: u32 = 0x656d614e;
69
70impl Entry {
71    /// If this table entry is a name table, return a `NameTable` object to the
72    /// name table, or `None` otherwise.
73    ///
74    /// Because the name table contains file relative pointers, we need the
75    /// original index as a parameter to resolve these.
76    pub fn as_name_table<'a>(&self, index: &Index<'a>) -> Option<NameTable<'a>> {
77        if self.id != NAME_TABLE_ID {
78            return None;
79        }
80
81        let num = index.num_sorts as u64 + index.num_terms as u64 + index.num_theorems as u64;
82        let entries = parser::parse_name_entries(index.file, num, self.ptr)
83            .ok()?
84            .1;
85
86        Some(NameTable::new(
87            index.num_sorts,
88            index.num_terms,
89            index.num_theorems,
90            index.file,
91            entries,
92        ))
93    }
94}
95
96impl<'a> Iterator for EntryIterator<'a> {
97    type Item = Entry;
98
99    fn next(&mut self) -> Option<Self::Item> {
100        let (left, entry) = parser::parse_index_entry(self.entries).ok()?;
101
102        self.entries = left;
103
104        Some(entry)
105    }
106}
mmb_parser/index.rs

mmb_parser/
index.rs
