dada_ir_sym/check/predicates/
is_provably_owned.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::var_infer::infer_is_provably;
19
20pub async fn term_is_provably_owned<'db>(
21    env: &mut Env<'db>,
22    term: SymGenericTerm<'db>,
23) -> Errors<bool> {
24    let (red_ty, perm) = term.to_red_ty(env);
25    let db = env.db();
26    match red_ty {
27        RedTy::Infer(infer) => infer_is_provably(env, perm, infer, Predicate::Owned).await,
28        RedTy::Var(var) => {
29            env.both(
30                async |env| Ok(test_var_is_provably(env, var, Predicate::Owned)),
31                async |env| perm_is_provably_owned(env, perm).await,
32            )
33            .await
34        }
35        RedTy::Never => perm_is_provably_owned(env, perm).await,
36        RedTy::Error(reported) => Err(reported),
37        RedTy::Named(sym_ty_name, ref generics) => match sym_ty_name {
38            SymTyName::Primitive(_) => Ok(true),
39            SymTyName::Aggregate(sym_aggregate) => match sym_aggregate.style(db) {
40                SymAggregateStyle::Struct => {
41                    env.for_all(generics, async |env, &generic| {
42                        term_is_provably_owned(env, perm.apply_to(db, generic)).await
43                    })
44                    .await
45                }
46                SymAggregateStyle::Class => perm_is_provably_owned(env, perm).await,
47            },
48            SymTyName::Future => perm_is_provably_owned(env, perm).await,
49            SymTyName::Tuple { arity: _ } => {
50                env.for_all(generics, async |env, &generic| {
51                    term_is_provably_owned(env, perm.apply_to(db, generic)).await
52                })
53                .await
54            }
55        },
56        RedTy::Perm => perm_is_provably_owned(env, perm).await,
57    }
58}
59
60async fn application_is_provably_owned<'db>(
61    env: &mut Env<'db>,
62    lhs: SymGenericTerm<'db>,
63    rhs: SymGenericTerm<'db>,
64) -> Errors<bool> {
65    env.both(
66        async |env| term_is_provably_owned(env, lhs).await,
67        async |env| term_is_provably_owned(env, rhs).await,
68    )
69    .await
70}
71
72#[boxed_async_fn]
73pub(crate) async fn perm_is_provably_owned<'db>(
74    env: &mut Env<'db>,
75    perm: SymPerm<'db>,
76) -> Errors<bool> {
77    let db = env.db();
78    match *perm.kind(db) {
79        SymPermKind::Error(reported) => Err(reported),
80        SymPermKind::My => Ok(true),
81        SymPermKind::Our | SymPermKind::Referenced(_) => Ok(false),
82        SymPermKind::Mutable(ref places) => {
83            env.exists(places, async |env, &place| {
84                place_is_provably_owned(env, place).await
85            })
86            .await
87        }
88
89        SymPermKind::Apply(lhs, rhs) => {
90            Ok(application_is_provably_owned(env, lhs.into(), rhs.into()).await?)
91        }
92
93        SymPermKind::Var(var) => Ok(test_var_is_provably(env, var, Predicate::Owned)),
94
95        SymPermKind::Infer(infer) => {
96            infer_is_provably(env, SymPerm::my(db), infer, Predicate::Owned).await
97        }
98
99        SymPermKind::Or(_, _) => todo!(),
100    }
101}
102
103pub(crate) async fn place_is_provably_owned<'db>(
104    env: &mut Env<'db>,
105    place: SymPlace<'db>,
106) -> Errors<bool> {
107    let ty = place.place_ty(env).await;
108    term_is_provably_owned(env, ty.into()).await
109}
dada_ir_sym/check/predicates/is_provably_owned.rs

dada_ir_sym/check/predicates/
is_provably_owned.rs
