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

dada_ir_sym/check/predicates/
is_provably_shared.rs
