Skip to content

Commit 0564828

Browse files
committed
Just delay merging an answer into the caller strand until the next cycle
1 parent 91dddee commit 0564828

File tree

1 file changed

+12
-14
lines changed

1 file changed

+12
-14
lines changed

chalk-engine/src/logic.rs

Lines changed: 12 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -925,6 +925,10 @@ impl<'forest, I: Interner, C: Context<I> + 'forest, CO: ContextOps<I, C> + 'fore
925925
Ok(())
926926
}
927927

928+
/// This is called when there are no remaining subgoals for a strand, so
929+
/// it represents an answer. If the strand is ambiguous and we don't want
930+
/// it yet, we just enqueue it again to pick it up later. Otherwise, we
931+
/// add the answer from the strand onto the table.
928932
fn on_no_remaining_subgoals(&mut self, strand: Strand<I, C>) -> NoRemainingSubgoalsResult {
929933
let ambiguous = strand.ex_clause.ambiguous;
930934
if let AnswerMode::Complete = self.forest.tables[self.stack.top().table].answer_mode {
@@ -950,8 +954,11 @@ impl<'forest, I: Interner, C: Context<I> + 'forest, CO: ContextOps<I, C> + 'fore
950954
// answer for this table. Now, this table was either a
951955
// subgoal for another strand, or was the root table.
952956
let table = self.stack.top().table;
953-
let mut caller_strand = match self.stack.pop_and_take_caller_strand() {
954-
Some(s) => s,
957+
match self.stack.pop_and_take_caller_strand() {
958+
Some(caller_strand) => {
959+
self.stack.top().active_strand = Some(caller_strand);
960+
return NoRemainingSubgoalsResult::Success;
961+
}
955962
None => {
956963
// That was the root table, so we are done --
957964
// *well*, unless there were delayed
@@ -972,22 +979,13 @@ impl<'forest, I: Interner, C: Context<I> + 'forest, CO: ContextOps<I, C> + 'fore
972979
return NoRemainingSubgoalsResult::RootAnswerAvailable;
973980
}
974981
};
975-
976-
match self.merge_answer_into_strand(&mut caller_strand) {
977-
Err(e) => {
978-
drop(caller_strand);
979-
return NoRemainingSubgoalsResult::RootSearchFail(e);
980-
}
981-
Ok(_) => {
982-
self.stack.top().active_strand = Some(caller_strand);
983-
return NoRemainingSubgoalsResult::Success;
984-
}
985-
}
986982
}
987983
None => {
988984
debug!("answer is not available (or not new)");
989985

990-
// This table ned nowhere of interest
986+
// This strand led nowhere of interest. There might be *other*
987+
// answers on this table, but we don't care right now, we'll
988+
// try again at another time.
991989

992990
// Now we yield with `QuantumExceeded`
993991
self.unwind_stack();

0 commit comments

Comments
 (0)