diff options
author | Dmitry <[email protected]> | 2020-08-14 19:32:05 +0100 |
---|---|---|
committer | Dmitry <[email protected]> | 2020-08-14 19:32:05 +0100 |
commit | 178c3e135a2a249692f7784712492e7884ae0c00 (patch) | |
tree | ac6b769dbf7162150caa0c1624786a4dd79ff3be /crates/hir_ty/src/traits.rs | |
parent | 06ff8e6c760ff05f10e868b5d1f9d79e42fbb49c (diff) | |
parent | c2594daf2974dbd4ce3d9b7ec72481764abaceb5 (diff) |
Merge remote-tracking branch 'origin/master'
Diffstat (limited to 'crates/hir_ty/src/traits.rs')
-rw-r--r-- | crates/hir_ty/src/traits.rs | 285 |
1 files changed, 285 insertions, 0 deletions
diff --git a/crates/hir_ty/src/traits.rs b/crates/hir_ty/src/traits.rs new file mode 100644 index 000000000..1c3abb18f --- /dev/null +++ b/crates/hir_ty/src/traits.rs | |||
@@ -0,0 +1,285 @@ | |||
1 | //! Trait solving using Chalk. | ||
2 | use std::sync::Arc; | ||
3 | |||
4 | use base_db::CrateId; | ||
5 | use chalk_ir::cast::Cast; | ||
6 | use chalk_solve::{logging_db::LoggingRustIrDatabase, Solver}; | ||
7 | use hir_def::{lang_item::LangItemTarget, TraitId}; | ||
8 | |||
9 | use crate::{db::HirDatabase, DebruijnIndex, Substs}; | ||
10 | |||
11 | use super::{Canonical, GenericPredicate, HirDisplay, ProjectionTy, TraitRef, Ty, TypeWalk}; | ||
12 | |||
13 | use self::chalk::{from_chalk, Interner, ToChalk}; | ||
14 | |||
15 | pub(crate) mod chalk; | ||
16 | |||
17 | // This controls the maximum size of types Chalk considers. If we set this too | ||
18 | // high, we can run into slow edge cases; if we set it too low, Chalk won't | ||
19 | // find some solutions. | ||
20 | // FIXME this is currently hardcoded in the recursive solver | ||
21 | // const CHALK_SOLVER_MAX_SIZE: usize = 10; | ||
22 | |||
23 | /// This controls how much 'time' we give the Chalk solver before giving up. | ||
24 | const CHALK_SOLVER_FUEL: i32 = 100; | ||
25 | |||
26 | #[derive(Debug, Copy, Clone)] | ||
27 | struct ChalkContext<'a> { | ||
28 | db: &'a dyn HirDatabase, | ||
29 | krate: CrateId, | ||
30 | } | ||
31 | |||
32 | fn create_chalk_solver() -> chalk_recursive::RecursiveSolver<Interner> { | ||
33 | let overflow_depth = 100; | ||
34 | let caching_enabled = true; | ||
35 | chalk_recursive::RecursiveSolver::new(overflow_depth, caching_enabled) | ||
36 | } | ||
37 | |||
38 | /// A set of clauses that we assume to be true. E.g. if we are inside this function: | ||
39 | /// ```rust | ||
40 | /// fn foo<T: Default>(t: T) {} | ||
41 | /// ``` | ||
42 | /// we assume that `T: Default`. | ||
43 | #[derive(Clone, Debug, PartialEq, Eq, Hash)] | ||
44 | pub struct TraitEnvironment { | ||
45 | pub predicates: Vec<GenericPredicate>, | ||
46 | } | ||
47 | |||
48 | impl TraitEnvironment { | ||
49 | /// Returns trait refs with the given self type which are supposed to hold | ||
50 | /// in this trait env. E.g. if we are in `foo<T: SomeTrait>()`, this will | ||
51 | /// find that `T: SomeTrait` if we call it for `T`. | ||
52 | pub(crate) fn trait_predicates_for_self_ty<'a>( | ||
53 | &'a self, | ||
54 | ty: &'a Ty, | ||
55 | ) -> impl Iterator<Item = &'a TraitRef> + 'a { | ||
56 | self.predicates.iter().filter_map(move |pred| match pred { | ||
57 | GenericPredicate::Implemented(tr) if tr.self_ty() == ty => Some(tr), | ||
58 | _ => None, | ||
59 | }) | ||
60 | } | ||
61 | } | ||
62 | |||
63 | /// Something (usually a goal), along with an environment. | ||
64 | #[derive(Clone, Debug, PartialEq, Eq, Hash)] | ||
65 | pub struct InEnvironment<T> { | ||
66 | pub environment: Arc<TraitEnvironment>, | ||
67 | pub value: T, | ||
68 | } | ||
69 | |||
70 | impl<T> InEnvironment<T> { | ||
71 | pub fn new(environment: Arc<TraitEnvironment>, value: T) -> InEnvironment<T> { | ||
72 | InEnvironment { environment, value } | ||
73 | } | ||
74 | } | ||
75 | |||
76 | /// Something that needs to be proven (by Chalk) during type checking, e.g. that | ||
77 | /// a certain type implements a certain trait. Proving the Obligation might | ||
78 | /// result in additional information about inference variables. | ||
79 | #[derive(Clone, Debug, PartialEq, Eq, Hash)] | ||
80 | pub enum Obligation { | ||
81 | /// Prove that a certain type implements a trait (the type is the `Self` type | ||
82 | /// parameter to the `TraitRef`). | ||
83 | Trait(TraitRef), | ||
84 | Projection(ProjectionPredicate), | ||
85 | } | ||
86 | |||
87 | impl Obligation { | ||
88 | pub fn from_predicate(predicate: GenericPredicate) -> Option<Obligation> { | ||
89 | match predicate { | ||
90 | GenericPredicate::Implemented(trait_ref) => Some(Obligation::Trait(trait_ref)), | ||
91 | GenericPredicate::Projection(projection_pred) => { | ||
92 | Some(Obligation::Projection(projection_pred)) | ||
93 | } | ||
94 | GenericPredicate::Error => None, | ||
95 | } | ||
96 | } | ||
97 | } | ||
98 | |||
99 | #[derive(Clone, Debug, PartialEq, Eq, Hash)] | ||
100 | pub struct ProjectionPredicate { | ||
101 | pub projection_ty: ProjectionTy, | ||
102 | pub ty: Ty, | ||
103 | } | ||
104 | |||
105 | impl TypeWalk for ProjectionPredicate { | ||
106 | fn walk(&self, f: &mut impl FnMut(&Ty)) { | ||
107 | self.projection_ty.walk(f); | ||
108 | self.ty.walk(f); | ||
109 | } | ||
110 | |||
111 | fn walk_mut_binders( | ||
112 | &mut self, | ||
113 | f: &mut impl FnMut(&mut Ty, DebruijnIndex), | ||
114 | binders: DebruijnIndex, | ||
115 | ) { | ||
116 | self.projection_ty.walk_mut_binders(f, binders); | ||
117 | self.ty.walk_mut_binders(f, binders); | ||
118 | } | ||
119 | } | ||
120 | |||
121 | /// Solve a trait goal using Chalk. | ||
122 | pub(crate) fn trait_solve_query( | ||
123 | db: &dyn HirDatabase, | ||
124 | krate: CrateId, | ||
125 | goal: Canonical<InEnvironment<Obligation>>, | ||
126 | ) -> Option<Solution> { | ||
127 | let _p = profile::span("trait_solve_query").detail(|| match &goal.value.value { | ||
128 | Obligation::Trait(it) => db.trait_data(it.trait_).name.to_string(), | ||
129 | Obligation::Projection(_) => "projection".to_string(), | ||
130 | }); | ||
131 | log::info!("trait_solve_query({})", goal.value.value.display(db)); | ||
132 | |||
133 | if let Obligation::Projection(pred) = &goal.value.value { | ||
134 | if let Ty::Bound(_) = &pred.projection_ty.parameters[0] { | ||
135 | // Hack: don't ask Chalk to normalize with an unknown self type, it'll say that's impossible | ||
136 | return Some(Solution::Ambig(Guidance::Unknown)); | ||
137 | } | ||
138 | } | ||
139 | |||
140 | let canonical = goal.to_chalk(db).cast(&Interner); | ||
141 | |||
142 | // We currently don't deal with universes (I think / hope they're not yet | ||
143 | // relevant for our use cases?) | ||
144 | let u_canonical = chalk_ir::UCanonical { canonical, universes: 1 }; | ||
145 | let solution = solve(db, krate, &u_canonical); | ||
146 | solution.map(|solution| solution_from_chalk(db, solution)) | ||
147 | } | ||
148 | |||
149 | fn solve( | ||
150 | db: &dyn HirDatabase, | ||
151 | krate: CrateId, | ||
152 | goal: &chalk_ir::UCanonical<chalk_ir::InEnvironment<chalk_ir::Goal<Interner>>>, | ||
153 | ) -> Option<chalk_solve::Solution<Interner>> { | ||
154 | let context = ChalkContext { db, krate }; | ||
155 | log::debug!("solve goal: {:?}", goal); | ||
156 | let mut solver = create_chalk_solver(); | ||
157 | |||
158 | let fuel = std::cell::Cell::new(CHALK_SOLVER_FUEL); | ||
159 | |||
160 | let should_continue = || { | ||
161 | context.db.check_canceled(); | ||
162 | let remaining = fuel.get(); | ||
163 | fuel.set(remaining - 1); | ||
164 | if remaining == 0 { | ||
165 | log::debug!("fuel exhausted"); | ||
166 | } | ||
167 | remaining > 0 | ||
168 | }; | ||
169 | |||
170 | let mut solve = || { | ||
171 | if is_chalk_print() { | ||
172 | let logging_db = LoggingRustIrDatabase::new(context); | ||
173 | let solution = solver.solve_limited(&logging_db, goal, should_continue); | ||
174 | log::debug!("chalk program:\n{}", logging_db); | ||
175 | solution | ||
176 | } else { | ||
177 | solver.solve_limited(&context, goal, should_continue) | ||
178 | } | ||
179 | }; | ||
180 | |||
181 | // don't set the TLS for Chalk unless Chalk debugging is active, to make | ||
182 | // extra sure we only use it for debugging | ||
183 | let solution = | ||
184 | if is_chalk_debug() { chalk::tls::set_current_program(db, solve) } else { solve() }; | ||
185 | |||
186 | log::debug!("solve({:?}) => {:?}", goal, solution); | ||
187 | |||
188 | solution | ||
189 | } | ||
190 | |||
191 | fn is_chalk_debug() -> bool { | ||
192 | std::env::var("CHALK_DEBUG").is_ok() | ||
193 | } | ||
194 | |||
195 | fn is_chalk_print() -> bool { | ||
196 | std::env::var("CHALK_PRINT").is_ok() | ||
197 | } | ||
198 | |||
199 | fn solution_from_chalk( | ||
200 | db: &dyn HirDatabase, | ||
201 | solution: chalk_solve::Solution<Interner>, | ||
202 | ) -> Solution { | ||
203 | let convert_subst = |subst: chalk_ir::Canonical<chalk_ir::Substitution<Interner>>| { | ||
204 | let result = from_chalk(db, subst); | ||
205 | SolutionVariables(result) | ||
206 | }; | ||
207 | match solution { | ||
208 | chalk_solve::Solution::Unique(constr_subst) => { | ||
209 | let subst = chalk_ir::Canonical { | ||
210 | value: constr_subst.value.subst, | ||
211 | binders: constr_subst.binders, | ||
212 | }; | ||
213 | Solution::Unique(convert_subst(subst)) | ||
214 | } | ||
215 | chalk_solve::Solution::Ambig(chalk_solve::Guidance::Definite(subst)) => { | ||
216 | Solution::Ambig(Guidance::Definite(convert_subst(subst))) | ||
217 | } | ||
218 | chalk_solve::Solution::Ambig(chalk_solve::Guidance::Suggested(subst)) => { | ||
219 | Solution::Ambig(Guidance::Suggested(convert_subst(subst))) | ||
220 | } | ||
221 | chalk_solve::Solution::Ambig(chalk_solve::Guidance::Unknown) => { | ||
222 | Solution::Ambig(Guidance::Unknown) | ||
223 | } | ||
224 | } | ||
225 | } | ||
226 | |||
227 | #[derive(Clone, Debug, PartialEq, Eq)] | ||
228 | pub struct SolutionVariables(pub Canonical<Substs>); | ||
229 | |||
230 | #[derive(Clone, Debug, PartialEq, Eq)] | ||
231 | /// A (possible) solution for a proposed goal. | ||
232 | pub enum Solution { | ||
233 | /// The goal indeed holds, and there is a unique value for all existential | ||
234 | /// variables. | ||
235 | Unique(SolutionVariables), | ||
236 | |||
237 | /// The goal may be provable in multiple ways, but regardless we may have some guidance | ||
238 | /// for type inference. In this case, we don't return any lifetime | ||
239 | /// constraints, since we have not "committed" to any particular solution | ||
240 | /// yet. | ||
241 | Ambig(Guidance), | ||
242 | } | ||
243 | |||
244 | #[derive(Clone, Debug, PartialEq, Eq)] | ||
245 | /// When a goal holds ambiguously (e.g., because there are multiple possible | ||
246 | /// solutions), we issue a set of *guidance* back to type inference. | ||
247 | pub enum Guidance { | ||
248 | /// The existential variables *must* have the given values if the goal is | ||
249 | /// ever to hold, but that alone isn't enough to guarantee the goal will | ||
250 | /// actually hold. | ||
251 | Definite(SolutionVariables), | ||
252 | |||
253 | /// There are multiple plausible values for the existentials, but the ones | ||
254 | /// here are suggested as the preferred choice heuristically. These should | ||
255 | /// be used for inference fallback only. | ||
256 | Suggested(SolutionVariables), | ||
257 | |||
258 | /// There's no useful information to feed back to type inference | ||
259 | Unknown, | ||
260 | } | ||
261 | |||
262 | #[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)] | ||
263 | pub enum FnTrait { | ||
264 | FnOnce, | ||
265 | FnMut, | ||
266 | Fn, | ||
267 | } | ||
268 | |||
269 | impl FnTrait { | ||
270 | fn lang_item_name(self) -> &'static str { | ||
271 | match self { | ||
272 | FnTrait::FnOnce => "fn_once", | ||
273 | FnTrait::FnMut => "fn_mut", | ||
274 | FnTrait::Fn => "fn", | ||
275 | } | ||
276 | } | ||
277 | |||
278 | pub fn get_id(&self, db: &dyn HirDatabase, krate: CrateId) -> Option<TraitId> { | ||
279 | let target = db.lang_item(krate, self.lang_item_name().into())?; | ||
280 | match target { | ||
281 | LangItemTarget::TraitId(t) => Some(t), | ||
282 | _ => None, | ||
283 | } | ||
284 | } | ||
285 | } | ||