dada_ir_sym/check/predicates/
is_provably_lent.rs

1use dada_ir_ast::diagnostic::Errors;
2use dada_util::boxed_async_fn;
3
4use crate::{
5    check::{
6        env::Env,
7        places::PlaceTy,
8        predicates::{Predicate, var_infer::test_var_is_provably},
9        red::RedTy,
10        to_red::ToRedTy,
11    },
12    ir::{
13        classes::SymAggregateStyle,
14        types::{SymGenericTerm, SymPerm, SymPermKind, SymPlace, SymTyName},
15    },
16};
17
18use super::{is_provably_unique::place_is_provably_unique, var_infer::infer_is_provably};
19
20pub async fn term_is_provably_lent<'db>(
21    env: &mut Env<'db>,
22    term: impl Into<SymGenericTerm<'db>>,
23) -> Errors<bool> {
24    let term: SymGenericTerm<'db> = term.into();
25    env.indent("term_is_provably_lent", &[&term], async |env| {
26        let db = env.db();
27        let (red_ty, perm) = term.to_red_ty(env);
28        match red_ty {
29            RedTy::Infer(infer) => infer_is_provably(env, perm, infer, Predicate::Lent).await,
30            RedTy::Var(var) => {
31                // Subtle: `perm` doesn't matter here because...
32                //
33                // (1) the generic variable could be a struct, in which case it would be ignored
34                // (2) even if it's not, if it's a lent thing (e.g., `ref[x] S` or `mut[x] S`),
35                // then whatever perm we apply, the result will still be lent.
36                Ok(test_var_is_provably(env, var, Predicate::Lent))
37            }
38            RedTy::Never => perm_is_provably_lent(env, perm).await,
39            RedTy::Error(reported) => Err(reported),
40            RedTy::Named(name, generics) => match name {
41                SymTyName::Primitive(_) => Ok(false),
42                SymTyName::Aggregate(sym_aggregate) => match sym_aggregate.style(db) {
43                    SymAggregateStyle::Struct => {
44                        env.exists(generics, async |env, generic| {
45                            term_is_provably_lent(env, perm.apply_to(db, generic)).await
46                        })
47                        .await
48                    }
49                    SymAggregateStyle::Class => perm_is_provably_lent(env, perm).await,
50                },
51                SymTyName::Future => Ok(false),
52                SymTyName::Tuple { arity: _ } => {
53                    env.exists(generics, async |env, generic| {
54                        term_is_provably_lent(env, perm.apply_to(db, generic)).await
55                    })
56                    .await
57                }
58            },
59            RedTy::Perm => perm_is_provably_lent(env, perm).await,
60        }
61    })
62    .await
63}
64
65async fn application_is_provably_lent<'db>(
66    env: &mut Env<'db>,
67    lhs: SymGenericTerm<'db>,
68    rhs: SymGenericTerm<'db>,
69) -> Errors<bool> {
70    env.either(
71        async |env| term_is_provably_lent(env, lhs).await,
72        async |env| term_is_provably_lent(env, rhs).await,
73    )
74    .await
75}
76
77#[boxed_async_fn]
78pub(crate) async fn perm_is_provably_lent<'db>(
79    env: &mut Env<'db>,
80    perm: SymPerm<'db>,
81) -> Errors<bool> {
82    let db = env.db();
83    match *perm.kind(db) {
84        SymPermKind::Error(reported) => Err(reported),
85        SymPermKind::My => Ok(false),
86
87        // Somewhat surprising, but `our` is considered lent because of subtyping.
88        SymPermKind::Our => Ok(true),
89
90        SymPermKind::Referenced(ref places) | SymPermKind::Mutable(ref places) => {
91            // This one is tricky. If the places are copy,
92            // then we will reduce to their chains, but then
93            // we would be lent if they are lent; but if they are not
94            // copy, we are lent.
95            env.either(
96                async |env| {
97                    env.for_all(places, async |env, &place| {
98                        place_is_provably_unique(env, place).await
99                    })
100                    .await
101                },
102                async |env| {
103                    env.exists(places, async |env, &place| {
104                        place_is_provably_lent(env, place).await
105                    })
106                    .await
107                },
108            )
109            .await
110        }
111        SymPermKind::Apply(lhs, rhs) => {
112            Ok(application_is_provably_lent(env, lhs.into(), rhs.into()).await?)
113        }
114        SymPermKind::Var(var) => Ok(test_var_is_provably(env, var, Predicate::Lent)),
115        SymPermKind::Infer(infer) => {
116            infer_is_provably(env, SymPerm::my(db), infer, Predicate::Lent).await
117        }
118        SymPermKind::Or(_, _) => todo!(),
119    }
120}
121
122pub(crate) async fn place_is_provably_lent<'db>(
123    env: &mut Env<'db>,
124    place: SymPlace<'db>,
125) -> Errors<bool> {
126    let ty = place.place_ty(env).await;
127    term_is_provably_lent(env, ty).await
128}
dada_ir_sym/check/predicates/is_provably_lent.rs

dada_ir_sym/check/predicates/
is_provably_lent.rs
