1use crate::{
2 Db,
3 check::inference::InferVarKind,
4 ir::{
5 binder::LeafBoundTerm,
6 classes::{SymAggregate, SymField},
7 indices::{FromInfer, FromInferVar, InferVarIndex},
8 primitive::{SymPrimitive, SymPrimitiveKind},
9 variables::{FromVar, SymVariable},
10 },
11 prelude::Symbol,
12 well_known,
13};
14use dada_ir_ast::{
15 ast::{AstGenericDecl, AstGenericKind, AstPerm, AstPermKind, AstSelfArg, VariableDecl},
16 diagnostic::{Err, Errors, Reported},
17 span::Spanned,
18};
19use dada_util::{FromImpls, SalsaSerialize};
20use salsa::Update;
21use serde::Serialize;
22
23use super::classes::SymAggregateStyle;
24
25#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Debug, Serialize)]
26pub struct Variance {
27 pub at_least_covariant: bool,
29
30 pub at_least_contravariant: bool,
32
33 pub relative: bool,
47}
48
49impl Variance {
50 pub fn covariant() -> Self {
51 Self {
52 at_least_covariant: true,
53 at_least_contravariant: false,
54 relative: false,
55 }
56 }
57}
58
59#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Update, Debug, Serialize)]
60pub enum SymGenericKind {
61 Type,
62 Perm,
63 Place,
64}
65
66impl std::fmt::Display for SymGenericKind {
67 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
68 match self {
69 Self::Type => write!(f, "type"),
70 Self::Perm => write!(f, "perm"),
71 Self::Place => write!(f, "place"),
72 }
73 }
74}
75
76pub trait HasKind<'db> {
80 fn has_kind(&self, db: &'db dyn crate::Db, kind: SymGenericKind) -> bool;
81}
82
83pub trait AssertKind<'db, R> {
86 fn assert_kind(self, db: &'db dyn crate::Db) -> R;
87}
88
89#[derive(
91 Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Update, Debug, FromImpls, Serialize,
92)]
93pub enum SymGenericTerm<'db> {
94 Type(SymTy<'db>),
95 Perm(SymPerm<'db>),
96 Place(SymPlace<'db>),
97 Error(Reported),
98}
99
100impl<'db> Err<'db> for SymGenericTerm<'db> {
101 fn err(_db: &'db dyn crate::Db, reported: Reported) -> Self {
102 SymGenericTerm::Error(reported)
103 }
104}
105
106impl std::fmt::Display for SymGenericTerm<'_> {
107 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
108 match self {
109 SymGenericTerm::Type(ty) => write!(f, "{ty}"),
110 SymGenericTerm::Perm(perm) => write!(f, "{perm}"),
111 SymGenericTerm::Place(place) => write!(f, "{place}"),
112 SymGenericTerm::Error(_) => write!(f, "<error>"),
113 }
114 }
115}
116
117impl<'db> HasKind<'db> for SymGenericTerm<'db> {
118 fn has_kind(&self, _db: &'db dyn crate::Db, kind: SymGenericKind) -> bool {
119 match self {
120 SymGenericTerm::Type(_) => kind == SymGenericKind::Type,
121 SymGenericTerm::Perm(_) => kind == SymGenericKind::Perm,
122 SymGenericTerm::Place(_) => kind == SymGenericKind::Place,
123 SymGenericTerm::Error(Reported(_)) => true,
124 }
125 }
126}
127
128impl<'db> AssertKind<'db, SymTy<'db>> for SymGenericTerm<'db> {
129 fn assert_kind(self, db: &'db dyn crate::Db) -> SymTy<'db> {
130 assert!(self.has_kind(db, SymGenericKind::Type));
131 match self {
132 SymGenericTerm::Type(v) => v,
133 SymGenericTerm::Error(r) => SymTy::err(db, r),
134 _ => unreachable!(),
135 }
136 }
137}
138
139impl<'db> AssertKind<'db, SymPerm<'db>> for SymGenericTerm<'db> {
140 fn assert_kind(self, db: &'db dyn crate::Db) -> SymPerm<'db> {
141 assert!(self.has_kind(db, SymGenericKind::Perm));
142 match self {
143 SymGenericTerm::Perm(v) => v,
144 SymGenericTerm::Error(r) => SymPerm::err(db, r),
145 _ => unreachable!(),
146 }
147 }
148}
149
150impl<'db> AssertKind<'db, SymPlace<'db>> for SymGenericTerm<'db> {
151 fn assert_kind(self, db: &'db dyn crate::Db) -> SymPlace<'db> {
152 assert!(self.has_kind(db, SymGenericKind::Place));
153 match self {
154 SymGenericTerm::Place(v) => v,
155 SymGenericTerm::Error(r) => SymPlace::err(db, r),
156 _ => unreachable!(),
157 }
158 }
159}
160
161impl<'db> FromVar<'db> for SymGenericTerm<'db> {
162 fn var(db: &'db dyn crate::Db, var: SymVariable<'db>) -> Self {
163 match var.kind(db) {
164 SymGenericKind::Type => SymTy::var(db, var).into(),
165 SymGenericKind::Perm => SymPerm::var(db, var).into(),
166 SymGenericKind::Place => SymPlace::var(db, var).into(),
167 }
168 }
169}
170
171impl<'db> FromInferVar<'db> for SymGenericTerm<'db> {
172 fn infer(db: &'db dyn crate::Db, kind: SymGenericKind, index: InferVarIndex) -> Self {
173 match kind {
174 SymGenericKind::Type => SymTy::new(db, SymTyKind::Infer(index)).into(),
175 SymGenericKind::Perm => SymPerm::new(db, SymPermKind::Infer(index)).into(),
176 SymGenericKind::Place => panic!("no inference variables for a place"),
177 }
178 }
179}
180
181impl<'db> SymGenericTerm<'db> {
182 #[track_caller]
183 pub fn assert_type(self, db: &'db dyn crate::Db) -> SymTy<'db> {
184 match self {
185 SymGenericTerm::Type(ty) => ty,
186 SymGenericTerm::Error(reported) => SymTy::new(db, SymTyKind::Error(reported)),
187 _ => unreachable!(),
188 }
189 }
190
191 #[track_caller]
192 pub fn assert_perm(self, db: &'db dyn crate::Db) -> SymPerm<'db> {
193 match self {
194 SymGenericTerm::Perm(perm) => perm,
195 SymGenericTerm::Error(reported) => SymPerm::new(db, SymPermKind::Error(reported)),
196 _ => unreachable!(),
197 }
198 }
199
200 #[track_caller]
201 pub fn assert_place(self, db: &'db dyn crate::Db) -> SymPlace<'db> {
202 match self {
203 SymGenericTerm::Place(place) => place,
204 SymGenericTerm::Error(reported) => SymPlace::new(db, SymPlaceKind::Error(reported)),
205 _ => unreachable!(),
206 }
207 }
208
209 pub fn kind(self) -> Errors<SymGenericKind> {
211 match self {
212 SymGenericTerm::Type(_) => Ok(SymGenericKind::Type),
213 SymGenericTerm::Perm(_) => Ok(SymGenericKind::Perm),
214 SymGenericTerm::Place(_) => Ok(SymGenericKind::Place),
215 SymGenericTerm::Error(r) => Err(r),
216 }
217 }
218
219 pub fn has_kind(self, _db: &'db dyn crate::Db, kind: SymGenericKind) -> bool {
221 match self {
222 SymGenericTerm::Type(_) => kind == SymGenericKind::Type,
223 SymGenericTerm::Perm(_) => kind == SymGenericKind::Perm,
224 SymGenericTerm::Place(_) => kind == SymGenericKind::Place,
225 SymGenericTerm::Error(_) => true,
226 }
227 }
228
229 pub fn as_infer(self, db: &'db dyn crate::Db) -> Option<InferVarIndex> {
231 match self {
232 SymGenericTerm::Type(ty) => match ty.kind(db) {
233 SymTyKind::Infer(infer) => Some(*infer),
234 SymTyKind::Var(..)
235 | SymTyKind::Named(..)
236 | SymTyKind::Never
237 | SymTyKind::Error(_)
238 | SymTyKind::Perm(..) => None,
239 },
240 SymGenericTerm::Perm(perm) => match perm.kind(db) {
241 SymPermKind::Infer(infer) => Some(*infer),
242 SymPermKind::My
243 | SymPermKind::Our
244 | SymPermKind::Referenced(_)
245 | SymPermKind::Mutable(_)
246 | SymPermKind::Var(_)
247 | SymPermKind::Error(_)
248 | SymPermKind::Or(..)
249 | SymPermKind::Apply(..) => None,
250 },
251 SymGenericTerm::Place(place) => match place.kind(db) {
252 SymPlaceKind::Var(_)
253 | SymPlaceKind::Erased
254 | SymPlaceKind::Field(..)
255 | SymPlaceKind::Index(..)
256 | SymPlaceKind::Error(..) => None,
257 },
258 SymGenericTerm::Error(_) => None,
259 }
260 }
261
262 pub fn describe(&self) -> String {
264 match self {
265 SymGenericTerm::Type(sym_ty) => format!("type `{sym_ty}`"),
266 SymGenericTerm::Perm(sym_perm) => format!("permission `{sym_perm}`"),
267 SymGenericTerm::Place(sym_place) => format!("place `{sym_place}`"),
268 SymGenericTerm::Error(_) => "(error)".to_string(),
269 }
270 }
271
272 pub fn fallback(db: &'db dyn crate::Db, kind: InferVarKind) -> Self {
273 match kind {
274 InferVarKind::Type => SymTy::fallback(db).into(),
275 InferVarKind::Perm => SymPerm::fallback(db).into(),
276 }
277 }
278}
279
280#[derive(SalsaSerialize)]
281#[salsa::interned(debug)]
282pub struct SymTy<'db> {
283 #[return_ref]
284 pub kind: SymTyKind<'db>,
285}
286
287impl<'db> SymTy<'db> {
288 pub fn primitive(db: &'db dyn Db, primitive: SymPrimitiveKind) -> Self {
290 SymTy::named(db, primitive.intern(db).into(), vec![])
291 }
292
293 pub fn u8(db: &'db dyn Db) -> Self {
295 SymTy::primitive(db, SymPrimitiveKind::Uint { bits: 8 })
296 }
297
298 pub fn u32(db: &'db dyn Db) -> Self {
300 SymTy::primitive(db, SymPrimitiveKind::Uint { bits: 32 })
301 }
302
303 pub fn string(db: &'db dyn Db) -> Self {
305 let string_class = match well_known::string_class(db) {
306 Ok(v) => v,
307 Err(reported) => return SymTy::err(db, reported),
308 };
309 SymTy::named(db, string_class.into(), vec![])
310 }
311
312 pub fn named(
314 db: &'db dyn Db,
315 name: SymTyName<'db>,
316 generics: Vec<SymGenericTerm<'db>>,
317 ) -> Self {
318 SymTy::new(db, SymTyKind::Named(name, generics))
319 }
320
321 pub fn var(db: &'db dyn Db, var: SymVariable<'db>) -> Self {
323 SymTy::new(db, SymTyKind::Var(var))
324 }
325
326 pub fn unit(db: &'db dyn Db) -> Self {
328 #[salsa::tracked]
329 fn unit_ty<'db>(db: &'db dyn Db) -> SymTy<'db> {
330 SymTy::named(db, SymTyName::Tuple { arity: 0 }, vec![])
331 }
332
333 unit_ty(db)
334 }
335
336 pub fn boolean(db: &'db dyn Db) -> Self {
338 SymTy::named(db, SymPrimitiveKind::Bool.intern(db).into(), vec![])
339 }
340
341 pub fn fallback(db: &'db dyn Db) -> Self {
344 Self::never(db)
345 }
346
347 pub fn never(db: &'db dyn Db) -> Self {
349 #[salsa::tracked]
350 fn never_ty<'db>(db: &'db dyn Db) -> SymTy<'db> {
351 SymTy::new(db, SymTyKind::Never)
352 }
353
354 never_ty(db)
355 }
356
357 pub fn perm(db: &'db dyn Db, perm: SymPerm<'db>, ty: SymTy<'db>) -> Self {
359 SymTy::new(db, SymTyKind::Perm(perm, ty))
360 }
361
362 pub fn referenced(self, db: &'db dyn Db, place: SymPlace<'db>) -> Self {
364 SymTy::new(
365 db,
366 SymTyKind::Perm(SymPerm::referenced(db, vec![place]), self),
367 )
368 }
369
370 pub fn mutable(self, db: &'db dyn Db, place: SymPlace<'db>) -> Self {
372 SymTy::new(db, SymTyKind::Perm(SymPerm::mutable(db, vec![place]), self))
373 }
374
375 pub fn shared(self, db: &'db dyn Db) -> Self {
377 SymTy::new(db, SymTyKind::Perm(SymPerm::our(db), self))
378 }
379}
380
381impl<'db> FromInfer<'db> for SymTy<'db> {
382 fn infer(db: &'db dyn crate::Db, var: InferVarIndex) -> Self {
383 SymTy::new(db, SymTyKind::Infer(var))
384 }
385}
386
387impl std::fmt::Display for SymTy<'_> {
388 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
389 salsa::with_attached_database(|db| match self.kind(db) {
390 SymTyKind::Named(name, generics) => {
391 if generics.is_empty() {
392 write!(f, "{name}")
393 } else {
394 write!(
395 f,
396 "{name}[{}]",
397 generics
398 .iter()
399 .map(|g| g.to_string())
400 .collect::<Vec<_>>()
401 .join(", ")
402 )
403 }
404 }
405 SymTyKind::Perm(sym_perm, sym_ty) => write!(f, "{sym_perm} {sym_ty}"),
406 SymTyKind::Infer(infer_var_index) => write!(f, "?{}", infer_var_index.as_usize()),
407 SymTyKind::Var(sym_variable) => write!(f, "{sym_variable}"),
408 SymTyKind::Never => write!(f, "!"),
409 SymTyKind::Error(_) => write!(f, "<error>"),
410 })
411 .unwrap_or_else(|| std::fmt::Debug::fmt(self, f))
412 }
413}
414
415impl<'db> LeafBoundTerm<'db> for SymTy<'db> {}
416
417impl<'db> Err<'db> for SymTy<'db> {
418 fn err(db: &'db dyn dada_ir_ast::Db, reported: Reported) -> Self {
419 SymTy::new(db, SymTyKind::Error(reported))
420 }
421}
422
423impl<'db> HasKind<'db> for SymTy<'db> {
424 fn has_kind(&self, _db: &'db dyn crate::Db, kind: SymGenericKind) -> bool {
425 kind == SymGenericKind::Type
426 }
427}
428
429impl<'db> FromVar<'db> for SymTy<'db> {
430 fn var(db: &'db dyn crate::Db, var: SymVariable<'db>) -> Self {
431 assert_eq!(var.kind(db), SymGenericKind::Type);
432 SymTy::new(db, SymTyKind::Var(var))
433 }
434}
435
436#[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Update, Debug, Serialize)]
437pub enum SymTyKind<'db> {
438 Perm(SymPerm<'db>, SymTy<'db>),
440
441 Named(SymTyName<'db>, Vec<SymGenericTerm<'db>>),
445
446 Infer(InferVarIndex),
448
449 Var(SymVariable<'db>),
451
452 Never,
454
455 Error(Reported),
457}
458
459#[derive(
460 Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Update, Debug, FromImpls, Serialize,
461)]
462pub enum SymTyName<'db> {
463 Primitive(SymPrimitive<'db>),
464
465 Aggregate(SymAggregate<'db>),
466
467 #[no_from_impl]
469 Future,
470
471 #[no_from_impl]
472 Tuple {
473 arity: usize,
474 },
475}
476
477impl<'db> SymTyName<'db> {
478 pub fn style(self, db: &'db dyn crate::Db) -> SymAggregateStyle {
480 match self {
481 SymTyName::Primitive(_) => SymAggregateStyle::Struct,
482 SymTyName::Aggregate(sym_aggregate) => sym_aggregate.style(db),
483 SymTyName::Future => SymAggregateStyle::Class,
484 SymTyName::Tuple { arity: _ } => SymAggregateStyle::Struct,
485 }
486 }
487}
488
489impl std::fmt::Display for SymTyName<'_> {
490 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
491 salsa::with_attached_database(|db| {
492 let db: &dyn crate::Db = db.as_view();
493 match self {
494 SymTyName::Primitive(primitive) => write!(f, "{primitive}"),
495 SymTyName::Aggregate(class) => write!(f, "{}", class.name(db)),
496 SymTyName::Tuple { arity } => write!(f, "{arity}-tuple"),
497 SymTyName::Future => write!(f, "Future"),
498 }
499 })
500 .unwrap_or_else(|| std::fmt::Debug::fmt(self, f))
501 }
502}
503
504#[derive(SalsaSerialize)]
505#[salsa::interned(debug)]
506pub struct SymPerm<'db> {
507 #[return_ref]
508 pub kind: SymPermKind<'db>,
509}
510
511impl<'db> SymPerm<'db> {
512 pub fn fallback(db: &'db dyn crate::Db) -> Self {
515 Self::my(db)
516 }
517
518 pub fn my(db: &'db dyn crate::Db) -> Self {
520 SymPerm::new(db, SymPermKind::My)
521 }
522
523 pub fn our(db: &'db dyn crate::Db) -> Self {
525 SymPerm::new(db, SymPermKind::Our)
526 }
527
528 pub fn referenced(db: &'db dyn crate::Db, places: Vec<SymPlace<'db>>) -> Self {
530 SymPerm::new(db, SymPermKind::Referenced(places))
531 }
532
533 pub fn mutable(db: &'db dyn crate::Db, places: Vec<SymPlace<'db>>) -> Self {
535 SymPerm::new(db, SymPermKind::Mutable(places))
536 }
537
538 pub fn var(db: &'db dyn crate::Db, var: SymVariable<'db>) -> Self {
540 SymPerm::new(db, SymPermKind::Var(var))
541 }
542
543 pub fn apply(db: &'db dyn crate::Db, perm1: SymPerm<'db>, perm2: SymPerm<'db>) -> Self {
545 SymPerm::new(db, SymPermKind::Apply(perm1, perm2))
546 }
547
548 pub fn or(db: &'db dyn crate::Db, perm1: SymPerm<'db>, perm2: SymPerm<'db>) -> Self {
550 SymPerm::new(db, SymPermKind::Or(perm1, perm2))
551 }
552
553 pub fn apply_to<T>(self, db: &'db dyn crate::Db, term: T) -> T
555 where
556 T: Applicable<'db>,
557 {
558 match self.kind(db) {
559 SymPermKind::My => term,
560 _ => term.apply_from(db, self),
561 }
562 }
563}
564
565pub trait Applicable<'db> {
566 fn apply_from(self, db: &'db dyn crate::Db, perm: SymPerm<'db>) -> Self;
567}
568
569impl<'db> Applicable<'db> for SymGenericTerm<'db> {
570 fn apply_from(self, db: &'db dyn crate::Db, perm: SymPerm<'db>) -> Self {
571 match self {
572 SymGenericTerm::Type(ty) => ty.apply_from(db, perm).into(),
573 SymGenericTerm::Perm(perm1) => perm1.apply_from(db, perm).into(),
574 SymGenericTerm::Place(_) => panic!("cannot apply a perm to a place"),
575 SymGenericTerm::Error(_) => self,
576 }
577 }
578}
579
580impl<'db> Applicable<'db> for SymTy<'db> {
581 fn apply_from(self, db: &'db dyn crate::Db, perm: SymPerm<'db>) -> Self {
582 SymTy::perm(db, perm, self)
583 }
584}
585
586impl<'db> Applicable<'db> for SymPerm<'db> {
587 fn apply_from(self, db: &'db dyn crate::Db, perm: SymPerm<'db>) -> Self {
588 match self.kind(db) {
589 SymPermKind::My => perm,
590 _ => SymPerm::apply(db, perm, self),
591 }
592 }
593}
594
595impl<'db> FromInfer<'db> for SymPerm<'db> {
596 fn infer(db: &'db dyn crate::Db, var: InferVarIndex) -> Self {
597 SymPerm::new(db, SymPermKind::Infer(var))
598 }
599}
600
601impl std::fmt::Display for SymPerm<'_> {
602 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
603 salsa::with_attached_database(|db| {
604 let db: &dyn crate::Db = db.as_view();
605 match self.kind(db) {
606 SymPermKind::My => write!(f, "my"),
607 SymPermKind::Our => write!(f, "our"),
608 SymPermKind::Referenced(places) => {
609 write!(f, "ref[")?;
610 for (i, place) in places.iter().enumerate() {
611 if i > 0 {
612 write!(f, ", ")?;
613 }
614 write!(f, "{place}")?;
615 }
616 write!(f, "]")
617 }
618 SymPermKind::Mutable(places) => {
619 write!(f, "mutable[")?;
620 for (i, place) in places.iter().enumerate() {
621 if i > 0 {
622 write!(f, ", ")?;
623 }
624 write!(f, "{place}")?;
625 }
626 write!(f, "]")
627 }
628 SymPermKind::Apply(perm1, perm2) => write!(f, "{perm1} {perm2}"),
629 SymPermKind::Infer(infer_var_index) => write!(f, "?{}", infer_var_index.as_usize()),
630 SymPermKind::Var(sym_variable) => write!(f, "{sym_variable}"),
631 SymPermKind::Or(l, r) => write!(f, "({l} | {r})"),
632 SymPermKind::Error(_) => write!(f, "<error>"),
633 }
634 })
635 .unwrap_or_else(|| write!(f, "{self:?}"))
636 }
637}
638
639impl<'db> LeafBoundTerm<'db> for SymPerm<'db> {}
640
641impl<'db> HasKind<'db> for SymPerm<'db> {
642 fn has_kind(&self, _db: &'db dyn crate::Db, kind: SymGenericKind) -> bool {
643 kind == SymGenericKind::Perm
644 }
645}
646
647impl<'db> FromVar<'db> for SymPerm<'db> {
648 fn var(db: &'db dyn crate::Db, var: SymVariable<'db>) -> Self {
649 assert_eq!(var.kind(db), SymGenericKind::Perm);
650 SymPerm::new(db, SymPermKind::Var(var))
651 }
652}
653
654impl<'db> Err<'db> for SymPerm<'db> {
655 fn err(db: &'db dyn dada_ir_ast::Db, reported: Reported) -> Self {
656 SymPerm::new(db, SymPermKind::Error(reported))
657 }
658}
659
660#[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Update, Debug, Serialize)]
661pub enum SymPermKind<'db> {
662 My,
664
665 Our,
667
668 Referenced(Vec<SymPlace<'db>>),
670
671 Mutable(Vec<SymPlace<'db>>),
673
674 Apply(SymPerm<'db>, SymPerm<'db>),
676
677 Infer(InferVarIndex),
679
680 Var(SymVariable<'db>),
682
683 Or(SymPerm<'db>, SymPerm<'db>),
685
686 Error(Reported),
688}
689
690#[derive(SalsaSerialize)]
691#[salsa::tracked(debug)]
692pub struct SymPlace<'db> {
693 #[return_ref]
694 pub kind: SymPlaceKind<'db>,
695}
696
697impl<'db> SymPlace<'db> {
698 pub fn field(self, db: &'db dyn crate::Db, field: SymField<'db>) -> Self {
699 SymPlace::new(db, SymPlaceKind::Field(self, field))
700 }
701
702 pub fn erased(db: &'db dyn crate::Db) -> Self {
703 SymPlace::new(db, SymPlaceKind::Erased)
704 }
705
706 pub fn no_inference_vars(self, db: &'db dyn crate::Db) -> bool {
708 match self.kind(db) {
709 SymPlaceKind::Var(..) => true,
710 SymPlaceKind::Field(sym_place, _) => sym_place.no_inference_vars(db),
711 SymPlaceKind::Index(sym_place) => sym_place.no_inference_vars(db),
712 SymPlaceKind::Error(..) => true,
713 SymPlaceKind::Erased => true,
714 }
715 }
716
717 pub fn is_prefix_of(self, db: &'db dyn crate::Db, other: SymPlace<'db>) -> bool {
723 assert!(self.no_inference_vars(db));
724 assert!(other.no_inference_vars(db));
725 self == other
726 || match (self.kind(db), other.kind(db)) {
727 (_, SymPlaceKind::Field(p2, _)) => self.is_prefix_of(db, *p2),
728 _ => false,
729 }
730 }
731}
732
733impl std::fmt::Display for SymPlace<'_> {
734 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
735 salsa::with_attached_database(|db| {
736 let db: &dyn crate::Db = db.as_view();
737 match self.kind(db) {
738 SymPlaceKind::Var(var) => write!(f, "{var}"),
739 SymPlaceKind::Field(place, field) => write!(f, "{place}.{field}"),
740 SymPlaceKind::Index(place) => write!(f, "{place}[_]"),
741 SymPlaceKind::Error(_) => write!(f, "<error>"),
742 SymPlaceKind::Erased => write!(f, "_"),
743 }
744 })
745 .unwrap_or_else(|| write!(f, "{self:?}"))
746 }
747}
748
749impl<'db> LeafBoundTerm<'db> for SymPlace<'db> {}
750
751impl<'db> Err<'db> for SymPlace<'db> {
752 fn err(db: &'db dyn dada_ir_ast::Db, reported: Reported) -> Self {
753 SymPlace::new(db, SymPlaceKind::Error(reported))
754 }
755}
756
757impl<'db> FromVar<'db> for SymPlace<'db> {
758 fn var(db: &'db dyn crate::Db, var: SymVariable<'db>) -> Self {
759 assert_eq!(var.kind(db), SymGenericKind::Place);
760 SymPlace::new(db, SymPlaceKind::Var(var))
761 }
762}
763
764#[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Update, Debug, Serialize)]
765pub enum SymPlaceKind<'db> {
766 Var(SymVariable<'db>),
768
769 Field(SymPlace<'db>, SymField<'db>),
771
772 Index(SymPlace<'db>),
774
775 Erased,
778
779 Error(Reported),
781}
782
783#[salsa::tracked]
786impl<'db> Symbol<'db> for AstGenericDecl<'db> {
787 type Output = SymVariable<'db>;
788
789 #[salsa::tracked]
790 fn symbol(self, db: &'db dyn crate::Db) -> SymVariable<'db> {
791 SymVariable::new(
792 db,
793 self.kind(db).symbol(db),
794 self.name(db).map(|n| n.id),
795 self.span(db),
796 )
797 }
798}
799
800impl<'db> Symbol<'db> for AstGenericKind<'db> {
802 type Output = SymGenericKind;
803
804 fn symbol(self, _db: &'db dyn crate::Db) -> Self::Output {
805 match self {
806 AstGenericKind::Type(_) => SymGenericKind::Type,
807 AstGenericKind::Perm(_) => SymGenericKind::Perm,
808 }
809 }
810}
811
812pub(crate) trait AnonymousPermSymbol<'db> {
813 fn anonymous_perm_symbol(self, db: &'db dyn crate::Db) -> SymVariable<'db>;
814}
815
816#[salsa::tracked]
821impl<'db> AnonymousPermSymbol<'db> for AstPerm<'db> {
822 #[salsa::tracked]
823 fn anonymous_perm_symbol(self, db: &'db dyn crate::Db) -> SymVariable<'db> {
824 match self.kind(db) {
825 AstPermKind::Referenced(None)
826 | AstPermKind::Mutable(None)
827 | AstPermKind::Given(None) => {
828 SymVariable::new(db, SymGenericKind::Perm, None, self.span(db))
829 }
830 AstPermKind::Our
831 | AstPermKind::Variable(_)
832 | AstPermKind::GenericDecl(_)
833 | AstPermKind::Referenced(Some(_))
834 | AstPermKind::Mutable(Some(_))
835 | AstPermKind::Given(Some(_))
836 | AstPermKind::My => {
837 panic!("`anonymous_perm_symbol` invoked on inappropriate perm: {self:?}")
838 }
839 }
840 }
841}
842
843#[salsa::tracked]
849impl<'db> AnonymousPermSymbol<'db> for AstSelfArg<'db> {
850 #[salsa::tracked]
851 fn anonymous_perm_symbol(self, db: &'db dyn crate::Db) -> SymVariable<'db> {
852 assert!(self.perm(db).is_none());
853 SymVariable::new(db, SymGenericKind::Perm, None, self.span(db))
854 }
855}
856
857#[salsa::tracked]
863impl<'db> AnonymousPermSymbol<'db> for VariableDecl<'db> {
864 #[salsa::tracked]
865 fn anonymous_perm_symbol(self, db: &'db dyn crate::Db) -> SymVariable<'db> {
866 assert!(self.perm(db).is_none());
867 SymVariable::new(db, SymGenericKind::Perm, None, self.span(db))
868 }
869}
870
871#[salsa::interned(debug)]
872pub struct Assumption<'db> {
873 pub kind: AssumptionKind,
874 pub var: SymVariable<'db>,
875}
876
877#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Update, Debug)]
878pub enum AssumptionKind {
879 Lent,
880 Referenced,
881 Unique,
882 Mutable,
883 Owned,
884 Shared,
885 My,
886 Our,
887}