const OPCODE_END: u8 = 0x00;
const OPCODE_STMT_AXIOM: u8 = 0x02;
const OPCODE_STMT_SORT: u8 = 0x04;
const OPCODE_STMT_TERM_DEF: u8 = 0x05;
const OPCODE_STMT_THM: u8 = 0x06;
const OPCODE_STMT_LOCAL_DEF: u8 = 0x0D;
const OPCODE_STMT_LOCAL_TERM: u8 = 0x0E;
const OPCODE_PROOF_TERM: u8 = 0x10;
const OPCODE_PROOF_TERM_SAVE: u8 = 0x11;
const OPCODE_PROOF_REF: u8 = 0x12;
const OPCODE_PROOF_DUMMY: u8 = 0x13;
const OPCODE_PROOF_THM: u8 = 0x14;
const OPCODE_PROOF_THM_SAVE: u8 = 0x15;
const OPCODE_PROOF_HYP: u8 = 0x16;
const OPCODE_PROOF_CONV: u8 = 0x17;
const OPCODE_PROOF_REFL: u8 = 0x18;
const OPCODE_PROOF_SYMM: u8 = 0x19;
const OPCODE_PROOF_CONG: u8 = 0x1A;
const OPCODE_PROOF_UNFOLD: u8 = 0x1B;
const OPCODE_PROOF_CONV_CUT: u8 = 0x1C;
const OPCODE_PROOF_CONV_REF: u8 = 0x1D;
const OPCODE_PROOF_CONV_SAVE: u8 = 0x1E;
const OPCODE_PROOF_SAVE: u8 = 0x1F;
const OPCODE_UNIFY_TERM: u8 = 0x30;
const OPCODE_UNIFY_TERM_SAVE: u8 = 0x31;
const OPCODE_UNIFY_REF: u8 = 0x32;
const OPCODE_UNIFY_DUMMY: u8 = 0x33;
const OPCODE_UNIFY_HYP: u8 = 0x36;
#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
#[repr(u8)]
pub enum Opcode {
End = OPCODE_END,
StAxiom = OPCODE_STMT_AXIOM,
StSort = OPCODE_STMT_SORT,
StTermDef = OPCODE_STMT_TERM_DEF,
StThm = OPCODE_STMT_THM,
StLocalDef = OPCODE_STMT_LOCAL_DEF,
StLocalTerm = OPCODE_STMT_LOCAL_TERM,
PrTerm = OPCODE_PROOF_TERM,
PrTermSave = OPCODE_PROOF_TERM_SAVE,
PrRef = OPCODE_PROOF_REF,
PrDummy = OPCODE_PROOF_DUMMY,
PrThm = OPCODE_PROOF_THM,
PrThmSave = OPCODE_PROOF_THM_SAVE,
PrHyp = OPCODE_PROOF_HYP,
PrConv = OPCODE_PROOF_CONV,
PrRefl = OPCODE_PROOF_REFL,
PrSymm = OPCODE_PROOF_SYMM,
PrCong = OPCODE_PROOF_CONG,
PrUnfold = OPCODE_PROOF_UNFOLD,
PrConvCut = OPCODE_PROOF_CONV_CUT,
PrConvRef = OPCODE_PROOF_CONV_REF,
PrConvSave = OPCODE_PROOF_CONV_SAVE,
PrSave = OPCODE_PROOF_SAVE,
UnTerm = OPCODE_UNIFY_TERM,
UnTermSave = OPCODE_UNIFY_TERM_SAVE,
UnRef = OPCODE_UNIFY_REF,
UnDummy = OPCODE_UNIFY_DUMMY,
UnHyp = OPCODE_UNIFY_HYP,
}
#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
pub struct Command<T> {
pub opcode: T,
pub operand: u32,
}
impl<T: Copy> From<&Command<T>> for Command<T> {
fn from(c: &Command<T>) -> Command<T> {
*c
}
}
#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
#[repr(u8)]
pub enum Statement {
End = OPCODE_END,
Axiom = OPCODE_STMT_AXIOM,
Sort = OPCODE_STMT_SORT,
TermDef = OPCODE_STMT_TERM_DEF,
Thm = OPCODE_STMT_THM,
LocalDef = OPCODE_STMT_LOCAL_DEF,
LocalTerm = OPCODE_STMT_LOCAL_TERM,
}
#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
#[repr(u8)]
pub enum Unify {
End = OPCODE_END,
Term = OPCODE_UNIFY_TERM,
TermSave = OPCODE_UNIFY_TERM_SAVE,
Ref = OPCODE_UNIFY_REF,
Dummy = OPCODE_UNIFY_DUMMY,
Hyp = OPCODE_UNIFY_HYP,
}
#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
#[repr(u8)]
pub enum Proof {
End = OPCODE_END,
Term = OPCODE_PROOF_TERM,
TermSave = OPCODE_PROOF_TERM_SAVE,
Ref = OPCODE_PROOF_REF,
Dummy = OPCODE_PROOF_DUMMY,
Thm = OPCODE_PROOF_THM,
ThmSave = OPCODE_PROOF_THM_SAVE,
Hyp = OPCODE_PROOF_HYP,
Conv = OPCODE_PROOF_CONV,
Refl = OPCODE_PROOF_REFL,
Symm = OPCODE_PROOF_SYMM,
Cong = OPCODE_PROOF_CONG,
Unfold = OPCODE_PROOF_UNFOLD,
ConvCut = OPCODE_PROOF_CONV_CUT,
ConvRef = OPCODE_PROOF_CONV_REF,
ConvSave = OPCODE_PROOF_CONV_SAVE,
Save = OPCODE_PROOF_SAVE,
}
use core::convert::TryFrom;
impl TryFrom<u8> for Opcode {
type Error = ();
fn try_from(value: u8) -> Result<Opcode, ()> {
use Opcode::*;
match value {
OPCODE_END => Ok(End),
OPCODE_STMT_AXIOM => Ok(StAxiom),
OPCODE_STMT_SORT => Ok(StSort),
OPCODE_STMT_TERM_DEF => Ok(StTermDef),
OPCODE_STMT_THM => Ok(StThm),
OPCODE_STMT_LOCAL_DEF => Ok(StLocalDef),
OPCODE_STMT_LOCAL_TERM => Ok(StLocalTerm),
OPCODE_PROOF_TERM => Ok(PrTerm),
OPCODE_PROOF_TERM_SAVE => Ok(PrTermSave),
OPCODE_PROOF_REF => Ok(PrRef),
OPCODE_PROOF_DUMMY => Ok(PrDummy),
OPCODE_PROOF_THM => Ok(PrThm),
OPCODE_PROOF_THM_SAVE => Ok(PrThmSave),
OPCODE_PROOF_HYP => Ok(PrHyp),
OPCODE_PROOF_CONV => Ok(PrConv),
OPCODE_PROOF_REFL => Ok(PrRefl),
OPCODE_PROOF_SYMM => Ok(PrSymm),
OPCODE_PROOF_CONG => Ok(PrCong),
OPCODE_PROOF_UNFOLD => Ok(PrUnfold),
OPCODE_PROOF_CONV_CUT => Ok(PrConvCut),
OPCODE_PROOF_CONV_REF => Ok(PrConvRef),
OPCODE_PROOF_CONV_SAVE => Ok(PrConvSave),
OPCODE_PROOF_SAVE => Ok(PrSave),
OPCODE_UNIFY_TERM => Ok(UnTerm),
OPCODE_UNIFY_TERM_SAVE => Ok(UnTermSave),
OPCODE_UNIFY_REF => Ok(UnRef),
OPCODE_UNIFY_DUMMY => Ok(UnDummy),
OPCODE_UNIFY_HYP => Ok(UnHyp),
_ => Err(()),
}
}
}
impl TryFrom<u8> for Statement {
type Error = ();
fn try_from(value: u8) -> Result<Statement, ()> {
use Statement::*;
match value {
OPCODE_END => Ok(End),
OPCODE_STMT_AXIOM => Ok(Axiom),
OPCODE_STMT_SORT => Ok(Sort),
OPCODE_STMT_TERM_DEF => Ok(TermDef),
OPCODE_STMT_THM => Ok(Thm),
OPCODE_STMT_LOCAL_DEF => Ok(LocalDef),
OPCODE_STMT_LOCAL_TERM => Ok(LocalTerm),
_ => Err(()),
}
}
}
impl TryFrom<u8> for Unify {
type Error = ();
fn try_from(value: u8) -> Result<Unify, ()> {
use Unify::*;
match value {
OPCODE_END => Ok(End),
OPCODE_UNIFY_TERM => Ok(Term),
OPCODE_UNIFY_TERM_SAVE => Ok(TermSave),
OPCODE_UNIFY_REF => Ok(Ref),
OPCODE_UNIFY_DUMMY => Ok(Dummy),
OPCODE_UNIFY_HYP => Ok(Hyp),
_ => Err(()),
}
}
}
impl TryFrom<u8> for Proof {
type Error = ();
fn try_from(value: u8) -> Result<Proof, ()> {
use Proof::*;
match value {
OPCODE_END => Ok(End),
OPCODE_PROOF_TERM => Ok(Term),
OPCODE_PROOF_TERM_SAVE => Ok(TermSave),
OPCODE_PROOF_REF => Ok(Ref),
OPCODE_PROOF_DUMMY => Ok(Dummy),
OPCODE_PROOF_THM => Ok(Thm),
OPCODE_PROOF_THM_SAVE => Ok(ThmSave),
OPCODE_PROOF_HYP => Ok(Hyp),
OPCODE_PROOF_CONV => Ok(Conv),
OPCODE_PROOF_REFL => Ok(Refl),
OPCODE_PROOF_SYMM => Ok(Symm),
OPCODE_PROOF_CONG => Ok(Cong),
OPCODE_PROOF_UNFOLD => Ok(Unfold),
OPCODE_PROOF_CONV_CUT => Ok(ConvCut),
OPCODE_PROOF_CONV_REF => Ok(ConvRef),
OPCODE_PROOF_CONV_SAVE => Ok(ConvSave),
OPCODE_PROOF_SAVE => Ok(Save),
_ => Err(()),
}
}
}