dada_ir_sym/check/predicates/
require_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::{
9            Predicate,
10            var_infer::{require_infer_is, require_var_is},
11        },
12        red::RedTy,
13        report::{Because, OrElse},
14        to_red::ToRedTy,
15    },
16    ir::{
17        classes::SymAggregateStyle,
18        types::{SymGenericTerm, SymPerm, SymPermKind, SymPlace, SymTy},
19    },
20};
21
22use super::is_provably_shared::{perm_is_provably_shared, term_is_provably_shared};
23
24pub(crate) async fn require_term_is_shared<'db>(
25    env: &mut Env<'db>,
26    term: SymGenericTerm<'db>,
27    or_else: &dyn OrElse<'db>,
28) -> Errors<()> {
29    match term {
30        SymGenericTerm::Type(sym_ty) => require_ty_is_shared(env, sym_ty, or_else).await,
31        SymGenericTerm::Perm(sym_perm) => require_perm_is_shared(env, sym_perm, or_else).await,
32        SymGenericTerm::Place(place) => panic!("unexpected place term: {place:?}"),
33        SymGenericTerm::Error(reported) => Err(reported),
34    }
35}
36
37/// Requires that `(lhs rhs)` satisfies the given predicate.
38/// The semantics of `(lhs rhs)` is: `rhs` if `rhs is copy` or `lhs union rhs` otherwise.
39async fn require_either_is_shared<'db>(
40    env: &mut Env<'db>,
41    lhs: SymGenericTerm<'db>,
42    rhs: SymGenericTerm<'db>,
43    or_else: &dyn OrElse<'db>,
44) -> Errors<()> {
45    // Simultaneously test for whether LHS/RHS is `predicate`.
46    // If either is, we are done.
47    // If either is *not*, the other must be.
48    env.require_both(
49        async |env| {
50            if !term_is_provably_shared(env, rhs).await? {
51                require_term_is_shared(env, lhs, or_else).await?;
52            }
53            Ok(())
54        },
55        async |env| {
56            if !term_is_provably_shared(env, lhs).await? {
57                require_term_is_shared(env, rhs, or_else).await?;
58            }
59            Ok(())
60        },
61    )
62    .await
63}
64
65#[boxed_async_fn]
66async fn require_ty_is_shared<'db>(
67    env: &mut Env<'db>,
68    term: SymTy<'db>,
69    or_else: &dyn OrElse<'db>,
70) -> Errors<()> {
71    env.indent("require_ty_is_shared", &[&term], async |env| {
72        let db = env.db();
73        let (red_ty, perm) = term.to_red_ty(env);
74        match red_ty {
75            // Error cases first
76            RedTy::Error(reported) => Err(reported),
77
78            // Never
79            RedTy::Never => Err(or_else.report(env, Because::NeverIsNotCopy)),
80
81            // Inference variables
82            RedTy::Infer(infer) => {
83                require_infer_is(env, perm, infer, Predicate::Shared, or_else).await
84            }
85
86            // Universal variables
87            RedTy::Var(var) => {
88                env.require(
89                    async |env| {
90                        env.either(
91                            async |env| perm_is_provably_shared(env, perm).await,
92                            async |env| Ok(env.var_is_declared_to_be(var, Predicate::Shared)),
93                        )
94                        .await
95                    },
96                    |_env| Because::JustSo,
97                    or_else,
98                )
99                .await
100            }
101
102            // Named types
103            RedTy::Named(sym_ty_name, ref generics) => match sym_ty_name.style(db) {
104                SymAggregateStyle::Struct => {
105                    require_generics_are_shared(env, perm, generics, or_else).await
106                }
107                SymAggregateStyle::Class => {
108                    env.require_both(
109                        async |env| require_perm_is_shared(env, perm, or_else).await,
110                        async |env| {
111                            require_generics_are_shared(env, SymPerm::my(db), generics, or_else)
112                                .await
113                        },
114                    )
115                    .await
116                }
117            },
118
119            RedTy::Perm => require_perm_is_shared(env, perm, or_else).await,
120        }
121    })
122    .await
123}
124
125async fn require_generics_are_shared<'db>(
126    env: &mut Env<'db>,
127    perm: SymPerm<'db>,
128    generics: &[SymGenericTerm<'db>],
129    or_else: &dyn OrElse<'db>,
130) -> Errors<()> {
131    let db = env.db();
132    env.require_for_all(generics, async |env, &generic| {
133        require_term_is_shared(env, perm.apply_to(db, generic), or_else).await
134    })
135    .await
136}
137
138#[boxed_async_fn]
139pub(super) async fn require_perm_is_shared<'db>(
140    env: &mut Env<'db>,
141    perm: SymPerm<'db>,
142    or_else: &dyn OrElse<'db>,
143) -> Errors<()> {
144    env.indent("require_perm_is_shared", &[&perm], async |env| {
145        let db = env.db();
146        match *perm.kind(db) {
147            SymPermKind::Error(reported) => Err(reported),
148
149            SymPermKind::My => Err(or_else.report(env, Because::JustSo)),
150
151            SymPermKind::Our => Ok(()),
152
153            SymPermKind::Referenced(_) => Ok(()),
154
155            SymPermKind::Mutable(ref places) => {
156                // For a mutable[p] to be copy, all the places in `p` must have copy permission.
157                env.require_for_all(places, async |env, &place| {
158                    require_place_is_shared(env, place, or_else).await
159                })
160                .await
161            }
162
163            // Apply
164            SymPermKind::Apply(lhs, rhs) => {
165                require_either_is_shared(env, lhs.into(), rhs.into(), or_else).await
166            }
167
168            // Variable and inference
169            SymPermKind::Var(var) => require_var_is(env, var, Predicate::Shared, or_else),
170
171            SymPermKind::Infer(infer) => {
172                require_infer_is(env, SymPerm::my(db), infer, Predicate::Shared, or_else).await
173            }
174
175            SymPermKind::Or(_, _) => todo!(),
176        }
177    })
178    .await
179}
180
181pub(crate) async fn require_place_is_shared<'db>(
182    env: &mut Env<'db>,
183    place: SymPlace<'db>,
184    or_else: &dyn OrElse<'db>,
185) -> Errors<()> {
186    env.indent("require_place_is_shared", &[&place], async |env| {
187        let ty = place.place_ty(env).await;
188        require_ty_is_shared(env, ty, or_else).await
189    })
190    .await
191}
dada_ir_sym/check/predicates/require_shared.rs

dada_ir_sym/check/predicates/
require_shared.rs
