Skip to content

Commit 013544c

Browse files
authored
Merge pull request #202 from tmandry/finer-salsa
[WIP] Finer-grained salsa queries
2 parents 083d843 + 0d9fa8b commit 013544c

File tree

17 files changed

+196
-4082
lines changed

17 files changed

+196
-4082
lines changed

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

Lines changed: 0 additions & 1115 deletions
This file was deleted.

chalk-solve/src/solve/test.rs

Lines changed: 0 additions & 2848 deletions
This file was deleted.

chalk-solve/src/solve/test/bench.rs

Lines changed: 23 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -3,35 +3,38 @@
33
extern crate test;
44
use self::test::Bencher;
55

6+
use crate::db::ChalkDatabase;
7+
use crate::query::{ProgramSolverChoice, ProgramText};
8+
use chalk_solve::solve::SolverChoice;
69
use ir;
710
use ir::solve::SolverChoice;
811
use std::sync::Arc;
912

10-
use super::{parse_and_lower_program,
11-
parse_and_lower_goal,
12-
assert_result};
13+
use super::{assert_result, parse_and_lower_goal, parse_and_lower_program};
1314

1415
fn run_bench(
1516
program_text: &str,
1617
solver_choice: SolverChoice,
1718
goal_text: &str,
1819
bencher: &mut Bencher,
19-
expected: &str
20+
expected: &str,
2021
) {
21-
let program = Arc::new(parse_and_lower_program(program_text, solver_choice).unwrap());
22-
let env = Arc::new(program.environment());
23-
ir::tls::set_current_program(&program, || {
24-
let goal = parse_and_lower_goal(&program, goal_text).unwrap();
25-
let peeled_goal = goal.into_peeled_goal();
26-
27-
// Execute once to get an expected result.
28-
let result = solver_choice.solve_root_goal(&env, &peeled_goal);
29-
30-
// Check expectation.
31-
assert_result(&result, expected);
32-
33-
// Then do it many times to measure time.
34-
bencher.iter(|| solver_choice.solve_root_goal(&env, &peeled_goal));
22+
ChalkDatabase::with_program(Arc::new(program_text.to_string()), solver_choice, |db| {
23+
let program = db.lowered_program().unwrap();
24+
let env = db.environment().unwrap();
25+
ir::tls::set_current_program(&program, || {
26+
let goal = parse_and_lower_goal(&program, goal_text).unwrap();
27+
let peeled_goal = goal.into_peeled_goal();
28+
29+
// Execute once to get an expected result.
30+
let result = solver_choice.solve_root_goal(&env, &peeled_goal);
31+
32+
// Check expectation.
33+
assert_result(&result, expected);
34+
35+
// Then do it many times to measure time.
36+
bencher.iter(|| solver_choice.solve_root_goal(&env, &peeled_goal));
37+
});
3538
});
3639
}
3740

@@ -101,11 +104,9 @@ forall<T> {
101104
fn cycley_slg(b: &mut Bencher) {
102105
run_bench(
103106
CYCLEY,
104-
SolverChoice::SLG {
105-
max_size: 20,
106-
},
107+
SolverChoice::SLG { max_size: 20 },
107108
CYCLEY_GOAL,
108109
b,
109-
"Unique"
110+
"Unique",
110111
);
111112
}

src/bin/chalki.rs

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,8 @@ use std::io::Read;
1717
use std::process::exit;
1818
use std::sync::Arc;
1919

20+
use chalk::db::ChalkDatabase;
21+
use chalk::query::LoweringDatabase;
2022
use chalk::rust_ir;
2123
use chalk::rust_ir::lowering::*;
2224
use chalk_engine::fallible::NoSolution;
@@ -74,9 +76,11 @@ impl Program {
7476
///
7577
/// [`SolverChoice`]: struct.solve.SolverChoice.html
7678
fn new(text: String, solver_choice: SolverChoice) -> Result<Program> {
77-
let ir = Arc::new(chalk_parse::parse_program(&text)?.lower(solver_choice)?);
78-
let env = Arc::new(ir.environment());
79-
Ok(Program { text, ir, env })
79+
ChalkDatabase::with_program(Arc::new(text.clone()), solver_choice, |db| {
80+
let ir = db.checked_program().unwrap();
81+
let env = db.environment().unwrap();
82+
Ok(Program { text, ir, env })
83+
})
8084
}
8185
}
8286

src/coherence.rs

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -2,21 +2,23 @@ use petgraph::prelude::*;
22

33
use crate::errors::Result;
44
use crate::rust_ir::Program;
5+
use chalk_ir::ProgramEnvironment;
56
use chalk_ir::{self, ItemId};
67
use chalk_solve::solve::SolverChoice;
78
use std::sync::Arc;
89

9-
mod orphan;
10+
crate mod orphan;
1011
mod solve;
1112
mod test;
1213

1314
impl Program {
1415
crate fn record_specialization_priorities(
1516
&mut self,
17+
env: Arc<ProgramEnvironment>,
1618
solver_choice: SolverChoice,
1719
) -> Result<()> {
1820
chalk_ir::tls::set_current_program(&Arc::new(self.clone()), || {
19-
let forest = self.build_specialization_forest(solver_choice)?;
21+
let forest = self.build_specialization_forest(env, solver_choice)?;
2022

2123
// Visit every root in the forest & set specialization
2224
// priority for the tree that is the root of.
@@ -31,6 +33,7 @@ impl Program {
3133
// Build the forest of specialization relationships.
3234
fn build_specialization_forest(
3335
&self,
36+
env: Arc<ProgramEnvironment>,
3437
solver_choice: SolverChoice,
3538
) -> Result<Graph<ItemId, ()>> {
3639
// The forest is returned as a graph but built as a GraphMap; this is
@@ -40,7 +43,7 @@ impl Program {
4043
// Find all specializations (implemented in coherence/solve)
4144
// Record them in the forest by adding an edge from the less special
4245
// to the more special.
43-
self.visit_specializations(solver_choice, |less_special, more_special| {
46+
self.visit_specializations(env, solver_choice, |less_special, more_special| {
4447
forest.add_edge(less_special, more_special, ());
4548
})?;
4649

src/coherence/orphan.rs

Lines changed: 18 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -12,29 +12,28 @@ struct OrphanSolver {
1212
solver_choice: SolverChoice,
1313
}
1414

15-
impl Program {
16-
crate fn perform_orphan_check(&self, solver_choice: SolverChoice) -> Result<()> {
17-
let solver = OrphanSolver {
18-
env: Arc::new(self.environment()),
19-
solver_choice,
20-
};
15+
crate fn perform_orphan_check(
16+
program: Arc<Program>,
17+
env: Arc<ProgramEnvironment>,
18+
solver_choice: SolverChoice,
19+
) -> Result<()> {
20+
let solver = OrphanSolver { env, solver_choice };
2121

22-
let local_impls = self
23-
.impl_data
24-
.values()
25-
// Only keep local impls (i.e. impls in the current crate)
26-
.filter(|impl_datum| impl_datum.binders.value.impl_type == ImplType::Local);
22+
let local_impls = program
23+
.impl_data
24+
.values()
25+
// Only keep local impls (i.e. impls in the current crate)
26+
.filter(|impl_datum| impl_datum.binders.value.impl_type == ImplType::Local);
2727

28-
for impl_datum in local_impls {
29-
if !solver.orphan_check(impl_datum) {
30-
let trait_id = impl_datum.binders.value.trait_ref.trait_ref().trait_id;
31-
let trait_id = self.type_kinds.get(&trait_id).unwrap().name;
32-
return Err(Error::from_kind(ErrorKind::FailedOrphanCheck(trait_id)));
33-
}
28+
for impl_datum in local_impls {
29+
if !solver.orphan_check(impl_datum) {
30+
let trait_id = impl_datum.binders.value.trait_ref.trait_ref().trait_id;
31+
let trait_id = program.type_kinds.get(&trait_id).unwrap().name;
32+
return Err(Error::from_kind(ErrorKind::FailedOrphanCheck(trait_id)));
3433
}
35-
36-
Ok(())
3734
}
35+
36+
Ok(())
3837
}
3938

4039
impl OrphanSolver {

src/coherence/solve.rs

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -17,16 +17,14 @@ struct DisjointSolver {
1717
impl Program {
1818
pub(super) fn visit_specializations<F>(
1919
&self,
20+
env: Arc<ProgramEnvironment>,
2021
solver_choice: SolverChoice,
2122
mut record_specialization: F,
2223
) -> Result<()>
2324
where
2425
F: FnMut(ItemId, ItemId),
2526
{
26-
let mut solver = DisjointSolver {
27-
env: Arc::new(self.environment()),
28-
solver_choice,
29-
};
27+
let mut solver = DisjointSolver { env, solver_choice };
3028

3129
// Create a vector of references to impl datums, sorted by trait ref.
3230
let impl_data = self

src/db.rs

Lines changed: 24 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,21 +1,43 @@
1-
use crate::query;
1+
use crate::query::{self, ProgramSolverChoice, ProgramText};
2+
use chalk_solve::solve::SolverChoice;
3+
use salsa::Database;
4+
use std::sync::Arc;
25

36
#[derive(Default)]
47
pub struct ChalkDatabase {
58
runtime: salsa::Runtime<ChalkDatabase>,
69
}
710

8-
impl salsa::Database for ChalkDatabase {
11+
impl Database for ChalkDatabase {
912
fn salsa_runtime(&self) -> &salsa::Runtime<ChalkDatabase> {
1013
&self.runtime
1114
}
1215
}
1316

17+
impl ChalkDatabase {
18+
pub fn with_program<F: FnOnce(&mut ChalkDatabase) -> R, R>(
19+
program_text: Arc<String>,
20+
solver_choice: SolverChoice,
21+
f: F,
22+
) -> R {
23+
let mut db = ChalkDatabase::default();
24+
25+
db.query_mut(ProgramText).set((), program_text);
26+
db.query_mut(ProgramSolverChoice).set((), solver_choice);
27+
28+
f(&mut db)
29+
}
30+
}
31+
1432
salsa::database_storage! {
1533
pub struct DatabaseStorage for ChalkDatabase {
1634
impl query::LoweringDatabase {
1735
fn program_text() for query::ProgramText;
36+
fn solver_choice() for query::ProgramSolverChoice;
37+
fn program_ir() for query::ProgramIr;
1838
fn lowered_program() for query::LoweredProgram;
39+
fn checked_program() for query::CheckedProgram;
40+
fn environment() for query::Environment;
1941
}
2042
}
2143
}

src/lib.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ crate mod coherence;
3030
pub mod errors;
3131
crate mod rules;
3232

33-
mod db;
34-
mod query;
33+
pub mod db;
34+
pub mod query;
3535

3636
mod test;

src/query.rs

Lines changed: 59 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,11 @@
11
// https://crates.io/crates/salsa
22
// hello world https://github.com/salsa-rs/salsa/blob/master/examples/hello_world/main.rs
33

4+
use crate::coherence::orphan;
5+
use crate::rules::wf;
46
use crate::rust_ir;
57
use crate::rust_ir::lowering::LowerProgram;
8+
use chalk_ir::ProgramEnvironment;
69
use chalk_solve::solve::SolverChoice;
710
use std::sync::Arc;
811

@@ -14,24 +17,71 @@ salsa::query_group! {
1417
storage input;
1518
}
1619

17-
// FIXME: Arc<Result<...>> is only needed because the error type is not clone
18-
fn lowered_program(solver_choice: SolverChoice) -> Result<Arc<rust_ir::Program>, String> {
20+
fn solver_choice() -> SolverChoice {
21+
type ProgramSolverChoice;
22+
23+
storage input;
24+
}
25+
26+
// FIXME: Result<..., String> is only needed because the error type is not clone
27+
28+
/// The program IR before recording specialization priorities.
29+
/// Do not use this query directly.
30+
fn program_ir() -> Result<Arc<rust_ir::Program>, String> {
31+
type ProgramIr;
32+
}
33+
34+
/// The lowered IR.
35+
fn lowered_program() -> Result<Arc<rust_ir::Program>, String> {
1936
type LoweredProgram;
37+
}
38+
39+
/// The lowered IR, with checks performed.
40+
fn checked_program() -> Result<Arc<rust_ir::Program>, String> {
41+
type CheckedProgram;
42+
}
2043

21-
// FIXME: only volatile because the Error type does not implement Eq
22-
storage volatile;
44+
/// The program as logic.
45+
fn environment() -> Result<Arc<ProgramEnvironment>, String> {
46+
type Environment;
2347
}
2448
}
2549
}
2650

27-
fn lowered_program(
28-
db: &impl LoweringDatabase,
29-
solver_choice: SolverChoice,
30-
) -> Result<Arc<rust_ir::Program>, String> {
51+
fn program_ir(db: &impl LoweringDatabase) -> Result<Arc<rust_ir::Program>, String> {
3152
let x: crate::errors::Result<_> = try {
3253
let text = db.program_text();
33-
Arc::new(chalk_parse::parse_program(&text)?.lower(solver_choice)?)
54+
Arc::new(chalk_parse::parse_program(&text)?.lower()?)
3455
};
3556

3657
x.map_err(|err| err.to_string())
3758
}
59+
60+
fn lowered_program(db: &impl LoweringDatabase) -> Result<Arc<rust_ir::Program>, String> {
61+
let mut program = db.program_ir()?;
62+
let env = db.environment()?;
63+
64+
let x: crate::errors::Result<_> = try {
65+
Arc::make_mut(&mut program).record_specialization_priorities(env, db.solver_choice())?;
66+
program
67+
};
68+
69+
x.map_err(|err| err.to_string())
70+
}
71+
72+
fn checked_program(db: &impl LoweringDatabase) -> Result<Arc<rust_ir::Program>, String> {
73+
let program = db.lowered_program()?;
74+
let env = db.environment()?;
75+
76+
let x: crate::errors::Result<_> = try {
77+
orphan::perform_orphan_check(program.clone(), env.clone(), db.solver_choice())?;
78+
wf::verify_well_formedness(program.clone(), env, db.solver_choice())?;
79+
program
80+
};
81+
x.map_err(|err| err.to_string())
82+
}
83+
84+
fn environment(db: &impl LoweringDatabase) -> Result<Arc<ProgramEnvironment>, String> {
85+
let env = db.program_ir()?.environment();
86+
Ok(Arc::new(env))
87+
}

src/rules.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ use chalk_ir::*;
66
use std::iter;
77

88
mod default;
9-
mod wf;
9+
crate mod wf;
1010

1111
impl Program {
1212
pub fn environment(&self) -> ProgramEnvironment {

0 commit comments

Comments
 (0)