dada_ir_sym/check/predicates/
require_lent.rs

1use dada_ir_ast::diagnostic::Errors;
2use dada_util::boxed_async_fn;
3
4use crate::{
5    check::{
6        env::Env,
7        predicates::{
8            Predicate,
9            var_infer::{require_infer_is, require_var_is},
10        },
11        red::RedTy,
12        report::{Because, OrElse},
13        to_red::ToRedTy,
14    },
15    ir::{
16        classes::SymAggregateStyle,
17        types::{SymGenericTerm, SymPerm, SymPermKind, SymTy},
18    },
19};
20
21use super::{
22    is_provably_lent::{place_is_provably_lent, term_is_provably_lent},
23    is_provably_unique::{place_is_provably_unique, term_is_provably_unique},
24};
25
26pub(crate) async fn require_term_is_lent<'db>(
27    env: &mut Env<'db>,
28    term: SymGenericTerm<'db>,
29    or_else: &dyn OrElse<'db>,
30) -> Errors<()> {
31    match term {
32        SymGenericTerm::Type(sym_ty) => require_ty_is_lent(env, sym_ty, or_else).await,
33        SymGenericTerm::Perm(sym_perm) => require_perm_is_lent(env, sym_perm, or_else).await,
34        SymGenericTerm::Place(place) => panic!("unexpected place term: {place:?}"),
35        SymGenericTerm::Error(reported) => Err(reported),
36    }
37}
38
39/// Requires that `(lhs rhs)` satisfies the given predicate.
40/// The semantics of `(lhs rhs)` is: `rhs` if `rhs is copy` or `lhs union rhs` otherwise.
41async fn require_application_is_lent<'db>(
42    env: &mut Env<'db>,
43    lhs: SymGenericTerm<'db>,
44    rhs: SymGenericTerm<'db>,
45    or_else: &dyn OrElse<'db>,
46) -> Errors<()> {
47    env.require(
48        async |env| {
49            env.either(
50                async |env| term_is_provably_lent(env, rhs).await,
51                async |env| {
52                    env.both(
53                        async |env| term_is_provably_unique(env, rhs).await,
54                        async |env| term_is_provably_lent(env, lhs).await,
55                    )
56                    .await
57                },
58            )
59            .await
60        },
61        |_env| Because::JustSo,
62        or_else,
63    )
64    .await
65}
66
67#[boxed_async_fn]
68async fn require_ty_is_lent<'db>(
69    env: &mut Env<'db>,
70    term: SymTy<'db>,
71    or_else: &dyn OrElse<'db>,
72) -> Errors<()> {
73    env.indent("require_ty_is_lent", &[&term], async |env| {
74        let db = env.db();
75        let (red_ty, perm) = term.to_red_ty(env);
76        match red_ty {
77            // Error cases first
78            RedTy::Error(reported) => Err(reported),
79
80            // Never
81            RedTy::Never => require_perm_is_lent(env, perm, or_else).await,
82
83            // Inference
84            RedTy::Infer(infer) => {
85                require_infer_is(env, perm, infer, Predicate::Lent, or_else).await
86            }
87
88            // Generic variable
89            RedTy::Var(var) => {
90                if env.var_is_declared_to_be(var, Predicate::Lent) {
91                    Ok(())
92                } else if env.var_is_declared_to_be(var, Predicate::Unique) {
93                    // If the perm is not known to be unique,
94                    // it might be a shared type, in which case,
95                    // even if `perm` is lent it doesn't matter.
96                    require_perm_is_lent(env, perm, or_else).await
97                } else {
98                    Err(or_else.report(env, Because::NoWhereClause(var, Predicate::Lent)))
99                }
100            }
101
102            // Named types
103            RedTy::Named(sym_ty_name, _) => match sym_ty_name.style(db) {
104                SymAggregateStyle::Struct => {
105                    // Structs are never *lent*.
106                    //
107                    // They can always have at least some content
108                    // that is owned.
109                    Err(or_else.report(env, Because::StructsAreNotLent(sym_ty_name)))
110                }
111                SymAggregateStyle::Class => {
112                    // For a class to be lent, the permission must be lent.
113                    //
114                    // We don't consider `Vec[ref[x] String]` to be lent
115                    // (though it is also not owned).
116                    require_perm_is_lent(env, perm, or_else).await
117                }
118            },
119
120            RedTy::Perm => require_perm_is_lent(env, perm, or_else).await,
121        }
122    })
123    .await
124}
125
126#[boxed_async_fn]
127async fn require_perm_is_lent<'db>(
128    env: &mut Env<'db>,
129    perm: SymPerm<'db>,
130    or_else: &dyn OrElse<'db>,
131) -> Errors<()> {
132    env.indent("require_perm_is_lent", &[&perm], async |env| {
133        let db = env.db();
134        match *perm.kind(db) {
135            // Error cases first
136            SymPermKind::Error(reported) => Err(reported),
137
138            // My = Move & Owned
139            SymPermKind::My => Err(or_else.report(env, Because::PermIsNot(perm, Predicate::Lent))),
140
141            // Our = Copy & Owned & Lent -- the latter because of subtyping
142            SymPermKind::Our => Ok(()),
143
144            // Shared = Copy & Lent, Mutable = Move & Lent
145            SymPermKind::Referenced(ref places) | SymPermKind::Mutable(ref places) => {
146                // This one is tricky. If the places are copy,
147                // then we will reduce to their chains, but then
148                // we would be lent if they are lent; but if they are not
149                // copy, we are lent.
150                env.require(
151                    async |env| {
152                        env.for_all(places, async |env, &place| {
153                            env.either(
154                                // If the place `p` is move, then the result will be `shared[p]` or `mutable[p]` perm,
155                                // which is lent.
156                                async |env| place_is_provably_unique(env, place).await,
157                                // Or, if the place `p` is not move and hence may be copy, then it must itself be `lent`.
158                                async |env| place_is_provably_lent(env, place).await,
159                            )
160                            .await
161                        })
162                        .await
163                    },
164                    |_env| Because::PermIsNot(perm, Predicate::Lent),
165                    or_else,
166                )
167                .await
168            }
169
170            // Apply
171            SymPermKind::Apply(lhs, rhs) => {
172                require_application_is_lent(env, lhs.into(), rhs.into(), or_else).await
173            }
174
175            // Variable and inference
176            SymPermKind::Var(var) => require_var_is(env, var, Predicate::Lent, or_else),
177            SymPermKind::Infer(infer) => {
178                require_infer_is(env, SymPerm::my(db), infer, Predicate::Lent, or_else).await
179            }
180            SymPermKind::Or(_, _) => todo!(),
181        }
182    })
183    .await
184}
dada_ir_sym/check/predicates/require_lent.rs

dada_ir_sym/check/predicates/
require_lent.rs
