Skip to main content

luaur_analysis/records/
refinement_arena_refinement.rs

1//! Source: `Analysis/src/Refinement.cpp` (hand-ported)
2use crate::records::conjunction_refinement::Conjunction;
3use crate::records::disjunction_refinement::Disjunction;
4use crate::records::equivalence::Equivalence;
5use crate::records::negation_refinement::Negation;
6use crate::records::proposition_refinement::Proposition;
7use crate::records::refinement_key::RefinementKey;
8use crate::records::typed_allocator::TypedAllocator;
9use crate::records::variadic::Variadic;
10use crate::type_aliases::refinement_id_refinement::RefinementId;
11use crate::type_aliases::refinement_refinement::Refinement;
12use crate::type_aliases::type_id::TypeId;
13use alloc::vec::Vec;
14
15#[derive(Debug)]
16pub struct RefinementArena {
17    pub(crate) allocator: TypedAllocator<Refinement>,
18}
19
20impl RefinementArena {
21    // Analysis/src/Refinement.cpp:8 — RefinementId RefinementArena::variadic(const std::vector<RefinementId>& refis)
22    pub fn variadic(&mut self, refis: &[RefinementId]) -> RefinementId {
23        // bool hasRefinements = false;
24        // for (RefinementId r : refis)
25        //     hasRefinements |= bool(r);
26        let mut has_refinements = false;
27        for r in refis {
28            has_refinements |= !r.is_null();
29        }
30
31        // if (!hasRefinements)
32        //     return nullptr;
33        if !has_refinements {
34            return core::ptr::null_mut();
35        }
36
37        // return NotNull{allocator.allocate(Variadic{refis})};
38        self.allocator.allocate(Refinement::Variadic(Variadic {
39            refinements: refis.to_vec(),
40        }))
41    }
42
43    // Analysis/src/Refinement.cpp:20 — RefinementId RefinementArena::negation(RefinementId refinement)
44    pub fn negation(&mut self, refinement: RefinementId) -> RefinementId {
45        // if (!refinement)
46        //     return nullptr;
47        if refinement.is_null() {
48            return core::ptr::null_mut();
49        }
50
51        // return NotNull{allocator.allocate(Negation{refinement})};
52        self.allocator
53            .allocate(Refinement::Negation(Negation { refinement }))
54    }
55
56    // Analysis/src/Refinement.cpp:28 — RefinementId RefinementArena::conjunction(RefinementId lhs, RefinementId rhs)
57    pub fn conjunction(&mut self, lhs: RefinementId, rhs: RefinementId) -> RefinementId {
58        // if (!lhs && !rhs)
59        //     return nullptr;
60        if lhs.is_null() && rhs.is_null() {
61            return core::ptr::null_mut();
62        }
63
64        // return NotNull{allocator.allocate(Conjunction{lhs, rhs})};
65        self.allocator
66            .allocate(Refinement::Conjunction(Conjunction { lhs, rhs }))
67    }
68
69    // Analysis/src/Refinement.cpp:36 — RefinementId RefinementArena::disjunction(RefinementId lhs, RefinementId rhs)
70    pub fn disjunction(&mut self, lhs: RefinementId, rhs: RefinementId) -> RefinementId {
71        // if (!lhs && !rhs)
72        //     return nullptr;
73        if lhs.is_null() && rhs.is_null() {
74            return core::ptr::null_mut();
75        }
76
77        // return NotNull{allocator.allocate(Disjunction{lhs, rhs})};
78        self.allocator
79            .allocate(Refinement::Disjunction(Disjunction { lhs, rhs }))
80    }
81
82    // Analysis/src/Refinement.cpp:44 — RefinementId RefinementArena::equivalence(RefinementId lhs, RefinementId rhs)
83    pub fn equivalence(&mut self, lhs: RefinementId, rhs: RefinementId) -> RefinementId {
84        // if (!lhs && !rhs)
85        //     return nullptr;
86        if lhs.is_null() && rhs.is_null() {
87            return core::ptr::null_mut();
88        }
89
90        // return NotNull{allocator.allocate(Equivalence{lhs, rhs})};
91        self.allocator
92            .allocate(Refinement::Equivalence(Equivalence { lhs, rhs }))
93    }
94
95    // Analysis/src/Refinement.cpp:52 — RefinementId RefinementArena::proposition(const RefinementKey* key, TypeId discriminantTy)
96    pub fn proposition(
97        &mut self,
98        key: *const RefinementKey,
99        discriminant_ty: TypeId,
100    ) -> RefinementId {
101        // if (!key)
102        //     return nullptr;
103        if key.is_null() {
104            return core::ptr::null_mut();
105        }
106
107        // return NotNull{allocator.allocate(Proposition{key, discriminantTy, false})};
108        self.allocator
109            .allocate(Refinement::Proposition(Proposition {
110                key,
111                discriminantTy: discriminant_ty,
112                implicitFromCall: false,
113            }))
114    }
115
116    // Analysis/src/Refinement.cpp:60 — RefinementId RefinementArena::implicitProposition(const RefinementKey* key, TypeId discriminantTy)
117    pub fn implicit_proposition(
118        &mut self,
119        key: *const RefinementKey,
120        discriminant_ty: TypeId,
121    ) -> RefinementId {
122        // if (!key)
123        //     return nullptr;
124        if key.is_null() {
125            return core::ptr::null_mut();
126        }
127
128        // return NotNull{allocator.allocate(Proposition{key, discriminantTy, true})};
129        self.allocator
130            .allocate(Refinement::Proposition(Proposition {
131                key,
132                discriminantTy: discriminant_ty,
133                implicitFromCall: true,
134            }))
135    }
136}