dada_ir_sym/check/predicates/
require_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::{
9            Predicate,
10            var_infer::{require_infer_is, require_var_is},
11        },
12        red::RedTy,
13        report::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::term_is_provably_shared, require_shared::require_place_is_shared};
23
24pub(crate) async fn require_term_is_owned<'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_owned(env, sym_ty, or_else).await,
31        SymGenericTerm::Perm(sym_perm) => require_perm_is_owned(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_both_are_owned<'db>(
40    env: &mut Env<'db>,
41    lhs: SymGenericTerm<'db>,
42    rhs: SymGenericTerm<'db>,
43    or_else: &dyn OrElse<'db>,
44) -> Errors<()> {
45    env.require_both(
46        async |env| require_term_is_owned(env, rhs, or_else).await,
47        async |env| {
48            // this isn't *perfect* -- if we can prove that the `lhs` is owned, we don't
49            // need to be able to conclude whether `rhs` is copy or not.
50            //
51            // not sure if I have the right combinator for this =)
52            if !term_is_provably_shared(env, rhs).await? {
53                require_term_is_owned(env, lhs, or_else).await
54            } else {
55                Ok(())
56            }
57        },
58    )
59    .await
60}
61
62#[boxed_async_fn]
63async fn require_ty_is_owned<'db>(
64    env: &mut Env<'db>,
65    term: SymTy<'db>,
66    or_else: &dyn OrElse<'db>,
67) -> Errors<()> {
68    env.indent("require_ty_is_owned", &[&term], async |env| {
69        let db = env.db();
70        let (red_ty, perm) = term.to_red_ty(env);
71        match red_ty {
72            // Error cases first
73            RedTy::Error(reported) => Err(reported),
74
75            // Never
76            RedTy::Never => require_perm_is_owned(env, perm, or_else).await,
77
78            // Inference
79            RedTy::Infer(infer) => {
80                require_infer_is(env, perm, infer, Predicate::Owned, or_else).await
81            }
82
83            // Generic variables
84            RedTy::Var(var) => {
85                env.require_both(
86                    async |env| require_perm_is_owned(env, perm, or_else).await,
87                    async |env| require_var_is(env, var, Predicate::Owned, or_else),
88                )
89                .await
90            }
91
92            // Named types: owned if all their generics are owned
93            RedTy::Named(sym_ty_name, ref generics) => match sym_ty_name.style(db) {
94                SymAggregateStyle::Struct => {
95                    require_generics_are_owned(env, perm, generics, or_else).await
96                }
97                SymAggregateStyle::Class => {
98                    env.require_both(
99                        async |env| require_perm_is_owned(env, perm, or_else).await,
100                        async |env| {
101                            require_generics_are_owned(env, SymPerm::my(db), generics, or_else)
102                                .await
103                        },
104                    )
105                    .await
106                }
107            },
108
109            RedTy::Perm => require_perm_is_owned(env, perm, or_else).await,
110        }
111    })
112    .await
113}
114
115async fn require_generics_are_owned<'db>(
116    env: &mut Env<'db>,
117    perm: SymPerm<'db>,
118    generics: &[SymGenericTerm<'db>],
119    or_else: &dyn OrElse<'db>,
120) -> Errors<()> {
121    let db = env.db();
122    env.require_for_all(generics, async |env, &generic| {
123        require_term_is_owned(env, perm.apply_to(db, generic), or_else).await
124    })
125    .await
126}
127
128#[boxed_async_fn]
129async fn require_perm_is_owned<'db>(
130    env: &mut Env<'db>,
131    perm: SymPerm<'db>,
132    or_else: &dyn OrElse<'db>,
133) -> Errors<()> {
134    env.indent("require_perm_is_owned", &[&perm], async |env| {
135        let db = env.db();
136        match *perm.kind(db) {
137            // Error cases first
138            SymPermKind::Error(reported) => Err(reported),
139
140            // My = Move & Owned
141            SymPermKind::My => Ok(()),
142
143            // Our = Copy & Owned
144            SymPermKind::Our => Ok(()),
145
146            // Shared = Copy & Lent, Mutable = Move & Lent
147            SymPermKind::Referenced(ref places) | SymPermKind::Mutable(ref places) => {
148                // In order for a shared[p] or mutable[p] type to be owned,
149                // the `p` values must be `our` -- copy so that the shared/mutable
150                // doesn't apply, and then themselves owned.
151                env.require_for_all(places, async |env, &place| {
152                    env.require_both(
153                        async |env| require_place_is_shared(env, place, or_else).await,
154                        async |env| require_place_is_owned(env, place, or_else).await,
155                    )
156                    .await
157                })
158                .await
159            }
160
161            // Apply
162            SymPermKind::Apply(lhs, rhs) => {
163                require_both_are_owned(env, lhs.into(), rhs.into(), or_else).await
164            }
165
166            // Variable and inference
167            SymPermKind::Var(var) => require_var_is(env, var, Predicate::Owned, or_else),
168            SymPermKind::Infer(infer) => {
169                require_infer_is(env, SymPerm::my(db), infer, Predicate::Owned, or_else).await
170            }
171
172            SymPermKind::Or(_, _) => todo!(),
173        }
174    })
175    .await
176}
177
178async fn require_place_is_owned<'db>(
179    env: &mut Env<'db>,
180    place: SymPlace<'db>,
181    or_else: &dyn OrElse<'db>,
182) -> Errors<()> {
183    env.indent("require_place_is_owned", &[&place], async |env| {
184        let ty = place.place_ty(env).await;
185        require_ty_is_owned(env, ty, or_else).await
186    })
187    .await
188}
dada_ir_sym/check/predicates/require_owned.rs

dada_ir_sym/check/predicates/
require_owned.rs
