1use crate::{
4 heap::heap::{Cell, Heap, Tag},
5 program::clause::BitFlag64,
6 resolution::unification::Substitution,
7};
8
9pub fn re_build_bound_arg_terms(heap: &mut impl Heap,substitution: &mut Substitution){
13 for i in 0..substitution.len(){
14 if let (_, bound_addr, true) = substitution[i]{
15 if heap.contains_args(bound_addr) {
16 let new_bound_addr = build(heap, substitution, None, bound_addr);
19 substitution[i].1 = new_bound_addr;
20 }
21 }
22
23 }
24}
25
26pub fn build(
31 heap: &mut impl Heap,
32 substitution: &mut Substitution,
33 meta_vars: Option<BitFlag64>,
34 src_addr: usize,
35) -> usize {
36 match heap[heap.deref_addr(src_addr)] {
37 (tag @ (Tag::Con | Tag::Flt | Tag::Int | Tag::Stri | Tag::ELis | Tag::Ref), value) => {
38 heap.heap_push((tag, value))
39 }
40 (Tag::Arg, _arg_id) => build_arg(heap, substitution, meta_vars, src_addr),
41 (Tag::Func | Tag::Tup | Tag::Set, _) => build_str(heap, substitution, meta_vars, src_addr),
42 (Tag::Lis, ptr) => {
43 let new_ptr = build_list(heap, substitution, meta_vars, ptr);
44 heap.heap_push((Tag::Lis, new_ptr))
45 }
46 cell => unimplemented!("build: unhandled cell type {cell:?}"),
47 }
48}
49
50fn build_arg(
51 heap: &mut impl Heap,
52 substitution: &mut Substitution,
53 meta_vars: Option<BitFlag64>,
54 src_addr: usize,
55) -> usize {
56 let arg_id = heap[src_addr].1;
57 match meta_vars {
58 Some(bit_flags) if !bit_flags.get(arg_id) => heap.heap_push(heap[src_addr]),
59 _ => match substitution.get_arg(arg_id) {
60 Some(bound_addr) => heap.set_ref(Some(bound_addr)),
61 None => {
62 let ref_addr = heap.set_ref(None);
63 substitution.set_arg(arg_id, ref_addr);
64 ref_addr
65 }
66 },
67 }
68}
69
70
71fn build_str(
72 heap: &mut impl Heap,
73 substitution: &mut Substitution,
74 meta_vars: Option<BitFlag64>,
75 src_addr: usize,
76) -> usize {
77 let (tag, length) = heap[src_addr];
78 let mut complex_terms: Vec<Option<Cell>> = Vec::with_capacity(length);
79 for i in 1..length + 1 {
80 complex_terms.push(build_complex_term(
81 heap,
82 substitution,
83 meta_vars,
84 src_addr + i,
85 ));
86 }
87 let addr = heap.heap_push((tag, length));
88 let mut i = 1;
89 for complex_term in complex_terms {
90 match complex_term {
91 Some(cell) => heap.heap_push(cell),
92 None => build(heap, substitution, meta_vars, src_addr + i),
93 };
94 i += 1;
95 }
96
97 addr
98}
99
100fn build_list(
101 heap: &mut impl Heap,
102 substitution: &mut Substitution,
103 meta_vars: Option<BitFlag64>,
104 src_addr: usize,
105) -> usize {
106 let head = build_complex_term(heap, substitution, meta_vars, src_addr);
107 let tail = build_complex_term(heap, substitution, meta_vars, src_addr+1);
108 let ptr = match head{
109 Some(cell) => heap.heap_push(cell),
110 None => build(heap, substitution, meta_vars, src_addr),
111 };
112 match tail {
113 Some(cell) => heap.heap_push(cell),
114 None => build(heap, substitution, meta_vars, src_addr+1),
115 };
116 ptr
117}
118
119fn build_complex_term(
120 heap: &mut impl Heap,
121 substitution: &mut Substitution,
122 meta_vars: Option<BitFlag64>,
123 src_addr: usize,
124) -> Option<Cell> {
125 match heap[heap.deref_addr(src_addr)] {
126 (Tag::Func | Tag::Tup | Tag::Set, _) => {
127 Some((Tag::Str, build_str(heap, substitution, meta_vars, src_addr)))
128 }
129 (Tag::Str, ptr) => Some((Tag::Str, build_str(heap, substitution, meta_vars, ptr))),
130 (Tag::Lis, ptr) => Some((Tag::Lis, build_list(heap, substitution, meta_vars, ptr))),
131 (Tag::Arg, id) => match meta_vars {
132 Some(bitflags) if !bitflags.get(id) => None,
133 _ => match substitution.get_arg(id) {
134 Some(addr) => build_complex_term(heap, substitution, meta_vars, addr),
135 None => None,
136 },
137 },
138 (Tag::Ref, ref_addr) if ref_addr == src_addr => {
139 if let Some(bound_addr) = substitution.bound(ref_addr) {
140 build_complex_term(heap, substitution, meta_vars, bound_addr)
141 } else {
142 None
143 }
144 }
145 _ => None,
146 }
147}
148
149#[cfg(test)]
150mod tests {
151 use crate::{
152 heap::{
153 heap::{Heap, Tag},
154 symbol_db::SymbolDB,
155 },
156 program::clause::BitFlag64,
157 resolution::{build::{build, re_build_bound_arg_terms}, unification::{unify, Substitution}},
158 };
159
160 #[test]
161 fn args() {
162 let p = SymbolDB::set_const("p".into());
163 let f = SymbolDB::set_const("f".into());
164
165 let mut heap = vec![(Tag::Func, 4), (Tag::Con, p), (Tag::Arg, 0), (Tag::Arg, 0), (Tag::Arg, 1)];
166 let mut substitution = Substitution::default();
167 let addr = build(&mut heap, &mut substitution, None, 0);
168 assert_eq!(
169 heap[addr..(addr + 4)],
170 [
171 (Tag::Func, 4),
172 (Tag::Con, p),
173 (Tag::Ref, addr + 2),
174 (Tag::Ref, addr + 2),
175 ]
176 );
177
178 let mut substitution = Substitution::default();
179 let mut meta_vars = BitFlag64::default();
180 meta_vars.set(0);
181 let addr = build(&mut heap, &mut substitution, Some(meta_vars), 0);
182 heap._print_heap();
183 assert_eq!(
184 heap[addr..(addr + 5)],
185 [(Tag::Func, 4), (Tag::Con, p), (Tag::Ref, addr+2), (Tag::Ref, addr+2), (Tag::Arg, 1)]
186 );
187
188 heap = vec![
189 (Tag::Func, 2),
190 (Tag::Con, f),
191 (Tag::Ref, 2),
192 (Tag::Func, 2),
193 (Tag::Con, p),
194 (Tag::Arg, 0),
195 ];
196 substitution = Substitution::default();
197 substitution.set_arg(0, 0);
198 let addr = build(&mut heap, &mut substitution, None, 3);
199 assert_eq!(
200 heap[addr - 3..(addr + 3)],
201 [
202 (Tag::Func, 2),
203 (Tag::Con, f),
204 (Tag::Ref, 2),
205 (Tag::Func, 2),
206 (Tag::Con, p),
207 (Tag::Str, addr-3),
208 ]
209 );
210 }
211
212 #[test]
213 fn lists() {
214 let p = SymbolDB::set_const("p".into());
215 let a = SymbolDB::set_const("a".into());
216 let b = SymbolDB::set_const("b".into());
217 let c = SymbolDB::set_const("c".into());
218
219 let mut heap = vec![
220 (Tag::Con, a), (Tag::Lis, 2), (Tag::Con, b), (Tag::Arg, 0), (Tag::Func, 2), (Tag::Con, p), (Tag::Lis, 0), (Tag::Con, a), (Tag::Lis, 9), (Tag::Con, b), (Tag::Lis, 11), (Tag::Con, c), (Tag::ELis, 0), (Tag::Func, 2), (Tag::Con, p), (Tag::Lis, 7), ];
240 let mut substitution = Substitution::default();
241 substitution.set_arg(0, 10);
242 let addr = build(&mut heap, &mut substitution, None, 4);
243 assert_eq!(heap.term_string(addr), "p([a,b,c])");
244
245
246 let mut heap = vec![
247 (Tag::Con, a), (Tag::Lis, 2), (Tag::Con, b), (Tag::Ref, 3), (Tag::Func, 2), (Tag::Con, p), (Tag::Lis, 0), (Tag::Con, a), (Tag::Lis, 9), (Tag::Con, b), (Tag::Lis, 11), (Tag::Arg, 0), (Tag::ELis, 0), (Tag::Func, 2), (Tag::Con, p), (Tag::Lis, 7), ];
267 let mut substitution = Substitution::default();
268 substitution = substitution.push((3,10,true));
269 re_build_bound_arg_terms(&mut heap, &mut substitution);
270 let new_term = build(&mut heap, &mut substitution, None, 13);
271 println!("{}",heap.term_string(new_term));
272 }
273
274 #[test]
275 fn meta_vars(){
276
277 }
278
279 #[test]
280 fn test1() {
281 let p = SymbolDB::set_const("p".into());
282 let mut heap = vec![
283 (Tag::Ref, 0), (Tag::Lis, 2), (Tag::Ref, 2), (Tag::ELis, 0), (Tag::Func, 3), (Tag::Con, p), (Tag::Ref, 6), (Tag::Lis, 0), (Tag::Func, 3), (Tag::Con, p), (Tag::Arg, 0), (Tag::Arg, 0), ];
296
297 let mut sub = unify(&heap, 8, 4).unwrap();
298 re_build_bound_arg_terms(&mut heap, &mut sub);
299
300 heap._print_heap();
301 println!("{:?}", sub.bound(6))
302 }
303
304 #[test]
305 fn test2() {
306 let p = SymbolDB::set_const("p".into());
307 let mut heap = vec![
308 (Tag::Ref, 0), (Tag::Lis, 2), (Tag::Ref, 2), (Tag::ELis, 0), (Tag::Func, 3), (Tag::Con, p), (Tag::Ref, 6), (Tag::Lis, 0), (Tag::Func, 3), (Tag::Con, p), (Tag::Arg, 0), (Tag::Arg, 0), ];
321
322 let mut sub = unify(&heap, 8, 4).unwrap();
323 re_build_bound_arg_terms(&mut heap, &mut sub);
324
325 heap._print_heap();
326 println!("{:?}", sub.bound(6))
327 }
328}