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