Skip to main content

dada_ir_sym/ir/
types.rs

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    /// If true, then `T[P] <: T[Q]` requires `P <: Q` (necessary, not sufficient)
28    pub at_least_covariant: bool,
29
30    /// If true, then `T[P] <: T[Q]` requires `Q <: P` (necessary, not sufficient)
31    pub at_least_contravariant: bool,
32
33    /// Indicates that this type or permission
34    /// is not directly owned by the struct/class but
35    /// rather is relative to something else.
36    ///
37    /// Non-relative generics inherit permissions
38    ///
39    /// # Examples
40    ///
41    /// * `class Foo[type T](T)` -- `T` is NOT relative, so `our Foo[String]` becomes `our Foo[our String]`
42    /// * `class Foo[perm P, type T](P T)` -- `P` is not relative, but `T` IS,
43    ///   so `our Foo[my, String]` becomes `our Foo[our, String]`
44    ///
45    /// FIXME: Need a better name.
46    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
76/// Test if `self` can be said to have the given kind (i.e., is it a type? a permission?).
77///
78/// Note that when errors occur, this may return true for multiple kinds.
79pub trait HasKind<'db> {
80    fn has_kind(&self, db: &'db dyn crate::Db, kind: SymGenericKind) -> bool;
81}
82
83/// Assert that `self` has the appropriate kind to produce an `R` value.
84/// Implemented by e.g. [`SymGenericTerm`][] to permit downcasting to [`SymTy`](`crate::ir::ty::SymTy`).
85pub trait AssertKind<'db, R> {
86    fn assert_kind(self, db: &'db dyn crate::Db) -> R;
87}
88
89/// Value of a generic parameter
90#[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    /// Returns the kind of term (or `Err` if it is an error).
210    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    /// True if self is an error or if it has the given kind.
220    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    /// Returns the inference variable index if `self` is an inference variable.
230    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    /// Returns a string describing `self`, similar to "type `X`"
263    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    /// Returns a [`SymTyKind::Named`][] type for the given primitive type.
289    pub fn primitive(db: &'db dyn Db, primitive: SymPrimitiveKind) -> Self {
290        SymTy::named(db, primitive.intern(db).into(), vec![])
291    }
292
293    /// Returns a [`SymTyKind::Named`][] type for `u8`.
294    pub fn u8(db: &'db dyn Db) -> Self {
295        SymTy::primitive(db, SymPrimitiveKind::Uint { bits: 8 })
296    }
297
298    /// Returns a [`SymTyKind::Named`][] type for `u32`.
299    pub fn u32(db: &'db dyn Db) -> Self {
300        SymTy::primitive(db, SymPrimitiveKind::Uint { bits: 32 })
301    }
302
303    /// Returns a [`SymTyKind::Named`][] type for `String`.
304    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    /// Returns a new [`SymTyKind::Named`][].
313    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    /// Returns a [`SymTyKind::Var`][] type for the given variable.
322    pub fn var(db: &'db dyn Db, var: SymVariable<'db>) -> Self {
323        SymTy::new(db, SymTyKind::Var(var))
324    }
325
326    /// Returns a [`SymTyKind::Named`][] type for `()`.
327    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    /// Returns a [`SymTyKind::Named`][] type for `bool`.
337    pub fn boolean(db: &'db dyn Db) -> Self {
338        SymTy::named(db, SymPrimitiveKind::Bool.intern(db).into(), vec![])
339    }
340
341    /// Returns the type we fallback to for type inference variables
342    /// that wind up unconstrained (never).
343    pub fn fallback(db: &'db dyn Db) -> Self {
344        Self::never(db)
345    }
346
347    /// Returns a [`SymTyKind::Never`][] type.
348    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    /// Returns a new [`SymTyKind::Perm`][].
358    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    /// Returns a version of this type shared from `place`.
363    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    /// Returns a version of this type mutable from `place`.
371    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    /// Returns a version of this type mutable from `place`.
376    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 $Ty`, e.g., `shared String
439    Perm(SymPerm<'db>, SymTy<'db>),
440
441    /// `path[arg1, arg2]`, e.g., `Vec[String]`
442    ///
443    /// Important: the generic arguments must be well-kinded and of the correct number.
444    Named(SymTyName<'db>, Vec<SymGenericTerm<'db>>),
445
446    /// An inference variable (e.g., `?X`).
447    Infer(InferVarIndex),
448
449    /// Reference to a generic variable, e.g., `T`.
450    Var(SymVariable<'db>),
451
452    /// A value that can never be created, denoted `!`.
453    Never,
454
455    /// Indicates some kind of error occurred and has been reported to the user.
456    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    /// For now, just make future a builtin type
468    #[no_from_impl]
469    Future,
470
471    #[no_from_impl]
472    Tuple {
473        arity: usize,
474    },
475}
476
477impl<'db> SymTyName<'db> {
478    /// Aggregate style (struct, etc)
479    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    /// When we have an inference variable without any bounds,
513    /// returns the permission we will fallback to (`my`).
514    pub fn fallback(db: &'db dyn crate::Db) -> Self {
515        Self::my(db)
516    }
517
518    /// Returns the permission `my`.
519    pub fn my(db: &'db dyn crate::Db) -> Self {
520        SymPerm::new(db, SymPermKind::My)
521    }
522
523    /// Returns the permission `our`.
524    pub fn our(db: &'db dyn crate::Db) -> Self {
525        SymPerm::new(db, SymPermKind::Our)
526    }
527
528    /// Returns a permission `shared` with the given places.
529    pub fn referenced(db: &'db dyn crate::Db, places: Vec<SymPlace<'db>>) -> Self {
530        SymPerm::new(db, SymPermKind::Referenced(places))
531    }
532
533    /// Returns a permission `mutable` with the given places.
534    pub fn mutable(db: &'db dyn crate::Db, places: Vec<SymPlace<'db>>) -> Self {
535        SymPerm::new(db, SymPermKind::Mutable(places))
536    }
537
538    /// Returns a generic permission with the given generic variable `var`.
539    pub fn var(db: &'db dyn crate::Db, var: SymVariable<'db>) -> Self {
540        SymPerm::new(db, SymPermKind::Var(var))
541    }
542
543    /// Returns a permission `perm1 perm2` (e.g., `shared[x] mutable[y]`).
544    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    /// Returns a permission `perm1 | perm2`
549    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    /// Apply this permission to the given term (if `self` is not `my`).
554    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`
663    My,
664
665    /// `our`
666    Our,
667
668    /// `ref[x]`
669    Referenced(Vec<SymPlace<'db>>),
670
671    /// `mutable[x]`
672    Mutable(Vec<SymPlace<'db>>),
673
674    /// `perm1 perm2` (e.g., `shared[x] mutable[y]`)
675    Apply(SymPerm<'db>, SymPerm<'db>),
676
677    /// An inference variable (e.g., `?X`).
678    Infer(InferVarIndex),
679
680    /// A generic variable (e.g., `T`).
681    Var(SymVariable<'db>),
682
683    /// Either `P | Q`
684    Or(SymPerm<'db>, SymPerm<'db>),
685
686    /// An error occurred and has been reported to the user.
687    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    /// True if `self` contains no inference variables.
707    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    /// True if `self` *covers* `other`. Neither place may contain inference variables.
718    ///
719    /// # Definition
720    ///
721    /// A place P *covers* another place Q if P includes all of Q. E.g., `a` covers `a.b`.
722    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    /// `x`
767    Var(SymVariable<'db>),
768
769    /// `x.f`
770    Field(SymPlace<'db>, SymField<'db>),
771
772    /// `x[_]`
773    Index(SymPlace<'db>),
774
775    /// Erased place, used during codegen.
776    /// Should never see it during type checking.
777    Erased,
778
779    /// An error occurred and has been reported to the user.
780    Error(Reported),
781}
782
783/// Create the symbol for an explicictly declared generic parameter.
784/// This is tracked so that we do it at most once.
785#[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
800/// Convert to `SymGenericKind`
801impl<'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/// Create the generic symbol for an anonymous permission like `shared T` or `mutable T`.
817/// This is desugared into the equivalent of `(perm:shared) T`.
818///
819/// Tracked so that it occurs at most once per `shared|mutable|given` declaration.
820#[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/// Create a generic symbol for an anonymous permission like `self`.
844/// This is not always needed; see the implementation of [`PopulateSignatureSymbols`][]
845/// for [`AstSelfArg`][].
846///
847/// Tracked so that it occurs at most once per `self` declaration.
848#[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/// Create a generic symbol for a variable declaration that has no explicit
858/// permission, like `x: String`. This is not always needed; see the
859/// implementation of [`PopulateSignatureSymbols`][] for [`VariableDecl`][].
860///
861/// Tracked so that it occurs at most once per `self` declaration.
862#[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}