Skip to content

Commit 4defa33

Browse files
authored
Merge pull request #78 from nikomatsakis/kill-eager-slg
add answer abstraction to on-demand solver; remove eager SLG solver
2 parents b0d1417 + ac66730 commit 4defa33

40 files changed

+1091
-3295
lines changed

src/bin/chalki.rs

Lines changed: 13 additions & 56 deletions
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,6 @@ use std::process::exit;
1818

1919
use chalk::ir;
2020
use chalk::lower::*;
21-
use chalk::solve::slg;
2221
use chalk::solve::SolverChoice;
2322
use docopt::Docopt;
2423
use rustyline::error::ReadlineError;
@@ -35,8 +34,7 @@ Options:
3534
--program=PATH Specifies the path to the `.chalk` file containing traits/impls.
3635
--goal=GOAL Specifies a goal to evaluate (may be given more than once).
3736
--overflow-depth=N Specifies the overflow depth [default: 10].
38-
--solver S Selects a solver (recursive, slg-eager, or slg-on-demand) [default: recursive]
39-
--all-answers When using SLG solver, dump out each individual answer.
37+
--solver S Selects a solver (recursive, slg) [default: recursive]
4038
--no-cache Disable caching.
4139
";
4240

@@ -46,7 +44,6 @@ struct Args {
4644
flag_goal: Vec<String>,
4745
flag_overflow_depth: usize,
4846
flag_solver: String,
49-
flag_all_answers: bool,
5047
flag_no_cache: bool,
5148
}
5249

@@ -90,24 +87,10 @@ fn run() -> Result<()> {
9087

9188
let mut prog = None;
9289

93-
let solver_choice = match args.solver_choice() {
94-
Some(s) => s,
95-
None => {
96-
eprintln!("error: invalid solver choice `{}`", args.flag_solver);
97-
eprintln!("try `recursive`, `slg-eager`, or `slg-on-demand`");
98-
exit(1);
99-
}
100-
};
101-
102-
if args.flag_all_answers {
103-
match solver_choice {
104-
SolverChoice::SLG { eager: true, .. } => { }
105-
_ => {
106-
eprintln!("error: in order to report all answers, \
107-
you must use the `slg-eager` solver");
108-
exit(1);
109-
}
110-
}
90+
if let None = args.solver_choice() {
91+
eprintln!("error: invalid solver choice `{}`", args.flag_solver);
92+
eprintln!("try `recursive` or `slg`");
93+
exit(1);
11194
}
11295

11396
if let Some(program) = &args.flag_program {
@@ -135,7 +118,7 @@ fn run() -> Result<()> {
135118
}
136119
};
137120

138-
ir::set_current_program(&prog.ir, || -> Result<()> {
121+
ir::tls::set_current_program(&prog.ir, || -> Result<()> {
139122
for g in &args.flag_goal {
140123
if let Err(e) = goal(&args, g, &prog) {
141124
eprintln!("error: {}", e);
@@ -185,7 +168,7 @@ fn process(
185168
*prog = Some(load_program(args, filename)?);
186169
} else {
187170
let prog = prog.as_ref().ok_or("no program currently loaded")?;
188-
ir::set_current_program(&prog.ir, || -> Result<()> {
171+
ir::tls::set_current_program(&prog.ir, || -> Result<()> {
189172
match command {
190173
"print" => println!("{}", prog.text),
191174
"lowered" => println!("{:#?}", prog.env),
@@ -228,45 +211,19 @@ fn read_program(rl: &mut rustyline::Editor<()>) -> Result<String> {
228211
fn goal(args: &Args, text: &str, prog: &Program) -> Result<()> {
229212
let goal = chalk_parse::parse_goal(text)?.lower(&*prog.ir)?;
230213
let peeled_goal = goal.into_peeled_goal();
231-
if args.flag_all_answers {
232-
match slg::solve_root_goal(args.flag_overflow_depth, &prog.env, &peeled_goal) {
233-
Ok(slg::SimplifiedAnswers { answers }) => if answers.is_empty() {
234-
println!("No answers found.");
235-
} else {
236-
println!("{} answer(s) found:", answers.len());
237-
for answer in &answers {
238-
println!(
239-
"- {}{}",
240-
answer.subst,
241-
if answer.ambiguous { " [ambiguous]" } else { "" }
242-
);
243-
}
244-
},
245-
Err(error) => {
246-
println!("exploration error: {:?}\n", error);
247-
}
248-
}
249-
} else {
250-
let solver_choice = args.solver_choice().unwrap();
251-
match solver_choice.solve_root_goal(&prog.env, &peeled_goal) {
252-
Ok(Some(v)) => println!("{}\n", v),
253-
Ok(None) => println!("No possible solution.\n"),
254-
Err(e) => println!("Solver failed: {}", e),
255-
}
214+
let solver_choice = args.solver_choice().unwrap();
215+
match solver_choice.solve_root_goal(&prog.env, &peeled_goal) {
216+
Ok(Some(v)) => println!("{}\n", v),
217+
Ok(None) => println!("No possible solution.\n"),
218+
Err(e) => println!("Solver failed: {}", e),
256219
}
257220
Ok(())
258221
}
259222

260223
impl Args {
261224
fn solver_choice(&self) -> Option<SolverChoice> {
262225
match &self.flag_solver[..] {
263-
"slg-eager" => Some(SolverChoice::SLG {
264-
eager: true,
265-
max_size: self.flag_overflow_depth,
266-
}),
267-
268-
"slg-on-demand" => Some(SolverChoice::SLG {
269-
eager: false,
226+
"slg" => Some(SolverChoice::SLG {
270227
max_size: self.flag_overflow_depth,
271228
}),
272229

src/cast.rs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ use std::marker::PhantomData;
2626
/// as part of this, they should always use the same set of free
2727
/// variables (the `Canonical` implementation, for example, relies on
2828
/// that).
29-
pub trait Cast<T>: Sized {
29+
crate trait Cast<T>: Sized {
3030
fn cast(self) -> T;
3131
}
3232

@@ -232,7 +232,7 @@ where
232232
}
233233
}
234234

235-
pub struct Casted<I, U> {
235+
crate struct Casted<I, U> {
236236
iterator: I,
237237
_cast: PhantomData<U>,
238238
}
@@ -254,7 +254,7 @@ where
254254

255255
/// An iterator adapter that casts each element we are iterating over
256256
/// to some other type.
257-
pub trait Caster<U>: Sized {
257+
crate trait Caster<U>: Sized {
258258
fn casted(self) -> Casted<Self, U>;
259259
}
260260

src/coherence/mod.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,8 @@ mod solve;
99

1010

1111
impl Program {
12-
pub fn record_specialization_priorities(&mut self, solver_choice: SolverChoice) -> Result<()> {
13-
ir::set_current_program(&Arc::new(self.clone()), || {
12+
crate fn record_specialization_priorities(&mut self, solver_choice: SolverChoice) -> Result<()> {
13+
ir::tls::set_current_program(&Arc::new(self.clone()), || {
1414
let forest = self.build_specialization_forest(solver_choice)?;
1515

1616
// Visit every root in the forest & set specialization

src/fold/mod.rs

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ use std::sync::Arc;
99
crate mod shift;
1010
mod subst;
1111

12-
pub use self::subst::Subst;
12+
crate use self::subst::Subst;
1313

1414
/// A "folder" is a transformer that can be used to make a copy of
1515
/// some term -- that is, some bit of IR, such as a `Goal` -- with
@@ -51,14 +51,14 @@ pub use self::subst::Subst;
5151
/// ```rust,ignore
5252
/// let x = x.fold_with(&mut folder, 0);
5353
/// ```
54-
pub trait Folder: ExistentialFolder + UniversalFolder + TypeFolder {
54+
crate trait Folder: ExistentialFolder + UniversalFolder + TypeFolder {
5555
/// Returns a "dynamic" version of this trait. There is no
5656
/// **particular** reason to require this, except that I didn't
5757
/// feel like making `super_fold_ty` generic for no reason.
5858
fn to_dyn(&mut self) -> &mut Folder;
5959
}
6060

61-
pub trait TypeFolder {
61+
crate trait TypeFolder {
6262
fn fold_ty(&mut self, ty: &Ty, binders: usize) -> Fallible<Ty>;
6363
fn fold_lifetime(&mut self, lifetime: &Lifetime, binders: usize) -> Fallible<Lifetime>;
6464
}
@@ -74,7 +74,7 @@ impl<T: ExistentialFolder + UniversalFolder + TypeFolder> Folder for T {
7474
/// their contents (note that free variables that are encountered in
7575
/// that process may still be substituted). The vast majority of
7676
/// folders implement this trait.
77-
pub trait DefaultTypeFolder {}
77+
crate trait DefaultTypeFolder {}
7878

7979
impl<T: ExistentialFolder + UniversalFolder + DefaultTypeFolder> TypeFolder for T {
8080
fn fold_ty(&mut self, ty: &Ty, binders: usize) -> Fallible<Ty> {
@@ -90,7 +90,7 @@ impl<T: ExistentialFolder + UniversalFolder + DefaultTypeFolder> TypeFolder for
9090
/// variables**; for example, if you folded over `Foo<?T> }`, where `?T`
9191
/// is an inference variable, then this would let you replace `?T` with
9292
/// some other type.
93-
pub trait ExistentialFolder {
93+
crate trait ExistentialFolder {
9494
/// Invoked for `Ty::Var` instances that are not bound within the type being folded
9595
/// over:
9696
///
@@ -112,7 +112,7 @@ pub trait ExistentialFolder {
112112
/// A convenience trait. If you implement this, you get an
113113
/// implementation of `UniversalFolder` for free that simply ignores
114114
/// universal values (that is, it replaces them with themselves).
115-
pub trait IdentityExistentialFolder {}
115+
crate trait IdentityExistentialFolder {}
116116

117117
impl<T: IdentityExistentialFolder> ExistentialFolder for T {
118118
fn fold_free_existential_ty(&mut self, depth: usize, binders: usize) -> Fallible<Ty> {
@@ -128,7 +128,7 @@ impl<T: IdentityExistentialFolder> ExistentialFolder for T {
128128
}
129129
}
130130

131-
pub trait UniversalFolder {
131+
crate trait UniversalFolder {
132132
/// Invoked for `Ty::Apply` instances where the type name is a `TypeName::ForAll`.
133133
/// Returns a type to use instead, which should be suitably shifted to account for `binders`.
134134
///
@@ -147,7 +147,7 @@ pub trait UniversalFolder {
147147
/// A convenience trait. If you implement this, you get an
148148
/// implementation of `UniversalFolder` for free that simply ignores
149149
/// universal values (that is, it replaces them with themselves).
150-
pub trait IdentityUniversalFolder {}
150+
crate trait IdentityUniversalFolder {}
151151

152152
impl<T: IdentityUniversalFolder> UniversalFolder for T {
153153
fn fold_free_universal_ty(&mut self, universe: UniverseIndex, _binders: usize) -> Fallible<Ty> {
@@ -164,7 +164,7 @@ impl<T: IdentityUniversalFolder> UniversalFolder for T {
164164
}
165165

166166
/// Applies the given folder to a value.
167-
pub trait Fold: Debug {
167+
crate trait Fold: Debug {
168168
/// The type of value that will be produced once folding is done.
169169
/// Typically this is `Self`, unless `Self` contains borrowed
170170
/// values, in which case owned values are produced (for example,
@@ -243,7 +243,7 @@ impl Fold for Ty {
243243
}
244244
}
245245

246-
pub fn super_fold_ty(folder: &mut Folder, ty: &Ty, binders: usize) -> Fallible<Ty> {
246+
crate fn super_fold_ty(folder: &mut Folder, ty: &Ty, binders: usize) -> Fallible<Ty> {
247247
match *ty {
248248
Ty::Var(depth) => if depth >= binders {
249249
folder.fold_free_existential_ty(depth - binders, binders)
@@ -337,7 +337,7 @@ impl Fold for Lifetime {
337337
}
338338
}
339339

340-
pub fn super_fold_lifetime(
340+
crate fn super_fold_lifetime(
341341
folder: &mut Folder,
342342
lifetime: &Lifetime,
343343
binders: usize,

src/fold/shift.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ use super::{DefaultTypeFolder, ExistentialFolder, Fold, IdentityUniversalFolder}
44

55
/// Methods for converting debruijn indices to move values into or out
66
/// of binders.
7-
pub trait Shift: Fold {
7+
crate trait Shift: Fold {
88
/// Shifts debruijn indices in `self` **up**, which is used when a
99
/// value is being placed under additional levels of binders.
1010
///

src/fold/subst.rs

Lines changed: 3 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -3,25 +3,21 @@ use ir::*;
33

44
use super::*;
55

6-
pub struct Subst<'s> {
6+
crate struct Subst<'s> {
77
/// Values to substitute. A reference to a free variable with
88
/// index `i` will be mapped to `parameters[i]` -- if `i >
99
/// parameters.len()`, then we will leave the variable untouched.
1010
parameters: &'s [Parameter],
1111
}
1212

1313
impl<'s> Subst<'s> {
14-
pub fn new(parameters: &'s [Parameter]) -> Subst<'s> {
15-
Subst { parameters }
16-
}
17-
18-
pub fn apply<T: Fold>(parameters: &[Parameter], value: &T) -> T::Result {
14+
crate fn apply<T: Fold>(parameters: &[Parameter], value: &T) -> T::Result {
1915
value.fold_with(&mut Subst { parameters }, 0).unwrap()
2016
}
2117
}
2218

2319
impl QuantifiedTy {
24-
pub fn substitute(&self, parameters: &[Parameter]) -> Ty {
20+
crate fn substitute(&self, parameters: &[Parameter]) -> Ty {
2521
assert_eq!(self.num_binders, parameters.len());
2622
Subst::apply(parameters, &self.ty)
2723
}

src/ir/could_match.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ use ir::*;
33
use zip::{Zip, Zipper};
44

55
/// A fast check to see whether two things could ever possibly match.
6-
pub trait CouldMatch<T> {
6+
crate trait CouldMatch<T> {
77
fn could_match(&self, other: &T) -> bool;
88
}
99

src/ir/debug.rs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ use super::*;
44

55
impl Debug for ItemId {
66
fn fmt(&self, fmt: &mut Formatter) -> Result<(), Error> {
7-
with_current_program(|p| match p {
7+
tls::with_current_program(|p| match p {
88
Some(prog) => if let Some(k) = prog.type_kinds.get(self) {
99
write!(fmt, "{}", k.name)
1010
} else if let Some(k) = prog.associated_ty_data.get(self) {
@@ -95,7 +95,7 @@ impl Debug for TraitRef {
9595

9696
impl Debug for ProjectionTy {
9797
fn fmt(&self, fmt: &mut Formatter) -> Result<(), Error> {
98-
with_current_program(|p| match p {
98+
tls::with_current_program(|p| match p {
9999
Some(program) => {
100100
let (associated_ty_data, trait_params, other_params) =
101101
program.split_projection(self);
@@ -131,7 +131,7 @@ impl Debug for UnselectedProjectionTy {
131131
}
132132
}
133133

134-
pub struct Angle<'a, T: 'a>(pub &'a [T]);
134+
crate struct Angle<'a, T: 'a>(pub &'a [T]);
135135

136136
impl<'a, T: Debug> Debug for Angle<'a, T> {
137137
fn fmt(&self, fmt: &mut Formatter) -> Result<(), Error> {

0 commit comments

Comments
 (0)