use crate::index_struct;
use crate::strand::CanonicalStrand;
use crate::{Answer, AnswerMode};
use rustc_hash::FxHashMap;
use std::collections::hash_map::Entry;
use std::collections::VecDeque;
use std::mem;
use chalk_ir::interner::Interner;
use chalk_ir::{AnswerSubst, Canonical, Goal, InEnvironment, UCanonical};
use tracing::{debug, info, instrument};
#[derive(Debug)]
pub(crate) struct Table<I: Interner> {
pub(crate) table_goal: UCanonical<InEnvironment<Goal<I>>>,
pub(crate) coinductive_goal: bool,
floundered: bool,
answers: Vec<Answer<I>>,
answers_hash: FxHashMap<Canonical<AnswerSubst<I>>, bool>,
strands: VecDeque<CanonicalStrand<I>>,
pub(crate) answer_mode: AnswerMode,
}
index_struct! {
pub(crate) struct AnswerIndex {
value: usize,
}
}
impl<I: Interner> Table<I> {
pub(crate) fn new(
table_goal: UCanonical<InEnvironment<Goal<I>>>,
coinductive_goal: bool,
) -> Table<I> {
Table {
table_goal,
coinductive_goal,
answers: Vec::new(),
floundered: false,
answers_hash: FxHashMap::default(),
strands: VecDeque::new(),
answer_mode: AnswerMode::Complete,
}
}
pub(crate) fn enqueue_strand(&mut self, strand: CanonicalStrand<I>) {
self.strands.push_back(strand);
}
pub(crate) fn strands_mut(&mut self) -> impl Iterator<Item = &mut CanonicalStrand<I>> {
self.strands.iter_mut()
}
pub(crate) fn strands(&self) -> impl Iterator<Item = &CanonicalStrand<I>> {
self.strands.iter()
}
pub(crate) fn take_strands(&mut self) -> VecDeque<CanonicalStrand<I>> {
mem::replace(&mut self.strands, VecDeque::new())
}
pub(crate) fn dequeue_next_strand_that(
&mut self,
test: impl Fn(&CanonicalStrand<I>) -> bool,
) -> Option<CanonicalStrand<I>> {
let first = self.strands.iter().position(test);
if let Some(first) = first {
self.strands.rotate_left(first);
self.strands.pop_front()
} else {
None
}
}
pub(crate) fn mark_floundered(&mut self) {
self.floundered = true;
self.strands = Default::default();
self.answers = Default::default();
}
pub(crate) fn is_floundered(&self) -> bool {
self.floundered
}
#[instrument(level = "debug", skip(self))]
pub(super) fn push_answer(&mut self, answer: Answer<I>) -> Option<AnswerIndex> {
assert!(!self.floundered);
debug!(
"pre-existing entry: {:?}",
self.answers_hash.get(&answer.subst)
);
let added = match self.answers_hash.entry(answer.subst.clone()) {
Entry::Vacant(entry) => {
entry.insert(answer.ambiguous);
true
}
Entry::Occupied(entry) => {
let was_ambiguous = entry.get();
if *was_ambiguous && !answer.ambiguous {
panic!("New answer was not ambiguous whereas previous answer was.");
}
false
}
};
info!(
goal = ?self.table_goal, ?answer,
"new answer to table",
);
if !added {
return None;
}
let index = self.answers.len();
self.answers.push(answer);
Some(AnswerIndex::from(index))
}
pub(super) fn answer(&self, index: AnswerIndex) -> Option<&Answer<I>> {
self.answers.get(index.value)
}
pub(super) fn next_answer_index(&self) -> AnswerIndex {
AnswerIndex::from(self.answers.len())
}
}
impl AnswerIndex {
pub(crate) const ZERO: AnswerIndex = AnswerIndex { value: 0 };
}