Test conjunction parser

src/parse/formulas.rs

@@ -491,6 +491,46 @@ mod tests
 		assert_eq!(formula("false"), Formula::false_());
 	}
 
+	#[test]
+	fn parse_and()
+	{
+		let formula_as_and = |i| match formula(i)
+		{
+			Formula::And(arguments) => arguments,
+			_ => panic!("expected conjunction"),
+		};
+
+		let as_predicate = |x| match x
+		{
+			Formula::Predicate(arguments) => arguments,
+			_ => panic!("expected predicate"),
+		};
+
+		assert_eq!(format_formula("true  and  false"), "true and false");
+		assert_eq!(formula_as_and("true and false").len(), 2);
+		assert_eq!(*formula_as_and("true and false").remove(0), Formula::true_());
+		assert_eq!(*formula_as_and("true and false").remove(1), Formula::false_());
+		// The order of elements is retained
+		assert_ne!(formula("true and false"), formula("false and true"));
+		assert_eq!(format_formula("p  and  q  and  r  and  s"), "p and q and r and s");
+		assert_eq!(
+			as_predicate(*formula_as_and("p and q and r and s").remove(0)).declaration.name, "p");
+		assert_eq!(
+			as_predicate(*formula_as_and("p and q and r and s").remove(3)).declaration.name, "s");
+
+		let formula = |i| original::formula(i, &Declarations::new());
+
+		// Malformed formulas shouldn’t be accepted
+		assert!(formula("and").is_err());
+		assert!(formula("and p").is_err());
+		assert_eq!(formula_remainder("p and"), " and");
+		assert_eq!(formula_remainder("p andq"), " andq");
+		assert_eq!(formula_remainder("p and q and"), " and");
+		assert_eq!(formula_remainder("p and q andq"), " andq");
+		assert!(formula("(p and) q").is_err());
+		assert_eq!(formula_remainder("p (and q)"), " (and q)");
+	}
+
 	#[test]
 	fn parse_predicate()
 	{