mmb_parser/index/
name_table.rs

1/// The name table of the index defines the names and pointers to the
2/// declarations of sorts, terms and theorems in the proof file.
3pub struct NameTable<'a> {
4    num_sorts: u8,
5    num_terms: u32,
6    num_theorems: u32,
7
8    file: &'a [u8],
9    entries: &'a [u8],
10}
11
12/// A subsection of the name table containing only a single kind of entry.
13pub struct NameTableSection<'a> {
14    file: &'a [u8],
15    entries: &'a [u8],
16}
17
18use crate::parser;
19
20impl<'a> NameTableSection<'a> {
21    /// Returns an entry of the name table by index, or `None` if the index is
22    /// out of range.
23    pub fn get(&self, idx: u64) -> Option<Name<'_>> {
24        let name = parser::seek_name_entry(self.file, self.entries, idx).ok()?;
25
26        Some(name.1)
27    }
28
29    /// Returns an iterator over all entries in this subsection of the name table.
30    pub fn iter(&self) -> NameIterator<'a> {
31        NameIterator {
32            file: self.file,
33            entries: self.entries,
34        }
35    }
36}
37
38impl<'a> NameTable<'a> {
39    pub(crate) fn new(
40        num_sorts: u8,
41        num_terms: u32,
42        num_theorems: u32,
43        file: &'a [u8],
44        entries: &'a [u8],
45    ) -> NameTable<'a> {
46        NameTable {
47            num_sorts,
48            num_terms,
49            num_theorems,
50            file,
51            entries,
52        }
53    }
54
55    /// Returns the subsection of the name table containing the sorts.
56    pub fn sorts(&self) -> NameTableSection<'_> {
57        let from = 0;
58        let len = self.num_sorts as u64;
59
60        self.kind(from, len)
61    }
62
63    /// Returns the subsection of the name table containing the terms.
64    pub fn terms(&self) -> NameTableSection<'_> {
65        let from = self.num_sorts as u64;
66        let len = self.num_terms as u64;
67
68        self.kind(from, len)
69    }
70
71    /// Returns the subsection of the name table containing the theorems.
72    pub fn theorems(&self) -> NameTableSection<'_> {
73        let from = self.num_sorts as u64 + self.num_terms as u64;
74        let len = self.num_theorems as u64;
75
76        self.kind(from, len)
77    }
78
79    /// Returns an iterator over all entries in the entire name table.
80    pub fn iter(&self) -> NameIterator<'a> {
81        NameIterator {
82            file: self.file,
83            entries: self.entries,
84        }
85    }
86
87    fn kind(&self, from: u64, len: u64) -> NameTableSection<'_> {
88        let entries = parser::subslice_name_table(self.entries, from, len)
89            .ok()
90            .unwrap()
91            .1;
92
93        NameTableSection {
94            file: self.file,
95            entries,
96        }
97    }
98}
99
100impl<'a> IntoIterator for NameTable<'a> {
101    type Item = Name<'a>;
102    type IntoIter = NameIterator<'a>;
103
104    fn into_iter(self) -> Self::IntoIter {
105        self.iter()
106    }
107}
108
109impl<'a> IntoIterator for &NameTable<'a> {
110    type Item = Name<'a>;
111    type IntoIter = NameIterator<'a>;
112
113    fn into_iter(self) -> Self::IntoIter {
114        self.iter()
115    }
116}
117
118impl<'a> IntoIterator for NameTableSection<'a> {
119    type Item = Name<'a>;
120    type IntoIter = NameIterator<'a>;
121
122    fn into_iter(self) -> Self::IntoIter {
123        self.iter()
124    }
125}
126
127impl<'a> IntoIterator for &NameTableSection<'a> {
128    type Item = Name<'a>;
129    type IntoIter = NameIterator<'a>;
130
131    fn into_iter(self) -> Self::IntoIter {
132        self.iter()
133    }
134}
135
136/// An iterator over entries in the name table.
137pub struct NameIterator<'a> {
138    file: &'a [u8],
139    entries: &'a [u8],
140}
141
142/// An entry in the name table.
143///
144/// Entries in the name table contain a pointer to the declaration of the item
145/// in the proof stream and a nul-terminated string of the name of the item.
146#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
147pub struct Name<'a> {
148    pub ptr: u64,
149    pub name: &'a [u8],
150}
151
152impl<'a> Iterator for NameIterator<'a> {
153    type Item = Name<'a>;
154
155    fn next(&mut self) -> Option<Self::Item> {
156        let (left, name) = parser::parse_name_entry(self.file, self.entries).ok()?;
157
158        self.entries = left;
159
160        Some(name)
161    }
162}
163
164impl<'a> Name<'a> {
165    pub fn to_str(&self) -> Result<&str, &[u8]> {
166        if self.name.len() == 0 {
167            Err(&[])
168        } else {
169            std::str::from_utf8(self.name).map_err(|_| self.name)
170        }
171    }
172}
mmb_parser/index/name_table.rs

mmb_parser/index/
name_table.rs
