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
//! Data structure used to inspect trait solver behavior.
//!
//! During trait solving we optionally build "proof trees", the root of
//! which is a [GoalEvaluation] with [GoalEvaluationKind::Root]. These
//! trees are used to improve the debug experience and are also used by
//! the compiler itself to provide necessary context for error messages.
//!
//! Because each nested goal in the solver gets [canonicalized] separately
//! and we discard inference progress via "probes", we cannot mechanically
//! use proof trees without somehow "lifting up" data local to the current
//! `InferCtxt`. Any data used mechanically is therefore canonicalized and
//! stored as [CanonicalState]. As printing canonicalized data worsens the
//! debugging dumps, we do not simply canonicalize everything.
//!
//! This means proof trees contain inference variables and placeholders
//! local to a different `InferCtxt` which must not be used with the
//! current one.
//!
//! [canonicalized]: https://rustc-dev-guide.rust-lang.org/solve/canonicalization.html

use super::{
    CandidateSource, Canonical, CanonicalInput, Certainty, Goal, IsNormalizesToHack, NoSolution,
    QueryInput, QueryResult,
};
use crate::{infer::canonical::CanonicalVarValues, ty};
use format::ProofTreeFormatter;
use std::fmt::{Debug, Write};

mod format;

/// Some `data` together with information about how they relate to the input
/// of the canonical query.
///
/// This is only ever used as [CanonicalState]. Any type information in proof
/// trees used mechanically has to be canonicalized as we otherwise leak
/// inference variables from a nested `InferCtxt`.
#[derive(Debug, Clone, Copy, Eq, PartialEq, TypeFoldable, TypeVisitable)]
pub struct State<'tcx, T> {
    pub var_values: CanonicalVarValues<'tcx>,
    pub data: T,
}

pub type CanonicalState<'tcx, T> = Canonical<'tcx, State<'tcx, T>>;

#[derive(Debug, Eq, PartialEq)]
pub enum CacheHit {
    Provisional,
    Global,
}

/// When evaluating the root goals we also store the
/// original values for the `CanonicalVarValues` of the
/// canonicalized goal. We use this to map any [CanonicalState]
/// from the local `InferCtxt` of the solver query to
/// the `InferCtxt` of the caller.
#[derive(Eq, PartialEq)]
pub enum GoalEvaluationKind<'tcx> {
    Root { orig_values: Vec<ty::GenericArg<'tcx>> },
    Nested { is_normalizes_to_hack: IsNormalizesToHack },
}

#[derive(Eq, PartialEq)]
pub struct GoalEvaluation<'tcx> {
    pub uncanonicalized_goal: Goal<'tcx, ty::Predicate<'tcx>>,
    pub kind: GoalEvaluationKind<'tcx>,
    pub evaluation: CanonicalGoalEvaluation<'tcx>,
    /// The nested goals from instantiating the query response.
    pub returned_goals: Vec<Goal<'tcx, ty::Predicate<'tcx>>>,
}

#[derive(Eq, PartialEq)]
pub struct CanonicalGoalEvaluation<'tcx> {
    pub goal: CanonicalInput<'tcx>,
    pub kind: CanonicalGoalEvaluationKind<'tcx>,
    pub result: QueryResult<'tcx>,
}

#[derive(Eq, PartialEq)]
pub enum CanonicalGoalEvaluationKind<'tcx> {
    Overflow,
    CacheHit(CacheHit),
    Uncached { revisions: Vec<GoalEvaluationStep<'tcx>> },
}
impl Debug for GoalEvaluation<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        ProofTreeFormatter::new(f).format_goal_evaluation(self)
    }
}

#[derive(Eq, PartialEq)]
pub struct AddedGoalsEvaluation<'tcx> {
    pub evaluations: Vec<Vec<GoalEvaluation<'tcx>>>,
    pub result: Result<Certainty, NoSolution>,
}

#[derive(Eq, PartialEq)]
pub struct GoalEvaluationStep<'tcx> {
    pub instantiated_goal: QueryInput<'tcx, ty::Predicate<'tcx>>,

    /// The actual evaluation of the goal, always `ProbeKind::Root`.
    pub evaluation: Probe<'tcx>,
}

/// A self-contained computation during trait solving. This either
/// corresponds to a `EvalCtxt::probe(_X)` call or the root evaluation
/// of a goal.
#[derive(Eq, PartialEq)]
pub struct Probe<'tcx> {
    /// What happened inside of this probe in chronological order.
    pub steps: Vec<ProbeStep<'tcx>>,
    pub kind: ProbeKind<'tcx>,
}

impl Debug for Probe<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        ProofTreeFormatter::new(f).format_probe(self)
    }
}

#[derive(Eq, PartialEq)]
pub enum ProbeStep<'tcx> {
    /// We added a goal to the `EvalCtxt` which will get proven
    /// the next time `EvalCtxt::try_evaluate_added_goals` is called.
    AddGoal(CanonicalState<'tcx, Goal<'tcx, ty::Predicate<'tcx>>>),
    /// The inside of a `EvalCtxt::try_evaluate_added_goals` call.
    EvaluateGoals(AddedGoalsEvaluation<'tcx>),
    /// A call to `probe` while proving the current goal. This is
    /// used whenever there are multiple candidates to prove the
    /// current goalby .
    NestedProbe(Probe<'tcx>),
}

/// What kind of probe we're in. In case the probe represents a candidate, or
/// the final result of the current goal - via [ProbeKind::Root] - we also
/// store the [QueryResult].
#[derive(Debug, PartialEq, Eq, Clone, Copy)]
pub enum ProbeKind<'tcx> {
    /// The root inference context while proving a goal.
    Root { result: QueryResult<'tcx> },
    /// Probe entered when normalizing the self ty during candidate assembly
    NormalizedSelfTyAssembly,
    /// Some candidate to prove the current goal.
    ///
    /// FIXME: Remove this in favor of always using more strongly typed variants.
    MiscCandidate { name: &'static str, result: QueryResult<'tcx> },
    /// A candidate for proving a trait or alias-relate goal.
    TraitCandidate { source: CandidateSource, result: QueryResult<'tcx> },
    /// Used in the probe that wraps normalizing the non-self type for the unsize
    /// trait, which is also structurally matched on.
    UnsizeAssembly,
    /// During upcasting from some source object to target object type, used to
    /// do a probe to find out what projection type(s) may be used to prove that
    /// the source type upholds all of the target type's object bounds.
    UpcastProjectionCompatibility,
}