Skip to content

Commit 8ecdac6

Browse files
committed
Add cargo features to enable SLG or recursive solvers
Enabling one but not the other avoids compiling an unnecessary solver.
1 parent 896f786 commit 8ecdac6

File tree

7 files changed

+76
-17
lines changed

7 files changed

+76
-17
lines changed

chalk-ir/Cargo.toml

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,4 +12,9 @@ edition = "2018"
1212
[dependencies]
1313
chalk-engine-base = { version = "0.10.1-dev", path = "../chalk-engine-base" }
1414
chalk-derive = { version = "0.10.1-dev", path = "../chalk-derive" }
15-
chalk-engine = { version = "0.10.1-dev", path = "../chalk-engine" }
15+
chalk-engine = { version = "0.10.1-dev", path = "../chalk-engine", optional = true }
16+
17+
[features]
18+
default = ["slg-solver"]
19+
20+
slg-solver = ["chalk-engine"]

chalk-ir/src/fold/boring_impls.rs

Lines changed: 11 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -6,11 +6,12 @@
66
77
use crate::interner::TargetInterner;
88
use crate::*;
9-
use chalk_engine::context::Context;
10-
use chalk_engine::{ExClause, FlounderedSubgoal, Literal};
119
use std::marker::PhantomData;
1210
use std::sync::Arc;
1311

12+
#[cfg(feature = "slg-solver")]
13+
use chalk_engine::{context::Context, ExClause, FlounderedSubgoal, Literal};
14+
1415
impl<'a, T: Fold<I, TI>, I: Interner, TI: TargetInterner<I>> Fold<I, TI> for &'a T {
1516
type Result = T::Result;
1617
fn fold_with<'i>(
@@ -240,8 +241,6 @@ copy_fold!(usize);
240241
copy_fold!(PlaceholderIndex);
241242
copy_fold!(QuantifierKind);
242243
copy_fold!(DebruijnIndex);
243-
copy_fold!(chalk_engine::TableIndex);
244-
copy_fold!(chalk_engine::TimeStamp);
245244
copy_fold!(());
246245
copy_fold!(UintTy);
247246
copy_fold!(IntTy);
@@ -250,6 +249,11 @@ copy_fold!(Scalar);
250249
copy_fold!(ClausePriority);
251250
copy_fold!(Mutability);
252251

252+
#[cfg(feature = "slg-solver")]
253+
copy_fold!(chalk_engine::TableIndex);
254+
#[cfg(feature = "slg-solver")]
255+
copy_fold!(chalk_engine::TimeStamp);
256+
253257
#[macro_export]
254258
macro_rules! id_fold {
255259
($t:ident) => {
@@ -337,6 +341,7 @@ impl<I: Interner, TI: TargetInterner<I>> Fold<I, TI> for PhantomData<I> {
337341
}
338342
}
339343

344+
#[cfg(feature = "slg-solver")]
340345
impl<C: Context, I: Interner, TI: TargetInterner<I>> Fold<I, TI> for ExClause<C>
341346
where
342347
C: Context,
@@ -377,6 +382,7 @@ where
377382
}
378383
}
379384

385+
#[cfg(feature = "slg-solver")]
380386
impl<C: Context, I: Interner, TI: TargetInterner<I>> Fold<I, TI> for FlounderedSubgoal<C>
381387
where
382388
C: Context,
@@ -407,6 +413,7 @@ where
407413
}
408414
}
409415

416+
#[cfg(feature = "slg-solver")]
410417
impl<C: Context, I: Interner, TI: TargetInterner<I>> Fold<I, TI> for Literal<C>
411418
where
412419
C: Context,

chalk-ir/src/interner.rs

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -29,13 +29,14 @@ use crate::TyData;
2929
use crate::VariableKind;
3030
use crate::VariableKinds;
3131
use crate::{Const, ConstData};
32-
use chalk_engine::context::Context;
33-
use chalk_engine::ExClause;
3432
use std::fmt::{self, Debug};
3533
use std::hash::Hash;
3634
use std::marker::PhantomData;
3735
use std::sync::Arc;
3836

37+
#[cfg(feature = "slg-solver")]
38+
use chalk_engine::{context::Context, ExClause};
39+
3940
/// A "interner" encapsulates the concrete representation of
4041
/// certain "core types" from chalk-ir. All the types in chalk-ir are
4142
/// parameterized by a `I: Interner`, and so (e.g.) if they want to
@@ -755,6 +756,7 @@ impl<'a, T: HasInterner> HasInterner for std::slice::Iter<'a, T> {
755756
type Interner = T::Interner;
756757
}
757758

759+
#[cfg(feature = "slg-solver")]
758760
impl<C: HasInterner + Context> HasInterner for ExClause<C> {
759761
type Interner = <C as HasInterner>::Interner;
760762
}

chalk-ir/src/visit/boring_impls.rs

Lines changed: 11 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -10,9 +10,11 @@ use crate::{
1010
ProgramClauses, QuantifiedWhereClauses, QuantifierKind, Scalar, Substitution, SuperVisit,
1111
TraitId, UintTy, UniverseIndex, Visit, VisitResult, Visitor,
1212
};
13-
use chalk_engine::{context::Context, ExClause, FlounderedSubgoal, Literal};
1413
use std::{marker::PhantomData, sync::Arc};
1514

15+
#[cfg(feature = "slg-solver")]
16+
use chalk_engine::{context::Context, ExClause, FlounderedSubgoal, Literal};
17+
1618
/// Convenience function to visit all the items in the iterator it.
1719
pub fn visit_iter<'i, T, I, R>(
1820
it: impl Iterator<Item = T>,
@@ -203,8 +205,6 @@ const_visit!(usize);
203205
const_visit!(PlaceholderIndex);
204206
const_visit!(QuantifierKind);
205207
const_visit!(DebruijnIndex);
206-
const_visit!(chalk_engine::TableIndex);
207-
const_visit!(chalk_engine::TimeStamp);
208208
const_visit!(ClausePriority);
209209
const_visit!(());
210210
const_visit!(Scalar);
@@ -213,6 +213,11 @@ const_visit!(IntTy);
213213
const_visit!(FloatTy);
214214
const_visit!(Mutability);
215215

216+
#[cfg(feature = "slg-solver")]
217+
const_visit!(chalk_engine::TableIndex);
218+
#[cfg(feature = "slg-solver")]
219+
const_visit!(chalk_engine::TimeStamp);
220+
216221
#[macro_export]
217222
macro_rules! id_visit {
218223
($t:ident) => {
@@ -299,6 +304,7 @@ impl<I: Interner> Visit<I> for PhantomData<I> {
299304
}
300305
}
301306

307+
#[cfg(feature = "slg-solver")]
302308
impl<C: Context, I: Interner> Visit<I> for ExClause<C>
303309
where
304310
C: Context,
@@ -336,6 +342,7 @@ where
336342
}
337343
}
338344

345+
#[cfg(feature = "slg-solver")]
339346
impl<C: Context, I: Interner> Visit<I> for FlounderedSubgoal<C>
340347
where
341348
C: Context,
@@ -363,6 +370,7 @@ where
363370
}
364371
}
365372

373+
#[cfg(feature = "slg-solver")]
366374
impl<C: Context, I: Interner> Visit<I> for Literal<C>
367375
where
368376
C: Context,

chalk-solve/Cargo.toml

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -17,8 +17,14 @@ rustc-hash = { version = "1.0.0" }
1717

1818
chalk-engine-base = { version = "0.10.1-dev", path = "../chalk-engine-base" }
1919
chalk-derive = { version = "0.10.1-dev", path = "../chalk-derive" }
20-
chalk-engine = { version = "0.10.1-dev", path = "../chalk-engine" }
21-
chalk-ir = { version = "0.10.1-dev", path = "../chalk-ir" }
20+
chalk-engine = { version = "0.10.1-dev", path = "../chalk-engine", optional = true }
21+
chalk-ir = { version = "0.10.1-dev", path = "../chalk-ir", default-features = false }
2222

2323
[dev-dependencies]
2424
chalk-integration = { version = "0.10.1-dev", path = "../chalk-integration" }
25+
26+
[features]
27+
default = ["slg-solver", "recursive-solver"]
28+
29+
slg-solver = ["chalk-engine", "chalk-ir/slg-solver"]
30+
recursive-solver = []

chalk-solve/src/lib.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@ mod coinductive_goal;
1919
pub mod ext;
2020
pub mod goal_builder;
2121
mod infer;
22+
#[cfg(feature = "recursive-solver")]
2223
pub mod recursive;
2324
pub mod rust_ir;
2425
mod solve;

chalk-solve/src/solve.rs

Lines changed: 35 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,18 @@
1-
use crate::solve::slg::SlgContext;
2-
use crate::{recursive::RecursiveContext, RustIrDatabase};
3-
use chalk_engine::forest::{Forest, SubstitutionResult};
1+
use crate::RustIrDatabase;
42
use chalk_ir::interner::Interner;
53
use chalk_ir::*;
64
use std::fmt;
75

6+
#[cfg(feature = "slg-solver")]
7+
use {
8+
crate::solve::slg::SlgContext,
9+
chalk_engine::forest::{Forest, SubstitutionResult},
10+
};
11+
12+
#[cfg(feature = "recursive-solver")]
13+
use crate::recursive::RecursiveContext;
14+
15+
#[cfg(feature = "slg-solver")]
816
mod slg;
917
pub(crate) mod truncate;
1018

@@ -179,11 +187,13 @@ impl<'a, I: Interner> fmt::Display for SolutionDisplay<'a, I> {
179187
#[derive(Copy, Clone, Debug, PartialOrd, Ord, PartialEq, Eq, Hash)]
180188
pub enum SolverChoice {
181189
/// Run the SLG solver, producing a Solution.
190+
#[cfg(feature = "slg-solver")]
182191
SLG {
183192
max_size: usize,
184193
expected_answers: Option<usize>,
185194
},
186195
/// Run the recursive solver.
196+
#[cfg(feature = "recursive-solver")]
187197
Recursive {
188198
overflow_depth: usize,
189199
caching_enabled: bool,
@@ -192,6 +202,7 @@ pub enum SolverChoice {
192202

193203
impl SolverChoice {
194204
/// Returns specific SLG parameters.
205+
#[cfg(feature = "slg-solver")]
195206
pub fn slg(max_size: usize, expected_answers: Option<usize>) -> Self {
196207
SolverChoice::SLG {
197208
max_size,
@@ -200,11 +211,13 @@ impl SolverChoice {
200211
}
201212

202213
/// Returns the default SLG parameters.
214+
#[cfg(feature = "slg-solver")]
203215
pub fn slg_default() -> Self {
204216
SolverChoice::slg(10, None)
205217
}
206218

207219
/// Returns the default recursive solver setup.
220+
#[cfg(feature = "recursive-solver")]
208221
pub fn recursive() -> Self {
209222
SolverChoice::Recursive {
210223
overflow_depth: 100,
@@ -215,12 +228,14 @@ impl SolverChoice {
215228
/// Creates a solver state.
216229
pub fn into_solver<I: Interner>(self) -> Solver<I> {
217230
match self {
231+
#[cfg(feature = "slg-solver")]
218232
SolverChoice::SLG {
219233
max_size,
220234
expected_answers,
221235
} => Solver(SolverImpl::Slg {
222236
forest: Box::new(Forest::new(SlgContext::new(max_size, expected_answers))),
223237
}),
238+
#[cfg(feature = "recursive-solver")]
224239
SolverChoice::Recursive {
225240
overflow_depth,
226241
caching_enabled,
@@ -232,10 +247,17 @@ impl SolverChoice {
232247
}
233248
}
234249

250+
#[cfg(feature = "slg-solver")]
235251
impl Default for SolverChoice {
236252
fn default() -> Self {
237-
// SolverChoice::recursive()
238-
SolverChoice::slg(10, None)
253+
SolverChoice::slg_default()
254+
}
255+
}
256+
257+
#[cfg(all(not(feature = "slg-solver"), feature = "recursive-solver"))]
258+
impl Default for SolverChoice {
259+
fn default() -> Self {
260+
SolverChoice::recursive()
239261
}
240262
}
241263

@@ -246,7 +268,9 @@ impl Default for SolverChoice {
246268
pub struct Solver<I: Interner>(SolverImpl<I>);
247269

248270
enum SolverImpl<I: Interner> {
271+
#[cfg(feature = "slg-solver")]
249272
Slg { forest: Box<Forest<SlgContext<I>>> },
273+
#[cfg(feature = "recursive-solver")]
250274
Recursive(Box<RecursiveContext<I>>),
251275
}
252276

@@ -275,10 +299,12 @@ impl<I: Interner> Solver<I> {
275299
goal: &UCanonical<InEnvironment<Goal<I>>>,
276300
) -> Option<Solution<I>> {
277301
match &mut self.0 {
302+
#[cfg(feature = "slg-solver")]
278303
SolverImpl::Slg { forest } => {
279304
let ops = forest.context().ops(program);
280305
forest.solve(&ops, goal, || true)
281306
}
307+
#[cfg(feature = "recursive-solver")]
282308
SolverImpl::Recursive(ctx) => ctx.solver(program).solve_root_goal(goal).ok(),
283309
}
284310
}
@@ -312,10 +338,12 @@ impl<I: Interner> Solver<I> {
312338
should_continue: impl std::ops::Fn() -> bool,
313339
) -> Option<Solution<I>> {
314340
match &mut self.0 {
341+
#[cfg(feature = "slg-solver")]
315342
SolverImpl::Slg { forest } => {
316343
let ops = forest.context().ops(program);
317344
forest.solve(&ops, goal, should_continue)
318345
}
346+
#[cfg(feature = "recursive-solver")]
319347
SolverImpl::Recursive(ctx) => {
320348
// TODO support should_continue in recursive solver
321349
ctx.solver(program).solve_root_goal(goal).ok()
@@ -345,6 +373,7 @@ impl<I: Interner> Solver<I> {
345373
///
346374
/// - `true` all solutions were processed with the function.
347375
/// - `false` the function returned `false` and solutions were interrupted.
376+
#[cfg(feature = "slg-solver")]
348377
pub fn solve_multiple(
349378
&mut self,
350379
program: &dyn RustIrDatabase<I>,
@@ -356,6 +385,7 @@ impl<I: Interner> Solver<I> {
356385
let ops = forest.context().ops(program);
357386
forest.solve_multiple(&ops, goal, f)
358387
}
388+
#[cfg(feature = "recursive-solver")]
359389
SolverImpl::Recursive(_ctx) => unimplemented!(),
360390
}
361391
}

0 commit comments

Comments
 (0)