Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remove leftover chalk types #71758

Merged
merged 1 commit into from
May 2, 2020
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 1 addition & 5 deletions src/librustc_infer/infer/canonical/query_response.rs
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ use crate::infer::nll_relate::{NormalizationStrategy, TypeRelating, TypeRelating
use crate::infer::region_constraints::{Constraint, RegionConstraintData};
use crate::infer::{InferCtxt, InferOk, InferResult, NLLRegionVariableOrigin};
use crate::traits::query::{Fallible, NoSolution};
use crate::traits::{DomainGoal, TraitEngine};
use crate::traits::TraitEngine;
use crate::traits::{Obligation, ObligationCause, PredicateObligation};
use rustc_data_structures::captures::Captures;
use rustc_index::vec::Idx;
Expand Down Expand Up @@ -671,10 +671,6 @@ impl<'tcx> TypeRelatingDelegate<'tcx> for QueryTypeRelatingDelegate<'_, 'tcx> {
});
}

fn push_domain_goal(&mut self, _: DomainGoal<'tcx>) {
bug!("should never be invoked with eager normalization")
}

fn normalization() -> NormalizationStrategy {
NormalizationStrategy::Eager
}
Expand Down
13 changes: 1 addition & 12 deletions src/librustc_infer/infer/nll_relate/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,6 @@

use crate::infer::InferCtxt;
use crate::infer::{ConstVarValue, ConstVariableValue};
use crate::traits::DomainGoal;
use rustc_data_structures::fx::FxHashMap;
use rustc_middle::ty::error::TypeError;
use rustc_middle::ty::fold::{TypeFoldable, TypeVisitor};
Expand Down Expand Up @@ -78,10 +77,6 @@ pub trait TypeRelatingDelegate<'tcx> {
/// delegate.
fn push_outlives(&mut self, sup: ty::Region<'tcx>, sub: ty::Region<'tcx>);

/// Push a domain goal that will need to be proved for the two types to
/// be related. Used for lazy normalization.
fn push_domain_goal(&mut self, domain_goal: DomainGoal<'tcx>);

/// Creates a new universe index. Used when instantiating placeholders.
fn create_next_universe(&mut self) -> ty::UniverseIndex;

Expand Down Expand Up @@ -265,7 +260,6 @@ where
value_ty: Ty<'tcx>,
) -> Ty<'tcx> {
use crate::infer::type_variable::{TypeVariableOrigin, TypeVariableOriginKind};
use crate::traits::WhereClause;
use rustc_span::DUMMY_SP;

match value_ty.kind {
Expand All @@ -279,12 +273,7 @@ where
var
}

_ => {
let projection = ty::ProjectionPredicate { projection_ty, ty: value_ty };
self.delegate
.push_domain_goal(DomainGoal::Holds(WhereClause::ProjectionEq(projection)));
value_ty
}
_ => bug!("should never be invoked with eager normalization"),
}
}

Expand Down
4 changes: 0 additions & 4 deletions src/librustc_interface/passes.rs
Original file line number Diff line number Diff line change
Expand Up @@ -838,10 +838,6 @@ fn analysis(tcx: TyCtxt<'_>, cnum: CrateNum) -> Result<()> {
tcx.par_body_owners(|def_id| tcx.ensure().mir_borrowck(def_id));
});

sess.time("dumping_chalk_like_clauses", || {
rustc_traits::lowering::dump_program_clauses(tcx);
});

sess.time("MIR_effect_checking", || {
for def_id in tcx.body_owners() {
mir::transform::check_unsafety::check_unsafety(tcx, def_id.to_def_id())
Expand Down
1 change: 0 additions & 1 deletion src/librustc_middle/dep_graph/dep_node.rs
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,6 @@

use crate::mir;
use crate::mir::interpret::{GlobalId, LitToConstInput};
use crate::traits;
use crate::traits::query::{
CanonicalPredicateGoal, CanonicalProjectionGoal, CanonicalTyGoal,
CanonicalTypeOpAscribeUserTypeGoal, CanonicalTypeOpEqGoal, CanonicalTypeOpNormalizeGoal,
Expand Down
14 changes: 0 additions & 14 deletions src/librustc_middle/query/mod.rs
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
use crate::dep_graph::SerializedDepNodeIndex;
use crate::mir;
use crate::mir::interpret::{GlobalId, LitToConstInput};
use crate::traits;
use crate::traits::query::{
CanonicalPredicateGoal, CanonicalProjectionGoal, CanonicalTyGoal,
CanonicalTypeOpAscribeUserTypeGoal, CanonicalTypeOpEqGoal, CanonicalTypeOpNormalizeGoal,
Expand Down Expand Up @@ -224,19 +223,6 @@ rustc_queries! {
anon
desc { "erasing regions from `{:?}`", ty }
}

query program_clauses_for(_: DefId) -> Clauses<'tcx> {
desc { "generating chalk-style clauses" }
}

query program_clauses_for_env(_: traits::Environment<'tcx>) -> Clauses<'tcx> {
desc { "generating chalk-style clauses for environment" }
}

// Get the chalk-style environment of the given item.
query environment(_: DefId) -> traits::Environment<'tcx> {
desc { "return a chalk-style environment" }
}
}

Linking {
Expand Down
158 changes: 1 addition & 157 deletions src/librustc_middle/traits/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ mod structural_impls;

use crate::mir::interpret::ErrorHandled;
use crate::ty::subst::SubstsRef;
use crate::ty::{self, AdtKind, List, Ty, TyCtxt};
use crate::ty::{self, AdtKind, Ty, TyCtxt};

use rustc_ast::ast;
use rustc_hir as hir;
Expand Down Expand Up @@ -307,162 +307,6 @@ pub struct DerivedObligationCause<'tcx> {
pub parent_code: Rc<ObligationCauseCode<'tcx>>,
}

/// The following types:
/// * `WhereClause`,
/// * `WellFormed`,
/// * `FromEnv`,
/// * `DomainGoal`,
/// * `Goal`,
/// * `Clause`,
/// * `Environment`,
/// * `InEnvironment`,
/// are used for representing the trait system in the form of
/// logic programming clauses. They are part of the interface
/// for the chalk SLG solver.
#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug, HashStable, TypeFoldable, Lift)]
pub enum WhereClause<'tcx> {
Implemented(ty::TraitPredicate<'tcx>),
ProjectionEq(ty::ProjectionPredicate<'tcx>),
RegionOutlives(ty::RegionOutlivesPredicate<'tcx>),
TypeOutlives(ty::TypeOutlivesPredicate<'tcx>),
}

#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug, HashStable, TypeFoldable, Lift)]
pub enum WellFormed<'tcx> {
Trait(ty::TraitPredicate<'tcx>),
Ty(Ty<'tcx>),
}

#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug, HashStable, TypeFoldable, Lift)]
pub enum FromEnv<'tcx> {
Trait(ty::TraitPredicate<'tcx>),
Ty(Ty<'tcx>),
}

#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug, HashStable, TypeFoldable, Lift)]
pub enum DomainGoal<'tcx> {
Holds(WhereClause<'tcx>),
WellFormed(WellFormed<'tcx>),
FromEnv(FromEnv<'tcx>),
Normalize(ty::ProjectionPredicate<'tcx>),
}

pub type PolyDomainGoal<'tcx> = ty::Binder<DomainGoal<'tcx>>;

#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug, HashStable)]
pub enum QuantifierKind {
Universal,
Existential,
}

#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug, HashStable, TypeFoldable, Lift)]
pub enum GoalKind<'tcx> {
Implies(Clauses<'tcx>, Goal<'tcx>),
And(Goal<'tcx>, Goal<'tcx>),
Not(Goal<'tcx>),
DomainGoal(DomainGoal<'tcx>),
Quantified(QuantifierKind, ty::Binder<Goal<'tcx>>),
Subtype(Ty<'tcx>, Ty<'tcx>),
CannotProve,
}

pub type Goal<'tcx> = &'tcx GoalKind<'tcx>;

pub type Goals<'tcx> = &'tcx List<Goal<'tcx>>;

impl<'tcx> DomainGoal<'tcx> {
pub fn into_goal(self) -> GoalKind<'tcx> {
GoalKind::DomainGoal(self)
}

pub fn into_program_clause(self) -> ProgramClause<'tcx> {
ProgramClause {
goal: self,
hypotheses: ty::List::empty(),
category: ProgramClauseCategory::Other,
}
}
}

impl<'tcx> GoalKind<'tcx> {
pub fn from_poly_domain_goal(
domain_goal: PolyDomainGoal<'tcx>,
tcx: TyCtxt<'tcx>,
) -> GoalKind<'tcx> {
match domain_goal.no_bound_vars() {
Some(p) => p.into_goal(),
None => GoalKind::Quantified(
QuantifierKind::Universal,
domain_goal.map_bound(|p| tcx.mk_goal(p.into_goal())),
),
}
}
}

/// This matches the definition from Page 7 of "A Proof Procedure for the Logic of Hereditary
/// Harrop Formulas".
#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug, HashStable, TypeFoldable)]
pub enum Clause<'tcx> {
Implies(ProgramClause<'tcx>),
ForAll(ty::Binder<ProgramClause<'tcx>>),
}

impl Clause<'tcx> {
pub fn category(self) -> ProgramClauseCategory {
match self {
Clause::Implies(clause) => clause.category,
Clause::ForAll(clause) => clause.skip_binder().category,
}
}
}

/// Multiple clauses.
pub type Clauses<'tcx> = &'tcx List<Clause<'tcx>>;

/// A "program clause" has the form `D :- G1, ..., Gn`. It is saying
/// that the domain goal `D` is true if `G1...Gn` are provable. This
/// is equivalent to the implication `G1..Gn => D`; we usually write
/// it with the reverse implication operator `:-` to emphasize the way
/// that programs are actually solved (via backchaining, which starts
/// with the goal to solve and proceeds from there).
#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug, HashStable, TypeFoldable)]
pub struct ProgramClause<'tcx> {
/// This goal will be considered true ...
pub goal: DomainGoal<'tcx>,

/// ... if we can prove these hypotheses (there may be no hypotheses at all):
pub hypotheses: Goals<'tcx>,

/// Useful for filtering clauses.
pub category: ProgramClauseCategory,
}

#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug, HashStable)]
pub enum ProgramClauseCategory {
ImpliedBound,
WellFormed,
Other,
}

/// A set of clauses that we assume to be true.
#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug, HashStable, TypeFoldable)]
pub struct Environment<'tcx> {
pub clauses: Clauses<'tcx>,
}

impl Environment<'tcx> {
pub fn with<G>(self, goal: G) -> InEnvironment<'tcx, G> {
InEnvironment { environment: self, goal }
}
}

/// Something (usually a goal), along with an environment.
#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug, HashStable, TypeFoldable)]
pub struct InEnvironment<'tcx, G> {
pub environment: Environment<'tcx>,
pub goal: G,
}

#[derive(Clone, Debug, TypeFoldable)]
pub enum SelectionError<'tcx> {
Unimplemented,
Expand Down
Loading