Skip to content

Commit

Permalink
Auto merge of #661 - jackh726:cleanup, r=nikomatsakis
Browse files Browse the repository at this point in the history
Some various bits of cleanup

- Remove the `InferenceTable`-like traits in engine and recursive
- In chalk-engine, do some refactoring around `Strand`
    - Pass around `CanonicalStrand` almost everywhere and instantiate as-needed
    - Make `Strand` not have the `InferenceTable` and make `CanonicalStrand` just `Canonical<Strand>`
- Make `Variances` share more code with other slice interners
  • Loading branch information
bors committed Jan 26, 2021
2 parents 750184a + 17512fc commit 9332c49
Show file tree
Hide file tree
Showing 16 changed files with 505 additions and 866 deletions.
415 changes: 224 additions & 191 deletions chalk-engine/src/logic.rs

Large diffs are not rendered by default.

4 changes: 2 additions & 2 deletions chalk-engine/src/normalize_deep.rs
Original file line number Diff line number Diff line change
Expand Up @@ -120,11 +120,11 @@ mod test {
struct TestDatabase;
impl UnificationDatabase<ChalkIr> for TestDatabase {
fn fn_def_variance(&self, _fn_def_id: FnDefId<ChalkIr>) -> Variances<ChalkIr> {
Variances::from(&ChalkIr, [Variance::Invariant; 20].iter().copied())
Variances::from_iter(&ChalkIr, [Variance::Invariant; 20].iter().copied())
}

fn adt_variance(&self, _adt_id: AdtId<ChalkIr>) -> Variances<ChalkIr> {
Variances::from(&ChalkIr, [Variance::Invariant; 20].iter().copied())
Variances::from_iter(&ChalkIr, [Variance::Invariant; 20].iter().copied())
}
}

Expand Down
82 changes: 51 additions & 31 deletions chalk-engine/src/simplify.rs
Original file line number Diff line number Diff line change
@@ -1,13 +1,14 @@
use crate::forest::Forest;
use crate::slg::{SlgContextOps, TruncatingInferenceTable, UnificationOps};
use crate::slg::SlgContextOps;
use crate::{ExClause, Literal, TimeStamp};

use chalk_ir::cast::Cast;
use chalk_ir::cast::{Cast, Caster};
use chalk_ir::interner::Interner;
use chalk_ir::{
Environment, FallibleOrFloundered, Goal, GoalData, InEnvironment, QuantifierKind, Substitution,
Variance,
TyKind, TyVariableKind, Variance,
};
use chalk_solve::infer::InferenceTable;
use tracing::debug;

impl<I: Interner> Forest<I> {
Expand All @@ -16,7 +17,7 @@ impl<I: Interner> Forest<I> {
/// includes unifications that cannot be completed.
pub(super) fn simplify_goal(
context: &SlgContextOps<I>,
infer: &mut TruncatingInferenceTable<I>,
infer: &mut InferenceTable<I>,
subst: Substitution<I>,
initial_environment: Environment<I>,
initial_goal: Goal<I>,
Expand Down Expand Up @@ -70,36 +71,55 @@ impl<I: Interner> Forest<I> {
subgoal.clone(),
)));
}
GoalData::EqGoal(goal) => match infer.relate_generic_args_into_ex_clause(
context.program().interner(),
context.unification_database(),
&environment,
Variance::Invariant,
&goal.a,
&goal.b,
&mut ex_clause,
) {
Ok(()) => {}
Err(_) => return FallibleOrFloundered::NoSolution,
},
GoalData::EqGoal(goal) => {
let interner = context.program().interner();
let db = context.unification_database();
let a = &goal.a;
let b = &goal.b;

let result =
match infer.relate(interner, db, &environment, Variance::Invariant, a, b) {
Ok(r) => r,
Err(_) => return FallibleOrFloundered::NoSolution,
};
ex_clause.subgoals.extend(
result
.goals
.into_iter()
.casted(interner)
.map(Literal::Positive),
);
}
GoalData::SubtypeGoal(goal) => {
match infer.relate_tys_into_ex_clause(
context.program().interner(),
context.unification_database(),
&environment,
Variance::Covariant,
&goal.a,
&goal.b,
&mut ex_clause,
let interner = context.program().interner();
let db = context.unification_database();
let a_norm = infer.normalize_ty_shallow(interner, &goal.a);
let a = a_norm.as_ref().unwrap_or(&goal.a);
let b_norm = infer.normalize_ty_shallow(interner, &goal.b);
let b = b_norm.as_ref().unwrap_or(&goal.b);

if matches!(
a.kind(interner),
TyKind::InferenceVar(_, TyVariableKind::General)
) && matches!(
b.kind(interner),
TyKind::InferenceVar(_, TyVariableKind::General)
) {
FallibleOrFloundered::Ok(_) => {}
FallibleOrFloundered::Floundered => {
return FallibleOrFloundered::Floundered
}
FallibleOrFloundered::NoSolution => {
return FallibleOrFloundered::NoSolution
}
return FallibleOrFloundered::Floundered;
}

let result =
match infer.relate(interner, db, &environment, Variance::Covariant, a, b) {
Ok(r) => r,
Err(_) => return FallibleOrFloundered::Floundered,
};
ex_clause.subgoals.extend(
result
.goals
.into_iter()
.casted(interner)
.map(Literal::Positive),
);
}
GoalData::DomainGoal(domain_goal) => {
ex_clause
Expand Down
Loading

0 comments on commit 9332c49

Please sign in to comment.