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 };
}