dada_ir_sym/check/
red.rs

1//! "Chains" are a canonicalized form of types/permissions.
2//! They can only be produced after inference is complete as they require enumerating the bounds of inference variables.
3//! They are used in borrow checking and for producing the final version of each inference variable.
4
5use dada_ir_ast::diagnostic::{Err, Errors, Reported};
6use dada_util::SalsaSerialize;
7use salsa::Update;
8use serde::Serialize;
9
10use crate::ir::{
11    indices::{FromInfer, InferVarIndex},
12    types::{SymGenericTerm, SymPerm, SymPlace, SymTy, SymTyName},
13    variables::SymVariable,
14};
15
16use super::{env::Env, predicates::Predicate};
17
18pub mod lattice;
19pub mod sub;
20
21/// A "lien chain" is a list of permissions by which some data may have been reached.
22/// An empty lien chain corresponds to owned data (`my`, in surface Dada syntax).
23/// A lien chain like `ref[p] mut[q]` would correspond to data referencing a variable `p`
24/// which in turn had data mutable from `q` (which in turn owned the data).
25#[derive(SalsaSerialize)]
26#[salsa::interned(debug)]
27pub(crate) struct RedPerm<'db> {
28    #[return_ref]
29    pub chains: Vec<RedChain<'db>>,
30}
31
32impl<'db> RedPerm<'db> {
33    /// Returns the fallback bound for a permission (`my`)
34    pub fn fallback(db: &'db dyn crate::Db) -> Self {
35        RedPerm::new(db, vec![RedChain::new(db, vec![])])
36    }
37
38    pub fn is_provably(self, env: &Env<'db>, predicate: Predicate) -> Errors<bool> {
39        let chains = self.chains(env.db());
40        assert!(!chains.is_empty());
41        for chain in chains {
42            if !chain.is_provably(env, predicate)? {
43                return Ok(false);
44            }
45        }
46        Ok(true)
47    }
48
49    #[expect(dead_code)]
50    pub fn is_our(self, env: &Env<'db>) -> Errors<bool> {
51        Ok(self.is_provably(env, Predicate::Shared)? && self.is_provably(env, Predicate::Owned)?)
52    }
53
54    pub fn to_sym_perm(self, db: &'db dyn crate::Db) -> SymPerm<'db> {
55        self.chains(db)
56            .iter()
57            .map(|&chain| chain.to_sym_perm(db))
58            .reduce(|perm1, perm2| SymPerm::or(db, perm1, perm2))
59            .unwrap()
60    }
61}
62
63impl<'db> Err<'db> for RedPerm<'db> {
64    fn err(db: &'db dyn dada_ir_ast::Db, reported: Reported) -> Self {
65        RedPerm::new(db, vec![RedChain::err(db, reported)])
66    }
67}
68
69#[derive(SalsaSerialize)]
70#[salsa::interned(debug)]
71pub(crate) struct RedChain<'db> {
72    #[return_ref]
73    pub links: Vec<RedLink<'db>>,
74}
75
76impl<'db> RedChain<'db> {
77    pub fn our(db: &'db dyn crate::Db) -> Self {
78        RedChain::new(db, [RedLink::Our])
79    }
80
81    pub fn is_provably(self, env: &Env<'db>, predicate: Predicate) -> Errors<bool> {
82        let db = env.db();
83        match predicate {
84            Predicate::Shared => RedLink::are_copy(env, self.links(db)),
85            Predicate::Unique => RedLink::are_move(env, self.links(db)),
86            Predicate::Owned => RedLink::are_owned(env, self.links(db)),
87            Predicate::Lent => RedLink::are_lent(env, self.links(db)),
88        }
89    }
90
91    fn to_sym_perm(self, db: &'db dyn crate::Db) -> SymPerm<'db> {
92        self.links(db)
93            .iter()
94            .map(|&link| link.to_sym_perm(db))
95            .reduce(|perm1, perm2| SymPerm::apply(db, perm1, perm2))
96            .unwrap_or_else(|| SymPerm::my(db))
97    }
98}
99
100impl<'db> Err<'db> for RedChain<'db> {
101    fn err(db: &'db dyn dada_ir_ast::Db, reported: Reported) -> Self {
102        RedChain::new(db, vec![RedLink::err(db, reported)])
103    }
104}
105
106#[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize)]
107pub(crate) enum RedLink<'db> {
108    Our,
109    Ref(Live, SymPlace<'db>),
110    Mut(Live, SymPlace<'db>),
111    Var(SymVariable<'db>),
112    Err(Reported),
113}
114
115#[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize)]
116pub struct Live(pub bool);
117
118impl<'db> RedLink<'db> {
119    pub fn are_copy(env: &Env<'db>, links: &[Self]) -> Errors<bool> {
120        let Some(first) = links.first() else {
121            return Ok(false);
122        };
123        first.is_copy(env)
124    }
125
126    pub fn are_move(env: &Env<'db>, links: &[Self]) -> Errors<bool> {
127        for link in links {
128            if !link.is_move(env)? {
129                return Ok(false);
130            }
131        }
132        Ok(true)
133    }
134
135    pub fn are_owned(env: &Env<'db>, links: &[Self]) -> Errors<bool> {
136        for link in links {
137            if !link.is_owned(env)? {
138                return Ok(false);
139            }
140        }
141        Ok(true)
142    }
143
144    pub fn are_lent(env: &Env<'db>, links: &[Self]) -> Errors<bool> {
145        for link in links {
146            if !link.is_lent(env)? {
147                return Ok(true);
148            }
149        }
150        Ok(false)
151    }
152
153    pub fn is_owned(&self, env: &Env<'db>) -> Errors<bool> {
154        match self {
155            RedLink::Our => Ok(true),
156            RedLink::Var(v) => Ok(env.var_is_declared_to_be(*v, Predicate::Owned)),
157            RedLink::Ref(..) | RedLink::Mut(..) => Ok(false),
158            RedLink::Err(reported) => Err(*reported),
159        }
160    }
161
162    pub fn is_lent(&self, env: &Env<'db>) -> Errors<bool> {
163        match self {
164            RedLink::Ref(..) | RedLink::Mut(..) => Ok(true),
165            RedLink::Var(v) => Ok(env.var_is_declared_to_be(*v, Predicate::Lent)),
166            RedLink::Our => Ok(false),
167            RedLink::Err(reported) => Err(*reported),
168        }
169    }
170
171    pub fn is_move(&self, env: &Env<'db>) -> Errors<bool> {
172        match self {
173            RedLink::Mut(..) => Ok(true),
174            RedLink::Var(v) => Ok(env.var_is_declared_to_be(*v, Predicate::Unique)),
175            RedLink::Our | RedLink::Ref(..) => Ok(false),
176            RedLink::Err(reported) => Err(*reported),
177        }
178    }
179
180    pub fn is_copy(&self, env: &Env<'db>) -> Errors<bool> {
181        match self {
182            RedLink::Our | RedLink::Ref(..) => Ok(true),
183            RedLink::Var(v) => Ok(env.var_is_declared_to_be(*v, Predicate::Shared)),
184            RedLink::Mut(..) => Ok(false),
185            RedLink::Err(reported) => Err(*reported),
186        }
187    }
188
189    pub fn to_sym_perm(self, db: &'db dyn crate::Db) -> SymPerm<'db> {
190        match self {
191            RedLink::Our => SymPerm::our(db),
192            RedLink::Ref(_, place) => SymPerm::referenced(db, vec![place]),
193            RedLink::Mut(_, place) => SymPerm::mutable(db, vec![place]),
194            RedLink::Var(v) => SymPerm::var(db, v),
195            RedLink::Err(reported) => SymPerm::err(db, reported),
196        }
197    }
198}
199
200impl<'db> Err<'db> for RedLink<'db> {
201    fn err(_db: &'db dyn dada_ir_ast::Db, reported: Reported) -> Self {
202        RedLink::Err(reported)
203    }
204}
205
206/// A "red(uced) type"-- captures just the
207/// type layout part of a [`SymGenericTerm`][].
208#[derive(Debug, PartialEq, Eq, Clone, PartialOrd, Ord, Hash, Update, Serialize)]
209pub enum RedTy<'db> {
210    /// An error occurred while processing this type.
211    Error(Reported),
212
213    /// A named type.
214    Named(SymTyName<'db>, Vec<SymGenericTerm<'db>>),
215
216    /// Never type.
217    Never,
218
219    /// An inference variable.
220    Infer(InferVarIndex),
221
222    /// A variable.
223    Var(SymVariable<'db>),
224
225    /// A permission -- this variant occurs when we convert a [`SymPerm`] to a [`RedTy`].
226    Perm,
227}
228
229impl<'db> Err<'db> for RedTy<'db> {
230    fn err(_db: &'db dyn crate::Db, reported: Reported) -> Self {
231        RedTy::Error(reported)
232    }
233}
234
235impl<'db> RedTy<'db> {
236    /// Inference fallback
237    pub fn fallback(_db: &'db dyn crate::Db) -> Self {
238        RedTy::Never
239    }
240
241    pub fn into_sym_ty(self, db: &'db dyn crate::Db) -> SymTy<'db> {
242        match self {
243            RedTy::Error(reported) => SymTy::err(db, reported),
244            RedTy::Named(name, terms) => SymTy::named(db, name, terms),
245            RedTy::Never => SymTy::never(db),
246            RedTy::Infer(var_index) => SymTy::infer(db, var_index),
247            RedTy::Var(variable) => SymTy::var(db, variable),
248            RedTy::Perm => panic!("unexpected RedTy (perm)"),
249        }
250    }
251}
dada_ir_sym/check/red.rs

dada_ir_sym/check/
red.rs
