Skip to content

Commit

Permalink
Turn a few generics into dynamic dispatch.
Browse files Browse the repository at this point in the history
  • Loading branch information
crlf0710 committed Aug 5, 2020
1 parent a030931 commit 6024630
Show file tree
Hide file tree
Showing 14 changed files with 89 additions and 149 deletions.
4 changes: 2 additions & 2 deletions chalk-engine/src/solve.rs
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ impl<I: Interner> Solver<I> for SLGSolver<I> {
&mut self,
program: &dyn RustIrDatabase<I>,
goal: &UCanonical<InEnvironment<Goal<I>>>,
should_continue: impl std::ops::Fn() -> bool,
should_continue: &dyn std::ops::Fn() -> bool,
) -> Option<Solution<I>> {
let ops = SlgContextOps::new(program, self.max_size, self.expected_answers);
ops.make_solution(goal, self.forest.iter_answers(&ops, goal), should_continue)
Expand All @@ -54,7 +54,7 @@ impl<I: Interner> Solver<I> for SLGSolver<I> {
&mut self,
program: &dyn RustIrDatabase<I>,
goal: &UCanonical<InEnvironment<Goal<I>>>,
mut f: impl FnMut(SubstitutionResult<Canonical<ConstrainedSubst<I>>>, bool) -> bool,
f: &mut dyn FnMut(SubstitutionResult<Canonical<ConstrainedSubst<I>>>, bool) -> bool,
) -> bool {
let ops = SlgContextOps::new(program, self.max_size, self.expected_answers);
let mut answers = self.forest.iter_answers(&ops, goal);
Expand Down
4 changes: 2 additions & 2 deletions chalk-integration/src/db.rs
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ use chalk_solve::rust_ir::{
AdtDatum, AdtRepr, AssociatedTyDatum, AssociatedTyValue, AssociatedTyValueId, ClosureKind,
FnDefDatum, FnDefInputsAndOutputDatum, ImplDatum, OpaqueTyDatum, TraitDatum, WellKnownTrait,
};
use chalk_solve::{RustIrDatabase, Solution, Solver, SubstitutionResult};
use chalk_solve::{RustIrDatabase, Solution, SubstitutionResult};
use salsa::Database;
use std::fmt;
use std::sync::Arc;
Expand Down Expand Up @@ -62,7 +62,7 @@ impl ChalkDatabase {
pub fn solve_multiple(
&self,
goal: &UCanonical<InEnvironment<Goal<ChalkIr>>>,
f: impl FnMut(SubstitutionResult<Canonical<ConstrainedSubst<ChalkIr>>>, bool) -> bool,
f: &mut dyn FnMut(SubstitutionResult<Canonical<ConstrainedSubst<ChalkIr>>>, bool) -> bool,
) -> bool {
let solver = self.solver();
let solution = solver.lock().unwrap().solve_multiple(self, goal, f);
Expand Down
67 changes: 11 additions & 56 deletions chalk-integration/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -13,9 +13,9 @@ pub mod tls;

use chalk_engine::solve::SLGSolver;
use chalk_ir::interner::HasInterner;
use chalk_ir::{Binders, Canonical, ConstrainedSubst, Goal, InEnvironment, UCanonical};
use chalk_ir::Binders;
use chalk_recursive::RecursiveSolver;
use chalk_solve::{RustIrDatabase, Solution, Solver, SubstitutionResult};
use chalk_solve::Solver;
use interner::ChalkIr;

pub use interner::{Identifier, RawId};
Expand Down Expand Up @@ -78,68 +78,23 @@ impl SolverChoice {
caching_enabled: true,
}
}
}

impl Default for SolverChoice {
fn default() -> Self {
SolverChoice::slg(10, None)
}
}

#[derive(Debug)]
pub enum SolverImpl {
Slg(SLGSolver<ChalkIr>),
Recursive(RecursiveSolver<ChalkIr>),
}

impl Solver<ChalkIr> for SolverImpl {
fn solve(
&mut self,
program: &dyn RustIrDatabase<ChalkIr>,
goal: &UCanonical<InEnvironment<Goal<ChalkIr>>>,
) -> Option<Solution<ChalkIr>> {
match self {
Self::Slg(solve) => solve.solve(program, goal),
Self::Recursive(solve) => solve.solve(program, goal),
}
}

fn solve_limited(
&mut self,
program: &dyn RustIrDatabase<ChalkIr>,
goal: &UCanonical<InEnvironment<Goal<ChalkIr>>>,
should_continue: impl std::ops::Fn() -> bool,
) -> Option<Solution<ChalkIr>> {
match self {
Self::Slg(solve) => solve.solve_limited(program, goal, should_continue),
Self::Recursive(solve) => solve.solve_limited(program, goal, should_continue),
}
}

fn solve_multiple(
&mut self,
program: &dyn RustIrDatabase<ChalkIr>,
goal: &UCanonical<InEnvironment<Goal<ChalkIr>>>,
f: impl FnMut(SubstitutionResult<Canonical<ConstrainedSubst<ChalkIr>>>, bool) -> bool,
) -> bool {
match self {
Self::Slg(solve) => solve.solve_multiple(program, goal, f),
Self::Recursive(solve) => solve.solve_multiple(program, goal, f),
}
}
}

impl Into<SolverImpl> for SolverChoice {
fn into(self) -> SolverImpl {
pub fn into_solver(self) -> Box<dyn Solver<ChalkIr>> {
match self {
SolverChoice::SLG {
max_size,
expected_answers,
} => SolverImpl::Slg(SLGSolver::new(max_size, expected_answers)),
} => Box::new(SLGSolver::new(max_size, expected_answers)),
SolverChoice::Recursive {
overflow_depth,
caching_enabled,
} => SolverImpl::Recursive(RecursiveSolver::new(overflow_depth, caching_enabled)),
} => Box::new(RecursiveSolver::new(overflow_depth, caching_enabled)),
}
}
}

impl Default for SolverChoice {
fn default() -> Self {
SolverChoice::slg(10, None)
}
}
26 changes: 12 additions & 14 deletions chalk-integration/src/query.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,14 +8,14 @@ use crate::program::Program;
use crate::program_environment::ProgramEnvironment;
use crate::tls;
use crate::SolverChoice;
use crate::SolverImpl;
use chalk_ir::TraitId;
use chalk_solve::clauses::builder::ClauseBuilder;
use chalk_solve::clauses::program_clauses::ToProgramClauses;
use chalk_solve::coherence::orphan;
use chalk_solve::coherence::{CoherenceSolver, SpecializationPriorities};
use chalk_solve::wf;
use chalk_solve::RustIrDatabase;
use chalk_solve::Solver;
use salsa::Database;
use std::clone::Clone;
use std::cmp::{Eq, PartialEq};
Expand Down Expand Up @@ -57,7 +57,7 @@ pub trait LoweringDatabase:
/// volatile, thus ensuring that the solver is recreated in every
/// revision (i.e., each time source program changes).
// HACK: salsa requires that queries return types that implement `Eq`
fn solver(&self) -> ArcEq<Mutex<SolverImpl>>;
fn solver(&self) -> ArcEq<Mutex<Box<dyn Solver<ChalkIr>>>>;
}

// Needed to go from dyn LoweringDatabase -> dyn RustIrDatabase
Expand Down Expand Up @@ -132,12 +132,9 @@ fn orphan_check(db: &dyn LoweringDatabase) -> Result<(), ChalkError> {

tls::set_current_program(&program, || -> Result<(), ChalkError> {
let local_impls = program.local_impl_ids();
let mut solver = db.solver_choice().into_solver();
for impl_id in local_impls {
orphan::perform_orphan_check::<ChalkIr, SolverImpl, SolverChoice>(
db.upcast(),
db.solver_choice(),
impl_id,
)?;
orphan::perform_orphan_check::<ChalkIr>(db.upcast(), &mut *solver, impl_id)?;
}
Ok(())
})
Expand All @@ -147,14 +144,14 @@ fn coherence(
db: &dyn LoweringDatabase,
) -> Result<BTreeMap<TraitId<ChalkIr>, Arc<SpecializationPriorities<ChalkIr>>>, ChalkError> {
let program = db.program_ir()?;

let mut solver = db.solver_choice().into_solver();
let priorities_map = tls::set_current_program(&program, || -> Result<_, ChalkError> {
let priorities_map: Result<BTreeMap<_, _>, ChalkError> = program
.trait_data
.keys()
.map(|&trait_id| {
let solver: CoherenceSolver<ChalkIr, SolverImpl, SolverChoice> =
CoherenceSolver::new(db.upcast(), db.solver_choice(), trait_id);
let mut solver: CoherenceSolver<ChalkIr> =
CoherenceSolver::new(db.upcast(), &mut *solver, trait_id);
let priorities = solver.specialization_priorities()?;
Ok((trait_id, priorities))
})
Expand All @@ -171,9 +168,10 @@ fn checked_program(db: &dyn LoweringDatabase) -> Result<Arc<Program>, ChalkError

db.coherence()?;

let mut solver = db.solver_choice().into_solver();

let () = tls::set_current_program(&program, || -> Result<(), ChalkError> {
let solver: wf::WfSolver<ChalkIr, SolverImpl, SolverChoice> =
wf::WfSolver::new(db.upcast(), db.solver_choice());
let mut solver: wf::WfSolver<ChalkIr> = wf::WfSolver::new(db.upcast(), &mut *solver);
for &id in program.adt_data.keys() {
solver.verify_adt_decl(id)?;
}
Expand Down Expand Up @@ -242,8 +240,8 @@ fn environment(db: &dyn LoweringDatabase) -> Result<Arc<ProgramEnvironment>, Cha
Ok(Arc::new(ProgramEnvironment::new(program_clauses)))
}

fn solver(db: &dyn LoweringDatabase) -> ArcEq<Mutex<SolverImpl>> {
fn solver(db: &dyn LoweringDatabase) -> ArcEq<Mutex<Box<dyn Solver<ChalkIr>>>> {
db.salsa_runtime().report_untracked_read();
let choice = db.solver_choice();
ArcEq::new(Mutex::new(choice.into()))
ArcEq::new(Mutex::new(choice.into_solver()))
}
7 changes: 5 additions & 2 deletions chalk-recursive/src/recursive.rs
Original file line number Diff line number Diff line change
Expand Up @@ -317,7 +317,7 @@ impl<I: Interner> chalk_solve::Solver<I> for RecursiveSolver<I> {
&mut self,
program: &dyn RustIrDatabase<I>,
goal: &UCanonical<InEnvironment<Goal<I>>>,
_should_continue: impl std::ops::Fn() -> bool,
_should_continue: &dyn std::ops::Fn() -> bool,
) -> Option<chalk_solve::Solution<I>> {
// TODO support should_continue in recursive solver
self.ctx
Expand All @@ -338,7 +338,10 @@ impl<I: Interner> chalk_solve::Solver<I> for RecursiveSolver<I> {
&mut self,
_program: &dyn RustIrDatabase<I>,
_goal: &UCanonical<InEnvironment<Goal<I>>>,
_f: impl FnMut(chalk_solve::SubstitutionResult<Canonical<ConstrainedSubst<I>>>, bool) -> bool,
_f: &mut dyn FnMut(
chalk_solve::SubstitutionResult<Canonical<ConstrainedSubst<I>>>,
bool,
) -> bool,
) -> bool {
unimplemented!("Recursive solver doesn't support multiple answers")
}
Expand Down
22 changes: 11 additions & 11 deletions chalk-solve/src/coherence.rs
Original file line number Diff line number Diff line change
Expand Up @@ -11,11 +11,10 @@ use std::sync::Arc;
pub mod orphan;
mod solve;

pub struct CoherenceSolver<'db, I: Interner, S, SC: Into<S> + Copy> {
pub struct CoherenceSolver<'db, 'solver, I: Interner> {
db: &'db dyn RustIrDatabase<I>,
solver_choice: SC,
solver: &'solver mut dyn Solver<I>,
trait_id: TraitId<I>,
_solver: std::marker::PhantomData<S>,
}

#[derive(Debug)]
Expand Down Expand Up @@ -72,24 +71,25 @@ impl<I: Interner> SpecializationPriorities<I> {
#[derive(Copy, Clone, Default, PartialOrd, Ord, PartialEq, Eq, Debug)]
pub struct SpecializationPriority(usize);

impl<'db, I, S, SC> CoherenceSolver<'db, I, S, SC>
impl<'db, 'solver, I> CoherenceSolver<'db, 'solver, I>
where
I: Interner,
S: Solver<I>,
SC: Into<S> + Copy,
{
/// Constructs a new `CoherenceSolver`.
pub fn new(db: &'db dyn RustIrDatabase<I>, solver_choice: SC, trait_id: TraitId<I>) -> Self {
pub fn new(
db: &'db dyn RustIrDatabase<I>,
solver: &'solver mut dyn Solver<I>,
trait_id: TraitId<I>,
) -> Self {
Self {
db,
solver_choice,
solver,
trait_id,
_solver: std::marker::PhantomData,
}
}

pub fn specialization_priorities(
&self,
&mut self,
) -> Result<Arc<SpecializationPriorities<I>>, CoherenceError<I>> {
let mut result = SpecializationPriorities::<I>::new();

Expand All @@ -105,7 +105,7 @@ where
}

// Build the forest of specialization relationships.
fn build_specialization_forest(&self) -> Result<Graph<ImplId<I>, ()>, CoherenceError<I>> {
fn build_specialization_forest(&mut self) -> Result<Graph<ImplId<I>, ()>, CoherenceError<I>> {
// The forest is returned as a graph but built as a GraphMap; this is
// so that we never add multiple nodes with the same ItemId.
let mut forest = DiGraphMap::new();
Expand Down
8 changes: 4 additions & 4 deletions chalk-solve/src/coherence/orphan.rs
Original file line number Diff line number Diff line change
Expand Up @@ -14,10 +14,10 @@ use tracing::{debug, instrument};
// forall<T> { LocalImplAllowed(MyType<T>: Trait) }
//
// This must be provable in order to pass the orphan check.
#[instrument(level = "debug", skip(db, solver_choice))]
pub fn perform_orphan_check<I: Interner, S: Solver<I>, SC: Into<S>>(
#[instrument(level = "debug", skip(db, solver))]
pub fn perform_orphan_check<I: Interner>(
db: &dyn RustIrDatabase<I>,
solver_choice: SC,
solver: &mut dyn Solver<I>,
impl_id: ImplId<I>,
) -> Result<(), CoherenceError<I>> {
let impl_datum = db.impl_datum(impl_id);
Expand All @@ -32,7 +32,7 @@ pub fn perform_orphan_check<I: Interner, S: Solver<I>, SC: Into<S>>(
.cast(db.interner());

let canonical_goal = &impl_allowed.into_closed_goal(db.interner());
let is_allowed = solver_choice.into().solve(db, canonical_goal).is_some();
let is_allowed = solver.solve(db, canonical_goal).is_some();
debug!("overlaps = {:?}", is_allowed);

if !is_allowed {
Expand Down
13 changes: 6 additions & 7 deletions chalk-solve/src/coherence/solve.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,6 @@ use crate::coherence::{CoherenceError, CoherenceSolver};
use crate::debug_span;
use crate::ext::*;
use crate::rust_ir::*;
use crate::solve::Solver;
use crate::{goal_builder::GoalBuilder, Solution};
use chalk_ir::cast::*;
use chalk_ir::fold::shift::Shift;
Expand All @@ -11,9 +10,9 @@ use chalk_ir::*;
use itertools::Itertools;
use tracing::{debug, instrument};

impl<I: Interner, S: Solver<I>, SC: Into<S> + Copy> CoherenceSolver<'_, I, S, SC> {
impl<I: Interner> CoherenceSolver<'_, '_, I> {
pub(super) fn visit_specializations_of_trait(
&self,
&mut self,
mut record_specialization: impl FnMut(ImplId<I>, ImplId<I>),
) -> Result<(), CoherenceError<I>> {
// Ignore impls for marker traits as they are allowed to overlap.
Expand Down Expand Up @@ -84,7 +83,7 @@ impl<I: Interner, S: Solver<I>, SC: Into<S> + Copy> CoherenceSolver<'_, I, S, SC
// not { compatible { exists<T> { exists<U> { Vec<T> = Vec<U>, T: Bar, U: Baz } } } }
//
#[instrument(level = "debug", skip(self))]
fn disjoint(&self, lhs: &ImplDatum<I>, rhs: &ImplDatum<I>) -> bool {
fn disjoint(&mut self, lhs: &ImplDatum<I>, rhs: &ImplDatum<I>) -> bool {
let interner = self.db.interner();

let (lhs_binders, lhs_bound) = lhs.binders.as_ref().into();
Expand Down Expand Up @@ -131,7 +130,7 @@ impl<I: Interner, S: Solver<I>, SC: Into<S> + Copy> CoherenceSolver<'_, I, S, SC
.negate(interner);

let canonical_goal = &goal.into_closed_goal(interner);
let solution = self.solver_choice.into().solve(self.db, canonical_goal);
let solution = self.solver.solve(self.db, canonical_goal);
let result = match solution {
// Goal was proven with a unique solution, so no impl was found that causes these two
// to overlap
Expand Down Expand Up @@ -193,7 +192,7 @@ impl<I: Interner, S: Solver<I>, SC: Into<S> + Copy> CoherenceSolver<'_, I, S, SC
// }
// ```
#[instrument(level = "debug", skip(self))]
fn specializes(&self, less_special_id: ImplId<I>, more_special_id: ImplId<I>) -> bool {
fn specializes(&mut self, less_special_id: ImplId<I>, more_special_id: ImplId<I>) -> bool {
let more_special = &self.db.impl_datum(more_special_id);
let less_special = &self.db.impl_datum(less_special_id);
debug_span!("specializes", ?less_special, ?more_special);
Expand Down Expand Up @@ -250,7 +249,7 @@ impl<I: Interner, S: Solver<I>, SC: Into<S> + Copy> CoherenceSolver<'_, I, S, SC
);

let canonical_goal = &goal.into_closed_goal(interner);
let result = match self.solver_choice.into().solve(self.db, canonical_goal) {
let result = match self.solver.solve(self.db, canonical_goal) {
Some(sol) => sol.is_unique(),
None => false,
};
Expand Down
4 changes: 2 additions & 2 deletions chalk-solve/src/solve.rs
Original file line number Diff line number Diff line change
Expand Up @@ -172,7 +172,7 @@ where
&mut self,
program: &dyn RustIrDatabase<I>,
goal: &UCanonical<InEnvironment<Goal<I>>>,
should_continue: impl std::ops::Fn() -> bool,
should_continue: &dyn std::ops::Fn() -> bool,
) -> Option<Solution<I>>;

/// Attempts to solve the given goal, which must be in canonical
Expand Down Expand Up @@ -201,6 +201,6 @@ where
&mut self,
program: &dyn RustIrDatabase<I>,
goal: &UCanonical<InEnvironment<Goal<I>>>,
f: impl FnMut(SubstitutionResult<Canonical<ConstrainedSubst<I>>>, bool) -> bool,
f: &mut dyn FnMut(SubstitutionResult<Canonical<ConstrainedSubst<I>>>, bool) -> bool,
) -> bool;
}
Loading

0 comments on commit 6024630

Please sign in to comment.