1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173
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> {
/// The goal this table is trying to solve (also the key to look
/// it up).
pub(crate) table_goal: UCanonical<InEnvironment<Goal<I>>>,
/// A goal is coinductive if it can assume itself to be true, more
/// or less. This is true for auto traits.
pub(crate) coinductive_goal: bool,
/// True if this table is floundered, meaning that it doesn't have
/// enough types specified for us to solve.
floundered: bool,
/// Stores the answers that we have found thus far. When we get a request
/// for an answer N, we will first check this vector.
answers: Vec<Answer<I>>,
/// An alternative storage for the answers we have so far, used to
/// detect duplicates. Not every answer in `answers` will be
/// represented here -- we discard answers from `answers_hash`
/// (but not `answers`) when better answers arrive (in particular,
/// answers with no ambiguity).
///
/// FIXME -- Ideally we would exclude the region constraints and
/// delayed subgoals from the hash, but that's a bit tricky to do
/// with the current canonicalization setup. It should be ok not
/// to do so though it can result in more answers than we need.
answers_hash: FxHashMap<Canonical<AnswerSubst<I>>, bool>,
/// Stores the active strands that we can "pull on" to find more
/// answers.
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,
}
}
/// Push a strand to the back of the queue of strands to be processed.
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::take(&mut self.strands)
}
/// Remove the next strand from the queue that meets the given criteria
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
}
}
/// Mark the table as floundered -- this also discards all pre-existing answers,
/// as they are no longer relevant.
pub(crate) fn mark_floundered(&mut self) {
self.floundered = true;
self.strands = Default::default();
self.answers = Default::default();
}
/// Returns true if the table is floundered.
pub(crate) fn is_floundered(&self) -> bool {
self.floundered
}
/// Adds `answer` to our list of answers, unless it is already present.
///
/// Returns true if `answer` was added.
///
/// # Panics
/// This will panic if a previous answer with the same substitution
/// was marked as ambgiuous, but the new answer is not. No current
/// tests trigger this case, and assumptions upstream assume that when
/// `true` is returned here, that a *new* answer was added (instead of an)
/// existing answer replaced.
#[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 };
}