delimiter $ ( [ { ~ $
          $ } ] ) , $;
--| Well formed formulas, or propositions - true or false.
strict provable sort wff;
--| Implication: if p, then q.
term im (p q: wff): wff; infixr im: $->$ prec 25;
--| Negation: p is false.
term not (p: wff): wff; prefix not: $~$ prec 41;
--| Axiom 1 of Lukasiewicz' axioms for classical propositional logic.
axiom ax_1 (a b: wff): $ a -> b -> a $;
--| Axiom 2 of Lukasiewicz' axioms for classical propositional logic.
axiom ax_2 (a b c: wff): $ (a -> b -> c) -> (a -> b) -> a -> c $;
--| Axiom 3 of Lukasiewicz' axioms for classical propositional logic.
axiom ax_3 (a b: wff): $ (~a -> ~b) -> b -> a $;
--| Modus ponens: from `a -> b` and `a`, infer `b`.
axiom ax_mp (a b: wff): $ a -> b $ > $ a $ > $ b $;

delimiter $ ( ) ~ { } , $;
--| Well formed formulas, or propositions - true or false.
strict provable sort wff;
--| Implication: if p, then q.
term im (p q: wff): wff; infixr im: $->$ prec 25;
--| Negation: p is false.
term not (p: wff): wff; prefix not: $~$ prec 41;
--| Axiom 1 of Lukasiewicz' axioms for classical propositional logic.
axiom ax_1 (a b: wff): $ a -> b -> a $;
--| Axiom 2 of Lukasiewicz' axioms for classical propositional logic.
axiom ax_2 (a b c: wff): $ (a -> b -> c) -> (a -> b) -> a -> c $;
--| Axiom 3 of Lukasiewicz' axioms for classical propositional logic.
axiom ax_3 (a b: wff): $ (~a -> ~b) -> b -> a $;
--| Modus ponens: from `a -> b` and `a`, infer `b`.
axiom ax_mp (a b: wff): $ a -> b $ > $ a $ > $ b $;

use std::convert::{ TryFrom, TryInto };
use std::marker::PhantomData;

use crate::mmb::unify::UnifyIter;
use crate::mmb::proof::ProofIter;
use crate::mmb::stmt::StmtCmd;
/// 10000000_11111111_11111111_11111111_11111111_11111111_11111111_11111111
const TYPE_SORT_MASK: u64 = (1 << 63) | ((1 << 56) - 1);

use mm0b_parser::NumdStmtCmd;
use mm0b_parser::ProofIter;
use mm0b_parser::ParseError;

macro_rules! io_err {

macro_rules! none_err {

        $e.map_err(|e| VerifErr::IoErr(file!(), line!(), Box::new(e)))

        $e.ok_or(VerifErr::NoneErr(file!(), line!()))

macro_rules! none_err {

macro_rules! conv_err {

        $e.ok_or(VerifErr::NoneErr(file!(), line!()))

        $e.map_err(|_| VerifErr::ConvErr(file!(), line!()))

macro_rules! conv_err {
    ( $e:expr ) => {
        $e.map_err(|_| VerifErr::ConvErr(file!(), line!()))

macro_rules! io_err {
    ( $r:expr ) => {
        $r.map_err(|e| VerifErr::IoErr(file!(), line!(), e))

macro_rules! bin_parser {
    ( $(($name: ident, $t:ident))* ) => {
        $(
            pub fn $name(source: &[u8]) -> Res<($t, &[u8])> {
                let int_bytes =
                    source
                    .get(0..std::mem::size_of::<$t>())
                    .ok_or_else(|| {
                        VerifErr::Msg(format!("binary parser ran out of input @ {}: {}", file!(), line!()))
                    })?;
                let new_pos = std::mem::size_of::<$t>();
                Ok(
                    ($t::from_le_bytes(int_bytes.try_into().unwrap()), &source[new_pos..])
                )
            }
        )*
    };
}
bin_parser! {
    (parse_u8,  u8)
    (parse_u16, u16)
    (parse_u32, u32)
    (parse_u64, u64)
}
macro_rules! bitwise_inner {
    ( $($t:ident),* ) => {
        $(
            impl std::ops::BitAnd<$t> for $t {
                type Output = Self;
                fn bitand(self, rhs: Self) -> Self::Output {
                    $t { inner: self.inner & rhs.inner }
                }
            }
            impl std::ops::BitAndAssign<$t> for $t {
                fn bitand_assign(&mut self, other: Self) {
                    self.inner &= other.inner
                }
            }
            impl std::ops::BitOr<$t> for $t {
                type Output = Self;
                fn bitor(self, rhs: Self) -> Self::Output {
                    $t { inner: self.inner | rhs.inner }
                }
            }
            impl std::ops::BitOrAssign<$t> for $t {
                fn bitor_assign(&mut self, other: Self) {
                    self.inner |= other.inner
                }
            }
            impl std::ops::Not for $t {
                type Output = $t;
                fn not(self) -> Self::Output {
                    $t { inner: !self.inner }
                }
            }
        )*
    }
}
bitwise_inner!(Type, Mods);

pub type SortNum = u8;
pub type TermNum = u32;
pub type AssertNum = u32;

#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub struct Ptr<'a, A>(pub u32, pub PhantomData<&'a A>);

}
pub type Arg = Type;
#[derive(Clone, Copy, PartialEq, Eq, Hash)]
pub struct Type {
    pub inner: u64
}
impl std::default::Default for Type {
    fn default() -> Self {
        Type { inner: 0 }
    }
}
impl Type {
    pub fn high_bit(self) -> Self {
        Type { inner: self.inner & (!crate::mmb::TYPE_DEPS_MASK) }
    }
    pub fn disjoint(self, other: Self) -> bool {
        (self.inner & other.inner) == 0
    }
    pub fn new_bound() -> Self {
        Type { inner: 1 << 63 }
    }
    
    pub fn new(bound: bool) -> Self {
        if bound {
            Type { inner: 1 << 63 }
        } else {
            Type { inner: 0 }
        }
    }
    pub fn new_with_sort(sort_num: u8) -> Self {
        Type { inner: (sort_num as u64) << 56 }
    }
    #[inline]
    pub fn is_bound(self) -> bool {
        self.inner & (1 << 63) != 0
    }
    
    pub fn add_sort(&mut self, sort_id: u8) {
        // clear existing sort if any;
        self.inner &= TYPE_SORT_MASK;
        // Add new sort
        self.inner |= ((sort_id as u64) << 56);
    }
    /// Add a dependency on bv_idx
    pub fn add_dep(&mut self, bv_idx: u64) {
        self.inner |= 1 << bv_idx.checked_sub(1).expect("No 0th bv to depend on")
    }
    pub fn sort(self) -> u8 {
        u8::try_from((self.inner >> 56) & 0x7F).unwrap()
    }
    pub fn depends_on_(self, j: u64) -> bool {
        self.inner & (1u64 << j.checked_sub(1).expect("No 0th to depend on")) != 0
    }
    /// If this is the type of a bound variable, return a u64 
    /// whose only activated bit is the bit indicating which bv
    /// it is.
    pub fn bound_digit(self) -> Res<u64> {
        if self.is_bound() {
            Ok(self.inner & !(0xFF << 56))
        } else {
            Err(VerifErr::Msg(format!("Not bound")))
        }
    }
    /// The POSITION (1 - 55) of this bound variable, NOT the literal u64.
    pub fn bound_pos(self) -> Res<u64> {
        if self.is_bound() {
            for i in 0..56 {
                if ((1 << i) & self.inner) != 0 {
                    return Ok(i + 1)
                }
            }
            Err(VerifErr::Msg(format!("should be unreachable")))
        } else {
            Err(VerifErr::Msg(format!("Not bound")))
        }
    }
    pub fn has_deps(self) -> bool {
        if self.is_bound() {
            false
        } else {
            (self.inner & crate::mmb::TYPE_DEPS_MASK) > 0
        }
    }
    /// If this is a regular/not-bound variable, return a u64
    /// whose only activated bits are the ones marking the bvs
    /// on which it depends.
    pub fn deps(self) -> Res<u64> {
        if !self.is_bound() {
            Ok(self.inner & !(0xFF << 56))
        } else {
            Err(VerifErr::Msg(format!("No deps")))
        }
    }
}
#[test]
fn bound1() {
    let mut t1 = Type::new_bound();
    t1 |= Type { inner: (1 << 15) };
    assert_eq!(t1.bound_pos().unwrap(), 16);
}
#[test]
fn bound2() {
    let mut t1 = Type::new_bound();
    t1 |= Type { inner: (1 << 0) };
    assert_eq!(t1.bound_pos().unwrap(), 1);
}
#[test]
fn bound3() {
    let mut t1 = Type::new_bound();
    t1 |= Type { inner: (1 << 55) };
    assert_eq!(t1.bound_pos().unwrap(), 56);
}
#[test]
fn bound_err1() {
    let t1 = Type::new_bound();
    assert!(t1.bound_pos().is_err())
}
#[test]
fn bound_err2() {
    let t1 = Type::new(false);
    assert!(t1.bound_pos().is_err())

#[test]
fn deps1() {
    let t0 = Type { inner: 0 };
    let mut t1_v = Type { inner: 0 };
    let mut t1 = Type { inner: 0 };
    let t2 = Type { inner: 1 };
    let t3 = Type::new_bound();

    assert!(!t0.has_deps());
    assert!(!t1.has_deps());
    assert!(t2.has_deps());
    assert!(!t3.has_deps());
    assert_eq!(t2.deps().unwrap(), 1);
    t1.add_dep(1);
    t1.add_dep(2);
    t1.add_dep(4);
    assert!(t1.has_deps());
    assert_eq!(t1.deps().unwrap(), 11);
    t1_v.add_dep(4);
    t1_v.add_dep(1);
    t1_v.add_dep(2);
    assert!(t1_v.has_deps());
    assert_eq!(t1_v.deps().unwrap(), 11);
    println!("t3: {:?}", t3);
    let bound_1 = Type { inner: Type::new_bound().inner | (1 << 8) };
    println!("bound idx: {:?}", bound_1.bound_digit());
    assert!(bound_1.is_bound());
}

    // Crate a rough backtrace; use the `localize!` macro to make this.

    // Create a rough backtrace; use the `localize!` macro to make this.

        }
    }
}
 /// A reference to an entry in the term table.
#[derive(Debug, Clone, Copy)]
pub struct Term<'a> {
    /// The sort of the term.
    pub term_num: u32,
    pub sort: u8,
    /// Number of args NOT including `ret`
    pub args_start: &'a [u8],
    // The pointer to the start of the unify stream.
    pub unify: UnifyIter<'a>,
}
/// An iterator over the arguments of a term/assertion that doesn't require allocation
/// of a vector, instead reading them from the source file each time.
#[derive(Debug, Clone, Copy)]
pub struct Args<'a> {
    source: &'a [u8],
}
impl<'a> DoubleEndedIterator for Args<'a> {
    fn next_back(&mut self) -> Option<Self::Item> {
        if self.source.is_empty() {
            None
        } else {
            let split = self.source.len().checked_sub(8)?;
            let (lhs, rhs) = self.source.split_at(split);
            self.source = lhs;
            match parse_u64(rhs) {
                Err(_) => unreachable!("Should have been guaranteed by check in `prefix_args`"),
                Ok((parsed, rest)) => {
                    assert!(rest.is_empty());
                    Some(Type { inner: parsed })
                }
            }
        }
    }
}
impl<'a> ExactSizeIterator for Args<'a> {
    fn len(&self) -> usize {
        self.source.len() / std::mem::size_of::<u64>()
    }
}
impl<'a> Iterator for Args<'a> {
    type Item = Arg;
    fn next(&mut self) -> Option<Self::Item> {
        if self.source.is_empty() {
            return None
        }
        match parse_u64(self.source) {
            Err(_) => unreachable!("Should have been guaranteed by check in `prefix_args`"),
            Ok((parsed, rest)) => {
                self.source = rest;
                Some(Type { inner: parsed })
            }
        }
    }
    // Needed for `len` to work correctly.
    fn size_hint(&self) -> (usize, Option<usize>) {
        (
            self.source.len() / std::mem::size_of::<u64>(),
            Some(self.source.len() / std::mem::size_of::<u64>())
        )
    }
}
#[test]
fn args_back1() {
    let s1 = &[
        10, 11, 12, 13, 14, 15, 16, 17,
        18, 19, 20, 21, 22, 23, 24, 25,
        26, 27, 28, 29, 30, 31, 32, 33
    ];
    let s2 = &[
        10, 11, 12, 13, 14, 15, 16, 17,
        18, 19, 20, 21, 22, 23, 24, 25,
    ];
    let s3 = &[
        10, 11, 12, 13, 14, 15, 16, 17,
    ];
    let tgt1 = [26, 27, 28, 29, 30, 31, 32, 33];
    let tgt2 = [18, 19, 20, 21, 22, 23, 24, 25];
    let tgt3 = [10, 11, 12, 13, 14, 15, 16, 17];
    let mut args = Args { source: s1 };
    let back = args.next_back().unwrap();
    assert_eq!(back.inner, u64::from_le_bytes(tgt1));
    assert_eq!(args.source, s2);
    let back = args.next_back().unwrap();
    assert_eq!(back.inner, u64::from_le_bytes(tgt2));
    assert_eq!(args.source, s3);
    let back = args.next_back().unwrap();
    assert_eq!(back.inner, u64::from_le_bytes(tgt3));
    assert!(args.source.is_empty());
}
#[test]
fn args_back_err1() {
    let s1 = &[10, 11, 12, 13, 14, 15, 16];
    let mut args = Args { source: s1 };
    let back = args.next_back();
    assert!(back.is_none());
}
#[test]
fn args_no_ret1() {
    let fake_unify = UnifyIter { buf: &[], pos: 0 };
    let s1 = &[
        10, 11, 12, 13, 14, 15, 16, 17,
        18, 19, 20, 21, 22, 23, 24, 25,
        26, 27, 28, 29, 30, 31, 32, 33
    ];
    let t = Term { term_num: 0, sort: 0, args_start: s1, unify: fake_unify };
    let s2 = &[
        10, 11, 12, 13, 14, 15, 16, 17,
        18, 19, 20, 21, 22, 23, 24, 25,
    ];
    let args_no_ret = t.args_no_ret();
    assert_eq!(args_no_ret.source, s2);
}
#[test]
fn args_no_ret2() {
    let fake_unify = UnifyIter { buf: &[], pos: 0 };
    let s1 = &[
        10, 11, 12, 13, 14, 15, 16, 17,
    ];
    let t = Term { term_num: 0, sort: 0, args_start: s1, unify: fake_unify };
    let args_no_ret = t.args_no_ret();
    assert_eq!(args_no_ret.source, &[]);
}
impl<'a> Term<'a> {
    /// Returns true if this is a `def`, false for a `term`.
    #[inline]
    pub fn is_def(&self) -> bool {
        self.sort & 0x80 != 0
    }
    /// The return sort of this term/def.
    #[inline]
    pub fn sort(&self) -> SortNum {
        self.sort & 0x7F
    }
    /// args; including the `ret` element at the end.
    #[inline]
    pub fn args(&self) -> Args<'a> {
        Args {
            source: self.args_start,
        }
    }
    /// args without the `ret` element at the end.
    /// This will panic if there are less than 8 bytes in `source`,
    /// which seems fine for now, since that would mean we had an invalid `Args` 
    /// to start with.
    #[inline]
    pub fn args_no_ret(&self) -> Args<'a> {
        Args {
            source: &self.args_start[..(self.args_start.len() - std::mem::size_of::<u64>())],
        }
    }    
    pub fn num_args_no_ret(&self) -> u16 {
        u16::try_from(self.args().len().checked_sub(1).unwrap()).unwrap()
    }
    /// The return sort and dependencies.
    pub fn ret(&self) -> Type {
        self.args().last().unwrap()
    }
    /// The beginning of the unify stream for the term.
    #[inline]
    pub fn unify(&self) -> UnifyIter<'_> {
        self.unify.clone()
    }
}
/// A reference to an entry in the theorem table.
#[derive(Debug, Clone, Copy)]
pub struct Assert<'a> {
    /// The array of arguments.
    // `Arg` is a u64
    pub assert_num: u32,
    pub args_start: &'a [u8],
    /// The pointer to the start of the unify stream.
    pub unify: UnifyIter<'a>,
}
impl<'a> Assert<'a> {
    /// The list of arguments of this axiom/theorem.
    #[inline]
    pub fn args(&self) -> Args<'a> {
        Args {
            source: self.args_start,
        }
    }
    /// The beginning of the unify stream.
    #[inline]
    pub fn unify(&self) -> UnifyIter<'a> {
        self.unify.clone()
    }
    pub fn num_args(&self) -> u16 {
        u16::try_from(self.args().len()).unwrap()
    }
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[repr(transparent)]
pub struct Mods {
    pub inner: u8,
}
#[test]
fn test_mods1() {
    let m = Mods { inner: 1 };
    assert!(!m.is_provable());
    let m = Mods { inner: 2 };
    assert!(!m.is_provable());
    let m = Mods { inner: 4 };
    assert!(m.is_provable());
    let m = Mods { inner: 8 };
    assert!(!m.is_provable());
    let m = Mods { inner: 3 };
    assert!(!m.is_provable());
    let m = Mods { inner: 12 };
    assert!(m.is_provable());
    let m = Mods { inner: 7 };
    assert!(m.is_provable());
}
impl Mods {
    pub fn new() -> Self {
        Mods { inner: 0u8 }
    }
    pub fn is_provable(self) -> bool {
        (self.inner & Mods::provable().inner) != 0
    }
    pub fn pure() -> Self {
        Mods { inner: 1 }
    }
    
    pub fn strict() -> Self {
        Mods { inner: 2 }
    }
    pub fn provable() -> Self {
        Mods { inner: 4 }
    }
    pub fn free() -> Self {
        Mods { inner: 8 }
    }
}
/// An iterator over the declaration stream. This is the main provider of 
/// verification obligations for mmb items, giving you both the target (for example,
/// `public term, number 13`) as well as the proof stream. The unification stream
/// Is later looked up using the item number when it's needed.
#[derive(Debug, Clone)]
pub struct DeclIter<'a> {
    /// The full source file.
    pub mmb: &'a [u8],
    /// The index of the current declaration in the file.
    /// Starts at `proof_stream_start` from the header file.
    pub pos: usize,
    pub next_sort_num: u8,
    pub next_termdef_num: u32,
    pub next_assert_num: u32,
}
/// We pair the item number (sortnum, termnum, assertnum) with the statement
/// So that during parallel checking of mmb declarations, we know which item is
/// which, since they may be checked out of order.
impl<'a> Iterator for DeclIter<'a> {
    type Item = Result<(StmtCmd, ProofIter<'a>), VerifErr>;
    fn next(&mut self) -> Option<Self::Item> {
        match try_next_decl(self.mmb, self.pos)? {
            Err(e) => Some(Err(e)),
            Ok((stmt, pr, rest)) => {
                let stmt = match stmt {
                    StmtCmd::Sort {..} => {
                        let num = self.next_sort_num;
                        self.next_sort_num += 1;
                        StmtCmd::Sort { num: Some(num) }
                    }
                    StmtCmd::TermDef {local, ..} => {
                        let num = self.next_termdef_num;
                        self.next_termdef_num += 1;
                        StmtCmd::TermDef { num: Some(num), local }
                    }
                    StmtCmd::Axiom {..} => {
                        let num = self.next_assert_num;
                        self.next_assert_num += 1;
                        StmtCmd::Axiom { num: Some(num) }
                    }
                    StmtCmd::Thm {local, ..} => {
                        let num = self.next_assert_num;
                        self.next_assert_num += 1;
                        StmtCmd::Thm { num: Some(num), local }
                    }
                };
                self.pos = rest;
                Some(Ok((stmt, pr)))
            }
        }
    }
}
/// is only used for `DeclIter::next`.
/// This always gets the full mmb file
fn try_next_decl(mmb: &[u8], pos: usize) -> Option<Res<(StmtCmd, ProofIter<'_>, usize)>> {
    let (cmd, data, rest) = match try_next_cmd(mmb, pos) {
        // Means cmd == 0, but here is unreachable
        Ok(None) => return None,
        // Means there was an error slicing in `try_next_cmd`
        Err(e) => return Some(Err(e)),
        Ok(Some(((cmd, data), rest))) => (cmd, data, rest)
    };
    let next2 = pos + data as usize;
    let pr = ProofIter {
        buf: mmb,
        pos: rest,
        ends_at: pos + (data as usize)
    };
    Some(Ok((
        StmtCmd::try_from(cmd).ok()?,
        pr, 
        next2
    )))
}
// used by proof and unify
// This now always gets the full mmb file.
pub fn try_next_cmd<T>(mmb: &[u8], pos: usize) -> Res<Option<(T, usize)>> 
where T: TryFrom<(u8, u32)> {
    let (cmd, data, new_pos) = parse_cmd(mmb, pos)?;
    if cmd == 0 {
        return Ok(None);
    }
    Ok(Some((
        T::try_from((cmd, data)).map_err(|_| VerifErr::Msg(format!("try_next_cmd failed @ pos {}", pos)))?,
        new_pos
    )))
}
/// Constants used in the MMB specification.
pub mod cmd {
    /// `DATA_8 = 0x40`, used as a command mask for an 8 bit data field
    pub const DATA_8: u8 = 0x40;
    /// `DATA_16 = 0x80`, used as a command mask for a 16 bit data field
    pub const DATA_16: u8 = 0x80;
    /// `DATA_32 = 0xC0`, used as a command mask for a 32 bit data field
    pub const DATA_32: u8 = 0xC0;
    /// `DATA_MASK = 0xC0`, selects one of `DATA_8`, `DATA_16`, or `DATA_32` for data size
    pub const DATA_MASK: u8 = 0xC0;
}
fn parse_cmd(mmb: &[u8], start_at: usize) -> Res<(u8, u32, usize)> {
    match mmb.get(start_at..) {
        None | Some([]) => Err(VerifErr::Msg("Parse cmd exhausted".to_string())),
        Some([n, tl @ ..]) => {
            let cmd_kind = n & !cmd::DATA_MASK;
            let cmd_size = n & cmd::DATA_MASK;
            match cmd_size {
                0 => Ok((cmd_kind, 0, mmb.len() - tl.len())),
                cmd::DATA_8 => {
                    let (data, rest) = parse_u8(tl)?;
                    Ok((cmd_kind, data as u32, mmb.len() - rest.len()))
                }
                cmd::DATA_16 => {
                    let (data, rest) = parse_u16(tl)?;
                    Ok((cmd_kind, data as u32, mmb.len() - rest.len()))
                }
                cmd::DATA_32 => {
                    let (data, rest) = parse_u32(tl)?;
                    Ok((cmd_kind, data, mmb.len() - rest.len()))
                }
                _ => Err(VerifErr::Msg("Parse cmd got unknown size".to_string())),
            }

    pub file_data: &'a crate::fs::FileData,
    pub header: crate::mmb::Header,
    pub index: crate::mmb::index::Index<'a>,

    pub file_view: &'a crate::fs::FileView<'a>,

    pub declarations: Vec<(StmtCmd, ProofIter<'a>)>,

    pub declarations: Vec<(NumdStmtCmd, ProofIter<'a>)>,

    pub fn new_from(file_data: &'a crate::fs::FileData) -> Res<Self> {
        let header = crate::mmb::parse_header(file_data.mmb_file.as_slice())?;
        let index  = crate::mmb::index::parse_index(file_data.mmb_file.as_slice(), header)?;
        let declars = DeclIter {
            mmb: file_data.mmb_file.as_slice(),
            pos: header.proof_stream_start as usize,
            next_sort_num: 0,
            next_termdef_num: 0,
            next_assert_num: 0,
        };

    pub fn mmb_num_sorts_done(&self) -> u8 {
        self.mmb_num_sorts_done.load(Relaxed)
    }
    pub fn mmb_num_termdefs_done(&self) -> u32 {
        self.mmb_num_termdefs_done.load(Relaxed)
    }
    pub fn mmb_num_asserts_done(&self) -> u32 {
        self.mmb_num_asserts_done.load(Relaxed)
    }
    pub fn new_from(file_data: &'a crate::fs::FileView<'a>) -> Res<Self> {
        let declars : Result<Vec<(NumdStmtCmd, ProofIter)>, ParseError> = file_data.mmb.proof().collect();

        let declarations: Vec<(StmtCmd, ProofIter)> = declars.collect::<Result<Vec<(StmtCmd, ProofIter)>, VerifErr>>()?;

            file_data,
            header,
            index,
            declarations,

            file_view: file_data,
            declarations: declars.map_err(|e| VerifErr::Msg(format!("{}", e)))?,

    pub fn add_declar(&self, stmt: StmtCmd) {

    pub fn add_declar(&self, stmt: NumdStmtCmd) {

            StmtCmd::Sort {..} => { self.next_sort(); },
            StmtCmd::TermDef {..} => { self.next_termdef(); },
            StmtCmd::Axiom {..} | StmtCmd::Thm {..} => { self.next_assert(); },

            NumdStmtCmd::Sort {..} => { self.mmb_num_sorts_done.fetch_add(1, Relaxed); },
            NumdStmtCmd::TermDef {..} => { self.mmb_num_termdefs_done.fetch_add(1, Relaxed); },
            NumdStmtCmd::Axiom {..} | NumdStmtCmd::Thm {..} => { self.mmb_num_asserts_done.fetch_add(1, Relaxed); },

    pub fn assert_mmz_done(&self, mmz: &crate::mmz::MmzMem<'a>, errs: &mut Vec<VerifErr>) {
        if mmz.num_sorts_done() != self.header.num_sorts {
            errs.push(VerifErr::Msg(format!(

    pub fn assert_mmz_done(&self, mmz: &crate::mmz::MmzMem<'a>) -> Res<()> {
        if mmz.num_sorts_done().into_inner() != self.file_view.mmb.header.num_sorts {
            return Err(VerifErr::Msg(format!(

                mmz.num_sorts_done(), 
                self.header.num_sorts

                mmz.num_sorts_done().into_inner(), 
                self.file_view.mmb.header.num_sorts

        if mmz.num_termdefs_done() != self.header.num_terms {
            errs.push(VerifErr::Msg(format!(

        if mmz.num_termdefs_done() != self.file_view.mmb.header.num_terms.get() {
            return Err(VerifErr::Msg(format!(

                self.header.num_terms

                self.file_view.mmb.header.num_terms.get()

        if mmz.num_asserts_done() != self.header.num_thms {
            errs.push(VerifErr::Msg(format!(

        if mmz.num_asserts_done() != self.file_view.mmb.header.num_thms.get() {
            return Err(VerifErr::Msg(format!(

                self.header.num_thms

                self.file_view.mmb.header.num_thms.get()

        Ok(())

    pub fn assert_mmb_done(&self, errs: &mut Vec<VerifErr>) {
        if self.mmb_num_sorts_done() != self.header.num_sorts {
            errs.push(VerifErr::Msg(format!(

    pub fn assert_mmb_done(&self) -> Res<()> {
        if self.mmb_num_sorts_done() != self.file_view.mmb.header.num_sorts {
            return Err(VerifErr::Msg(format!(

                self.header.num_sorts

                self.file_view.mmb.header.num_sorts

        }

        } 

        if self.mmb_num_termdefs_done() != self.header.num_terms {
            errs.push(VerifErr::Msg(format!(

        if self.mmb_num_termdefs_done() != self.file_view.mmb.header.num_terms.get() {
            return Err(VerifErr::Msg(format!(

                self.header.num_terms

                self.file_view.mmb.header.num_terms.get()

        if self.mmb_num_asserts_done() != self.header.num_thms {
            errs.push(VerifErr::Msg(format!(

        if self.mmb_num_asserts_done() != self.file_view.mmb.header.num_thms.get() {
            return Err(VerifErr::Msg(format!(

                self.header.num_thms

                self.file_view.mmb.header.num_thms.get()

    }
}
impl<'a> Outline<'a> {
    pub fn mmb(&self) -> &'a [u8] {
        self.file_data.mmb_file.as_slice()
    }
    pub fn mmb_num_sorts_done(&self) -> u8 {
        self.mmb_num_sorts_done.load(Relaxed)
    }
    pub fn mmb_num_termdefs_done(&self) -> u32 {
        self.mmb_num_termdefs_done.load(Relaxed)
    }
    pub fn mmb_num_asserts_done(&self) -> u32 {
        self.mmb_num_asserts_done.load(Relaxed)
    }
    fn next_sort(&self) -> u8 {
        self.mmb_num_sorts_done.fetch_add(1, Relaxed)
    }
    
    fn next_termdef(&self) -> u32 {
        self.mmb_num_termdefs_done.fetch_add(1, Relaxed)
    }
    fn next_assert(&self) -> u32 {
        self.mmb_num_asserts_done.fetch_add(1, Relaxed)
    }
    pub fn get_sort_mods(&self, n: usize) -> Res<Mods> {
        none_err! {
            self
            .mmb()
            .get(self.header.sort_data_start as usize + n)
            .map(|byte| Mods { inner: *byte })
        }
    }    
    /// Get a term (by number) from the mmb file
    pub fn get_term_by_num(&self, term_num: u32) -> Res<Term<'a>> {
        let start_point = (self.header.terms_start as usize) + ((term_num as usize) * 8);
        let source = none_err!(self.mmb().get(start_point..))?;
        let (num_args, source) = parse_u16(source)?;
        let (sort, source) = parse_u8(source)?;
        let (_reserved, source) = parse_u8(source)?;
        let (term_args_start, _) = parse_u32(source)?;
        let args_start = none_err!(self.mmb().get(term_args_start as usize..))?;
        let split_point = none_err!{ std::mem::size_of::<u64>().checked_mul((num_args + 1) as usize) }?;
        let (args_start, unify_start) = args_start.split_at(split_point);
        let unify = UnifyIter {
            buf: self.mmb(),
            pos: self.mmb().len() - unify_start.len(),
        };
        Ok(Term { term_num, sort, args_start, unify })
    }
    /// Get an assertion (by number) from the mmb file
    pub fn get_assert_by_num(&self, assert_num: u32) -> Res<Assert<'a>> {
        let thm_start = (self.header.thms_start + (assert_num * 8)) as usize;
        let source = self.mmb().get(thm_start..).ok_or(VerifErr::Msg(format!("Bad index")))?;
        let (num_args, source) = parse_u16(source)?;
        let (_reserved, source) = parse_u16(source)?;
        let (args_start, _) = parse_u32(source)?;
        let args_slice = none_err!(self.mmb().get(args_start as usize..))?;
        let split_point = none_err! { std::mem::size_of::<u64>().checked_mul(num_args as usize) }?;
        let (args_start, unify_start) = args_slice.split_at(split_point);
        let unify = UnifyIter {
            buf: self.mmb(),
            pos: self.mmb().len() - unify_start.len(),
        };
        Ok(Assert { assert_num, args_start, unify })        
    }      
}
/// These are helper functions for rendering unsigned integers
/// as a sequence of bits. For example, `view64(TYPE_SORT_MASK)` renders as:
///
/// 10000000_11111111_11111111_11111111_11111111_11111111_11111111_11111111
/// 
/// They're not efficient, but they're for debugging and I'm too lazy to write efficient
/// ones right now.
pub fn view64(n: u64) -> String {
    let s = format!("{:#066b}", n);  
    let mut acc = String::new();
    for (idx, c) in s.chars().skip(2).enumerate() {
        if idx % 8 == 0 && idx != 0 {
            acc.push('_');
        }
        acc.push(c);

        Ok(())

    acc

pub fn view32(n: u32) -> String {
    let s = format!("{:#034b}", n);  
    let mut acc = String::new();
    for (idx, c) in s.chars().skip(2).enumerate() {
        if idx % 8 == 0 && idx != 0 {
            acc.push('_');
        }
        acc.push(c);
    }
    acc
}

///// These are helper functions for rendering unsigned integers
///// as a sequence of bits. For example, `view64(TYPE_SORT_MASK)` renders as:
/////
///// 10000000_11111111_11111111_11111111_11111111_11111111_11111111_11111111
///// 
///// They're not efficient, but they're for debugging and I'm too lazy to write efficient
///// ones right now.
//pub fn view64(n: u64) -> String {
//    let s = format!("{:#066b}", n);  
//    let mut acc = String::new();
//    for (idx, c) in s.chars().skip(2).enumerate() {
//        if idx % 8 == 0 && idx != 0 {
//            acc.push('_');
//        }
//        acc.push(c);
//    }
//    acc
//}

pub fn view16(n: u16) -> String {
    let s = format!("{:#018b}", n);  
    let mut acc = String::new();
    for (idx, c) in s.chars().skip(2).enumerate() {
        if idx % 8 == 0 && idx != 0 {
            acc.push('_');
        }
        acc.push(c);
    }
    acc
}

//pub fn view32(n: u32) -> String {
//    let s = format!("{:#034b}", n);  
//    let mut acc = String::new();
//    for (idx, c) in s.chars().skip(2).enumerate() {
//        if idx % 8 == 0 && idx != 0 {
//            acc.push('_');
//        }
//        acc.push(c);
//    }
//    acc
//}

pub fn view8(n: u8) -> String {
    let s = format!("{:#010b}", n);  
    let mut acc = String::new();
    for (idx, c) in s.chars().skip(2).enumerate() {
        if idx % 8 == 0 && idx != 0 {
            acc.push('_');
        }
        acc.push(c);
    }
    acc
}

//pub fn view16(n: u16) -> String {
//    let s = format!("{:#018b}", n);  
//    let mut acc = String::new();
//    for (idx, c) in s.chars().skip(2).enumerate() {
//        if idx % 8 == 0 && idx != 0 {
//            acc.push('_');
//        }
//        acc.push(c);
//    }
//    acc
//}

impl Debug for Type {
    fn fmt(&self, f: &mut Formatter) -> FmtResult {
        write!(f, "{}", view64(self.inner))
    }
}

//pub fn view8(n: u8) -> String {
//    let s = format!("{:#010b}", n);  
//    let mut acc = String::new();
//    for (idx, c) in s.chars().skip(2).enumerate() {
//        if idx % 8 == 0 && idx != 0 {
//            acc.push('_');
//        }
//        acc.push(c);
//    }
//    acc
//}

use std::convert::TryFrom;

use crate::mmb::stmt::StmtCmd;

use mm0b_parser::NumdStmtCmd;

    Mods, 

    SortNum,
    Type,

    Term, 
    Assert, 

    Args,

use crate::mmb::unify::{ UnifyCmd, UnifyIter, UMode };

use mm0b_parser::{ UnifyCmd, Arg, Type, UnifyIter, TermRef, ThmRef };
use mm0_util::{ SortId, Modifiers };
use crate::mmb::unify::{ UMode };

    pub fn is_empty(&self) -> bool {
        self.mmz_pos == self.mmz.len()
    }
    pub fn cur(&self) -> Option<u8> {
        self.mmz.get(self.mmz_pos).copied()
    }

    pub fn advance(&mut self, n: usize) {
        self.mmz_pos += n;
    }       

        stmt_cmd: StmtCmd, 
        item: Option<Either<Term<'a>, Assert<'a>>>

        stmt_cmd: NumdStmtCmd, 
        item: Option<Either<TermRef<'a>, ThmRef<'a>>>

                let mut mmz_st = MmzState::new_from(&mut *self, bump);

                let mut mmz_st = MmzState::new_from(self, bump);

                        make_sure!(matches!(stmt_cmd, StmtCmd::Axiom {..}) || matches!(stmt_cmd, StmtCmd::Thm {..}));

                        make_sure!(matches!(stmt_cmd, NumdStmtCmd::Axiom {..}) || matches!(stmt_cmd, NumdStmtCmd::Thm {..}));

                    format!("`parse_until` ran out of input with remaining verification obligations.")

                    format!("`parse_until` ran out of input with remaining verification obligations. Remaining: {:?}", String::from_utf8_lossy(self.cur_slice()))

    pub fn coerce(&mut self, e_x: MmzExpr<'b>, z: SortNum) -> Res<MmzExpr<'b>> {

    pub fn coerce(&mut self, e_x: MmzExpr<'b>, z: SortId) -> Res<MmzExpr<'b>> {

        let _binders = self.binders(term.args(), "notation")?;

        let _binders = self.binders(term.args_and_ret(), "notation")?;

            term.term_num,

            term.tid.into_inner(),

            term.num_args_no_ret(),

            u16::try_from(term.args().len()).unwrap(),

        for (s1, m) in self.mem.coes.iter() {
            for s2 in m.keys() {
                if self.mem.outline.get_sort_mods(*s2 as usize)?.is_provable() {
                    if let Some(_s2) = provs.insert(*s1, *s2) {
                        println!("Coercion diamond to provable detected");
                        panic!();

        for (&s1, m) in self.mem.coes.iter() {
            for s2 in m.keys().copied() {
                if self.mem.outline.file_view.mmb_sort_mods(s2)?.contains(Modifiers::PROVABLE) {
                    if let Some(_s2) = provs.insert(s1, s2) {
                        return Err(VerifErr::Msg(format!("Coercion diamond to provable detected. from: {:?}, to: {:?}", s1, s2)))

        term: Term,

        term: TermRef,

        from: u8,
        to: u8,

        from: SortId,
        to: SortId,

        term: Term,
        x: u8,
        y: u8,

        term: TermRef,
        x: SortId,
        y: SortId,

            Some(&Coe::Single { term_num }) if term_num == term.term_num => return Ok(()),

            Some(&Coe::Single { term_num }) if term_num == term.tid => return Ok(()),

        let coe_x_y = Arc::new(Coe::Single { term_num: term.term_num });

        let coe_x_y = Arc::new(Coe::Single { term_num: term.tid });

        term: Term,

        term: TermRef,

        from: u8,
        to: u8,

        from: SortId,
        to: SortId,

        assert_eq!(term.num_args_no_ret(), 1);

        assert_eq!(term.args().len(), 1);

        let from_num = self.mem.get_sort_num(from)?;
        let to_num = self.mem.get_sort_num(to)?;

        let from_num = self.mem.get_sort_id(from)?;
        let to_num = self.mem.get_sort_id(to)?;

        term: Term<'a>,

        term: TermRef<'a>,

        if let Some(n) = term.num_args_no_ret().checked_sub(1) {

        if let Some(n) = term.args().len().checked_sub(1) {

            term_num: term.term_num,

            term_num: term.tid.into_inner(),

        if term.num_args_no_ret() > 0 {

        if term.args().len() > 0 {

        term: Term<'a>,

        term: TermRef<'a>,

                if term.num_args_no_ret() != 2 {

                if term.args().len() != 2 {

                        format!("infix notations must be for terms with 2 arguments. {:?} had {}", term_ident, term.num_args_no_ret())

                        format!("infix notations must be for terms with 2 arguments. {:?} had {}", term_ident, term.args().len())

                    term_num: term.term_num,

                    term_num: term.tid.into_inner(),

    fn sort(&mut self) -> Res<(Str<'a>, Mods)> {
        let mut mods = Mods::new();

    fn sort(&mut self) -> Res<(Str<'a>, Modifiers)> {
        let mut mods = Modifiers::empty();

                mods |= Mods::provable();

                mods.insert(Modifiers::PROVABLE);

                mods |= Mods::strict();

                mods.insert(Modifiers::STRICT);

                mods |= Mods::pure();

                mods.insert(Modifiers::PURE);

                mods |= Mods::free();

                mods.insert(Modifiers::FREE);

        let mmb_mods = self.mem.outline.get_sort_mods(self.mem.num_sorts_done() as usize)?;

        let mmb_mods = self.mem.outline.file_view.mmb_sort_mods(self.mem.num_sorts_done())?;

        self.mem.add_sort(ident);

        self.mem.add_sort(ident)?;

        term: Term<'a>,

        term: TermRef<'a>,

        let mode = if term.def() { "def" } else { "term" };
        self.binders(term.args_and_ret(), mode)?;

        let mode = if term.is_def() { "def" } else { "term" };
        self.binders(term.args(), mode)?;
        if term.is_def() && self.peek_word() == b"=" {

        if term.def() && self.peek_word() == b"=" {

        assert: Assert<'a>,

        assert: ThmRef<'a>,

        args: Args<'a>,

        args: &[Arg],

            let args_todo = args.skip(self.non_dummy_vars().count());

            let args_todo = args.iter().copied().skip(self.non_dummy_vars().count());

        let args_todo = args.skip(self.non_dummy_vars().count());

        let args_todo = args.iter().copied().skip(self.non_dummy_vars().count());

    fn binder_group(&mut self, args_todo: std::iter::Skip<Args<'a>>, mode: &str) -> Res<()> {

    fn binder_group<I>(&mut self, args_todo: I, mode: &str) -> Res<()> 
    where I: Iterator<Item = Arg> + ExactSizeIterator {

        let sort_num = self.mem.get_sort_num(sort_ident)?;

        let sort_id = self.mem.get_sort_id(sort_ident)?;
        // Needs to make a new bound type

        ty_accum.add_sort(sort_num);

        ty_accum.add_sort(sort_id);

            ty_accum.inner |= self.take_next_bv();

            ty_accum |= Type::from(self.take_next_bv());

                let dep_pos = 1 + none_err!(self.potential_deps().position(|v| v.ident == Some(dep_ident)))?;

                let dep_pos = none_err!(self.potential_deps().position(|v| v.ident == Some(dep_ident)))?;

    fn return_ty(&mut self, mut arrow_args: std::iter::Skip<Args<'a>>, mode: &str) -> Res<()> {

    fn return_ty<I>(&mut self, mut arrow_args: I, mode: &str) -> Res<()> 
    where I: Iterator<Item = Arg> + ExactSizeIterator + Clone {

                let sort_num = self.mem.get_sort_num(sort_ident)?;
                let mut ty_accum = Type::new_with_sort(sort_num);

                let sort_id = self.mem.get_sort_id(sort_ident)?;
                let mut ty_accum = Type::new_of_sort(sort_id.into_inner());

                    let dep_pos = 1 + none_err!(self.potential_deps().position(|v| v.ident == Some(dep_ident)))?;

                    let dep_pos = none_err!(self.potential_deps().position(|v| v.ident == Some(dep_ident)))?;

            match maybe_cmd? {

            match maybe_cmd.map_err(|e| VerifErr::Msg(format!("{}", e)))? {

                UnifyCmd::Term { term_num, save } => {

                UnifyCmd::Term { tid, save } => {

                        make_sure!(term_num == n2);

                        make_sure!(tid == n2);

                UnifyCmd::Dummy { sort_id } => {

                UnifyCmd::Dummy(sort_id) => {

    SortNum,
    TermNum,
    AssertNum,

    Type,
    Term

use crate::mmb::stmt::StmtCmd;

use mm0_util::{ Modifiers, SortId, TermId, ThmId };
use mm0b_parser::{ NumdStmtCmd, TermRef, Type };

        term_num: u32,

        term_num: TermId,

        sort: SortNum,

        sort: SortId,

    fn sort(self) -> SortNum {

    fn sort(self) -> SortId {

        self.ty.is_bound()

        self.ty.bound()

    pub fn sort(self) -> u8 {

    pub fn sort(self) -> SortId {

//#[derive(Debug)]
//pub struct DeclaredNotation<'a> {
//    pub has_coe: bool,
//    pub consts: Vec<(Str<'a>, Option<Fix>)>
//}

//impl<'a> std::default::Default for DeclaredNotation<'a> {
//    fn default() -> Self {
//        DeclaredNotation {
//            has_coe: false,
//            consts: Vec::new()
//        }
//    }
//}

        term_num: TermNum,

        term_num: TermId,

        middleman_sort: SortNum,

        middleman_sort: SortId,

    // unneeded
    //pub declared_notations: FxIndexMap<Str<'a>, DeclaredNotation<'a>>,
    pub nonlocal_termdefs: HashMap<TermIdent<'a>, TermNum>,
    pub nonlocal_asserts: HashMap<AssertIdent<'a>, AssertNum>,

    pub nonlocal_termdefs: HashMap<TermIdent<'a>, TermId>,
    pub nonlocal_asserts: HashMap<AssertIdent<'a>, ThmId>,

    pub provs: HashMap<SortNum, bool>,

    pub provs: HashMap<SortId, bool>,

    pub coes: HashMap<SortNum, HashMap<SortNum, Coe>>,

    pub coes: HashMap<SortId, HashMap<SortId, Coe>>,

    pub coe_prov: HashMap<SortNum, SortNum>,

    pub coe_prov: HashMap<SortId, SortId>,

            mmz: none_err!(outline.file_data.mmz_files.first())?.as_bytes(),
            mmz_files: outline.file_data.mmz_files.as_slice(),

            mmz: none_err!(outline.file_view.mmz.first())?.as_bytes(),
            mmz_files: outline.file_view.mmz,

            //declared_notations: FxIndexMap::with_hasher(Default::default()),

    pub fn verify1(&mut self, bump: &mut Bump, stmt: StmtCmd) -> Res<()> {

    pub fn verify1(&mut self, bump: &mut Bump, stmt: NumdStmtCmd) -> Res<()> {

                StmtCmd::Sort {..} => None,
                StmtCmd::TermDef {..} => {
                    let term = self.outline.get_term_by_num(self.num_termdefs_done())?;

                NumdStmtCmd::Sort {..} => None,
                NumdStmtCmd::TermDef {..} => {
                    let term = none_err!(self.outline.file_view.mmb.term(TermId(self.num_termdefs_done())))?;

                StmtCmd::Axiom {..} | StmtCmd::Thm {..} => {
                    let assert = self.outline.get_assert_by_num(self.num_asserts_done())?;

                NumdStmtCmd::Axiom {..} | NumdStmtCmd::Thm {..} => {
                    let assert = none_err!(self.outline.file_view.mmb.thm(ThmId(self.num_asserts_done())))?;

    pub fn coe_prov_or_else(&self, from: SortNum) -> SortNum {

    pub fn coe_prov_or_else(&self, from: SortId) -> SortId {

    pub fn add_termdef(&mut self, ident: Str<'a>) -> TermNum {
        let idx = self.num_termdefs;

    pub fn add_termdef(&mut self, ident: Str<'a>) -> TermId {
        let idx = TermId(self.num_termdefs);

    pub fn add_assert(&mut self, ident: Str<'a>) -> AssertNum {
        let idx = self.num_asserts;

    pub fn add_assert(&mut self, ident: Str<'a>) -> ThmId {
        let idx = ThmId(self.num_asserts);

    pub fn get_sort_num(&self, ident: Str<'a>) -> Res<u8> {

    pub fn get_sort_id(&self, ident: Str<'a>) -> Res<SortId> {

        conv_err!(u8::try_from(idx))

        conv_err!(u8::try_from(idx).map(|n| SortId(n)))

    pub fn add_sort(&mut self, ident: Str<'a>) -> SortNum {

    pub fn add_sort(&mut self, ident: Str<'a>) -> Res<SortId> {

        let sort_num = u8::try_from(idx).unwrap();
        let mods = self.outline.get_sort_mods(idx).unwrap();
        assert!(self.provs.insert(sort_num, mods.is_provable()).is_none());
        sort_num

        let sort_id = SortId(u8::try_from(idx).unwrap());
        let is_provable = self.outline.file_view.mmb_sort_mods(sort_id)?.contains(Modifiers::PROVABLE);
        assert!(self.provs.insert(sort_id, is_provable).is_none());
        Ok(sort_id)

    pub fn num_sorts_done(&self) -> u8{
        self.num_sorts

    pub fn num_sorts_done(&self) -> SortId {
        SortId(self.num_sorts)

    pub fn add_declar(&mut self, stmt_cmd: StmtCmd) {

    pub fn add_declar(&mut self, stmt_cmd: NumdStmtCmd) {

            StmtCmd::Sort {..} => self.num_sorts += 1,
            StmtCmd::TermDef {..} => self.num_termdefs += 1,
            StmtCmd::Axiom {..} | StmtCmd::Thm {..} => self.num_asserts += 1,

            NumdStmtCmd::Sort {..} => self.num_sorts += 1,
            NumdStmtCmd::TermDef {..} => self.num_termdefs += 1,
            NumdStmtCmd::Axiom {..} | NumdStmtCmd::Thm {..} => self.num_asserts += 1,

    pub fn get_term_by_ident(&self, ident: &Str<'a>) -> Res<Term<'a>> {

    pub fn get_term_by_ident(&self, ident: &Str<'a>) -> Res<TermRef<'a>> {

        self.outline.get_term_by_num(term_num)

        none_err!(self.outline.file_view.mmb.term(term_num))

        assert!(outgoing >> 56 == 0);

        assert!(outgoing >> 55 == 0);

    /// Produce an iterator with the same elements as what an Mmb `Args` should have ()
    pub fn args_iter(&self) -> impl Iterator<Item = MmzVar> {
        self.vars_done.iter().copied().filter(|v| !v.is_dummy)
    }

use std::convert::TryFrom;

    Term,

use mm0_util::TermId;
use mm0b_parser::TermRef;

        if term.num_args_no_ret() == 0 {

        if term.args().len() == 0 {

                term_num: term.term_num, 

                term_num: term.tid, 

            for arg in term.args() {

            for arg in term.args_and_ret() {

                term_num: term.term_num,
                num_args: term.num_args_no_ret(),

                term_num: term.tid,
                num_args: u16::try_from(term.args().len()).unwrap(),

                let term = self.mem.outline.get_term_by_num(term_num)?;

                let term = none_err!(self.mem.outline.file_view.mmb.term(TermId(term_num)))?;

        term: Term<'a>, 

        term: TermRef<'a>, 

                    let sig_e = none_err!(term.args().nth(*pos))?;

                    let sig_e = none_err!(term.args_and_ret().get(*pos))?;

            term_num: term.term_num,
            num_args: term.num_args_no_ret(),

            term_num: term.tid,
            num_args: u16::try_from(term.args().len()).unwrap(),

    fn take_ge_infix(&mut self, last_prec: Prec) -> Option<Res<(Term<'a>, Prec)>> {

    fn take_ge_infix(&mut self, last_prec: Prec) -> Option<Res<(TermRef<'a>, Prec)>> {

        let infix_term = self.mem.outline.get_term_by_num(notation_info.term_num);

        let infix_term = none_err!(self.mem.outline.file_view.mmb.term(TermId(notation_info.term_num)));

        (op0_term, op0_prec): (Term<'a>, Prec),

        (op0_term, op0_prec): (TermRef<'a>, Prec),

            let mut plus_args = op0_term.args();
            if let (Some(fst), Some(snd), Some(_), None) = (plus_args.next(), plus_args.next(), plus_args.next(), plus_args.next()) {

            if let [fst, snd, _] = op0_term.args_and_ret() {

                    term_num: op0_term.term_num,
                    num_args: op0_term.num_args_no_ret(),

                    term_num: op0_term.tid,
                    num_args: u16::try_from(op0_term.args().len()).unwrap(),

/// `STMT_AXIOM = 0x02`, starts an `axiom` declaration
pub const STMT_AXIOM: u8 = 0x02;
/// `STMT_SORT = 0x04`, starts a `sort` declaration
pub const STMT_SORT: u8 = 0x04;
// `STMT_TERM = 0x05`, starts a `term` declaration
//pub const STMT_TERM: u8 = 0x05;
/// `STMT_DEF = 0x05`, starts a `def` declaration. (This is the same as
/// `STMT_TERM` because the actual indication of whether this is a
/// def is in the term header)
pub const STMT_DEF: u8 = 0x05;
/// `STMT_THM = 0x06`, starts a `theorem` declaration
pub const STMT_THM: u8 = 0x06;
/// `STMT_LOCAL = 0x08`, starts a `local` declaration
/// (a bit mask to be combined with `STMT_THM` or `STMT_DEF`)
pub const STMT_LOCAL: u8 = 0x08;
/// `STMT_LOCAL_DEF = 0x0D`
pub const STMT_LOCAL_DEF: u8 = STMT_LOCAL | STMT_DEF;
/// `STMT_LOCAL_THM = 0x0E`
pub const STMT_LOCAL_THM: u8 = STMT_LOCAL | STMT_THM;
/// The main part of the proof consists of a sequence of declarations,
/// and these commands denote the different kind of declaration that can
/// be introduced.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum StmtCmd {
    /// A new sort. Equivalent to `sort foo;`. This is followed by no data,
    /// as the sort data is stored in the header.
    Sort { num: Option<u8> },
    /// A new axiom. Equivalent to `axiom foo ...`. This is followed by a proof
    /// sequence, that should unify with the unify sequence in the header.
    Axiom { num: Option<u32> },
    /// A new term or def. Equivalent to `term/def foo ...`.
    /// If `local` is true, then this is `local def foo`. This is followed by
    /// no data, as the header contains the unify sequence and can be checked on its own.
    TermDef { num: Option<u32>, local: bool },
    /// A new theorem. Equivalent to `(pub) theorem foo ...`, where `local` means
    /// that the theorem is not `pub`. This is followed by a proof sequence,
    /// that will construct the statement and proof, and should unify
    /// with the unify sequence in the header.
    Thm { num: Option<u32>, local: bool },
}
impl StmtCmd {
    pub fn is_local(self) -> bool {
        match self {
            | StmtCmd::TermDef { local: true, .. } 
            | StmtCmd::Thm { local: true, .. } => true,
            _ => false
        }
    }
}
impl std::convert::TryFrom<u8> for StmtCmd {
    type Error = ();
    fn try_from(cmd: u8) -> Result<Self, ()> {
        Ok(match cmd {
            STMT_SORT => StmtCmd::Sort { num: None },
            STMT_AXIOM => StmtCmd::Axiom { num: None },
            STMT_DEF => StmtCmd::TermDef { num: None, local: false },
            STMT_LOCAL_DEF => StmtCmd::TermDef { num: None, local: true },
            STMT_THM => StmtCmd::Thm { num: None, local: false },
            STMT_LOCAL_THM => StmtCmd::Thm { num: None, local: true },
            _ => return Err(()),
        })
    }
}

use std::fmt::{ Debug, Formatter, Result as FmtResult };
use crate::mmb::Header;
use crate::util::{
    parse_u8,
    parse_u32,
    parse_u64,
    Res,
    VerifErr
};
use crate::none_err;
/// A parsed `MMB` file index.
pub struct Index<'a> {
    /// The full file
    pub mmb: &'a [u8],
    /// A pointer to the root of the binary search tree, for searching based on name.
    pub root: u64,
    /// Pointers to the index entries for the sorts
    pub sorts: Vec<u64>,
    /// Pointers to the index entries for the terms
    // The u64 you get back is to an `indexentry`.
    pub terms: Vec<u64>,
    /// Pointers to the index entries for the theorems
    pub thms: Vec<u64>,
}
impl<'a> Debug for Index<'a> {
    fn fmt(&self, f: &mut Formatter) -> FmtResult {
        let mut d = f.debug_struct("Index");
        d.field("root", &self.root);
        d.field("sorts", &self.sorts);
        d.field("terms", &self.terms);
        d.field("thms", &self.thms);
        d.finish()
    }
}
impl<'a> std::default::Default for Index<'a> {
    fn default() -> Index<'a> {
        Index {
            mmb: b"",
            root: 0,
            sorts: Vec::new(),
            terms: Vec::new(),
            thms: Vec::new(),
        }
    }
}
#[derive(Debug, Clone)]
pub struct IndexEntry<'a> {
    // pointer to left subchild (for binary searching by strings)
    pub left: u64,
    // pointer to right subchild
    pub right: u64,
    // For locating in the source file
    pub row: u32,
    // For locating in the source file
    pub col: u32,
    // pointer to the command that declares this item
    pub proof: u64,
    // Index of the object in the relevant table
    pub ix: u32,
    // sort, term, thm, var
    pub kind: u8,
    // zero-terminated char* buffer
    pub charbuff: &'a [u8],
}
use crate::Outline;
impl<'a> Outline<'a> {
    #[inline]
    pub fn term_index_entry(&self, term_num: u32) -> Option<IndexEntry<'a>> {
        let entry = *&self.index.terms[term_num as usize];
        self.index_entry(entry as usize)
    }
    #[inline]
    pub fn assert_index_entry(&self, assert_num: u32) -> Option<IndexEntry<'a>> {
        let entry = *&self.index.thms[assert_num as usize];
        self.index_entry(entry as usize)
    }
    #[inline]
    pub fn index_entry(&self, start_at: usize) -> Option<IndexEntry<'a>> {
        let (left, rest) = parse_u64(&self.mmb()[start_at..]).unwrap();
        let (right, rest) = parse_u64(rest).unwrap();
        let (row, rest) = parse_u32(rest).unwrap();
        let (col, rest) = parse_u32(rest).unwrap();
        let (proof, rest) = parse_u64(rest).unwrap();
        let (ix, rest) = parse_u32(rest).unwrap();
        let (kind, rest) = parse_u8(rest).unwrap();
        let charbuff = parse_cstr(rest)?;
        Some(IndexEntry {
            left,
            right,
            row,
            col,
            proof,
            ix,
            kind,
            charbuff,
        })
    }
}
fn parse_cstr<'a>(source: &'a [u8]) -> Option<&'a [u8]> {
    let null = source.iter().position(|c| *c == 0)?;
    let (s, _) = source.split_at(null);
    Some(s)
}
pub fn parse_index<'a>(mmb: &'a [u8], header: Header) -> Res<Index<'a>> {
    let (root, rest) = parse_u64(&mmb[header.index_start as usize..])
        .expect("Failed to get u64 for index root");
    let (sorts, rest) = prefix_u64(rest, header.num_sorts as usize)
        .expect("Failed to get sorts in index");
    let (terms, rest) = prefix_u64(rest, header.num_terms as usize)
        .expect("Failed to get num terms");
    let (thms, _) = prefix_u64(rest, header.num_thms as usize)
        .expect("Failed to get num thms in index");
    Ok(Index {
        mmb,
        root,
        sorts,
        terms,
        thms,
    })
}
#[inline]
pub fn prefix_u64(mut bytes: &[u8], num_elems: usize) -> Res<(Vec<u64>, &[u8])> {
    let split_point = none_err!{ std::mem::size_of::<u64>().checked_mul(num_elems) }?;
    if split_point <= bytes.len() {
        let mut v = Vec::with_capacity(num_elems);
        for _ in 0..num_elems {
            let (inner, rest_) = parse_u64(bytes)?;
            bytes = rest_;
            v.push(inner);
        }
        Ok((v, bytes))
    } else {
        Err(VerifErr::Msg(format!("Bad prefix arg")))
    }
}

use bumpalo::collections::Vec as BumpVec;

use mm0b_parser::{ UnifyIter, UnifyCmd };
use mm0_util::{ SortId, TermId };

use crate::util::try_next_cmd;

/// `UNIFY_TERM = 0x30`: See [`UnifyCmd`](super::UnifyCmd).
pub const UNIFY_TERM: u8 = 0x30;
/// `UNIFY_TERM_SAVE = 0x31`: See [`UnifyCmd`](super::UnifyCmd).
pub const UNIFY_TERM_SAVE: u8 = 0x31;
/// `UNIFY_REF = 0x32`: See [`UnifyCmd`](super::UnifyCmd).
pub const UNIFY_REF: u8 = 0x32;
/// `UNIFY_DUMMY = 0x33`: See [`UnifyCmd`](super::UnifyCmd).
pub const UNIFY_DUMMY: u8 = 0x33;
/// `UNIFY_HYP = 0x36`: See [`UnifyCmd`](super::UnifyCmd).
pub const UNIFY_HYP: u8 = 0x36;
/// Unify commands appear in the header data for a `def` or `axiom`/`theorem`.
/// They are executed by the [`ProofCmd::Thm`] command in order to perform
/// substitutions. The state of the unify stack machine is:
///
/// * `MS: Stack<StackEl>`: The main stack, called `S` in the [`ProofCmd`]
///   documentation.
///   Since a unification is called as a subroutine during a proof command,
///   the main stack is available, but most operations don't use it.
/// * `S: Stack<Expr>`: The unify stack, which contains expressions
///   from the target context that are being destructured.
/// * `H: Vec<Expr>: The unify heap, also known as the substitution. This is
///   initialized with the expressions that the target context would like to
///   substitute for the variable names in the theorem being applied, but
///   it can be extended in order to support substitutions with sharing
///   as well as dummy variables.
#[derive(Debug, Clone, Copy)]
pub enum UnifyCmd {
    /// ```text
    /// UTerm t: S, (t e1 ... en) --> S, en, ..., e1
    /// USave: H; S, e --> H, e; S, e
    /// UTermSave t = USave; UTerm t:
    ///   H; S, (t e1 ... en) --> H, (t e1 ... en); S, en, ..., e1
    /// ```
    /// Pop an element from the stack, ensure that the head is `t`, then
    /// push the `n` arguments to the term (in reverse order, so that they
    /// are dealt with in the correct order in the command stream).
    /// `UTermSave` does the same thing but saves the term to the unify heap
    /// before the destructuring.
    Term {
        /** The term that should be at the head */
        term_num: u32,
        /** True if we want to recall this substitution for later */
        save: bool,
    },
    /// ```text
    /// URef i: H; S, Hi --> H; S
    /// ```
    /// Get the `i`-th element from the unify heap (the substitution),
    /// and match it against the head of the unify stack.
    Ref(u32),
    /// ```text
    /// UDummy s: H; S, x --> H, x; S   (where x:s)
    /// ```
    /// Pop a variable from the unify stack (ensure that it is a name of
    /// the appropriate sort) and push it to the heap (ensure that it is
    /// distinct from everything else in the substitution).
    Dummy { sort_id: u8 },
    /// ```text
    /// UHyp (UThm mode):  MS, |- e; S --> MS; S, e
    /// UHyp (UThmEnd mode):  HS, e; S --> HS; S, e
    /// ```
    /// `UHyp` is a command that is used in theorem declarations to indicate that
    /// we are about to read a hypothesis. There are two contexts where we read
    /// this, when we are first declaring the theorem and check the statement (`UThmEnd` mode),
    /// and later when we are applying the theorem and have to apply a substitution (`UThm` mode).
    /// When we are applying the theorem, we have `|- e` on the main stack, and we
    /// pop that and load the expression onto the unify stack.
    /// When we are checking a theorem, we have been pushing hypotheses onto the
    /// hypothesis stack, so we pop it from there instead.
    Hyp,
}
impl std::convert::TryFrom<(u8, u32)> for UnifyCmd {
    type Error = VerifErr;
    fn try_from((cmd, data): (u8, u32)) -> Result<Self, VerifErr> {
        Ok(match cmd {
            UNIFY_TERM => UnifyCmd::Term {
                term_num: data,
                save: false,
            },
            UNIFY_TERM_SAVE => UnifyCmd::Term {
                term_num: data,
                save: true,
            },
            UNIFY_REF => UnifyCmd::Ref(data),
            UNIFY_DUMMY => {
                let sort_id = u8::try_from(data).map_err(|_| {
                    VerifErr::Msg("Failure to shrink u32 to u8 in proof_cmd try from".to_string())
                })?;
                UnifyCmd::Dummy { sort_id }
            }
            UNIFY_HYP => UnifyCmd::Hyp,
            _ => return Err(VerifErr::Msg("Unrecognized try_form in try from unifycmd".to_string())),
        })
    }
}
/// An iterator over a unify command stream.
#[derive(Debug, Clone, Copy)]
pub struct UnifyIter<'a> {
    /// The full source file.
    pub buf: &'a [u8],
    /// The index of the current declaration in the file.
    pub pos: usize,
}
impl<'a> Iterator for UnifyIter<'a> {
    type Item = Result<UnifyCmd, VerifErr>;
    fn next(&mut self) -> Option<Self::Item> {
        match try_next_cmd(self.buf, self.pos) {
            // err
            Err(e) => Some(Err(e)),
            // Exhausted
            Ok(None) => None,
            // next
            Ok(Some((stmt, rest))) => {
                self.pos = rest;
                Some(Ok(stmt))
            }            
        }
    }
}

            match maybe_cmd? {

            match maybe_cmd.map_err(|e| VerifErr::Msg(format!("{:?}", e)))? {

                UnifyCmd::Term { term_num, save } => self.unify_term(term_num, save)?,
                UnifyCmd::Dummy { sort_id } => self.unify_dummy(mode, sort_id)?,

                UnifyCmd::Term { tid, save } => self.unify_term(tid, save)?,
                UnifyCmd::Dummy(sort_id) => self.unify_dummy(mode, sort_id)?,

        }
    }
    pub fn push_ustack_rev_mmb(&mut self, items: &'b BumpVec<'b, &'b MmbItem<'b>>) {
        for elem in items.iter().rev() {
            self.ustack.push(elem)

        term_num: u32,

        term_num: TermId,

        sort_id: u8,

        sort_id: SortId,

            let bound_idx = ty.bound_digit()?;

            let bound_idx = none_err!(ty.bound_digit())?;

                make_sure!(ty.inner & bound_idx == 0);

                make_sure!(ty.into_inner() & bound_idx == 0);

use mm0b_parser::{ ProofIter, Type, ProofCmd, TYPE_BOUND_MASK };
use mm0_util::{ Modifiers, SortId, TermId, ThmId };

    try_next_cmd,

    Type,

pub const TYPE_BOUND_MASK: u64 = 1 << 63;
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum Mode {
    Def,
    Thm,
}

/// `PROOF_TERM = 0x10`: See [`ProofCmd`](super::ProofCmd).
pub const PROOF_TERM: u8 = 0x10;
/// `PROOF_TERM_SAVE = 0x11`: See [`ProofCmd`](super::ProofCmd).
pub const PROOF_TERM_SAVE: u8 = 0x11;
/// `PROOF_REF = 0x12`: See [`ProofCmd`](super::ProofCmd).
pub const PROOF_REF: u8 = 0x12;
/// `PROOF_DUMMY = 0x13`: See [`ProofCmd`](super::ProofCmd).
pub const PROOF_DUMMY: u8 = 0x13;
/// `PROOF_THM = 0x14`: See [`ProofCmd`](super::ProofCmd).
pub const PROOF_THM: u8 = 0x14;
/// `PROOF_THM_SAVE = 0x15`: See [`ProofCmd`](super::ProofCmd).
pub const PROOF_THM_SAVE: u8 = 0x15;
/// `PROOF_HYP = 0x16`: See [`ProofCmd`](super::ProofCmd).
pub const PROOF_HYP: u8 = 0x16;
/// `PROOF_CONV = 0x17`: See [`ProofCmd`](super::ProofCmd).
pub const PROOF_CONV: u8 = 0x17;
/// `PROOF_REFL = 0x18`: See [`ProofCmd`](super::ProofCmd).
pub const PROOF_REFL: u8 = 0x18;
/// `PROOF_SYMM = 0x19`: See [`ProofCmd`](super::ProofCmd).
pub const PROOF_SYMM: u8 = 0x19;
/// `PROOF_CONG = 0x1A`: See [`ProofCmd`](super::ProofCmd).
pub const PROOF_CONG: u8 = 0x1A;
/// `PROOF_UNFOLD = 0x1B`: See [`ProofCmd`](super::ProofCmd).
pub const PROOF_UNFOLD: u8 = 0x1B;
/// `PROOF_CONV_CUT = 0x1C`: See [`ProofCmd`](super::ProofCmd).
pub const PROOF_CONV_CUT: u8 = 0x1C;
/// `PROOF_CONV_REF = 0x1D`: See [`ProofCmd`](super::ProofCmd).
pub const PROOF_CONV_REF: u8 = 0x1D;
/// `PROOF_CONV_SAVE = 0x1E`: See [`ProofCmd`](super::ProofCmd).
pub const PROOF_CONV_SAVE: u8 = 0x1E;
/// `PROOF_SAVE = 0x1F`: See [`ProofCmd`](super::ProofCmd).
pub const PROOF_SAVE: u8 = 0x1F;

/// A proof command, which acts on a stack machine with the following components:
///
/// * `H: Vec<StackEl>`: a "heap" consisting of indexable elements that can be copied
///   onto the stack using [`Ref`](ProofCmd::Ref)
/// * `S: Stack<StackEl>`: The main stack, which most operations push and pop from.
/// * `HS: Vec<Expr>`: The hypothesis list, which grows only on [`Hyp`](ProofCmd::Hyp)
///   operations and collects the hypotheses of the theorem.

pub enum ProofCmd {
    /// ```text
    /// Term t: H; S, e1, ..., en --> H; S, (t e1 .. en)
    /// Save: H; S, e --> H, e; S, e
    /// TermSave t = Term t; Save:
    ///   H; S, e1, ..., en --> H, (t e1 .. en); S, (t e1 .. en)
    /// ```
    ///
    /// Pop `n` elements from the stack and allocate a new term `t` applied to those
    /// expressions. When `save` is used, the new term is also saved to the heap
    /// (this is used if the term will ever be needed more than once).
    Term {
        /** The term to construct */
        term_num: u32,
        /** True if we should save to the heap */
        save: bool,
    },
    /// ```text
    /// Ref i: H; S --> H; S, Hi
    /// ```
    /// Get the `i`-th heap element and push it on the stack.
    Ref(u32),
    /// ```text
    /// Dummy s: H; S --> H, x; S, x    alloc(x:s)
    /// ```
    /// Allocate a new variable `x` of sort `s`, and push it to the stack and the heap.
    Dummy { sort_num: u8 },
    /// ```text
    /// Thm T: H; S, e1, ..., en, e --> H; S', |- e
    ///   (where Unify(T): S; e1, ... en; e --> S'; H'; .)
    /// Save: H; S, |- e --> H, |- e; S, |- e
    /// ```
    /// Pop `n` elements from the stack and put them on the unify heap, then call the
    /// unifier for `T` with `e` as the target. The unifier will pop additional
    /// proofs from the stack if the UHyp command is used, and when it is done,
    /// the conclusion is pushed as a proven statement.
    ///
    /// When Save is used, the proven statement is also saved to the heap.
    Thm {
        /** The theorem to apply */
        thm_num: u32,
        /** True if we should save to the heap */
        save: bool,
    },
    /// ```text
    /// Hyp: HS; H; S, e --> HS, e; H, |- e; S
    /// ```
    /// This command means that we are finished constructing the expression `e`
    /// which denotes a statement, and wish to assume it as a hypothesis.
    /// Push `e` to the hypothesis stack, and push `|- e` to the heap.
    Hyp,
    /// ```text
    /// Conv: S, e1, |- e2 --> S, |- e1, e1 =?= e2
    /// ```
    /// Pop `e1` and `|- e2`, and push `|- e1`, guarded by a convertibility obligation
    /// `e1 =?= e2`.
    Conv,
    /// ```text
    /// Refl: S, e =?= e --> S
    /// ```
    /// Pop a convertibility obligation where the two sides are equal.
    Refl,
    /// ```text
    /// Symm: S, e1 =?= e2 --> S, e2 =?= e1
    /// ```
    /// Swap the direction of a convertibility obligation.
    Sym,
    /// ```text
    /// Cong: S, (t e1 ... en) =?= (t e1' ... en') --> S, en =?= en', ..., e1 =?= e1'
    /// ```
    /// Pop a convertibility obligation for two term expressions, and
    /// push convertibility obligations for all the parts.
    /// The parts are pushed in reverse order so that they are dealt with
    /// in declaration order in the proof stream.
    Cong,
    /// ```text
    /// Unfold: S, (t e1 ... en) =?= e', (t e1 ... en), e --> S, e =?= e'
    ///   (where Unify(t): e1, ..., en; e --> H'; .)
    /// ```
    /// Pop terms `(t e1 ... en)`, `e` from the stack and run the unifier for `t`
    /// (which should be a definition) to make sure that `(t e1 ... en)` unfolds to `e`.
    /// Then pop `(t e1 ... en) =?= e'` and push `e =?= e'`.
    Unfold,
    /// ```text
    /// ConvCut: S, e1 =?= e2 --> S, e1 = e2, e1 =?= e2
    /// ```
    /// Pop a convertibility obligation `e1 =?= e2`, and
    /// push a convertability assertion `e1 = e2` guarded by `e1 =?= e2`.
    ConvCut,
    /// ```text
    /// ConvRef i: H; S, e1 =?= e2 --> H; S   (where Hi is e1 = e2)
    /// ```
    /// Pop a convertibility obligation `e1 =?= e2`, where `e1 = e2` is
    /// `i`-th on the heap.
    ConvRef(u32),
    /// ```text
    /// ConvSave: H; S, e1 = e2 --> H, e1 = e2; S
    /// ```
    /// Pop a convertibility proof `e1 = e2` and save it to the heap.
    ConvSave,
    /// ```text
    /// Save: H; S, s --> H, s; S, s
    /// ```
    /// Save the outline of the stack to the heap, without popping it.
    Save,
}
impl std::convert::TryFrom<(u8, u32)> for ProofCmd {
    type Error = VerifErr;
    fn try_from((cmd, data): (u8, u32)) -> Result<Self, Self::Error> {
        Ok(match cmd {
            PROOF_TERM => ProofCmd::Term {
                term_num: data,
                save: false,
            },
            PROOF_TERM_SAVE => ProofCmd::Term {
                term_num: data,
                save: true,
            },
            PROOF_REF => ProofCmd::Ref(data),
            PROOF_DUMMY => {
                let sort_num = u8::try_from(data).map_err(|_| {
                    VerifErr::Msg("Failure to shrink u32 to u8 in proof_cmd try from".to_string())
                })?;
                ProofCmd::Dummy { sort_num }
            }
            PROOF_THM => ProofCmd::Thm {
                thm_num: data,
                save: false,
            },
            PROOF_THM_SAVE => ProofCmd::Thm {
                thm_num: data,
                save: true,
            },
            PROOF_HYP => ProofCmd::Hyp,
            PROOF_CONV => ProofCmd::Conv,
            PROOF_REFL => ProofCmd::Refl,
            PROOF_SYMM => ProofCmd::Sym,
            PROOF_CONG => ProofCmd::Cong,
            PROOF_UNFOLD => ProofCmd::Unfold,
            PROOF_CONV_CUT => ProofCmd::ConvCut,
            PROOF_CONV_REF => ProofCmd::ConvRef(data),
            PROOF_CONV_SAVE => ProofCmd::ConvSave,
            PROOF_SAVE => ProofCmd::Save,
            owise => {
                println!("Failed to convert {:?}\n", owise);
                return Err(VerifErr::Msg("try_from for ProofCmd failed match".to_string()));
            }
        })
    }
}
/// An iterator over a proof command stream.
#[derive(Debug, Clone, Copy)]
pub struct ProofIter<'a> {
    /// The full source file, but trimmed such that the end
    /// is the expected end of the proof stream. The final call to `next`
    /// will fail if it does not hit the expected end when the
    /// proof stream runs out.
    pub buf: &'a [u8],
    /// The index of the current proof command in the file.
    pub pos: usize,
    /// Mark `ends_at` instead of giving ProofIter a truncated slice just so
    /// the behvaior wrt `try_next_cmd` is identical.
    pub ends_at: usize,
}
impl<'a> ProofIter<'a> {
    /// True if this iterator is "null", meaning that it has zero commands.
    /// This is not the same as being empty, which happens when there is one command
    /// which is the terminating `CMD_END` command.
    pub fn is_null(&self) -> bool {
        //self.buf.len() == self.pos
        self.pos == self.ends_at
    }
}
impl<'a> Iterator for ProofIter<'a> {
    type Item = Result<ProofCmd, VerifErr>;
    fn next(&mut self) -> Option<Self::Item> {
        match try_next_cmd(self.buf, self.pos) {
            // An actual error.
            Err(e) => Some(Err(e)),
            // `try_next_cmd` got `Ok(None)` by receiving a 0 command at the correct position
            Ok(None) if self.ends_at == self.pos + 1 => None,
            // `try_next_cmd` got `Ok(None)` by receiving a 0 command at the WRONG position
            Ok(None) => Some(Err(VerifErr::Msg(format!("Proof iter err @ {}", self.pos)))),
            // `try_next_cmd` parsed a new command.
            Ok(Some((stmt, rest))) => {
                self.pos = rest;
                Some(Ok(stmt))
            }
        }
    }

pub enum Mode {
    Def,
    Thm,

            match maybe_cmd? {

            match maybe_cmd.map_err(|e| VerifErr::Msg(format!("{:?}", e)))? {

                ProofCmd::Dummy { sort_num } => self.proof_dummy(sort_num)?,
                ProofCmd::Term { term_num, save } => self.proof_term(mode, term_num, save)?,
                ProofCmd::Thm { thm_num, save } => self.proof_thm(thm_num, save)?,

                ProofCmd::Dummy(sort_num) => self.proof_dummy(sort_num)?,
                ProofCmd::Term { tid, save } => self.proof_term(mode, tid, save)?,
                ProofCmd::Thm { tid, save } => self.proof_thm(tid, save)?,

                ProofCmd::ConvRef(i) => self.proof_conv_ref(i)?,

                ProofCmd::Sorry => self.proof_sorry()?,

        let heap_elem = *&self.heap[i as usize];
        Ok(self.stack.push(heap_elem))

        match none_err!(self.heap.get(i as usize).copied())? {
            MmbItem::Conv(c1, c2) => {
                let stack_coconv = none_err!(self.stack.pop())?;
                if let MmbItem::CoConv(cc1, cc2) = stack_coconv {
                    make_sure!(c1 == cc1);
                    Ok(make_sure!(c2 == cc2))
                } else {
                    return Err(VerifErr::Unreachable(file!(), line!()));
                }
            }
            heap_elem => Ok(self.stack.push(heap_elem))
        }

    fn proof_dummy(&mut self, sort_num: u8) -> Res<()> {
        make_sure!(sort_num < self.outline.header.num_sorts);
        make_sure!(self.outline.get_sort_mods(sort_num as usize).unwrap().inner & crate::mmb::SORT_STRICT == 0);

    fn proof_dummy(&mut self, sort_num: SortId) -> Res<()> {
        make_sure!(sort_num.into_inner() < self.outline.file_view.mmb.header.num_sorts);
        make_sure!(!(self.outline.file_view.mmb_sort_mods(sort_num)?.contains(Modifiers::STRICT)));

        let ty = Type { inner: TYPE_BOUND_MASK | ((sort_num as u64) << 56) | self.take_next_bv() };

        let ty = Type::from(TYPE_BOUND_MASK | ((sort_num.into_inner() as u64) << 56) | self.take_next_bv());

        term_num: u32,

        term_num: TermId,

        make_sure!(term_num < self.outline.header.num_terms);
        let termref = self.outline.get_term_by_num(term_num)?;

        make_sure!(term_num.into_inner() < self.outline.file_view.mmb.header.num_terms.get());
        let termref = none_err!(self.outline.file_view.mmb.term(term_num))?;

        let drain_from = self.stack.len() - (termref.num_args_no_ret() as usize);

        let drain_from = self.stack.len() - (termref.args().len());

        let all_args = || { termref.args_no_ret().zip(stack_args.iter()) };

        let all_args = || { termref.args().iter().zip(stack_args.iter()) };

            if sig.is_bound() {

            if sig.bound() {

            make_sure!(sorts_compatible(stack_arg.get_ty()?, sig_arg)) 

            make_sure!(sorts_compatible(stack_arg.get_ty()?, *sig_arg)) 

        let mut new_type_accum = Type::new_with_sort(termref.sort());

        let mut new_type_accum = Type::new_of_sort(termref.sort().into_inner());

        for (sig_unbound, stack_arg) in all_args().filter(|(sig, _)| !sig.is_bound()) {

        for (sig_unbound, stack_arg) in all_args().filter(|(sig, _)| !sig.bound()) {

                    if sig_unbound.depends_on_((idx + 1) as u64) {

                    if sig_unbound.depends_on((idx) as u64) {

                if termref.ret().depends_on_((idx + 1) as u64) {

                if termref.ret().depends_on((idx) as u64) {

        let drain = self.stack.drain((self.stack.len() - (termref.num_args_no_ret() as usize))..);

        let drain = self.stack.drain((self.stack.len() - (termref.args().len()))..);

        thm_num: u32,

        thm_num: ThmId,

        make_sure!(thm_num < self.outline.header.num_thms);
        let thmref = self.outline.get_assert_by_num(thm_num)?;

        make_sure!(thm_num.into_inner() < self.outline.file_view.mmb.header.num_thms.get());
        let thmref = none_err!(self.outline.file_view.mmb.thm(thm_num))?;

        let bound_by_sig = sig_args.zip(stack_args).enumerate().filter(|(_, (sig, _))| sig.is_bound());

        let bound_by_sig = sig_args.iter().zip(stack_args).enumerate().filter(|(_, (sig, _))| sig.bound());

        for (sig_a, stack_a) in  sig_args.zip(stack_args).filter(|(sig, _)| !sig.is_bound()) {