dada_ir_sym/check/predicates/
require_unique.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::is_provably_unique::{place_is_provably_unique, term_is_provably_unique};
22
23pub(crate) async fn require_term_is_unique<'db>(
24    env: &mut Env<'db>,
25    term: SymGenericTerm<'db>,
26    or_else: &dyn OrElse<'db>,
27) -> Errors<()> {
28    match term {
29        SymGenericTerm::Type(sym_ty) => require_ty_is_unique(env, sym_ty, or_else).await,
30        SymGenericTerm::Perm(sym_perm) => require_perm_is_unique(env, sym_perm, or_else).await,
31        SymGenericTerm::Place(place) => panic!("unexpected place term: {place:?}"),
32        SymGenericTerm::Error(reported) => Err(reported),
33    }
34}
35
36#[boxed_async_fn]
37async fn require_ty_is_unique<'db>(
38    env: &mut Env<'db>,
39    term: SymTy<'db>,
40    or_else: &dyn OrElse<'db>,
41) -> Errors<()> {
42    env.indent("require_ty_is_unique", &[&term], async |env| {
43        let db = env.db();
44        let (red_ty, perm) = term.to_red_ty(env);
45        match red_ty {
46            // Error cases first
47            RedTy::Error(reported) => Err(reported),
48
49            // Never
50            RedTy::Never => require_perm_is_unique(env, perm, or_else).await,
51
52            // Variable and inference
53            RedTy::Infer(infer) => {
54                require_infer_is(env, perm, infer, Predicate::Unique, or_else).await
55            }
56
57            RedTy::Var(var) => {
58                // The variable must be unique, but in that case, the permission must also be
59                env.require_both(
60                    async |env| require_perm_is_unique(env, perm, or_else).await,
61                    async |env| require_var_is(env, var, Predicate::Unique, or_else),
62                )
63                .await
64            }
65
66            // Named types
67            RedTy::Named(sym_ty_name, ref generics) => match sym_ty_name.style(db) {
68                SymAggregateStyle::Struct => {
69                    require_some_generic_is_unique(env, perm, generics, or_else).await
70                }
71                SymAggregateStyle::Class => require_perm_is_unique(env, perm, or_else).await,
72            },
73
74            RedTy::Perm => require_perm_is_unique(env, perm, or_else).await,
75        }
76    })
77    .await
78}
79
80async fn require_some_generic_is_unique<'db>(
81    env: &mut Env<'db>,
82    perm: SymPerm<'db>,
83    generics: &[SymGenericTerm<'db>],
84    or_else: &dyn OrElse<'db>,
85) -> Errors<()> {
86    let db = env.db();
87    env.require(
88        async |env| {
89            env.exists(generics, async |env, &generic| {
90                term_is_provably_unique(env, perm.apply_to(db, generic)).await
91            })
92            .await
93        },
94        |_env| Because::JustSo,
95        or_else,
96    )
97    .await
98}
99
100#[boxed_async_fn]
101async fn require_perm_is_unique<'db>(
102    env: &mut Env<'db>,
103    perm: SymPerm<'db>,
104    or_else: &dyn OrElse<'db>,
105) -> Errors<()> {
106    env.indent("require_perm_is_unique", &[&perm], async |env| {
107        let db = env.db();
108        match *perm.kind(db) {
109            SymPermKind::Error(reported) => Err(reported),
110
111            SymPermKind::My => Ok(()),
112
113            SymPermKind::Our => Err(or_else.report(env, Because::JustSo)),
114
115            SymPermKind::Referenced(_) => Err(or_else.report(env, Because::JustSo)),
116
117            SymPermKind::Mutable(ref places) => {
118                // If there is at least one place `p` that is move, this will result in a `mutable[p]` chain.
119                env.require(
120                    async |env| {
121                        env.exists(places, async |env, &place| {
122                            place_is_provably_unique(env, place).await
123                        })
124                        .await
125                    },
126                    |_env| Because::LeasedFromCopyIsCopy(places.to_vec()),
127                    or_else,
128                )
129                .await
130            }
131
132            // Apply
133            SymPermKind::Apply(lhs, rhs) => {
134                env.require_both(
135                    async |env| require_perm_is_unique(env, lhs, or_else).await,
136                    async |env| require_perm_is_unique(env, rhs, or_else).await,
137                )
138                .await
139            }
140
141            // Variable and inference
142            SymPermKind::Var(var) => require_var_is(env, var, Predicate::Unique, or_else),
143            SymPermKind::Infer(infer) => {
144                require_infer_is(env, SymPerm::my(db), infer, Predicate::Unique, or_else).await
145            }
146
147            SymPermKind::Or(_, _) => todo!(),
148        }
149    })
150    .await
151}
dada_ir_sym/check/predicates/require_unique.rs

dada_ir_sym/check/predicates/
require_unique.rs
