1 use crate::index_struct
;
2 use crate::strand
::CanonicalStrand
;
3 use crate::{Answer, AnswerMode}
;
4 use rustc_hash
::FxHashMap
;
5 use std
::collections
::hash_map
::Entry
;
6 use std
::collections
::VecDeque
;
9 use chalk_ir
::interner
::Interner
;
10 use chalk_ir
::{AnswerSubst, Canonical, Goal, InEnvironment, UCanonical}
;
11 use tracing
::{debug, info, instrument}
;
13 pub(crate) struct Table
<I
: Interner
> {
14 /// The goal this table is trying to solve (also the key to look
16 pub(crate) table_goal
: UCanonical
<InEnvironment
<Goal
<I
>>>,
18 /// A goal is coinductive if it can assume itself to be true, more
19 /// or less. This is true for auto traits.
20 pub(crate) coinductive_goal
: bool
,
22 /// True if this table is floundered, meaning that it doesn't have
23 /// enough types specified for us to solve.
26 /// Stores the answers that we have found thus far. When we get a request
27 /// for an answer N, we will first check this vector.
28 answers
: Vec
<Answer
<I
>>,
30 /// An alternative storage for the answers we have so far, used to
31 /// detect duplicates. Not every answer in `answers` will be
32 /// represented here -- we discard answers from `answers_hash`
33 /// (but not `answers`) when better answers arrive (in particular,
34 /// answers with no ambiguity).
36 /// FIXME -- Ideally we would exclude the region constraints and
37 /// delayed subgoals from the hash, but that's a bit tricky to do
38 /// with the current canonicalization setup. It should be ok not
39 /// to do so though it can result in more answers than we need.
40 answers_hash
: FxHashMap
<Canonical
<AnswerSubst
<I
>>, bool
>,
42 /// Stores the active strands that we can "pull on" to find more
44 strands
: VecDeque
<CanonicalStrand
<I
>>,
46 pub(crate) answer_mode
: AnswerMode
,
50 pub(crate) struct AnswerIndex
{
55 impl<I
: Interner
> Table
<I
> {
57 table_goal
: UCanonical
<InEnvironment
<Goal
<I
>>>,
58 coinductive_goal
: bool
,
65 answers_hash
: FxHashMap
::default(),
66 strands
: VecDeque
::new(),
67 answer_mode
: AnswerMode
::Complete
,
71 /// Push a strand to the back of the queue of strands to be processed.
72 pub(crate) fn enqueue_strand(&mut self, strand
: CanonicalStrand
<I
>) {
73 self.strands
.push_back(strand
);
76 pub(crate) fn strands_mut(&mut self) -> impl Iterator
<Item
= &mut CanonicalStrand
<I
>> {
77 self.strands
.iter_mut()
80 pub(crate) fn strands(&self) -> impl Iterator
<Item
= &CanonicalStrand
<I
>> {
84 pub(crate) fn take_strands(&mut self) -> VecDeque
<CanonicalStrand
<I
>> {
85 mem
::replace(&mut self.strands
, VecDeque
::new())
88 pub(crate) fn drain_strands(
90 test
: impl Fn(&CanonicalStrand
<I
>) -> bool
,
91 ) -> VecDeque
<CanonicalStrand
<I
>> {
92 let old
= mem
::replace(&mut self.strands
, VecDeque
::new());
93 let (test_in
, test_out
): (VecDeque
<CanonicalStrand
<I
>>, VecDeque
<CanonicalStrand
<I
>>) =
94 old
.into_iter().partition(test
);
95 let _
= mem
::replace(&mut self.strands
, test_out
);
99 /// Remove the next strand from the queue that meets the given criteria
100 pub(crate) fn dequeue_next_strand_that(
102 test
: impl Fn(&CanonicalStrand
<I
>) -> bool
,
103 ) -> Option
<CanonicalStrand
<I
>> {
104 let first
= self.strands
.iter().position(test
);
105 if let Some(first
) = first
{
106 self.strands
.rotate_left(first
);
107 self.strands
.pop_front()
113 /// Mark the table as floundered -- this also discards all pre-existing answers,
114 /// as they are no longer relevant.
115 pub(crate) fn mark_floundered(&mut self) {
116 self.floundered
= true;
117 self.strands
= Default
::default();
118 self.answers
= Default
::default();
121 /// Returns true if the table is floundered.
122 pub(crate) fn is_floundered(&self) -> bool
{
126 /// Adds `answer` to our list of answers, unless it is already present.
128 /// Returns true if `answer` was added.
131 /// This will panic if a previous answer with the same substitution
132 /// was marked as ambgiuous, but the new answer is not. No current
133 /// tests trigger this case, and assumptions upstream assume that when
134 /// `true` is returned here, that a *new* answer was added (instead of an)
135 /// existing answer replaced.
136 #[instrument(level = "debug", skip(self))]
137 pub(super) fn push_answer(&mut self, answer
: Answer
<I
>) -> Option
<AnswerIndex
> {
138 assert
!(!self.floundered
);
140 "pre-existing entry: {:?}",
141 self.answers_hash
.get(&answer
.subst
)
144 let added
= match self.answers_hash
.entry(answer
.subst
.clone()) {
145 Entry
::Vacant(entry
) => {
146 entry
.insert(answer
.ambiguous
);
150 Entry
::Occupied(entry
) => {
151 let was_ambiguous
= entry
.get();
152 if *was_ambiguous
&& !answer
.ambiguous
{
153 panic
!("New answer was not ambiguous whereas previous answer was.");
160 "new answer to table with goal {:?}: answer={:?}",
161 self.table_goal
, answer
,
167 let index
= self.answers
.len();
168 self.answers
.push(answer
);
169 Some(AnswerIndex
::from(index
))
172 pub(super) fn answer(&self, index
: AnswerIndex
) -> Option
<&Answer
<I
>> {
173 self.answers
.get(index
.value
)
176 pub(super) fn next_answer_index(&self) -> AnswerIndex
{
177 AnswerIndex
::from(self.answers
.len())
182 pub(crate) const ZERO
: AnswerIndex
= AnswerIndex { value: 0 }
;