dada_ir_sym/check/
to_red.rs

1//! "Chains" are a canonicalized form of types/permissions.
2//! They can only be produced after inference is complete as they require enumerating the bounds of inference variables.
3//! They are used in borrow checking and for producing the final version of each inference variable.
4
5use dada_ir_ast::diagnostic::{Err, Errors};
6use dada_util::boxed_async_fn;
7
8use crate::ir::{
9    indices::FromInfer,
10    types::{SymGenericTerm, SymPerm, SymPermKind, SymPlace, SymTy, SymTyKind},
11};
12
13use super::{
14    Env,
15    inference::Direction,
16    live_places::LivePlaces,
17    places::PlaceTy,
18    predicates::Predicate,
19    red::{Live, RedChain, RedLink, RedPerm, RedTy},
20    runtime::Runtime,
21    stream::Consumer,
22};
23
24pub trait RedTyExt<'db>: Sized {
25    fn display<'a>(&'a self, env: &'a Env<'db>) -> impl std::fmt::Display;
26}
27
28impl<'db> RedTyExt<'db> for RedTy<'db> {
29    fn display<'a>(&'a self, env: &'a Env<'db>) -> impl std::fmt::Display {
30        struct Wrapper<'a, 'db> {
31            ty: &'a RedTy<'db>,
32            #[expect(dead_code)] // FIXME?
33            env: &'a Env<'db>,
34        }
35
36        impl std::fmt::Display for Wrapper<'_, '_> {
37            fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
38                match &self.ty {
39                    RedTy::Error(_reported) => write!(f, "<error>"),
40                    RedTy::Named(sym_ty_name, sym_generic_terms) => {
41                        write!(f, "{sym_ty_name}[{sym_generic_terms:?}]")
42                    }
43                    RedTy::Never => write!(f, "!"),
44
45                    // FIXME: do better by querying the env state
46                    RedTy::Infer(v) => write!(f, "?{}", v.as_usize()),
47
48                    RedTy::Var(sym_variable) => write!(f, "{sym_variable}"),
49                    RedTy::Perm => write!(f, "<perm>"),
50                }
51            }
52        }
53
54        Wrapper { ty: self, env }
55    }
56}
57
58/// Convert something to a [`RedTy`] and an (optional) permission that is applied to that [`RedTy`][].
59pub trait ToRedTy<'db> {
60    fn to_red_ty(&self, env: &mut Env<'db>) -> (RedTy<'db>, SymPerm<'db>);
61}
62
63impl<'db> ToRedTy<'db> for SymGenericTerm<'db> {
64    fn to_red_ty(&self, env: &mut Env<'db>) -> (RedTy<'db>, SymPerm<'db>) {
65        match *self {
66            SymGenericTerm::Type(ty) => ty.to_red_ty(env),
67            SymGenericTerm::Perm(perm) => perm.to_red_ty(env),
68            SymGenericTerm::Place(_) => panic!("cannot create a red term from a place"),
69            SymGenericTerm::Error(reported) => {
70                let db = env.db();
71                (RedTy::err(db, reported), SymPerm::my(db))
72            }
73        }
74    }
75}
76
77impl<'db> ToRedTy<'db> for SymTy<'db> {
78    fn to_red_ty(&self, env: &mut Env<'db>) -> (RedTy<'db>, SymPerm<'db>) {
79        to_red_ty_with_runtime(*self, env.runtime())
80    }
81}
82
83/// Convert `ty` to a red-ty given a runtime.
84///
85/// See [`ToRedTy`][].
86pub fn to_red_ty_with_runtime<'db>(
87    ty: SymTy<'db>,
88    runtime: &Runtime<'db>,
89) -> (RedTy<'db>, SymPerm<'db>) {
90    let db = runtime.db;
91    match *ty.kind(db) {
92        SymTyKind::Perm(perm0, sym_ty) => {
93            let (red_ty, perm1) = to_red_ty_with_runtime(sym_ty, runtime);
94            (red_ty, perm0.apply_to(db, perm1))
95        }
96        SymTyKind::Named(n, ref g) => (RedTy::Named(n, g.clone()), SymPerm::my(db)),
97        SymTyKind::Infer(infer) => {
98            // every type inference variable has an associated permission inference variable,
99            // so split that off
100            let perm_infer = runtime.perm_infer(infer);
101            (RedTy::Infer(infer), SymPerm::infer(db, perm_infer))
102        }
103        SymTyKind::Var(v) => (RedTy::Var(v), SymPerm::my(db)),
104        SymTyKind::Never => (RedTy::Never, SymPerm::my(db)),
105        SymTyKind::Error(reported) => (RedTy::err(db, reported), SymPerm::my(db)),
106    }
107}
108
109impl<'db> ToRedTy<'db> for SymPerm<'db> {
110    fn to_red_ty(&self, env: &mut Env<'db>) -> (RedTy<'db>, SymPerm<'db>) {
111        let db = env.db();
112        match *self.kind(db) {
113            SymPermKind::Error(reported) => (RedTy::err(db, reported), SymPerm::my(db)),
114            _ => (RedTy::Perm, *self),
115        }
116    }
117}
118
119pub trait ToRedPerm<'db> {
120    async fn to_red_perm(
121        &self,
122        env: &mut Env<'db>,
123        live_after: LivePlaces,
124        direction: Direction,
125        consumer: Consumer<'_, 'db, RedPerm<'db>, Errors<()>>,
126    ) -> Errors<()>;
127}
128
129impl<'db, T: ToRedChainVec<'db>> ToRedPerm<'db> for T {
130    async fn to_red_perm(
131        &self,
132        env: &mut Env<'db>,
133        live_after: LivePlaces,
134        direction: Direction,
135        mut consumer: Consumer<'_, 'db, RedPerm<'db>, Errors<()>>,
136    ) -> Errors<()> {
137        self.to_red_chain_vec(
138            env,
139            live_after,
140            direction,
141            Consumer::new(async |env, chainvec| {
142                consumer
143                    .consume(env, RedPerm::new(env.db(), chainvec))
144                    .await
145            }),
146        )
147        .await
148    }
149}
150
151/// Create a `Vec<RedChain>`, each of which are a canonical list of permissions.
152/// Canonical means that
153///
154/// * inference variables have been bounded,
155/// * permissions have been flattened into distinct chains (`ref[p, q] => ref[p], ref[q]`),
156/// * copy applications reduced (`mut[p] ref[q] => ref[q]`),
157/// * and tails expanded (`mut[q] => mut[q] mut[p]`, given `let q: mut[p] String`).
158///
159/// The `consumer` callback may be invoked multiple times as a result of
160/// inference variable bounding. Each callback is given a vector
161/// corresponding to the collected results from
162/// [`some_expanded_red_chain` in dada-model][dm].
163///
164/// [dm]: https://github.com/dada-lang/dada-model/blob/main/src/type_system/redperms.rs
165pub trait ToRedChainVec<'db> {
166    async fn to_red_chain_vec(
167        &self,
168        env: &mut Env<'db>,
169        live_after: LivePlaces,
170        direction: Direction,
171        consumer: Consumer<'_, 'db, Vec<RedChain<'db>>, Errors<()>>,
172    ) -> Errors<()>;
173}
174
175impl<'db, T: ToRedLinkVecs<'db>> ToRedChainVec<'db> for T {
176    async fn to_red_chain_vec(
177        &self,
178        env: &mut Env<'db>,
179        live_after: LivePlaces,
180        direction: Direction,
181        mut consumer: Consumer<'_, 'db, Vec<RedChain<'db>>, Errors<()>>,
182    ) -> Errors<()> {
183        self.to_red_linkvecs(
184            env,
185            live_after,
186            direction,
187            Consumer::new(async |env, linkvecs| {
188                expand_tail(env, live_after, direction, linkvecs, vec![], &mut consumer).await
189            }),
190        )
191        .await
192    }
193}
194
195/// After we've done the initial expansion to red links, we may end up with a chain
196/// that ends in something like `mut[p]` or `ref[p]`. In that case, we need to
197/// find the permissions from `p` and append them to the chain. This is called
198/// "expansion" in the dada-model code. This function expands the tail recursively
199/// until there are no more permissions to add and then invokes `consumer.consume`.
200#[boxed_async_fn]
201async fn expand_tail<'db>(
202    env: &mut Env<'db>,
203    live_after: LivePlaces,
204    direction: Direction,
205    mut unexpanded_linkvecs: Vec<Vec<RedLink<'db>>>,
206    mut expanded_chains: Vec<RedChain<'db>>,
207    consumer: &mut Consumer<'_, 'db, Vec<RedChain<'db>>, Errors<()>>,
208) -> Errors<()> {
209    let db = env.db();
210
211    // This is super annoying. We have a vector of "pseudo-chains" (Vec<RedLink>)
212    // like `[[mut[a]], [ref[b]], [my]]`. We want to take the tail of each
213    // of those chains and expand it, so, e.g., if `a: mut[x] String`,
214    // then we might expand to `[[mut[a] mut[x]], [ref[b]], [my]]`.
215    // But if `x: mut[y, z] String`, then we have to expand again,
216    // and this time with some flattening, yielding
217    // `[[mut[a] mut[x] muy[y]], [mut[a] mut[x] mut[z]], [ref[b]], [my]]`.
218    // And we haven't even started in on `ref[b]`.
219    // To make it more often, we need to expect multiple callbacks because
220    // of inference, so we have to write everything in a "callback, recursive"
221    // style and can't readily return values.
222    //
223    // We do this by popping links from `unexpected_links`, examining them,
224    // and then either expanding them or else pushing onto `expanded_links`.
225
226    let Some(linkvec) = unexpanded_linkvecs.pop() else {
227        // Nothing left to expand! Great.
228        return consumer.consume(env, expanded_chains).await;
229    };
230
231    let place = match linkvec.last() {
232        Some(RedLink::Ref(_, place)) | Some(RedLink::Mut(_, place)) => place,
233
234        // If the last link does not reference a place,
235        // or there is no last link (i.e., we have `my`),
236        // then we are done expanding. Push resulting chain and recurse.
237        Some(RedLink::Our) | Some(RedLink::Var(_)) | None => {
238            expanded_chains.push(RedChain::new(db, linkvec));
239            return expand_tail(
240                env,
241                live_after,
242                direction,
243                unexpanded_linkvecs,
244                expanded_chains,
245                consumer,
246            )
247            .await;
248        }
249
250        Some(RedLink::Err(reported)) => return Err(*reported),
251    };
252
253    // Otherwise, convert expand that place to red-links. This will yield
254    // a vector so we have to "flat map" the result onto the list of expanded
255    // chains.
256    place
257        .to_red_linkvecs(
258            env,
259            live_after,
260            direction,
261            Consumer::new(async |env, linkvecs_place: Vec<Vec<_>>| {
262                let mut unexpanded_linkvecs = unexpanded_linkvecs.clone();
263                let mut expanded_chains = expanded_chains.clone();
264
265                for linkvec_place in linkvecs_place {
266                    if linkvec_place.is_empty() {
267                        // If the link vec we get back is `my`, then push a fully expanded chain.
268                        // This corresponds to e.g. `mut[a]` where `a: my String` -- the permission
269                        // is complete.
270                        expanded_chains.push(RedChain::new(db, linkvec.clone()));
271                    } else {
272                        // Otherwise, concatenate this new link vec with our original
273                        // and push it back onto the "unexpanded" list. We will recursively
274                        // examine it.
275                        let output = concat_linkvecs(env, &linkvec, &linkvec_place)?;
276                        unexpanded_linkvecs.push(output);
277                    }
278                }
279                expand_tail(
280                    env,
281                    live_after,
282                    direction,
283                    unexpanded_linkvecs,
284                    expanded_chains,
285                    consumer,
286                )
287                .await
288            }),
289        )
290        .await
291}
292
293/// Convert the permission into a vector of red-links.
294///
295/// This is part of the red permission process and does three forms of processing.
296///
297/// * Copy links drop their prefix, so e.g. `mut[p] ref[q]` becomes just `[ref[q]]`
298/// * Flattening, so `ref[p,q]` becomes `[ref[p], ref[q]]`.
299/// * If inference variables are involved, we block waiting for their bounds.
300///
301/// The `consumer` callback may be invoked multiple times as a result of inference bounds.
302/// Each callback has a list of lists of links.
303pub trait ToRedLinkVecs<'db> {
304    async fn to_red_linkvecs(
305        &self,
306        env: &mut Env<'db>,
307        live_after: LivePlaces,
308        direction: Direction,
309        consumer: Consumer<'_, 'db, Vec<Vec<RedLink<'db>>>, Errors<()>>,
310    ) -> Errors<()>;
311}
312
313impl<'db> ToRedLinkVecs<'db> for SymPerm<'db> {
314    #[boxed_async_fn]
315    async fn to_red_linkvecs(
316        &self,
317        env: &mut Env<'db>,
318        live_after: LivePlaces,
319        direction: Direction,
320        mut consumer: Consumer<'_, 'db, Vec<Vec<RedLink<'db>>>, Errors<()>>,
321    ) -> Errors<()> {
322        let db = env.db();
323        match *self.kind(db) {
324            SymPermKind::My => consumer.consume(env, vec![vec![]]).await,
325            SymPermKind::Our => consumer.consume(env, vec![vec![RedLink::Our]]).await,
326            SymPermKind::Referenced(ref places) => {
327                let links = places
328                    .iter()
329                    .map(|&place| RedLink::Ref(Live(live_after.is_live(env, place)), place))
330                    .map(|link| vec![link])
331                    .collect::<Vec<_>>();
332                consumer.consume(env, links).await
333            }
334            SymPermKind::Mutable(ref places) => {
335                let links = places
336                    .iter()
337                    .map(|&place| RedLink::Mut(Live(live_after.is_live(env, place)), place))
338                    .map(|link| vec![link])
339                    .collect::<Vec<_>>();
340                consumer.consume(env, links).await
341            }
342            SymPermKind::Apply(lhs, rhs) => {
343                lhs.to_red_linkvecs(
344                    env,
345                    live_after,
346                    direction,
347                    Consumer::new(async |env, linkvecs_lhs: Vec<Vec<RedLink<'db>>>| {
348                        rhs.to_red_linkvecs(
349                            env,
350                            live_after,
351                            direction,
352                            Consumer::new(async |env, linkvecs_rhs: Vec<Vec<_>>| {
353                                let links = concat_linkvecvecs(env, &linkvecs_lhs, &linkvecs_rhs)?;
354                                consumer.consume(env, links).await
355                            }),
356                        )
357                        .await
358                    }),
359                )
360                .await
361            }
362            SymPermKind::Infer(v) => {
363                let mut bounds = env.red_perm_bounds(v);
364                while let Some((direction_bound, red_perm)) = bounds.next(env).await {
365                    if direction_bound == direction {
366                        for &chain in red_perm.chains(db) {
367                            let links = chain.links(db).to_vec();
368                            consumer.consume(env, vec![links]).await?;
369                        }
370                    }
371                }
372                Ok(())
373            }
374            SymPermKind::Var(v) => {
375                let linkvec = {
376                    if env.var_is_declared_to_be(v, Predicate::Owned)
377                        && env.var_is_declared_to_be(v, Predicate::Unique)
378                    {
379                        vec![]
380                    } else if env.var_is_declared_to_be(v, Predicate::Owned)
381                        && env.var_is_declared_to_be(v, Predicate::Unique)
382                    {
383                        vec![RedLink::Our]
384                    } else {
385                        vec![RedLink::Var(v)]
386                    }
387                };
388
389                consumer.consume(env, vec![linkvec]).await
390            }
391            SymPermKind::Error(reported) => return Err(reported),
392            SymPermKind::Or(perm1, perm2) => {
393                perm1
394                    .to_red_linkvecs(
395                        env,
396                        live_after,
397                        direction,
398                        Consumer::new(async |env, linkvecs1: Vec<Vec<_>>| {
399                            perm2
400                                .to_red_linkvecs(
401                                    env,
402                                    live_after,
403                                    direction,
404                                    Consumer::new(async |env, linkvecs2: Vec<Vec<_>>| {
405                                        let linkvecs3 =
406                                            linkvecs1.iter().chain(&linkvecs2).cloned().collect();
407                                        consumer.consume(env, linkvecs3).await
408                                    }),
409                                )
410                                .await
411                        }),
412                    )
413                    .await
414            }
415        }
416    }
417}
418
419impl<'db> ToRedLinkVecs<'db> for SymPlace<'db> {
420    #[boxed_async_fn]
421    async fn to_red_linkvecs(
422        &self,
423        env: &mut Env<'db>,
424        live_after: LivePlaces,
425        direction: Direction,
426        consumer: Consumer<'_, 'db, Vec<Vec<RedLink<'db>>>, Errors<()>>,
427    ) -> Errors<()> {
428        let ty = self.place_ty(env).await;
429        ty.to_red_linkvecs(env, live_after, direction, consumer)
430            .await
431    }
432}
433
434impl<'db> ToRedLinkVecs<'db> for SymTy<'db> {
435    #[boxed_async_fn]
436    async fn to_red_linkvecs(
437        &self,
438        env: &mut Env<'db>,
439        live_after: LivePlaces,
440        direction: Direction,
441        consumer: Consumer<'_, 'db, Vec<Vec<RedLink<'db>>>, Errors<()>>,
442    ) -> Errors<()> {
443        let (_, perm) = self.to_red_ty(env);
444        perm.to_red_linkvecs(env, live_after, direction, consumer)
445            .await
446    }
447}
448
449fn concat_linkvecvecs<'db>(
450    env: &mut Env<'db>,
451    lhs: &[Vec<RedLink<'db>>],
452    rhs: &[Vec<RedLink<'db>>],
453) -> Errors<Vec<Vec<RedLink<'db>>>> {
454    let mut output = Vec::with_capacity(lhs.len() * rhs.len());
455    for l in lhs {
456        for r in rhs {
457            output.push(concat_linkvecs(env, l, r)?);
458        }
459    }
460    Ok(output)
461}
462
463fn concat_linkvecs<'db>(
464    env: &mut Env<'db>,
465    lhs: &[RedLink<'db>],
466    mut rhs: &[RedLink<'db>],
467) -> Errors<Vec<RedLink<'db>>> {
468    let mut lhs = lhs.to_vec();
469
470    while let Some((rhs_head, rhs_tail)) = rhs.split_first() {
471        if rhs_head.is_copy(env)? {
472            return Ok(rhs.to_vec());
473        }
474        lhs.push(*rhs_head);
475        rhs = rhs_tail;
476    }
477
478    Ok(lhs)
479}
dada_ir_sym/check/to_red.rs

dada_ir_sym/check/
to_red.rs
