1#[cfg(not(feature = "std"))]
2use alloc::{string::String, vec::Vec};
3#[cfg(feature = "std")]
4use std::{string::String, vec::Vec};
5
6use crate::{AlgebraicSignature, Obligation, Origin};
7
8#[derive(Debug, Clone, PartialEq, Eq)]
10pub struct ObligationBundle {
11 pub name: String,
12 pub origin: Origin,
13 obligations: Vec<Obligation>,
14}
15
16impl ObligationBundle {
17 pub fn new(name: impl Into<String>, origin: Origin) -> Self {
18 Self {
19 name: name.into(),
20 origin,
21 obligations: Vec::new(),
22 }
23 }
24
25 pub fn with(mut self, obligation: Obligation) -> Self {
26 self.obligations.push(obligation);
27 self
28 }
29
30 pub fn push(&mut self, obligation: Obligation) {
31 self.obligations.push(obligation);
32 }
33
34 pub fn obligations(&self) -> &[Obligation] {
35 &self.obligations
36 }
37
38 pub fn into_obligations(self) -> Vec<Obligation> {
39 self.obligations
40 }
41
42 pub fn semigroup(
43 name: impl Into<String>,
44 origin: Origin,
45 signature: &AlgebraicSignature,
46 ) -> Self {
47 Self::new(name, origin.clone()).with(Obligation::associativity_in(
48 "associativity",
49 origin,
50 signature,
51 "combine",
52 ))
53 }
54
55 pub fn monoid(name: impl Into<String>, origin: Origin, signature: &AlgebraicSignature) -> Self {
56 Self::new(name, origin.clone())
57 .with(Obligation::associativity_in(
58 "associativity",
59 origin.clone(),
60 signature,
61 "combine",
62 ))
63 .with(Obligation::left_identity_in(
64 "left_identity",
65 origin.clone(),
66 signature,
67 "combine",
68 "identity",
69 ))
70 .with(Obligation::right_identity_in(
71 "right_identity",
72 origin,
73 signature,
74 "combine",
75 "identity",
76 ))
77 }
78
79 pub fn group(name: impl Into<String>, origin: Origin, signature: &AlgebraicSignature) -> Self {
80 Self::monoid(name, origin.clone(), signature)
81 .with(Obligation::left_inverse_in(
82 "left_inverse",
83 origin.clone(),
84 signature,
85 ))
86 .with(Obligation::right_inverse_in(
87 "right_inverse",
88 origin,
89 signature,
90 ))
91 }
92
93 pub fn semiring(
94 name: impl Into<String>,
95 origin: Origin,
96 signature: &AlgebraicSignature,
97 ) -> Self {
98 Self::new(name, origin.clone())
99 .with(Obligation::associativity_in(
100 "add_associativity",
101 origin.clone(),
102 signature,
103 "add",
104 ))
105 .with(Obligation::associativity_in(
106 "mul_associativity",
107 origin.clone(),
108 signature,
109 "mul",
110 ))
111 .with(Obligation::additive_commutativity_in(
112 "add_commutativity",
113 origin.clone(),
114 signature,
115 ))
116 .with(Obligation::left_identity_in(
117 "add_left_identity",
118 origin.clone(),
119 signature,
120 "add",
121 "zero",
122 ))
123 .with(Obligation::right_identity_in(
124 "add_right_identity",
125 origin.clone(),
126 signature,
127 "add",
128 "zero",
129 ))
130 .with(Obligation::left_identity_in(
131 "mul_left_identity",
132 origin.clone(),
133 signature,
134 "mul",
135 "one",
136 ))
137 .with(Obligation::right_identity_in(
138 "mul_right_identity",
139 origin.clone(),
140 signature,
141 "mul",
142 "one",
143 ))
144 .with(Obligation::left_distributivity_in(
145 "left_distributivity",
146 origin.clone(),
147 signature,
148 ))
149 .with(Obligation::right_distributivity_in(
150 "right_distributivity",
151 origin,
152 signature,
153 ))
154 }
155
156 pub fn ring(name: impl Into<String>, origin: Origin, signature: &AlgebraicSignature) -> Self {
157 Self::semiring(name, origin.clone(), signature)
158 .with(Obligation::left_inverse(
159 "add_left_inverse",
160 origin.clone(),
161 signature.carrier.clone(),
162 signature.require_binary("add"),
163 signature.require_unary("neg"),
164 signature.require_constant("zero"),
165 ))
166 .with(Obligation::right_inverse(
167 "add_right_inverse",
168 origin,
169 signature.carrier.clone(),
170 signature.require_binary("add"),
171 signature.require_unary("neg"),
172 signature.require_constant("zero"),
173 ))
174 }
175
176 pub fn lattice(
177 name: impl Into<String>,
178 origin: Origin,
179 signature: &AlgebraicSignature,
180 ) -> Self {
181 Self::new(name, origin.clone())
182 .with(Obligation::associativity_in(
183 "meet_associativity",
184 origin.clone(),
185 signature,
186 "meet",
187 ))
188 .with(Obligation::associativity_in(
189 "join_associativity",
190 origin.clone(),
191 signature,
192 "join",
193 ))
194 .with(Obligation::commutativity_in(
195 "meet_commutativity",
196 origin.clone(),
197 signature,
198 "meet",
199 ))
200 .with(Obligation::commutativity_in(
201 "join_commutativity",
202 origin.clone(),
203 signature,
204 "join",
205 ))
206 .with(Obligation::idempotency_in(
207 "meet_idempotency",
208 origin.clone(),
209 signature,
210 "meet",
211 ))
212 .with(Obligation::idempotency_in(
213 "join_idempotency",
214 origin.clone(),
215 signature,
216 "join",
217 ))
218 .with(Obligation::absorption_in("absorption", origin, signature))
219 }
220}
221
222#[cfg(test)]
223mod tests {
224 use super::*;
225 use crate::Sort;
226
227 #[test]
228 fn monoid_bundle_contains_expected_laws() {
229 let sig = AlgebraicSignature::monoid(Sort::Int, "combine", "e");
230 let bundle = ObligationBundle::monoid("sum", Origin::new("karpal-core", "Sum<i32>"), &sig);
231 assert_eq!(bundle.obligations().len(), 3);
232 }
233
234 #[test]
235 fn semiring_bundle_contains_expected_laws() {
236 let sig = AlgebraicSignature::semiring(Sort::Int, "add", "mul", "zero", "one");
237 let bundle = ObligationBundle::semiring("ring", Origin::new("karpal-algebra", "i32"), &sig);
238 assert_eq!(bundle.obligations().len(), 9);
239 }
240
241 #[test]
242 fn ring_bundle_contains_additive_inverse_laws() {
243 let sig = AlgebraicSignature::ring(Sort::Int, "add", "mul", "zero", "one", "neg");
244 let bundle = ObligationBundle::ring("ring", Origin::new("karpal-algebra", "i32"), &sig);
245 assert_eq!(bundle.obligations().len(), 11);
246 assert!(
247 bundle
248 .obligations()
249 .iter()
250 .any(|obligation| obligation.name == "add_left_inverse")
251 );
252 }
253}