Skip to content

Commit e14cdfc

Browse files
jackh726jackh726
committed
Forest shouldn't have solve or solve_multiple, only iter_answers
1 parent 2f6a365 commit e14cdfc

File tree

9 files changed

+126
-123
lines changed

9 files changed

+126
-123
lines changed

‎chalk-engine/src/context.rs

Lines changed: 1 addition & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -34,11 +34,6 @@ use std::fmt::Debug;
3434
/// FIXME: Clone and Debug bounds are just for easy derive, they are
3535
/// not actually necessary. But dang are they convenient.
3636
pub trait Context<I: Interner>: Clone + Debug {
37-
/// A final solution that is passed back to the user. This is
38-
/// completely opaque to the SLG solver; it is produced by
39-
/// `make_solution`.
40-
type Solution;
41-
4237
/// Represents an inference table.
4338
type InferenceTable: InferenceTable<I, Self> + Clone;
4439

@@ -47,9 +42,7 @@ pub trait Context<I: Interner>: Clone + Debug {
4742
fn next_subgoal_index(ex_clause: &ExClause<I>) -> usize;
4843
}
4944

50-
pub trait ContextOps<I: Interner, C: Context<I>>:
51-
Sized + Clone + Debug + AggregateOps<I, C>
52-
{
45+
pub trait ContextOps<I: Interner, C: Context<I>>: Sized + Clone + Debug {
5346
/// True if this is a coinductive goal -- e.g., proving an auto trait.
5447
fn is_coinductive(&self, goal: &UCanonical<InEnvironment<Goal<I>>>) -> bool;
5548

@@ -147,16 +140,6 @@ pub trait ContextOps<I: Interner, C: Context<I>>:
147140
) -> bool;
148141
}
149142

150-
/// Methods for combining solutions to yield an aggregate solution.
151-
pub trait AggregateOps<I: Interner, C: Context<I>> {
152-
fn make_solution(
153-
&self,
154-
root_goal: &UCanonical<InEnvironment<Goal<I>>>,
155-
answers: impl AnswerStream<I>,
156-
should_continue: impl Fn() -> bool,
157-
) -> Option<C::Solution>;
158-
}
159-
160143
/// An "inference table" contains the state to support unification and
161144
/// other operations on terms.
162145
pub trait InferenceTable<I: Interner, C: Context<I>>:

‎chalk-engine/src/forest.rs

Lines changed: 2 additions & 86 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,10 @@ use crate::logic::RootSearchFail;
33
use crate::table::AnswerIndex;
44
use crate::tables::Tables;
55
use crate::{TableIndex, TimeStamp};
6-
use std::fmt::Display;
76

87
use chalk_ir::debug;
98
use chalk_ir::interner::Interner;
10-
use chalk_ir::{Canonical, ConstrainedSubst, Goal, InEnvironment, Substitution, UCanonical};
9+
use chalk_ir::{Goal, InEnvironment, Substitution, UCanonical};
1110

1211
pub struct Forest<I: Interner, C: Context<I>> {
1312
pub(crate) tables: Tables<I>,
@@ -39,7 +38,7 @@ impl<I: Interner, C: Context<I>> Forest<I, C> {
3938
/// iterator. Each time you invoke `next`, it will do the work to
4039
/// extract one more answer. These answers are cached in between
4140
/// invocations. Invoking `next` fewer times is preferable =)
42-
fn iter_answers<'f>(
41+
pub fn iter_answers<'f>(
4342
&'f mut self,
4443
context: &'f impl ContextOps<I, C>,
4544
goal: &UCanonical<InEnvironment<Goal<I>>>,
@@ -54,89 +53,6 @@ impl<I: Interner, C: Context<I>> Forest<I, C> {
5453
_context: std::marker::PhantomData::<C>,
5554
}
5655
}
57-
58-
/// Solves a given goal, producing the solution. This will do only
59-
/// as much work towards `goal` as it has to (and that works is
60-
/// cached for future attempts).
61-
pub fn solve(
62-
&mut self,
63-
context: &impl ContextOps<I, C>,
64-
goal: &UCanonical<InEnvironment<Goal<I>>>,
65-
should_continue: impl Fn() -> bool,
66-
) -> Option<C::Solution> {
67-
context.make_solution(&goal, self.iter_answers(context, goal), should_continue)
68-
}
69-
70-
/// Solves a given goal, producing the solution. This will do only
71-
/// as much work towards `goal` as it has to (and that works is
72-
/// cached for future attempts). Calls provided function `f` to
73-
/// iterate over multiple solutions until the function return `false`.
74-
pub fn solve_multiple(
75-
&mut self,
76-
context: &impl ContextOps<I, C>,
77-
goal: &UCanonical<InEnvironment<Goal<I>>>,
78-
mut f: impl FnMut(SubstitutionResult<Canonical<ConstrainedSubst<I>>>, bool) -> bool,
79-
) -> bool {
80-
let mut answers = self.iter_answers(context, goal);
81-
loop {
82-
let subst = match answers.next_answer(|| true) {
83-
AnswerResult::Answer(answer) => {
84-
if !answer.ambiguous {
85-
SubstitutionResult::Definite(answer.subst)
86-
} else {
87-
if context.is_trivial_constrained_substitution(&answer.subst) {
88-
SubstitutionResult::Floundered
89-
} else {
90-
SubstitutionResult::Ambiguous(answer.subst)
91-
}
92-
}
93-
}
94-
AnswerResult::Floundered => SubstitutionResult::Floundered,
95-
AnswerResult::NoMoreSolutions => {
96-
return true;
97-
}
98-
AnswerResult::QuantumExceeded => continue,
99-
};
100-
101-
if !f(subst, !answers.peek_answer(|| true).is_no_more_solutions()) {
102-
return false;
103-
}
104-
}
105-
}
106-
}
107-
108-
#[derive(Debug)]
109-
pub enum SubstitutionResult<S> {
110-
Definite(S),
111-
Ambiguous(S),
112-
Floundered,
113-
}
114-
115-
impl<S> SubstitutionResult<S> {
116-
pub fn as_ref(&self) -> SubstitutionResult<&S> {
117-
match self {
118-
SubstitutionResult::Definite(subst) => SubstitutionResult::Definite(subst),
119-
SubstitutionResult::Ambiguous(subst) => SubstitutionResult::Ambiguous(subst),
120-
SubstitutionResult::Floundered => SubstitutionResult::Floundered,
121-
}
122-
}
123-
pub fn map<U, F: FnOnce(S) -> U>(self, f: F) -> SubstitutionResult<U> {
124-
match self {
125-
SubstitutionResult::Definite(subst) => SubstitutionResult::Definite(f(subst)),
126-
SubstitutionResult::Ambiguous(subst) => SubstitutionResult::Ambiguous(f(subst)),
127-
SubstitutionResult::Floundered => SubstitutionResult::Floundered,
128-
}
129-
}
130-
}
131-
132-
impl<S: Display> Display for SubstitutionResult<S> {
133-
fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
134-
match self {
135-
SubstitutionResult::Definite(subst) => write!(fmt, "{}", subst),
136-
SubstitutionResult::Ambiguous(subst) => write!(fmt, "Ambiguous({})", subst),
137-
SubstitutionResult::Floundered => write!(fmt, "Floundered"),
138-
}
139-
}
14056
}
14157

14258
struct ForestSolver<'me, I: Interner, C: Context<I>, CO: ContextOps<I, C>> {

‎chalk-integration/src/db.rs

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,6 @@ use crate::{
66
query::{Lowering, LoweringDatabase},
77
tls,
88
};
9-
use chalk_engine::forest::SubstitutionResult;
109
use chalk_ir::{
1110
AdtId, AssocTypeId, Canonical, ConstrainedSubst, Environment, FnDefId, GenericArg, Goal,
1211
ImplId, InEnvironment, OpaqueTyId, ProgramClause, ProgramClauses, TraitId, Ty, UCanonical,
@@ -15,7 +14,7 @@ use chalk_solve::rust_ir::{
1514
AdtDatum, AssociatedTyDatum, AssociatedTyValue, AssociatedTyValueId, FnDefDatum, ImplDatum,
1615
OpaqueTyDatum, TraitDatum, WellKnownTrait,
1716
};
18-
use chalk_solve::{RustIrDatabase, Solution, SolverChoice};
17+
use chalk_solve::{RustIrDatabase, Solution, SolverChoice, SubstitutionResult};
1918
use salsa::Database;
2019
use std::sync::Arc;
2120

@@ -58,6 +57,10 @@ impl ChalkDatabase {
5857
solution
5958
}
6059

60+
/// Solves a given goal, producing the solution. This will do only
61+
/// as much work towards `goal` as it has to (and that works is
62+
/// cached for future attempts). Calls provided function `f` to
63+
/// iterate over multiple solutions until the function return `false`.
6164
pub fn solve_multiple(
6265
&self,
6366
goal: &UCanonical<InEnvironment<Goal<ChalkIr>>>,

‎chalk-solve/src/lib.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -109,3 +109,4 @@ pub use solve::Guidance;
109109
pub use solve::Solution;
110110
pub use solve::Solver;
111111
pub use solve::SolverChoice;
112+
pub use solve::SubstitutionResult;

‎chalk-solve/src/recursive/fulfill.rs

Lines changed: 12 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -140,7 +140,12 @@ pub trait RecursiveSolver<I: Interner> {
140140
/// of type inference in general. But when solving trait constraints, *fresh*
141141
/// `Fulfill` instances will be created to solve canonicalized, free-standing
142142
/// goals, and transport what was learned back to the outer context.
143-
pub(crate) struct Fulfill<'s, I: Interner, Solver: RecursiveSolver<I>, Infer: RecursiveInferenceTable<I>> {
143+
pub(crate) struct Fulfill<
144+
's,
145+
I: Interner,
146+
Solver: RecursiveSolver<I>,
147+
Infer: RecursiveInferenceTable<I>,
148+
> {
144149
solver: &'s mut Solver,
145150
subst: Substitution<I>,
146151
infer: Infer,
@@ -158,7 +163,9 @@ pub(crate) struct Fulfill<'s, I: Interner, Solver: RecursiveSolver<I>, Infer: Re
158163
cannot_prove: bool,
159164
}
160165

161-
impl<'s, I: Interner, Solver: RecursiveSolver<I>, Infer: RecursiveInferenceTable<I>> Fulfill<'s, I, Solver, Infer> {
166+
impl<'s, I: Interner, Solver: RecursiveSolver<I>, Infer: RecursiveInferenceTable<I>>
167+
Fulfill<'s, I, Solver, Infer>
168+
{
162169
pub(crate) fn new_with_clause(
163170
solver: &'s mut Solver,
164171
infer: Infer,
@@ -261,9 +268,9 @@ impl<'s, I: Interner, Solver: RecursiveSolver<I>, Infer: RecursiveInferenceTable
261268
where
262269
T: ?Sized + Zip<I> + Debug,
263270
{
264-
let (goals, constraints) =
265-
self.infer
266-
.unify(self.solver.interner(), environment, a, b)?;
271+
let (goals, constraints) = self
272+
.infer
273+
.unify(self.solver.interner(), environment, a, b)?;
267274
debug!("unify({:?}, {:?}) succeeded", a, b);
268275
debug!("unify: goals={:?}", goals);
269276
debug!("unify: constraints={:?}", constraints);

‎chalk-solve/src/recursive/lib.rs

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
use chalk_ir::{
2+
Goal, InEnvironment, UCanonical
3+
};
4+
use super::search_graph::DepthFirstNumber;
5+
6+
pub type UCanonicalGoal<I> = UCanonical<InEnvironment<Goal<I>>>;
7+
8+
/// The `minimums` struct is used while solving to track whether we encountered
9+
/// any cycles in the process.
10+
#[derive(Copy, Clone, Debug)]
11+
pub struct Minimums {
12+
pub positive: DepthFirstNumber,
13+
}
14+
15+
impl Minimums {
16+
pub fn new() -> Self {
17+
Minimums {
18+
positive: DepthFirstNumber::MAX,
19+
}
20+
}
21+
22+
pub fn update_from(&mut self, minimums: Minimums) {
23+
self.positive = ::std::cmp::min(self.positive, minimums.positive);
24+
}
25+
}

‎chalk-solve/src/solve.rs

Lines changed: 33 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,13 @@ use chalk_ir::interner::Interner;
33
use chalk_ir::*;
44
use std::fmt;
55

6+
#[cfg(feature = "slg-solver")]
7+
pub use crate::solve::slg::SubstitutionResult;
68
#[cfg(feature = "slg-solver")]
79
use {
8-
crate::solve::slg::{SlgContext, SlgContextOps},
9-
chalk_engine::forest::{Forest, SubstitutionResult},
10+
crate::solve::slg::{aggregate::AggregateOps, SlgContext, SlgContextOps},
11+
chalk_engine::context::{AnswerResult, AnswerStream, ContextOps},
12+
chalk_engine::forest::Forest,
1013
};
1114

1215
#[cfg(feature = "recursive-solver")]
@@ -316,7 +319,7 @@ impl<I: Interner> Solver<I> {
316319
expected_answers,
317320
} => {
318321
let ops = SlgContextOps::new(program, *max_size, *expected_answers);
319-
forest.solve(&ops, goal, || true)
322+
ops.make_solution(goal, forest.iter_answers(&ops, goal), || true)
320323
}
321324
#[cfg(feature = "recursive-solver")]
322325
SolverImpl::Recursive(ctx) => ctx.solver(program).solve_root_goal(goal).ok(),
@@ -359,7 +362,7 @@ impl<I: Interner> Solver<I> {
359362
expected_answers,
360363
} => {
361364
let ops = SlgContextOps::new(program, *max_size, *expected_answers);
362-
forest.solve(&ops, goal, should_continue)
365+
ops.make_solution(goal, forest.iter_answers(&ops, goal), should_continue)
363366
}
364367
#[cfg(feature = "recursive-solver")]
365368
SolverImpl::Recursive(ctx) => {
@@ -396,7 +399,7 @@ impl<I: Interner> Solver<I> {
396399
&mut self,
397400
program: &dyn RustIrDatabase<I>,
398401
goal: &UCanonical<InEnvironment<Goal<I>>>,
399-
f: impl FnMut(SubstitutionResult<Canonical<ConstrainedSubst<I>>>, bool) -> bool,
402+
mut f: impl FnMut(SubstitutionResult<Canonical<ConstrainedSubst<I>>>, bool) -> bool,
400403
) -> bool {
401404
match &mut self.0 {
402405
SolverImpl::Slg {
@@ -405,7 +408,31 @@ impl<I: Interner> Solver<I> {
405408
expected_answers,
406409
} => {
407410
let ops = SlgContextOps::new(program, *max_size, *expected_answers);
408-
forest.solve_multiple(&ops, goal, f)
411+
let mut answers = forest.iter_answers(&ops, goal);
412+
loop {
413+
let subst = match answers.next_answer(|| true) {
414+
AnswerResult::Answer(answer) => {
415+
if !answer.ambiguous {
416+
SubstitutionResult::Definite(answer.subst)
417+
} else {
418+
if ops.is_trivial_constrained_substitution(&answer.subst) {
419+
SubstitutionResult::Floundered
420+
} else {
421+
SubstitutionResult::Ambiguous(answer.subst)
422+
}
423+
}
424+
}
425+
AnswerResult::Floundered => SubstitutionResult::Floundered,
426+
AnswerResult::NoMoreSolutions => {
427+
return true;
428+
}
429+
AnswerResult::QuantumExceeded => continue,
430+
};
431+
432+
if !f(subst, !answers.peek_answer(|| true).is_no_more_solutions()) {
433+
return false;
434+
}
435+
}
409436
}
410437
#[cfg(feature = "recursive-solver")]
411438
SolverImpl::Recursive(_ctx) => unimplemented!(),

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

Lines changed: 36 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,6 @@ use crate::infer::ucanonicalize::UCanonicalized;
44
use crate::infer::unify::UnificationResult;
55
use crate::infer::InferenceTable;
66
use crate::solve::truncate;
7-
use crate::solve::Solution;
87
use crate::RustIrDatabase;
98
use chalk_derive::HasInterner;
109
use chalk_engine::context;
@@ -14,12 +13,46 @@ use chalk_ir::cast::Caster;
1413
use chalk_ir::interner::Interner;
1514
use chalk_ir::*;
1615

17-
use std::fmt::Debug;
16+
use std::fmt::{Debug, Display};
1817
use std::marker::PhantomData;
1918

20-
mod aggregate;
19+
pub(crate) mod aggregate;
2120
mod resolvent;
2221

22+
#[derive(Debug)]
23+
pub enum SubstitutionResult<S> {
24+
Definite(S),
25+
Ambiguous(S),
26+
Floundered,
27+
}
28+
29+
impl<S> SubstitutionResult<S> {
30+
pub fn as_ref(&self) -> SubstitutionResult<&S> {
31+
match self {
32+
SubstitutionResult::Definite(subst) => SubstitutionResult::Definite(subst),
33+
SubstitutionResult::Ambiguous(subst) => SubstitutionResult::Ambiguous(subst),
34+
SubstitutionResult::Floundered => SubstitutionResult::Floundered,
35+
}
36+
}
37+
pub fn map<U, F: FnOnce(S) -> U>(self, f: F) -> SubstitutionResult<U> {
38+
match self {
39+
SubstitutionResult::Definite(subst) => SubstitutionResult::Definite(f(subst)),
40+
SubstitutionResult::Ambiguous(subst) => SubstitutionResult::Ambiguous(f(subst)),
41+
SubstitutionResult::Floundered => SubstitutionResult::Floundered,
42+
}
43+
}
44+
}
45+
46+
impl<S: Display> Display for SubstitutionResult<S> {
47+
fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
48+
match self {
49+
SubstitutionResult::Definite(subst) => write!(fmt, "{}", subst),
50+
SubstitutionResult::Ambiguous(subst) => write!(fmt, "Ambiguous({})", subst),
51+
SubstitutionResult::Floundered => write!(fmt, "Floundered"),
52+
}
53+
}
54+
}
55+
2356
#[derive(Clone, Debug, HasInterner)]
2457
pub(crate) struct SlgContext<I: Interner> {
2558
phantom: PhantomData<I>,
@@ -53,7 +86,6 @@ pub struct TruncatingInferenceTable<I: Interner> {
5386
}
5487

5588
impl<I: Interner> context::Context<I> for SlgContext<I> {
56-
type Solution = Solution<I>;
5789
type InferenceTable = TruncatingInferenceTable<I>;
5890

5991
// Used by: logic

0 commit comments

Comments
 (0)