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