blob: d8b3a061b77d563aa2699c7aed30749c0a12b0c6 [file] [log] [blame]
use super::{
CandidateSource, CanonicalInput, Certainty, Goal, IsNormalizesToHack, NoSolution, QueryInput,
QueryResult,
};
use crate::ty;
use format::ProofTreeFormatter;
use std::fmt::{Debug, Write};
mod format;
#[derive(Debug, Eq, PartialEq)]
pub enum CacheHit {
Provisional,
Global,
}
#[derive(Eq, PartialEq)]
pub struct GoalEvaluation<'tcx> {
pub uncanonicalized_goal: Goal<'tcx, ty::Predicate<'tcx>>,
pub is_normalizes_to_hack: IsNormalizesToHack,
pub evaluation: CanonicalGoalEvaluation<'tcx>,
pub returned_goals: Vec<Goal<'tcx, ty::Predicate<'tcx>>>,
}
#[derive(Eq, PartialEq)]
pub struct CanonicalGoalEvaluation<'tcx> {
pub goal: CanonicalInput<'tcx>,
pub kind: GoalEvaluationKind<'tcx>,
pub result: QueryResult<'tcx>,
}
#[derive(Eq, PartialEq)]
pub enum GoalEvaluationKind<'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: GoalCandidate<'tcx>,
}
#[derive(Eq, PartialEq)]
pub struct GoalCandidate<'tcx> {
pub added_goals_evaluations: Vec<AddedGoalsEvaluation<'tcx>>,
pub candidates: Vec<GoalCandidate<'tcx>>,
pub kind: ProbeKind<'tcx>,
}
impl Debug for GoalCandidate<'_> {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
ProofTreeFormatter::new(f).format_candidate(self)
}
}
#[derive(Debug, PartialEq, Eq)]
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,
}