1pub trait BinaryFunc {
4 type L;
5
6 type R;
7
8 type Cod;
9
10 fn f(
11 _: Self::L,
12 _: Self::R,
13 ) -> Self::Cod;
14}
15
16pub trait ExtBinaryOp: BinaryFunc {}
19
20impl<T: BinaryFunc> ExtBinaryOp for T {}
21
22pub trait BinaryOp {
25 type S;
26
27 fn op(
28 _: Self::S,
29 _: Self::S,
30 ) -> Self::S;
31}
32
33fn is_left_identity<S, F>(
34 f: &F,
35 e: S,
36 x: S,
37) -> bool
38where
39 F: Fn(S, S) -> S,
40 S: Clone + PartialEq,
41{
42 f(e, x.clone()) == x
43}
44
45fn is_right_identity<S, F>(
46 f: &F,
47 e: S,
48 x: S,
49) -> bool
50where
51 F: Fn(S, S) -> S,
52 S: Clone + PartialEq,
53{
54 f(x.clone(), e) == x
55}
56
57fn is_identity<S, F>(
58 f: &F,
59 e: S,
60 x: S,
61) -> bool
62where
63 F: Fn(S, S) -> S,
64 S: Clone + PartialEq,
65{
66 is_left_identity(f, e.clone(), x.clone()) && is_right_identity(f, e, x)
67}
68
69pub trait Identity: BinaryOp {
72 fn e() -> Self::S;
73
74 fn assert(x: Self::S)
75 where
76 Self::S: Clone + PartialEq,
77 {
78 assert!(is_identity(&Self::op, Self::e(), x));
79 }
80}
81
82fn is_invertible<F, G, X>(
83 op: &F,
84 inv: &G,
85 e: X,
86 x: X,
87) -> bool
88where
89 F: Fn(X, X) -> X,
90 G: Fn(X) -> X,
91 X: Clone + PartialEq,
92{
93 op(x.clone(), inv(x.clone())) == e.clone()
94 && op(inv(x.clone()), x.clone()) == e
95}
96
97pub trait Inverse: Identity {
100 fn inv(_: Self::S) -> Self::S;
101
102 fn assert(x: Self::S)
103 where
104 Self::S: Clone + PartialEq,
105 {
106 assert!(is_invertible(&Self::op, &Self::inv, Self::e(), x));
107 }
108}
109
110fn is_commutative<F, X, Y>(
111 f: &F,
112 a: X,
113 b: X,
114) -> bool
115where
116 F: Fn(X, X) -> Y,
117 X: Clone,
118 Y: PartialEq,
119{
120 f(a.clone(), b.clone()) == f(b, a)
121}
122
123pub trait Commutative: BinaryOp {
126 fn assert(
127 a: Self::S,
128 b: Self::S,
129 ) where
130 Self::S: Clone + PartialEq,
131 {
132 assert!(is_commutative(&Self::op, a, b));
133 }
134}
135
136fn is_associative<F, X>(
137 f: &F,
138 a: X,
139 b: X,
140 c: X,
141) -> bool
142where
143 F: Fn(X, X) -> X,
144 X: Clone + PartialEq,
145{
146 f(f(a.clone(), b.clone()), c.clone()) == f(a, f(b, c))
147}
148
149pub trait Associative: BinaryOp {
152 fn assert(
153 x: Self::S,
154 y: Self::S,
155 z: Self::S,
156 ) where
157 Self::S: Clone + PartialEq,
158 {
159 assert!(is_associative(&Self::op, x, y, z));
160 }
161}
162
163fn is_idempotent<F, X>(
164 f: &F,
165 x: X,
166) -> bool
167where
168 F: Fn(X, X) -> X,
169 X: Clone + PartialEq,
170{
171 f(x.clone(), x.clone()) == x
172}
173
174pub trait Idempotence: BinaryOp {
175 fn assert(x: Self::S)
176 where
177 Self::S: Clone + PartialEq,
178 {
179 assert!(is_idempotent(&Self::op, x));
180 }
181}
182
183pub trait LatinSquare: BinaryOp {}
186
187impl<T: Inverse> LatinSquare for T {}
188
189fn is_left_absorbing<F, X>(
191 f: &F,
192 z: X,
193 x: X,
194) -> bool
195where
196 F: Fn(X, X) -> X,
197 X: Clone + PartialEq,
198{
199 f(z.clone(), x) == z
200}
201
202fn is_right_absorbing<F, X>(
203 f: &F,
204 z: X,
205 x: X,
206) -> bool
207where
208 F: Fn(X, X) -> X,
209 X: Clone + PartialEq,
210{
211 f(x, z.clone()) == z
212}
213
214fn is_absorbing<F, X>(
215 f: &F,
216 z: X,
217 x: X,
218) -> bool
219where
220 F: Fn(X, X) -> X,
221 X: Clone + PartialEq,
222{
223 is_left_absorbing(f, z.clone(), x.clone()) && is_right_absorbing(f, z, x)
224}
225
226pub trait Absorbing: BinaryOp {
229 fn z() -> Self::S;
230
231 fn assert(x: Self::S)
232 where
233 Self::S: Clone + PartialEq,
234 {
235 assert!(is_absorbing(&Self::op, Self::z(), x));
236 }
237}
238
239pub trait Add {
240 type S;
241
242 fn add(
243 _: Self::S,
244 _: Self::S,
245 ) -> Self::S;
246}
247
248pub trait Mul: Add {
249 fn mul(
250 _: Self::S,
251 _: Self::S,
252 ) -> Self::S;
253}
254
255fn iz_zero<F, X>(
256 mul: &F,
257 z: X,
258 x: X,
259) -> bool
260where
261 F: Fn(X, X) -> X,
262 X: Clone + PartialEq,
263{
264 is_absorbing(mul, z, x)
265}
266
267pub trait Zero: Mul {
268 fn zero() -> Self::S;
269
270 fn assert(x: Self::S)
271 where
272 Self::S: Clone + PartialEq,
273 {
274 assert!(iz_zero(&Self::mul, Self::zero(), x));
275 }
276}
277
278pub trait One: Mul {
279 fn one() -> Self::S;
280}
281
282pub trait AddInv: Add {
283 fn add_inv(_: Self::S) -> Self::S;
284}
285
286pub trait MulInv: Mul {
287 fn mul_inv(_: Self::S) -> Self::S;
288}
289
290fn is_left_distributive<Add, Mul, X>(
291 add: &Add,
292 mul: &Mul,
293 x: X,
294 y: X,
295 z: X,
296) -> bool
297where
298 Add: Fn(X, X) -> X,
299 Mul: Fn(X, X) -> X,
300 X: Clone + PartialEq,
301{
302 mul(x.clone(), add(y.clone(), z.clone()))
303 == add(mul(x.clone(), y), mul(x, z))
304}
305
306fn is_right_distributive<Add, Mul, X>(
307 add: &Add,
308 mul: &Mul,
309 y: X,
310 z: X,
311 x: X,
312) -> bool
313where
314 Add: Fn(X, X) -> X,
315 Mul: Fn(X, X) -> X,
316 X: Clone + PartialEq,
317{
318 mul(add(y.clone(), z.clone()), x.clone())
319 == add(mul(y, x.clone()), mul(z, x))
320}
321
322fn is_distributive<Add, Mul, X>(
323 add: &Add,
324 mul: &Mul,
325 x: X,
326 y: X,
327 z: X,
328) -> bool
329where
330 Add: Fn(X, X) -> X,
331 Mul: Fn(X, X) -> X,
332 X: Clone + PartialEq,
333{
334 is_left_distributive(add, mul, x.clone(), y.clone(), z.clone())
335 && is_right_distributive(add, mul, y, z, x)
336}
337
338pub trait Distributive: Mul {
339 fn assert(
340 x: Self::S,
341 y: Self::S,
342 z: Self::S,
343 ) where
344 Self::S: Clone + PartialEq,
345 {
346 assert!(is_distributive(&Self::mul, &Self::add, x, y, z));
347 }
348}
349
350pub mod dynamic {
351
352 pub trait BinaryOp {
353 type S;
354
355 fn op(
356 &self,
357 _: Self::S,
358 _: Self::S,
359 ) -> Self::S;
360 }
361}
362
363pub mod itself {
364
365 pub trait Id {}
366
367 impl<T> Id for T {}
368
369 pub trait BinaryOp<I: Id> {
370 fn op(
371 _: Self,
372 _: Self,
373 ) -> Self;
374 }
375
376 pub trait Commutative<I: Id> {}
377
378 pub trait Associative<I: Id> {}
379
380 pub trait Idempotence<I: Id> {}
381
382 pub trait Identity<I: Id> {
383 fn e() -> Self;
384 }
385
386 pub trait Inverse<I: Id> {
387 fn inv(_: Self) -> Self;
388 }
389}