rename ProgramClauseSet to ChalkSolverDatabase

Author: nikomatsakis

chalk-solve/src/lib.rs

@@ -7,7 +7,7 @@ pub mod ext;
 mod infer;
 mod solve;
 
-pub use solve::ProgramClauseSet;
+pub use solve::ChalkSolveDatabase;
 pub use solve::Solution;
 pub use solve::Solver;
 pub use solve::SolverChoice;

chalk-solve/src/solve.rs

@@ -124,7 +124,7 @@ impl Solver {
     ///   although `solution` may reflect ambiguity and unknowns.
     pub fn solve(
         &mut self,
-        program: &dyn ProgramClauseSet,
+        program: &dyn ChalkSolveDatabase,
         goal: &UCanonical<InEnvironment<Goal>>,
     ) -> Option<Solution> {
         let ops = self.forest.context().ops(program);
@@ -168,7 +168,7 @@ impl TestSolver {
     /// its debug representation).
     pub fn force_answers(
         &mut self,
-        program: &dyn ProgramClauseSet,
+        program: &dyn ChalkSolveDatabase,
         goal: &UCanonical<InEnvironment<Goal>>,
         num_answers: usize,
     ) -> Box<std::fmt::Debug> {
@@ -180,7 +180,7 @@ impl TestSolver {
     /// testing.
     pub fn num_cached_answers_for_goal(
         &mut self,
-        program: &dyn ProgramClauseSet,
+        program: &dyn ChalkSolveDatabase,
         goal: &UCanonical<InEnvironment<Goal>>,
     ) -> usize {
         let ops = self.forest.context().ops(program);
@@ -190,10 +190,10 @@ impl TestSolver {
 
 /// The trait for defining the program clauses that are in scope when
 /// solving a goal.
-pub trait ProgramClauseSet: Debug + IsCoinductive {
+pub trait ChalkSolveDatabase: Debug + IsCoinductive {
     /// Convert to a dyn trait value representing `self`. This is a
     /// workaround for the lack of proper upcasting in Rust.
-    fn as_dyn(&self) -> &dyn ProgramClauseSet;
+    fn as_dyn(&self) -> &dyn ChalkSolveDatabase;
 
     /// Returns a set of program clauses that could possibly match
     /// `goal`. This can be any superset of the correct set, but the

chalk-solve/src/solve/slg.rs

@@ -2,7 +2,7 @@ use crate::infer::ucanonicalize::{UCanonicalized, UniverseMap};
 use crate::infer::unify::UnificationResult;
 use crate::infer::InferenceTable;
 use crate::solve::truncate::{self, Truncated};
-use crate::solve::ProgramClauseSet;
+use crate::solve::ChalkSolveDatabase;
 use crate::solve::Solution;
 use chalk_engine::fallible::Fallible;
 use chalk_ir::cast::{Cast, Caster};
@@ -29,7 +29,7 @@ impl SlgContext {
         SlgContext { max_size }
     }
 
-    pub(crate) fn ops<'p>(&self, program: &'p dyn ProgramClauseSet) -> SlgContextOps<'p> {
+    pub(crate) fn ops<'p>(&self, program: &'p dyn ChalkSolveDatabase) -> SlgContextOps<'p> {
         SlgContextOps {
             program,
             max_size: self.max_size,
@@ -39,12 +39,12 @@ impl SlgContext {
 
 #[derive(Clone, Debug)]
 pub(crate) struct SlgContextOps<'me> {
-    program: &'me dyn ProgramClauseSet,
+    program: &'me dyn ChalkSolveDatabase,
     max_size: usize,
 }
 
 pub(super) struct TruncatingInferenceTable<'me> {
-    program: &'me dyn ProgramClauseSet,
+    program: &'me dyn ChalkSolveDatabase,
     max_size: usize,
     infer: InferenceTable,
 }
@@ -148,7 +148,7 @@ impl<'me> context::ContextOps<SlgContext> for SlgContextOps<'me> {
 }
 
 impl<'me> TruncatingInferenceTable<'me> {
-    fn new(program: &'me dyn ProgramClauseSet, max_size: usize, infer: InferenceTable) -> Self {
+    fn new(program: &'me dyn ChalkSolveDatabase, max_size: usize, infer: InferenceTable) -> Self {
         Self {
             program,
             max_size,

src/db.rs

@@ -27,7 +27,7 @@ use chalk_rust_ir::AssociatedTyDatum;
 use chalk_rust_ir::ImplDatum;
 use chalk_rust_ir::StructDatum;
 use chalk_rust_ir::TraitDatum;
-use chalk_solve::ProgramClauseSet;
+use chalk_solve::ChalkSolveDatabase;
 use chalk_solve::Solution;
 use chalk_solve::SolverChoice;
 use salsa::Database;
@@ -64,8 +64,8 @@ impl ChalkDatabase {
     }
 }
 
-impl ProgramClauseSet for ChalkDatabase {
-    fn as_dyn(&self) -> &dyn ProgramClauseSet {
+impl ChalkSolveDatabase for ChalkDatabase {
+    fn as_dyn(&self) -> &dyn ChalkSolveDatabase {
         self
     }
 

src/query.rs

@@ -13,15 +13,15 @@ use chalk_rules::coherence::{CoherenceSolver, SpecializationPriorities};
 use chalk_rules::wf;
 use chalk_rules::ChalkRulesDatabase;
 use chalk_rules::RustIrSource;
-use chalk_solve::ProgramClauseSet;
+use chalk_solve::ChalkSolveDatabase;
 use chalk_solve::Solver;
 use chalk_solve::SolverChoice;
 use std::collections::BTreeMap;
 use std::sync::Arc;
 use std::sync::Mutex;
 
 #[salsa::query_group(Lowering)]
-pub trait LoweringDatabase: ChalkRulesDatabase + ProgramClauseSet + RustIrSource {
+pub trait LoweringDatabase: ChalkRulesDatabase + ChalkSolveDatabase + RustIrSource {
     #[salsa::input]
     fn program_text(&self) -> Arc<String>;