1pub use ops::*;
2
3use std::rc::Rc;
4use std::mem;
5use std::fmt;
6use std::ops::{BitAnd, BitOr, BitXor, Not};
7
8#[derive(Debug, Eq, PartialEq, Hash)]
9pub enum Expr<T> {
10 Truth(bool),
11 Proposition(Rc<T>),
12 Not(Box<Expr<T>>),
13 And(Box<Expr<T>>, Box<Expr<T>>),
14 Or(Box<Expr<T>>, Box<Expr<T>>),
15 Xor(Box<Expr<T>>, Box<Expr<T>>),
16 Implies(Box<Expr<T>>, Box<Expr<T>>),
17 Equivalent(Box<Expr<T>>, Box<Expr<T>>),
18}
19
20impl<T> Expr<T> {
21 pub fn truth(t: bool) -> Self {
22 Expr::Truth(t)
23 }
24
25 pub fn proposition(p: T) -> Self {
26 Expr::Proposition(Rc::new(p))
27 }
28
29 pub fn has_same_operation(&self, e: &Expr<T>) -> bool {
30 mem::discriminant(self) == mem::discriminant(e)
31 }
32
33 fn priority(&self) -> u8 {
34 match *self {
35 Expr::Truth(..) | Expr::Proposition(..) => 0,
36 Expr::Not(..) => 1,
37 Expr::And(..) => 2,
38 Expr::Or(..) => 3,
39 Expr::Xor(..) => 4,
40 Expr::Implies(..) => 5,
41 Expr::Equivalent(..) => 6,
42 }
43 }
44
45 fn vague_priority(&self) -> u8 {
46 match *self {
47 Expr::Truth(..) | Expr::Proposition(..) => 0,
48 Expr::Not(..) => 1,
49 Expr::And(..) | Expr::Or(..) | Expr::Xor(..) => 2,
50 Expr::Implies(..) | Expr::Equivalent(..) => 3,
51 }
52 }
53
54 fn has_obvious_priority_over(&self, e: &Expr<T>) -> bool {
55 self.vague_priority() < e.vague_priority()
56 }
57}
58
59impl<T> Clone for Expr<T> {
61 fn clone(&self) -> Self {
62 match *self {
63 Expr::Truth(t) => Expr::Truth(t),
64 Expr::Proposition(ref p) => Expr::Proposition(p.clone()),
65 Expr::Not(ref e) => Expr::Not(e.clone()),
66 Expr::And(ref e1, ref e2) => Expr::And(e1.clone(), e2.clone()),
67 Expr::Or(ref e1, ref e2) => Expr::Or(e1.clone(), e2.clone()),
68 Expr::Xor(ref e1, ref e2) => Expr::Xor(e1.clone(), e2.clone()),
69 Expr::Implies(ref e1, ref e2) => Expr::Implies(e1.clone(), e2.clone()),
70 Expr::Equivalent(ref e1, ref e2) => Expr::Equivalent(e1.clone(), e2.clone()),
71 }
72 }
73}
74
75impl<T> fmt::Display for Expr<T>
76where
77 T: fmt::Display,
78{
79 fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
80 match *self {
81 Expr::Truth(t) => write!(f, "{}", if t { 'T' } else { 'F' }),
82 Expr::Proposition(ref p) => write!(f, "{}", p),
83 Expr::Not(ref e) => {
84 if e.has_obvious_priority_over(self) || e.priority() == self.priority() {
85 write!(f, "¬{}", e)
86 } else {
87 write!(f, "¬({})", e)
88 }
89 }
90 Expr::And(ref e1, ref e2) => {
91 if e1.has_obvious_priority_over(self) || e1.has_same_operation(self) {
92 write!(f, "{}∧", e1)
93 } else {
94 write!(f, "({})∧", e1)
95 }?;
96 if e2.has_obvious_priority_over(self) || e2.has_same_operation(self) {
97 write!(f, "{}", e2)
98 } else {
99 write!(f, "({})", e2)
100 }
101 }
102 Expr::Or(ref e1, ref e2) => {
103 if e1.has_obvious_priority_over(self) || e1.has_same_operation(self) {
104 write!(f, "{}∨", e1)
105 } else {
106 write!(f, "({})∨", e1)
107 }?;
108 if e2.has_obvious_priority_over(self) || e2.has_same_operation(self) {
109 write!(f, "{}", e2)
110 } else {
111 write!(f, "({})", e2)
112 }
113 }
114 Expr::Xor(ref e1, ref e2) => {
115 if e1.has_obvious_priority_over(self) || e1.has_same_operation(self) {
116 write!(f, "{}⊕", e1)
117 } else {
118 write!(f, "({})⊕", e1)
119 }?;
120 if e2.has_obvious_priority_over(self) || e2.has_same_operation(self) {
121 write!(f, "{}", e2)
122 } else {
123 write!(f, "({})", e2)
124 }
125 }
126 Expr::Implies(ref e1, ref e2) => {
127 if e1.has_obvious_priority_over(self) {
128 write!(f, "{}⇒", e1)
129 } else {
130 write!(f, "({})⇒", e1)
131 }?;
132 if e2.has_obvious_priority_over(self) || e2.has_same_operation(self) {
133 write!(f, "{}", e2)
134 } else {
135 write!(f, "({})", e2)
136 }
137 }
138 Expr::Equivalent(ref e1, ref e2) => {
139 if e1.has_obvious_priority_over(self) {
140 write!(f, "{}⇔", e1)
141 } else {
142 write!(f, "({})⇔", e1)
143 }?;
144 if e2.has_obvious_priority_over(self) || e2.has_same_operation(self) {
145 write!(f, "{}", e2)
146 } else {
147 write!(f, "({})", e2)
148 }
149 }
150 }
151 }
152}
153
154impl<T> Not for Expr<T> {
155 type Output = Expr<T>;
156 fn not(self) -> Self::Output {
157 Expr::Not(Box::new(self))
158 }
159}
160
161impl<RHS, T> BitAnd<RHS> for Expr<T>
162where
163 RHS: Into<Expr<T>>,
164{
165 type Output = Expr<T>;
166 fn bitand(self, e: RHS) -> Self::Output {
167 self.and(e.into())
168 }
169}
170
171impl<RHS, T> BitOr<RHS> for Expr<T>
172where
173 RHS: Into<Expr<T>>,
174{
175 type Output = Expr<T>;
176 fn bitor(self, e: RHS) -> Self::Output {
177 self.or(e.into())
178 }
179}
180
181impl<RHS, T> BitXor<RHS> for Expr<T>
182where
183 RHS: Into<Expr<T>>,
184{
185 type Output = Expr<T>;
186 fn bitxor(self, e: RHS) -> Self::Output {
187 self.xor(e.into())
188 }
189}
190
191#[cfg(test)]
192mod tests {
193 use super::*;
194
195 #[test]
196 fn operation() {
197 let (p, q) = (Expr::proposition('p'), Expr::proposition('q'));
198 assert_eq!(p.clone().not(), !p.clone());
199 assert_eq!(p.clone().and(q.clone()), p.clone() & q.clone());
200 assert_eq!(p.clone().or(q.clone()), p.clone() | q.clone());
201 assert_eq!(p.clone().xor(q.clone()), p.clone() ^ q.clone());
202 }
203
204 #[test]
205 fn clone() {
206 #[derive(Debug, Eq, PartialEq)]
207 struct A(i32);
208 let e1 = Expr::proposition(A(1));
209 let e2 = e1.clone();
210 assert_eq!(e1, e2);
211 }
212
213 macro_rules! format_eq {
214 ($e: expr, $s: expr) => {
215 assert_eq!(format!("{}", $e), $s);
216 };
217 }
218
219 #[test]
220 fn expression_display() {
221 let p = Expr::proposition('p');
222 let q = Expr::proposition('q');
223
224 format_eq!(Expr::Truth::<i32>(true), "T");
225 format_eq!(Expr::Truth::<i32>(false), "F");
226 format_eq!(p.clone().not(), "¬p");
227 format_eq!(p.clone().and(q.clone()), "p∧q");
228 format_eq!(p.clone().or(q.clone()), "p∨q");
229 format_eq!(p.clone().xor(q.clone()), "p⊕q");
230 format_eq!(p.clone().implies(q.clone()), "p⇒q");
231 format_eq!(p.clone().equivalent(q.clone()), "p⇔q");
232 }
233
234 #[test]
235 fn expression_priority_display() {
236 let p = Expr::proposition('p');
237 let q = Expr::proposition('q');
238 let r = Expr::proposition('r');
239
240 format_eq!(p.clone().not().not(), "¬¬p");
241
242 let p_and_q = p.clone().and(q.clone());
243 format_eq!(p_and_q.clone().not(), "¬(p∧q)");
244
245 format_eq!(p_and_q.clone().and(r.clone()), "p∧q∧r");
246 format_eq!(r.clone().and(p_and_q.clone()), "r∧p∧q");
247
248 let p_or_q = p.clone().or(q.clone());
249 format_eq!(p_or_q.clone().or(r.clone()), "p∨q∨r");
250 format_eq!(r.clone().or(p_or_q.clone()), "r∨p∨q");
251
252 format_eq!(p_and_q.clone().or(r.clone()), "(p∧q)∨r");
253 format_eq!(r.clone().or(p_and_q.clone()), "r∨(p∧q)");
254
255 let p_implies_q = p.clone().implies(q.clone());
256 format_eq!(p_implies_q.clone().not(), "¬(p⇒q)");
257 format_eq!(p_implies_q.clone().implies(r.clone()), "(p⇒q)⇒r");
258 format_eq!(r.clone().implies(p_implies_q.clone()), "r⇒p⇒q");
259
260 let p_equivalent_q = p.clone().equivalent(q.clone());
261 format_eq!(p_equivalent_q.clone().not(), "¬(p⇔q)");
262 format_eq!(p_equivalent_q.clone().equivalent(r.clone()), "(p⇔q)⇔r");
263 format_eq!(r.clone().equivalent(p_equivalent_q.clone()), "r⇔p⇔q");
264 }
265}