mmb_parser/
visitor.rs

1use crate::opcode::{Command, Proof, Statement, Unify};
2
3pub trait UnifyStream {
4    fn push(&mut self, command: Command<Unify>);
5
6    fn done(&self) -> (usize, usize);
7}
8
9pub trait ProofStream {
10    fn push(&mut self, command: Command<Proof>);
11
12    fn done(&self) -> (usize, usize);
13}
14
15pub trait Visitor<'a> {
16    type Binder: From<u64>;
17    type Sort: From<u8>;
18    type Statement: From<Statement>;
19    type Unify: UnifyStream;
20    type Proof: ProofStream;
21
22    fn parse_sort(&mut self, sort: Self::Sort);
23
24    fn parse_statement(
25        &mut self,
26        statement: Self::Statement,
27        offset: usize,
28        slice: &'a [u8],
29        proof: Option<(usize, usize)>,
30    );
31
32    fn try_reserve_binder_slice(&mut self, nr: usize) -> Option<(&mut [Self::Binder], usize)>;
33
34    fn start_unify_stream(&mut self) -> &mut Self::Unify;
35
36    fn start_proof_stream(&mut self) -> &mut Self::Proof;
37
38    fn parse_term(
39        &mut self,
40        sort_idx: u8,
41        binders: (usize, usize),
42        ret_ty: Self::Binder,
43        unify: &'a [u8],
44        unify_indices: (usize, usize),
45    );
46
47    fn parse_theorem(
48        &mut self,
49        binders: (usize, usize),
50        unify: &'a [u8],
51        unify_indices: (usize, usize),
52    );
53}
mmb_parser/visitor.rs

mmb_parser/
visitor.rs
