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 }
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}