1
Fork 0

initial info dump

This commit is contained in:
Boxy 2023-06-08 19:10:07 +01:00
parent 8d1fa473dd
commit 3009b2c647
11 changed files with 929 additions and 402 deletions

View file

@ -981,7 +981,7 @@ pub enum CodegenObligationError {
FulfillmentError,
}
#[derive(Debug, PartialEq, Eq, Clone, Copy, Hash, TypeFoldable, TypeVisitable)]
#[derive(Debug, PartialEq, Eq, Clone, Copy, Hash, HashStable, TypeFoldable, TypeVisitable)]
pub enum DefiningAnchor {
/// `DefId` of the item.
Bind(LocalDefId),

View file

@ -92,7 +92,7 @@ pub type CanonicalTypeOpProvePredicateGoal<'tcx> =
pub type CanonicalTypeOpNormalizeGoal<'tcx, T> =
Canonical<'tcx, ty::ParamEnvAnd<'tcx, type_op::Normalize<T>>>;
#[derive(Copy, Clone, Debug, HashStable, PartialEq, Eq)]
#[derive(Copy, Clone, Debug, Hash, HashStable, PartialEq, Eq)]
pub struct NoSolution;
impl<'tcx> From<TypeError<'tcx>> for NoSolution {

View file

@ -11,6 +11,8 @@ use crate::ty::{
TypeVisitor,
};
pub mod inspect;
pub type EvaluationCache<'tcx> = Cache<CanonicalInput<'tcx>, QueryResult<'tcx>>;
/// A goal is a statement, i.e. `predicate`, we want to prove
@ -18,7 +20,7 @@ pub type EvaluationCache<'tcx> = Cache<CanonicalInput<'tcx>, QueryResult<'tcx>>;
///
/// Most of the time the `param_env` contains the `where`-bounds of the function
/// we're currently typechecking while the `predicate` is some trait bound.
#[derive(Debug, PartialEq, Eq, Clone, Copy, Hash, TypeFoldable, TypeVisitable)]
#[derive(Debug, PartialEq, Eq, Clone, Copy, Hash, HashStable, TypeFoldable, TypeVisitable)]
pub struct Goal<'tcx, P> {
pub predicate: P,
pub param_env: ty::ParamEnv<'tcx>,
@ -39,7 +41,7 @@ impl<'tcx, P> Goal<'tcx, P> {
}
}
#[derive(Debug, PartialEq, Eq, Clone, Copy, Hash, TypeFoldable, TypeVisitable)]
#[derive(Debug, PartialEq, Eq, Clone, Copy, Hash, HashStable, TypeFoldable, TypeVisitable)]
pub struct Response<'tcx> {
pub certainty: Certainty,
pub var_values: CanonicalVarValues<'tcx>,
@ -47,7 +49,7 @@ pub struct Response<'tcx> {
pub external_constraints: ExternalConstraints<'tcx>,
}
#[derive(Debug, PartialEq, Eq, Clone, Copy, Hash, TypeFoldable, TypeVisitable)]
#[derive(Debug, PartialEq, Eq, Clone, Copy, Hash, HashStable, TypeFoldable, TypeVisitable)]
pub enum Certainty {
Yes,
Maybe(MaybeCause),
@ -86,7 +88,7 @@ impl Certainty {
}
/// Why we failed to evaluate a goal.
#[derive(Debug, PartialEq, Eq, Clone, Copy, Hash, TypeFoldable, TypeVisitable)]
#[derive(Debug, PartialEq, Eq, Clone, Copy, Hash, HashStable, TypeFoldable, TypeVisitable)]
pub enum MaybeCause {
/// We failed due to ambiguity. This ambiguity can either
/// be a true ambiguity, i.e. there are multiple different answers,
@ -96,7 +98,7 @@ pub enum MaybeCause {
Overflow,
}
#[derive(Debug, PartialEq, Eq, Clone, Copy, Hash, TypeFoldable, TypeVisitable)]
#[derive(Debug, PartialEq, Eq, Clone, Copy, Hash, HashStable, TypeFoldable, TypeVisitable)]
pub struct QueryInput<'tcx, T> {
pub goal: Goal<'tcx, T>,
pub anchor: DefiningAnchor,
@ -104,12 +106,12 @@ pub struct QueryInput<'tcx, T> {
}
/// Additional constraints returned on success.
#[derive(Debug, PartialEq, Eq, Clone, Hash, Default)]
#[derive(Debug, PartialEq, Eq, Clone, Hash, HashStable, Default)]
pub struct PredefinedOpaquesData<'tcx> {
pub opaque_types: Vec<(ty::OpaqueTypeKey<'tcx>, Ty<'tcx>)>,
}
#[derive(Debug, PartialEq, Eq, Copy, Clone, Hash)]
#[derive(Debug, PartialEq, Eq, Copy, Clone, Hash, HashStable)]
pub struct PredefinedOpaques<'tcx>(pub(crate) Interned<'tcx, PredefinedOpaquesData<'tcx>>);
impl<'tcx> std::ops::Deref for PredefinedOpaques<'tcx> {
@ -132,7 +134,7 @@ pub type CanonicalResponse<'tcx> = Canonical<'tcx, Response<'tcx>>;
/// solver, merge the two responses again.
pub type QueryResult<'tcx> = Result<CanonicalResponse<'tcx>, NoSolution>;
#[derive(Debug, PartialEq, Eq, Copy, Clone, Hash)]
#[derive(Debug, PartialEq, Eq, Copy, Clone, Hash, HashStable)]
pub struct ExternalConstraints<'tcx>(pub(crate) Interned<'tcx, ExternalConstraintsData<'tcx>>);
impl<'tcx> std::ops::Deref for ExternalConstraints<'tcx> {
@ -144,7 +146,7 @@ impl<'tcx> std::ops::Deref for ExternalConstraints<'tcx> {
}
/// Additional constraints returned on success.
#[derive(Debug, PartialEq, Eq, Clone, Hash, Default)]
#[derive(Debug, PartialEq, Eq, Clone, Hash, HashStable, Default)]
pub struct ExternalConstraintsData<'tcx> {
// FIXME: implement this.
pub region_constraints: QueryRegionConstraints<'tcx>,

View file

@ -0,0 +1,168 @@
use super::{CanonicalInput, Certainty, Goal, NoSolution, QueryInput, QueryResult};
use crate::ty;
use std::fmt::{Debug, Write};
#[derive(Eq, PartialEq, Hash, HashStable)]
pub struct GoalEvaluation<'tcx> {
pub uncanonicalized_goal: Goal<'tcx, ty::Predicate<'tcx>>,
pub canonicalized_goal: Option<CanonicalInput<'tcx>>,
/// To handle coinductive cycles we can end up re-evaluating a goal
/// multiple times with different results for a nested goal. Each rerun
/// is represented as an entry in this vec.
pub evaluation_steps: Vec<GoalEvaluationStep<'tcx>>,
pub cache_hit: bool,
pub result: Option<QueryResult<'tcx>>,
}
impl Debug for GoalEvaluation<'_> {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
ProofTreeFormatter { f, on_newline: true }.format_goal_evaluation(self)
}
}
#[derive(Eq, PartialEq, Hash, HashStable)]
pub struct AddedGoalsEvaluation<'tcx> {
pub evaluations: Vec<Vec<GoalEvaluation<'tcx>>>,
pub result: Option<Result<Certainty, NoSolution>>,
}
impl Debug for AddedGoalsEvaluation<'_> {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
ProofTreeFormatter { f, on_newline: true }.format_nested_goal_evaluation(self)
}
}
#[derive(Eq, PartialEq, Hash, HashStable)]
pub struct GoalEvaluationStep<'tcx> {
pub instantiated_goal: QueryInput<'tcx, ty::Predicate<'tcx>>,
pub nested_goal_evaluations: Vec<AddedGoalsEvaluation<'tcx>>,
pub candidates: Vec<GoalCandidate<'tcx>>,
pub result: Option<QueryResult<'tcx>>,
}
impl Debug for GoalEvaluationStep<'_> {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
ProofTreeFormatter { f, on_newline: true }.format_evaluation_step(self)
}
}
#[derive(Eq, PartialEq, Hash, HashStable)]
pub struct GoalCandidate<'tcx> {
pub nested_goal_evaluations: Vec<AddedGoalsEvaluation<'tcx>>,
pub candidates: Vec<GoalCandidate<'tcx>>,
pub name: Option<String>,
pub result: Option<QueryResult<'tcx>>,
}
impl Debug for GoalCandidate<'_> {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
ProofTreeFormatter { f, on_newline: true }.format_candidate(self)
}
}
struct ProofTreeFormatter<'a, 'b> {
f: &'a mut (dyn Write + 'b),
on_newline: bool,
}
impl Write for ProofTreeFormatter<'_, '_> {
fn write_str(&mut self, s: &str) -> std::fmt::Result {
for line in s.split_inclusive("\n") {
if self.on_newline {
self.f.write_str(" ")?;
}
self.on_newline = line.ends_with("\n");
self.f.write_str(line)?;
}
Ok(())
}
}
impl ProofTreeFormatter<'_, '_> {
fn nested(&mut self) -> ProofTreeFormatter<'_, '_> {
ProofTreeFormatter { f: self, on_newline: true }
}
fn format_goal_evaluation(&mut self, goal: &GoalEvaluation<'_>) -> std::fmt::Result {
let f = &mut *self.f;
writeln!(f, "GOAL: {:?}", goal.uncanonicalized_goal)?;
writeln!(f, "CANONICALIZED: {:?}", goal.canonicalized_goal)?;
match goal.cache_hit {
true => writeln!(f, "CACHE HIT: {:?}", goal.result),
false => {
for (n, step) in goal.evaluation_steps.iter().enumerate() {
let f = &mut *self.f;
writeln!(f, "REVISION {n}: {:?}", step.result.unwrap())?;
let mut f = self.nested();
f.format_evaluation_step(step)?;
}
let f = &mut *self.f;
writeln!(f, "RESULT: {:?}", goal.result.unwrap())
}
}
}
fn format_evaluation_step(
&mut self,
evaluation_step: &GoalEvaluationStep<'_>,
) -> std::fmt::Result {
let f = &mut *self.f;
writeln!(f, "INSTANTIATED: {:?}", evaluation_step.instantiated_goal)?;
for candidate in &evaluation_step.candidates {
let mut f = self.nested();
f.format_candidate(candidate)?;
}
for nested_goal_evaluation in &evaluation_step.nested_goal_evaluations {
let mut f = self.nested();
f.format_nested_goal_evaluation(nested_goal_evaluation)?;
}
Ok(())
}
fn format_candidate(&mut self, candidate: &GoalCandidate<'_>) -> std::fmt::Result {
let f = &mut *self.f;
match (candidate.name.as_ref(), candidate.result) {
(Some(name), Some(result)) => writeln!(f, "CANDIDATE {}: {:?}", name, result,)?,
(None, None) => writeln!(f, "MISC PROBE")?,
(None, Some(_)) => unreachable!("unexpected probe with no name but a result"),
(Some(_), None) => unreachable!("unexpected probe with a name but no candidate"),
};
let mut f = self.nested();
for candidate in &candidate.candidates {
f.format_candidate(candidate)?;
}
for nested_evaluations in &candidate.nested_goal_evaluations {
f.format_nested_goal_evaluation(nested_evaluations)?;
}
Ok(())
}
fn format_nested_goal_evaluation(
&mut self,
nested_goal_evaluation: &AddedGoalsEvaluation<'_>,
) -> std::fmt::Result {
let f = &mut *self.f;
writeln!(f, "TRY_EVALUATE_ADDED_GOALS: {:?}", nested_goal_evaluation.result.unwrap())?;
for (n, revision) in nested_goal_evaluation.evaluations.iter().enumerate() {
let f = &mut *self.f;
writeln!(f, "REVISION {n}")?;
let mut f = self.nested();
for goal_evaluation in revision {
f.format_goal_evaluation(goal_evaluation)?;
}
}
Ok(())
}
}