Skip to content

Commit b9037b3

Browse files
jackh726jackh726
committed
Remove some unneeded functions from Context
1 parent bf332ae commit b9037b3

File tree

6 files changed

+24
-123
lines changed

6 files changed

+24
-123
lines changed

‎chalk-engine/src/context.rs

Lines changed: 0 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -45,38 +45,6 @@ pub trait Context<I: Interner>: Clone + Debug {
4545
/// the equality relation.
4646
type Variance;
4747

48-
/// Given an environment and a goal, glue them together to create
49-
/// a `GoalInEnvironment`.
50-
fn goal_in_environment(
51-
environment: &Environment<I>,
52-
goal: Goal<I>,
53-
) -> InEnvironment<Goal<I>>;
54-
55-
/// Extracts the inner normalized substitution from a canonical ex-clause.
56-
fn inference_normalized_subst_from_ex_clause(
57-
canon_ex_clause: &Canonical<ExClause<I>>,
58-
) -> &Substitution<I>;
59-
60-
/// Extracts the inner normalized substitution from a canonical constraint subst.
61-
fn inference_normalized_subst_from_subst(
62-
canon_ex_clause: &Canonical<AnswerSubst<I>>,
63-
) -> &Substitution<I>;
64-
65-
/// True if this solution has no region constraints.
66-
fn empty_constraints(ccs: &Canonical<AnswerSubst<I>>) -> bool;
67-
68-
fn canonical(u_canon: &UCanonical<InEnvironment<Goal<I>>>) -> &Canonical<InEnvironment<Goal<I>>>;
69-
70-
fn has_delayed_subgoals(canonical_subst: &Canonical<AnswerSubst<I>>) -> bool;
71-
72-
fn num_universes(_: &UCanonical<InEnvironment<Goal<I>>>) -> usize;
73-
74-
fn canonical_constrained_subst_from_canonical_constrained_answer(
75-
canonical_subst: &Canonical<AnswerSubst<I>>,
76-
) -> Canonical<ConstrainedSubst<I>>;
77-
78-
fn goal_from_goal_in_environment(goal: &InEnvironment<Goal<I>>) -> &Goal<I>;
79-
8048
/// Selects the next appropriate subgoal index for evaluation.
8149
/// Used by: logic
8250
fn next_subgoal_index(ex_clause: &ExClause<I>) -> usize;
@@ -138,12 +106,6 @@ pub trait ContextOps<I: Interner, C: Context<I>>: Sized + Clone + Debug + Aggreg
138106
Vec<InEnvironment<Goal<I>>>,
139107
);
140108

141-
/// returns unique solution from answer
142-
fn constrained_subst_from_answer(
143-
&self,
144-
answer: CompleteAnswer<I>,
145-
) -> Canonical<ConstrainedSubst<I>>;
146-
147109
/// Returns a identity substitution.
148110
fn identity_constrained_subst(
149111
&self,

‎chalk-engine/src/forest.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -90,9 +90,9 @@ impl<I: Interner, C: Context<I>> Forest<I, C> {
9090
let subst = match answers.next_answer(|| true) {
9191
AnswerResult::Answer(answer) => {
9292
if !answer.ambiguous {
93-
SubstitutionResult::Definite(context.constrained_subst_from_answer(answer))
93+
SubstitutionResult::Definite(answer.subst)
9494
} else {
95-
SubstitutionResult::Ambiguous(context.constrained_subst_from_answer(answer))
95+
SubstitutionResult::Ambiguous(answer.subst)
9696
}
9797
}
9898
AnswerResult::Floundered => SubstitutionResult::Floundered,

‎chalk-engine/src/logic.rs

Lines changed: 17 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ use crate::{
1212
use chalk_base::results::{Floundered, NoSolution};
1313

1414
use chalk_ir::interner::Interner;
15-
use chalk_ir::{Goal, InEnvironment, Substitution, UCanonical, UniverseMap};
15+
use chalk_ir::{Canonical, ConstrainedSubst, Goal, InEnvironment, Substitution, UCanonical, UniverseMap};
1616

1717
type RootSearchResult<T> = Result<T, RootSearchFail>;
1818

@@ -93,14 +93,17 @@ impl<I: Interner, C: Context<I>> Forest<I, C> {
9393
Ok(()) => {
9494
assert!(state.stack.is_empty());
9595
let answer = state.forest.answer(table, answer_index);
96-
let has_delayed_subgoals = C::has_delayed_subgoals(&answer.subst);
97-
if has_delayed_subgoals {
96+
if !answer.subst.value.delayed_subgoals.is_empty() {
9897
return Err(RootSearchFail::InvalidAnswer);
9998
}
10099
Ok(CompleteAnswer {
101-
subst: C::canonical_constrained_subst_from_canonical_constrained_answer(
102-
&answer.subst,
103-
),
100+
subst: Canonical {
101+
binders: answer.subst.binders.clone(),
102+
value: ConstrainedSubst {
103+
subst: answer.subst.value.subst.clone(),
104+
constraints: answer.subst.value.constraints.clone(),
105+
},
106+
},
104107
ambiguous: answer.ambiguous,
105108
})
106109
}
@@ -116,13 +119,11 @@ impl<I: Interner, C: Context<I>> Forest<I, C> {
116119
) -> bool {
117120
if let Some(answer) = self.tables[table].answer(answer) {
118121
info!("answer cached = {:?}", answer);
119-
return test(C::inference_normalized_subst_from_subst(&answer.subst));
122+
return test(&answer.subst.value.subst);
120123
}
121124

122125
self.tables[table].strands().any(|strand| {
123-
test(C::inference_normalized_subst_from_ex_clause(
124-
&strand.canonical_ex_clause,
125-
))
126+
test(&strand.canonical_ex_clause.value.subst)
126127
})
127128
}
128129

@@ -465,7 +466,7 @@ impl<'forest, I: Interner, C: Context<I> + 'forest, CO: ContextOps<I, C> + 'fore
465466
self.forest.tables[table]
466467
.dequeue_next_strand_if(|strand| strand.last_pursued_time < clock)
467468
.map(|canonical_strand| {
468-
let num_universes = C::num_universes(&self.forest.tables[table].table_goal);
469+
let num_universes = self.forest.tables[table].table_goal.universes;
469470
let CanonicalStrand {
470471
canonical_ex_clause,
471472
selected_subgoal,
@@ -568,7 +569,7 @@ impl<'forest, I: Interner, C: Context<I> + 'forest, CO: ContextOps<I, C> + 'fore
568569
} = selected_subgoal;
569570
let table_goal = &self.context.map_goal_from_canonical(
570571
&universe_map,
571-
&C::canonical(&self.forest.tables[subgoal_table].table_goal),
572+
&self.forest.tables[subgoal_table].table_goal.canonical,
572573
);
573574
let answer_subst = &self.context.map_subst_from_canonical(
574575
&universe_map,
@@ -636,7 +637,7 @@ impl<'forest, I: Interner, C: Context<I> + 'forest, CO: ContextOps<I, C> + 'fore
636637
// need to permit `not { L }` where `L` is a
637638
// coinductive goal. We could improve this if needed,
638639
// but it keeps things simple.
639-
if C::has_delayed_subgoals(&answer.subst) {
640+
if !answer.subst.value.delayed_subgoals.is_empty() {
640641
panic!("Negative subgoal had delayed_subgoals");
641642
}
642643

@@ -965,11 +966,11 @@ impl<'forest, I: Interner, C: Context<I> + 'forest, CO: ContextOps<I, C> + 'fore
965966
) -> Option<CanonicalStrand<I>> {
966967
// If there are no delayed subgoals, then there is no need for
967968
// a refinement strand.
968-
if !C::has_delayed_subgoals(&answer.subst) {
969+
if answer.subst.value.delayed_subgoals.is_empty() {
969970
return None;
970971
}
971972

972-
let num_universes = C::num_universes(&self.forest.tables[table].table_goal);
973+
let num_universes = self.forest.tables[table].table_goal.universes;
973974
let (table, subst, constraints, delayed_subgoals) = self
974975
.context
975976
.instantiate_answer_subst(num_universes, &answer.subst);
@@ -1402,7 +1403,7 @@ impl<'forest, I: Interner, C: Context<I> + 'forest, CO: ContextOps<I, C> + 'fore
14021403
&& self
14031404
.context
14041405
.is_trivial_substitution(&self.forest.tables[table].table_goal, &answer.subst)
1405-
&& C::empty_constraints(&answer.subst)
1406+
&& answer.subst.value.constraints.is_empty()
14061407
};
14071408

14081409
if let Some(answer_index) = self.forest.tables[table].push_answer(answer) {

‎chalk-engine/src/simplify.rs

Lines changed: 3 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ use crate::{ExClause, Literal, TimeStamp};
55
use chalk_base::results::Fallible;
66

77
use chalk_ir::interner::Interner;
8-
use chalk_ir::{Environment, Substitution};
8+
use chalk_ir::{Environment, InEnvironment, Substitution};
99

1010
impl<I: Interner, C: Context<I>> Forest<I, C> {
1111
/// Simplifies an HH goal into a series of positive domain goals
@@ -55,10 +55,7 @@ impl<I: Interner, C: Context<I>> Forest<I, C> {
5555
HhGoal::Not(subgoal) => {
5656
ex_clause
5757
.subgoals
58-
.push(Literal::Negative(C::goal_in_environment(
59-
&environment,
60-
subgoal,
61-
)));
58+
.push(Literal::Negative(InEnvironment::new(&environment, subgoal)));
6259
}
6360
HhGoal::Unify(variance, a, b) => infer.unify_generic_args_into_ex_clause(
6461
context.interner(),
@@ -71,10 +68,7 @@ impl<I: Interner, C: Context<I>> Forest<I, C> {
7168
HhGoal::DomainGoal(domain_goal) => {
7269
ex_clause
7370
.subgoals
74-
.push(Literal::Positive(C::goal_in_environment(
75-
&environment,
76-
context.into_goal(domain_goal),
77-
)));
71+
.push(Literal::Positive(InEnvironment::new(&environment, context.into_goal(domain_goal))));
7872
}
7973
HhGoal::CannotProve => {
8074
ex_clause.ambiguous = true;

‎chalk-solve/src/solve/slg.rs

Lines changed: 0 additions & 56 deletions
Original file line numberDiff line numberDiff line change
@@ -69,54 +69,6 @@ impl<I: Interner> context::Context<I> for SlgContext<I> {
6969
type InferenceTable = TruncatingInferenceTable<I>;
7070
type Variance = ();
7171

72-
fn goal_in_environment(environment: &Environment<I>, goal: Goal<I>) -> InEnvironment<Goal<I>> {
73-
InEnvironment::new(environment, goal)
74-
}
75-
76-
fn inference_normalized_subst_from_ex_clause(
77-
canon_ex_clause: &Canonical<ExClause<I>>,
78-
) -> &Substitution<I> {
79-
&canon_ex_clause.value.subst
80-
}
81-
82-
fn empty_constraints(ccs: &Canonical<AnswerSubst<I>>) -> bool {
83-
ccs.value.constraints.is_empty()
84-
}
85-
86-
fn inference_normalized_subst_from_subst(ccs: &Canonical<AnswerSubst<I>>) -> &Substitution<I> {
87-
&ccs.value.subst
88-
}
89-
90-
fn canonical(
91-
u_canon: &UCanonical<InEnvironment<Goal<I>>>,
92-
) -> &Canonical<InEnvironment<Goal<I>>> {
93-
&u_canon.canonical
94-
}
95-
96-
fn has_delayed_subgoals(canonical_subst: &Canonical<AnswerSubst<I>>) -> bool {
97-
!canonical_subst.value.delayed_subgoals.is_empty()
98-
}
99-
100-
fn num_universes(u_canon: &UCanonical<InEnvironment<Goal<I>>>) -> usize {
101-
u_canon.universes
102-
}
103-
104-
fn canonical_constrained_subst_from_canonical_constrained_answer(
105-
canonical_subst: &Canonical<AnswerSubst<I>>,
106-
) -> Canonical<ConstrainedSubst<I>> {
107-
Canonical {
108-
binders: canonical_subst.binders.clone(),
109-
value: ConstrainedSubst {
110-
subst: canonical_subst.value.subst.clone(),
111-
constraints: canonical_subst.value.constraints.clone(),
112-
},
113-
}
114-
}
115-
116-
fn goal_from_goal_in_environment(goal: &InEnvironment<Goal<I>>) -> &Goal<I> {
117-
&goal.goal
118-
}
119-
12072
// Used by: logic
12173
fn next_subgoal_index(ex_clause: &ExClause<I>) -> usize {
12274
// For now, we always pick the last subgoal in the
@@ -222,14 +174,6 @@ impl<'me, I: Interner> context::ContextOps<I, SlgContext<I>> for SlgContextOps<'
222174
(infer_table, subst, constraints, delayed_subgoals)
223175
}
224176

225-
fn constrained_subst_from_answer(
226-
&self,
227-
answer: CompleteAnswer<I>,
228-
) -> Canonical<ConstrainedSubst<I>> {
229-
let CompleteAnswer { subst, .. } = answer;
230-
subst
231-
}
232-
233177
fn identity_constrained_subst(
234178
&self,
235179
goal: &UCanonical<InEnvironment<Goal<I>>>,

‎chalk-solve/src/solve/slg/aggregate.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ use chalk_ir::cast::Cast;
88
use chalk_ir::interner::Interner;
99
use chalk_ir::*;
1010

11-
use chalk_engine::context::{self, AnswerResult, Context, ContextOps};
11+
use chalk_engine::context::{self, AnswerResult, ContextOps};
1212
use chalk_engine::CompleteAnswer;
1313
use std::fmt::Debug;
1414

@@ -97,7 +97,7 @@ impl<I: Interner> context::AggregateOps<I, SlgContext<I>> for SlgContextOps<'_,
9797
};
9898
subst = merge_into_guidance(
9999
interner,
100-
SlgContext::canonical(root_goal),
100+
&root_goal.canonical,
101101
subst,
102102
&new_subst,
103103
);

0 commit comments

Comments
 (0)