Skip to content

Commit

Permalink
Propagate results of Fold signature change up the call graph
Browse files Browse the repository at this point in the history
  • Loading branch information
ecstatic-morse committed Dec 4, 2020
1 parent d89dde3 commit 4b62b7c
Show file tree
Hide file tree
Showing 36 changed files with 476 additions and 408 deletions.
34 changes: 18 additions & 16 deletions chalk-engine/src/logic.rs
Original file line number Diff line number Diff line change
Expand Up @@ -149,7 +149,7 @@ impl<I: Interner> Forest<I> {
Forest::canonicalize_strand_from(
context,
&mut infer,
&ex_clause,
ex_clause,
selected_subgoal,
last_pursued_time,
)
Expand All @@ -158,12 +158,12 @@ impl<I: Interner> Forest<I> {
fn canonicalize_strand_from(
context: &SlgContextOps<I>,
infer: &mut TruncatingInferenceTable<I>,
ex_clause: &ExClause<I>,
ex_clause: ExClause<I>,
selected_subgoal: Option<SelectedSubgoal>,
last_pursued_time: TimeStamp,
) -> CanonicalStrand<I> {
let canonical_ex_clause =
infer.canonicalize_ex_clause(context.program().interner(), &ex_clause);
infer.canonicalize_ex_clause(context.program().interner(), ex_clause);
CanonicalStrand {
canonical_ex_clause,
selected_subgoal,
Expand Down Expand Up @@ -194,10 +194,10 @@ impl<I: Interner> Forest<I> {
// Subgoal abstraction:
let (ucanonical_subgoal, universe_map) = match subgoal {
Literal::Positive(subgoal) => {
Forest::abstract_positive_literal(context, infer, subgoal)?
Forest::abstract_positive_literal(context, infer, subgoal.clone())?
}
Literal::Negative(subgoal) => {
Forest::abstract_negative_literal(context, infer, subgoal)?
Forest::abstract_negative_literal(context, infer, subgoal.clone())?
}
};

Expand Down Expand Up @@ -257,7 +257,7 @@ impl<I: Interner> Forest<I> {
chalk_solve::infer::InferenceTable::from_canonical(
context.program().interner(),
goal.universes,
&goal.canonical,
goal.canonical,
);
let mut infer = TruncatingInferenceTable::new(context.max_size(), infer);
let goal_data = goal.data(context.program().interner());
Expand Down Expand Up @@ -350,9 +350,9 @@ impl<I: Interner> Forest<I> {
fn abstract_positive_literal(
context: &SlgContextOps<I>,
infer: &mut TruncatingInferenceTable<I>,
subgoal: &InEnvironment<Goal<I>>,
subgoal: InEnvironment<Goal<I>>,
) -> Option<(UCanonical<InEnvironment<Goal<I>>>, UniverseMap)> {
if infer.goal_needs_truncation(context.program().interner(), subgoal) {
if infer.goal_needs_truncation(context.program().interner(), &subgoal) {
None
} else {
Some(infer.fully_canonicalize_goal(context.program().interner(), subgoal))
Expand All @@ -369,7 +369,7 @@ impl<I: Interner> Forest<I> {
fn abstract_negative_literal(
context: &SlgContextOps<I>,
infer: &mut TruncatingInferenceTable<I>,
subgoal: &InEnvironment<Goal<I>>,
subgoal: InEnvironment<Goal<I>>,
) -> Option<(UCanonical<InEnvironment<Goal<I>>>, UniverseMap)> {
// First, we have to check that the selected negative literal
// is ground, and invert any universally quantified variables.
Expand Down Expand Up @@ -413,7 +413,7 @@ impl<I: Interner> Forest<I> {
if infer.goal_needs_truncation(context.program().interner(), &inverted_subgoal) {
None
} else {
Some(infer.fully_canonicalize_goal(context.program().interner(), &inverted_subgoal))
Some(infer.fully_canonicalize_goal(context.program().interner(), inverted_subgoal))
}
}
}
Expand Down Expand Up @@ -494,7 +494,7 @@ impl<'forest, I: Interner> SolveState<'forest, I> {
let (_, _, ex_clause) = chalk_solve::infer::InferenceTable::from_canonical(
context.program().interner(),
num_universes,
&strand.canonical_ex_clause,
strand.canonical_ex_clause.clone(),
);
let time_eligble = strand.last_pursued_time < clock;
let mode_eligble = match (table_answer_mode, ex_clause.ambiguous) {
Expand All @@ -515,7 +515,7 @@ impl<'forest, I: Interner> SolveState<'forest, I> {
chalk_solve::infer::InferenceTable::from_canonical(
context.program().interner(),
num_universes,
&canonical_ex_clause,
canonical_ex_clause,
);
let infer = TruncatingInferenceTable::new(context.max_size(), infer);
Strand {
Expand Down Expand Up @@ -660,7 +660,7 @@ impl<'forest, I: Interner> SolveState<'forest, I> {
&mut strand.ex_clause,
&subgoal,
&table_goal,
&answer_subst,
answer_subst,
) {
Ok(()) => {
let Strand {
Expand Down Expand Up @@ -1078,7 +1078,7 @@ impl<'forest, I: Interner> SolveState<'forest, I> {
) = chalk_solve::infer::InferenceTable::from_canonical(
self.context.program().interner(),
num_universes,
&answer.subst,
answer.subst.clone(),
);
let table = TruncatingInferenceTable::new(self.context.max_size(), infer);

Expand Down Expand Up @@ -1414,8 +1414,10 @@ impl<'forest, I: Interner> SolveState<'forest, I> {
let filtered_delayed_subgoals = delayed_subgoals
.into_iter()
.filter(|delayed_subgoal| {
let (canonicalized, _) = infer
.fully_canonicalize_goal(self.context.program().interner(), delayed_subgoal);
let (canonicalized, _) = infer.fully_canonicalize_goal(
self.context.program().interner(),
delayed_subgoal.clone(),
);
*table_goal != canonicalized
})
.collect();
Expand Down
9 changes: 6 additions & 3 deletions chalk-engine/src/normalize_deep.rs
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ impl<I: Interner> DeepNormalizer<'_, '_, I> {
pub fn normalize_deep<T: Fold<I>>(
table: &mut InferenceTable<I>,
interner: &I,
value: &T,
value: T,
) -> T::Result {
value
.fold_with(
Expand Down Expand Up @@ -53,6 +53,7 @@ where
match self.table.probe_var(var) {
Some(ty) => Ok(ty
.assert_ty_ref(interner)
.clone()
.fold_with(self, DebruijnIndex::INNERMOST)?
.shifted_in(interner)), // FIXME shift
None => {
Expand All @@ -72,6 +73,7 @@ where
match self.table.probe_var(var) {
Some(l) => Ok(l
.assert_lifetime_ref(interner)
.clone()
.fold_with(self, DebruijnIndex::INNERMOST)?
.shifted_in(interner)),
None => Ok(var.to_lifetime(interner)), // FIXME shift
Expand All @@ -80,17 +82,18 @@ where

fn fold_inference_const(
&mut self,
ty: &Ty<I>,
ty: Ty<I>,
var: InferenceVar,
_outer_binder: DebruijnIndex,
) -> Fallible<Const<I>> {
let interner = self.interner;
match self.table.probe_var(var) {
Some(c) => Ok(c
.assert_const_ref(interner)
.clone()
.fold_with(self, DebruijnIndex::INNERMOST)?
.shifted_in(interner)),
None => Ok(var.to_const(interner, ty.clone())), // FIXME shift
None => Ok(var.to_const(interner, ty)), // FIXME shift
}
}

Expand Down
12 changes: 8 additions & 4 deletions chalk-engine/src/simplify.rs
Original file line number Diff line number Diff line change
Expand Up @@ -37,13 +37,17 @@ impl<I: Interner> Forest<I> {
while let Some((environment, goal)) = pending_goals.pop() {
match goal.data(context.program().interner()) {
GoalData::Quantified(QuantifierKind::ForAll, subgoal) => {
let subgoal = infer
.instantiate_binders_universally(context.program().interner(), &subgoal);
let subgoal = infer.instantiate_binders_universally(
context.program().interner(),
subgoal.clone(),
);
pending_goals.push((environment, subgoal.clone()));
}
GoalData::Quantified(QuantifierKind::Exists, subgoal) => {
let subgoal = infer
.instantiate_binders_existentially(context.program().interner(), &subgoal);
let subgoal = infer.instantiate_binders_existentially(
context.program().interner(),
subgoal.clone(),
);
pending_goals.push((environment, subgoal.clone()));
}
GoalData::Implies(wc, subgoal) => {
Expand Down
37 changes: 17 additions & 20 deletions chalk-engine/src/slg.rs
Original file line number Diff line number Diff line change
Expand Up @@ -61,12 +61,12 @@ impl<I: Interner> SlgContextOps<'_, I> {
let (mut infer, subst, _) = InferenceTable::from_canonical(
self.program.interner(),
goal.universes,
&goal.canonical,
goal.canonical.clone(),
);
infer
.canonicalize(
self.program.interner(),
&ConstrainedSubst {
ConstrainedSubst {
subst,
constraints: Constraints::empty(self.program.interner()),
},
Expand Down Expand Up @@ -130,21 +130,18 @@ pub trait ResolventOps<I: Interner> {
ex_clause: &mut ExClause<I>,
selected_goal: &InEnvironment<Goal<I>>,
answer_table_goal: &Canonical<InEnvironment<Goal<I>>>,
canonical_answer_subst: &Canonical<AnswerSubst<I>>,
canonical_answer_subst: Canonical<AnswerSubst<I>>,
) -> Fallible<()>;
}

/// Methods for unifying and manipulating terms and binders.
pub trait UnificationOps<I: Interner> {
// Used by: simplify
fn instantiate_binders_universally(&mut self, interner: &I, arg: &Binders<Goal<I>>) -> Goal<I>;
fn instantiate_binders_universally(&mut self, interner: &I, arg: Binders<Goal<I>>) -> Goal<I>;

// Used by: simplify
fn instantiate_binders_existentially(
&mut self,
interner: &I,
arg: &Binders<Goal<I>>,
) -> Goal<I>;
fn instantiate_binders_existentially(&mut self, interner: &I, arg: Binders<Goal<I>>)
-> Goal<I>;

// Used by: logic (but for debugging only)
fn debug_ex_clause<'v>(&mut self, interner: &I, value: &'v ExClause<I>) -> Box<dyn Debug + 'v>;
Expand All @@ -153,14 +150,14 @@ pub trait UnificationOps<I: Interner> {
fn fully_canonicalize_goal(
&mut self,
interner: &I,
value: &InEnvironment<Goal<I>>,
value: InEnvironment<Goal<I>>,
) -> (UCanonical<InEnvironment<Goal<I>>>, UniverseMap);

// Used by: logic
fn canonicalize_ex_clause(
&mut self,
interner: &I,
value: &ExClause<I>,
value: ExClause<I>,
) -> Canonical<ExClause<I>>;

// Used by: logic
Expand All @@ -184,7 +181,7 @@ pub trait UnificationOps<I: Interner> {
fn invert_goal(
&mut self,
interner: &I,
value: &InEnvironment<Goal<I>>,
value: InEnvironment<Goal<I>>,
) -> Option<InEnvironment<Goal<I>>>;

/// First unify the parameters, then add the residual subgoals
Expand Down Expand Up @@ -239,14 +236,14 @@ impl<I: Interner> TruncateOps<I> for TruncatingInferenceTable<I> {
}

impl<I: Interner> UnificationOps<I> for TruncatingInferenceTable<I> {
fn instantiate_binders_universally(&mut self, interner: &I, arg: &Binders<Goal<I>>) -> Goal<I> {
fn instantiate_binders_universally(&mut self, interner: &I, arg: Binders<Goal<I>>) -> Goal<I> {
self.infer.instantiate_binders_universally(interner, arg)
}

fn instantiate_binders_existentially(
&mut self,
interner: &I,
arg: &Binders<Goal<I>>,
arg: Binders<Goal<I>>,
) -> Goal<I> {
self.infer.instantiate_binders_existentially(interner, arg)
}
Expand All @@ -255,14 +252,14 @@ impl<I: Interner> UnificationOps<I> for TruncatingInferenceTable<I> {
Box::new(DeepNormalizer::normalize_deep(
&mut self.infer,
interner,
value,
value.clone(),
))
}

fn fully_canonicalize_goal(
&mut self,
interner: &I,
value: &InEnvironment<Goal<I>>,
value: InEnvironment<Goal<I>>,
) -> (UCanonical<InEnvironment<Goal<I>>>, UniverseMap) {
let canonicalized_goal = self.infer.canonicalize(interner, value).quantified;
let UCanonicalized {
Expand All @@ -275,7 +272,7 @@ impl<I: Interner> UnificationOps<I> for TruncatingInferenceTable<I> {
fn canonicalize_ex_clause(
&mut self,
interner: &I,
value: &ExClause<I>,
value: ExClause<I>,
) -> Canonical<ExClause<I>> {
self.infer.canonicalize(interner, value).quantified
}
Expand All @@ -289,7 +286,7 @@ impl<I: Interner> UnificationOps<I> for TruncatingInferenceTable<I> {
self.infer
.canonicalize(
interner,
&ConstrainedSubst {
ConstrainedSubst {
subst,
constraints: Constraints::from_iter(interner, constraints),
},
Expand All @@ -307,7 +304,7 @@ impl<I: Interner> UnificationOps<I> for TruncatingInferenceTable<I> {
self.infer
.canonicalize(
interner,
&AnswerSubst {
AnswerSubst {
subst,
constraints: Constraints::from_iter(interner, constraints),
delayed_subgoals,
Expand All @@ -319,7 +316,7 @@ impl<I: Interner> UnificationOps<I> for TruncatingInferenceTable<I> {
fn invert_goal(
&mut self,
interner: &I,
value: &InEnvironment<Goal<I>>,
value: InEnvironment<Goal<I>>,
) -> Option<InEnvironment<Goal<I>>> {
self.infer.invert(interner, value)
}
Expand Down
2 changes: 1 addition & 1 deletion chalk-engine/src/slg/aggregate.rs
Original file line number Diff line number Diff line change
Expand Up @@ -181,7 +181,7 @@ fn merge_into_guidance<I: Interner>(

let aggr_subst = Substitution::from_iter(interner, aggr_generic_args);

infer.canonicalize(interner, &aggr_subst).quantified
infer.canonicalize(interner, aggr_subst).quantified
}

fn is_trivial<I: Interner>(interner: &I, subst: &Canonical<Substitution<I>>) -> bool {
Expand Down
15 changes: 5 additions & 10 deletions chalk-engine/src/slg/resolvent.rs
Original file line number Diff line number Diff line change
Expand Up @@ -82,7 +82,7 @@ impl<I: Interner> ResolventOps<I> for TruncatingInferenceTable<I> {
let ProgramClauseData(implication) = clause.data(interner);

self.infer
.instantiate_binders_existentially(interner, implication)
.instantiate_binders_existentially(interner, implication.clone())
};
debug!(?consequence, ?conditions, ?constraints);

Expand Down Expand Up @@ -213,9 +213,9 @@ impl<I: Interner> ResolventOps<I> for TruncatingInferenceTable<I> {
ex_clause: &mut ExClause<I>,
selected_goal: &InEnvironment<Goal<I>>,
answer_table_goal: &Canonical<InEnvironment<Goal<I>>>,
canonical_answer_subst: &Canonical<AnswerSubst<I>>,
canonical_answer_subst: Canonical<AnswerSubst<I>>,
) -> Fallible<()> {
debug!(selected_goal = ?DeepNormalizer::normalize_deep(&mut self.infer, interner, selected_goal));
debug!(selected_goal = ?DeepNormalizer::normalize_deep(&mut self.infer, interner, selected_goal.clone()));

// C' is now `answer`. No variables in common with G.
let AnswerSubst {
Expand All @@ -231,7 +231,7 @@ impl<I: Interner> ResolventOps<I> for TruncatingInferenceTable<I> {
delayed_subgoals,
} = self
.infer
.instantiate_canonical(interner, &canonical_answer_subst);
.instantiate_canonical(interner, canonical_answer_subst);

AnswerSubstitutor::substitute(
interner,
Expand Down Expand Up @@ -320,12 +320,7 @@ impl<I: Interner> AnswerSubstitutor<'_, I> {

let pending_shifted = pending
.shifted_out_to(interner, self.outer_binder)
.unwrap_or_else(|_| {
panic!(
"truncate extracted a pending value that references internal binder: {:?}",
pending,
)
});
.expect("truncate extracted a pending value that references internal binder");

slg::into_ex_clause(
interner,
Expand Down
Loading

0 comments on commit 4b62b7c

Please sign in to comment.