cache ball terms before unifying in handle_ball/3 (#1608)

This commit is contained in:
Mark Thom
2022-10-22 22:56:06 -06:00
parent f2940ddfcf
commit 8781e03863
8 changed files with 87 additions and 37 deletions

View File

@@ -404,8 +404,6 @@ enum SystemClauseType {
InferenceLevel,
#[strum_discriminants(strum(props(Arity = "1", Name = "$clean_up_block")))]
CleanUpBlock,
#[strum_discriminants(strum(props(Arity = "0", Name = "$erase_ball")))]
EraseBall,
#[strum_discriminants(strum(props(Arity = "0", Name = "$fail")))]
Fail,
#[strum_discriminants(strum(props(Arity = "1", Name = "$get_ball")))]
@@ -434,6 +432,12 @@ enum SystemClauseType {
ReturnFromVerifyAttr,
#[strum_discriminants(strum(props(Arity = "1", Name = "$set_ball")))]
SetBall,
#[strum_discriminants(strum(props(Arity = "0", Name = "$push_ball_stack")))]
PushBallStack,
#[strum_discriminants(strum(props(Arity = "0", Name = "$pop_ball_stack")))]
PopBallStack,
#[strum_discriminants(strum(props(Arity = "0", Name = "$pop_from_ball_stack")))]
PopFromBallStack,
#[strum_discriminants(strum(props(Arity = "1", Name = "$set_cp_by_default")))]
SetCutPointByDefault(RegType),
#[strum_discriminants(strum(props(Arity = "1", Name = "$set_double_quotes")))]
@@ -1680,7 +1684,6 @@ fn generate_instruction_preface() -> TokenStream {
&Instruction::CallSetStreamPosition(_) |
&Instruction::CallInferenceLevel(_) |
&Instruction::CallCleanUpBlock(_) |
&Instruction::CallEraseBall(_) |
&Instruction::CallFail(_) |
&Instruction::CallGetBall(_) |
&Instruction::CallGetCurrentBlock(_) |
@@ -1703,6 +1706,9 @@ fn generate_instruction_preface() -> TokenStream {
&Instruction::CallResetBlock(_) |
&Instruction::CallReturnFromVerifyAttr(_) |
&Instruction::CallSetBall(_) |
&Instruction::CallPushBallStack(_) |
&Instruction::CallPopBallStack(_) |
&Instruction::CallPopFromBallStack(_) |
&Instruction::CallSetCutPointByDefault(..) |
&Instruction::CallSetDoubleQuotes(_) |
&Instruction::CallSetSeed(_) |
@@ -1892,7 +1898,6 @@ fn generate_instruction_preface() -> TokenStream {
&Instruction::ExecuteSetStreamPosition(_) |
&Instruction::ExecuteInferenceLevel(_) |
&Instruction::ExecuteCleanUpBlock(_) |
&Instruction::ExecuteEraseBall(_) |
&Instruction::ExecuteFail(_) |
&Instruction::ExecuteGetBall(_) |
&Instruction::ExecuteGetCurrentBlock(_) |
@@ -1915,6 +1920,9 @@ fn generate_instruction_preface() -> TokenStream {
&Instruction::ExecuteResetBlock(_) |
&Instruction::ExecuteReturnFromVerifyAttr(_) |
&Instruction::ExecuteSetBall(_) |
&Instruction::ExecutePushBallStack(_) |
&Instruction::ExecutePopBallStack(_) |
&Instruction::ExecutePopFromBallStack(_) |
&Instruction::ExecuteSetCutPointByDefault(_, _) |
&Instruction::ExecuteSetDoubleQuotes(_) |
&Instruction::ExecuteSetSeed(_) |

View File

@@ -644,6 +644,7 @@ catch(G,C,R,Bb) :-
catch(G,C,R,Bb) :-
'$reset_block'(Bb),
'$get_ball'(Ball),
'$push_ball_stack', % move ball to ball stack.
handle_ball(Ball, C, R).
@@ -660,9 +661,10 @@ end_block(Bb, NBb) :-
handle_ball(C, C, R) :-
!,
'$erase_ball',
'$pop_ball_stack', % remove ball from ball stack.
call(R).
handle_ball(_, _, _) :-
'$pop_from_ball_stack', % restore ball from ball stack.
'$unwind_stack'.
:- non_counted_backtracking throw/1.

View File

@@ -75,19 +75,19 @@ scc_helper(C, G, Bb) :-
'$get_cp'(Cp),
'$install_scc_cleaner'(C, NBb),
'$call_with_inference_counting'(call(G)),
( '$check_cp'(Cp) ->
'$reset_block'(Bb),
run_cleaners_without_handling(Cp)
; true
; '$reset_block'(NBb),
'$fail'
( '$check_cp'(Cp) ->
'$reset_block'(Bb),
run_cleaners_without_handling(Cp)
; true
; '$reset_block'(NBb),
'$fail'
).
scc_helper(_, _, Bb) :-
'$reset_block'(Bb),
'$get_ball'(Ball),
'$erase_ball',
'$push_ball_stack',
run_cleaners_with_handling,
throw(Ball).
'$pop_from_ball_stack',
'$unwind_stack'.
scc_helper(_, _, _) :-
'$get_cp'(Cp),
run_cleaners_without_handling(Cp),
@@ -130,10 +130,13 @@ end_block(B, _Bb, NBb, L) :-
:- non_counted_backtracking handle_ile/3.
handle_ile(B, inference_limit_exceeded(B), inference_limit_exceeded) :- !.
handle_ile(B, E, _) :-
handle_ile(B, inference_limit_exceeded(B), inference_limit_exceeded) :-
!,
'$pop_ball_stack'.
handle_ile(B, _, _) :-
'$remove_call_policy_check'(B),
throw(E).
'$pop_from_ball_stack',
'$unwind_stack'.
:- meta_predicate(call_with_inference_limit(0, ?, ?)).
@@ -167,18 +170,18 @@ call_with_inference_limit(G, L, R, Bb, B) :-
'$call_with_inference_counting'(call(G)),
'$inference_level'(R, B),
'$remove_inference_counter'(B, Count1),
is(Diff, L - (Count1 - Count0)),
Diff is L - (Count1 - Count0),
end_block(B, Bb, NBb, Diff).
call_with_inference_limit(_, _, R, Bb, B) :-
'$reset_block'(Bb),
'$remove_inference_counter'(B, _),
( '$get_ball'(Ball),
'$push_ball_stack',
'$get_level'(Cp),
'$set_cp_by_default'(Cp)
; '$remove_call_policy_check'(B),
'$fail'
),
'$erase_ball',
handle_ile(B, Ball, R).
partial_string(String, L, L0) :-

View File

@@ -32,9 +32,9 @@ write_error(Error) :-
),
write('.').
'$print_message_and_fail'(inference_limit_exceeded(B)) :-
integer(B),
throw(inference_limit_exceeded(B)).
% '$print_message_and_fail'(inference_limit_exceeded(B)) :-
% integer(B),
% throw(inference_limit_exceeded(B)).
'$print_message_and_fail'(Error) :-
write_error(Error),
nl,

View File

@@ -4125,14 +4125,6 @@ impl Machine {
self.clean_up_block();
self.machine_st.p = self.machine_st.cp;
}
&Instruction::CallEraseBall(_) => {
self.erase_ball();
self.machine_st.p += 1;
}
&Instruction::ExecuteEraseBall(_) => {
self.erase_ball();
self.machine_st.p = self.machine_st.cp;
}
&Instruction::CallFail(_) | &Instruction::ExecuteFail(_) => {
self.machine_st.backtrack();
}
@@ -4284,6 +4276,30 @@ impl Machine {
self.set_ball();
self.machine_st.p = self.machine_st.cp;
}
&Instruction::CallPushBallStack(_) => {
self.push_ball_stack();
step_or_fail!(self, self.machine_st.p += 1);
}
&Instruction::ExecutePushBallStack(_) => {
self.push_ball_stack();
step_or_fail!(self, self.machine_st.p = self.machine_st.cp);
}
&Instruction::CallPopBallStack(_) => {
self.pop_ball_stack();
self.machine_st.p += 1;
}
&Instruction::ExecutePopBallStack(_) => {
self.pop_ball_stack();
self.machine_st.p = self.machine_st.cp;
}
&Instruction::CallPopFromBallStack(_) => {
self.pop_from_ball_stack();
self.machine_st.p += 1;
}
&Instruction::ExecutePopFromBallStack(_) => {
self.pop_from_ball_stack();
self.machine_st.p = self.machine_st.cp;
}
&Instruction::CallSetCutPointByDefault(r, _) => {
self.set_cut_point_by_default(r);
step_or_fail!(self, self.machine_st.p += 1);
@@ -4970,11 +4986,11 @@ impl Machine {
}
&Instruction::CallPredicateDefined(_) => {
self.machine_st.fail = !self.predicate_defined();
self.machine_st.p += 1;
step_or_fail!(self, self.machine_st.p += 1);
}
&Instruction::ExecutePredicateDefined(_) => {
self.machine_st.fail = !self.predicate_defined();
self.machine_st.p = self.machine_st.cp;
step_or_fail!(self, self.machine_st.p = self.machine_st.cp);
}
&Instruction::CallStripModule(_) => {
let (module_loc, qualified_goal) = self.machine_st.strip_module(

View File

@@ -75,6 +75,7 @@ pub struct MachineState {
pub(super) hb: usize,
pub(super) block: usize, // an offset into the OR stack.
pub(super) ball: Ball,
pub(super) ball_stack: Vec<Ball>, // save current ball before jumping via, e.g., verify_attr interrupt.
pub(super) lifted_heap: Heap,
pub(super) interms: Vec<Number>, // intermediate numbers.
// locations of cleaners, cut points, the previous block. for setup_call_cleanup.
@@ -113,6 +114,7 @@ impl fmt::Debug for MachineState {
.field("hb", &self.hb)
.field("block", &self.block)
.field("ball", &self.ball)
.field("ball_stack", &self.ball_stack)
.field("lifted_heap", &self.lifted_heap)
.field("interms", &self.interms)
.field("flags", &self.flags)

View File

@@ -47,6 +47,7 @@ impl MachineState {
hb: 0,
block: 0,
ball: Ball::new(),
ball_stack: vec![],
lifted_heap: Heap::new(),
interms: vec![Number::default();256],
cont_pts: Vec::with_capacity(256),

View File

@@ -4804,11 +4804,6 @@ impl Machine {
}
}
#[inline(always)]
pub(crate) fn erase_ball(&mut self) {
self.machine_st.ball.reset();
}
#[inline(always)]
pub(crate) fn get_ball(&mut self) {
let addr = self.machine_st.store(self.machine_st.deref(self.machine_st.registers[1]));
@@ -4828,6 +4823,29 @@ impl Machine {
};
}
#[inline(always)]
pub(crate) fn push_ball_stack(&mut self) {
if self.machine_st.ball.stub.len() > 0 {
self.machine_st.ball_stack.push(
mem::replace(&mut self.machine_st.ball, Ball::new())
);
} else {
self.machine_st.fail = true;
}
}
#[inline(always)]
pub(crate) fn pop_ball_stack(&mut self) {
self.machine_st.ball_stack.pop();
}
#[inline(always)]
pub(crate) fn pop_from_ball_stack(&mut self) {
if let Some(ball) = self.machine_st.ball_stack.pop() {
self.machine_st.ball = ball;
}
}
#[inline(always)]
pub(crate) fn get_current_block(&mut self) {
let n = Fixnum::build_with(i64::try_from(self.machine_st.block).unwrap());