mmb_types/
opcode.rs

1const OPCODE_END: u8 = 0x00;
2const OPCODE_STMT_AXIOM: u8 = 0x02;
3const OPCODE_STMT_SORT: u8 = 0x04;
4const OPCODE_STMT_TERM_DEF: u8 = 0x05;
5const OPCODE_STMT_THM: u8 = 0x06;
6const OPCODE_STMT_LOCAL_DEF: u8 = 0x0D;
7const OPCODE_STMT_LOCAL_TERM: u8 = 0x0E;
8const OPCODE_PROOF_TERM: u8 = 0x10;
9const OPCODE_PROOF_TERM_SAVE: u8 = 0x11;
10const OPCODE_PROOF_REF: u8 = 0x12;
11const OPCODE_PROOF_DUMMY: u8 = 0x13;
12const OPCODE_PROOF_THM: u8 = 0x14;
13const OPCODE_PROOF_THM_SAVE: u8 = 0x15;
14const OPCODE_PROOF_HYP: u8 = 0x16;
15const OPCODE_PROOF_CONV: u8 = 0x17;
16const OPCODE_PROOF_REFL: u8 = 0x18;
17const OPCODE_PROOF_SYMM: u8 = 0x19;
18const OPCODE_PROOF_CONG: u8 = 0x1A;
19const OPCODE_PROOF_UNFOLD: u8 = 0x1B;
20const OPCODE_PROOF_CONV_CUT: u8 = 0x1C;
21const OPCODE_PROOF_CONV_REF: u8 = 0x1D;
22const OPCODE_PROOF_CONV_SAVE: u8 = 0x1E;
23const OPCODE_PROOF_SAVE: u8 = 0x1F;
24const OPCODE_UNIFY_TERM: u8 = 0x30;
25const OPCODE_UNIFY_TERM_SAVE: u8 = 0x31;
26const OPCODE_UNIFY_REF: u8 = 0x32;
27const OPCODE_UNIFY_DUMMY: u8 = 0x33;
28const OPCODE_UNIFY_HYP: u8 = 0x36;
29
30#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
31#[repr(u8)]
32pub enum Opcode {
33    End = OPCODE_END,
34    StAxiom = OPCODE_STMT_AXIOM,
35    StSort = OPCODE_STMT_SORT,
36    StTermDef = OPCODE_STMT_TERM_DEF,
37    StThm = OPCODE_STMT_THM,
38    StLocalDef = OPCODE_STMT_LOCAL_DEF,
39    StLocalTerm = OPCODE_STMT_LOCAL_TERM,
40    PrTerm = OPCODE_PROOF_TERM,
41    PrTermSave = OPCODE_PROOF_TERM_SAVE,
42    PrRef = OPCODE_PROOF_REF,
43    PrDummy = OPCODE_PROOF_DUMMY,
44    PrThm = OPCODE_PROOF_THM,
45    PrThmSave = OPCODE_PROOF_THM_SAVE,
46    PrHyp = OPCODE_PROOF_HYP,
47    PrConv = OPCODE_PROOF_CONV,
48    PrRefl = OPCODE_PROOF_REFL,
49    PrSymm = OPCODE_PROOF_SYMM,
50    PrCong = OPCODE_PROOF_CONG,
51    PrUnfold = OPCODE_PROOF_UNFOLD,
52    PrConvCut = OPCODE_PROOF_CONV_CUT,
53    PrConvRef = OPCODE_PROOF_CONV_REF,
54    PrConvSave = OPCODE_PROOF_CONV_SAVE,
55    PrSave = OPCODE_PROOF_SAVE,
56    UnTerm = OPCODE_UNIFY_TERM,
57    UnTermSave = OPCODE_UNIFY_TERM_SAVE,
58    UnRef = OPCODE_UNIFY_REF,
59    UnDummy = OPCODE_UNIFY_DUMMY,
60    UnHyp = OPCODE_UNIFY_HYP,
61}
62
63#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
64pub struct Command<T> {
65    pub opcode: T,
66    pub operand: u32,
67}
68
69impl<T: Copy> From<&Command<T>> for Command<T> {
70    fn from(c: &Command<T>) -> Command<T> {
71        *c
72    }
73}
74
75#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
76#[repr(u8)]
77pub enum Statement {
78    End = OPCODE_END,
79    Axiom = OPCODE_STMT_AXIOM,
80    Sort = OPCODE_STMT_SORT,
81    TermDef = OPCODE_STMT_TERM_DEF,
82    Thm = OPCODE_STMT_THM,
83    LocalDef = OPCODE_STMT_LOCAL_DEF,
84    LocalTerm = OPCODE_STMT_LOCAL_TERM,
85}
86
87#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
88#[repr(u8)]
89pub enum Unify {
90    End = OPCODE_END,
91    Term = OPCODE_UNIFY_TERM,
92    TermSave = OPCODE_UNIFY_TERM_SAVE,
93    Ref = OPCODE_UNIFY_REF,
94    Dummy = OPCODE_UNIFY_DUMMY,
95    Hyp = OPCODE_UNIFY_HYP,
96}
97
98#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
99#[repr(u8)]
100pub enum Proof {
101    End = OPCODE_END,
102    Term = OPCODE_PROOF_TERM,
103    TermSave = OPCODE_PROOF_TERM_SAVE,
104    Ref = OPCODE_PROOF_REF,
105    Dummy = OPCODE_PROOF_DUMMY,
106    Thm = OPCODE_PROOF_THM,
107    ThmSave = OPCODE_PROOF_THM_SAVE,
108    Hyp = OPCODE_PROOF_HYP,
109    Conv = OPCODE_PROOF_CONV,
110    Refl = OPCODE_PROOF_REFL,
111    Symm = OPCODE_PROOF_SYMM,
112    Cong = OPCODE_PROOF_CONG,
113    Unfold = OPCODE_PROOF_UNFOLD,
114    ConvCut = OPCODE_PROOF_CONV_CUT,
115    ConvRef = OPCODE_PROOF_CONV_REF,
116    ConvSave = OPCODE_PROOF_CONV_SAVE,
117    Save = OPCODE_PROOF_SAVE,
118}
119
120use core::convert::TryFrom;
121
122impl TryFrom<u8> for Opcode {
123    type Error = ();
124
125    fn try_from(value: u8) -> Result<Opcode, ()> {
126        use Opcode::*;
127        match value {
128            OPCODE_END => Ok(End),
129            OPCODE_STMT_AXIOM => Ok(StAxiom),
130            OPCODE_STMT_SORT => Ok(StSort),
131            OPCODE_STMT_TERM_DEF => Ok(StTermDef),
132            OPCODE_STMT_THM => Ok(StThm),
133            OPCODE_STMT_LOCAL_DEF => Ok(StLocalDef),
134            OPCODE_STMT_LOCAL_TERM => Ok(StLocalTerm),
135            OPCODE_PROOF_TERM => Ok(PrTerm),
136            OPCODE_PROOF_TERM_SAVE => Ok(PrTermSave),
137            OPCODE_PROOF_REF => Ok(PrRef),
138            OPCODE_PROOF_DUMMY => Ok(PrDummy),
139            OPCODE_PROOF_THM => Ok(PrThm),
140            OPCODE_PROOF_THM_SAVE => Ok(PrThmSave),
141            OPCODE_PROOF_HYP => Ok(PrHyp),
142            OPCODE_PROOF_CONV => Ok(PrConv),
143            OPCODE_PROOF_REFL => Ok(PrRefl),
144            OPCODE_PROOF_SYMM => Ok(PrSymm),
145            OPCODE_PROOF_CONG => Ok(PrCong),
146            OPCODE_PROOF_UNFOLD => Ok(PrUnfold),
147            OPCODE_PROOF_CONV_CUT => Ok(PrConvCut),
148            OPCODE_PROOF_CONV_REF => Ok(PrConvRef),
149            OPCODE_PROOF_CONV_SAVE => Ok(PrConvSave),
150            OPCODE_PROOF_SAVE => Ok(PrSave),
151            OPCODE_UNIFY_TERM => Ok(UnTerm),
152            OPCODE_UNIFY_TERM_SAVE => Ok(UnTermSave),
153            OPCODE_UNIFY_REF => Ok(UnRef),
154            OPCODE_UNIFY_DUMMY => Ok(UnDummy),
155            OPCODE_UNIFY_HYP => Ok(UnHyp),
156            _ => Err(()),
157        }
158    }
159}
160
161impl TryFrom<u8> for Statement {
162    type Error = ();
163
164    fn try_from(value: u8) -> Result<Statement, ()> {
165        use Statement::*;
166        match value {
167            OPCODE_END => Ok(End),
168            OPCODE_STMT_AXIOM => Ok(Axiom),
169            OPCODE_STMT_SORT => Ok(Sort),
170            OPCODE_STMT_TERM_DEF => Ok(TermDef),
171            OPCODE_STMT_THM => Ok(Thm),
172            OPCODE_STMT_LOCAL_DEF => Ok(LocalDef),
173            OPCODE_STMT_LOCAL_TERM => Ok(LocalTerm),
174            _ => Err(()),
175        }
176    }
177}
178
179impl TryFrom<u8> for Unify {
180    type Error = ();
181
182    fn try_from(value: u8) -> Result<Unify, ()> {
183        use Unify::*;
184        match value {
185            OPCODE_END => Ok(End),
186            OPCODE_UNIFY_TERM => Ok(Term),
187            OPCODE_UNIFY_TERM_SAVE => Ok(TermSave),
188            OPCODE_UNIFY_REF => Ok(Ref),
189            OPCODE_UNIFY_DUMMY => Ok(Dummy),
190            OPCODE_UNIFY_HYP => Ok(Hyp),
191            _ => Err(()),
192        }
193    }
194}
195
196impl TryFrom<u8> for Proof {
197    type Error = ();
198
199    fn try_from(value: u8) -> Result<Proof, ()> {
200        use Proof::*;
201        match value {
202            OPCODE_END => Ok(End),
203            OPCODE_PROOF_TERM => Ok(Term),
204            OPCODE_PROOF_TERM_SAVE => Ok(TermSave),
205            OPCODE_PROOF_REF => Ok(Ref),
206            OPCODE_PROOF_DUMMY => Ok(Dummy),
207            OPCODE_PROOF_THM => Ok(Thm),
208            OPCODE_PROOF_THM_SAVE => Ok(ThmSave),
209            OPCODE_PROOF_HYP => Ok(Hyp),
210            OPCODE_PROOF_CONV => Ok(Conv),
211            OPCODE_PROOF_REFL => Ok(Refl),
212            OPCODE_PROOF_SYMM => Ok(Symm),
213            OPCODE_PROOF_CONG => Ok(Cong),
214            OPCODE_PROOF_UNFOLD => Ok(Unfold),
215            OPCODE_PROOF_CONV_CUT => Ok(ConvCut),
216            OPCODE_PROOF_CONV_REF => Ok(ConvRef),
217            OPCODE_PROOF_CONV_SAVE => Ok(ConvSave),
218            OPCODE_PROOF_SAVE => Ok(Save),
219            _ => Err(()),
220        }
221    }
222}
mmb_types/opcode.rs

mmb_types/
opcode.rs
