2019-05-01 10:06:11 -05:00
|
|
|
//! Trait solving using Chalk.
|
2021-04-09 07:39:07 -05:00
|
|
|
|
2020-11-20 11:00:34 -06:00
|
|
|
use std::env::var;
|
2019-03-31 13:02:16 -05:00
|
|
|
|
2021-05-16 08:50:28 -05:00
|
|
|
use chalk_ir::GoalData;
|
2020-07-13 15:03:26 -05:00
|
|
|
use chalk_solve::{logging_db::LoggingRustIrDatabase, Solver};
|
2021-04-09 07:39:07 -05:00
|
|
|
|
|
|
|
use base_db::CrateId;
|
2020-07-12 08:26:02 -05:00
|
|
|
use hir_def::{lang_item::LangItemTarget, TraitId};
|
2020-10-23 08:25:22 -05:00
|
|
|
use stdx::panic_context;
|
2019-03-31 13:02:16 -05:00
|
|
|
|
2021-03-18 20:07:15 -05:00
|
|
|
use crate::{
|
2021-05-16 08:50:28 -05:00
|
|
|
db::HirDatabase, AliasEq, AliasTy, Canonical, DomainGoal, Goal, Guidance, InEnvironment,
|
2021-04-09 07:15:26 -05:00
|
|
|
Interner, Solution, TraitRefExt, Ty, TyKind, WhereClause,
|
2021-03-13 07:44:51 -06:00
|
|
|
};
|
2019-05-01 10:06:11 -05:00
|
|
|
|
2020-01-17 15:12:15 -06:00
|
|
|
/// This controls how much 'time' we give the Chalk solver before giving up.
|
|
|
|
const CHALK_SOLVER_FUEL: i32 = 100;
|
2019-05-07 10:35:45 -05:00
|
|
|
|
2019-04-20 05:34:36 -05:00
|
|
|
#[derive(Debug, Copy, Clone)]
|
2021-04-09 07:11:37 -05:00
|
|
|
pub(crate) struct ChalkContext<'a> {
|
|
|
|
pub(crate) db: &'a dyn HirDatabase,
|
|
|
|
pub(crate) krate: CrateId,
|
2019-04-20 05:34:36 -05:00
|
|
|
}
|
2019-03-31 13:02:16 -05:00
|
|
|
|
2020-07-11 08:22:46 -05:00
|
|
|
fn create_chalk_solver() -> chalk_recursive::RecursiveSolver<Interner> {
|
2020-11-20 11:00:34 -06:00
|
|
|
let overflow_depth =
|
|
|
|
var("CHALK_OVERFLOW_DEPTH").ok().and_then(|s| s.parse().ok()).unwrap_or(100);
|
2020-07-11 08:22:46 -05:00
|
|
|
let caching_enabled = true;
|
2020-11-20 11:00:34 -06:00
|
|
|
let max_size = var("CHALK_SOLVER_MAX_SIZE").ok().and_then(|s| s.parse().ok()).unwrap_or(30);
|
|
|
|
chalk_recursive::RecursiveSolver::new(overflow_depth, max_size, caching_enabled)
|
2019-04-20 05:34:36 -05:00
|
|
|
}
|
|
|
|
|
2019-06-29 10:40:00 -05:00
|
|
|
/// A set of clauses that we assume to be true. E.g. if we are inside this function:
|
|
|
|
/// ```rust
|
|
|
|
/// fn foo<T: Default>(t: T) {}
|
|
|
|
/// ```
|
|
|
|
/// we assume that `T: Default`.
|
2021-03-12 12:12:17 -06:00
|
|
|
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
|
2019-07-09 14:34:23 -05:00
|
|
|
pub struct TraitEnvironment {
|
2021-05-16 08:50:28 -05:00
|
|
|
pub krate: CrateId,
|
2021-03-12 12:12:17 -06:00
|
|
|
// When we're using Chalk's Ty we can make this a BTreeMap since it's Ord,
|
|
|
|
// but for now it's too annoying...
|
|
|
|
pub(crate) traits_from_clauses: Vec<(Ty, TraitId)>,
|
2021-03-21 14:19:07 -05:00
|
|
|
pub env: chalk_ir::Environment<Interner>,
|
2019-06-29 12:14:52 -05:00
|
|
|
}
|
2019-06-29 10:40:00 -05:00
|
|
|
|
2019-09-07 09:24:26 -05:00
|
|
|
impl TraitEnvironment {
|
2021-05-16 08:50:28 -05:00
|
|
|
pub fn empty(krate: CrateId) -> Self {
|
|
|
|
TraitEnvironment {
|
|
|
|
krate,
|
|
|
|
traits_from_clauses: Vec::new(),
|
|
|
|
env: chalk_ir::Environment::new(&Interner),
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2021-03-12 12:12:17 -06:00
|
|
|
pub(crate) fn traits_in_scope_from_clauses<'a>(
|
2019-09-07 09:24:26 -05:00
|
|
|
&'a self,
|
|
|
|
ty: &'a Ty,
|
2021-03-12 12:12:17 -06:00
|
|
|
) -> impl Iterator<Item = TraitId> + 'a {
|
|
|
|
self.traits_from_clauses.iter().filter_map(move |(self_ty, trait_id)| {
|
|
|
|
if self_ty == ty {
|
|
|
|
Some(*trait_id)
|
|
|
|
} else {
|
|
|
|
None
|
|
|
|
}
|
2019-09-07 09:24:26 -05:00
|
|
|
})
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2019-07-08 14:43:52 -05:00
|
|
|
/// Solve a trait goal using Chalk.
|
2019-07-09 14:34:23 -05:00
|
|
|
pub(crate) fn trait_solve_query(
|
2020-03-13 10:05:46 -05:00
|
|
|
db: &dyn HirDatabase,
|
2019-11-27 00:42:55 -06:00
|
|
|
krate: CrateId,
|
2021-05-16 08:50:28 -05:00
|
|
|
goal: Canonical<InEnvironment<Goal>>,
|
2019-04-20 05:34:36 -05:00
|
|
|
) -> Option<Solution> {
|
2021-05-16 08:50:28 -05:00
|
|
|
let _p = profile::span("trait_solve_query").detail(|| match &goal.value.goal.data(&Interner) {
|
|
|
|
GoalData::DomainGoal(DomainGoal::Holds(WhereClause::Implemented(it))) => {
|
2021-03-20 05:23:59 -05:00
|
|
|
db.trait_data(it.hir_trait_id()).name.to_string()
|
|
|
|
}
|
2021-05-16 08:50:28 -05:00
|
|
|
GoalData::DomainGoal(DomainGoal::Holds(WhereClause::AliasEq(_))) => "alias_eq".to_string(),
|
2021-04-08 06:51:04 -05:00
|
|
|
_ => "??".to_string(),
|
2020-03-06 10:23:08 -06:00
|
|
|
});
|
2021-05-16 08:50:28 -05:00
|
|
|
log::info!("trait_solve_query({:?})", goal.value.goal);
|
2019-09-24 12:04:53 -05:00
|
|
|
|
2021-05-16 08:50:28 -05:00
|
|
|
if let GoalData::DomainGoal(DomainGoal::Holds(WhereClause::AliasEq(AliasEq {
|
2021-03-20 05:23:59 -05:00
|
|
|
alias: AliasTy::Projection(projection_ty),
|
|
|
|
..
|
2021-05-16 08:50:28 -05:00
|
|
|
}))) = &goal.value.goal.data(&Interner)
|
2021-03-18 20:07:15 -05:00
|
|
|
{
|
2021-04-05 09:37:24 -05:00
|
|
|
if let TyKind::BoundVar(_) = projection_ty.self_type_parameter(&Interner).kind(&Interner) {
|
2019-09-24 12:04:53 -05:00
|
|
|
// Hack: don't ask Chalk to normalize with an unknown self type, it'll say that's impossible
|
|
|
|
return Some(Solution::Ambig(Guidance::Unknown));
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2019-05-21 12:57:36 -05:00
|
|
|
// We currently don't deal with universes (I think / hope they're not yet
|
|
|
|
// relevant for our use cases?)
|
2021-05-16 08:50:28 -05:00
|
|
|
let u_canonical = chalk_ir::UCanonical { canonical: goal, universes: 1 };
|
2021-04-08 07:35:15 -05:00
|
|
|
solve(db, krate, &u_canonical)
|
2019-03-31 13:02:16 -05:00
|
|
|
}
|
|
|
|
|
2020-03-06 16:04:14 -06:00
|
|
|
fn solve(
|
2020-03-13 10:05:46 -05:00
|
|
|
db: &dyn HirDatabase,
|
2020-03-06 16:04:14 -06:00
|
|
|
krate: CrateId,
|
|
|
|
goal: &chalk_ir::UCanonical<chalk_ir::InEnvironment<chalk_ir::Goal<Interner>>>,
|
|
|
|
) -> Option<chalk_solve::Solution<Interner>> {
|
|
|
|
let context = ChalkContext { db, krate };
|
|
|
|
log::debug!("solve goal: {:?}", goal);
|
|
|
|
let mut solver = create_chalk_solver();
|
|
|
|
|
|
|
|
let fuel = std::cell::Cell::new(CHALK_SOLVER_FUEL);
|
|
|
|
|
2020-03-27 12:56:18 -05:00
|
|
|
let should_continue = || {
|
2020-03-06 16:04:14 -06:00
|
|
|
context.db.check_canceled();
|
|
|
|
let remaining = fuel.get();
|
|
|
|
fuel.set(remaining - 1);
|
|
|
|
if remaining == 0 {
|
|
|
|
log::debug!("fuel exhausted");
|
|
|
|
}
|
|
|
|
remaining > 0
|
2020-03-27 12:56:18 -05:00
|
|
|
};
|
2020-07-26 05:27:25 -05:00
|
|
|
|
2020-08-14 07:47:06 -05:00
|
|
|
let mut solve = || {
|
2020-10-23 08:25:22 -05:00
|
|
|
let _ctx = if is_chalk_debug() || is_chalk_print() {
|
|
|
|
Some(panic_context::enter(format!("solving {:?}", goal)))
|
|
|
|
} else {
|
|
|
|
None
|
|
|
|
};
|
|
|
|
let solution = if is_chalk_print() {
|
|
|
|
let logging_db =
|
|
|
|
LoggingRustIrDatabaseLoggingOnDrop(LoggingRustIrDatabase::new(context));
|
|
|
|
let solution = solver.solve_limited(&logging_db.0, goal, &should_continue);
|
2020-07-26 05:27:25 -05:00
|
|
|
solution
|
2020-08-14 07:47:06 -05:00
|
|
|
} else {
|
2020-08-16 11:15:44 -05:00
|
|
|
solver.solve_limited(&context, goal, &should_continue)
|
2020-10-23 08:25:22 -05:00
|
|
|
};
|
|
|
|
|
|
|
|
log::debug!("solve({:?}) => {:?}", goal, solution);
|
|
|
|
|
|
|
|
solution
|
2020-04-12 05:28:24 -05:00
|
|
|
};
|
2020-03-06 16:04:14 -06:00
|
|
|
|
2020-08-14 07:47:06 -05:00
|
|
|
// don't set the TLS for Chalk unless Chalk debugging is active, to make
|
|
|
|
// extra sure we only use it for debugging
|
|
|
|
let solution =
|
2021-04-09 07:11:37 -05:00
|
|
|
if is_chalk_debug() { crate::tls::set_current_program(db, solve) } else { solve() };
|
2020-08-14 07:47:06 -05:00
|
|
|
|
2020-03-06 16:04:14 -06:00
|
|
|
solution
|
|
|
|
}
|
|
|
|
|
2020-10-23 08:25:22 -05:00
|
|
|
struct LoggingRustIrDatabaseLoggingOnDrop<'a>(LoggingRustIrDatabase<Interner, ChalkContext<'a>>);
|
|
|
|
|
|
|
|
impl<'a> Drop for LoggingRustIrDatabaseLoggingOnDrop<'a> {
|
|
|
|
fn drop(&mut self) {
|
|
|
|
eprintln!("chalk program:\n{}", self.0);
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2020-03-27 12:56:18 -05:00
|
|
|
fn is_chalk_debug() -> bool {
|
|
|
|
std::env::var("CHALK_DEBUG").is_ok()
|
|
|
|
}
|
|
|
|
|
2020-08-14 07:47:06 -05:00
|
|
|
fn is_chalk_print() -> bool {
|
|
|
|
std::env::var("CHALK_PRINT").is_ok()
|
|
|
|
}
|
|
|
|
|
2019-09-09 15:10:58 -05:00
|
|
|
#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)]
|
|
|
|
pub enum FnTrait {
|
|
|
|
FnOnce,
|
|
|
|
FnMut,
|
|
|
|
Fn,
|
|
|
|
}
|
|
|
|
|
|
|
|
impl FnTrait {
|
|
|
|
fn lang_item_name(self) -> &'static str {
|
|
|
|
match self {
|
|
|
|
FnTrait::FnOnce => "fn_once",
|
|
|
|
FnTrait::FnMut => "fn_mut",
|
|
|
|
FnTrait::Fn => "fn",
|
|
|
|
}
|
|
|
|
}
|
2020-06-20 01:42:35 -05:00
|
|
|
|
|
|
|
pub fn get_id(&self, db: &dyn HirDatabase, krate: CrateId) -> Option<TraitId> {
|
|
|
|
let target = db.lang_item(krate, self.lang_item_name().into())?;
|
|
|
|
match target {
|
|
|
|
LangItemTarget::TraitId(t) => Some(t),
|
|
|
|
_ => None,
|
|
|
|
}
|
|
|
|
}
|
2019-09-09 15:10:58 -05:00
|
|
|
}
|