]>
Commit | Line | Data |
---|---|---|
f035d41b XL |
1 | //! Defines the IR for types and logical predicates. |
2 | ||
f9f354fc | 3 | #![deny(rust_2018_idioms)] |
f035d41b | 4 | #![warn(missing_docs)] |
f9f354fc XL |
5 | |
6 | // Allows macros to refer to this crate as `::chalk_ir` | |
7 | extern crate self as chalk_ir; | |
8 | ||
3dfed10e | 9 | use crate::cast::{Cast, CastTo, Caster}; |
f9f354fc XL |
10 | use crate::fold::shift::Shift; |
11 | use crate::fold::{Fold, Folder, Subst, SuperFold}; | |
a2a8927a | 12 | use crate::visit::{SuperVisit, Visit, VisitExt, Visitor}; |
f9f354fc | 13 | use chalk_derive::{Fold, HasInterner, SuperVisit, Visit, Zip}; |
f9f354fc | 14 | use std::marker::PhantomData; |
a2a8927a | 15 | use std::ops::ControlFlow; |
f9f354fc XL |
16 | |
17 | pub use crate::debug::SeparatorTraitRef; | |
5869c6ff XL |
18 | #[macro_use(bitflags)] |
19 | extern crate bitflags; | |
f035d41b | 20 | /// Uninhabited (empty) type, used in combination with `PhantomData`. |
f9f354fc XL |
21 | #[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] |
22 | pub enum Void {} | |
23 | ||
f035d41b XL |
24 | /// Many of our internal operations (e.g., unification) are an attempt |
25 | /// to perform some operation which may not complete. | |
26 | pub type Fallible<T> = Result<T, NoSolution>; | |
27 | ||
5869c6ff XL |
28 | /// A combination of `Fallible` and `Floundered`. |
29 | pub enum FallibleOrFloundered<T> { | |
30 | /// Success | |
31 | Ok(T), | |
32 | /// No solution. See `chalk_ir::NoSolution`. | |
33 | NoSolution, | |
34 | /// Floundered. See `chalk_ir::Floundered`. | |
35 | Floundered, | |
36 | } | |
37 | ||
f035d41b XL |
38 | /// Indicates that the attempted operation has "no solution" -- i.e., |
39 | /// cannot be performed. | |
40 | #[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)] | |
41 | pub struct NoSolution; | |
42 | ||
5869c6ff | 43 | /// Indicates that the complete set of program clauses for this goal |
f035d41b XL |
44 | /// cannot be enumerated. |
45 | pub struct Floundered; | |
46 | ||
f9f354fc XL |
47 | macro_rules! impl_debugs { |
48 | ($($id:ident), *) => { | |
49 | $( | |
50 | impl<I: Interner> std::fmt::Debug for $id<I> { | |
51 | fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> Result<(), std::fmt::Error> { | |
52 | write!(fmt, "{}({:?})", stringify!($id), self.0) | |
53 | } | |
54 | } | |
55 | )* | |
56 | }; | |
57 | } | |
58 | ||
f9f354fc XL |
59 | #[macro_use] |
60 | pub mod zip; | |
61 | ||
62 | #[macro_use] | |
63 | pub mod fold; | |
64 | ||
65 | #[macro_use] | |
66 | pub mod visit; | |
67 | ||
68 | pub mod cast; | |
69 | ||
70 | pub mod interner; | |
71 | use interner::{HasInterner, Interner}; | |
72 | ||
73 | pub mod could_match; | |
74 | pub mod debug; | |
f9f354fc | 75 | |
5869c6ff XL |
76 | /// Variance |
77 | #[derive(Copy, Clone, Debug, PartialEq, Eq, Hash)] | |
78 | pub enum Variance { | |
79 | /// a <: b | |
80 | Covariant, | |
81 | /// a == b | |
82 | Invariant, | |
83 | /// b <: a | |
84 | Contravariant, | |
85 | } | |
86 | ||
87 | impl Variance { | |
88 | /// `a.xform(b)` combines the variance of a context with the | |
89 | /// variance of a type with the following meaning. If we are in a | |
90 | /// context with variance `a`, and we encounter a type argument in | |
91 | /// a position with variance `b`, then `a.xform(b)` is the new | |
92 | /// variance with which the argument appears. | |
93 | /// | |
94 | /// Example 1: | |
95 | /// | |
96 | /// ```ignore | |
97 | /// *mut Vec<i32> | |
98 | /// ``` | |
99 | /// | |
100 | /// Here, the "ambient" variance starts as covariant. `*mut T` is | |
101 | /// invariant with respect to `T`, so the variance in which the | |
102 | /// `Vec<i32>` appears is `Covariant.xform(Invariant)`, which | |
103 | /// yields `Invariant`. Now, the type `Vec<T>` is covariant with | |
104 | /// respect to its type argument `T`, and hence the variance of | |
105 | /// the `i32` here is `Invariant.xform(Covariant)`, which results | |
106 | /// (again) in `Invariant`. | |
107 | /// | |
108 | /// Example 2: | |
109 | /// | |
110 | /// ```ignore | |
111 | /// fn(*const Vec<i32>, *mut Vec<i32) | |
112 | /// ``` | |
113 | /// | |
114 | /// The ambient variance is covariant. A `fn` type is | |
115 | /// contravariant with respect to its parameters, so the variance | |
116 | /// within which both pointer types appear is | |
117 | /// `Covariant.xform(Contravariant)`, or `Contravariant`. `*const | |
118 | /// T` is covariant with respect to `T`, so the variance within | |
119 | /// which the first `Vec<i32>` appears is | |
120 | /// `Contravariant.xform(Covariant)` or `Contravariant`. The same | |
121 | /// is true for its `i32` argument. In the `*mut T` case, the | |
122 | /// variance of `Vec<i32>` is `Contravariant.xform(Invariant)`, | |
123 | /// and hence the outermost type is `Invariant` with respect to | |
124 | /// `Vec<i32>` (and its `i32` argument). | |
125 | /// | |
126 | /// Source: Figure 1 of "Taming the Wildcards: | |
127 | /// Combining Definition- and Use-Site Variance" published in PLDI'11. | |
128 | /// (Doc from rustc) | |
129 | pub fn xform(self, other: Variance) -> Variance { | |
130 | match (self, other) { | |
131 | (Variance::Invariant, _) => Variance::Invariant, | |
132 | (_, Variance::Invariant) => Variance::Invariant, | |
133 | (_, Variance::Covariant) => self, | |
134 | (Variance::Covariant, Variance::Contravariant) => Variance::Contravariant, | |
135 | (Variance::Contravariant, Variance::Contravariant) => Variance::Covariant, | |
136 | } | |
137 | } | |
138 | ||
139 | /// Converts `Covariant` into `Contravariant` and vice-versa. `Invariant` | |
140 | /// stays the same. | |
141 | pub fn invert(self) -> Variance { | |
142 | match self { | |
143 | Variance::Invariant => Variance::Invariant, | |
144 | Variance::Covariant => Variance::Contravariant, | |
145 | Variance::Contravariant => Variance::Covariant, | |
146 | } | |
147 | } | |
148 | } | |
149 | ||
f9f354fc XL |
150 | #[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner)] |
151 | /// The set of assumptions we've made so far, and the current number of | |
152 | /// universal (forall) quantifiers we're within. | |
153 | pub struct Environment<I: Interner> { | |
f035d41b | 154 | /// The clauses in the environment. |
f9f354fc XL |
155 | pub clauses: ProgramClauses<I>, |
156 | } | |
157 | ||
f035d41b XL |
158 | impl<I: Interner> Copy for Environment<I> where I::InternedProgramClauses: Copy {} |
159 | ||
f9f354fc | 160 | impl<I: Interner> Environment<I> { |
f035d41b | 161 | /// Creates a new environment. |
a2a8927a | 162 | pub fn new(interner: I) -> Self { |
f9f354fc | 163 | Environment { |
3dfed10e | 164 | clauses: ProgramClauses::empty(interner), |
f9f354fc XL |
165 | } |
166 | } | |
167 | ||
f035d41b | 168 | /// Adds (an iterator of) clauses to the environment. |
a2a8927a | 169 | pub fn add_clauses<II>(&self, interner: I, clauses: II) -> Self |
f9f354fc XL |
170 | where |
171 | II: IntoIterator<Item = ProgramClause<I>>, | |
172 | { | |
173 | let mut env = self.clone(); | |
174 | env.clauses = | |
3dfed10e | 175 | ProgramClauses::from_iter(interner, env.clauses.iter(interner).cloned().chain(clauses)); |
f9f354fc XL |
176 | env |
177 | } | |
3dfed10e XL |
178 | |
179 | /// True if any of the clauses in the environment have a consequence of `Compatible`. | |
180 | /// Panics if the conditions or constraints of that clause are not empty. | |
a2a8927a | 181 | pub fn has_compatible_clause(&self, interner: I) -> bool { |
3dfed10e XL |
182 | self.clauses.as_slice(interner).iter().any(|c| { |
183 | let ProgramClauseData(implication) = c.data(interner); | |
184 | match implication.skip_binders().consequence { | |
185 | DomainGoal::Compatible => { | |
186 | // We currently don't generate `Compatible` with any conditions or constraints | |
187 | // If this was needed, for whatever reason, then a third "yes, but must evaluate" | |
188 | // return value would have to be added. | |
189 | assert!(implication.skip_binders().conditions.is_empty(interner)); | |
190 | assert!(implication.skip_binders().constraints.is_empty(interner)); | |
191 | true | |
192 | } | |
193 | _ => false, | |
194 | } | |
195 | }) | |
196 | } | |
f9f354fc XL |
197 | } |
198 | ||
f035d41b | 199 | /// A goal with an environment to solve it in. |
f9f354fc | 200 | #[derive(Clone, Debug, PartialEq, Eq, Hash, Fold, Visit)] |
f035d41b | 201 | #[allow(missing_docs)] |
f9f354fc XL |
202 | pub struct InEnvironment<G: HasInterner> { |
203 | pub environment: Environment<G::Interner>, | |
204 | pub goal: G, | |
205 | } | |
206 | ||
f035d41b XL |
207 | impl<G: HasInterner<Interner = I> + Copy, I: Interner> Copy for InEnvironment<G> where |
208 | I::InternedProgramClauses: Copy | |
209 | { | |
210 | } | |
211 | ||
f9f354fc | 212 | impl<G: HasInterner> InEnvironment<G> { |
f035d41b | 213 | /// Creates a new environment/goal pair. |
f9f354fc XL |
214 | pub fn new(environment: &Environment<G::Interner>, goal: G) -> Self { |
215 | InEnvironment { | |
216 | environment: environment.clone(), | |
217 | goal, | |
218 | } | |
219 | } | |
220 | ||
f035d41b | 221 | /// Maps the goal without touching the environment. |
f9f354fc XL |
222 | pub fn map<OP, H>(self, op: OP) -> InEnvironment<H> |
223 | where | |
224 | OP: FnOnce(G) -> H, | |
225 | H: HasInterner<Interner = G::Interner>, | |
226 | { | |
227 | InEnvironment { | |
228 | environment: self.environment, | |
229 | goal: op(self.goal), | |
230 | } | |
231 | } | |
232 | } | |
233 | ||
234 | impl<G: HasInterner> HasInterner for InEnvironment<G> { | |
235 | type Interner = G::Interner; | |
236 | } | |
237 | ||
f035d41b | 238 | /// Different signed int types. |
f9f354fc | 239 | #[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)] |
f035d41b | 240 | #[allow(missing_docs)] |
f9f354fc XL |
241 | pub enum IntTy { |
242 | Isize, | |
243 | I8, | |
244 | I16, | |
245 | I32, | |
246 | I64, | |
247 | I128, | |
248 | } | |
249 | ||
f035d41b | 250 | /// Different unsigned int types. |
f9f354fc | 251 | #[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)] |
f035d41b | 252 | #[allow(missing_docs)] |
f9f354fc XL |
253 | pub enum UintTy { |
254 | Usize, | |
255 | U8, | |
256 | U16, | |
257 | U32, | |
258 | U64, | |
259 | U128, | |
260 | } | |
261 | ||
f035d41b | 262 | /// Different kinds of float types. |
f9f354fc | 263 | #[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)] |
f035d41b | 264 | #[allow(missing_docs)] |
f9f354fc XL |
265 | pub enum FloatTy { |
266 | F32, | |
267 | F64, | |
268 | } | |
269 | ||
f035d41b | 270 | /// Types of scalar values. |
f9f354fc | 271 | #[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)] |
f035d41b | 272 | #[allow(missing_docs)] |
f9f354fc XL |
273 | pub enum Scalar { |
274 | Bool, | |
275 | Char, | |
276 | Int(IntTy), | |
277 | Uint(UintTy), | |
278 | Float(FloatTy), | |
279 | } | |
280 | ||
3dfed10e XL |
281 | /// Whether a function is safe or not. |
282 | #[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)] | |
283 | pub enum Safety { | |
284 | /// Safe | |
285 | Safe, | |
286 | /// Unsafe | |
287 | Unsafe, | |
288 | } | |
289 | ||
f035d41b XL |
290 | /// Whether a type is mutable or not. |
291 | #[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)] | |
292 | pub enum Mutability { | |
293 | /// Mutable | |
294 | Mut, | |
295 | /// Immutable | |
296 | Not, | |
297 | } | |
298 | ||
f9f354fc XL |
299 | /// An universe index is how a universally quantified parameter is |
300 | /// represented when it's binder is moved into the environment. | |
301 | /// An example chain of transformations would be: | |
302 | /// `forall<T> { Goal(T) }` (syntactical representation) | |
303 | /// `forall { Goal(?0) }` (used a DeBruijn index) | |
304 | /// `Goal(!U1)` (the quantifier was moved to the environment and replaced with a universe index) | |
a2a8927a | 305 | /// See <https://rustc-dev-guide.rust-lang.org/borrow_check/region_inference.html#placeholders-and-universes> for more. |
f9f354fc XL |
306 | #[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] |
307 | pub struct UniverseIndex { | |
f035d41b | 308 | /// The counter for the universe index, starts with 0. |
f9f354fc XL |
309 | pub counter: usize, |
310 | } | |
311 | ||
312 | impl UniverseIndex { | |
f035d41b | 313 | /// Root universe index (0). |
f9f354fc XL |
314 | pub const ROOT: UniverseIndex = UniverseIndex { counter: 0 }; |
315 | ||
f035d41b | 316 | /// Root universe index (0). |
f9f354fc XL |
317 | pub fn root() -> UniverseIndex { |
318 | Self::ROOT | |
319 | } | |
320 | ||
f035d41b | 321 | /// Whether one universe can "see" another. |
f9f354fc XL |
322 | pub fn can_see(self, ui: UniverseIndex) -> bool { |
323 | self.counter >= ui.counter | |
324 | } | |
325 | ||
f035d41b | 326 | /// Increases the index counter. |
f9f354fc XL |
327 | pub fn next(self) -> UniverseIndex { |
328 | UniverseIndex { | |
329 | counter: self.counter + 1, | |
330 | } | |
331 | } | |
332 | } | |
333 | ||
f035d41b XL |
334 | /// Maps the universes found in the `u_canonicalize` result (the |
335 | /// "canonical" universes) to the universes found in the original | |
336 | /// value (and vice versa). When used as a folder -- i.e., from | |
337 | /// outside this module -- converts from "canonical" universes to the | |
338 | /// original (but see the `UMapToCanonical` folder). | |
339 | #[derive(Clone, Debug)] | |
340 | pub struct UniverseMap { | |
341 | /// A reverse map -- for each universe Ux that appears in | |
342 | /// `quantified`, the corresponding universe in the original was | |
343 | /// `universes[x]`. | |
344 | pub universes: Vec<UniverseIndex>, | |
345 | } | |
346 | ||
347 | impl UniverseMap { | |
348 | /// Creates a new universe map. | |
349 | pub fn new() -> Self { | |
350 | UniverseMap { | |
351 | universes: vec![UniverseIndex::root()], | |
352 | } | |
353 | } | |
354 | ||
355 | /// Number of canonical universes. | |
356 | pub fn num_canonical_universes(&self) -> usize { | |
357 | self.universes.len() | |
358 | } | |
359 | } | |
360 | ||
361 | /// The id for an Abstract Data Type (i.e. structs, unions and enums). | |
f9f354fc | 362 | #[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] |
f035d41b | 363 | pub struct AdtId<I: Interner>(pub I::InternedAdtId); |
f9f354fc XL |
364 | |
365 | /// The id of a trait definition; could be used to load the trait datum by | |
366 | /// invoking the [`trait_datum`] method. | |
367 | /// | |
368 | /// [`trait_datum`]: ../chalk_solve/trait.RustIrDatabase.html#tymethod.trait_datum | |
369 | #[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] | |
370 | pub struct TraitId<I: Interner>(pub I::DefId); | |
371 | ||
f035d41b | 372 | /// The id for an impl. |
f9f354fc XL |
373 | #[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] |
374 | pub struct ImplId<I: Interner>(pub I::DefId); | |
375 | ||
f035d41b | 376 | /// Id for a specific clause. |
f9f354fc XL |
377 | #[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] |
378 | pub struct ClauseId<I: Interner>(pub I::DefId); | |
379 | ||
380 | /// The id for the associated type member of a trait. The details of the type | |
381 | /// can be found by invoking the [`associated_ty_data`] method. | |
382 | /// | |
383 | /// [`associated_ty_data`]: ../chalk_solve/trait.RustIrDatabase.html#tymethod.associated_ty_data | |
384 | #[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] | |
385 | pub struct AssocTypeId<I: Interner>(pub I::DefId); | |
386 | ||
f035d41b | 387 | /// Id for an opaque type. |
f9f354fc XL |
388 | #[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] |
389 | pub struct OpaqueTyId<I: Interner>(pub I::DefId); | |
390 | ||
f035d41b XL |
391 | /// Function definition id. |
392 | #[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] | |
393 | pub struct FnDefId<I: Interner>(pub I::DefId); | |
394 | ||
395 | /// Id for Rust closures. | |
396 | #[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] | |
397 | pub struct ClosureId<I: Interner>(pub I::DefId); | |
398 | ||
29967ef6 XL |
399 | /// Id for Rust generators. |
400 | #[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] | |
401 | pub struct GeneratorId<I: Interner>(pub I::DefId); | |
402 | ||
1b1a35ee XL |
403 | /// Id for foreign types. |
404 | #[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] | |
405 | pub struct ForeignDefId<I: Interner>(pub I::DefId); | |
406 | ||
f9f354fc XL |
407 | impl_debugs!(ImplId, ClauseId); |
408 | ||
29967ef6 | 409 | /// A Rust type. The actual type data is stored in `TyKind`. |
f9f354fc XL |
410 | #[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord, HasInterner)] |
411 | pub struct Ty<I: Interner> { | |
412 | interned: I::InternedType, | |
413 | } | |
414 | ||
415 | impl<I: Interner> Ty<I> { | |
29967ef6 | 416 | /// Creates a type from `TyKind`. |
a2a8927a XL |
417 | pub fn new(interner: I, data: impl CastTo<TyKind<I>>) -> Self { |
418 | let ty_kind = data.cast(interner); | |
f9f354fc | 419 | Ty { |
a2a8927a | 420 | interned: I::intern_ty(interner, ty_kind), |
f9f354fc XL |
421 | } |
422 | } | |
423 | ||
f035d41b | 424 | /// Gets the interned type. |
f9f354fc XL |
425 | pub fn interned(&self) -> &I::InternedType { |
426 | &self.interned | |
427 | } | |
428 | ||
f035d41b | 429 | /// Gets the underlying type data. |
a2a8927a | 430 | pub fn data(&self, interner: I) -> &TyData<I> { |
f9f354fc XL |
431 | I::ty_data(interner, &self.interned) |
432 | } | |
433 | ||
29967ef6 | 434 | /// Gets the underlying type kind. |
a2a8927a | 435 | pub fn kind(&self, interner: I) -> &TyKind<I> { |
29967ef6 XL |
436 | &I::ty_data(interner, &self.interned).kind |
437 | } | |
438 | ||
f035d41b | 439 | /// Creates a `FromEnv` constraint using this type. |
f9f354fc XL |
440 | pub fn from_env(&self) -> FromEnv<I> { |
441 | FromEnv::Ty(self.clone()) | |
442 | } | |
443 | ||
f035d41b | 444 | /// Creates a WF-constraint for this type. |
f9f354fc XL |
445 | pub fn well_formed(&self) -> WellFormed<I> { |
446 | WellFormed::Ty(self.clone()) | |
447 | } | |
448 | ||
449 | /// Creates a domain goal `FromEnv(T)` where `T` is this type. | |
a2a8927a | 450 | pub fn into_from_env_goal(self, interner: I) -> DomainGoal<I> { |
f9f354fc XL |
451 | self.from_env().cast(interner) |
452 | } | |
453 | ||
29967ef6 | 454 | /// If this is a `TyKind::BoundVar(d)`, returns `Some(d)` else `None`. |
a2a8927a | 455 | pub fn bound_var(&self, interner: I) -> Option<BoundVar> { |
29967ef6 | 456 | if let TyKind::BoundVar(bv) = self.kind(interner) { |
f9f354fc XL |
457 | Some(*bv) |
458 | } else { | |
459 | None | |
460 | } | |
461 | } | |
462 | ||
29967ef6 | 463 | /// If this is a `TyKind::InferenceVar(d)`, returns `Some(d)` else `None`. |
a2a8927a | 464 | pub fn inference_var(&self, interner: I) -> Option<InferenceVar> { |
29967ef6 | 465 | if let TyKind::InferenceVar(depth, _) = self.kind(interner) { |
f9f354fc XL |
466 | Some(*depth) |
467 | } else { | |
468 | None | |
469 | } | |
470 | } | |
471 | ||
29967ef6 | 472 | /// Returns true if this is a `BoundVar` or an `InferenceVar` of `TyVariableKind::General`. |
a2a8927a | 473 | pub fn is_general_var(&self, interner: I, binders: &CanonicalVarKinds<I>) -> bool { |
29967ef6 XL |
474 | match self.kind(interner) { |
475 | TyKind::BoundVar(bv) | |
3dfed10e | 476 | if bv.debruijn == DebruijnIndex::INNERMOST |
29967ef6 XL |
477 | && binders.at(interner, bv.index).kind |
478 | == VariableKind::Ty(TyVariableKind::General) => | |
3dfed10e XL |
479 | { |
480 | true | |
481 | } | |
29967ef6 | 482 | TyKind::InferenceVar(_, TyVariableKind::General) => true, |
f9f354fc XL |
483 | _ => false, |
484 | } | |
485 | } | |
486 | ||
f035d41b | 487 | /// Returns true if this is an `Alias`. |
a2a8927a | 488 | pub fn is_alias(&self, interner: I) -> bool { |
29967ef6 XL |
489 | match self.kind(interner) { |
490 | TyKind::Alias(..) => true, | |
f9f354fc XL |
491 | _ => false, |
492 | } | |
493 | } | |
494 | ||
f035d41b | 495 | /// Returns true if this is an `IntTy` or `UintTy`. |
a2a8927a | 496 | pub fn is_integer(&self, interner: I) -> bool { |
29967ef6 XL |
497 | match self.kind(interner) { |
498 | TyKind::Scalar(Scalar::Int(_)) | TyKind::Scalar(Scalar::Uint(_)) => true, | |
f035d41b XL |
499 | _ => false, |
500 | } | |
501 | } | |
502 | ||
503 | /// Returns true if this is a `FloatTy`. | |
a2a8927a | 504 | pub fn is_float(&self, interner: I) -> bool { |
29967ef6 XL |
505 | match self.kind(interner) { |
506 | TyKind::Scalar(Scalar::Float(_)) => true, | |
f035d41b XL |
507 | _ => false, |
508 | } | |
509 | } | |
510 | ||
1b1a35ee | 511 | /// Returns `Some(adt_id)` if this is an ADT, `None` otherwise |
a2a8927a | 512 | pub fn adt_id(&self, interner: I) -> Option<AdtId<I>> { |
29967ef6 XL |
513 | match self.kind(interner) { |
514 | TyKind::Adt(adt_id, _) => Some(*adt_id), | |
1b1a35ee XL |
515 | _ => None, |
516 | } | |
517 | } | |
518 | ||
f9f354fc XL |
519 | /// True if this type contains "bound" types/lifetimes, and hence |
520 | /// needs to be shifted across binders. This is a very inefficient | |
521 | /// check, intended only for debug assertions, because I am lazy. | |
a2a8927a | 522 | pub fn needs_shift(&self, interner: I) -> bool { |
f9f354fc XL |
523 | self.has_free_vars(interner) |
524 | } | |
525 | } | |
526 | ||
29967ef6 XL |
527 | /// Contains the data for a Ty |
528 | #[derive(Clone, PartialEq, Eq, Hash, HasInterner)] | |
529 | pub struct TyData<I: Interner> { | |
530 | /// The kind | |
531 | pub kind: TyKind<I>, | |
5869c6ff XL |
532 | /// Type flags |
533 | pub flags: TypeFlags, | |
534 | } | |
535 | ||
536 | bitflags! { | |
537 | /// Contains flags indicating various properties of a Ty | |
538 | pub struct TypeFlags : u16 { | |
539 | /// Does the type contain an InferenceVar | |
540 | const HAS_TY_INFER = 1; | |
541 | /// Does the type contain a lifetime with an InferenceVar | |
542 | const HAS_RE_INFER = 1 << 1; | |
543 | /// Does the type contain a ConstValue with an InferenceVar | |
544 | const HAS_CT_INFER = 1 << 2; | |
545 | /// Does the type contain a Placeholder TyKind | |
546 | const HAS_TY_PLACEHOLDER = 1 << 3; | |
547 | /// Does the type contain a lifetime with a Placeholder | |
548 | const HAS_RE_PLACEHOLDER = 1 << 4; | |
549 | /// Does the type contain a ConstValue Placeholder | |
550 | const HAS_CT_PLACEHOLDER = 1 << 5; | |
551 | /// True when the type has free lifetimes related to a local context | |
552 | const HAS_FREE_LOCAL_REGIONS = 1 << 6; | |
553 | /// Does the type contain a projection of an associated type | |
554 | const HAS_TY_PROJECTION = 1 << 7; | |
555 | /// Does the type contain an opaque type | |
556 | const HAS_TY_OPAQUE = 1 << 8; | |
557 | /// Does the type contain an unevaluated const projection | |
558 | const HAS_CT_PROJECTION = 1 << 9; | |
559 | /// Does the type contain an error | |
560 | const HAS_ERROR = 1 << 10; | |
561 | /// Does the type contain any free lifetimes | |
562 | const HAS_FREE_REGIONS = 1 << 11; | |
563 | /// True when the type contains lifetimes that will be substituted when function is called | |
564 | const HAS_RE_LATE_BOUND = 1 << 12; | |
565 | /// True when the type contains an erased lifetime | |
566 | const HAS_RE_ERASED = 1 << 13; | |
567 | /// Does the type contain placeholders or inference variables that could be replaced later | |
568 | const STILL_FURTHER_SPECIALIZABLE = 1 << 14; | |
569 | ||
570 | /// True when the type contains free names local to a particular context | |
571 | const HAS_FREE_LOCAL_NAMES = TypeFlags::HAS_TY_INFER.bits | |
572 | | TypeFlags::HAS_CT_INFER.bits | |
573 | | TypeFlags::HAS_TY_PLACEHOLDER.bits | |
574 | | TypeFlags::HAS_CT_PLACEHOLDER.bits | |
575 | | TypeFlags::HAS_FREE_LOCAL_REGIONS.bits; | |
576 | ||
577 | /// Does the type contain any form of projection | |
578 | const HAS_PROJECTION = TypeFlags::HAS_TY_PROJECTION.bits | |
579 | | TypeFlags::HAS_TY_OPAQUE.bits | |
580 | | TypeFlags::HAS_CT_PROJECTION.bits; | |
581 | } | |
29967ef6 | 582 | } |
f035d41b | 583 | /// Type data, which holds the actual type information. |
f9f354fc | 584 | #[derive(Clone, PartialEq, Eq, Hash, HasInterner)] |
29967ef6 XL |
585 | pub enum TyKind<I: Interner> { |
586 | /// Abstract data types, i.e., structs, unions, or enumerations. | |
587 | /// For example, a type like `Vec<T>`. | |
588 | Adt(AdtId<I>, Substitution<I>), | |
589 | ||
590 | /// an associated type like `Iterator::Item`; see `AssociatedType` for details | |
591 | AssociatedType(AssocTypeId<I>, Substitution<I>), | |
592 | ||
593 | /// a scalar type like `bool` or `u32` | |
594 | Scalar(Scalar), | |
595 | ||
596 | /// a tuple of the given arity | |
597 | Tuple(usize, Substitution<I>), | |
598 | ||
599 | /// an array type like `[T; N]` | |
600 | Array(Ty<I>, Const<I>), | |
601 | ||
602 | /// a slice type like `[T]` | |
603 | Slice(Ty<I>), | |
604 | ||
605 | /// a raw pointer type like `*const T` or `*mut T` | |
606 | Raw(Mutability, Ty<I>), | |
607 | ||
608 | /// a reference type like `&T` or `&mut T` | |
609 | Ref(Mutability, Lifetime<I>, Ty<I>), | |
610 | ||
611 | /// a placeholder for opaque types like `impl Trait` | |
612 | OpaqueType(OpaqueTyId<I>, Substitution<I>), | |
613 | ||
614 | /// a function definition | |
615 | FnDef(FnDefId<I>, Substitution<I>), | |
616 | ||
617 | /// the string primitive type | |
618 | Str, | |
619 | ||
620 | /// the never type `!` | |
621 | Never, | |
622 | ||
623 | /// A closure. | |
624 | Closure(ClosureId<I>, Substitution<I>), | |
625 | ||
626 | /// A generator. | |
627 | Generator(GeneratorId<I>, Substitution<I>), | |
628 | ||
629 | /// A generator witness. | |
630 | GeneratorWitness(GeneratorId<I>, Substitution<I>), | |
631 | ||
632 | /// foreign types | |
633 | Foreign(ForeignDefId<I>), | |
634 | ||
635 | /// This can be used to represent an error, e.g. during name resolution of a type. | |
636 | /// Chalk itself will not produce this, just pass it through when given. | |
637 | Error, | |
f9f354fc | 638 | |
3dfed10e | 639 | /// instantiated from a universally quantified type, e.g., from |
f9f354fc XL |
640 | /// `forall<T> { .. }`. Stands in as a representative of "some |
641 | /// unknown type". | |
642 | Placeholder(PlaceholderIndex), | |
643 | ||
644 | /// A "dyn" type is a trait object type created via the "dyn Trait" syntax. | |
645 | /// In the chalk parser, the traits that the object represents is parsed as | |
646 | /// a QuantifiedInlineBound, and is then changed to a list of where clauses | |
647 | /// during lowering. | |
648 | /// | |
649 | /// See the `Opaque` variant for a discussion about the use of | |
650 | /// binders here. | |
651 | Dyn(DynTy<I>), | |
652 | ||
653 | /// An "alias" type represents some form of type alias, such as: | |
654 | /// - An associated type projection like `<T as Iterator>::Item` | |
655 | /// - `impl Trait` types | |
656 | /// - Named type aliases like `type Foo<X> = Vec<X>` | |
657 | Alias(AliasTy<I>), | |
658 | ||
659 | /// A function type such as `for<'a> fn(&'a u32)`. | |
660 | /// Note that "higher-ranked" types (starting with `for<>`) are either | |
661 | /// function types or dyn types, and do not appear otherwise in Rust | |
662 | /// surface syntax. | |
3dfed10e | 663 | Function(FnPointer<I>), |
f9f354fc XL |
664 | |
665 | /// References the binding at the given depth. The index is a [de | |
666 | /// Bruijn index], so it counts back through the in-scope binders. | |
667 | BoundVar(BoundVar), | |
668 | ||
669 | /// Inference variable defined in the current inference context. | |
29967ef6 | 670 | InferenceVar(InferenceVar, TyVariableKind), |
f035d41b XL |
671 | } |
672 | ||
29967ef6 | 673 | impl<I: Interner> Copy for TyKind<I> |
f035d41b XL |
674 | where |
675 | I::InternedLifetime: Copy, | |
676 | I::InternedSubstitution: Copy, | |
677 | I::InternedVariableKinds: Copy, | |
678 | I::InternedQuantifiedWhereClauses: Copy, | |
29967ef6 XL |
679 | I::InternedType: Copy, |
680 | I::InternedConst: Copy, | |
f035d41b | 681 | { |
f9f354fc XL |
682 | } |
683 | ||
29967ef6 | 684 | impl<I: Interner> TyKind<I> { |
f035d41b | 685 | /// Casts the type data to a type. |
a2a8927a | 686 | pub fn intern(self, interner: I) -> Ty<I> { |
f9f354fc XL |
687 | Ty::new(interner, self) |
688 | } | |
a2a8927a XL |
689 | |
690 | /// Compute type flags for a TyKind | |
691 | pub fn compute_flags(&self, interner: I) -> TypeFlags { | |
692 | match self { | |
693 | TyKind::Adt(_, substitution) | |
694 | | TyKind::AssociatedType(_, substitution) | |
695 | | TyKind::Tuple(_, substitution) | |
696 | | TyKind::Closure(_, substitution) | |
697 | | TyKind::Generator(_, substitution) | |
698 | | TyKind::GeneratorWitness(_, substitution) | |
699 | | TyKind::FnDef(_, substitution) | |
700 | | TyKind::OpaqueType(_, substitution) => substitution.compute_flags(interner), | |
701 | TyKind::Scalar(_) | TyKind::Str | TyKind::Never | TyKind::Foreign(_) => { | |
702 | TypeFlags::empty() | |
703 | } | |
704 | TyKind::Error => TypeFlags::HAS_ERROR, | |
705 | TyKind::Slice(ty) | TyKind::Raw(_, ty) => ty.data(interner).flags, | |
706 | TyKind::Ref(_, lifetime, ty) => { | |
707 | lifetime.compute_flags(interner) | ty.data(interner).flags | |
708 | } | |
709 | TyKind::Array(ty, const_ty) => { | |
710 | let flags = ty.data(interner).flags; | |
711 | let const_data = const_ty.data(interner); | |
712 | flags | |
713 | | const_data.ty.data(interner).flags | |
714 | | match const_data.value { | |
715 | ConstValue::BoundVar(_) | ConstValue::Concrete(_) => TypeFlags::empty(), | |
716 | ConstValue::InferenceVar(_) => { | |
717 | TypeFlags::HAS_CT_INFER | TypeFlags::STILL_FURTHER_SPECIALIZABLE | |
718 | } | |
719 | ConstValue::Placeholder(_) => { | |
720 | TypeFlags::HAS_CT_PLACEHOLDER | TypeFlags::STILL_FURTHER_SPECIALIZABLE | |
721 | } | |
722 | } | |
723 | } | |
724 | TyKind::Placeholder(_) => TypeFlags::HAS_TY_PLACEHOLDER, | |
725 | TyKind::Dyn(dyn_ty) => { | |
726 | let lifetime_flags = dyn_ty.lifetime.compute_flags(interner); | |
727 | let mut dyn_flags = TypeFlags::empty(); | |
728 | for var_kind in dyn_ty.bounds.skip_binders().iter(interner) { | |
729 | match &(var_kind.skip_binders()) { | |
730 | WhereClause::Implemented(trait_ref) => { | |
731 | dyn_flags |= trait_ref.substitution.compute_flags(interner) | |
732 | } | |
733 | WhereClause::AliasEq(alias_eq) => { | |
734 | dyn_flags |= alias_eq.alias.compute_flags(interner); | |
735 | dyn_flags |= alias_eq.ty.data(interner).flags; | |
736 | } | |
737 | WhereClause::LifetimeOutlives(lifetime_outlives) => { | |
738 | dyn_flags |= lifetime_outlives.a.compute_flags(interner) | |
739 | | lifetime_outlives.b.compute_flags(interner); | |
740 | } | |
741 | WhereClause::TypeOutlives(type_outlives) => { | |
742 | dyn_flags |= type_outlives.ty.data(interner).flags; | |
743 | dyn_flags |= type_outlives.lifetime.compute_flags(interner); | |
744 | } | |
745 | } | |
746 | } | |
747 | lifetime_flags | dyn_flags | |
748 | } | |
749 | TyKind::Alias(alias_ty) => alias_ty.compute_flags(interner), | |
750 | TyKind::BoundVar(_) => TypeFlags::empty(), | |
751 | TyKind::InferenceVar(_, _) => TypeFlags::HAS_TY_INFER, | |
752 | TyKind::Function(fn_pointer) => fn_pointer.substitution.0.compute_flags(interner), | |
753 | } | |
754 | } | |
f9f354fc XL |
755 | } |
756 | ||
757 | /// Identifies a particular bound variable within a binder. | |
758 | /// Variables are identified by the combination of a [`DebruijnIndex`], | |
759 | /// which identifies the *binder*, and an index within that binder. | |
760 | /// | |
761 | /// Consider this case: | |
762 | /// | |
763 | /// ```ignore | |
764 | /// forall<'a, 'b> { forall<'c, 'd> { ... } } | |
765 | /// ``` | |
766 | /// | |
767 | /// Within the `...` term: | |
768 | /// | |
769 | /// * the variable `'a` have a debruijn index of 1 and index 0 | |
770 | /// * the variable `'b` have a debruijn index of 1 and index 1 | |
771 | /// * the variable `'c` have a debruijn index of 0 and index 0 | |
772 | /// * the variable `'d` have a debruijn index of 0 and index 1 | |
773 | /// | |
774 | /// The variables `'a` and `'b` both have debruijn index of 1 because, | |
775 | /// counting out, they are the 2nd binder enclosing `...`. The indices | |
776 | /// identify the location *within* that binder. | |
777 | /// | |
778 | /// The variables `'c` and `'d` both have debruijn index of 0 because | |
779 | /// they appear in the *innermost* binder enclosing the `...`. The | |
780 | /// indices identify the location *within* that binder. | |
781 | #[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)] | |
782 | pub struct BoundVar { | |
f035d41b | 783 | /// Debruijn index, which identifies the binder. |
f9f354fc | 784 | pub debruijn: DebruijnIndex, |
f035d41b | 785 | /// Index within the binder. |
f9f354fc XL |
786 | pub index: usize, |
787 | } | |
788 | ||
789 | impl BoundVar { | |
f035d41b | 790 | /// Creates a new bound variable. |
f9f354fc XL |
791 | pub fn new(debruijn: DebruijnIndex, index: usize) -> Self { |
792 | Self { debruijn, index } | |
793 | } | |
794 | ||
f035d41b | 795 | /// Casts the bound variable to a type. |
a2a8927a | 796 | pub fn to_ty<I: Interner>(self, interner: I) -> Ty<I> { |
29967ef6 | 797 | TyKind::<I>::BoundVar(self).intern(interner) |
f9f354fc XL |
798 | } |
799 | ||
f035d41b | 800 | /// Wrap the bound variable in a lifetime. |
a2a8927a | 801 | pub fn to_lifetime<I: Interner>(self, interner: I) -> Lifetime<I> { |
f9f354fc XL |
802 | LifetimeData::<I>::BoundVar(self).intern(interner) |
803 | } | |
804 | ||
f035d41b | 805 | /// Wraps the bound variable in a constant. |
a2a8927a | 806 | pub fn to_const<I: Interner>(self, interner: I, ty: Ty<I>) -> Const<I> { |
f035d41b XL |
807 | ConstData { |
808 | ty, | |
809 | value: ConstValue::<I>::BoundVar(self), | |
810 | } | |
811 | .intern(interner) | |
812 | } | |
813 | ||
f9f354fc XL |
814 | /// True if this variable is bound within the `amount` innermost binders. |
815 | pub fn bound_within(self, outer_binder: DebruijnIndex) -> bool { | |
816 | self.debruijn.within(outer_binder) | |
817 | } | |
818 | ||
819 | /// Adjusts the debruijn index (see [`DebruijnIndex::shifted_in`]). | |
820 | #[must_use] | |
821 | pub fn shifted_in(self) -> Self { | |
822 | BoundVar::new(self.debruijn.shifted_in(), self.index) | |
823 | } | |
824 | ||
825 | /// Adjusts the debruijn index (see [`DebruijnIndex::shifted_in`]). | |
826 | #[must_use] | |
827 | pub fn shifted_in_from(self, outer_binder: DebruijnIndex) -> Self { | |
828 | BoundVar::new(self.debruijn.shifted_in_from(outer_binder), self.index) | |
829 | } | |
830 | ||
831 | /// Adjusts the debruijn index (see [`DebruijnIndex::shifted_in`]). | |
832 | #[must_use] | |
833 | pub fn shifted_out(self) -> Option<Self> { | |
834 | self.debruijn | |
835 | .shifted_out() | |
836 | .map(|db| BoundVar::new(db, self.index)) | |
837 | } | |
838 | ||
839 | /// Adjusts the debruijn index (see [`DebruijnIndex::shifted_in`]). | |
840 | #[must_use] | |
841 | pub fn shifted_out_to(self, outer_binder: DebruijnIndex) -> Option<Self> { | |
842 | self.debruijn | |
843 | .shifted_out_to(outer_binder) | |
844 | .map(|db| BoundVar::new(db, self.index)) | |
845 | } | |
846 | ||
847 | /// Return the index of the bound variable, but only if it is bound | |
848 | /// at the innermost binder. Otherwise, returns `None`. | |
849 | pub fn index_if_innermost(self) -> Option<usize> { | |
850 | self.index_if_bound_at(DebruijnIndex::INNERMOST) | |
851 | } | |
852 | ||
853 | /// Return the index of the bound variable, but only if it is bound | |
854 | /// at the innermost binder. Otherwise, returns `None`. | |
855 | pub fn index_if_bound_at(self, debruijn: DebruijnIndex) -> Option<usize> { | |
856 | if self.debruijn == debruijn { | |
857 | Some(self.index) | |
858 | } else { | |
859 | None | |
860 | } | |
861 | } | |
862 | } | |
863 | ||
864 | /// References the binder at the given depth. The index is a [de | |
865 | /// Bruijn index], so it counts back through the in-scope binders, | |
866 | /// with 0 being the innermost binder. This is used in impls and | |
867 | /// the like. For example, if we had a rule like `for<T> { (T: | |
868 | /// Clone) :- (T: Copy) }`, then `T` would be represented as a | |
869 | /// `BoundVar(0)` (as the `for` is the innermost binder). | |
870 | /// | |
871 | /// [de Bruijn index]: https://en.wikipedia.org/wiki/De_Bruijn_index | |
872 | #[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)] | |
873 | pub struct DebruijnIndex { | |
874 | depth: u32, | |
875 | } | |
876 | ||
877 | impl DebruijnIndex { | |
f035d41b | 878 | /// Innermost index. |
f9f354fc | 879 | pub const INNERMOST: DebruijnIndex = DebruijnIndex { depth: 0 }; |
f035d41b | 880 | /// One level higher than the innermost index. |
f9f354fc XL |
881 | pub const ONE: DebruijnIndex = DebruijnIndex { depth: 1 }; |
882 | ||
f035d41b | 883 | /// Creates a new de Bruijn index with a given depth. |
f9f354fc XL |
884 | pub fn new(depth: u32) -> Self { |
885 | DebruijnIndex { depth } | |
886 | } | |
887 | ||
f035d41b XL |
888 | /// Depth of the De Bruijn index, counting from 0 starting with |
889 | /// the innermost binder. | |
f9f354fc XL |
890 | pub fn depth(self) -> u32 { |
891 | self.depth | |
892 | } | |
893 | ||
894 | /// True if the binder identified by this index is within the | |
895 | /// binder identified by the index `outer_binder`. | |
896 | /// | |
897 | /// # Example | |
898 | /// | |
899 | /// Imagine you have the following binders in scope | |
900 | /// | |
901 | /// ```ignore | |
902 | /// forall<a> forall<b> forall<c> | |
903 | /// ``` | |
904 | /// | |
905 | /// then the Debruijn index for `c` would be `0`, the index for | |
906 | /// `b` would be 1, and so on. Now consider the following calls: | |
907 | /// | |
908 | /// * `c.within(a) = true` | |
909 | /// * `b.within(a) = true` | |
910 | /// * `a.within(a) = false` | |
911 | /// * `a.within(c) = false` | |
912 | pub fn within(self, outer_binder: DebruijnIndex) -> bool { | |
913 | self < outer_binder | |
914 | } | |
915 | ||
916 | /// Returns the resulting index when this value is moved into | |
917 | /// through one binder. | |
918 | #[must_use] | |
919 | pub fn shifted_in(self) -> DebruijnIndex { | |
920 | self.shifted_in_from(DebruijnIndex::ONE) | |
921 | } | |
922 | ||
923 | /// Update this index in place by shifting it "in" through | |
924 | /// `amount` number of binders. | |
925 | pub fn shift_in(&mut self) { | |
926 | *self = self.shifted_in(); | |
927 | } | |
928 | ||
929 | /// Adds `outer_binder` levels to the `self` index. Intuitively, this | |
930 | /// shifts the `self` index, which was valid at the outer binder, | |
931 | /// so that it is valid at the innermost binder. | |
932 | /// | |
933 | /// Example: Assume that the following binders are in scope: | |
934 | /// | |
935 | /// ```ignore | |
936 | /// for<A> for<B> for<C> for<D> | |
937 | /// ^ outer binder | |
938 | /// ``` | |
939 | /// | |
940 | /// Assume further that the `outer_binder` argument is 2, | |
941 | /// which means that it is referring to the `for<B>` binder | |
942 | /// (since `D` would be the innermost binder). | |
943 | /// | |
944 | /// This means that `self` is relative to the binder `B` -- so | |
945 | /// if `self` is 0 (`INNERMOST`), then it refers to `B`, | |
946 | /// and if `self` is 1, then it refers to `A`. | |
947 | /// | |
948 | /// We will return as follows: | |
949 | /// | |
950 | /// * `0.shifted_in_from(2) = 2` -- i.e., `B`, when shifted in to the binding level `D`, has index 2 | |
951 | /// * `1.shifted_in_from(2) = 3` -- i.e., `A`, when shifted in to the binding level `D`, has index 3 | |
952 | /// * `2.shifted_in_from(1) = 3` -- here, we changed the `outer_binder` to refer to `C`. | |
953 | /// Therefore `2` (relative to `C`) refers to `A`, so the result is still 3 (since `A`, relative to the | |
954 | /// innermost binder, has index 3). | |
955 | #[must_use] | |
956 | pub fn shifted_in_from(self, outer_binder: DebruijnIndex) -> DebruijnIndex { | |
957 | DebruijnIndex::new(self.depth() + outer_binder.depth()) | |
958 | } | |
959 | ||
960 | /// Returns the resulting index when this value is moved out from | |
961 | /// `amount` number of new binders. | |
962 | #[must_use] | |
963 | pub fn shifted_out(self) -> Option<DebruijnIndex> { | |
964 | self.shifted_out_to(DebruijnIndex::ONE) | |
965 | } | |
966 | ||
967 | /// Update in place by shifting out from `amount` binders. | |
968 | pub fn shift_out(&mut self) { | |
969 | *self = self.shifted_out().unwrap(); | |
970 | } | |
971 | ||
972 | /// Subtracts `outer_binder` levels from the `self` index. Intuitively, this | |
973 | /// shifts the `self` index, which was valid at the innermost | |
974 | /// binder, to one that is valid at the binder `outer_binder`. | |
975 | /// | |
976 | /// This will return `None` if the `self` index is internal to the | |
977 | /// outer binder (i.e., if `self < outer_binder`). | |
978 | /// | |
979 | /// Example: Assume that the following binders are in scope: | |
980 | /// | |
981 | /// ```ignore | |
982 | /// for<A> for<B> for<C> for<D> | |
983 | /// ^ outer binder | |
984 | /// ``` | |
985 | /// | |
986 | /// Assume further that the `outer_binder` argument is 2, | |
987 | /// which means that it is referring to the `for<B>` binder | |
988 | /// (since `D` would be the innermost binder). | |
989 | /// | |
990 | /// This means that the result is relative to the binder `B` -- so | |
991 | /// if `self` is 0 (`INNERMOST`), then it refers to `B`, | |
992 | /// and if `self` is 1, then it refers to `A`. | |
993 | /// | |
994 | /// We will return as follows: | |
995 | /// | |
996 | /// * `1.shifted_out_to(2) = None` -- i.e., the binder for `C` can't be named from the binding level `B` | |
997 | /// * `3.shifted_out_to(2) = Some(1)` -- i.e., `A`, when shifted out to the binding level `B`, has index 1 | |
998 | pub fn shifted_out_to(self, outer_binder: DebruijnIndex) -> Option<DebruijnIndex> { | |
999 | if self.within(outer_binder) { | |
1000 | None | |
1001 | } else { | |
1002 | Some(DebruijnIndex::new(self.depth() - outer_binder.depth())) | |
1003 | } | |
1004 | } | |
1005 | } | |
1006 | ||
f035d41b XL |
1007 | /// A "DynTy" represents a trait object (`dyn Trait`). Trait objects |
1008 | /// are conceptually very related to an "existential type" of the form | |
1009 | /// `exists<T> { T: Trait }` (another example of such type is `impl Trait`). | |
1010 | /// `DynTy` represents the bounds on that type. | |
f9f354fc | 1011 | /// |
f035d41b XL |
1012 | /// The "bounds" here represents the unknown self type. So, a type like |
1013 | /// `dyn for<'a> Fn(&'a u32)` would be represented with two-levels of | |
f9f354fc XL |
1014 | /// binder, as "depicted" here: |
1015 | /// | |
1016 | /// ```notrust | |
1017 | /// exists<type> { | |
1018 | /// vec![ | |
1019 | /// // A QuantifiedWhereClause: | |
f035d41b | 1020 | /// forall<region> { ^1.0: Fn(&^0.0 u32) } |
f9f354fc XL |
1021 | /// ] |
1022 | /// } | |
1023 | /// ``` | |
1024 | /// | |
1025 | /// The outer `exists<type>` binder indicates that there exists | |
1026 | /// some type that meets the criteria within, but that type is not | |
f035d41b | 1027 | /// known. It is referenced within the type using `^1.0`, indicating |
f9f354fc XL |
1028 | /// a bound type with debruijn index 1 (i.e., skipping through one |
1029 | /// level of binder). | |
5869c6ff | 1030 | #[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner)] |
f9f354fc | 1031 | pub struct DynTy<I: Interner> { |
f035d41b | 1032 | /// The unknown self type. |
f9f354fc | 1033 | pub bounds: Binders<QuantifiedWhereClauses<I>>, |
f035d41b XL |
1034 | /// Lifetime of the `DynTy`. |
1035 | pub lifetime: Lifetime<I>, | |
f9f354fc XL |
1036 | } |
1037 | ||
f035d41b XL |
1038 | impl<I: Interner> Copy for DynTy<I> |
1039 | where | |
1040 | I::InternedLifetime: Copy, | |
1041 | I::InternedQuantifiedWhereClauses: Copy, | |
1042 | I::InternedVariableKinds: Copy, | |
1043 | { | |
1044 | } | |
1045 | ||
1046 | /// A type, lifetime or constant whose value is being inferred. | |
f9f354fc XL |
1047 | #[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)] |
1048 | pub struct InferenceVar { | |
1049 | index: u32, | |
1050 | } | |
1051 | ||
1052 | impl From<u32> for InferenceVar { | |
1053 | fn from(index: u32) -> InferenceVar { | |
1054 | InferenceVar { index } | |
1055 | } | |
1056 | } | |
1057 | ||
1058 | impl InferenceVar { | |
f035d41b | 1059 | /// Gets the underlying index value. |
f9f354fc XL |
1060 | pub fn index(self) -> u32 { |
1061 | self.index | |
1062 | } | |
1063 | ||
f035d41b | 1064 | /// Wraps the inference variable in a type. |
a2a8927a | 1065 | pub fn to_ty<I: Interner>(self, interner: I, kind: TyVariableKind) -> Ty<I> { |
29967ef6 | 1066 | TyKind::<I>::InferenceVar(self, kind).intern(interner) |
f9f354fc XL |
1067 | } |
1068 | ||
f035d41b | 1069 | /// Wraps the inference variable in a lifetime. |
a2a8927a | 1070 | pub fn to_lifetime<I: Interner>(self, interner: I) -> Lifetime<I> { |
f9f354fc XL |
1071 | LifetimeData::<I>::InferenceVar(self).intern(interner) |
1072 | } | |
f035d41b XL |
1073 | |
1074 | /// Wraps the inference variable in a constant. | |
a2a8927a | 1075 | pub fn to_const<I: Interner>(self, interner: I, ty: Ty<I>) -> Const<I> { |
f035d41b XL |
1076 | ConstData { |
1077 | ty, | |
1078 | value: ConstValue::<I>::InferenceVar(self), | |
1079 | } | |
1080 | .intern(interner) | |
1081 | } | |
f9f354fc XL |
1082 | } |
1083 | ||
1b1a35ee XL |
1084 | /// A function signature. |
1085 | #[derive(Clone, Copy, PartialEq, Eq, Hash, HasInterner, Debug)] | |
1086 | #[allow(missing_docs)] | |
1087 | pub struct FnSig<I: Interner> { | |
1088 | pub abi: I::FnAbi, | |
1089 | pub safety: Safety, | |
1090 | pub variadic: bool, | |
1091 | } | |
5869c6ff XL |
1092 | /// A wrapper for the substs on a Fn. |
1093 | #[derive(Clone, PartialEq, Eq, Hash, HasInterner, Fold, Visit)] | |
1094 | pub struct FnSubst<I: Interner>(pub Substitution<I>); | |
1095 | ||
1096 | impl<I: Interner> Copy for FnSubst<I> where I::InternedSubstitution: Copy {} | |
1b1a35ee | 1097 | |
f9f354fc XL |
1098 | /// for<'a...'z> X -- all binders are instantiated at once, |
1099 | /// and we use deBruijn indices within `self.ty` | |
1100 | #[derive(Clone, PartialEq, Eq, Hash, HasInterner)] | |
f035d41b | 1101 | #[allow(missing_docs)] |
3dfed10e | 1102 | pub struct FnPointer<I: Interner> { |
f9f354fc | 1103 | pub num_binders: usize, |
1b1a35ee | 1104 | pub sig: FnSig<I>, |
5869c6ff | 1105 | pub substitution: FnSubst<I>, |
f9f354fc XL |
1106 | } |
1107 | ||
3dfed10e | 1108 | impl<I: Interner> Copy for FnPointer<I> where I::InternedSubstitution: Copy {} |
f035d41b | 1109 | |
5869c6ff XL |
1110 | impl<I: Interner> FnPointer<I> { |
1111 | /// Represent the current `Fn` as if it was wrapped in `Binders` | |
a2a8927a | 1112 | pub fn into_binders(self, interner: I) -> Binders<FnSubst<I>> { |
5869c6ff XL |
1113 | Binders::new( |
1114 | VariableKinds::from_iter( | |
1115 | interner, | |
1116 | (0..self.num_binders).map(|_| VariableKind::Lifetime), | |
1117 | ), | |
1118 | self.substitution, | |
1119 | ) | |
1120 | } | |
1121 | ||
1122 | /// Represent the current `Fn` as if it was wrapped in `Binders` | |
a2a8927a | 1123 | pub fn as_binders(&self, interner: I) -> Binders<&FnSubst<I>> { |
5869c6ff XL |
1124 | Binders::new( |
1125 | VariableKinds::from_iter( | |
1126 | interner, | |
1127 | (0..self.num_binders).map(|_| VariableKind::Lifetime), | |
1128 | ), | |
1129 | &self.substitution, | |
1130 | ) | |
1131 | } | |
1132 | } | |
1133 | ||
f035d41b XL |
1134 | /// Constants. |
1135 | #[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord, HasInterner)] | |
1136 | pub struct Const<I: Interner> { | |
1137 | interned: I::InternedConst, | |
1138 | } | |
1139 | ||
1140 | impl<I: Interner> Const<I> { | |
1141 | /// Create a `Const` using something that can be cast to const data. | |
a2a8927a | 1142 | pub fn new(interner: I, data: impl CastTo<ConstData<I>>) -> Self { |
f035d41b XL |
1143 | Const { |
1144 | interned: I::intern_const(interner, data.cast(interner)), | |
1145 | } | |
1146 | } | |
1147 | ||
1148 | /// Gets the interned constant. | |
1149 | pub fn interned(&self) -> &I::InternedConst { | |
1150 | &self.interned | |
1151 | } | |
1152 | ||
1153 | /// Gets the constant data from the interner. | |
a2a8927a | 1154 | pub fn data(&self, interner: I) -> &ConstData<I> { |
f035d41b XL |
1155 | I::const_data(interner, &self.interned) |
1156 | } | |
1157 | ||
1158 | /// If this is a `ConstData::BoundVar(d)`, returns `Some(d)` else `None`. | |
a2a8927a | 1159 | pub fn bound_var(&self, interner: I) -> Option<BoundVar> { |
f035d41b XL |
1160 | if let ConstValue::BoundVar(bv) = &self.data(interner).value { |
1161 | Some(*bv) | |
1162 | } else { | |
1163 | None | |
1164 | } | |
1165 | } | |
1166 | ||
1167 | /// If this is a `ConstData::InferenceVar(d)`, returns `Some(d)` else `None`. | |
a2a8927a | 1168 | pub fn inference_var(&self, interner: I) -> Option<InferenceVar> { |
f035d41b XL |
1169 | if let ConstValue::InferenceVar(iv) = &self.data(interner).value { |
1170 | Some(*iv) | |
1171 | } else { | |
1172 | None | |
1173 | } | |
1174 | } | |
1175 | ||
1176 | /// True if this const is a "bound" const, and hence | |
1177 | /// needs to be shifted across binders. Meant for debug assertions. | |
a2a8927a | 1178 | pub fn needs_shift(&self, interner: I) -> bool { |
f035d41b XL |
1179 | match &self.data(interner).value { |
1180 | ConstValue::BoundVar(_) => true, | |
1181 | ConstValue::InferenceVar(_) => false, | |
1182 | ConstValue::Placeholder(_) => false, | |
1183 | ConstValue::Concrete(_) => false, | |
1184 | } | |
1185 | } | |
1186 | } | |
1187 | ||
1188 | /// Constant data, containing the constant's type and value. | |
1189 | #[derive(Clone, PartialEq, Eq, Hash, HasInterner)] | |
1190 | pub struct ConstData<I: Interner> { | |
1191 | /// Type that holds the constant. | |
1192 | pub ty: Ty<I>, | |
1193 | /// The value of the constant. | |
1194 | pub value: ConstValue<I>, | |
1195 | } | |
1196 | ||
1197 | /// A constant value, not necessarily concrete. | |
1198 | #[derive(Clone, PartialEq, Eq, Hash, HasInterner)] | |
1199 | pub enum ConstValue<I: Interner> { | |
1200 | /// Bound var (e.g. a parameter). | |
1201 | BoundVar(BoundVar), | |
1202 | /// Constant whose value is being inferred. | |
1203 | InferenceVar(InferenceVar), | |
1204 | /// Lifetime on some yet-unknown placeholder. | |
1205 | Placeholder(PlaceholderIndex), | |
1206 | /// Concrete constant value. | |
1207 | Concrete(ConcreteConst<I>), | |
1208 | } | |
1209 | ||
1210 | impl<I: Interner> Copy for ConstValue<I> where I::InternedConcreteConst: Copy {} | |
1211 | ||
1212 | impl<I: Interner> ConstData<I> { | |
1213 | /// Wraps the constant data in a `Const`. | |
a2a8927a | 1214 | pub fn intern(self, interner: I) -> Const<I> { |
f035d41b XL |
1215 | Const::new(interner, self) |
1216 | } | |
1217 | } | |
1218 | ||
1219 | /// Concrete constant, whose value is known (as opposed to | |
1220 | /// inferred constants and placeholders). | |
1221 | #[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord, HasInterner)] | |
1222 | pub struct ConcreteConst<I: Interner> { | |
1223 | /// The interned constant. | |
1224 | pub interned: I::InternedConcreteConst, | |
1225 | } | |
1226 | ||
1227 | impl<I: Interner> ConcreteConst<I> { | |
1228 | /// Checks whether two concrete constants are equal. | |
a2a8927a | 1229 | pub fn const_eq(&self, ty: &Ty<I>, other: &ConcreteConst<I>, interner: I) -> bool { |
f035d41b XL |
1230 | interner.const_eq(&ty.interned, &self.interned, &other.interned) |
1231 | } | |
1232 | } | |
1233 | ||
1234 | /// A Rust lifetime. | |
f9f354fc XL |
1235 | #[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord, HasInterner)] |
1236 | pub struct Lifetime<I: Interner> { | |
1237 | interned: I::InternedLifetime, | |
1238 | } | |
1239 | ||
1240 | impl<I: Interner> Lifetime<I> { | |
f035d41b XL |
1241 | /// Create a lifetime from lifetime data |
1242 | /// (or something that can be cast to lifetime data). | |
a2a8927a | 1243 | pub fn new(interner: I, data: impl CastTo<LifetimeData<I>>) -> Self { |
f9f354fc XL |
1244 | Lifetime { |
1245 | interned: I::intern_lifetime(interner, data.cast(interner)), | |
1246 | } | |
1247 | } | |
1248 | ||
f035d41b | 1249 | /// Gets the interned value. |
f9f354fc XL |
1250 | pub fn interned(&self) -> &I::InternedLifetime { |
1251 | &self.interned | |
1252 | } | |
1253 | ||
f035d41b | 1254 | /// Gets the lifetime data. |
a2a8927a | 1255 | pub fn data(&self, interner: I) -> &LifetimeData<I> { |
f9f354fc XL |
1256 | I::lifetime_data(interner, &self.interned) |
1257 | } | |
1258 | ||
f035d41b | 1259 | /// If this is a `Lifetime::BoundVar(d)`, returns `Some(d)` else `None`. |
a2a8927a | 1260 | pub fn bound_var(&self, interner: I) -> Option<BoundVar> { |
f035d41b XL |
1261 | if let LifetimeData::BoundVar(bv) = self.data(interner) { |
1262 | Some(*bv) | |
1263 | } else { | |
1264 | None | |
1265 | } | |
1266 | } | |
1267 | ||
f9f354fc | 1268 | /// If this is a `Lifetime::InferenceVar(d)`, returns `Some(d)` else `None`. |
a2a8927a | 1269 | pub fn inference_var(&self, interner: I) -> Option<InferenceVar> { |
f9f354fc XL |
1270 | if let LifetimeData::InferenceVar(depth) = self.data(interner) { |
1271 | Some(*depth) | |
1272 | } else { | |
1273 | None | |
1274 | } | |
1275 | } | |
1276 | ||
1277 | /// True if this lifetime is a "bound" lifetime, and hence | |
1278 | /// needs to be shifted across binders. Meant for debug assertions. | |
a2a8927a | 1279 | pub fn needs_shift(&self, interner: I) -> bool { |
f9f354fc XL |
1280 | match self.data(interner) { |
1281 | LifetimeData::BoundVar(_) => true, | |
1282 | LifetimeData::InferenceVar(_) => false, | |
1283 | LifetimeData::Placeholder(_) => false, | |
29967ef6 | 1284 | LifetimeData::Static => false, |
5869c6ff XL |
1285 | LifetimeData::Empty(_) => false, |
1286 | LifetimeData::Erased => false, | |
f9f354fc XL |
1287 | LifetimeData::Phantom(..) => unreachable!(), |
1288 | } | |
1289 | } | |
a2a8927a XL |
1290 | |
1291 | ///compute type flags for Lifetime | |
1292 | fn compute_flags(&self, interner: I) -> TypeFlags { | |
1293 | match self.data(interner) { | |
1294 | LifetimeData::InferenceVar(_) => { | |
1295 | TypeFlags::HAS_RE_INFER | |
1296 | | TypeFlags::HAS_FREE_LOCAL_REGIONS | |
1297 | | TypeFlags::HAS_FREE_REGIONS | |
1298 | } | |
1299 | LifetimeData::Placeholder(_) => { | |
1300 | TypeFlags::HAS_RE_PLACEHOLDER | |
1301 | | TypeFlags::HAS_FREE_LOCAL_REGIONS | |
1302 | | TypeFlags::HAS_FREE_REGIONS | |
1303 | } | |
1304 | LifetimeData::Static | LifetimeData::Empty(_) => TypeFlags::HAS_FREE_REGIONS, | |
1305 | LifetimeData::Phantom(_, _) => TypeFlags::empty(), | |
1306 | LifetimeData::BoundVar(_) => TypeFlags::HAS_RE_LATE_BOUND, | |
1307 | LifetimeData::Erased => TypeFlags::HAS_RE_ERASED, | |
1308 | } | |
1309 | } | |
f9f354fc XL |
1310 | } |
1311 | ||
f035d41b | 1312 | /// Lifetime data, including what kind of lifetime it is and what it points to. |
f9f354fc XL |
1313 | #[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord, HasInterner)] |
1314 | pub enum LifetimeData<I: Interner> { | |
29967ef6 | 1315 | /// See TyKind::BoundVar. |
f9f354fc | 1316 | BoundVar(BoundVar), |
f035d41b | 1317 | /// Lifetime whose value is being inferred. |
f9f354fc | 1318 | InferenceVar(InferenceVar), |
f035d41b | 1319 | /// Lifetime on some yet-unknown placeholder. |
f9f354fc | 1320 | Placeholder(PlaceholderIndex), |
29967ef6 XL |
1321 | /// Static lifetime |
1322 | Static, | |
5869c6ff XL |
1323 | /// An empty lifetime: a lifetime shorter than any other lifetime in a |
1324 | /// universe with a lesser or equal index. The universe only non-zero in | |
1325 | /// lexical region resolve in rustc, so chalk shouldn't ever see a non-zero | |
1326 | /// index. | |
1327 | Empty(UniverseIndex), | |
1328 | /// An erased lifetime, used by rustc to improve caching when we doesn't | |
1329 | /// care about lifetimes | |
1330 | Erased, | |
f035d41b | 1331 | /// Lifetime on phantom data. |
f9f354fc XL |
1332 | Phantom(Void, PhantomData<I>), |
1333 | } | |
1334 | ||
1335 | impl<I: Interner> LifetimeData<I> { | |
f035d41b | 1336 | /// Wrap the lifetime data in a lifetime. |
a2a8927a | 1337 | pub fn intern(self, interner: I) -> Lifetime<I> { |
f9f354fc XL |
1338 | Lifetime::new(interner, self) |
1339 | } | |
1340 | } | |
1341 | ||
1342 | /// Index of an universally quantified parameter in the environment. | |
1343 | /// Two indexes are required, the one of the universe itself | |
1344 | /// and the relative index inside the universe. | |
1345 | #[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] | |
1346 | pub struct PlaceholderIndex { | |
1347 | /// Index *of* the universe. | |
1348 | pub ui: UniverseIndex, | |
1349 | /// Index *in* the universe. | |
1350 | pub idx: usize, | |
1351 | } | |
1352 | ||
1353 | impl PlaceholderIndex { | |
f035d41b | 1354 | /// Wrap the placeholder instance in a lifetime. |
a2a8927a | 1355 | pub fn to_lifetime<I: Interner>(self, interner: I) -> Lifetime<I> { |
f9f354fc XL |
1356 | LifetimeData::<I>::Placeholder(self).intern(interner) |
1357 | } | |
1358 | ||
f035d41b | 1359 | /// Create an interned type. |
a2a8927a | 1360 | pub fn to_ty<I: Interner>(self, interner: I) -> Ty<I> { |
29967ef6 | 1361 | TyKind::Placeholder(self).intern(interner) |
f035d41b XL |
1362 | } |
1363 | ||
1364 | /// Wrap the placeholder index in a constant. | |
a2a8927a | 1365 | pub fn to_const<I: Interner>(self, interner: I, ty: Ty<I>) -> Const<I> { |
f035d41b XL |
1366 | ConstData { |
1367 | ty, | |
1368 | value: ConstValue::Placeholder(self), | |
1369 | } | |
1370 | .intern(interner) | |
f9f354fc XL |
1371 | } |
1372 | } | |
f035d41b XL |
1373 | /// Represents some extra knowledge we may have about the type variable. |
1374 | /// ```ignore | |
1375 | /// let x: &[u32]; | |
1376 | /// let i = 1; | |
1377 | /// x[i] | |
1378 | /// ``` | |
1379 | /// In this example, `i` is known to be some type of integer. We can infer that | |
1380 | /// it is `usize` because that is the only integer type that slices have an | |
29967ef6 | 1381 | /// `Index` impl for. `i` would have a `TyVariableKind` of `Integer` to guide the |
f035d41b XL |
1382 | /// inference process. |
1383 | #[derive(Copy, Clone, Debug, PartialEq, Eq, Hash)] | |
1384 | #[allow(missing_docs)] | |
29967ef6 | 1385 | pub enum TyVariableKind { |
f035d41b XL |
1386 | General, |
1387 | Integer, | |
1388 | Float, | |
1389 | } | |
1390 | ||
1391 | /// The "kind" of variable. Type, lifetime or constant. | |
1392 | #[derive(Clone, PartialEq, Eq, Hash)] | |
1393 | #[allow(missing_docs)] | |
1394 | pub enum VariableKind<I: Interner> { | |
29967ef6 | 1395 | Ty(TyVariableKind), |
f035d41b XL |
1396 | Lifetime, |
1397 | Const(Ty<I>), | |
f9f354fc XL |
1398 | } |
1399 | ||
3dfed10e XL |
1400 | impl<I: Interner> interner::HasInterner for VariableKind<I> { |
1401 | type Interner = I; | |
1402 | } | |
1403 | ||
f035d41b XL |
1404 | impl<I: Interner> Copy for VariableKind<I> where I::InternedType: Copy {} |
1405 | ||
1406 | impl<I: Interner> VariableKind<I> { | |
a2a8927a | 1407 | fn to_bound_variable(&self, interner: I, bound_var: BoundVar) -> GenericArg<I> { |
f9f354fc | 1408 | match self { |
f035d41b | 1409 | VariableKind::Ty(_) => { |
29967ef6 | 1410 | GenericArgData::Ty(TyKind::BoundVar(bound_var).intern(interner)).intern(interner) |
f035d41b XL |
1411 | } |
1412 | VariableKind::Lifetime => { | |
1413 | GenericArgData::Lifetime(LifetimeData::BoundVar(bound_var).intern(interner)) | |
1414 | .intern(interner) | |
1415 | } | |
1416 | VariableKind::Const(ty) => GenericArgData::Const( | |
1417 | ConstData { | |
1418 | ty: ty.clone(), | |
1419 | value: ConstValue::BoundVar(bound_var), | |
1420 | } | |
1421 | .intern(interner), | |
1422 | ) | |
1423 | .intern(interner), | |
f9f354fc XL |
1424 | } |
1425 | } | |
f035d41b | 1426 | } |
f9f354fc | 1427 | |
f035d41b XL |
1428 | /// A generic argument, see `GenericArgData` for more information. |
1429 | #[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord, HasInterner)] | |
1430 | pub struct GenericArg<I: Interner> { | |
1431 | interned: I::InternedGenericArg, | |
1432 | } | |
1433 | ||
1434 | impl<I: Interner> GenericArg<I> { | |
1435 | /// Constructs a generic argument using `GenericArgData`. | |
a2a8927a | 1436 | pub fn new(interner: I, data: GenericArgData<I>) -> Self { |
f035d41b XL |
1437 | let interned = I::intern_generic_arg(interner, data); |
1438 | GenericArg { interned } | |
f9f354fc XL |
1439 | } |
1440 | ||
f035d41b XL |
1441 | /// Gets the interned value. |
1442 | pub fn interned(&self) -> &I::InternedGenericArg { | |
1443 | &self.interned | |
1444 | } | |
1445 | ||
1446 | /// Gets the underlying data. | |
a2a8927a | 1447 | pub fn data(&self, interner: I) -> &GenericArgData<I> { |
f035d41b | 1448 | I::generic_arg_data(interner, &self.interned) |
f9f354fc | 1449 | } |
f9f354fc | 1450 | |
f035d41b | 1451 | /// Asserts that this is a type argument. |
a2a8927a | 1452 | pub fn assert_ty_ref(&self, interner: I) -> &Ty<I> { |
f035d41b | 1453 | self.ty(interner).unwrap() |
f9f354fc XL |
1454 | } |
1455 | ||
f035d41b | 1456 | /// Asserts that this is a lifetime argument. |
a2a8927a | 1457 | pub fn assert_lifetime_ref(&self, interner: I) -> &Lifetime<I> { |
f035d41b | 1458 | self.lifetime(interner).unwrap() |
f9f354fc XL |
1459 | } |
1460 | ||
f035d41b | 1461 | /// Asserts that this is a constant argument. |
a2a8927a | 1462 | pub fn assert_const_ref(&self, interner: I) -> &Const<I> { |
f035d41b XL |
1463 | self.constant(interner).unwrap() |
1464 | } | |
1465 | ||
1466 | /// Checks whether the generic argument is a type. | |
a2a8927a | 1467 | pub fn is_ty(&self, interner: I) -> bool { |
f035d41b XL |
1468 | match self.data(interner) { |
1469 | GenericArgData::Ty(_) => true, | |
1470 | GenericArgData::Lifetime(_) => false, | |
1471 | GenericArgData::Const(_) => false, | |
f9f354fc XL |
1472 | } |
1473 | } | |
1474 | ||
f035d41b | 1475 | /// Returns the type if it is one, `None` otherwise. |
a2a8927a | 1476 | pub fn ty(&self, interner: I) -> Option<&Ty<I>> { |
f035d41b XL |
1477 | match self.data(interner) { |
1478 | GenericArgData::Ty(t) => Some(t), | |
1479 | _ => None, | |
f9f354fc XL |
1480 | } |
1481 | } | |
1482 | ||
f035d41b | 1483 | /// Returns the lifetime if it is one, `None` otherwise. |
a2a8927a | 1484 | pub fn lifetime(&self, interner: I) -> Option<&Lifetime<I>> { |
f035d41b XL |
1485 | match self.data(interner) { |
1486 | GenericArgData::Lifetime(t) => Some(t), | |
f9f354fc XL |
1487 | _ => None, |
1488 | } | |
1489 | } | |
1490 | ||
f035d41b | 1491 | /// Returns the constant if it is one, `None` otherwise. |
a2a8927a | 1492 | pub fn constant(&self, interner: I) -> Option<&Const<I>> { |
f035d41b XL |
1493 | match self.data(interner) { |
1494 | GenericArgData::Const(c) => Some(c), | |
f9f354fc XL |
1495 | _ => None, |
1496 | } | |
1497 | } | |
a2a8927a XL |
1498 | |
1499 | /// Compute type flags for GenericArg<I> | |
1500 | fn compute_flags(&self, interner: I) -> TypeFlags { | |
1501 | match self.data(interner) { | |
1502 | GenericArgData::Ty(ty) => ty.data(interner).flags, | |
1503 | GenericArgData::Lifetime(lifetime) => lifetime.compute_flags(interner), | |
1504 | GenericArgData::Const(constant) => { | |
1505 | let data = constant.data(interner); | |
1506 | let flags = data.ty.data(interner).flags; | |
1507 | match data.value { | |
1508 | ConstValue::BoundVar(_) => flags, | |
1509 | ConstValue::InferenceVar(_) => { | |
1510 | flags | TypeFlags::HAS_CT_INFER | TypeFlags::STILL_FURTHER_SPECIALIZABLE | |
1511 | } | |
1512 | ConstValue::Placeholder(_) => { | |
1513 | flags | |
1514 | | TypeFlags::HAS_CT_PLACEHOLDER | |
1515 | | TypeFlags::STILL_FURTHER_SPECIALIZABLE | |
1516 | } | |
1517 | ConstValue::Concrete(_) => flags, | |
1518 | } | |
1519 | } | |
1520 | } | |
1521 | } | |
f9f354fc XL |
1522 | } |
1523 | ||
f035d41b XL |
1524 | /// Generic arguments data. |
1525 | #[derive(Clone, PartialEq, Eq, Hash, Visit, Fold, Zip)] | |
1526 | pub enum GenericArgData<I: Interner> { | |
1527 | /// Type argument | |
1528 | Ty(Ty<I>), | |
1529 | /// Lifetime argument | |
1530 | Lifetime(Lifetime<I>), | |
1531 | /// Constant argument | |
1532 | Const(Const<I>), | |
f9f354fc XL |
1533 | } |
1534 | ||
f035d41b XL |
1535 | impl<I: Interner> Copy for GenericArgData<I> |
1536 | where | |
1537 | I::InternedType: Copy, | |
1538 | I::InternedLifetime: Copy, | |
1539 | I::InternedConst: Copy, | |
1540 | { | |
1541 | } | |
f9f354fc | 1542 | |
f035d41b XL |
1543 | impl<I: Interner> GenericArgData<I> { |
1544 | /// Create an interned type. | |
a2a8927a | 1545 | pub fn intern(self, interner: I) -> GenericArg<I> { |
f035d41b | 1546 | GenericArg::new(interner, self) |
f9f354fc | 1547 | } |
f035d41b | 1548 | } |
f9f354fc | 1549 | |
f035d41b XL |
1550 | /// A value with an associated variable kind. |
1551 | #[derive(Clone, PartialEq, Eq, Hash)] | |
1552 | pub struct WithKind<I: Interner, T> { | |
1553 | /// The associated variable kind. | |
1554 | pub kind: VariableKind<I>, | |
1555 | /// The wrapped value. | |
1556 | value: T, | |
1557 | } | |
f9f354fc | 1558 | |
f035d41b | 1559 | impl<I: Interner, T: Copy> Copy for WithKind<I, T> where I::InternedType: Copy {} |
f9f354fc | 1560 | |
f035d41b XL |
1561 | impl<I: Interner, T> HasInterner for WithKind<I, T> { |
1562 | type Interner = I; | |
1563 | } | |
1564 | ||
1565 | impl<I: Interner, T> From<WithKind<I, T>> for (VariableKind<I>, T) { | |
1566 | fn from(with_kind: WithKind<I, T>) -> Self { | |
1567 | (with_kind.kind, with_kind.value) | |
f9f354fc | 1568 | } |
f035d41b | 1569 | } |
f9f354fc | 1570 | |
f035d41b XL |
1571 | impl<I: Interner, T> WithKind<I, T> { |
1572 | /// Creates a `WithKind` from a variable kind and a value. | |
1573 | pub fn new(kind: VariableKind<I>, value: T) -> Self { | |
1574 | Self { kind, value } | |
f9f354fc XL |
1575 | } |
1576 | ||
f035d41b XL |
1577 | /// Maps the value in `WithKind`. |
1578 | pub fn map<U, OP>(self, op: OP) -> WithKind<I, U> | |
1579 | where | |
1580 | OP: FnOnce(T) -> U, | |
1581 | { | |
1582 | WithKind { | |
1583 | kind: self.kind, | |
1584 | value: op(self.value), | |
f9f354fc XL |
1585 | } |
1586 | } | |
1587 | ||
f035d41b XL |
1588 | /// Maps a function taking `WithKind<I, &T>` over `&WithKind<I, T>`. |
1589 | pub fn map_ref<U, OP>(&self, op: OP) -> WithKind<I, U> | |
1590 | where | |
1591 | OP: FnOnce(&T) -> U, | |
1592 | { | |
1593 | WithKind { | |
1594 | kind: self.kind.clone(), | |
1595 | value: op(&self.value), | |
f9f354fc XL |
1596 | } |
1597 | } | |
1598 | ||
f035d41b XL |
1599 | /// Extract the value, ignoring the variable kind. |
1600 | pub fn skip_kind(&self) -> &T { | |
1601 | &self.value | |
f9f354fc XL |
1602 | } |
1603 | } | |
1604 | ||
f035d41b | 1605 | /// A variable kind with universe index. |
f9f354fc | 1606 | #[allow(type_alias_bounds)] |
f035d41b | 1607 | pub type CanonicalVarKind<I: Interner> = WithKind<I, UniverseIndex>; |
f9f354fc | 1608 | |
f035d41b | 1609 | /// An alias, which is a trait indirection such as a projection or opaque type. |
f9f354fc XL |
1610 | #[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner, Zip)] |
1611 | pub enum AliasTy<I: Interner> { | |
f035d41b | 1612 | /// An associated type projection. |
f9f354fc | 1613 | Projection(ProjectionTy<I>), |
f035d41b | 1614 | /// An opaque type. |
f9f354fc XL |
1615 | Opaque(OpaqueTy<I>), |
1616 | } | |
1617 | ||
f035d41b XL |
1618 | impl<I: Interner> Copy for AliasTy<I> where I::InternedSubstitution: Copy {} |
1619 | ||
f9f354fc | 1620 | impl<I: Interner> AliasTy<I> { |
f035d41b | 1621 | /// Create an interned type for this alias. |
a2a8927a | 1622 | pub fn intern(self, interner: I) -> Ty<I> { |
f9f354fc XL |
1623 | Ty::new(interner, self) |
1624 | } | |
1625 | ||
a2a8927a XL |
1626 | /// Compute type flags for aliases |
1627 | fn compute_flags(&self, interner: I) -> TypeFlags { | |
f9f354fc | 1628 | match self { |
a2a8927a XL |
1629 | AliasTy::Projection(projection_ty) => { |
1630 | TypeFlags::HAS_TY_PROJECTION | projection_ty.substitution.compute_flags(interner) | |
1631 | } | |
1632 | AliasTy::Opaque(opaque_ty) => { | |
1633 | TypeFlags::HAS_TY_OPAQUE | opaque_ty.substitution.compute_flags(interner) | |
1634 | } | |
f9f354fc XL |
1635 | } |
1636 | } | |
1637 | } | |
1638 | ||
f035d41b | 1639 | /// A projection `<P0 as TraitName<P1..Pn>>::AssocItem<Pn+1..Pm>`. |
5869c6ff | 1640 | #[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner)] |
f9f354fc | 1641 | pub struct ProjectionTy<I: Interner> { |
f035d41b | 1642 | /// The id for the associated type member. |
f9f354fc | 1643 | pub associated_ty_id: AssocTypeId<I>, |
f035d41b | 1644 | /// The substitution for the projection. |
f9f354fc XL |
1645 | pub substitution: Substitution<I>, |
1646 | } | |
1647 | ||
f035d41b XL |
1648 | impl<I: Interner> Copy for ProjectionTy<I> where I::InternedSubstitution: Copy {} |
1649 | ||
5869c6ff XL |
1650 | impl<I: Interner> ProjectionTy<I> { |
1651 | /// Gets the type parameters of the `Self` type in this alias type. | |
a2a8927a | 1652 | pub fn self_type_parameter(&self, interner: I) -> Ty<I> { |
5869c6ff XL |
1653 | self.substitution |
1654 | .iter(interner) | |
1655 | .find_map(move |p| p.ty(interner)) | |
1656 | .unwrap() | |
1657 | .clone() | |
1658 | } | |
1659 | } | |
1660 | ||
f035d41b | 1661 | /// An opaque type `opaque type T<..>: Trait = HiddenTy`. |
5869c6ff | 1662 | #[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner)] |
f9f354fc | 1663 | pub struct OpaqueTy<I: Interner> { |
f035d41b | 1664 | /// The id for the opaque type. |
f9f354fc | 1665 | pub opaque_ty_id: OpaqueTyId<I>, |
f035d41b | 1666 | /// The substitution for the opaque type. |
f9f354fc XL |
1667 | pub substitution: Substitution<I>, |
1668 | } | |
1669 | ||
f035d41b XL |
1670 | impl<I: Interner> Copy for OpaqueTy<I> where I::InternedSubstitution: Copy {} |
1671 | ||
1672 | /// A trait reference describes the relationship between a type and a trait. | |
1673 | /// This can be used in two forms: | |
1674 | /// - `P0: Trait<P1..Pn>` (e.g. `i32: Copy`), which mentions that the type | |
1675 | /// implements the trait. | |
1676 | /// - `<P0 as Trait<P1..Pn>>` (e.g. `i32 as Copy`), which casts the type to | |
1677 | /// that specific trait. | |
5869c6ff | 1678 | #[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner)] |
f9f354fc | 1679 | pub struct TraitRef<I: Interner> { |
f035d41b | 1680 | /// The trait id. |
f9f354fc | 1681 | pub trait_id: TraitId<I>, |
f035d41b | 1682 | /// The substitution, containing both the `Self` type and the parameters. |
f9f354fc XL |
1683 | pub substitution: Substitution<I>, |
1684 | } | |
1685 | ||
f035d41b XL |
1686 | impl<I: Interner> Copy for TraitRef<I> where I::InternedSubstitution: Copy {} |
1687 | ||
f9f354fc | 1688 | impl<I: Interner> TraitRef<I> { |
f035d41b | 1689 | /// Gets all type parameters in this trait ref, including `Self`. |
a2a8927a | 1690 | pub fn type_parameters<'a>(&'a self, interner: I) -> impl Iterator<Item = Ty<I>> + 'a { |
f9f354fc XL |
1691 | self.substitution |
1692 | .iter(interner) | |
1693 | .filter_map(move |p| p.ty(interner)) | |
1694 | .cloned() | |
1695 | } | |
1696 | ||
f035d41b | 1697 | /// Gets the type parameters of the `Self` type in this trait ref. |
a2a8927a | 1698 | pub fn self_type_parameter(&self, interner: I) -> Ty<I> { |
f9f354fc XL |
1699 | self.type_parameters(interner).next().unwrap() |
1700 | } | |
1701 | ||
f035d41b | 1702 | /// Construct a `FromEnv` using this trait ref. |
f9f354fc XL |
1703 | pub fn from_env(self) -> FromEnv<I> { |
1704 | FromEnv::Trait(self) | |
1705 | } | |
1706 | ||
f035d41b | 1707 | /// Construct a `WellFormed` using this trait ref. |
f9f354fc XL |
1708 | pub fn well_formed(self) -> WellFormed<I> { |
1709 | WellFormed::Trait(self) | |
1710 | } | |
1711 | } | |
1712 | ||
f035d41b XL |
1713 | /// Lifetime outlives, which for `'a: 'b`` checks that the lifetime `'a` |
1714 | /// is a superset of the value of `'b`. | |
1715 | #[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner, Zip)] | |
1716 | #[allow(missing_docs)] | |
1717 | pub struct LifetimeOutlives<I: Interner> { | |
1718 | pub a: Lifetime<I>, | |
1719 | pub b: Lifetime<I>, | |
1720 | } | |
1721 | ||
1722 | impl<I: Interner> Copy for LifetimeOutlives<I> where I::InternedLifetime: Copy {} | |
1723 | ||
3dfed10e XL |
1724 | /// Type outlives, which for `T: 'a` checks that the type `T` |
1725 | /// lives at least as long as the lifetime `'a` | |
1726 | #[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner, Zip)] | |
1727 | pub struct TypeOutlives<I: Interner> { | |
1728 | /// The type which must outlive the given lifetime. | |
1729 | pub ty: Ty<I>, | |
1730 | /// The lifetime which the type must outlive. | |
1731 | pub lifetime: Lifetime<I>, | |
1732 | } | |
1733 | ||
1734 | impl<I: Interner> Copy for TypeOutlives<I> | |
1735 | where | |
1736 | I::InternedLifetime: Copy, | |
1737 | I::InternedType: Copy, | |
1738 | { | |
1739 | } | |
1740 | ||
f9f354fc XL |
1741 | /// Where clauses that can be written by a Rust programmer. |
1742 | #[derive(Clone, PartialEq, Eq, Hash, Fold, SuperVisit, HasInterner, Zip)] | |
1743 | pub enum WhereClause<I: Interner> { | |
f035d41b | 1744 | /// Type implements a trait. |
f9f354fc | 1745 | Implemented(TraitRef<I>), |
f035d41b | 1746 | /// Type is equal to an alias. |
f9f354fc | 1747 | AliasEq(AliasEq<I>), |
f035d41b XL |
1748 | /// One lifetime outlives another. |
1749 | LifetimeOutlives(LifetimeOutlives<I>), | |
3dfed10e XL |
1750 | /// Type outlives a lifetime. |
1751 | TypeOutlives(TypeOutlives<I>), | |
f9f354fc XL |
1752 | } |
1753 | ||
f035d41b XL |
1754 | impl<I: Interner> Copy for WhereClause<I> |
1755 | where | |
1756 | I::InternedSubstitution: Copy, | |
1757 | I::InternedLifetime: Copy, | |
1758 | I::InternedType: Copy, | |
1759 | { | |
1760 | } | |
1761 | ||
1762 | /// Checks whether a type or trait ref is well-formed. | |
f9f354fc XL |
1763 | #[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner, Zip)] |
1764 | pub enum WellFormed<I: Interner> { | |
f035d41b | 1765 | /// A predicate which is true when some trait ref is well-formed. |
f9f354fc XL |
1766 | /// For example, given the following trait definitions: |
1767 | /// | |
1768 | /// ```notrust | |
1769 | /// trait Clone { ... } | |
1770 | /// trait Copy where Self: Clone { ... } | |
1771 | /// ``` | |
1772 | /// | |
1773 | /// then we have the following rule: | |
1774 | /// | |
1775 | /// ```notrust | |
1776 | /// WellFormed(?Self: Copy) :- ?Self: Copy, WellFormed(?Self: Clone) | |
1777 | /// ``` | |
1778 | Trait(TraitRef<I>), | |
1779 | ||
f035d41b | 1780 | /// A predicate which is true when some type is well-formed. |
f9f354fc XL |
1781 | /// For example, given the following type definition: |
1782 | /// | |
1783 | /// ```notrust | |
1784 | /// struct Set<K> where K: Hash { | |
1785 | /// ... | |
1786 | /// } | |
1787 | /// ``` | |
1788 | /// | |
1789 | /// then we have the following rule: `WellFormedTy(Set<K>) :- Implemented(K: Hash)`. | |
1790 | Ty(Ty<I>), | |
1791 | } | |
1792 | ||
f035d41b XL |
1793 | impl<I: Interner> Copy for WellFormed<I> |
1794 | where | |
1795 | I::InternedType: Copy, | |
1796 | I::InternedSubstitution: Copy, | |
1797 | { | |
1798 | } | |
1799 | ||
1800 | /// Checks whether a type or trait ref can be derived from the contents of the environment. | |
f9f354fc XL |
1801 | #[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner, Zip)] |
1802 | pub enum FromEnv<I: Interner> { | |
1803 | /// A predicate which enables deriving everything which should be true if we *know* that | |
1804 | /// some trait ref is well-formed. For example given the above trait definitions, we can use | |
1805 | /// `FromEnv(T: Copy)` to derive that `T: Clone`, like in: | |
1806 | /// | |
1807 | /// ```notrust | |
1808 | /// forall<T> { | |
1809 | /// if (FromEnv(T: Copy)) { | |
1810 | /// T: Clone | |
1811 | /// } | |
1812 | /// } | |
1813 | /// ``` | |
1814 | Trait(TraitRef<I>), | |
1815 | ||
1816 | /// A predicate which enables deriving everything which should be true if we *know* that | |
1817 | /// some type is well-formed. For example given the above type definition, we can use | |
1818 | /// `FromEnv(Set<K>)` to derive that `K: Hash`, like in: | |
1819 | /// | |
1820 | /// ```notrust | |
1821 | /// forall<K> { | |
1822 | /// if (FromEnv(Set<K>)) { | |
1823 | /// K: Hash | |
1824 | /// } | |
1825 | /// } | |
1826 | /// ``` | |
1827 | Ty(Ty<I>), | |
1828 | } | |
1829 | ||
f035d41b XL |
1830 | impl<I: Interner> Copy for FromEnv<I> |
1831 | where | |
1832 | I::InternedType: Copy, | |
1833 | I::InternedSubstitution: Copy, | |
1834 | { | |
1835 | } | |
1836 | ||
f9f354fc XL |
1837 | /// A "domain goal" is a goal that is directly about Rust, rather than a pure |
1838 | /// logical statement. As much as possible, the Chalk solver should avoid | |
1839 | /// decomposing this enum, and instead treat its values opaquely. | |
1840 | #[derive(Clone, PartialEq, Eq, Hash, Fold, SuperVisit, HasInterner, Zip)] | |
1841 | pub enum DomainGoal<I: Interner> { | |
f035d41b | 1842 | /// Simple goal that is true if the where clause is true. |
f9f354fc XL |
1843 | Holds(WhereClause<I>), |
1844 | ||
f035d41b | 1845 | /// True if the type or trait ref is well-formed. |
f9f354fc XL |
1846 | WellFormed(WellFormed<I>), |
1847 | ||
f035d41b | 1848 | /// True if the trait ref can be derived from in-scope where clauses. |
f9f354fc XL |
1849 | FromEnv(FromEnv<I>), |
1850 | ||
f035d41b | 1851 | /// True if the alias type can be normalized to some other type |
f9f354fc XL |
1852 | Normalize(Normalize<I>), |
1853 | ||
1854 | /// True if a type is considered to have been "defined" by the current crate. This is true for | |
1855 | /// a `struct Foo { }` but false for a `#[upstream] struct Foo { }`. However, for fundamental types | |
1856 | /// like `Box<T>`, it is true if `T` is local. | |
1857 | IsLocal(Ty<I>), | |
1858 | ||
1859 | /// True if a type is *not* considered to have been "defined" by the current crate. This is | |
1860 | /// false for a `struct Foo { }` but true for a `#[upstream] struct Foo { }`. However, for | |
1861 | /// fundamental types like `Box<T>`, it is true if `T` is upstream. | |
1862 | IsUpstream(Ty<I>), | |
1863 | ||
1864 | /// True if a type and its input types are fully visible, known types. That is, there are no | |
1865 | /// unknown type parameters anywhere in this type. | |
1866 | /// | |
1867 | /// More formally, for each struct S<P0..Pn>: | |
1868 | /// forall<P0..Pn> { | |
1869 | /// IsFullyVisible(S<P0...Pn>) :- | |
1870 | /// IsFullyVisible(P0), | |
1871 | /// ... | |
1872 | /// IsFullyVisible(Pn) | |
1873 | /// } | |
1874 | /// | |
1875 | /// Note that any of these types can have lifetimes in their parameters too, but we only | |
1876 | /// consider type parameters. | |
1877 | IsFullyVisible(Ty<I>), | |
1878 | ||
1879 | /// Used to dictate when trait impls are allowed in the current (local) crate based on the | |
1880 | /// orphan rules. | |
1881 | /// | |
1882 | /// `LocalImplAllowed(T: Trait)` is true if the type T is allowed to impl trait Trait in | |
1883 | /// the current crate. Under the current rules, this is unconditionally true for all types if | |
1884 | /// the Trait is considered to be "defined" in the current crate. If that is not the case, then | |
1885 | /// `LocalImplAllowed(T: Trait)` can still be true if `IsLocal(T)` is true. | |
1886 | LocalImplAllowed(TraitRef<I>), | |
1887 | ||
1888 | /// Used to activate the "compatible modality" rules. Rules that introduce predicates that have | |
1889 | /// to do with "all compatible universes" should depend on this clause so that they only apply | |
1890 | /// if this is present. | |
3dfed10e | 1891 | Compatible, |
f9f354fc XL |
1892 | |
1893 | /// Used to indicate that a given type is in a downstream crate. Downstream crates contain the | |
1894 | /// current crate at some level of their dependencies. | |
1895 | /// | |
1896 | /// Since chalk does not actually see downstream types, this is usually introduced with | |
1897 | /// implication on a fresh, universally quantified type. | |
1898 | /// | |
1899 | /// forall<T> { if (DownstreamType(T)) { /* ... */ } } | |
1900 | /// | |
1901 | /// This makes a new type `T` available and makes `DownstreamType(T)` provable for that type. | |
1902 | DownstreamType(Ty<I>), | |
1903 | ||
1904 | /// Used to activate the "reveal mode", in which opaque (`impl Trait`) types can be equated | |
1905 | /// to their actual type. | |
3dfed10e | 1906 | Reveal, |
f035d41b XL |
1907 | |
1908 | /// Used to indicate that a trait is object safe. | |
1909 | ObjectSafe(TraitId<I>), | |
f9f354fc XL |
1910 | } |
1911 | ||
f035d41b XL |
1912 | impl<I: Interner> Copy for DomainGoal<I> |
1913 | where | |
1914 | I::InternedSubstitution: Copy, | |
1915 | I::InternedLifetime: Copy, | |
1916 | I::InternedType: Copy, | |
1917 | { | |
1918 | } | |
1919 | ||
1920 | /// A where clause that can contain `forall<>` or `exists<>` quantifiers. | |
f9f354fc XL |
1921 | pub type QuantifiedWhereClause<I> = Binders<WhereClause<I>>; |
1922 | ||
1923 | impl<I: Interner> WhereClause<I> { | |
1924 | /// Turn a where clause into the WF version of it i.e.: | |
1925 | /// * `Implemented(T: Trait)` maps to `WellFormed(T: Trait)` | |
1926 | /// * `ProjectionEq(<T as Trait>::Item = Foo)` maps to `WellFormed(<T as Trait>::Item = Foo)` | |
1927 | /// * any other clause maps to itself | |
a2a8927a | 1928 | pub fn into_well_formed_goal(self, interner: I) -> DomainGoal<I> { |
f9f354fc XL |
1929 | match self { |
1930 | WhereClause::Implemented(trait_ref) => WellFormed::Trait(trait_ref).cast(interner), | |
1931 | wc => wc.cast(interner), | |
1932 | } | |
1933 | } | |
1934 | ||
1935 | /// Same as `into_well_formed_goal` but with the `FromEnv` predicate instead of `WellFormed`. | |
a2a8927a | 1936 | pub fn into_from_env_goal(self, interner: I) -> DomainGoal<I> { |
f9f354fc XL |
1937 | match self { |
1938 | WhereClause::Implemented(trait_ref) => FromEnv::Trait(trait_ref).cast(interner), | |
1939 | wc => wc.cast(interner), | |
1940 | } | |
1941 | } | |
f035d41b XL |
1942 | |
1943 | /// If where clause is a `TraitRef`, returns its trait id. | |
1944 | pub fn trait_id(&self) -> Option<TraitId<I>> { | |
1945 | match self { | |
1946 | WhereClause::Implemented(trait_ref) => Some(trait_ref.trait_id), | |
1947 | WhereClause::AliasEq(_) => None, | |
1948 | WhereClause::LifetimeOutlives(_) => None, | |
3dfed10e | 1949 | WhereClause::TypeOutlives(_) => None, |
f035d41b XL |
1950 | } |
1951 | } | |
f9f354fc XL |
1952 | } |
1953 | ||
1954 | impl<I: Interner> QuantifiedWhereClause<I> { | |
1955 | /// As with `WhereClause::into_well_formed_goal`, but for a | |
1956 | /// quantified where clause. For example, `forall<T> { | |
1957 | /// Implemented(T: Trait)}` would map to `forall<T> { | |
1958 | /// WellFormed(T: Trait) }`. | |
a2a8927a | 1959 | pub fn into_well_formed_goal(self, interner: I) -> Binders<DomainGoal<I>> { |
f9f354fc XL |
1960 | self.map(|wc| wc.into_well_formed_goal(interner)) |
1961 | } | |
1962 | ||
1963 | /// As with `WhereClause::into_from_env_goal`, but mapped over any | |
1964 | /// binders. For example, `forall<T> { | |
1965 | /// Implemented(T: Trait)}` would map to `forall<T> { | |
1966 | /// FromEnv(T: Trait) }`. | |
a2a8927a | 1967 | pub fn into_from_env_goal(self, interner: I) -> Binders<DomainGoal<I>> { |
f9f354fc XL |
1968 | self.map(|wc| wc.into_from_env_goal(interner)) |
1969 | } | |
f035d41b XL |
1970 | |
1971 | /// If the underlying where clause is a `TraitRef`, returns its trait id. | |
1972 | pub fn trait_id(&self) -> Option<TraitId<I>> { | |
1973 | self.skip_binders().trait_id() | |
1974 | } | |
f9f354fc XL |
1975 | } |
1976 | ||
f9f354fc XL |
1977 | impl<I: Interner> DomainGoal<I> { |
1978 | /// Convert `Implemented(...)` into `FromEnv(...)`, but leave other | |
1979 | /// goals unchanged. | |
a2a8927a | 1980 | pub fn into_from_env_goal(self, interner: I) -> DomainGoal<I> { |
f9f354fc XL |
1981 | match self { |
1982 | DomainGoal::Holds(wc) => wc.into_from_env_goal(interner), | |
1983 | goal => goal, | |
1984 | } | |
1985 | } | |
1986 | ||
f035d41b | 1987 | /// Lists generic arguments that are inputs to this domain goal. |
a2a8927a | 1988 | pub fn inputs(&self, interner: I) -> Vec<GenericArg<I>> { |
f9f354fc XL |
1989 | match self { |
1990 | DomainGoal::Holds(WhereClause::AliasEq(alias_eq)) => { | |
f035d41b | 1991 | vec![GenericArgData::Ty(alias_eq.alias.clone().intern(interner)).intern(interner)] |
f9f354fc XL |
1992 | } |
1993 | _ => Vec::new(), | |
1994 | } | |
1995 | } | |
1996 | } | |
1997 | ||
f035d41b | 1998 | /// Equality goal: tries to prove that two values are equal. |
f9f354fc | 1999 | #[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, Zip)] |
f035d41b | 2000 | #[allow(missing_docs)] |
f9f354fc | 2001 | pub struct EqGoal<I: Interner> { |
f035d41b XL |
2002 | pub a: GenericArg<I>, |
2003 | pub b: GenericArg<I>, | |
f9f354fc XL |
2004 | } |
2005 | ||
f035d41b XL |
2006 | impl<I: Interner> Copy for EqGoal<I> where I::InternedGenericArg: Copy {} |
2007 | ||
5869c6ff XL |
2008 | /// Subtype goal: tries to prove that `a` is a subtype of `b` |
2009 | #[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, Zip)] | |
2010 | #[allow(missing_docs)] | |
2011 | pub struct SubtypeGoal<I: Interner> { | |
2012 | pub a: Ty<I>, | |
2013 | pub b: Ty<I>, | |
2014 | } | |
2015 | ||
2016 | impl<I: Interner> Copy for SubtypeGoal<I> where I::InternedType: Copy {} | |
2017 | ||
f9f354fc XL |
2018 | /// Proves that the given type alias **normalizes** to the given |
2019 | /// type. A projection `T::Foo` normalizes to the type `U` if we can | |
2020 | /// **match it to an impl** and that impl has a `type Foo = V` where | |
2021 | /// `U = V`. | |
2022 | #[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, Zip)] | |
f035d41b | 2023 | #[allow(missing_docs)] |
f9f354fc XL |
2024 | pub struct Normalize<I: Interner> { |
2025 | pub alias: AliasTy<I>, | |
2026 | pub ty: Ty<I>, | |
2027 | } | |
2028 | ||
f035d41b XL |
2029 | impl<I: Interner> Copy for Normalize<I> |
2030 | where | |
2031 | I::InternedSubstitution: Copy, | |
2032 | I::InternedType: Copy, | |
2033 | { | |
2034 | } | |
2035 | ||
f9f354fc XL |
2036 | /// Proves **equality** between an alias and a type. |
2037 | #[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, Zip)] | |
f035d41b | 2038 | #[allow(missing_docs)] |
f9f354fc XL |
2039 | pub struct AliasEq<I: Interner> { |
2040 | pub alias: AliasTy<I>, | |
2041 | pub ty: Ty<I>, | |
2042 | } | |
2043 | ||
f035d41b XL |
2044 | impl<I: Interner> Copy for AliasEq<I> |
2045 | where | |
2046 | I::InternedSubstitution: Copy, | |
2047 | I::InternedType: Copy, | |
2048 | { | |
2049 | } | |
2050 | ||
f9f354fc XL |
2051 | impl<I: Interner> HasInterner for AliasEq<I> { |
2052 | type Interner = I; | |
2053 | } | |
2054 | ||
2055 | /// Indicates that the `value` is universally quantified over `N` | |
2056 | /// parameters of the given kinds, where `N == self.binders.len()`. A | |
2057 | /// variable with depth `i < N` refers to the value at | |
2058 | /// `self.binders[i]`. Variables with depth `>= N` are free. | |
2059 | /// | |
2060 | /// (IOW, we use deBruijn indices, where binders are introduced in reverse order | |
2061 | /// of `self.binders`.) | |
2062 | #[derive(Clone, PartialEq, Eq, Hash)] | |
2063 | pub struct Binders<T: HasInterner> { | |
f035d41b XL |
2064 | /// The binders that quantify over the value. |
2065 | pub binders: VariableKinds<T::Interner>, | |
2066 | ||
2067 | /// The value being quantified over. | |
f9f354fc XL |
2068 | value: T, |
2069 | } | |
2070 | ||
f035d41b XL |
2071 | impl<T: HasInterner + Copy> Copy for Binders<T> where |
2072 | <T::Interner as Interner>::InternedVariableKinds: Copy | |
2073 | { | |
2074 | } | |
2075 | ||
f9f354fc XL |
2076 | impl<T: HasInterner> HasInterner for Binders<T> { |
2077 | type Interner = T::Interner; | |
2078 | } | |
2079 | ||
5869c6ff XL |
2080 | impl<T: Clone + HasInterner> Binders<&T> { |
2081 | /// Converts a `Binders<&T>` to a `Binders<T>` by cloning `T`. | |
2082 | pub fn cloned(self) -> Binders<T> { | |
2083 | self.map(Clone::clone) | |
2084 | } | |
2085 | } | |
2086 | ||
f9f354fc | 2087 | impl<T: HasInterner> Binders<T> { |
f035d41b XL |
2088 | /// Create new binders. |
2089 | pub fn new(binders: VariableKinds<T::Interner>, value: T) -> Self { | |
2090 | Self { binders, value } | |
2091 | } | |
2092 | ||
2093 | /// Wraps the given value in a binder without variables, i.e. `for<> | |
2094 | /// (value)`. Since our deBruijn indices count binders, not variables, this | |
2095 | /// is sometimes useful. | |
a2a8927a | 2096 | pub fn empty(interner: T::Interner, value: T) -> Self { |
3dfed10e | 2097 | let binders = VariableKinds::empty(interner); |
f9f354fc XL |
2098 | Self { binders, value } |
2099 | } | |
2100 | ||
2101 | /// Skips the binder and returns the "bound" value. This is a | |
2102 | /// risky thing to do because it's easy to get confused about | |
2103 | /// De Bruijn indices and the like. `skip_binder` is only valid | |
2104 | /// when you are either extracting data that has nothing to | |
2105 | /// do with bound vars, or you are being very careful about | |
2106 | /// your depth accounting. | |
2107 | /// | |
2108 | /// Some examples where `skip_binder` is reasonable: | |
2109 | /// | |
2110 | /// - extracting the `TraitId` from a TraitRef; | |
2111 | /// - checking if there are any fields in a StructDatum | |
2112 | pub fn skip_binders(&self) -> &T { | |
2113 | &self.value | |
2114 | } | |
2115 | ||
5869c6ff | 2116 | /// Skips the binder and returns the "bound" value as well as the skipped free variables. This |
a2a8927a | 2117 | /// is just as risky as [`skip_binders`][Self::skip_binders]. |
5869c6ff XL |
2118 | pub fn into_value_and_skipped_binders(self) -> (T, VariableKinds<T::Interner>) { |
2119 | (self.value, self.binders) | |
2120 | } | |
2121 | ||
f9f354fc XL |
2122 | /// Converts `&Binders<T>` to `Binders<&T>`. Produces new `Binders` |
2123 | /// with cloned quantifiers containing a reference to the original | |
2124 | /// value, leaving the original in place. | |
2125 | pub fn as_ref(&self) -> Binders<&T> { | |
2126 | Binders { | |
2127 | binders: self.binders.clone(), | |
2128 | value: &self.value, | |
2129 | } | |
2130 | } | |
2131 | ||
f035d41b | 2132 | /// Maps the binders by applying a function. |
f9f354fc XL |
2133 | pub fn map<U, OP>(self, op: OP) -> Binders<U> |
2134 | where | |
2135 | OP: FnOnce(T) -> U, | |
2136 | U: HasInterner<Interner = T::Interner>, | |
2137 | { | |
2138 | let value = op(self.value); | |
2139 | Binders { | |
2140 | binders: self.binders, | |
2141 | value, | |
2142 | } | |
2143 | } | |
2144 | ||
f035d41b XL |
2145 | /// Transforms the inner value according to the given function; returns |
2146 | /// `None` if the function returns `None`. | |
2147 | pub fn filter_map<U, OP>(self, op: OP) -> Option<Binders<U>> | |
2148 | where | |
2149 | OP: FnOnce(T) -> Option<U>, | |
2150 | U: HasInterner<Interner = T::Interner>, | |
2151 | { | |
2152 | let value = op(self.value)?; | |
2153 | Some(Binders { | |
2154 | binders: self.binders, | |
2155 | value, | |
2156 | }) | |
2157 | } | |
2158 | ||
2159 | /// Maps a function taking `Binders<&T>` over `&Binders<T>`. | |
f9f354fc XL |
2160 | pub fn map_ref<'a, U, OP>(&'a self, op: OP) -> Binders<U> |
2161 | where | |
2162 | OP: FnOnce(&'a T) -> U, | |
2163 | U: HasInterner<Interner = T::Interner>, | |
2164 | { | |
2165 | self.as_ref().map(op) | |
2166 | } | |
2167 | ||
f035d41b XL |
2168 | /// Creates a `Substitution` containing bound vars such that applying this |
2169 | /// substitution will not change the value, i.e. `^0.0, ^0.1, ^0.2` and so | |
2170 | /// on. | |
a2a8927a | 2171 | pub fn identity_substitution(&self, interner: T::Interner) -> Substitution<T::Interner> { |
3dfed10e | 2172 | Substitution::from_iter( |
f035d41b XL |
2173 | interner, |
2174 | self.binders | |
2175 | .iter(interner) | |
2176 | .enumerate() | |
2177 | .map(|p| p.to_generic_arg(interner)), | |
2178 | ) | |
2179 | } | |
2180 | ||
f9f354fc XL |
2181 | /// Creates a fresh binders that contains a single type |
2182 | /// variable. The result of the closure will be embedded in this | |
2183 | /// binder. Note that you should be careful with what you return | |
2184 | /// from the closure to account for the binder that will be added. | |
2185 | /// | |
2186 | /// XXX FIXME -- this is potentially a pretty footgun-y function. | |
2187 | pub fn with_fresh_type_var( | |
a2a8927a | 2188 | interner: T::Interner, |
f9f354fc XL |
2189 | op: impl FnOnce(Ty<T::Interner>) -> T, |
2190 | ) -> Binders<T> { | |
2191 | // The new variable is at the front and everything afterwards is shifted up by 1 | |
29967ef6 | 2192 | let new_var = TyKind::BoundVar(BoundVar::new(DebruijnIndex::INNERMOST, 0)).intern(interner); |
f9f354fc | 2193 | let value = op(new_var); |
29967ef6 | 2194 | let binders = VariableKinds::from1(interner, VariableKind::Ty(TyVariableKind::General)); |
f9f354fc XL |
2195 | Binders { binders, value } |
2196 | } | |
2197 | ||
f035d41b | 2198 | /// Returns the number of binders. |
a2a8927a | 2199 | pub fn len(&self, interner: T::Interner) -> usize { |
f9f354fc XL |
2200 | self.binders.len(interner) |
2201 | } | |
2202 | } | |
2203 | ||
f035d41b XL |
2204 | impl<T, I> Binders<Binders<T>> |
2205 | where | |
5869c6ff | 2206 | T: Fold<I> + HasInterner<Interner = I>, |
f035d41b XL |
2207 | T::Result: HasInterner<Interner = I>, |
2208 | I: Interner, | |
2209 | { | |
2210 | /// This turns two levels of binders (`for<A> for<B>`) into one level (`for<A, B>`). | |
a2a8927a | 2211 | pub fn fuse_binders(self, interner: T::Interner) -> Binders<T::Result> { |
f035d41b XL |
2212 | let num_binders = self.len(interner); |
2213 | // generate a substitution to shift the indexes of the inner binder: | |
3dfed10e | 2214 | let subst = Substitution::from_iter( |
f035d41b XL |
2215 | interner, |
2216 | self.value | |
2217 | .binders | |
2218 | .iter(interner) | |
2219 | .enumerate() | |
2220 | .map(|(i, pk)| (i + num_binders, pk).to_generic_arg(interner)), | |
2221 | ); | |
3dfed10e | 2222 | let binders = VariableKinds::from_iter( |
f035d41b XL |
2223 | interner, |
2224 | self.binders | |
2225 | .iter(interner) | |
2226 | .chain(self.value.binders.iter(interner)) | |
2227 | .cloned(), | |
2228 | ); | |
5869c6ff | 2229 | let value = self.value.substitute(interner, &subst); |
f035d41b XL |
2230 | Binders { binders, value } |
2231 | } | |
2232 | } | |
2233 | ||
2234 | impl<T: HasInterner> From<Binders<T>> for (VariableKinds<T::Interner>, T) { | |
f9f354fc XL |
2235 | fn from(binders: Binders<T>) -> Self { |
2236 | (binders.binders, binders.value) | |
2237 | } | |
2238 | } | |
2239 | ||
2240 | impl<T, I> Binders<T> | |
2241 | where | |
5869c6ff | 2242 | T: Fold<I> + HasInterner<Interner = I>, |
f9f354fc XL |
2243 | I: Interner, |
2244 | { | |
2245 | /// Substitute `parameters` for the variables introduced by these | |
2246 | /// binders. So if the binders represent (e.g.) `<X, Y> { T }` and | |
2247 | /// parameters is the slice `[A, B]`, then returns `[X => A, Y => | |
2248 | /// B] T`. | |
2249 | pub fn substitute( | |
5869c6ff | 2250 | self, |
a2a8927a | 2251 | interner: I, |
f9f354fc XL |
2252 | parameters: &(impl AsParameters<I> + ?Sized), |
2253 | ) -> T::Result { | |
2254 | let parameters = parameters.as_parameters(interner); | |
2255 | assert_eq!(self.binders.len(interner), parameters.len()); | |
5869c6ff | 2256 | Subst::apply(interner, parameters, self.value) |
f9f354fc XL |
2257 | } |
2258 | } | |
2259 | ||
f9f354fc XL |
2260 | /// Allows iterating over a Binders<Vec<T>>, for instance. |
2261 | /// Each element will include the same set of parameter bounds. | |
2262 | impl<V, U> IntoIterator for Binders<V> | |
2263 | where | |
2264 | V: HasInterner + IntoIterator<Item = U>, | |
2265 | U: HasInterner<Interner = V::Interner>, | |
2266 | { | |
2267 | type Item = Binders<U>; | |
2268 | type IntoIter = BindersIntoIterator<V>; | |
2269 | ||
2270 | fn into_iter(self) -> Self::IntoIter { | |
2271 | BindersIntoIterator { | |
2272 | iter: self.value.into_iter(), | |
2273 | binders: self.binders, | |
2274 | } | |
2275 | } | |
2276 | } | |
2277 | ||
f035d41b | 2278 | /// `IntoIterator` for binders. |
f9f354fc XL |
2279 | pub struct BindersIntoIterator<V: HasInterner + IntoIterator> { |
2280 | iter: <V as IntoIterator>::IntoIter, | |
f035d41b | 2281 | binders: VariableKinds<V::Interner>, |
f9f354fc XL |
2282 | } |
2283 | ||
2284 | impl<V> Iterator for BindersIntoIterator<V> | |
2285 | where | |
2286 | V: HasInterner + IntoIterator, | |
2287 | <V as IntoIterator>::Item: HasInterner<Interner = V::Interner>, | |
2288 | { | |
2289 | type Item = Binders<<V as IntoIterator>::Item>; | |
2290 | fn next(&mut self) -> Option<Self::Item> { | |
2291 | self.iter | |
2292 | .next() | |
2293 | .map(|v| Binders::new(self.binders.clone(), v)) | |
2294 | } | |
2295 | } | |
2296 | ||
2297 | /// Represents one clause of the form `consequence :- conditions` where | |
2298 | /// `conditions = cond_1 && cond_2 && ...` is the conjunction of the individual | |
2299 | /// conditions. | |
2300 | #[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner, Zip)] | |
2301 | pub struct ProgramClauseImplication<I: Interner> { | |
f035d41b | 2302 | /// The consequence of the clause, which holds if the conditions holds. |
f9f354fc | 2303 | pub consequence: DomainGoal<I>, |
f035d41b XL |
2304 | |
2305 | /// The condition goals that should hold. | |
f9f354fc | 2306 | pub conditions: Goals<I>, |
f035d41b | 2307 | |
3dfed10e XL |
2308 | /// The lifetime constraints that should be proven. |
2309 | pub constraints: Constraints<I>, | |
2310 | ||
f035d41b | 2311 | /// The relative priority of the implication. |
f9f354fc XL |
2312 | pub priority: ClausePriority, |
2313 | } | |
2314 | ||
f035d41b | 2315 | /// Specifies how important an implication is. |
f9f354fc XL |
2316 | #[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)] |
2317 | pub enum ClausePriority { | |
f035d41b | 2318 | /// High priority, the solver should prioritize this. |
f9f354fc | 2319 | High, |
f035d41b XL |
2320 | |
2321 | /// Low priority, this implication has lower chance to be relevant to the goal. | |
f9f354fc XL |
2322 | Low, |
2323 | } | |
2324 | ||
2325 | impl std::ops::BitAnd for ClausePriority { | |
2326 | type Output = ClausePriority; | |
2327 | fn bitand(self, rhs: ClausePriority) -> Self::Output { | |
2328 | match (self, rhs) { | |
2329 | (ClausePriority::High, ClausePriority::High) => ClausePriority::High, | |
2330 | _ => ClausePriority::Low, | |
2331 | } | |
2332 | } | |
2333 | } | |
2334 | ||
f035d41b | 2335 | /// Contains the data for a program clause. |
f9f354fc | 2336 | #[derive(Clone, PartialEq, Eq, Hash, Fold, HasInterner, Zip)] |
f035d41b | 2337 | pub struct ProgramClauseData<I: Interner>(pub Binders<ProgramClauseImplication<I>>); |
f9f354fc XL |
2338 | |
2339 | impl<I: Interner> ProgramClauseImplication<I> { | |
f035d41b | 2340 | /// Change the implication into an application holding a `FromEnv` goal. |
a2a8927a | 2341 | pub fn into_from_env_clause(self, interner: I) -> ProgramClauseImplication<I> { |
f9f354fc XL |
2342 | if self.conditions.is_empty(interner) { |
2343 | ProgramClauseImplication { | |
2344 | consequence: self.consequence.into_from_env_goal(interner), | |
2345 | conditions: self.conditions.clone(), | |
3dfed10e | 2346 | constraints: self.constraints.clone(), |
f9f354fc XL |
2347 | priority: self.priority, |
2348 | } | |
2349 | } else { | |
2350 | self | |
2351 | } | |
2352 | } | |
2353 | } | |
2354 | ||
2355 | impl<I: Interner> ProgramClauseData<I> { | |
f035d41b | 2356 | /// Change the program clause data into a `FromEnv` program clause. |
a2a8927a | 2357 | pub fn into_from_env_clause(self, interner: I) -> ProgramClauseData<I> { |
f035d41b | 2358 | ProgramClauseData(self.0.map(|i| i.into_from_env_clause(interner))) |
f9f354fc XL |
2359 | } |
2360 | ||
f035d41b | 2361 | /// Intern the program clause data. |
a2a8927a | 2362 | pub fn intern(self, interner: I) -> ProgramClause<I> { |
f9f354fc XL |
2363 | ProgramClause { |
2364 | interned: interner.intern_program_clause(self), | |
2365 | } | |
2366 | } | |
2367 | } | |
2368 | ||
f035d41b | 2369 | /// A program clause is a logic expression used to describe a part of the program. |
f9f354fc XL |
2370 | #[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord, HasInterner)] |
2371 | pub struct ProgramClause<I: Interner> { | |
2372 | interned: I::InternedProgramClause, | |
2373 | } | |
2374 | ||
2375 | impl<I: Interner> ProgramClause<I> { | |
f035d41b | 2376 | /// Create a new program clause using `ProgramClauseData`. |
a2a8927a | 2377 | pub fn new(interner: I, clause: ProgramClauseData<I>) -> Self { |
f9f354fc XL |
2378 | let interned = interner.intern_program_clause(clause); |
2379 | Self { interned } | |
2380 | } | |
2381 | ||
f035d41b | 2382 | /// Change the clause into a `FromEnv` clause. |
a2a8927a | 2383 | pub fn into_from_env_clause(self, interner: I) -> ProgramClause<I> { |
f9f354fc XL |
2384 | let program_clause_data = self.data(interner); |
2385 | let new_clause = program_clause_data.clone().into_from_env_clause(interner); | |
2386 | Self::new(interner, new_clause) | |
2387 | } | |
2388 | ||
f035d41b | 2389 | /// Get the interned program clause. |
f9f354fc XL |
2390 | pub fn interned(&self) -> &I::InternedProgramClause { |
2391 | &self.interned | |
2392 | } | |
2393 | ||
f035d41b | 2394 | /// Get the program clause data. |
a2a8927a | 2395 | pub fn data(&self, interner: I) -> &ProgramClauseData<I> { |
f9f354fc XL |
2396 | interner.program_clause_data(&self.interned) |
2397 | } | |
2398 | } | |
2399 | ||
f9f354fc XL |
2400 | /// Wraps a "canonicalized item". Items are canonicalized as follows: |
2401 | /// | |
2402 | /// All unresolved existential variables are "renumbered" according to their | |
2403 | /// first appearance; the kind/universe of the variable is recorded in the | |
2404 | /// `binders` field. | |
2405 | #[derive(Clone, Debug, PartialEq, Eq, Hash)] | |
2406 | pub struct Canonical<T: HasInterner> { | |
f035d41b | 2407 | /// The item that is canonicalized. |
f9f354fc | 2408 | pub value: T, |
f035d41b XL |
2409 | |
2410 | /// The kind/universe of the variable. | |
f9f354fc XL |
2411 | pub binders: CanonicalVarKinds<T::Interner>, |
2412 | } | |
2413 | ||
2414 | impl<T: HasInterner> HasInterner for Canonical<T> { | |
2415 | type Interner = T::Interner; | |
2416 | } | |
2417 | ||
2418 | /// A "universe canonical" value. This is a wrapper around a | |
2419 | /// `Canonical`, indicating that the universes within have been | |
2420 | /// "renumbered" to start from 0 and collapse unimportant | |
2421 | /// distinctions. | |
2422 | /// | |
2423 | /// To produce one of these values, use the `u_canonicalize` method. | |
2424 | #[derive(Clone, Debug, PartialEq, Eq, Hash)] | |
2425 | pub struct UCanonical<T: HasInterner> { | |
f035d41b | 2426 | /// The wrapped `Canonical`. |
f9f354fc | 2427 | pub canonical: Canonical<T>, |
f035d41b XL |
2428 | |
2429 | /// The number of universes that have been collapsed. | |
f9f354fc XL |
2430 | pub universes: usize, |
2431 | } | |
2432 | ||
2433 | impl<T: HasInterner> UCanonical<T> { | |
f035d41b XL |
2434 | /// Checks whether the universe canonical value is a trivial |
2435 | /// substitution (e.g. an identity substitution). | |
f9f354fc XL |
2436 | pub fn is_trivial_substitution( |
2437 | &self, | |
a2a8927a | 2438 | interner: T::Interner, |
f9f354fc XL |
2439 | canonical_subst: &Canonical<AnswerSubst<T::Interner>>, |
2440 | ) -> bool { | |
2441 | let subst = &canonical_subst.value.subst; | |
2442 | assert_eq!( | |
2443 | self.canonical.binders.len(interner), | |
3dfed10e | 2444 | subst.as_slice(interner).len() |
f9f354fc XL |
2445 | ); |
2446 | subst.is_identity_subst(interner) | |
2447 | } | |
2448 | ||
f035d41b | 2449 | /// Creates an identity substitution. |
a2a8927a | 2450 | pub fn trivial_substitution(&self, interner: T::Interner) -> Substitution<T::Interner> { |
f9f354fc | 2451 | let binders = &self.canonical.binders; |
3dfed10e | 2452 | Substitution::from_iter( |
f9f354fc XL |
2453 | interner, |
2454 | binders | |
2455 | .iter(interner) | |
2456 | .enumerate() | |
2457 | .map(|(index, pk)| { | |
2458 | let bound_var = BoundVar::new(DebruijnIndex::INNERMOST, index); | |
f035d41b XL |
2459 | match &pk.kind { |
2460 | VariableKind::Ty(_) => { | |
29967ef6 | 2461 | GenericArgData::Ty(TyKind::BoundVar(bound_var).intern(interner)) |
f9f354fc XL |
2462 | .intern(interner) |
2463 | } | |
f035d41b | 2464 | VariableKind::Lifetime => GenericArgData::Lifetime( |
f9f354fc XL |
2465 | LifetimeData::BoundVar(bound_var).intern(interner), |
2466 | ) | |
2467 | .intern(interner), | |
f035d41b XL |
2468 | VariableKind::Const(ty) => GenericArgData::Const( |
2469 | ConstData { | |
2470 | ty: ty.clone(), | |
2471 | value: ConstValue::BoundVar(bound_var), | |
2472 | } | |
2473 | .intern(interner), | |
2474 | ) | |
2475 | .intern(interner), | |
f9f354fc XL |
2476 | } |
2477 | }) | |
2478 | .collect::<Vec<_>>(), | |
2479 | ) | |
2480 | } | |
2481 | } | |
2482 | ||
f9f354fc XL |
2483 | #[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord, HasInterner)] |
2484 | /// A general goal; this is the full range of questions you can pose to Chalk. | |
2485 | pub struct Goal<I: Interner> { | |
2486 | interned: I::InternedGoal, | |
2487 | } | |
2488 | ||
2489 | impl<I: Interner> Goal<I> { | |
f035d41b | 2490 | /// Create a new goal using `GoalData`. |
a2a8927a | 2491 | pub fn new(interner: I, interned: GoalData<I>) -> Self { |
f9f354fc XL |
2492 | let interned = I::intern_goal(interner, interned); |
2493 | Self { interned } | |
2494 | } | |
2495 | ||
f035d41b | 2496 | /// Gets the interned goal. |
f9f354fc XL |
2497 | pub fn interned(&self) -> &I::InternedGoal { |
2498 | &self.interned | |
2499 | } | |
2500 | ||
f035d41b | 2501 | /// Gets the interned goal data. |
a2a8927a | 2502 | pub fn data(&self, interner: I) -> &GoalData<I> { |
f9f354fc XL |
2503 | interner.goal_data(&self.interned) |
2504 | } | |
2505 | ||
f035d41b | 2506 | /// Create a goal using a `forall` or `exists` quantifier. |
a2a8927a | 2507 | pub fn quantify(self, interner: I, kind: QuantifierKind, binders: VariableKinds<I>) -> Goal<I> { |
f9f354fc XL |
2508 | GoalData::Quantified(kind, Binders::new(binders, self)).intern(interner) |
2509 | } | |
2510 | ||
f035d41b | 2511 | /// Takes a goal `G` and turns it into `not { G }`. |
a2a8927a | 2512 | pub fn negate(self, interner: I) -> Self { |
f9f354fc XL |
2513 | GoalData::Not(self).intern(interner) |
2514 | } | |
2515 | ||
2516 | /// Takes a goal `G` and turns it into `compatible { G }`. | |
a2a8927a | 2517 | pub fn compatible(self, interner: I) -> Self { |
f9f354fc XL |
2518 | // compatible { G } desugars into: forall<T> { if (Compatible, DownstreamType(T)) { G } } |
2519 | // This activates the compatible modality rules and introduces an anonymous downstream type | |
2520 | GoalData::Quantified( | |
2521 | QuantifierKind::ForAll, | |
2522 | Binders::with_fresh_type_var(interner, |ty| { | |
2523 | GoalData::Implies( | |
3dfed10e | 2524 | ProgramClauses::from_iter( |
f9f354fc | 2525 | interner, |
3dfed10e | 2526 | vec![DomainGoal::Compatible, DomainGoal::DownstreamType(ty)], |
f9f354fc XL |
2527 | ), |
2528 | self.shifted_in(interner), | |
2529 | ) | |
2530 | .intern(interner) | |
2531 | }), | |
2532 | ) | |
2533 | .intern(interner) | |
2534 | } | |
2535 | ||
f035d41b | 2536 | /// Create an implication goal that holds if the predicates are true. |
a2a8927a | 2537 | pub fn implied_by(self, interner: I, predicates: ProgramClauses<I>) -> Goal<I> { |
f9f354fc XL |
2538 | GoalData::Implies(predicates, self).intern(interner) |
2539 | } | |
2540 | ||
2541 | /// True if this goal is "trivially true" -- i.e., no work is | |
2542 | /// required to prove it. | |
a2a8927a | 2543 | pub fn is_trivially_true(&self, interner: I) -> bool { |
f9f354fc XL |
2544 | match self.data(interner) { |
2545 | GoalData::All(goals) => goals.is_empty(interner), | |
2546 | _ => false, | |
2547 | } | |
2548 | } | |
2549 | } | |
2550 | ||
2551 | impl<I> Goal<I> | |
2552 | where | |
2553 | I: Interner, | |
2554 | { | |
f035d41b | 2555 | /// Creates a single goal that only holds if a list of goals holds. |
a2a8927a | 2556 | pub fn all<II>(interner: I, iter: II) -> Self |
f9f354fc XL |
2557 | where |
2558 | II: IntoIterator<Item = Goal<I>>, | |
2559 | { | |
2560 | let mut iter = iter.into_iter(); | |
2561 | if let Some(goal0) = iter.next() { | |
2562 | if let Some(goal1) = iter.next() { | |
2563 | // More than one goal to prove | |
3dfed10e | 2564 | let goals = Goals::from_iter( |
f9f354fc XL |
2565 | interner, |
2566 | Some(goal0).into_iter().chain(Some(goal1)).chain(iter), | |
2567 | ); | |
2568 | GoalData::All(goals).intern(interner) | |
2569 | } else { | |
2570 | // One goal to prove | |
2571 | goal0 | |
2572 | } | |
2573 | } else { | |
2574 | // No goals to prove, always true | |
3dfed10e | 2575 | GoalData::All(Goals::empty(interner)).intern(interner) |
f9f354fc XL |
2576 | } |
2577 | } | |
2578 | } | |
2579 | ||
2580 | #[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner, Zip)] | |
2581 | /// A general goal; this is the full range of questions you can pose to Chalk. | |
2582 | pub enum GoalData<I: Interner> { | |
2583 | /// Introduces a binding at depth 0, shifting other bindings up | |
2584 | /// (deBruijn index). | |
2585 | Quantified(QuantifierKind, Binders<Goal<I>>), | |
f035d41b XL |
2586 | |
2587 | /// A goal that holds given some clauses (like an if-statement). | |
f9f354fc | 2588 | Implies(ProgramClauses<I>, Goal<I>), |
f035d41b XL |
2589 | |
2590 | /// List of goals that all should hold. | |
f9f354fc | 2591 | All(Goals<I>), |
f035d41b XL |
2592 | |
2593 | /// Negation: the inner goal should not hold. | |
f9f354fc XL |
2594 | Not(Goal<I>), |
2595 | ||
2596 | /// Make two things equal; the rules for doing so are well known to the logic | |
2597 | EqGoal(EqGoal<I>), | |
2598 | ||
5869c6ff XL |
2599 | /// Make one thing a subtype of another; the rules for doing so are well known to the logic |
2600 | SubtypeGoal(SubtypeGoal<I>), | |
2601 | ||
f9f354fc XL |
2602 | /// A "domain goal" indicates some base sort of goal that can be |
2603 | /// proven via program clauses | |
2604 | DomainGoal(DomainGoal<I>), | |
2605 | ||
2606 | /// Indicates something that cannot be proven to be true or false | |
2607 | /// definitively. This can occur with overflow but also with | |
2608 | /// unifications of skolemized variables like `forall<X,Y> { X = Y | |
2609 | /// }`. Of course, that statement is false, as there exist types | |
2610 | /// X, Y where `X = Y` is not true. But we treat it as "cannot | |
2611 | /// prove" so that `forall<X,Y> { not { X = Y } }` also winds up | |
2612 | /// as cannot prove. | |
3dfed10e | 2613 | CannotProve, |
f9f354fc XL |
2614 | } |
2615 | ||
f035d41b XL |
2616 | impl<I: Interner> Copy for GoalData<I> |
2617 | where | |
2618 | I::InternedType: Copy, | |
2619 | I::InternedLifetime: Copy, | |
2620 | I::InternedGenericArg: Copy, | |
2621 | I::InternedSubstitution: Copy, | |
2622 | I::InternedGoal: Copy, | |
2623 | I::InternedGoals: Copy, | |
2624 | I::InternedProgramClauses: Copy, | |
2625 | I::InternedVariableKinds: Copy, | |
2626 | { | |
2627 | } | |
2628 | ||
f9f354fc | 2629 | impl<I: Interner> GoalData<I> { |
f035d41b | 2630 | /// Create an interned goal. |
a2a8927a | 2631 | pub fn intern(self, interner: I) -> Goal<I> { |
f9f354fc XL |
2632 | Goal::new(interner, self) |
2633 | } | |
2634 | } | |
2635 | ||
f035d41b | 2636 | /// Kinds of quantifiers in the logic, such as `forall` and `exists`. |
f9f354fc XL |
2637 | #[derive(Copy, Clone, Debug, PartialEq, Eq, Hash, PartialOrd, Ord)] |
2638 | pub enum QuantifierKind { | |
f035d41b XL |
2639 | /// Universal quantifier `ForAll`. |
2640 | /// | |
2641 | /// A formula with the universal quantifier `forall(x). P(x)` is satisfiable | |
2642 | /// if and only if the subformula `P(x)` is true for all possible values for x. | |
f9f354fc | 2643 | ForAll, |
f035d41b XL |
2644 | |
2645 | /// Existential quantifier `Exists`. | |
2646 | /// | |
2647 | /// A formula with the existential quantifier `exists(x). P(x)` is satisfiable | |
2648 | /// if and only if there exists at least one value for all possible values of x | |
2649 | /// which satisfies the subformula `P(x)`. | |
2650 | ||
2651 | /// In the context of chalk, the existential quantifier usually demands the | |
2652 | /// existence of exactly one instance (i.e. type) that satisfies the formula | |
2653 | /// (i.e. type constraints). More than one instance means that the result is ambiguous. | |
f9f354fc XL |
2654 | Exists, |
2655 | } | |
2656 | ||
2657 | /// A constraint on lifetimes. | |
2658 | /// | |
2659 | /// When we search for solutions within the trait system, we essentially ignore | |
2660 | /// lifetime constraints, instead gathering them up to return with our solution | |
2661 | /// for later checking. This allows for decoupling between type and region | |
2662 | /// checking in the compiler. | |
3dfed10e | 2663 | #[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner, Zip)] |
f9f354fc | 2664 | pub enum Constraint<I: Interner> { |
f035d41b XL |
2665 | /// Outlives constraint `'a: 'b`, indicating that the value of `'a` must be |
2666 | /// a superset of the value of `'b`. | |
3dfed10e | 2667 | LifetimeOutlives(Lifetime<I>, Lifetime<I>), |
f9f354fc | 2668 | |
3dfed10e XL |
2669 | /// Type outlives constraint `T: 'a`, indicating that the type `T` must live |
2670 | /// at least as long as the value of `'a`. | |
2671 | TypeOutlives(Ty<I>, Lifetime<I>), | |
2672 | } | |
f035d41b | 2673 | |
3dfed10e XL |
2674 | impl<I: Interner> Copy for Constraint<I> |
2675 | where | |
2676 | I::InternedLifetime: Copy, | |
2677 | I::InternedType: Copy, | |
2678 | { | |
f9f354fc XL |
2679 | } |
2680 | ||
2681 | impl<I: Interner> Substitution<I> { | |
f9f354fc XL |
2682 | /// A substitution is an **identity substitution** if it looks |
2683 | /// like this | |
2684 | /// | |
2685 | /// ```text | |
2686 | /// ?0 := ?0 | |
2687 | /// ?1 := ?1 | |
2688 | /// ?2 := ?2 | |
2689 | /// ... | |
2690 | /// ``` | |
2691 | /// | |
2692 | /// Basically, each value is mapped to a type or lifetime with its | |
2693 | /// same index. | |
a2a8927a | 2694 | pub fn is_identity_subst(&self, interner: I) -> bool { |
f035d41b | 2695 | self.iter(interner).zip(0..).all(|(generic_arg, index)| { |
f9f354fc | 2696 | let index_db = BoundVar::new(DebruijnIndex::INNERMOST, index); |
f035d41b | 2697 | match generic_arg.data(interner) { |
29967ef6 XL |
2698 | GenericArgData::Ty(ty) => match ty.kind(interner) { |
2699 | TyKind::BoundVar(depth) => index_db == *depth, | |
f9f354fc XL |
2700 | _ => false, |
2701 | }, | |
f035d41b | 2702 | GenericArgData::Lifetime(lifetime) => match lifetime.data(interner) { |
f9f354fc XL |
2703 | LifetimeData::BoundVar(depth) => index_db == *depth, |
2704 | _ => false, | |
2705 | }, | |
f035d41b XL |
2706 | GenericArgData::Const(constant) => match &constant.data(interner).value { |
2707 | ConstValue::BoundVar(depth) => index_db == *depth, | |
2708 | _ => false, | |
2709 | }, | |
f9f354fc XL |
2710 | } |
2711 | }) | |
2712 | } | |
2713 | ||
f035d41b | 2714 | /// Apply the substitution to a value. |
a2a8927a | 2715 | pub fn apply<T>(&self, value: T, interner: I) -> T::Result |
f9f354fc | 2716 | where |
5869c6ff | 2717 | T: Fold<I>, |
f9f354fc | 2718 | { |
5869c6ff | 2719 | Substitute::apply(self, value, interner) |
f9f354fc | 2720 | } |
29967ef6 XL |
2721 | |
2722 | /// Gets an iterator of all type parameters. | |
a2a8927a | 2723 | pub fn type_parameters<'a>(&'a self, interner: I) -> impl Iterator<Item = Ty<I>> + 'a { |
29967ef6 XL |
2724 | self.iter(interner) |
2725 | .filter_map(move |p| p.ty(interner)) | |
2726 | .cloned() | |
2727 | } | |
a2a8927a XL |
2728 | |
2729 | /// Compute type flags for Substitution<I> | |
2730 | fn compute_flags(&self, interner: I) -> TypeFlags { | |
2731 | let mut flags = TypeFlags::empty(); | |
2732 | for generic_arg in self.iter(interner) { | |
2733 | flags |= generic_arg.compute_flags(interner); | |
2734 | } | |
2735 | flags | |
2736 | } | |
f9f354fc XL |
2737 | } |
2738 | ||
5869c6ff | 2739 | struct SubstFolder<'i, I: Interner, A: AsParameters<I>> { |
a2a8927a | 2740 | interner: I, |
5869c6ff | 2741 | subst: &'i A, |
f9f354fc XL |
2742 | } |
2743 | ||
5869c6ff | 2744 | impl<I: Interner, A: AsParameters<I>> SubstFolder<'_, I, A> { |
f035d41b XL |
2745 | /// Index into the list of parameters. |
2746 | pub fn at(&self, index: usize) -> &GenericArg<I> { | |
f9f354fc | 2747 | let interner = self.interner; |
5869c6ff | 2748 | &self.subst.as_parameters(interner)[index] |
f9f354fc XL |
2749 | } |
2750 | } | |
2751 | ||
f035d41b | 2752 | /// Convert a value to a list of parameters. |
f9f354fc | 2753 | pub trait AsParameters<I: Interner> { |
f035d41b | 2754 | /// Convert the current value to parameters. |
a2a8927a | 2755 | fn as_parameters(&self, interner: I) -> &[GenericArg<I>]; |
f9f354fc XL |
2756 | } |
2757 | ||
2758 | impl<I: Interner> AsParameters<I> for Substitution<I> { | |
2759 | #[allow(unreachable_code, unused_variables)] | |
a2a8927a | 2760 | fn as_parameters(&self, interner: I) -> &[GenericArg<I>] { |
3dfed10e | 2761 | self.as_slice(interner) |
f9f354fc XL |
2762 | } |
2763 | } | |
2764 | ||
f035d41b | 2765 | impl<I: Interner> AsParameters<I> for [GenericArg<I>] { |
a2a8927a | 2766 | fn as_parameters(&self, _interner: I) -> &[GenericArg<I>] { |
f9f354fc XL |
2767 | self |
2768 | } | |
2769 | } | |
2770 | ||
f035d41b | 2771 | impl<I: Interner> AsParameters<I> for [GenericArg<I>; 1] { |
a2a8927a | 2772 | fn as_parameters(&self, _interner: I) -> &[GenericArg<I>] { |
f9f354fc XL |
2773 | self |
2774 | } | |
2775 | } | |
2776 | ||
f035d41b | 2777 | impl<I: Interner> AsParameters<I> for Vec<GenericArg<I>> { |
a2a8927a | 2778 | fn as_parameters(&self, _interner: I) -> &[GenericArg<I>] { |
f9f354fc XL |
2779 | self |
2780 | } | |
2781 | } | |
2782 | ||
2783 | impl<T, I: Interner> AsParameters<I> for &T | |
2784 | where | |
2785 | T: ?Sized + AsParameters<I>, | |
2786 | { | |
a2a8927a | 2787 | fn as_parameters(&self, interner: I) -> &[GenericArg<I>] { |
f9f354fc XL |
2788 | T::as_parameters(self, interner) |
2789 | } | |
2790 | } | |
2791 | ||
5869c6ff XL |
2792 | /// An extension trait to anything that can be represented as list of `GenericArg`s that signifies |
2793 | /// that it can applied as a substituion to a value | |
2794 | pub trait Substitute<I: Interner>: AsParameters<I> { | |
2795 | /// Apply the substitution to a value. | |
a2a8927a | 2796 | fn apply<T: Fold<I>>(&self, value: T, interner: I) -> T::Result; |
5869c6ff XL |
2797 | } |
2798 | ||
2799 | impl<I: Interner, A: AsParameters<I>> Substitute<I> for A { | |
a2a8927a | 2800 | fn apply<T>(&self, value: T, interner: I) -> T::Result |
5869c6ff XL |
2801 | where |
2802 | T: Fold<I>, | |
2803 | { | |
2804 | value | |
2805 | .fold_with( | |
2806 | &mut &SubstFolder { | |
2807 | interner, | |
2808 | subst: self, | |
2809 | }, | |
2810 | DebruijnIndex::INNERMOST, | |
2811 | ) | |
2812 | .unwrap() | |
2813 | } | |
2814 | } | |
2815 | ||
f035d41b XL |
2816 | /// Utility for converting a list of all the binders into scope |
2817 | /// into references to those binders. Simply pair the binders with | |
2818 | /// the indices, and invoke `to_generic_arg()` on the `(binder, | |
2819 | /// index)` pair. The result will be a reference to a bound | |
2820 | /// variable of appropriate kind at the corresponding index. | |
2821 | pub trait ToGenericArg<I: Interner> { | |
2822 | /// Converts the binders in scope to references to those binders. | |
a2a8927a | 2823 | fn to_generic_arg(&self, interner: I) -> GenericArg<I> { |
f035d41b XL |
2824 | self.to_generic_arg_at_depth(interner, DebruijnIndex::INNERMOST) |
2825 | } | |
2826 | ||
2827 | /// Converts the binders at the specified depth to references to those binders. | |
a2a8927a | 2828 | fn to_generic_arg_at_depth(&self, interner: I, debruijn: DebruijnIndex) -> GenericArg<I>; |
f035d41b XL |
2829 | } |
2830 | ||
2831 | impl<'a, I: Interner> ToGenericArg<I> for (usize, &'a VariableKind<I>) { | |
a2a8927a | 2832 | fn to_generic_arg_at_depth(&self, interner: I, debruijn: DebruijnIndex) -> GenericArg<I> { |
f035d41b XL |
2833 | let &(index, binder) = self; |
2834 | let bound_var = BoundVar::new(debruijn, index); | |
2835 | binder.to_bound_variable(interner, bound_var) | |
2836 | } | |
2837 | } | |
2838 | ||
a2a8927a XL |
2839 | impl<'i, I: Interner, A: AsParameters<I>> Folder<I> for &SubstFolder<'i, I, A> { |
2840 | type Error = NoSolution; | |
2841 | ||
2842 | fn as_dyn(&mut self) -> &mut dyn Folder<I, Error = Self::Error> { | |
f9f354fc XL |
2843 | self |
2844 | } | |
2845 | ||
2846 | fn fold_free_var_ty( | |
2847 | &mut self, | |
2848 | bound_var: BoundVar, | |
2849 | outer_binder: DebruijnIndex, | |
2850 | ) -> Fallible<Ty<I>> { | |
2851 | assert_eq!(bound_var.debruijn, DebruijnIndex::INNERMOST); | |
2852 | let ty = self.at(bound_var.index); | |
2853 | let ty = ty.assert_ty_ref(self.interner()); | |
5869c6ff | 2854 | Ok(ty.clone().shifted_in_from(self.interner(), outer_binder)) |
f9f354fc XL |
2855 | } |
2856 | ||
2857 | fn fold_free_var_lifetime( | |
2858 | &mut self, | |
2859 | bound_var: BoundVar, | |
2860 | outer_binder: DebruijnIndex, | |
2861 | ) -> Fallible<Lifetime<I>> { | |
2862 | assert_eq!(bound_var.debruijn, DebruijnIndex::INNERMOST); | |
2863 | let l = self.at(bound_var.index); | |
2864 | let l = l.assert_lifetime_ref(self.interner()); | |
5869c6ff | 2865 | Ok(l.clone().shifted_in_from(self.interner(), outer_binder)) |
f9f354fc XL |
2866 | } |
2867 | ||
f035d41b XL |
2868 | fn fold_free_var_const( |
2869 | &mut self, | |
5869c6ff | 2870 | _ty: Ty<I>, |
f035d41b XL |
2871 | bound_var: BoundVar, |
2872 | outer_binder: DebruijnIndex, | |
2873 | ) -> Fallible<Const<I>> { | |
2874 | assert_eq!(bound_var.debruijn, DebruijnIndex::INNERMOST); | |
2875 | let c = self.at(bound_var.index); | |
2876 | let c = c.assert_const_ref(self.interner()); | |
5869c6ff | 2877 | Ok(c.clone().shifted_in_from(self.interner(), outer_binder)) |
f035d41b XL |
2878 | } |
2879 | ||
a2a8927a | 2880 | fn interner(&self) -> I { |
f9f354fc XL |
2881 | self.interner |
2882 | } | |
f9f354fc XL |
2883 | } |
2884 | ||
5869c6ff | 2885 | macro_rules! interned_slice_common { |
3dfed10e XL |
2886 | ($seq:ident, $data:ident => $elem:ty, $intern:ident => $interned:ident) => { |
2887 | /// List of interned elements. | |
2888 | #[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord, HasInterner)] | |
2889 | pub struct $seq<I: Interner> { | |
2890 | interned: I::$interned, | |
2891 | } | |
2892 | ||
2893 | impl<I: Interner> $seq<I> { | |
2894 | /// Get the interned elements. | |
2895 | pub fn interned(&self) -> &I::$interned { | |
2896 | &self.interned | |
2897 | } | |
5869c6ff XL |
2898 | |
2899 | /// Returns a slice containing the elements. | |
a2a8927a | 2900 | pub fn as_slice(&self, interner: I) -> &[$elem] { |
5869c6ff XL |
2901 | Interner::$data(interner, &self.interned) |
2902 | } | |
2903 | ||
2904 | /// Index into the sequence. | |
a2a8927a | 2905 | pub fn at(&self, interner: I, index: usize) -> &$elem { |
5869c6ff XL |
2906 | &self.as_slice(interner)[index] |
2907 | } | |
2908 | ||
2909 | /// Create an empty sequence. | |
a2a8927a | 2910 | pub fn empty(interner: I) -> Self { |
5869c6ff XL |
2911 | Self::from_iter(interner, None::<$elem>) |
2912 | } | |
2913 | ||
2914 | /// Check whether this is an empty sequence. | |
a2a8927a | 2915 | pub fn is_empty(&self, interner: I) -> bool { |
5869c6ff XL |
2916 | self.as_slice(interner).is_empty() |
2917 | } | |
2918 | ||
2919 | /// Get an iterator over the elements of the sequence. | |
a2a8927a | 2920 | pub fn iter(&self, interner: I) -> std::slice::Iter<'_, $elem> { |
5869c6ff XL |
2921 | self.as_slice(interner).iter() |
2922 | } | |
2923 | ||
2924 | /// Get the length of the sequence. | |
a2a8927a | 2925 | pub fn len(&self, interner: I) -> usize { |
5869c6ff XL |
2926 | self.as_slice(interner).len() |
2927 | } | |
3dfed10e | 2928 | } |
5869c6ff XL |
2929 | }; |
2930 | } | |
2931 | ||
2932 | macro_rules! interned_slice { | |
2933 | ($seq:ident, $data:ident => $elem:ty, $intern:ident => $interned:ident) => { | |
2934 | interned_slice_common!($seq, $data => $elem, $intern => $interned); | |
3dfed10e XL |
2935 | |
2936 | impl<I: Interner> $seq<I> { | |
2937 | /// Tries to create a sequence using an iterator of element-like things. | |
2938 | pub fn from_fallible<E>( | |
a2a8927a | 2939 | interner: I, |
3dfed10e XL |
2940 | elements: impl IntoIterator<Item = Result<impl CastTo<$elem>, E>>, |
2941 | ) -> Result<Self, E> { | |
2942 | Ok(Self { | |
2943 | interned: I::$intern(interner, elements.into_iter().casted(interner))?, | |
2944 | }) | |
2945 | } | |
2946 | ||
3dfed10e XL |
2947 | /// Create a sequence from elements |
2948 | pub fn from_iter( | |
a2a8927a | 2949 | interner: I, |
3dfed10e XL |
2950 | elements: impl IntoIterator<Item = impl CastTo<$elem>>, |
2951 | ) -> Self { | |
2952 | Self::from_fallible( | |
2953 | interner, | |
2954 | elements | |
2955 | .into_iter() | |
2956 | .map(|el| -> Result<$elem, ()> { Ok(el.cast(interner)) }), | |
2957 | ) | |
2958 | .unwrap() | |
2959 | } | |
2960 | ||
3dfed10e | 2961 | /// Create a sequence from a single element. |
a2a8927a | 2962 | pub fn from1(interner: I, element: impl CastTo<$elem>) -> Self { |
3dfed10e XL |
2963 | Self::from_iter(interner, Some(element)) |
2964 | } | |
3dfed10e XL |
2965 | } |
2966 | }; | |
2967 | } | |
2968 | ||
2969 | interned_slice!( | |
2970 | QuantifiedWhereClauses, | |
2971 | quantified_where_clauses_data => QuantifiedWhereClause<I>, | |
2972 | intern_quantified_where_clauses => InternedQuantifiedWhereClauses | |
2973 | ); | |
2974 | ||
2975 | interned_slice!( | |
2976 | ProgramClauses, | |
2977 | program_clauses_data => ProgramClause<I>, | |
2978 | intern_program_clauses => InternedProgramClauses | |
2979 | ); | |
2980 | ||
2981 | interned_slice!( | |
2982 | VariableKinds, | |
2983 | variable_kinds_data => VariableKind<I>, | |
2984 | intern_generic_arg_kinds => InternedVariableKinds | |
2985 | ); | |
2986 | ||
2987 | interned_slice!( | |
2988 | CanonicalVarKinds, | |
2989 | canonical_var_kinds_data => CanonicalVarKind<I>, | |
2990 | intern_canonical_var_kinds => InternedCanonicalVarKinds | |
2991 | ); | |
2992 | ||
2993 | interned_slice!(Goals, goals_data => Goal<I>, intern_goals => InternedGoals); | |
2994 | ||
2995 | interned_slice!( | |
2996 | Constraints, | |
2997 | constraints_data => InEnvironment<Constraint<I>>, | |
2998 | intern_constraints => InternedConstraints | |
2999 | ); | |
3000 | ||
3001 | interned_slice!( | |
3002 | Substitution, | |
3003 | substitution_data => GenericArg<I>, | |
3004 | intern_substitution => InternedSubstitution | |
3005 | ); | |
3006 | ||
5869c6ff XL |
3007 | interned_slice_common!( |
3008 | Variances, | |
3009 | variances_data => Variance, | |
3010 | intern_variance => InternedVariances | |
3011 | ); | |
3012 | ||
3013 | impl<I: Interner> Variances<I> { | |
3014 | /// Tries to create a list of canonical variable kinds using an iterator. | |
3015 | pub fn from_fallible<E>( | |
a2a8927a | 3016 | interner: I, |
5869c6ff XL |
3017 | variances: impl IntoIterator<Item = Result<Variance, E>>, |
3018 | ) -> Result<Self, E> { | |
3019 | Ok(Variances { | |
3020 | interned: I::intern_variances(interner, variances.into_iter())?, | |
3021 | }) | |
3022 | } | |
3023 | ||
3024 | /// Creates a list of canonical variable kinds using an iterator. | |
a2a8927a | 3025 | pub fn from_iter(interner: I, variances: impl IntoIterator<Item = Variance>) -> Self { |
5869c6ff XL |
3026 | Self::from_fallible( |
3027 | interner, | |
3028 | variances | |
3029 | .into_iter() | |
3030 | .map(|p| -> Result<Variance, ()> { Ok(p) }), | |
3031 | ) | |
3032 | .unwrap() | |
3033 | } | |
3034 | ||
3035 | /// Creates a list of canonical variable kinds from a single canonical variable kind. | |
a2a8927a | 3036 | pub fn from1(interner: I, variance: Variance) -> Self { |
5869c6ff XL |
3037 | Self::from_iter(interner, Some(variance)) |
3038 | } | |
3039 | } | |
3040 | ||
f9f354fc XL |
3041 | /// Combines a substitution (`subst`) with a set of region constraints |
3042 | /// (`constraints`). This represents the result of a query; the | |
3043 | /// substitution stores the values for the query's unknown variables, | |
3044 | /// and the constraints represents any region constraints that must | |
3045 | /// additionally be solved. | |
3046 | #[derive(Clone, Debug, PartialEq, Eq, Hash, Fold, Visit, HasInterner)] | |
3047 | pub struct ConstrainedSubst<I: Interner> { | |
f035d41b XL |
3048 | /// The substitution that is being constrained. |
3049 | /// | |
3050 | /// NB: The `is_trivial` routine relies on the fact that `subst` is folded first. | |
3051 | pub subst: Substitution<I>, | |
3052 | ||
3053 | /// Region constraints that constrain the substitution. | |
3dfed10e | 3054 | pub constraints: Constraints<I>, |
f9f354fc XL |
3055 | } |
3056 | ||
f035d41b | 3057 | /// The resulting substitution after solving a goal. |
f9f354fc XL |
3058 | #[derive(Clone, Debug, PartialEq, Eq, Hash, Fold, Visit, HasInterner)] |
3059 | pub struct AnswerSubst<I: Interner> { | |
f035d41b XL |
3060 | /// The substitution result. |
3061 | /// | |
3062 | /// NB: The `is_trivial` routine relies on the fact that `subst` is folded first. | |
3063 | pub subst: Substitution<I>, | |
3064 | ||
3065 | /// List of constraints that are part of the answer. | |
3dfed10e | 3066 | pub constraints: Constraints<I>, |
f035d41b XL |
3067 | |
3068 | /// Delayed subgoals, used when the solver answered with an (incomplete) `Answer` (instead of a `CompleteAnswer`). | |
f9f354fc XL |
3069 | pub delayed_subgoals: Vec<InEnvironment<Goal<I>>>, |
3070 | } | |
5869c6ff XL |
3071 | |
3072 | /// Logic to decide the Variance for a given subst | |
3073 | pub trait UnificationDatabase<I> | |
3074 | where | |
3075 | Self: std::fmt::Debug, | |
3076 | I: Interner, | |
3077 | { | |
3078 | /// Gets the variances for the substitution of a fn def | |
3079 | fn fn_def_variance(&self, fn_def_id: FnDefId<I>) -> Variances<I>; | |
3080 | ||
3081 | /// Gets the variances for the substitution of a adt | |
3082 | fn adt_variance(&self, adt_id: AdtId<I>) -> Variances<I>; | |
3083 | } |