#![warn(
bare_trait_objects,
elided_lifetimes_in_paths,
missing_copy_implementations,
missing_debug_implementations,
future_incompatible,
rust_2018_idioms,
trivial_numeric_casts,
variant_size_differences,
unreachable_pub,
unused,
missing_docs
)]
#![warn(clippy::all, clippy::pedantic, clippy::nursery, clippy::cargo)]
#![warn(
clippy::else_if_without_else,
clippy::float_arithmetic,
clippy::get_unwrap,
clippy::inline_asm_x86_att_syntax,
clippy::integer_division,
clippy::rc_buffer,
clippy::rest_pat_in_fully_bound_structs,
clippy::string_add,
clippy::unwrap_used
)]
#![allow(
clippy::cognitive_complexity,
clippy::comparison_chain,
clippy::default_trait_access,
clippy::inline_always,
clippy::manual_filter_map,
clippy::map_err_ignore,
clippy::missing_const_for_fn,
clippy::missing_errors_doc,
clippy::missing_panics_doc,
clippy::module_name_repetitions,
clippy::multiple_crate_versions,
clippy::option_if_let_else,
clippy::semicolon_if_nothing_returned,
clippy::shadow_unrelated,
clippy::too_many_lines,
clippy::use_self
)]
mod parser;
mod ty;
mod write;
use std::convert::{TryFrom, TryInto};
use std::ffi::CStr;
use std::mem::size_of;
use byteorder::LE;
use mm0_util::{Modifiers, SortId, TermId, ThmId};
use zerocopy::{AsBytes, FromBytes, Unaligned, U16, U32, U64};
pub use mm0_util::u32_as_usize;
pub use {parser::*, ty::*, write::*};
pub const MAX_BOUND_VARS: usize = 55;
pub mod cmd {
pub const MM0B_MAGIC: [u8; 4] = *b"MM0B";
pub const MM0B_VERSION: u8 = 1;
pub const DATA_8: u8 = 0x40;
pub const DATA_16: u8 = 0x80;
pub const DATA_32: u8 = 0xC0;
pub const DATA_MASK: u8 = 0xC0;
pub const STMT_AXIOM: u8 = 0x02;
pub const STMT_SORT: u8 = 0x04;
pub const STMT_TERM: u8 = 0x05;
pub const STMT_DEF: u8 = 0x05;
pub const STMT_THM: u8 = 0x06;
pub const STMT_LOCAL: u8 = 0x08;
pub const STMT_LOCAL_DEF: u8 = STMT_LOCAL | STMT_DEF;
pub const STMT_LOCAL_THM: u8 = STMT_LOCAL | STMT_THM;
pub const PROOF_TERM: u8 = 0x10;
pub const PROOF_TERM_SAVE: u8 = 0x11;
pub const PROOF_REF: u8 = 0x12;
pub const PROOF_DUMMY: u8 = 0x13;
pub const PROOF_THM: u8 = 0x14;
pub const PROOF_THM_SAVE: u8 = 0x15;
pub const PROOF_HYP: u8 = 0x16;
pub const PROOF_CONV: u8 = 0x17;
pub const PROOF_REFL: u8 = 0x18;
pub const PROOF_SYMM: u8 = 0x19;
pub const PROOF_CONG: u8 = 0x1A;
pub const PROOF_UNFOLD: u8 = 0x1B;
pub const PROOF_CONV_CUT: u8 = 0x1C;
pub const PROOF_CONV_SAVE: u8 = 0x1E;
pub const PROOF_SAVE: u8 = 0x1F;
pub const PROOF_SORRY: u8 = 0x20;
pub const UNIFY_TERM: u8 = 0x30;
pub const UNIFY_TERM_SAVE: u8 = 0x31;
pub const UNIFY_REF: u8 = 0x32;
pub const UNIFY_DUMMY: u8 = 0x33;
pub const UNIFY_HYP: u8 = 0x36;
pub const INDEX_NAME: [u8; 4] = *b"Name";
pub const INDEX_VAR_NAME: [u8; 4] = *b"VarN";
pub const INDEX_HYP_NAME: [u8; 4] = *b"HypN";
}
#[inline]
fn u64_as_usize(n: U64<LE>) -> usize {
n.get().try_into().expect("here's a nickel, get a better computer")
}
#[must_use]
pub fn cstr_from_bytes_prefix(bytes: &[u8]) -> Option<(&CStr, &[u8])> {
let mid = memchr::memchr(0, bytes)? + 1;
unsafe {
Some((
CStr::from_bytes_with_nul_unchecked(bytes.get_unchecked(..mid)),
bytes.get_unchecked(..mid),
))
}
}
#[derive(Debug, Clone, Copy)]
pub enum StmtCmd {
Sort,
Axiom,
TermDef {
local: bool,
},
Thm {
local: bool,
},
}
#[derive(Debug, Clone, Copy)]
pub enum NumdStmtCmd {
Sort {
sort_id: SortId,
},
Axiom {
thm_id: ThmId,
},
TermDef {
term_id: TermId,
local: bool,
},
Thm {
thm_id: ThmId,
local: bool,
},
}
impl StmtCmd {
#[must_use]
pub fn is_local(self) -> bool {
match self {
Self::Sort | Self::Axiom => false,
Self::TermDef { local } | Self::Thm { local } => local,
}
}
}
impl NumdStmtCmd {
#[must_use]
pub fn is_local(self) -> bool {
match self {
Self::Sort { .. } | Self::Axiom { .. } => false,
Self::TermDef { local, .. } | Self::Thm { local, .. } => local,
}
}
}
impl std::convert::TryFrom<u8> for StmtCmd {
type Error = ParseError;
fn try_from(cmd: u8) -> Result<Self, Self::Error> {
Ok(match cmd {
cmd::STMT_SORT => StmtCmd::Sort,
cmd::STMT_AXIOM => StmtCmd::Axiom,
cmd::STMT_DEF => StmtCmd::TermDef { local: false },
cmd::STMT_LOCAL_DEF => StmtCmd::TermDef { local: true },
cmd::STMT_THM => StmtCmd::Thm { local: false },
cmd::STMT_LOCAL_THM => StmtCmd::Thm { local: true },
_ => return Err(ParseError::StmtCmdConv(cmd)),
})
}
}
#[derive(Debug, Clone, Copy)]
pub enum ProofCmd {
Term {
tid: TermId,
save: bool,
},
Ref(u32),
Dummy(SortId),
Thm {
tid: ThmId,
save: bool,
},
Hyp,
Conv,
Refl,
Sym,
Cong,
Unfold,
ConvCut,
ConvSave,
Save,
Sorry,
}
impl std::convert::TryFrom<(u8, u32)> for ProofCmd {
type Error = ParseError;
fn try_from((cmd, data): (u8, u32)) -> Result<Self, Self::Error> {
Ok(match cmd {
cmd::PROOF_TERM => ProofCmd::Term { tid: TermId(data), save: false },
cmd::PROOF_TERM_SAVE => ProofCmd::Term { tid: TermId(data), save: true },
cmd::PROOF_REF => ProofCmd::Ref(data),
cmd::PROOF_DUMMY =>
ProofCmd::Dummy(SortId(data.try_into().map_err(|_| ParseError::ProofCmdConv(cmd, data))?)),
cmd::PROOF_THM => ProofCmd::Thm { tid: ThmId(data), save: false },
cmd::PROOF_THM_SAVE => ProofCmd::Thm { tid: ThmId(data), save: true },
cmd::PROOF_HYP => ProofCmd::Hyp,
cmd::PROOF_CONV => ProofCmd::Conv,
cmd::PROOF_REFL => ProofCmd::Refl,
cmd::PROOF_SYMM => ProofCmd::Sym,
cmd::PROOF_CONG => ProofCmd::Cong,
cmd::PROOF_UNFOLD => ProofCmd::Unfold,
cmd::PROOF_CONV_CUT => ProofCmd::ConvCut,
cmd::PROOF_CONV_SAVE => ProofCmd::ConvSave,
cmd::PROOF_SAVE => ProofCmd::Save,
cmd::PROOF_SORRY => ProofCmd::Sorry,
_ => return Err(ParseError::ProofCmdConv(cmd, data)),
})
}
}
#[derive(Debug, Clone, Copy)]
pub enum UnifyCmd {
Term {
tid: TermId,
save: bool,
},
Ref(u32),
Dummy(SortId),
Hyp,
}
impl std::convert::TryFrom<(u8, u32)> for UnifyCmd {
type Error = ParseError;
fn try_from((cmd, data): (u8, u32)) -> Result<Self, Self::Error> {
Ok(match cmd {
cmd::UNIFY_TERM => UnifyCmd::Term { tid: TermId(data), save: false },
cmd::UNIFY_TERM_SAVE => UnifyCmd::Term { tid: TermId(data), save: true },
cmd::UNIFY_REF => UnifyCmd::Ref(data),
cmd::UNIFY_DUMMY =>
UnifyCmd::Dummy(SortId(data.try_into().map_err(|_| ParseError::UnifyCmdConv(cmd, data))?)),
cmd::UNIFY_HYP => UnifyCmd::Hyp,
_ => return Err(ParseError::UnifyCmdConv(cmd, data)),
})
}
}
#[repr(C, align(8))]
#[derive(Debug, Clone, Copy, Default, FromBytes, AsBytes)]
pub struct Header {
pub magic: [u8; 4],
pub version: u8,
pub num_sorts: u8,
pub reserved: [u8; 2],
pub num_terms: U32<LE>,
pub num_thms: U32<LE>,
pub p_terms: U32<LE>,
pub p_thms: U32<LE>,
pub p_proof: U32<LE>,
pub reserved2: [u8; 4],
pub p_index: U64<LE>,
}
impl Header {
pub fn check(&self, mmb: &[u8]) -> Result<(), ParseError> {
use crate::cmd::{MM0B_MAGIC, MM0B_VERSION};
if self.magic != MM0B_MAGIC {
return Err(ParseError::BadMagic { parsed_magic: self.magic })
}
if self.version != MM0B_VERSION {
return Err(ParseError::BadVersion { parsed_version: self.version })
}
let p_terms = u32_as_usize(self.p_terms.get());
let p_thms = u32_as_usize(self.p_thms.get());
let p_proof = u32_as_usize(self.p_proof.get());
let p_index = u64_as_usize(self.p_index);
let headerspace = size_of::<Header>();
let sortspace = self.num_sorts as usize;
let termspace = size_of::<u32>() * u32_as_usize(self.num_terms.get());
let thmspace = size_of::<u32>() * u32_as_usize(self.num_thms.get());
if headerspace + sortspace <= p_terms
&& p_terms + termspace <= p_thms
&& p_thms + thmspace <= p_proof
&& p_proof <= mmb.len()
&& (p_index == 0 || p_proof < p_index && p_index <= mmb.len())
{
Ok(())
} else {
Err(ParseError::SuspectHeader)
}
}
}
#[repr(C)]
#[derive(Debug, Clone, Copy, FromBytes, AsBytes, Unaligned)]
pub struct SortData(pub u8);
impl TryFrom<SortData> for Modifiers {
type Error = ();
#[inline]
fn try_from(s: SortData) -> Result<Modifiers, ()> {
let m = Modifiers::new(s.0);
if Modifiers::sort_data().contains(m) {
Ok(m)
} else {
Err(())
}
}
}
#[repr(C, align(8))]
#[derive(Debug, Clone, Copy, FromBytes, AsBytes)]
pub struct TermEntry {
pub num_args: U16<LE>,
pub sort: u8,
pub reserved: u8,
pub p_args: U32<LE>,
}
#[repr(C, align(8))]
#[derive(Debug, Clone, Copy, FromBytes, AsBytes)]
pub struct ThmEntry {
pub num_args: U16<LE>,
pub reserved: [u8; 2],
pub p_args: U32<LE>,
}
#[repr(C, align(8))]
#[derive(Debug, Clone, Copy, FromBytes, AsBytes)]
pub struct TableEntry {
pub id: [u8; 4],
pub data: U32<LE>,
pub ptr: U64<LE>,
}
#[repr(C, align(8))]
#[derive(Debug, Clone, Copy, FromBytes, AsBytes)]
pub struct NameEntry {
pub p_proof: U64<LE>,
pub p_name: U64<LE>,
}