From d1ab7963b14400e42cf1b94b828b3e41cf7d5d5e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick@luehne.de>
Date: Sun, 5 Apr 2020 18:12:06 +0200
Subject: [PATCH] Before larger refactoring

---
 src/format/formulas.rs | 97 ++++++++++++++++++++++++++++++++++++------
 1 file changed, 83 insertions(+), 14 deletions(-)

diff --git a/src/format/formulas.rs b/src/format/formulas.rs
index 9539f36..098d777 100644
--- a/src/format/formulas.rs
+++ b/src/format/formulas.rs
@@ -10,19 +10,21 @@ impl super::Precedence for crate::Formula
 			| Self::Boolean(_)
 			| Self::Compare(_)
 				=> 0,
-			Self::Exists(_)
+			/*Self::And(formulas)
+			| Self::Or(formulas) if formulas.len() == 1
+				=> 0,*/
+			Self::Not(_)
+			| Self::Exists(_)
 			| Self::ForAll(_)
 				=> 1,
-			Self::Not(_)
-				=> 2,
 			Self::And(_)
-				=> 3,
+				=> 2,
 			Self::Or(_)
-				=> 4,
+				=> 3,
 			Self::Implies(_)
-				=> 5,
+				=> 4,
 			Self::IfAndOnlyIf(_)
-				=> 6,
+				=> 5,
 		}
 	}
 }
@@ -609,6 +611,13 @@ mod tests
 		let term_3 = || exponentiate(constant("a"), exponentiate(constant("b"), constant("c")));
 		let term_4 = || negative(function("f", vec![integer(5), add(variable("X"), integer(3))]));
 
+		assert_eq!(format(not(greater(term_1(), term_2()))), "not (a + b) * c > |d - e|");
+		assert_eq!(format(not(less(term_1(), term_2()))), "not (a + b) * c < |d - e|");
+		assert_eq!(format(not(less_or_equal(term_1(), term_2()))), "not (a + b) * c <= |d - e|");
+		assert_eq!(format(not(greater_or_equal(term_1(), term_2()))), "not (a + b) * c >= |d - e|");
+		assert_eq!(format(not(equal(term_1(), term_2()))), "not (a + b) * c = |d - e|");
+		assert_eq!(format(not(not_equal(term_1(), term_2()))), "not (a + b) * c != |d - e|");
+
 		assert_eq!(format(
 			exists(vec![variable_declaration("X")], greater(term_1(), term_2()))),
 			"exists X (a + b) * c > |d - e|");
@@ -646,13 +655,6 @@ mod tests
 			for_all(vec![variable_declaration("X")], not_equal(term_1(), term_2()))),
 			"forall X (a + b) * c != |d - e|");
 
-		assert_eq!(format(not(greater(term_1(), term_2()))), "not (a + b) * c > |d - e|");
-		assert_eq!(format(not(less(term_1(), term_2()))), "not (a + b) * c < |d - e|");
-		assert_eq!(format(not(less_or_equal(term_1(), term_2()))), "not (a + b) * c <= |d - e|");
-		assert_eq!(format(not(greater_or_equal(term_1(), term_2()))), "not (a + b) * c >= |d - e|");
-		assert_eq!(format(not(equal(term_1(), term_2()))), "not (a + b) * c = |d - e|");
-		assert_eq!(format(not(not_equal(term_1(), term_2()))), "not (a + b) * c != |d - e|");
-
 		assert_eq!(format(
 			and(vec![greater(term_1(), term_2()), greater(term_3(), term_4()),
 				greater(term_2(), term_4())])),
@@ -777,4 +779,71 @@ mod tests
 				not_equal(term_2(), term_4())])),
 			"(a + b) * c != |d - e| <-> a ** b ** c != -f(5, X + 3) <-> |d - e| != -f(5, X + 3)");
 	}
+
+	#[test]
+	fn format_combination_not_and_lower()
+	{
+		assert_eq!(format(not(not(predicate("p", vec![])))), "not not p");
+
+		assert_eq!(format(
+			not(exists(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")], predicate("p", vec![])))),
+			"not exists X, Y, Z p");
+		assert_eq!(format(
+			exists(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")], not(predicate("p", vec![])))),
+			"exists X, Y, Z not p");
+		assert_eq!(format(
+			not(for_all(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")], predicate("p", vec![])))),
+			"not forall X, Y, Z p");
+		assert_eq!(format(
+			for_all(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")], not(predicate("p", vec![])))),
+			"forall X, Y, Z not p");
+
+		assert_eq!(format(
+			not(and(vec![predicate("p", vec![])]))),
+			"not p");
+		assert_eq!(format(
+			not(and(vec![predicate("p", vec![]), predicate("q", vec![]), predicate("r", vec![])]))),
+			"not (p and q and r)");
+
+		assert_eq!(format(
+			or(vec![predicate("p", vec![]), or(vec![or(vec![predicate("q", vec![]), predicate("r", vec![])])])])),
+			"p or q or r");
+
+		assert_eq!(format(
+			and(vec![predicate("p", vec![]), or(vec![or(vec![predicate("q", vec![]), predicate("r", vec![])])])])),
+			"p and (q or r)");
+	}
+
+	#[test]
+	fn format_combination_quantifiers_and_lower()
+	{
+		assert_eq!(format(
+			exists(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")], exists(vec![variable_declaration("A"),
+					variable_declaration("B"), variable_declaration("C")],
+					predicate("p", vec![])))),
+			"exists X, Y, Z exists A, B, C p");
+		assert_eq!(format(
+			exists(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")], for_all(vec![variable_declaration("A"),
+					variable_declaration("B"), variable_declaration("C")],
+					predicate("p", vec![])))),
+			"exists X, Y, Z forall A, B, C p");
+		assert_eq!(format(
+			for_all(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")], exists(vec![variable_declaration("A"),
+					variable_declaration("B"), variable_declaration("C")],
+					predicate("p", vec![])))),
+			"forall X, Y, Z exists A, B, C p");
+		assert_eq!(format(
+			for_all(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")], for_all(vec![variable_declaration("A"),
+					variable_declaration("B"), variable_declaration("C")],
+					predicate("p", vec![])))),
+			"forall X, Y, Z forall A, B, C p");
+	}
 }