dada_ir_sym/check/
inference.rs

1//! Type and permission inference for Dada.
2#![doc = include_str!("../../docs/type_inference.md")]
3
4use dada_ir_ast::span::Span;
5use salsa::Update;
6use serde::Serialize;
7
8use crate::ir::{indices::InferVarIndex, types::SymGenericKind};
9
10use super::{
11    red::{RedPerm, RedTy},
12    report::{ArcOrElse, InferenceFallback, OrElse},
13};
14
15mod serialize;
16
17#[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Serialize)]
18pub enum Direction {
19    FromBelow,
20    FromAbove,
21}
22
23pub(crate) struct InferenceVarData<'db> {
24    span: Span<'db>,
25
26    /// Bounds on this variable suitable for its kind.
27    bounds: InferenceVarBounds<'db>,
28}
29
30impl<'db> InferenceVarData<'db> {
31    fn new(span: Span<'db>, bounds: InferenceVarBounds<'db>) -> Self {
32        Self { span, bounds }
33    }
34
35    /// Create the data for a new permission inference variable.
36    pub fn new_perm(span: Span<'db>) -> Self {
37        Self::new(
38            span,
39            InferenceVarBounds::Perm {
40                lower: Default::default(),
41                upper: Default::default(),
42            },
43        )
44    }
45
46    /// Create the data for a new type inference variable.
47    /// Requires the index `perm` of a corresponding permission variable.
48    pub fn new_ty(span: Span<'db>, perm: InferVarIndex) -> Self {
49        Self::new(
50            span,
51            InferenceVarBounds::Ty {
52                perm,
53                lower: Default::default(),
54                upper: Default::default(),
55            },
56        )
57    }
58
59    /// Returns the span of code which triggered the inference variable to be created.
60    pub fn span(&self) -> Span<'db> {
61        self.span
62    }
63
64    /// Returns the kind of the inference variable.
65    pub fn kind(&self) -> InferVarKind {
66        match self.bounds {
67            InferenceVarBounds::Perm { .. } => InferVarKind::Perm,
68            InferenceVarBounds::Ty { .. } => InferVarKind::Type,
69        }
70    }
71
72    /// Returns the upper or lower bounds on this permission variable.
73    ///
74    /// # Panics
75    ///
76    /// If this is not a permission variable.
77    #[track_caller]
78    pub fn red_perm_bound(&self, direction: Direction) -> Option<(RedPerm<'db>, ArcOrElse<'db>)> {
79        match &self.bounds {
80            InferenceVarBounds::Perm { lower, upper, .. } => match direction {
81                Direction::FromBelow => lower.clone(),
82                Direction::FromAbove => upper.clone(),
83            },
84            _ => panic!("lower_chains invoked on a var of kind `{:?}`", self.kind()),
85        }
86    }
87
88    /// Returns the permission variable corresponding to this type variable.
89    /// Returns `None` if this is a permission variable.
90    #[track_caller]
91    pub fn perm(&self) -> Option<InferVarIndex> {
92        match &self.bounds {
93            InferenceVarBounds::Ty { perm, .. } => Some(*perm),
94            InferenceVarBounds::Perm { .. } => None,
95        }
96    }
97
98    /// Returns the lower or upper bound on this type variable, depending on `direction`.
99    ///
100    /// # Panics
101    ///
102    /// If this is not a type variable.
103    #[track_caller]
104    pub fn red_ty_bound(&self, direction: Direction) -> Option<(RedTy<'db>, ArcOrElse<'db>)> {
105        match &self.bounds {
106            InferenceVarBounds::Ty { lower, upper, .. } => match direction {
107                Direction::FromBelow => lower.clone(),
108                Direction::FromAbove => upper.clone(),
109            },
110            _ => panic!("red_ty_bound invoked on a var of kind `{:?}`", self.kind()),
111        }
112    }
113
114    /// Insert a red perm as a (lower|upper) bound.
115    /// Returns `Some(or_else.to_arc())` if this is a new (lower|upper) bound.
116    pub fn set_red_perm_bound(
117        &mut self,
118        direction: Direction,
119        red_perm: RedPerm<'db>,
120        or_else: &dyn OrElse<'db>,
121    ) {
122        let perm_bound = match &mut self.bounds {
123            InferenceVarBounds::Perm { lower, upper, .. } => match direction {
124                Direction::FromBelow => lower,
125                Direction::FromAbove => upper,
126            },
127            _ => panic!(
128                "insert_lower_chain invoked on a var of kind `{:?}`",
129                self.kind()
130            ),
131        };
132        *perm_bound = Some((red_perm, or_else.to_arc()));
133    }
134
135    /// Overwrite the lower or upper bounding red ty, depending on `direction`.
136    /// Returns the [to_arc'd](`OrElse::to_arc`) version of `or_else`.
137    pub fn set_red_ty_bound(
138        &mut self,
139        direction: Direction,
140        red_ty: RedTy<'db>,
141        or_else: &dyn OrElse<'db>,
142    ) {
143        let red_ty_bound = match &mut self.bounds {
144            InferenceVarBounds::Ty { lower, upper, .. } => match direction {
145                Direction::FromBelow => lower,
146                Direction::FromAbove => upper,
147            },
148            _ => panic!(
149                "set_lower_red_ty invoked on a var of kind `{:?}`",
150                self.kind()
151            ),
152        };
153        *red_ty_bound = Some((red_ty, or_else.to_arc()));
154    }
155
156    /// If this inference variable is unbounded, apply a default type. This is invoked
157    /// during [`Runtime::mark_complete`](`crate::check::runtime::Runtime::mark_complete`)
158    pub fn fallback(&mut self, db: &'db dyn crate::Db) {
159        match &mut self.bounds {
160            InferenceVarBounds::Perm { lower, upper } => {
161                if lower.is_none() && upper.is_none() {
162                    let fallback = RedPerm::fallback(db);
163                    let fallback_term = fallback.to_sym_perm(db);
164                    *lower = Some((
165                        fallback,
166                        InferenceFallback::new(self.span, InferVarKind::Perm, fallback_term)
167                            .to_arc(),
168                    ));
169                }
170            }
171            InferenceVarBounds::Ty {
172                perm: _,
173                lower,
174                upper,
175            } => {
176                if lower.is_none() && upper.is_none() {
177                    let fallback = RedTy::fallback(db);
178                    let fallback_term = fallback.clone().into_sym_ty(db);
179                    *lower = Some((
180                        fallback,
181                        InferenceFallback::new(self.span, InferVarKind::Perm, fallback_term)
182                            .to_arc(),
183                    ));
184                }
185            }
186        }
187    }
188}
189
190#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Update, Debug, Serialize)]
191pub enum InferVarKind {
192    Type,
193    Perm,
194}
195
196impl std::fmt::Display for InferVarKind {
197    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
198        match self {
199            InferVarKind::Type => write!(f, "type"),
200            InferVarKind::Perm => write!(f, "perm"),
201        }
202    }
203}
204
205impl From<InferVarKind> for SymGenericKind {
206    fn from(value: InferVarKind) -> Self {
207        match value {
208            InferVarKind::Type => SymGenericKind::Type,
209            InferVarKind::Perm => SymGenericKind::Perm,
210        }
211    }
212}
213
214pub enum InferenceVarBounds<'db> {
215    /// Bounds for a permission:
216    ///
217    /// The inferred permission `?P` must meet
218    ///
219    /// * `L <: ?P` for each `L` in `lower`
220    /// * `?P <: U` for each `U` in `upper`
221    ///
222    /// This in turn implies that `L <: U`
223    /// for all `L in lower`, `U in upper`.
224    Perm {
225        lower: Option<(RedPerm<'db>, ArcOrElse<'db>)>,
226        upper: Option<(RedPerm<'db>, ArcOrElse<'db>)>,
227    },
228
229    /// Bounds for a type:
230    ///
231    /// The inferred type `?T` must
232    ///
233    /// * have a red-perm of `perm`
234    ///   (we always create an associated permission
235    ///   variable for every type variable)
236    /// * have a red-ty `R` where `lower <= R`
237    /// * have a red-ty `R` where `R <= upper`
238    Ty {
239        perm: InferVarIndex,
240        lower: Option<(RedTy<'db>, ArcOrElse<'db>)>,
241        upper: Option<(RedTy<'db>, ArcOrElse<'db>)>,
242    },
243}
244
245/// Trait implemented by types returned by mutation methods
246/// like `InferenceVarData::set_red_perm_bound`
247/// or `InferenceVarData::set_red_ty_bound`.
248/// Can be used to check if those return values indicate that
249/// the inference var data was actually changed.
250pub trait InferenceVarDataChanged {
251    fn did_change(&self) -> bool;
252}
253
254impl InferenceVarDataChanged for bool {
255    fn did_change(&self) -> bool {
256        *self
257    }
258}
259
260impl InferenceVarDataChanged for Option<ArcOrElse<'_>> {
261    fn did_change(&self) -> bool {
262        self.is_some()
263    }
264}
265
266impl InferenceVarDataChanged for () {
267    fn did_change(&self) -> bool {
268        true
269    }
270}
dada_ir_sym/check/inference.rs

dada_ir_sym/check/
inference.rs
