dada_ir_sym/check/
predicates.rs

1//! Permission system and ownership predicates.
2#![doc = include_str!("../../docs/permission_system.md")]
3
4pub mod is_provably_lent;
5pub mod is_provably_owned;
6pub mod is_provably_shared;
7pub mod is_provably_unique;
8pub mod require_lent;
9pub mod require_owned;
10pub mod require_shared;
11pub mod require_unique;
12pub mod require_where_clause;
13pub mod var_infer;
14
15use dada_ir_ast::diagnostic::Errors;
16use is_provably_lent::term_is_provably_lent;
17use is_provably_owned::term_is_provably_owned;
18use is_provably_shared::term_is_provably_shared;
19use is_provably_unique::term_is_provably_unique;
20use require_lent::require_term_is_lent;
21use require_owned::require_term_is_owned;
22use require_shared::require_term_is_shared;
23use require_unique::require_term_is_unique;
24use serde::Serialize;
25
26use crate::ir::types::SymGenericTerm;
27
28use super::{env::Env, report::OrElse};
29
30#[derive(Copy, Clone, Debug, Eq, PartialEq, Hash, Ord, PartialOrd, Serialize)]
31pub enum Predicate {
32    Shared,
33    Unique,
34    Owned,
35    Lent,
36}
37
38impl std::fmt::Display for Predicate {
39    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
40        match self {
41            Predicate::Shared => write!(f, "copy"),
42            Predicate::Unique => write!(f, "move"),
43            Predicate::Owned => write!(f, "owned"),
44            Predicate::Lent => write!(f, "lent"),
45        }
46    }
47}
48
49pub(crate) async fn require_term_is<'db>(
50    env: &mut Env<'db>,
51    term: impl Into<SymGenericTerm<'db>>,
52    predicate: Predicate,
53    or_else: &dyn OrElse<'db>,
54) -> Errors<()> {
55    let term: SymGenericTerm<'db> = term.into();
56    match predicate {
57        Predicate::Shared => require_term_is_shared(env, term, or_else).await,
58        Predicate::Unique => require_term_is_unique(env, term, or_else).await,
59        Predicate::Owned => require_term_is_owned(env, term, or_else).await,
60        Predicate::Lent => require_term_is_lent(env, term, or_else).await,
61    }
62}
63
64pub(crate) async fn term_is_provably<'db>(
65    env: &mut Env<'db>,
66    term: impl Into<SymGenericTerm<'db>>,
67    predicate: Predicate,
68) -> Errors<bool> {
69    let term: SymGenericTerm<'db> = term.into();
70    match predicate {
71        Predicate::Shared => term_is_provably_shared(env, term).await,
72        Predicate::Unique => term_is_provably_unique(env, term).await,
73        Predicate::Owned => term_is_provably_owned(env, term).await,
74        Predicate::Lent => term_is_provably_lent(env, term).await,
75    }
76}
dada_ir_sym/check/predicates.rs

dada_ir_sym/check/
predicates.rs
