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
//! A newtype wrapper whose [`Semigroup`](crate::classes::Semigroup) and [`Monoid`](crate::classes::Monoid) instances use
//! conjunction from [`HeytingAlgebra`](crate::classes::HeytingAlgebra).
//!
//! ### Examples
//!
//! ```
//! use fp_library::{
//! functions::*,
//! types::Conjunctive,
//! };
//!
//! assert_eq!(append(Conjunctive(true), Conjunctive(false)), Conjunctive(false));
//! assert_eq!(empty::<Conjunctive<bool>>(), Conjunctive(true));
//! ```
#[fp_macros::document_module]
mod inner {
use {
crate::classes::*,
fp_macros::*,
};
/// A newtype wrapper whose [`Semigroup`] instance uses
/// [`HeytingAlgebra::conjoin`].
///
/// This provides a [`Monoid`] based on logical conjunction (AND),
/// with [`HeytingAlgebra::true_value`] as the identity element.
#[document_examples]
///
/// ```
/// use fp_library::{
/// functions::*,
/// types::Conjunctive,
/// };
///
/// assert_eq!(append(Conjunctive(true), Conjunctive(true)), Conjunctive(true));
/// assert_eq!(append(Conjunctive(true), Conjunctive(false)), Conjunctive(false));
/// assert_eq!(empty::<Conjunctive<bool>>(), Conjunctive(true));
/// ```
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
#[derive(Clone, Copy, Debug, Default, Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct Conjunctive<A>(
/// The wrapped value.
pub A,
);
#[document_type_parameters("The Heyting algebra type.")]
impl<A: HeytingAlgebra> Semigroup for Conjunctive<A> {
/// Combines two values using [`HeytingAlgebra::conjoin`].
#[document_signature]
///
#[document_parameters("The first conjunctive value.", "The second conjunctive value.")]
///
#[document_returns("The conjunction wrapped in `Conjunctive`.")]
#[document_examples]
///
/// ```
/// use fp_library::{
/// functions::*,
/// types::Conjunctive,
/// };
///
/// assert_eq!(append(Conjunctive(true), Conjunctive(true)), Conjunctive(true));
/// ```
fn append(
a: Self,
b: Self,
) -> Self {
Conjunctive(A::conjoin(a.0, b.0))
}
}
#[document_type_parameters("The Heyting algebra type.")]
impl<A: HeytingAlgebra> Monoid for Conjunctive<A> {
/// Returns `Conjunctive(true_value())`.
#[document_signature]
///
#[document_returns("The top element wrapped in `Conjunctive`.")]
#[document_examples]
///
/// ```
/// use fp_library::{
/// functions::*,
/// types::Conjunctive,
/// };
///
/// assert_eq!(empty::<Conjunctive<bool>>(), Conjunctive(true));
/// ```
fn empty() -> Self {
Conjunctive(A::true_value())
}
}
}
pub use inner::*;
#[cfg(test)]
mod tests {
use {
super::*,
crate::functions::*,
quickcheck_macros::quickcheck,
};
#[quickcheck]
fn semigroup_associativity(
a: bool,
b: bool,
c: bool,
) -> bool {
let x = Conjunctive(a);
let y = Conjunctive(b);
let z = Conjunctive(c);
append(x, append(y, z)) == append(append(x, y), z)
}
#[quickcheck]
fn monoid_left_identity(a: bool) -> bool {
let x = Conjunctive(a);
append(empty::<Conjunctive<bool>>(), x) == x
}
#[quickcheck]
fn monoid_right_identity(a: bool) -> bool {
let x = Conjunctive(a);
append(x, empty::<Conjunctive<bool>>()) == x
}
}