]>
Commit | Line | Data |
---|---|---|
f035d41b | 1 | use crate::index_struct; |
f9f354fc | 2 | use crate::strand::CanonicalStrand; |
f035d41b | 3 | use crate::{Answer, AnswerMode}; |
f9f354fc XL |
4 | use rustc_hash::FxHashMap; |
5 | use std::collections::hash_map::Entry; | |
6 | use std::collections::VecDeque; | |
7 | use std::mem; | |
8 | ||
f035d41b XL |
9 | use chalk_ir::interner::Interner; |
10 | use chalk_ir::{AnswerSubst, Canonical, Goal, InEnvironment, UCanonical}; | |
11 | use tracing::{debug, info, instrument}; | |
12 | ||
13 | pub(crate) struct Table<I: Interner> { | |
f9f354fc XL |
14 | /// The goal this table is trying to solve (also the key to look |
15 | /// it up). | |
f035d41b | 16 | pub(crate) table_goal: UCanonical<InEnvironment<Goal<I>>>, |
f9f354fc XL |
17 | |
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, | |
21 | ||
22 | /// True if this table is floundered, meaning that it doesn't have | |
23 | /// enough types specified for us to solve. | |
24 | floundered: bool, | |
25 | ||
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. | |
f035d41b | 28 | answers: Vec<Answer<I>>, |
f9f354fc XL |
29 | |
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). | |
35 | /// | |
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. | |
f035d41b | 40 | answers_hash: FxHashMap<Canonical<AnswerSubst<I>>, bool>, |
f9f354fc XL |
41 | |
42 | /// Stores the active strands that we can "pull on" to find more | |
43 | /// answers. | |
f035d41b XL |
44 | strands: VecDeque<CanonicalStrand<I>>, |
45 | ||
46 | pub(crate) answer_mode: AnswerMode, | |
f9f354fc XL |
47 | } |
48 | ||
49 | index_struct! { | |
50 | pub(crate) struct AnswerIndex { | |
51 | value: usize, | |
52 | } | |
53 | } | |
54 | ||
f035d41b | 55 | impl<I: Interner> Table<I> { |
f9f354fc | 56 | pub(crate) fn new( |
f035d41b | 57 | table_goal: UCanonical<InEnvironment<Goal<I>>>, |
f9f354fc | 58 | coinductive_goal: bool, |
f035d41b | 59 | ) -> Table<I> { |
f9f354fc XL |
60 | Table { |
61 | table_goal, | |
62 | coinductive_goal, | |
63 | answers: Vec::new(), | |
64 | floundered: false, | |
65 | answers_hash: FxHashMap::default(), | |
66 | strands: VecDeque::new(), | |
f035d41b | 67 | answer_mode: AnswerMode::Complete, |
f9f354fc XL |
68 | } |
69 | } | |
70 | ||
71 | /// Push a strand to the back of the queue of strands to be processed. | |
f035d41b | 72 | pub(crate) fn enqueue_strand(&mut self, strand: CanonicalStrand<I>) { |
f9f354fc XL |
73 | self.strands.push_back(strand); |
74 | } | |
75 | ||
f035d41b | 76 | pub(crate) fn strands_mut(&mut self) -> impl Iterator<Item = &mut CanonicalStrand<I>> { |
f9f354fc XL |
77 | self.strands.iter_mut() |
78 | } | |
79 | ||
f035d41b | 80 | pub(crate) fn strands(&self) -> impl Iterator<Item = &CanonicalStrand<I>> { |
f9f354fc XL |
81 | self.strands.iter() |
82 | } | |
83 | ||
f035d41b | 84 | pub(crate) fn take_strands(&mut self) -> VecDeque<CanonicalStrand<I>> { |
f9f354fc XL |
85 | mem::replace(&mut self.strands, VecDeque::new()) |
86 | } | |
87 | ||
f035d41b | 88 | pub(crate) fn drain_strands( |
f9f354fc | 89 | &mut self, |
f035d41b XL |
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); | |
96 | test_in | |
97 | } | |
98 | ||
99 | /// Remove the next strand from the queue that meets the given criteria | |
100 | pub(crate) fn dequeue_next_strand_that( | |
101 | &mut self, | |
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() | |
108 | } else { | |
109 | None | |
f9f354fc | 110 | } |
f9f354fc XL |
111 | } |
112 | ||
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(); | |
119 | } | |
120 | ||
121 | /// Returns true if the table is floundered. | |
122 | pub(crate) fn is_floundered(&self) -> bool { | |
123 | self.floundered | |
124 | } | |
125 | ||
126 | /// Adds `answer` to our list of answers, unless it is already present. | |
127 | /// | |
128 | /// Returns true if `answer` was added. | |
129 | /// | |
130 | /// # Panics | |
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. | |
f035d41b XL |
136 | #[instrument(level = "debug", skip(self))] |
137 | pub(super) fn push_answer(&mut self, answer: Answer<I>) -> Option<AnswerIndex> { | |
f9f354fc | 138 | assert!(!self.floundered); |
f9f354fc XL |
139 | debug!( |
140 | "pre-existing entry: {:?}", | |
141 | self.answers_hash.get(&answer.subst) | |
142 | ); | |
143 | ||
144 | let added = match self.answers_hash.entry(answer.subst.clone()) { | |
145 | Entry::Vacant(entry) => { | |
146 | entry.insert(answer.ambiguous); | |
147 | true | |
148 | } | |
149 | ||
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."); | |
154 | } | |
155 | false | |
156 | } | |
157 | }; | |
158 | ||
159 | info!( | |
160 | "new answer to table with goal {:?}: answer={:?}", | |
161 | self.table_goal, answer, | |
162 | ); | |
163 | if !added { | |
164 | return None; | |
165 | } | |
166 | ||
167 | let index = self.answers.len(); | |
168 | self.answers.push(answer); | |
169 | Some(AnswerIndex::from(index)) | |
170 | } | |
171 | ||
f035d41b | 172 | pub(super) fn answer(&self, index: AnswerIndex) -> Option<&Answer<I>> { |
f9f354fc XL |
173 | self.answers.get(index.value) |
174 | } | |
175 | ||
176 | pub(super) fn next_answer_index(&self) -> AnswerIndex { | |
177 | AnswerIndex::from(self.answers.len()) | |
178 | } | |
179 | } | |
180 | ||
181 | impl AnswerIndex { | |
182 | pub(crate) const ZERO: AnswerIndex = AnswerIndex { value: 0 }; | |
183 | } |