diff options
Diffstat (limited to 'crates/hir_ty/src/traits.rs')
-rw-r--r-- | crates/hir_ty/src/traits.rs | 140 |
1 files changed, 13 insertions, 127 deletions
diff --git a/crates/hir_ty/src/traits.rs b/crates/hir_ty/src/traits.rs index ccee0e5ad..9936d0803 100644 --- a/crates/hir_ty/src/traits.rs +++ b/crates/hir_ty/src/traits.rs | |||
@@ -1,28 +1,26 @@ | |||
1 | //! Trait solving using Chalk. | 1 | //! Trait solving using Chalk. |
2 | |||
2 | use std::env::var; | 3 | use std::env::var; |
3 | 4 | ||
4 | use base_db::CrateId; | ||
5 | use chalk_ir::cast::Cast; | 5 | use chalk_ir::cast::Cast; |
6 | use chalk_solve::{logging_db::LoggingRustIrDatabase, Solver}; | 6 | use chalk_solve::{logging_db::LoggingRustIrDatabase, Solver}; |
7 | |||
8 | use base_db::CrateId; | ||
7 | use hir_def::{lang_item::LangItemTarget, TraitId}; | 9 | use hir_def::{lang_item::LangItemTarget, TraitId}; |
8 | use stdx::panic_context; | 10 | use stdx::panic_context; |
9 | 11 | ||
10 | use crate::{ | 12 | use crate::{ |
11 | db::HirDatabase, AliasTy, Canonical, DebruijnIndex, HirDisplay, Substitution, Ty, TyKind, | 13 | db::HirDatabase, AliasEq, AliasTy, Canonical, DomainGoal, Guidance, HirDisplay, InEnvironment, |
12 | TypeWalk, WhereClause, | 14 | Interner, Solution, TraitRefExt, Ty, TyKind, WhereClause, |
13 | }; | 15 | }; |
14 | 16 | ||
15 | use self::chalk::{from_chalk, Interner, ToChalk}; | ||
16 | |||
17 | pub(crate) mod chalk; | ||
18 | |||
19 | /// This controls how much 'time' we give the Chalk solver before giving up. | 17 | /// This controls how much 'time' we give the Chalk solver before giving up. |
20 | const CHALK_SOLVER_FUEL: i32 = 100; | 18 | const CHALK_SOLVER_FUEL: i32 = 100; |
21 | 19 | ||
22 | #[derive(Debug, Copy, Clone)] | 20 | #[derive(Debug, Copy, Clone)] |
23 | struct ChalkContext<'a> { | 21 | pub(crate) struct ChalkContext<'a> { |
24 | db: &'a dyn HirDatabase, | 22 | pub(crate) db: &'a dyn HirDatabase, |
25 | krate: CrateId, | 23 | pub(crate) krate: CrateId, |
26 | } | 24 | } |
27 | 25 | ||
28 | fn create_chalk_solver() -> chalk_recursive::RecursiveSolver<Interner> { | 26 | fn create_chalk_solver() -> chalk_recursive::RecursiveSolver<Interner> { |
@@ -70,55 +68,6 @@ impl Default for TraitEnvironment { | |||
70 | } | 68 | } |
71 | } | 69 | } |
72 | 70 | ||
73 | /// Something (usually a goal), along with an environment. | ||
74 | #[derive(Clone, Debug, PartialEq, Eq, Hash)] | ||
75 | pub struct InEnvironment<T> { | ||
76 | pub environment: chalk_ir::Environment<Interner>, | ||
77 | pub goal: T, | ||
78 | } | ||
79 | |||
80 | impl<T> InEnvironment<T> { | ||
81 | pub fn new(environment: chalk_ir::Environment<Interner>, value: T) -> InEnvironment<T> { | ||
82 | InEnvironment { environment, goal: value } | ||
83 | } | ||
84 | } | ||
85 | |||
86 | /// Something that needs to be proven (by Chalk) during type checking, e.g. that | ||
87 | /// a certain type implements a certain trait. Proving the Obligation might | ||
88 | /// result in additional information about inference variables. | ||
89 | #[derive(Clone, Debug, PartialEq, Eq, Hash)] | ||
90 | pub enum DomainGoal { | ||
91 | Holds(WhereClause), | ||
92 | } | ||
93 | |||
94 | #[derive(Clone, Debug, PartialEq, Eq, Hash)] | ||
95 | pub struct AliasEq { | ||
96 | pub alias: AliasTy, | ||
97 | pub ty: Ty, | ||
98 | } | ||
99 | |||
100 | impl TypeWalk for AliasEq { | ||
101 | fn walk(&self, f: &mut impl FnMut(&Ty)) { | ||
102 | self.ty.walk(f); | ||
103 | match &self.alias { | ||
104 | AliasTy::Projection(projection_ty) => projection_ty.walk(f), | ||
105 | AliasTy::Opaque(opaque) => opaque.walk(f), | ||
106 | } | ||
107 | } | ||
108 | |||
109 | fn walk_mut_binders( | ||
110 | &mut self, | ||
111 | f: &mut impl FnMut(&mut Ty, DebruijnIndex), | ||
112 | binders: DebruijnIndex, | ||
113 | ) { | ||
114 | self.ty.walk_mut_binders(f, binders); | ||
115 | match &mut self.alias { | ||
116 | AliasTy::Projection(projection_ty) => projection_ty.walk_mut_binders(f, binders), | ||
117 | AliasTy::Opaque(opaque) => opaque.walk_mut_binders(f, binders), | ||
118 | } | ||
119 | } | ||
120 | } | ||
121 | |||
122 | /// Solve a trait goal using Chalk. | 71 | /// Solve a trait goal using Chalk. |
123 | pub(crate) fn trait_solve_query( | 72 | pub(crate) fn trait_solve_query( |
124 | db: &dyn HirDatabase, | 73 | db: &dyn HirDatabase, |
@@ -130,6 +79,7 @@ pub(crate) fn trait_solve_query( | |||
130 | db.trait_data(it.hir_trait_id()).name.to_string() | 79 | db.trait_data(it.hir_trait_id()).name.to_string() |
131 | } | 80 | } |
132 | DomainGoal::Holds(WhereClause::AliasEq(_)) => "alias_eq".to_string(), | 81 | DomainGoal::Holds(WhereClause::AliasEq(_)) => "alias_eq".to_string(), |
82 | _ => "??".to_string(), | ||
133 | }); | 83 | }); |
134 | log::info!("trait_solve_query({})", goal.value.goal.display(db)); | 84 | log::info!("trait_solve_query({})", goal.value.goal.display(db)); |
135 | 85 | ||
@@ -138,19 +88,18 @@ pub(crate) fn trait_solve_query( | |||
138 | .. | 88 | .. |
139 | })) = &goal.value.goal | 89 | })) = &goal.value.goal |
140 | { | 90 | { |
141 | if let TyKind::BoundVar(_) = &projection_ty.substitution[0].interned(&Interner) { | 91 | if let TyKind::BoundVar(_) = projection_ty.self_type_parameter(&Interner).kind(&Interner) { |
142 | // Hack: don't ask Chalk to normalize with an unknown self type, it'll say that's impossible | 92 | // Hack: don't ask Chalk to normalize with an unknown self type, it'll say that's impossible |
143 | return Some(Solution::Ambig(Guidance::Unknown)); | 93 | return Some(Solution::Ambig(Guidance::Unknown)); |
144 | } | 94 | } |
145 | } | 95 | } |
146 | 96 | ||
147 | let canonical = goal.to_chalk(db).cast(&Interner); | 97 | let canonical = goal.cast(&Interner); |
148 | 98 | ||
149 | // We currently don't deal with universes (I think / hope they're not yet | 99 | // We currently don't deal with universes (I think / hope they're not yet |
150 | // relevant for our use cases?) | 100 | // relevant for our use cases?) |
151 | let u_canonical = chalk_ir::UCanonical { canonical, universes: 1 }; | 101 | let u_canonical = chalk_ir::UCanonical { canonical, universes: 1 }; |
152 | let solution = solve(db, krate, &u_canonical); | 102 | solve(db, krate, &u_canonical) |
153 | solution.map(|solution| solution_from_chalk(db, solution)) | ||
154 | } | 103 | } |
155 | 104 | ||
156 | fn solve( | 105 | fn solve( |
@@ -197,7 +146,7 @@ fn solve( | |||
197 | // don't set the TLS for Chalk unless Chalk debugging is active, to make | 146 | // don't set the TLS for Chalk unless Chalk debugging is active, to make |
198 | // extra sure we only use it for debugging | 147 | // extra sure we only use it for debugging |
199 | let solution = | 148 | let solution = |
200 | if is_chalk_debug() { chalk::tls::set_current_program(db, solve) } else { solve() }; | 149 | if is_chalk_debug() { crate::tls::set_current_program(db, solve) } else { solve() }; |
201 | 150 | ||
202 | solution | 151 | solution |
203 | } | 152 | } |
@@ -218,69 +167,6 @@ fn is_chalk_print() -> bool { | |||
218 | std::env::var("CHALK_PRINT").is_ok() | 167 | std::env::var("CHALK_PRINT").is_ok() |
219 | } | 168 | } |
220 | 169 | ||
221 | fn solution_from_chalk( | ||
222 | db: &dyn HirDatabase, | ||
223 | solution: chalk_solve::Solution<Interner>, | ||
224 | ) -> Solution { | ||
225 | let convert_subst = |subst: chalk_ir::Canonical<chalk_ir::Substitution<Interner>>| { | ||
226 | let result = from_chalk(db, subst); | ||
227 | SolutionVariables(result) | ||
228 | }; | ||
229 | match solution { | ||
230 | chalk_solve::Solution::Unique(constr_subst) => { | ||
231 | let subst = chalk_ir::Canonical { | ||
232 | value: constr_subst.value.subst, | ||
233 | binders: constr_subst.binders, | ||
234 | }; | ||
235 | Solution::Unique(convert_subst(subst)) | ||
236 | } | ||
237 | chalk_solve::Solution::Ambig(chalk_solve::Guidance::Definite(subst)) => { | ||
238 | Solution::Ambig(Guidance::Definite(convert_subst(subst))) | ||
239 | } | ||
240 | chalk_solve::Solution::Ambig(chalk_solve::Guidance::Suggested(subst)) => { | ||
241 | Solution::Ambig(Guidance::Suggested(convert_subst(subst))) | ||
242 | } | ||
243 | chalk_solve::Solution::Ambig(chalk_solve::Guidance::Unknown) => { | ||
244 | Solution::Ambig(Guidance::Unknown) | ||
245 | } | ||
246 | } | ||
247 | } | ||
248 | |||
249 | #[derive(Clone, Debug, PartialEq, Eq)] | ||
250 | pub struct SolutionVariables(pub Canonical<Substitution>); | ||
251 | |||
252 | #[derive(Clone, Debug, PartialEq, Eq)] | ||
253 | /// A (possible) solution for a proposed goal. | ||
254 | pub enum Solution { | ||
255 | /// The goal indeed holds, and there is a unique value for all existential | ||
256 | /// variables. | ||
257 | Unique(SolutionVariables), | ||
258 | |||
259 | /// The goal may be provable in multiple ways, but regardless we may have some guidance | ||
260 | /// for type inference. In this case, we don't return any lifetime | ||
261 | /// constraints, since we have not "committed" to any particular solution | ||
262 | /// yet. | ||
263 | Ambig(Guidance), | ||
264 | } | ||
265 | |||
266 | #[derive(Clone, Debug, PartialEq, Eq)] | ||
267 | /// When a goal holds ambiguously (e.g., because there are multiple possible | ||
268 | /// solutions), we issue a set of *guidance* back to type inference. | ||
269 | pub enum Guidance { | ||
270 | /// The existential variables *must* have the given values if the goal is | ||
271 | /// ever to hold, but that alone isn't enough to guarantee the goal will | ||
272 | /// actually hold. | ||
273 | Definite(SolutionVariables), | ||
274 | |||
275 | /// There are multiple plausible values for the existentials, but the ones | ||
276 | /// here are suggested as the preferred choice heuristically. These should | ||
277 | /// be used for inference fallback only. | ||
278 | Suggested(SolutionVariables), | ||
279 | |||
280 | /// There's no useful information to feed back to type inference | ||
281 | Unknown, | ||
282 | } | ||
283 | |||
284 | #[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)] | 170 | #[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)] |
285 | pub enum FnTrait { | 171 | pub enum FnTrait { |
286 | FnOnce, | 172 | FnOnce, |