From 21d4b1d60576a1cc9b733cf18a4cc018af49304b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick@luehne.de>
Date: Tue, 7 Apr 2020 17:50:00 +0200
Subject: [PATCH] Test biconditionals

---
 src/format/formulas.rs | 63 +++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 62 insertions(+), 1 deletion(-)

diff --git a/src/format/formulas.rs b/src/format/formulas.rs
index 24f1615..8f24906 100644
--- a/src/format/formulas.rs
+++ b/src/format/formulas.rs
@@ -1756,6 +1756,67 @@ mod tests
 				if_and_only_if(vec![implies_left(p2(), q2())]))),
 			"q2 <- p2 <- (q1 <- p1)");
 
-		// TODO: Implies + if and only if
+		// Implies + if and only if
+		assert_eq!(format(
+			implies_right(if_and_only_if(p1q1r1()), if_and_only_if(p2q2r2()))),
+			"(p1 <-> q1 <-> r1) -> (p2 <-> q2 <-> r2)");
+		assert_eq!(format(
+			implies_right(and(vec![if_and_only_if(p1q1r1())]),
+				and(vec![if_and_only_if(p2q2r2())]))),
+			"(p1 <-> q1 <-> r1) -> (p2 <-> q2 <-> r2)");
+		assert_eq!(format(
+			implies_right(or(vec![if_and_only_if(p1q1r1())]), or(vec![if_and_only_if(p2q2r2())]))),
+			"(p1 <-> q1 <-> r1) -> (p2 <-> q2 <-> r2)");
+		assert_eq!(format(
+			implies_right(if_and_only_if(vec![if_and_only_if(p1q1r1())]),
+				if_and_only_if(vec![if_and_only_if(p2q2r2())]))),
+			"(p1 <-> q1 <-> r1) -> (p2 <-> q2 <-> r2)");
+		assert_eq!(format(
+			implies_left(if_and_only_if(p1q1r1()), if_and_only_if(p2q2r2()))),
+			"(p2 <-> q2 <-> r2) <- (p1 <-> q1 <-> r1)");
+		assert_eq!(format(
+			implies_left(and(vec![if_and_only_if(p1q1r1())]), and(vec![if_and_only_if(p2q2r2())]))),
+			"(p2 <-> q2 <-> r2) <- (p1 <-> q1 <-> r1)");
+		assert_eq!(format(
+			implies_left(or(vec![if_and_only_if(p1q1r1())]), or(vec![if_and_only_if(p2q2r2())]))),
+			"(p2 <-> q2 <-> r2) <- (p1 <-> q1 <-> r1)");
+		assert_eq!(format(
+			implies_left(if_and_only_if(vec![if_and_only_if(p1q1r1())]),
+				if_and_only_if(vec![if_and_only_if(p2q2r2())]))),
+			"(p2 <-> q2 <-> r2) <- (p1 <-> q1 <-> r1)");
+		assert_eq!(format(
+			if_and_only_if(vec![implies_right(p1(), q1()), implies_right(p2(), q2()),
+				implies_right(p3(), q3())])),
+			"p1 -> q1 <-> p2 -> q2 <-> p3 -> q3");
+		assert_eq!(format(
+			if_and_only_if(vec![and(vec![implies_right(p1(), q1())]),
+				and(vec![implies_right(p2(), q2())]), and(vec![implies_right(p3(), q3())])])),
+			"p1 -> q1 <-> p2 -> q2 <-> p3 -> q3");
+		assert_eq!(format(
+			if_and_only_if(vec![or(vec![implies_right(p1(), q1())]),
+				or(vec![implies_right(p2(), q2())]), or(vec![implies_right(p3(), q3())])])),
+			"p1 -> q1 <-> p2 -> q2 <-> p3 -> q3");
+		assert_eq!(format(
+			if_and_only_if(vec![if_and_only_if(vec![implies_right(p1(), q1())]),
+				if_and_only_if(vec![implies_right(p2(), q2())]),
+				if_and_only_if(vec![implies_right(p3(), q3())])])),
+			"p1 -> q1 <-> p2 -> q2 <-> p3 -> q3");
+		assert_eq!(format(
+			if_and_only_if(vec![implies_left(p1(), q1()), implies_left(p2(), q2()),
+				implies_left(p3(), q3())])),
+			"q1 <- p1 <-> q2 <- p2 <-> q3 <- p3");
+		assert_eq!(format(
+			if_and_only_if(vec![and(vec![implies_left(p1(), q1())]),
+				and(vec![implies_left(p2(), q2())]), and(vec![implies_left(p3(), q3())])])),
+			"q1 <- p1 <-> q2 <- p2 <-> q3 <- p3");
+		assert_eq!(format(
+			if_and_only_if(vec![or(vec![implies_left(p1(), q1())]), or(vec![implies_left(p2(), q2())]),
+				or(vec![implies_left(p3(), q3())])])),
+			"q1 <- p1 <-> q2 <- p2 <-> q3 <- p3");
+		assert_eq!(format(
+			if_and_only_if(vec![if_and_only_if(vec![implies_left(p1(), q1())]),
+				if_and_only_if(vec![implies_left(p2(), q2())]),
+				if_and_only_if(vec![implies_left(p3(), q3())])])),
+			"q1 <- p1 <-> q2 <- p2 <-> q3 <- p3");
 	}
 }