luaur_analysis/records/
refinement_arena_refinement.rs1use 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 pub fn variadic(&mut self, refis: &[RefinementId]) -> RefinementId {
23 let mut has_refinements = false;
27 for r in refis {
28 has_refinements |= !r.is_null();
29 }
30
31 if !has_refinements {
34 return core::ptr::null_mut();
35 }
36
37 self.allocator.allocate(Refinement::Variadic(Variadic {
39 refinements: refis.to_vec(),
40 }))
41 }
42
43 pub fn negation(&mut self, refinement: RefinementId) -> RefinementId {
45 if refinement.is_null() {
48 return core::ptr::null_mut();
49 }
50
51 self.allocator
53 .allocate(Refinement::Negation(Negation { refinement }))
54 }
55
56 pub fn conjunction(&mut self, lhs: RefinementId, rhs: RefinementId) -> RefinementId {
58 if lhs.is_null() && rhs.is_null() {
61 return core::ptr::null_mut();
62 }
63
64 self.allocator
66 .allocate(Refinement::Conjunction(Conjunction { lhs, rhs }))
67 }
68
69 pub fn disjunction(&mut self, lhs: RefinementId, rhs: RefinementId) -> RefinementId {
71 if lhs.is_null() && rhs.is_null() {
74 return core::ptr::null_mut();
75 }
76
77 self.allocator
79 .allocate(Refinement::Disjunction(Disjunction { lhs, rhs }))
80 }
81
82 pub fn equivalence(&mut self, lhs: RefinementId, rhs: RefinementId) -> RefinementId {
84 if lhs.is_null() && rhs.is_null() {
87 return core::ptr::null_mut();
88 }
89
90 self.allocator
92 .allocate(Refinement::Equivalence(Equivalence { lhs, rhs }))
93 }
94
95 pub fn proposition(
97 &mut self,
98 key: *const RefinementKey,
99 discriminant_ty: TypeId,
100 ) -> RefinementId {
101 if key.is_null() {
104 return core::ptr::null_mut();
105 }
106
107 self.allocator
109 .allocate(Refinement::Proposition(Proposition {
110 key,
111 discriminantTy: discriminant_ty,
112 implicitFromCall: false,
113 }))
114 }
115
116 pub fn implicit_proposition(
118 &mut self,
119 key: *const RefinementKey,
120 discriminant_ty: TypeId,
121 ) -> RefinementId {
122 if key.is_null() {
125 return core::ptr::null_mut();
126 }
127
128 self.allocator
130 .allocate(Refinement::Proposition(Proposition {
131 key,
132 discriminantTy: discriminant_ty,
133 implicitFromCall: true,
134 }))
135 }
136}