From 17d8dbd8ba01cbf5dce75128ab8a6f6f6b67bd05 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Fri, 27 Mar 2020 04:53:31 +0100 Subject: [PATCH] Test conjunction parser --- src/parse/formulas.rs | 40 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) diff --git a/src/parse/formulas.rs b/src/parse/formulas.rs index 9367469..1a01c55 100644 --- a/src/parse/formulas.rs +++ b/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() {