use super::combine;
use super::fulfill::Fulfill;
use crate::fixed_point::Minimums;
use crate::UCanonicalGoal;
use chalk_ir::could_match::CouldMatch;
use chalk_ir::fold::TypeFoldable;
use chalk_ir::interner::{HasInterner, Interner};
use chalk_ir::{
Canonical, ClausePriority, DomainGoal, Fallible, Floundered, Goal, GoalData, InEnvironment,
NoSolution, ProgramClause, ProgramClauseData, Substitution, UCanonical,
};
use chalk_solve::clauses::program_clauses_that_could_match;
use chalk_solve::debug_span;
use chalk_solve::infer::InferenceTable;
use chalk_solve::{Guidance, RustIrDatabase, Solution};
use tracing::{debug, instrument};
pub(super) trait SolveDatabase<I: Interner>: Sized {
fn solve_goal(
&mut self,
goal: UCanonical<InEnvironment<Goal<I>>>,
minimums: &mut Minimums,
should_continue: impl std::ops::Fn() -> bool + Clone,
) -> Fallible<Solution<I>>;
fn max_size(&self) -> usize;
fn interner(&self) -> I;
fn db(&self) -> &dyn RustIrDatabase<I>;
}
pub(super) trait SolveIteration<I: Interner>: SolveDatabase<I> {
#[instrument(level = "debug", skip(self, should_continue))]
fn solve_iteration(
&mut self,
canonical_goal: &UCanonicalGoal<I>,
minimums: &mut Minimums,
should_continue: impl std::ops::Fn() -> bool + Clone,
) -> Fallible<Solution<I>> {
if !should_continue() {
return Ok(Solution::Ambig(Guidance::Unknown));
}
let UCanonical {
universes,
canonical:
Canonical {
binders,
value: InEnvironment { environment, goal },
},
} = canonical_goal.clone();
match goal.data(self.interner()) {
GoalData::DomainGoal(domain_goal) => {
let canonical_goal = UCanonical {
universes,
canonical: Canonical {
binders,
value: InEnvironment {
environment,
goal: domain_goal.clone(),
},
},
};
let prog_solution = {
debug_span!("prog_clauses");
self.solve_from_clauses(&canonical_goal, minimums, should_continue)
};
debug!(?prog_solution);
prog_solution
}
_ => {
let canonical_goal = UCanonical {
universes,
canonical: Canonical {
binders,
value: InEnvironment { environment, goal },
},
};
self.solve_via_simplification(&canonical_goal, minimums, should_continue)
}
}
}
}
impl<S, I> SolveIteration<I> for S
where
S: SolveDatabase<I>,
I: Interner,
{
}
trait SolveIterationHelpers<I: Interner>: SolveDatabase<I> {
#[instrument(level = "debug", skip(self, minimums, should_continue))]
fn solve_via_simplification(
&mut self,
canonical_goal: &UCanonicalGoal<I>,
minimums: &mut Minimums,
should_continue: impl std::ops::Fn() -> bool + Clone,
) -> Fallible<Solution<I>> {
let (infer, subst, goal) = self.new_inference_table(canonical_goal);
match Fulfill::new_with_simplification(self, infer, subst, goal) {
Ok(fulfill) => fulfill.solve(minimums, should_continue),
Err(e) => Err(e),
}
}
fn solve_from_clauses(
&mut self,
canonical_goal: &UCanonical<InEnvironment<DomainGoal<I>>>,
minimums: &mut Minimums,
should_continue: impl std::ops::Fn() -> bool + Clone,
) -> Fallible<Solution<I>> {
let mut clauses = vec![];
let db = self.db();
let could_match = |c: &ProgramClause<I>| {
c.could_match(
db.interner(),
db.unification_database(),
&canonical_goal.canonical.value.goal,
)
};
clauses.extend(db.custom_clauses().into_iter().filter(could_match));
match program_clauses_that_could_match(db, canonical_goal) {
Ok(goal_clauses) => clauses.extend(goal_clauses.into_iter().filter(could_match)),
Err(Floundered) => {
return Ok(Solution::Ambig(Guidance::Unknown));
}
}
let (infer, subst, goal) = self.new_inference_table(canonical_goal);
clauses.extend(
db.program_clauses_for_env(&goal.environment)
.iter(db.interner())
.cloned()
.filter(could_match),
);
let mut cur_solution = None;
for program_clause in clauses {
debug_span!("solve_from_clauses", clause = ?program_clause);
let ProgramClauseData(implication) = program_clause.data(self.interner());
let infer = infer.clone();
let subst = subst.clone();
let goal = goal.clone();
let res = match Fulfill::new_with_clause(self, infer, subst, goal, implication) {
Ok(fulfill) => (
fulfill.solve(minimums, should_continue.clone()),
implication.skip_binders().priority,
),
Err(e) => (Err(e), ClausePriority::High),
};
if let (Ok(solution), priority) = res {
debug!(?solution, ?priority, "Ok");
cur_solution = Some(match cur_solution {
None => (solution, priority),
Some((cur, cur_priority)) => combine::with_priorities(
self.interner(),
&canonical_goal.canonical.value.goal,
cur,
cur_priority,
solution,
priority,
),
});
} else {
debug!("Error");
}
if let Some((cur_solution, _)) = &cur_solution {
if cur_solution.is_trivial_and_always_true(self.interner()) {
break;
}
}
}
if let Some((s, _)) = cur_solution {
debug!("solve_from_clauses: result = {:?}", s);
Ok(s)
} else {
debug!("solve_from_clauses: error");
Err(NoSolution)
}
}
fn new_inference_table<T: TypeFoldable<I> + HasInterner<Interner = I> + Clone>(
&self,
ucanonical_goal: &UCanonical<InEnvironment<T>>,
) -> (InferenceTable<I>, Substitution<I>, InEnvironment<T>) {
let (infer, subst, canonical_goal) = InferenceTable::from_canonical(
self.interner(),
ucanonical_goal.universes,
ucanonical_goal.canonical.clone(),
);
(infer, subst, canonical_goal)
}
}
impl<S, I> SolveIterationHelpers<I> for S
where
S: SolveDatabase<I>,
I: Interner,
{
}