From 9a8013f1cb530b868e5d1a86d48350a8bab19744 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick@luehne.de>
Date: Wed, 8 Apr 2020 12:09:27 +0200
Subject: [PATCH] Support empty n-aries

---
 src/ast.rs             |  6 ---
 src/format/formulas.rs | 96 +++++++++++++++++++++++++-----------------
 2 files changed, 57 insertions(+), 45 deletions(-)

diff --git a/src/ast.rs b/src/ast.rs
index 9f43335..27e7883 100644
--- a/src/ast.rs
+++ b/src/ast.rs
@@ -486,8 +486,6 @@ impl Formula
 {
 	pub fn and(arguments: Formulas) -> Self
 	{
-		assert!(!arguments.is_empty());
-
 		Self::And(arguments)
 	}
 
@@ -537,8 +535,6 @@ impl Formula
 
 	pub fn if_and_only_if(arguments: Formulas) -> Self
 	{
-		assert!(!arguments.is_empty());
-
 		Self::IfAndOnlyIf(arguments)
 	}
 
@@ -570,8 +566,6 @@ impl Formula
 
 	pub fn or(arguments: Formulas) -> Self
 	{
-		assert!(!arguments.is_empty());
-
 		Self::Or(arguments)
 	}
 
diff --git a/src/format/formulas.rs b/src/format/formulas.rs
index ce7b0f1..dcfe0cb 100644
--- a/src/format/formulas.rs
+++ b/src/format/formulas.rs
@@ -177,42 +177,52 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 				display_formula(argument, Some(self.formula), ChildPosition::Any))?,
 			crate::Formula::And(arguments) =>
 			{
-				let mut separator = "";
-
-				assert!(!arguments.is_empty());
-
-				let (parent_formula, position) = match arguments.len()
+				if arguments.is_empty()
 				{
-					0 | 1 => (self.parent_formula, self.position),
-					_ => (Some(self.formula), ChildPosition::Any),
-				};
-
-				for argument in arguments
+					write!(format, "true")?;
+				}
+				else
 				{
-					write!(format, "{}{:?}", separator,
-						display_formula(argument, parent_formula, position))?;
+					let (parent_formula, position) = match arguments.len()
+					{
+						1 => (self.parent_formula, self.position),
+						_ => (Some(self.formula), ChildPosition::Any),
+					};
 
-					separator = " and "
+					let mut separator = "";
+
+					for argument in arguments
+					{
+						write!(format, "{}{:?}", separator,
+							display_formula(argument, parent_formula, position))?;
+
+						separator = " and "
+					}
 				}
 			},
 			crate::Formula::Or(arguments) =>
 			{
-				let mut separator = "";
-
-				assert!(!arguments.is_empty());
-
-				let (parent_formula, position) = match arguments.len()
+				if arguments.is_empty()
 				{
-					0 | 1 => (self.parent_formula, self.position),
-					_ => (Some(self.formula), ChildPosition::Any),
-				};
-
-				for argument in arguments
+					write!(format, "false")?;
+				}
+				else
 				{
-					write!(format, "{}{:?}", separator,
-						display_formula(argument, parent_formula, position))?;
+					let (parent_formula, position) = match arguments.len()
+					{
+						1 => (self.parent_formula, self.position),
+						_ => (Some(self.formula), ChildPosition::Any),
+					};
 
-					separator = " or "
+					let mut separator = "";
+
+					for argument in arguments
+					{
+						write!(format, "{}{:?}", separator,
+							display_formula(argument, parent_formula, position))?;
+
+						separator = " or "
+					}
 				}
 			},
 			crate::Formula::Implies(crate::Implies{direction, antecedent, implication}) =>
@@ -248,22 +258,27 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 			},
 			crate::Formula::IfAndOnlyIf(arguments) =>
 			{
-				let mut separator = "";
-
-				assert!(!arguments.is_empty());
-
-				let (parent_formula, position) = match arguments.len()
+				if arguments.is_empty()
 				{
-					0 | 1 => (self.parent_formula, self.position),
-					_ => (Some(self.formula), ChildPosition::Any),
-				};
-
-				for argument in arguments
+					write!(format, "true")?;
+				}
+				else
 				{
-					write!(format, "{}{:?}", separator,
-						display_formula(argument, parent_formula, position))?;
+					let (parent_formula, position) = match arguments.len()
+					{
+						1 => (self.parent_formula, self.position),
+						_ => (Some(self.formula), ChildPosition::Any),
+					};
 
-					separator = " <-> "
+					let mut separator = "";
+
+					for argument in arguments
+					{
+						write!(format, "{}{:?}", separator,
+							display_formula(argument, parent_formula, position))?;
+
+						separator = " <-> "
+					}
 				}
 			},
 			crate::Formula::Compare(
@@ -666,6 +681,7 @@ mod tests
 	#[test]
 	fn format_and()
 	{
+		assert!(and(vec![]), "true");
 		assert!(and(vec![p()]), "p");
 		assert!(and(pqr()), "p and q and r");
 	}
@@ -673,6 +689,7 @@ mod tests
 	#[test]
 	fn format_or()
 	{
+		assert!(or(vec![]), "false");
 		assert!(or(vec![p()]), "p");
 		assert!(or(pqr()), "p or q or r");
 	}
@@ -687,6 +704,7 @@ mod tests
 	#[test]
 	fn format_if_and_only_if()
 	{
+		assert!(if_and_only_if(vec![]), "true");
 		assert!(if_and_only_if(vec![p()]), "p");
 		assert!(if_and_only_if(vec![p(), q()]), "p <-> q");
 		assert!(if_and_only_if(pqr()), "p <-> q <-> r");