Merge pull request #197 from nikomatsakis/salsaify

introduce salsa and use a really coarse-grained query

Author: nikomatsakis

Cargo.lock

@@ -17,6 +17,7 @@ itertools = "0.7.8"
 lalrpop-intern = "0.15.1"
 petgraph = "0.4.13"
 rustyline = "1.0"
+salsa = "0.9.1"
 serde = "1.0"
 serde_derive = "1.0"
 stacker = "0.1.2"

Cargo.toml

@@ -1,5 +1,6 @@
 use super::*;
 use crate::fold::shift::Shift;
+use crate::*;
 
 pub struct Subst<'s> {
     /// Values to substitute. A reference to a free variable with

chalk-ir/src/fold/subst.rs

@@ -0,0 +1,21 @@
+use crate::query;
+
+#[derive(Default)]
+pub struct ChalkDatabase {
+    runtime: salsa::Runtime<ChalkDatabase>,
+}
+
+impl salsa::Database for ChalkDatabase {
+    fn salsa_runtime(&self) -> &salsa::Runtime<ChalkDatabase> {
+        &self.runtime
+    }
+}
+
+salsa::database_storage! {
+    pub struct DatabaseStorage for ChalkDatabase {
+        impl query::LoweringDatabase {
+            fn program_text() for query::ProgramText;
+            fn lowered_program() for query::LoweredProgram;
+        }
+    }
+}

src/db.rs

@@ -4,6 +4,7 @@
 #![feature(in_band_lifetimes)]
 #![feature(specialization)]
 #![feature(step_trait)]
+#![feature(try_blocks)]
 
 extern crate chalk_parse;
 #[macro_use]
@@ -29,4 +30,7 @@ crate mod coherence;
 pub mod errors;
 crate mod rules;
 
+mod db;
+mod query;
+
 mod test;

src/lib.rs

@@ -0,0 +1,37 @@
+// https://crates.io/crates/salsa
+// hello world https://github.com/salsa-rs/salsa/blob/master/examples/hello_world/main.rs
+
+use crate::rust_ir;
+use crate::rust_ir::lowering::LowerProgram;
+use chalk_solve::solve::SolverChoice;
+use std::sync::Arc;
+
+salsa::query_group! {
+    pub trait LoweringDatabase: salsa::Database {
+        fn program_text() -> Arc<String> {
+            type ProgramText;
+
+            storage input;
+        }
+
+        // FIXME: Arc<Result<...>> is only needed because the error type is not clone
+        fn lowered_program(solver_choice: SolverChoice) -> Result<Arc<rust_ir::Program>, String> {
+            type LoweredProgram;
+
+            // FIXME: only volatile because the Error type does not implement Eq
+            storage volatile;
+        }
+    }
+}
+
+fn lowered_program(
+    db: &impl LoweringDatabase,
+    solver_choice: SolverChoice,
+) -> Result<Arc<rust_ir::Program>, String> {
+    let x: crate::errors::Result<_> = try {
+        let text = db.program_text();
+        Arc::new(chalk_parse::parse_program(&text)?.lower(solver_choice)?)
+    };
+
+    x.map_err(|err| err.to_string())
+}

src/query.rs

@@ -3,7 +3,6 @@
 use crate::test_util::*;
 use chalk_ir::tls;
 use chalk_solve::solve::SolverChoice;
-use std::sync::Arc;
 
 #[test]
 fn lower_success() {
@@ -158,8 +157,7 @@ fn assoc_tys() {
 
 #[test]
 fn goal_quantifiers() {
-    let program =
-        Arc::new(parse_and_lower_program("trait Foo<A, B> { }", SolverChoice::default()).unwrap());
+    let program = parse_and_lower_program("trait Foo<A, B> { }", SolverChoice::default()).unwrap();
     let goal =
         parse_and_lower_goal(&program, "forall<X> {exists<Y> {forall<Z> {Z: Foo<Y, X>}}}").unwrap();
     tls::set_current_program(&program, || {
@@ -172,9 +170,8 @@ fn goal_quantifiers() {
 
 #[test]
 fn atc_accounting() {
-    let program = Arc::new(
-        parse_and_lower_program(
-            "
+    let program = parse_and_lower_program(
+        "
             struct Vec<T> { }
 
             trait Iterable {
@@ -187,10 +184,9 @@ fn atc_accounting() {
 
             struct Iter<'a, T> { }
             ",
-            SolverChoice::default(),
-        )
-        .unwrap(),
-    );
+        SolverChoice::default(),
+    )
+    .unwrap();
     tls::set_current_program(&program, || {
         let impl_text = format!("{:#?}", &program.impl_data.values().next().unwrap());
         println!("{}", impl_text);

src/rust_ir/lowering/test.rs

@@ -90,7 +90,7 @@ fn solve_goal(program_text: &str, goals: Vec<(&str, SolverChoice, &str)>) {
     for (goal_text, solver_choice, expected) in goals {
         let (program, env) = program_env_cache.entry(solver_choice).or_insert_with(|| {
             let program_text = &program_text[1..program_text.len() - 1]; // exclude `{}`
-            let program = Arc::new(parse_and_lower_program(program_text, solver_choice).unwrap());
+            let program = parse_and_lower_program(program_text, solver_choice).unwrap();
             let env = Arc::new(program.environment());
             (program, env)
         });

src/test.rs

@@ -17,7 +17,7 @@ fn run_bench(
     bencher: &mut Bencher,
     expected: &str,
 ) {
-    let program = Arc::new(parse_and_lower_program(program_text, solver_choice).unwrap());
+    let program = parse_and_lower_program(program_text, solver_choice).unwrap();
     let env = Arc::new(program.environment());
     chalk_ir::tls::set_current_program(&program, || {
         let goal = parse_and_lower_goal(&program, goal_text).unwrap();

src/test/bench.rs

@@ -24,13 +24,11 @@ fn solve_goal(program_text: &str, goals: Vec<(usize, usize, &str, &str)>) {
     println!("program {}", program_text);
     assert!(program_text.starts_with("{"));
     assert!(program_text.ends_with("}"));
-    let program = &Arc::new(
-        parse_and_lower_program(
-            &program_text[1..program_text.len() - 1],
-            SolverChoice::default(),
-        )
-        .unwrap(),
-    );
+    let program = &parse_and_lower_program(
+        &program_text[1..program_text.len() - 1],
+        SolverChoice::default(),
+    )
+    .unwrap();
     let env = &Arc::new(program.environment());
     chalk_ir::tls::set_current_program(&program, || {
         for (max_size, num_answers, goal_text, expected) in goals {
@@ -52,13 +50,11 @@ fn solve_goal_fixed_num_answers(program_text: &str, goals: Vec<(usize, usize, &s
     println!("program {}", program_text);
     assert!(program_text.starts_with("{"));
     assert!(program_text.ends_with("}"));
-    let program = &Arc::new(
-        parse_and_lower_program(
-            &program_text[1..program_text.len() - 1],
-            SolverChoice::default(),
-        )
-        .unwrap(),
-    );
+    let program = &parse_and_lower_program(
+        &program_text[1..program_text.len() - 1],
+        SolverChoice::default(),
+    )
+    .unwrap();
     let env = &Arc::new(program.environment());
     chalk_ir::tls::set_current_program(&program, || {
         for (max_size, num_answers, goal_text, expected) in goals {

src/test/slg.rs

@@ -1,17 +1,31 @@
 #![cfg(test)]
 
+use crate::db::ChalkDatabase;
 use crate::errors::Result;
-use crate::rust_ir::lowering::{LowerGoal, LowerProgram};
+use crate::query::LoweringDatabase;
+use crate::query::ProgramText;
+use crate::rust_ir::lowering::LowerGoal;
 use crate::rust_ir::Program;
 use chalk_ir::Goal;
 use chalk_parse;
 use chalk_solve::solve::SolverChoice;
 use diff;
 use itertools::Itertools;
+use salsa::Database;
 use std::fmt::Write;
+use std::prelude::v1::Result as StdResult;
+use std::sync::Arc;
 
-pub fn parse_and_lower_program(text: &str, solver_choice: SolverChoice) -> Result<Program> {
-    chalk_parse::parse_program(text)?.lower(solver_choice)
+pub fn parse_and_lower_program(
+    text: &str,
+    solver_choice: SolverChoice,
+) -> StdResult<Arc<Program>, String> {
+    let mut db = ChalkDatabase::default();
+
+    db.query_mut(ProgramText)
+        .set((), Arc::new(text.to_string()));
+
+    db.lowered_program(solver_choice)
 }
 
 pub fn parse_and_lower_goal(program: &Program, text: &str) -> Result<Box<Goal>> {