use crate::{
cmd, cstr_from_bytes_prefix, exhausted, u32_as_usize, u64_as_usize, Arg, Header, NameEntry,
NumdStmtCmd, ProofCmd, SortData, StmtCmd, TableEntry, TermEntry, ThmEntry, UnifyCmd,
};
use byteorder::LE;
use mm0_util::{SortId, TermId, ThmId};
use std::borrow::Cow;
use std::convert::{TryFrom, TryInto};
use std::ops::Range;
use std::{io, mem, mem::size_of};
use zerocopy::{FromBytes, LayoutVerified, U16, U32, U64};
#[derive(Debug, Default)]
#[non_exhaustive]
pub struct MmbFile<'a, X = BasicIndex<'a>> {
pub header: Header,
pub buf: &'a [u8],
pub sorts: &'a [SortData],
pub terms: &'a [TermEntry],
pub thms: &'a [ThmEntry],
pub index: X,
}
pub type BasicMmbFile<'a> = MmbFile<'a, BasicIndex<'a>>;
pub type BareMmbFile<'a> = MmbFile<'a, ()>;
pub trait MmbIndexBuilder<'a>: Default {
fn build<X>(&mut self, f: &mut MmbFile<'a, X>, e: &'a TableEntry) -> Result<(), ParseError>;
}
impl<'a> MmbIndexBuilder<'a> for () {
#[inline]
fn build<X>(&mut self, _: &mut MmbFile<'a, X>, _: &'a TableEntry) -> Result<(), ParseError> {
Ok(())
}
}
impl<'a, A: MmbIndexBuilder<'a>, B: MmbIndexBuilder<'a>> MmbIndexBuilder<'a> for (A, B) {
#[inline]
fn build<X>(&mut self, f: &mut MmbFile<'a, X>, e: &'a TableEntry) -> Result<(), ParseError> {
self.0.build(f, e)?;
self.1.build(f, e)
}
}
#[macro_export]
macro_rules! make_index_trait {
([<$($lft:lifetime),*>, $ty:ident, $trait:ident, $notrait:ident, $f:ident, $f_mut:ident]
$($fns:item)*) => {
pub trait $trait<$($lft),*> {
fn $f(&self) -> Option<&$ty<$($lft),*>>;
fn $f_mut(&mut self) -> Option<&mut $ty<$($lft),*>>;
$($fns)*
}
pub trait $notrait {}
impl $notrait for () {}
impl<$($lft),*, T: $notrait> $trait<$($lft),*> for T {
#[inline]
fn $f(&self) -> Option<&$ty<$($lft),*>> { None }
#[inline]
fn $f_mut(&mut self) -> Option<&mut $ty<$($lft),*>> { None }
}
impl<$($lft),*> $trait<$($lft),*> for $ty<$($lft),*> {
#[inline]
fn $f(&self) -> Option<&$ty<$($lft),*>> { Some(self) }
#[inline]
fn $f_mut(&mut self) -> Option<&mut $ty<$($lft),*>> { Some(self) }
}
impl<$($lft),*> $trait<$($lft),*> for Option<$ty<$($lft),*>> {
#[inline]
fn $f(&self) -> Option<&$ty<$($lft),*>> { self.as_ref() }
#[inline]
fn $f_mut(&mut self) -> Option<&mut $ty<$($lft),*>> { self.as_mut() }
}
impl<$($lft),*, A: $trait<$($lft),*>, B: $trait<$($lft),*>> $trait<$($lft),*> for (A, B) {
#[inline]
fn $f(&self) -> Option<&$ty<$($lft),*>> {
match self.0.$f() {
Some(e) => Some(e),
None => self.1.$f()
}
}
#[inline]
fn $f_mut(&mut self) -> Option<&mut $ty<$($lft),*>> {
match self.0.$f_mut() {
Some(e) => Some(e),
None => self.1.$f_mut()
}
}
}
}
}
#[derive(Debug)]
pub struct SymbolNames<'a> {
sorts: &'a [NameEntry],
terms: &'a [NameEntry],
thms: &'a [NameEntry],
}
impl<'a> MmbIndexBuilder<'a> for Option<SymbolNames<'a>> {
fn build<X>(&mut self, f: &mut MmbFile<'a, X>, e: &'a TableEntry) -> Result<(), ParseError> {
if e.id == cmd::INDEX_NAME {
let rest = f.buf.get(u64_as_usize(e.ptr)..).ok_or_else(|| f.bad_index_parse())?;
let (sorts, rest) =
new_slice_prefix(rest, f.sorts.len()).ok_or_else(|| f.bad_index_parse())?;
let (terms, rest) =
new_slice_prefix(rest, f.terms.len()).ok_or_else(|| f.bad_index_parse())?;
let (thms, _) = new_slice_prefix(rest, f.thms.len()).ok_or_else(|| f.bad_index_parse())?;
if self.replace(SymbolNames { sorts, terms, thms }).is_some() {
return Err(ParseError::DuplicateIndexTable {
p_index: u64_as_usize(f.header.p_index),
id: e.id,
})
}
}
Ok(())
}
}
make_index_trait! {
[<'a>, SymbolNames, HasSymbolNames, NoSymbolNames, get_symbol_names, get_symbol_names_mut]
}
impl<'a> NoSymbolNames for Option<VarNames<'a>> {}
impl<'a> NoSymbolNames for Option<HypNames<'a>> {}
#[derive(Debug)]
pub struct VarNames<'a> {
terms: &'a [U64<LE>],
thms: &'a [U64<LE>],
}
impl<'a> MmbIndexBuilder<'a> for Option<VarNames<'a>> {
fn build<X>(&mut self, f: &mut MmbFile<'a, X>, e: &'a TableEntry) -> Result<(), ParseError> {
if e.id == cmd::INDEX_VAR_NAME {
let rest = f.buf.get(u64_as_usize(e.ptr)..).ok_or_else(|| f.bad_index_parse())?;
let (terms, rest) =
new_slice_prefix(rest, f.terms.len()).ok_or_else(|| f.bad_index_parse())?;
let (thms, _) = new_slice_prefix(rest, f.thms.len()).ok_or_else(|| f.bad_index_parse())?;
if self.replace(VarNames { terms, thms }).is_some() {
return Err(ParseError::DuplicateIndexTable {
p_index: u64_as_usize(f.header.p_index),
id: e.id,
})
}
}
Ok(())
}
}
make_index_trait! {
[<'a>, VarNames, HasVarNames, NoVarNames, get_var_names, get_var_names_mut]
}
impl<'a> NoVarNames for Option<SymbolNames<'a>> {}
impl<'a> NoVarNames for Option<HypNames<'a>> {}
#[derive(Debug)]
pub struct HypNames<'a> {
thms: &'a [U64<LE>],
}
impl<'a> MmbIndexBuilder<'a> for Option<HypNames<'a>> {
fn build<X>(&mut self, f: &mut MmbFile<'a, X>, e: &'a TableEntry) -> Result<(), ParseError> {
if e.id == cmd::INDEX_HYP_NAME {
let rest = f.buf.get(u64_as_usize(e.ptr)..).ok_or_else(|| f.bad_index_parse())?;
let (thms, _) = new_slice_prefix(rest, f.thms.len()).ok_or_else(|| f.bad_index_parse())?;
if self.replace(HypNames { thms }).is_some() {
return Err(ParseError::DuplicateIndexTable {
p_index: u64_as_usize(f.header.p_index),
id: e.id,
})
}
}
Ok(())
}
}
make_index_trait! {
[<'a>, HypNames, HasHypNames, NoHypNames, get_hyp_names, get_hyp_names_mut]
}
impl<'a> NoHypNames for Option<SymbolNames<'a>> {}
impl<'a> NoHypNames for Option<VarNames<'a>> {}
pub type BasicIndex<'a> = (Option<SymbolNames<'a>>, (Option<VarNames<'a>>, Option<HypNames<'a>>));
pub fn try_next_cmd(mmb: &[u8], start_at: usize) -> Result<Option<(u8, u32, usize)>, ParseError> {
let (cmd, data, new_start_at) = parse_cmd(mmb, start_at)?;
if cmd == 0 {
return Ok(None)
}
assert!(new_start_at > start_at);
Ok(Some((cmd, data, new_start_at)))
}
pub fn parse_cmd(mmb: &[u8], starts_at: usize) -> Result<(u8, u32, usize), ParseError> {
use super::cmd::{DATA_16, DATA_32, DATA_8, DATA_MASK};
match mmb.get(starts_at..) {
None | Some([]) => Err(exhausted!()),
Some([cmd, tl @ ..]) => {
let val = cmd & !DATA_MASK;
#[allow(clippy::unnecessary_lazy_evaluations)]
match cmd & DATA_MASK {
0 => Ok((val, 0, starts_at + size_of::<u8>())),
DATA_8 => tl
.first()
.map(|&n| (val, n.into(), starts_at + size_of::<u8>() + size_of::<u8>()))
.ok_or_else(|| exhausted!()),
DATA_16 => LayoutVerified::<_, U16<LE>>::new_from_prefix(tl)
.map(|(n, _)| (val, n.get().into(), starts_at + size_of::<u8>() + size_of::<u16>()))
.ok_or_else(|| exhausted!()),
DATA_32 => LayoutVerified::<_, U32<LE>>::new_from_prefix(tl)
.map(|(n, _)| (val, n.get(), starts_at + size_of::<u8>() + size_of::<u32>()))
.ok_or_else(|| exhausted!()),
_ => unreachable!(),
}
}
}
}
#[must_use]
#[derive(Debug, Clone)]
pub struct ProofIter<'a> {
mmb_source: &'a [u8],
pub pos: usize,
pub ends_at: usize,
}
impl<'a> ProofIter<'a> {
#[must_use]
pub fn is_null(&self) -> bool { self.pos == self.ends_at }
}
impl<'a> ProofIter<'a> {
#[must_use]
pub fn peek(&self) -> Option<Result<ProofCmd, ParseError>> { self.clone().next() }
}
impl<'a> Iterator for ProofIter<'a> {
type Item = Result<ProofCmd, ParseError>;
fn next(&mut self) -> Option<Self::Item> {
match try_next_cmd(self.mmb_source, self.pos) {
Err(e) => Some(Err(e)),
Ok(None) if self.ends_at == self.pos + 1 => None,
Ok(None) => Some(Err(exhausted!())),
Ok(Some((cmd, data, rest))) => match ProofCmd::try_from((cmd, data)) {
Err(e) => Some(Err(e)),
Ok(proof_cmd) => {
self.pos = rest;
Some(Ok(proof_cmd))
}
},
}
}
}
#[must_use]
#[derive(Debug, Clone)]
pub struct UnifyIter<'a> {
mmb_file: &'a [u8],
pub pos: usize,
}
impl<'a> UnifyIter<'a> {
#[inline]
fn new((mmb_file, pos): (&'a [u8], usize)) -> UnifyIter<'a> { Self { mmb_file, pos } }
#[must_use]
pub fn peek(&self) -> Option<Result<UnifyCmd, ParseError>> { self.clone().next() }
pub fn after_end(&self) -> Result<usize, ParseError> {
let UnifyIter { mmb_file: mmb, mut pos } = *self;
loop {
let (cmd, _, new_pos) = parse_cmd(mmb, pos)?;
if cmd == 0 {
return Ok(new_pos)
}
pos = new_pos;
}
}
pub fn as_bytes(&self) -> Result<&'a [u8], ParseError> {
Ok(&self.mmb_file[self.pos..self.after_end()?])
}
}
impl<'a> Iterator for UnifyIter<'a> {
type Item = Result<UnifyCmd, ParseError>;
fn next(&mut self) -> Option<Self::Item> {
match try_next_cmd(self.mmb_file, self.pos) {
Err(e) => Some(Err(e)),
Ok(None) => None,
Ok(Some((cmd, data, rest))) => match UnifyCmd::try_from((cmd, data)) {
Err(e) => Some(Err(e)),
Ok(unify_cmd) => {
self.pos = rest;
Some(Ok(unify_cmd))
}
},
}
}
}
#[derive(Debug, Clone, Copy)]
pub struct TermRef<'a> {
pub tid: TermId,
sort: u8,
args_and_ret: &'a [Arg],
unify: (&'a [u8], usize),
}
#[derive(Debug, Clone, Copy)]
pub struct ThmRef<'a> {
pub tid: ThmId,
args: &'a [Arg],
unify: (&'a [u8], usize),
}
#[derive(Debug)]
pub enum ParseError {
BadProofLen(usize),
StmtCmdConv(u8),
ProofCmdConv(u8, u32),
UnifyCmdConv(u8, u32),
Trace(&'static str, u32, Box<ParseError>),
Exhausted(&'static str, u32),
BadMagic {
parsed_magic: [u8; 4],
},
Unaligned,
SuspectHeader,
IncompleteHeader {
file_len: usize,
},
BadVersion {
parsed_version: u8,
},
BadSorts(Range<usize>),
BadTerms(Range<usize>),
BadThms(Range<usize>),
BadProofs(Range<usize>),
BadIndexParse {
p_index: usize,
},
DuplicateIndexTable {
p_index: usize,
id: [u8; 4],
},
BadIndexLookup {
p_index: Option<usize>,
},
SorryError,
StrError(&'static str, usize),
IoError(io::Error),
}
#[macro_export]
macro_rules! exhausted {
() => {
ParseError::Exhausted(file!(), line!())
};
}
#[macro_export]
macro_rules! trace {
($e:expr) => {
ParseError::Trace(file!(), line!(), Box::new($e))
};
}
const HEADER_CAVEAT: &str = "\
Be advised that the given position(s) may be the result of an \
untrustworthy header, and should therefore be considered \
suggestions for where to begin troubleshooting.";
impl std::fmt::Display for ParseError {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
match self {
ParseError::BadProofLen(start) =>
write!(f, "proof starting at byte {} has an incorrect length", start),
ParseError::StmtCmdConv(cmd) =>
write!(f, "bad StmtCmd conversion (`TryFrom`); cmd was {}", cmd),
ParseError::ProofCmdConv(cmd, data) =>
write!(f, "bad ProofCmd conversion (`TryFrom`). data: ({}, {})", cmd, data),
ParseError::UnifyCmdConv(cmd, data) =>
write!(f, "bad UnifyCmd conversion (`TryFrom`). data: ({}, {})", cmd, data),
ParseError::Trace(file, line, inner) => write!(f, "trace {} : {} -> {}", file, line, inner),
ParseError::Exhausted(file, line) =>
write!(f, "mmb parser was prematurely exhausted at {} : {}", file, line),
ParseError::BadSorts(range) => write!(
f,
"Failed to parse list of sorts in MMB file. \
According to the header, `sorts` should inhabit {:?}. {}",
range, HEADER_CAVEAT
),
ParseError::BadTerms(range) => write!(
f,
"Failed to parse list of terms in MMB file. \
According to the header, `terms` should inhabit {:?}. {}",
range, HEADER_CAVEAT
),
ParseError::BadThms(range) => write!(
f,
"Failed to parse list of thms in MMB file. \
According to the header, `thms` should inhabit {:?}. {}",
range, HEADER_CAVEAT
),
ParseError::BadProofs(range) => write!(
f,
"Failed to parse list of proofs in MMB file. \
According to the header, `proofs` should inhabit {:?}. {}",
range, HEADER_CAVEAT
),
ParseError::BadMagic { parsed_magic } => write!(
f,
"Bad header; unable to find MMB magic number at expected location \
(MMB magic number is {:?} ('MM0B' in bytes), found {:?})",
crate::cmd::MM0B_MAGIC,
parsed_magic
),
ParseError::Unaligned => write!(f, "The MMB file is not 8-byte aligned."),
ParseError::SuspectHeader => write!(
f,
"The MMB file's header parsed correctly, \
but the parsed header indicates an improperly constructed MMB file."
),
ParseError::IncompleteHeader { file_len } => write!(
f,
"Received an mmb file with length {} bytes. \
This is too short to contain a header, and cannot be well-formed",
file_len
),
ParseError::BadVersion { parsed_version } => write!(
f,
"MMB version mismatch: File header specifies version {}, but verifier version is {}",
parsed_version,
crate::cmd::MM0B_VERSION
),
ParseError::BadIndexParse { p_index } => write!(
f,
"MMB index is malformed. According to the header, it begins at byte {}. {}",
p_index, HEADER_CAVEAT
),
ParseError::DuplicateIndexTable { p_index, id } => {
write!(f, "MMB index at {} contains a duplicate index entry for key = ", p_index)?;
match std::str::from_utf8(id) {
Ok(s) => write!(f, "'{}'", s)?,
Err(_) => write!(f, "{:?}", id)?,
}
write!(f, ". {}", HEADER_CAVEAT)
}
ParseError::BadIndexLookup { p_index: None } => write!(
f,
"There was an error looking up an item in the MMB index, \
and the header didn't specify its location in the file"
),
ParseError::BadIndexLookup { p_index: Some(b) } => write!(
f,
"MMB index is malformed. According to the header, it begins at byte {}. {}",
b, HEADER_CAVEAT
),
ParseError::SorryError => write!(f, "Proof uses 'sorry'."),
ParseError::StrError(s, _) => write!(f, "{}", s),
ParseError::IoError(e) => write!(f, "{}", e),
}
}
}
impl From<io::Error> for ParseError {
fn from(e: io::Error) -> Self { Self::IoError(e) }
}
#[inline]
fn new_slice_prefix<T: FromBytes>(bytes: &[u8], n: usize) -> Option<(&[T], &[u8])> {
let mid = mem::size_of::<T>().checked_mul(n)?;
if mid <= bytes.len() {
let (left, right) = bytes.split_at(mid);
Some((LayoutVerified::new_slice(left)?.into_slice(), right))
} else {
None
}
}
impl<'a, X> MmbFile<'a, X> {
#[must_use]
pub fn bad_index_lookup(&self) -> ParseError {
ParseError::BadIndexLookup { p_index: self.p_index() }
}
#[must_use]
pub fn p_index(&self) -> Option<usize> {
let n = u64_as_usize(self.header.p_index);
if n == 0 {
None
} else {
Some(n)
}
}
pub fn bad_index_parse(&self) -> ParseError {
ParseError::BadIndexParse { p_index: u64_as_usize(self.header.p_index) }
}
}
impl<'a, X: MmbIndexBuilder<'a>> MmbFile<'a, X> {
pub fn parse(buf: &'a [u8]) -> Result<Self, ParseError> {
use ParseError::{BadIndexParse, BadSorts, BadTerms, BadThms};
let (zc_header, sorts) =
LayoutVerified::<_, Header>::new_from_prefix(buf).ok_or_else(|| find_header_error(buf))?;
let p_sorts = zc_header.bytes().len();
let header = zc_header.into_ref();
header.check(buf)?;
let sorts = sorts
.get(..header.num_sorts.into())
.and_then(LayoutVerified::new_slice_unaligned)
.ok_or_else(|| BadSorts(p_sorts..u32_as_usize(header.p_terms.get())))?
.into_slice();
let terms = buf
.get(u32_as_usize(header.p_terms.get())..)
.and_then(|s| new_slice_prefix(s, u32_as_usize(header.num_terms.get())))
.ok_or_else(|| {
BadTerms(u32_as_usize(header.p_terms.get())..u32_as_usize(header.p_thms.get()))
})?
.0;
let thms = buf
.get(u32_as_usize(header.p_thms.get())..)
.and_then(|s| new_slice_prefix(s, u32_as_usize(header.num_thms.get())))
.ok_or_else(|| {
BadThms(u32_as_usize(header.p_thms.get())..u32_as_usize(header.p_proof.get()))
})?
.0;
let mut file = MmbFile { header: *header, buf, sorts, terms, thms, index: X::default() };
let n = u64_as_usize(header.p_index);
if n != 0 {
let (entries, _) = (|| -> Option<_> {
let (num_entries, rest) =
LayoutVerified::<_, U64<LE>>::new_unaligned_from_prefix(&*buf.get(n..)?)?;
new_slice_prefix(rest, num_entries.get().try_into().ok()?)
})()
.ok_or_else(|| BadIndexParse { p_index: u64_as_usize(header.p_index) })?;
let mut index = X::default();
for e in entries {
index.build(&mut file, e)?
}
file.index = index;
}
Ok(file)
}
}
macro_rules! bin_parser {
($(($name: ident, $t:ident))*) => {
$(
fn $name((mmb_file, pos): (&[u8], usize)) -> Result<($t, usize), ParseError> {
let int_bytes = mmb_file
.get(pos..(pos + size_of::<$t>()))
.ok_or_else(|| ParseError::IncompleteHeader { file_len: mmb_file.len() })?;
if int_bytes.len() != size_of::<$t>() {
return Err(ParseError::IncompleteHeader { file_len: mmb_file.len()})
}
Ok(($t::from_le_bytes(int_bytes.try_into().unwrap()), pos + size_of::<$t>()))
}
)*
};
}
bin_parser! {
(parse_u8, u8)
(parse_u16, u16)
(parse_u32, u32)
(parse_u64, u64)
}
#[must_use]
pub fn find_header_error(mmb: &[u8]) -> ParseError {
fn find_header_error_aux(mmb: &[u8]) -> Result<(), ParseError> {
if <*const [u8]>::cast::<u8>(mmb).align_offset(8) != 0 {
return Err(ParseError::Unaligned)
}
let (magic0, pos) = parse_u8((mmb, 0))?;
let (magic1, pos) = parse_u8((mmb, pos))?;
let (magic2, pos) = parse_u8((mmb, pos))?;
let (magic3, pos) = parse_u8((mmb, pos))?;
let magic = [magic0, magic1, magic2, magic3];
if magic != crate::cmd::MM0B_MAGIC {
return Err(ParseError::BadMagic { parsed_magic: magic })
}
let (version, pos) = parse_u8((mmb, pos))?;
if version != crate::cmd::MM0B_VERSION {
return Err(ParseError::BadVersion { parsed_version: version })
}
let (_num_sorts, pos) = parse_u8((mmb, pos))?;
let (_reserved, pos) = parse_u16((mmb, pos))?;
let (_num_terms, pos) = parse_u32((mmb, pos))?;
let (_num_thms, pos) = parse_u32((mmb, pos))?;
let (_terms_start, pos) = parse_u32((mmb, pos))?;
let (_thms_start, pos) = parse_u32((mmb, pos))?;
let (_proof_stream_start, pos) = parse_u32((mmb, pos))?;
let (_reserved2, pos) = parse_u32((mmb, pos))?;
let (_index_start, _) = parse_u64((mmb, pos))?;
Ok(())
}
match find_header_error_aux(mmb) {
Err(e) => e,
Ok(_) => panic!(
"zerocopy errored out when parsing mmb header, \
but `inspect_header_aux` wasn't able to find a problem"
),
}
}
#[inline]
fn term_ref(buf: &[u8], t: TermEntry, tid: TermId) -> Option<TermRef<'_>> {
let (args_and_ret, unify) =
new_slice_prefix(buf.get(u32_as_usize(t.p_args.get())..)?, usize::from(t.num_args.get()) + 1)?;
let unify = (buf, buf.len() - unify.len());
Some(TermRef { tid, sort: t.sort, args_and_ret, unify })
}
#[inline]
fn thm_ref(buf: &[u8], t: ThmEntry, tid: ThmId) -> Option<ThmRef<'_>> {
let (args, unify) =
new_slice_prefix(buf.get(u32_as_usize(t.p_args.get())..)?, t.num_args.get().into())?;
let unify = (buf, buf.len() - unify.len());
Some(ThmRef { tid, args, unify })
}
impl<'a, X> MmbFile<'a, X> {
#[inline]
#[must_use]
pub fn sort(&self, n: SortId) -> Option<SortData> { self.sorts.get(usize::from(n.0)).copied() }
#[inline]
#[must_use]
pub fn term(&self, n: TermId) -> Option<TermRef<'a>> {
term_ref(self.buf, *self.terms.get(u32_as_usize(n.0))?, n)
}
#[inline]
#[must_use]
pub fn thm(&self, n: ThmId) -> Option<ThmRef<'a>> {
thm_ref(self.buf, *self.thms.get(u32_as_usize(n.0))?, n)
}
#[inline]
pub fn proof(&self) -> DeclIter<'a> {
DeclIter {
mmb_file: self.buf,
pos: u32_as_usize(self.header.p_proof.get()),
next_sort_id: 0_u8,
next_term_id: 0_u32,
next_thm_id: 0_u32,
}
}
}
#[derive(Debug, Clone, Copy)]
#[non_exhaustive]
pub struct NameEntryRef<'a> {
pub buf: &'a [u8],
pub p_proof: U64<LE>,
pub value: &'a [u8],
}
#[inline]
fn name_entry_ref(
buf: &[u8], NameEntry { p_proof, p_name }: NameEntry,
) -> Option<NameEntryRef<'_>> {
let value = buf.get(u64_as_usize(p_name)..)?;
Some(NameEntryRef { buf, p_proof, value })
}
impl<'a, X: HasSymbolNames<'a>> MmbFile<'a, X> {
#[must_use]
pub fn sort_index(&self, n: SortId) -> Option<NameEntryRef<'a>> {
name_entry_ref(self.buf, *self.index.get_symbol_names()?.sorts.get(usize::from(n.0))?)
}
#[must_use]
pub fn term_index(&self, n: TermId) -> Option<NameEntryRef<'a>> {
name_entry_ref(self.buf, *self.index.get_symbol_names()?.terms.get(u32_as_usize(n.0))?)
}
#[must_use]
pub fn thm_index(&self, n: ThmId) -> Option<NameEntryRef<'a>> {
name_entry_ref(self.buf, *self.index.get_symbol_names()?.thms.get(u32_as_usize(n.0))?)
}
#[must_use]
pub fn stmt_index(&self, stmt: NumdStmtCmd) -> Option<NameEntryRef<'a>> {
use crate::NumdStmtCmd::{Axiom, Sort, TermDef, Thm};
match stmt {
Sort { sort_id } => self.sort_index(sort_id),
Axiom { thm_id } | Thm { thm_id, .. } => self.thm_index(thm_id),
TermDef { term_id, .. } => self.term_index(term_id),
}
}
#[must_use]
pub fn try_sort_name(&self, n: SortId) -> Option<&'a str> {
self.sort_index(n).and_then(|t| t.value())
}
#[must_use]
pub fn try_term_name(&self, n: TermId) -> Option<&'a str> {
self.term_index(n).and_then(|t| t.value())
}
#[must_use]
pub fn try_thm_name(&self, n: ThmId) -> Option<&'a str> {
self.thm_index(n).and_then(|t| t.value())
}
#[must_use]
pub fn sort_name(&self, n: SortId) -> Cow<'a, str> {
match self.try_sort_name(n) {
Some(v) => Cow::Borrowed(v),
None => Cow::Owned(format!("s{}", n.0)),
}
}
#[must_use]
pub fn term_name(&self, n: TermId) -> Cow<'a, str> {
match self.try_term_name(n) {
Some(v) => Cow::Borrowed(v),
None => Cow::Owned(format!("t{}", n.0)),
}
}
#[must_use]
pub fn thm_name(&self, n: ThmId) -> Cow<'a, str> {
match self.try_thm_name(n) {
Some(v) => Cow::Borrowed(v),
None => Cow::Owned(format!("T{}", n.0)),
}
}
}
#[derive(Debug, Clone, Copy)]
struct StrListRef<'a> {
buf: &'a [u8],
strs: &'a [U64<LE>],
}
impl<'a> StrListRef<'a> {
fn new(buf: &'a [u8]) -> Self { Self { buf, strs: &[] } }
fn get(&self, n: usize) -> Option<&'a str> {
cstr_from_bytes_prefix(self.buf.get(u64_as_usize(*self.strs.get(n)?)..)?)?.0.to_str().ok()
}
}
macro_rules! str_list_wrapper {
($($(#[$m:meta])* $ty:ident($e:expr);)*) => {$(
$(#[$m])*
#[derive(Debug, Clone, Copy)]
pub struct $ty<'a>(StrListRef<'a>);
impl<'a> std::ops::Deref for $ty<'a> {
type Target = &'a [U64<LE>];
fn deref(&self) -> &&'a [U64<LE>] { &self.0.strs }
}
impl<'a> $ty<'a> {
fn new(buf: &'a [u8]) -> Self { Self(StrListRef::new(buf)) }
#[must_use]
pub fn get_opt(&self, n: usize) -> Option<&'a str> { self.0.get(n) }
#[must_use]
pub fn get(&self, n: usize) -> Cow<'a, str> {
match self.get_opt(n) {
Some(v) => Cow::Borrowed(v),
None => Cow::Owned(format!($e, n))
}
}
}
)*}
}
str_list_wrapper! {
VarListRef("v{}");
HypListRef("h{}");
}
impl<'a, X> MmbFile<'a, X> {
fn str_list_ref(&self, p_vars: U64<LE>) -> Option<StrListRef<'a>> {
let (num_vars, rest) = LayoutVerified::<_, U64<LE>>::new_unaligned_from_prefix(
&*self.buf.get(u64_as_usize(p_vars)..)?,
)?;
Some(StrListRef {
buf: self.buf,
strs: new_slice_prefix(rest, num_vars.get().try_into().ok()?)?.0,
})
}
}
impl<'a, X: HasVarNames<'a>> MmbFile<'a, X> {
#[must_use]
pub fn term_vars_opt(&self, n: TermId) -> Option<VarListRef<'a>> {
let strs = self.str_list_ref(*self.index.get_var_names()?.terms.get(u32_as_usize(n.0))?)?;
Some(VarListRef(strs))
}
#[must_use]
pub fn term_vars(&self, n: TermId) -> VarListRef<'a> {
self.term_vars_opt(n).unwrap_or_else(|| VarListRef::new(self.buf))
}
#[must_use]
pub fn thm_vars_opt(&self, n: ThmId) -> Option<VarListRef<'a>> {
let strs = self.str_list_ref(*self.index.get_var_names()?.thms.get(u32_as_usize(n.0))?)?;
Some(VarListRef(strs))
}
#[must_use]
pub fn thm_vars(&self, n: ThmId) -> VarListRef<'a> {
self.thm_vars_opt(n).unwrap_or_else(|| VarListRef::new(self.buf))
}
#[must_use]
pub fn stmt_vars(&self, stmt: NumdStmtCmd) -> VarListRef<'a> {
use crate::NumdStmtCmd::{Axiom, Sort, TermDef, Thm};
match stmt {
Sort { .. } => VarListRef::new(self.buf),
Axiom { thm_id } | Thm { thm_id, .. } => self.thm_vars(thm_id),
TermDef { term_id, .. } => self.term_vars(term_id),
}
}
}
#[derive(Debug, Clone, Copy)]
pub struct HypsEntryRef<'a> {
buf: &'a [u8],
pub vars: &'a [U64<LE>],
}
impl<'a, X: HasHypNames<'a>> MmbFile<'a, X> {
#[must_use]
pub fn thm_hyps_opt(&self, n: ThmId) -> Option<HypListRef<'a>> {
let strs = self.str_list_ref(*self.index.get_hyp_names()?.thms.get(u32_as_usize(n.0))?)?;
Some(HypListRef(strs))
}
#[must_use]
pub fn thm_hyps(&self, n: ThmId) -> HypListRef<'a> {
self.thm_hyps_opt(n).unwrap_or_else(|| HypListRef::new(self.buf))
}
#[must_use]
pub fn stmt_hyps(&self, stmt: NumdStmtCmd) -> HypListRef<'a> {
use crate::NumdStmtCmd::{Axiom, Sort, TermDef, Thm};
match stmt {
Sort { .. } | TermDef { .. } => HypListRef::new(self.buf),
Axiom { thm_id } | Thm { thm_id, .. } => self.thm_hyps(thm_id),
}
}
}
impl<'a> TermRef<'a> {
#[inline]
#[must_use]
pub fn def(&self) -> bool { self.sort & 0x80 != 0 }
#[inline]
#[must_use]
pub fn sort(&self) -> SortId { SortId(self.sort & 0x7F) }
#[inline]
#[must_use]
pub fn args(&self) -> &[Arg] { self.args_and_ret.split_last().expect("nonempty").1 }
#[inline]
#[must_use]
pub fn args_and_ret(&self) -> &[Arg] { self.args_and_ret }
#[inline]
#[must_use]
pub fn ret(&self) -> Arg { *self.args_and_ret.last().expect("nonempty") }
#[inline]
pub fn unify(&self) -> UnifyIter<'a> { UnifyIter::new(self.unify) }
}
impl<'a> ThmRef<'a> {
#[inline]
#[must_use]
pub fn args(&self) -> &[Arg] { self.args }
#[inline]
pub fn unify(&self) -> UnifyIter<'a> { UnifyIter::new(self.unify) }
}
fn try_next_decl(mmb: &[u8], pos: usize) -> Result<Option<(StmtCmd, ProofIter<'_>)>, ParseError> {
let (stmt_cmd, proof_len, proof_starts_at) = match try_next_cmd(mmb, pos)? {
None => return Ok(None),
Some((cmd, data, rest)) => (cmd, data, rest),
};
let proof_ends_at = pos + proof_len as usize;
if proof_ends_at < proof_starts_at {
return Err(ParseError::BadProofLen(pos))
}
let pr = ProofIter { mmb_source: mmb, pos: proof_starts_at, ends_at: proof_ends_at };
Ok(Some((StmtCmd::try_from(stmt_cmd)?, pr)))
}
#[must_use]
#[derive(Debug, Clone)]
pub struct DeclIter<'a> {
mmb_file: &'a [u8],
pub pos: usize,
next_sort_id: u8,
next_term_id: u32,
next_thm_id: u32,
}
impl<'a> DeclIter<'a> {
#[must_use]
pub fn peek(&self) -> Option<Result<(NumdStmtCmd, ProofIter<'a>), ParseError>> {
self.clone().next()
}
pub fn after_end(&self) -> Result<usize, ParseError> {
let mut pos = self.pos;
loop {
let (cmd, stmt_len, next_cmd) = parse_cmd(self.mmb_file, pos)?;
if cmd == 0 {
return Ok(next_cmd)
}
let new_pos = pos + (stmt_len as usize);
if new_pos < next_cmd {
return Err(ParseError::BadProofLen(pos))
}
pos = new_pos;
}
}
}
impl<'a> Iterator for DeclIter<'a> {
type Item = Result<(NumdStmtCmd, ProofIter<'a>), ParseError>;
fn next(&mut self) -> Option<Self::Item> {
match try_next_decl(self.mmb_file, self.pos) {
Err(e) => Some(Err(e)),
Ok(None) => None,
Ok(Some((stmt, proof_iter))) => {
self.pos = proof_iter.ends_at;
let cmd = match stmt {
StmtCmd::Sort => {
let out = NumdStmtCmd::Sort { sort_id: SortId(self.next_sort_id) };
self.next_sort_id += 1;
out
}
StmtCmd::Axiom => {
let out = NumdStmtCmd::Axiom { thm_id: ThmId(self.next_thm_id) };
self.next_thm_id += 1;
out
}
StmtCmd::TermDef { local } => {
let out = NumdStmtCmd::TermDef { term_id: TermId(self.next_term_id), local };
self.next_term_id += 1;
out
}
StmtCmd::Thm { local } => {
let out = NumdStmtCmd::Thm { thm_id: ThmId(self.next_thm_id), local };
self.next_thm_id += 1;
out
}
};
Some(Ok((cmd, proof_iter)))
}
}
}
}
impl<'a> NameEntryRef<'a> {
#[must_use]
pub fn value(&self) -> Option<&'a str> { cstr_from_bytes_prefix(self.value)?.0.to_str().ok() }
pub fn decl(&self) -> Result<Option<(StmtCmd, ProofIter<'a>)>, ParseError> {
try_next_decl(self.buf, u64_as_usize(self.p_proof))
}
}