trivial_compiler/
lib.rs

1pub use mmb_types::opcode;
2
3#[derive(Copy, Clone)]
4enum Ptr {
5    Ref { id: u32 },
6    Term { id: u32 },
7}
8
9#[derive(Debug, Copy, Clone)]
10pub enum ConversionError {
11    InvalidTermIndex,
12}
13
14#[derive(Copy, Clone)]
15struct HeapAlloc(Ptr);
16
17#[derive(Debug, Copy, Clone)]
18enum Cmd {
19    Ref { id: u32 },
20    Term { id: u32 },
21    TermSave { id: u32 },
22    Dummy { sort: u32 },
23    Hyp,
24}
25
26struct Term {
27    id: u32,
28    nr_args: u32,
29    ptr_args: usize,
30}
31
32fn term(
33    id: u32,
34    nr_args: u32,
35    data: &mut Vec<Term>,
36    args: &mut Vec<Ptr>,
37    stack: &mut Vec<Ptr>,
38) -> Ptr {
39    let ptr_args = args.len();
40    let ptr = data.len();
41
42    data.push(Term {
43        id,
44        nr_args,
45        ptr_args,
46    });
47
48    let len = stack.len();
49    let diff = len - nr_args as usize;
50    let last_elements = stack.get(diff..).unwrap();
51
52    args.extend(last_elements);
53
54    stack.truncate(diff);
55
56    Ptr::Term { id: ptr as u32 }
57}
58
59pub fn unify_to_proof<'a, T, F>(
60    init_vars: u32,
61    unify_stream: T,
62    get_nr_args: F,
63) -> Result<Vec<opcode::Command<opcode::Proof>>, ConversionError>
64where
65    T: IntoIterator<Item = &'a opcode::Command<opcode::Unify>>,
66    F: Fn(u32) -> Option<u32>,
67{
68    let mut command_stack = Vec::new();
69    let mut counter = init_vars;
70
71    for command in unify_stream {
72        use opcode::Unify;
73        match command.opcode {
74            Unify::TermSave => {
75                counter += 1;
76            }
77            Unify::Dummy => {
78                counter += 1;
79            }
80            Unify::End => {
81                break;
82            }
83            _ => {}
84        }
85
86        command_stack.push(command);
87    }
88
89    let mut data = Vec::new();
90    let mut args: Vec<Ptr> = Vec::new();
91    let mut stack = Vec::new();
92    let mut heap_translate = Vec::new();
93
94    let mut buffer = Vec::new();
95
96    while let Some(command) = command_stack.pop() {
97        use opcode::Unify;
98        match command.opcode {
99            Unify::End => {
100                //
101            }
102            Unify::Ref => {
103                stack.push(Ptr::Ref {
104                    id: command.operand,
105                });
106            }
107            Unify::Term => {
108                let nr_args =
109                    get_nr_args(command.operand).ok_or(ConversionError::InvalidTermIndex)?;
110                let ret = term(command.operand, nr_args, &mut data, &mut args, &mut stack);
111
112                stack.push(ret);
113            }
114            Unify::TermSave => {
115                let nr_args =
116                    get_nr_args(command.operand).ok_or(ConversionError::InvalidTermIndex)?;
117                let ret = term(command.operand, nr_args, &mut data, &mut args, &mut stack);
118
119                let ref_var = counter;
120                counter -= 1;
121
122                stack.push(Ptr::Ref { id: ref_var });
123                heap_translate.push((ref_var, HeapAlloc(ret)));
124            }
125            Unify::Dummy => {
126                let ref_var = counter;
127                counter -= 1;
128
129                let ret = Ptr::Ref {
130                    id: command.operand,
131                };
132
133                stack.push(Ptr::Ref { id: ref_var });
134                heap_translate.push((ref_var, HeapAlloc(ret)));
135            }
136            Unify::Hyp => {
137                expand_preorder(stack.iter(), &mut buffer, &data, &args);
138                stack.clear();
139                buffer.push(Cmd::Hyp);
140            }
141        }
142    }
143
144    expand_preorder(stack.iter(), &mut buffer, &data, &args);
145    stack.clear();
146
147    let mut temp = Vec::new();
148
149    for i in buffer {
150        let translate = heap_translate.last();
151
152        match (i, translate) {
153            (Cmd::Ref { id }, Some((trans_id, HeapAlloc(value)))) => {
154                if id == *trans_id {
155                    match value {
156                        Ptr::Ref { id } => temp.push(Cmd::Dummy { sort: *id }),
157                        Ptr::Term { id } => {
158                            let term = data.get(*id as usize).unwrap();
159                            let ptrs = args
160                                .get(term.ptr_args..(term.ptr_args + term.nr_args as usize))
161                                .unwrap();
162
163                            expand_preorder(ptrs.iter().rev(), &mut temp, &data, &args);
164
165                            temp.push(Cmd::TermSave { id: term.id });
166                        }
167                    }
168
169                    heap_translate.pop();
170                } else {
171                    temp.push(i);
172                }
173            }
174            _ => {
175                temp.push(i);
176            }
177        }
178    }
179
180    let done = temp
181        .into_iter()
182        .map(|c| match c {
183            Cmd::Ref { id } => opcode::Command {
184                opcode: opcode::Proof::Ref,
185                operand: id,
186            },
187            Cmd::Term { id } => opcode::Command {
188                opcode: opcode::Proof::Term,
189                operand: id,
190            },
191            Cmd::TermSave { id } => opcode::Command {
192                opcode: opcode::Proof::TermSave,
193                operand: id,
194            },
195            Cmd::Dummy { sort } => opcode::Command {
196                opcode: opcode::Proof::Dummy,
197                operand: sort,
198            },
199            Cmd::Hyp => opcode::Command {
200                opcode: opcode::Proof::Hyp,
201                operand: 0,
202            },
203        })
204        .collect();
205
206    Ok(done)
207}
208
209fn expand_preorder<'a, I>(ptrs: I, out: &mut Vec<Cmd>, data: &[Term], args: &[Ptr])
210where
211    I: Iterator<Item = &'a Ptr>,
212{
213    for i in ptrs {
214        match i {
215            Ptr::Ref { id } => out.push(Cmd::Ref { id: *id }),
216            Ptr::Term { id } => {
217                let term = data.get(*id as usize).unwrap();
218                let ptrs = args
219                    .get(term.ptr_args..(term.ptr_args + term.nr_args as usize))
220                    .unwrap();
221
222                expand_preorder(ptrs.iter().rev(), out, data, args);
223
224                out.push(Cmd::Term { id: term.id });
225            }
226        }
227    }
228}