backtrack attributed variable bindings after failure (#242)
This commit is contained in:
@@ -28,7 +28,7 @@ call_verify_attributes(Attrs, _, _, []) :-
|
|||||||
call_verify_attributes([], _, _, []).
|
call_verify_attributes([], _, _, []).
|
||||||
call_verify_attributes([Attr|Attrs], Var, Value, ListOfGoalLists) :-
|
call_verify_attributes([Attr|Attrs], Var, Value, ListOfGoalLists) :-
|
||||||
gather_modules([Attr|Attrs], Modules0),
|
gather_modules([Attr|Attrs], Modules0),
|
||||||
sort(Modules0, Modules),
|
sort(Modules0, Modules),
|
||||||
verify_attrs(Modules, Var, Value, ListOfGoalLists).
|
verify_attrs(Modules, Var, Value, ListOfGoalLists).
|
||||||
|
|
||||||
call_goals([ListOfGoalLists | ListsCubed]) :-
|
call_goals([ListOfGoalLists | ListsCubed]) :-
|
||||||
|
|||||||
@@ -36,19 +36,25 @@ impl AttrVarInitializer {
|
|||||||
self.attr_var_queue.clear();
|
self.attr_var_queue.clear();
|
||||||
self.bindings.clear();
|
self.bindings.clear();
|
||||||
}
|
}
|
||||||
|
|
||||||
|
#[inline]
|
||||||
|
pub(super) fn backtrack(&mut self, queue_b: usize, bindings_b: usize) {
|
||||||
|
self.attr_var_queue.truncate(queue_b);
|
||||||
|
self.bindings.truncate(bindings_b);
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
impl MachineState {
|
impl MachineState {
|
||||||
pub(super) fn push_attr_var_binding(&mut self, h: usize, addr: Addr) {
|
pub(super) fn push_attr_var_binding(&mut self, h: usize, addr: Addr) {
|
||||||
if self.attr_var_init.bindings.is_empty() {
|
if self.attr_var_init.bindings.is_empty() {
|
||||||
self.attr_var_init.instigating_p = self.p.local();
|
self.attr_var_init.instigating_p = self.p.local();
|
||||||
|
|
||||||
if self.last_call {
|
if self.last_call {
|
||||||
self.attr_var_init.cp = self.cp;
|
self.attr_var_init.cp = self.cp;
|
||||||
} else {
|
} else {
|
||||||
self.attr_var_init.cp = self.p.local() + 1;
|
self.attr_var_init.cp = self.p.local() + 1;
|
||||||
}
|
}
|
||||||
|
|
||||||
self.p = CodePtr::VerifyAttrInterrupt(self.attr_var_init.verify_attrs_loc);
|
self.p = CodePtr::VerifyAttrInterrupt(self.attr_var_init.verify_attrs_loc);
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -61,6 +67,7 @@ impl MachineState {
|
|||||||
.bindings
|
.bindings
|
||||||
.iter()
|
.iter()
|
||||||
.map(|(ref h, _)| Addr::AttrVar(*h));
|
.map(|(ref h, _)| Addr::AttrVar(*h));
|
||||||
|
|
||||||
let var_list_addr = Addr::HeapCell(self.heap.to_list(iter));
|
let var_list_addr = Addr::HeapCell(self.heap.to_list(iter));
|
||||||
|
|
||||||
let iter = self
|
let iter = self
|
||||||
@@ -68,6 +75,7 @@ impl MachineState {
|
|||||||
.bindings
|
.bindings
|
||||||
.iter()
|
.iter()
|
||||||
.map(|(_, ref addr)| addr.clone());
|
.map(|(_, ref addr)| addr.clone());
|
||||||
|
|
||||||
let value_list_addr = Addr::HeapCell(self.heap.to_list(iter));
|
let value_list_addr = Addr::HeapCell(self.heap.to_list(iter));
|
||||||
|
|
||||||
(var_list_addr, value_list_addr)
|
(var_list_addr, value_list_addr)
|
||||||
|
|||||||
@@ -58,34 +58,6 @@ impl<T: CopierTarget> CopyTermState<T> {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
fn reinstantiate_var(&mut self, addr: Addr, threshold: usize) {
|
|
||||||
match addr {
|
|
||||||
Addr::HeapCell(h) => {
|
|
||||||
self.target[threshold] = HeapCellValue::Addr(Addr::HeapCell(threshold));
|
|
||||||
self.target[h] = HeapCellValue::Addr(Addr::HeapCell(threshold));
|
|
||||||
self.trail
|
|
||||||
.push((Ref::HeapCell(h), HeapCellValue::Addr(Addr::HeapCell(h))));
|
|
||||||
}
|
|
||||||
Addr::StackCell(fr, sc) => {
|
|
||||||
self.target[threshold] = HeapCellValue::Addr(Addr::HeapCell(threshold));
|
|
||||||
self.target.stack()[fr][sc] = Addr::HeapCell(threshold);
|
|
||||||
self.trail.push((
|
|
||||||
Ref::StackCell(fr, sc),
|
|
||||||
HeapCellValue::Addr(Addr::StackCell(fr, sc)),
|
|
||||||
));
|
|
||||||
}
|
|
||||||
Addr::AttrVar(h) => {
|
|
||||||
let redirect_tag = self.attr_var_redirect_tag();
|
|
||||||
|
|
||||||
self.target[threshold] = HeapCellValue::Addr(redirect_tag(threshold));
|
|
||||||
self.target[h] = HeapCellValue::Addr(redirect_tag(threshold));
|
|
||||||
self.trail
|
|
||||||
.push((Ref::AttrVar(h), HeapCellValue::Addr(Addr::AttrVar(h))));
|
|
||||||
}
|
|
||||||
_ => {}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
fn copied_list(&mut self, addr: usize) -> bool {
|
fn copied_list(&mut self, addr: usize) -> bool {
|
||||||
if let HeapCellValue::Addr(Addr::Lis(addr)) = self.target[addr].clone() {
|
if let HeapCellValue::Addr(Addr::Lis(addr)) = self.target[addr].clone() {
|
||||||
if addr >= self.old_h {
|
if addr >= self.old_h {
|
||||||
@@ -113,22 +85,10 @@ impl<T: CopierTarget> CopyTermState<T> {
|
|||||||
let rd = self.target.store(self.target.deref(ra));
|
let rd = self.target.store(self.target.deref(ra));
|
||||||
|
|
||||||
match rd.clone() {
|
match rd.clone() {
|
||||||
Addr::AttrVar(h) if h >= self.old_h => {
|
Addr::AttrVar(h) | Addr::HeapCell(h) if h >= self.old_h => {
|
||||||
let redirect_tag = self.attr_var_redirect_tag();
|
|
||||||
self.target[threshold] = HeapCellValue::Addr(redirect_tag(h));
|
|
||||||
}
|
|
||||||
Addr::HeapCell(h) if h >= self.old_h => {
|
|
||||||
self.target[threshold] = HeapCellValue::Addr(rd)
|
self.target[threshold] = HeapCellValue::Addr(rd)
|
||||||
}
|
}
|
||||||
Addr::AttrVar(h) => {
|
ra @ Addr::AttrVar(..) | ra @ Addr::HeapCell(_) | ra @ Addr::StackCell(..) => {
|
||||||
if Addr::AttrVar(h) == rd {
|
|
||||||
self.reinstantiate_var(Addr::AttrVar(h), threshold);
|
|
||||||
} else {
|
|
||||||
let redirect_tag = self.attr_var_redirect_tag();
|
|
||||||
self.target[threshold] = HeapCellValue::Addr(redirect_tag(h));
|
|
||||||
}
|
|
||||||
}
|
|
||||||
ra @ Addr::HeapCell(..) | ra @ Addr::StackCell(..) => {
|
|
||||||
if ra == rd {
|
if ra == rd {
|
||||||
self.reinstantiate_var(ra, threshold);
|
self.reinstantiate_var(ra, threshold);
|
||||||
} else {
|
} else {
|
||||||
@@ -148,6 +108,38 @@ impl<T: CopierTarget> CopyTermState<T> {
|
|||||||
self.scan += 1;
|
self.scan += 1;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
fn reinstantiate_var(&mut self, addr: Addr, threshold: usize) {
|
||||||
|
match addr {
|
||||||
|
Addr::HeapCell(h) => {
|
||||||
|
self.target[threshold] = HeapCellValue::Addr(Addr::HeapCell(threshold));
|
||||||
|
self.target[h] = HeapCellValue::Addr(Addr::HeapCell(threshold));
|
||||||
|
self.trail.push((
|
||||||
|
Ref::HeapCell(h),
|
||||||
|
HeapCellValue::Addr(Addr::HeapCell(h)),
|
||||||
|
));
|
||||||
|
}
|
||||||
|
Addr::StackCell(fr, sc) => {
|
||||||
|
self.target[threshold] = HeapCellValue::Addr(Addr::HeapCell(threshold));
|
||||||
|
self.target.stack()[fr][sc] = Addr::HeapCell(threshold);
|
||||||
|
self.trail.push((
|
||||||
|
Ref::StackCell(fr, sc),
|
||||||
|
HeapCellValue::Addr(Addr::StackCell(fr, sc)),
|
||||||
|
));
|
||||||
|
}
|
||||||
|
Addr::AttrVar(h) => {
|
||||||
|
let redirect_tag = self.attr_var_redirect_tag();
|
||||||
|
|
||||||
|
self.target[threshold] = HeapCellValue::Addr(redirect_tag(threshold));
|
||||||
|
self.target[h] = HeapCellValue::Addr(redirect_tag(threshold));
|
||||||
|
self.trail.push((
|
||||||
|
Ref::AttrVar(h),
|
||||||
|
HeapCellValue::Addr(Addr::AttrVar(h)),
|
||||||
|
));
|
||||||
|
}
|
||||||
|
_ => unreachable!()
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
fn copy_var(&mut self, addr: Addr) {
|
fn copy_var(&mut self, addr: Addr) {
|
||||||
let rd = self.target.store(self.target.deref(addr.clone()));
|
let rd = self.target.store(self.target.deref(addr.clone()));
|
||||||
|
|
||||||
@@ -168,7 +160,7 @@ impl<T: CopierTarget> CopyTermState<T> {
|
|||||||
self.target
|
self.target
|
||||||
.push(HeapCellValue::Addr(redirect_tag(threshold)));
|
.push(HeapCellValue::Addr(redirect_tag(threshold)));
|
||||||
|
|
||||||
if let Addr::AttrVar(_) = redirect_tag(threshold) {
|
if let AttrVarPolicy::DeepCopy = self.attr_var_policy {
|
||||||
let list_val = self.target[h + 1].clone();
|
let list_val = self.target[h + 1].clone();
|
||||||
self.target.push(list_val);
|
self.target.push(list_val);
|
||||||
}
|
}
|
||||||
@@ -181,7 +173,9 @@ impl<T: CopierTarget> CopyTermState<T> {
|
|||||||
self.reinstantiate_var(addr, scan);
|
self.reinstantiate_var(addr, scan);
|
||||||
self.scan += 1;
|
self.scan += 1;
|
||||||
}
|
}
|
||||||
_ => *self.value_at_scan() = HeapCellValue::Addr(rd),
|
_ => {
|
||||||
|
*self.value_at_scan() = HeapCellValue::Addr(rd);
|
||||||
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|||||||
@@ -445,11 +445,13 @@ pub(crate) trait CallPolicy: Any {
|
|||||||
|
|
||||||
machine_st.heap.truncate(machine_st.or_stack[b].h);
|
machine_st.heap.truncate(machine_st.or_stack[b].h);
|
||||||
|
|
||||||
let attr_var_init_b = machine_st.or_stack[b].attr_var_init_b;
|
let attr_var_init_queue_b = machine_st.or_stack[b].attr_var_init_queue_b;
|
||||||
machine_st
|
let attr_var_init_bindings_b = machine_st.or_stack[b].attr_var_init_bindings_b;
|
||||||
.attr_var_init
|
|
||||||
.attr_var_queue
|
machine_st.attr_var_init.backtrack(
|
||||||
.truncate(attr_var_init_b);
|
attr_var_init_queue_b,
|
||||||
|
attr_var_init_bindings_b,
|
||||||
|
);
|
||||||
|
|
||||||
machine_st.hb = machine_st.heap.h;
|
machine_st.hb = machine_st.heap.h;
|
||||||
machine_st.p += 1;
|
machine_st.p += 1;
|
||||||
@@ -491,11 +493,13 @@ pub(crate) trait CallPolicy: Any {
|
|||||||
|
|
||||||
machine_st.heap.truncate(machine_st.or_stack[b].h);
|
machine_st.heap.truncate(machine_st.or_stack[b].h);
|
||||||
|
|
||||||
let attr_var_init_b = machine_st.or_stack[b].attr_var_init_b;
|
let attr_var_init_queue_b = machine_st.or_stack[b].attr_var_init_queue_b;
|
||||||
machine_st
|
let attr_var_init_bindings_b = machine_st.or_stack[b].attr_var_init_bindings_b;
|
||||||
.attr_var_init
|
|
||||||
.attr_var_queue
|
machine_st.attr_var_init.backtrack(
|
||||||
.truncate(attr_var_init_b);
|
attr_var_init_queue_b,
|
||||||
|
attr_var_init_bindings_b,
|
||||||
|
);
|
||||||
|
|
||||||
machine_st.hb = machine_st.heap.h;
|
machine_st.hb = machine_st.heap.h;
|
||||||
machine_st.p += offset;
|
machine_st.p += offset;
|
||||||
@@ -533,11 +537,13 @@ pub(crate) trait CallPolicy: Any {
|
|||||||
|
|
||||||
machine_st.heap.truncate(machine_st.or_stack[b].h);
|
machine_st.heap.truncate(machine_st.or_stack[b].h);
|
||||||
|
|
||||||
let attr_var_init_b = machine_st.or_stack[b].attr_var_init_b;
|
let attr_var_init_queue_b = machine_st.or_stack[b].attr_var_init_queue_b;
|
||||||
machine_st
|
let attr_var_init_bindings_b = machine_st.or_stack[b].attr_var_init_bindings_b;
|
||||||
.attr_var_init
|
|
||||||
.attr_var_queue
|
machine_st.attr_var_init.backtrack(
|
||||||
.truncate(attr_var_init_b);
|
attr_var_init_queue_b,
|
||||||
|
attr_var_init_bindings_b,
|
||||||
|
);
|
||||||
|
|
||||||
machine_st.b = machine_st.or_stack[b].b;
|
machine_st.b = machine_st.or_stack[b].b;
|
||||||
machine_st.or_stack.truncate(machine_st.b);
|
machine_st.or_stack.truncate(machine_st.b);
|
||||||
@@ -580,12 +586,14 @@ pub(crate) trait CallPolicy: Any {
|
|||||||
|
|
||||||
machine_st.heap.truncate(machine_st.or_stack[b].h);
|
machine_st.heap.truncate(machine_st.or_stack[b].h);
|
||||||
|
|
||||||
let attr_var_init_b = machine_st.or_stack[b].attr_var_init_b;
|
let attr_var_init_queue_b = machine_st.or_stack[b].attr_var_init_queue_b;
|
||||||
machine_st
|
let attr_var_init_bindings_b = machine_st.or_stack[b].attr_var_init_bindings_b;
|
||||||
.attr_var_init
|
|
||||||
.attr_var_queue
|
|
||||||
.truncate(attr_var_init_b);
|
|
||||||
|
|
||||||
|
machine_st.attr_var_init.backtrack(
|
||||||
|
attr_var_init_queue_b,
|
||||||
|
attr_var_init_bindings_b,
|
||||||
|
);
|
||||||
|
|
||||||
machine_st.b = machine_st.or_stack[b].b;
|
machine_st.b = machine_st.or_stack[b].b;
|
||||||
machine_st.or_stack.truncate(machine_st.b);
|
machine_st.or_stack.truncate(machine_st.b);
|
||||||
|
|
||||||
|
|||||||
@@ -3300,6 +3300,7 @@ impl MachineState {
|
|||||||
self.e,
|
self.e,
|
||||||
self.cp.clone(),
|
self.cp.clone(),
|
||||||
self.attr_var_init.attr_var_queue.len(),
|
self.attr_var_init.attr_var_queue.len(),
|
||||||
|
self.attr_var_init.bindings.len(),
|
||||||
self.b,
|
self.b,
|
||||||
self.p.clone() + 1,
|
self.p.clone() + 1,
|
||||||
self.tr,
|
self.tr,
|
||||||
@@ -3339,6 +3340,7 @@ impl MachineState {
|
|||||||
self.e,
|
self.e,
|
||||||
self.cp.clone(),
|
self.cp.clone(),
|
||||||
self.attr_var_init.attr_var_queue.len(),
|
self.attr_var_init.attr_var_queue.len(),
|
||||||
|
self.attr_var_init.bindings.len(),
|
||||||
self.b,
|
self.b,
|
||||||
self.p.clone() + offset,
|
self.p.clone() + offset,
|
||||||
self.tr,
|
self.tr,
|
||||||
|
|||||||
@@ -8,7 +8,8 @@ pub struct Frame {
|
|||||||
pub global_index: usize,
|
pub global_index: usize,
|
||||||
pub e: usize,
|
pub e: usize,
|
||||||
pub cp: LocalCodePtr,
|
pub cp: LocalCodePtr,
|
||||||
pub attr_var_init_b: usize,
|
pub attr_var_init_queue_b: usize,
|
||||||
|
pub attr_var_init_bindings_b: usize,
|
||||||
pub b: usize,
|
pub b: usize,
|
||||||
pub bp: CodePtr,
|
pub bp: CodePtr,
|
||||||
pub tr: usize,
|
pub tr: usize,
|
||||||
@@ -23,7 +24,8 @@ impl Frame {
|
|||||||
global_index: usize,
|
global_index: usize,
|
||||||
e: usize,
|
e: usize,
|
||||||
cp: LocalCodePtr,
|
cp: LocalCodePtr,
|
||||||
attr_var_init_b: usize,
|
attr_var_init_queue_b: usize,
|
||||||
|
attr_var_init_bindings_b: usize,
|
||||||
b: usize,
|
b: usize,
|
||||||
bp: CodePtr,
|
bp: CodePtr,
|
||||||
tr: usize,
|
tr: usize,
|
||||||
@@ -36,7 +38,8 @@ impl Frame {
|
|||||||
global_index,
|
global_index,
|
||||||
e,
|
e,
|
||||||
cp,
|
cp,
|
||||||
attr_var_init_b,
|
attr_var_init_queue_b,
|
||||||
|
attr_var_init_bindings_b,
|
||||||
b,
|
b,
|
||||||
bp,
|
bp,
|
||||||
tr,
|
tr,
|
||||||
@@ -64,7 +67,8 @@ impl OrStack {
|
|||||||
global_index: usize,
|
global_index: usize,
|
||||||
e: usize,
|
e: usize,
|
||||||
cp: LocalCodePtr,
|
cp: LocalCodePtr,
|
||||||
attr_var_init_b: usize,
|
attr_var_init_queue_b: usize,
|
||||||
|
attr_var_init_bindings_b: usize,
|
||||||
b: usize,
|
b: usize,
|
||||||
bp: CodePtr,
|
bp: CodePtr,
|
||||||
tr: usize,
|
tr: usize,
|
||||||
@@ -77,7 +81,8 @@ impl OrStack {
|
|||||||
global_index,
|
global_index,
|
||||||
e,
|
e,
|
||||||
cp,
|
cp,
|
||||||
attr_var_init_b,
|
attr_var_init_queue_b,
|
||||||
|
attr_var_init_bindings_b,
|
||||||
b,
|
b,
|
||||||
bp,
|
bp,
|
||||||
tr,
|
tr,
|
||||||
|
|||||||
@@ -44,8 +44,7 @@
|
|||||||
),
|
),
|
||||||
( '$get_b_value'(B), call(Term), '$write_eqs_and_read_input'(B, VarList), !
|
( '$get_b_value'(B), call(Term), '$write_eqs_and_read_input'(B, VarList), !
|
||||||
; write('false.'), nl
|
; write('false.'), nl
|
||||||
),
|
).
|
||||||
'$reset_attr_var_state'.
|
|
||||||
|
|
||||||
'$needs_bracketing'(Value, Op) :-
|
'$needs_bracketing'(Value, Op) :-
|
||||||
catch((functor(Value, F, _),
|
catch((functor(Value, F, _),
|
||||||
|
|||||||
Reference in New Issue
Block a user