diff --git a/src/lib.rs b/src/lib.rs index 7dc9315..f960aa7 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -123,7 +123,7 @@ impl std::fmt::Display for VariableDeclaration } } -fn term_precedence(term: &Term) -> u64 +pub fn term_precedence(term: &Term) -> u64 { match term { @@ -134,17 +134,17 @@ fn term_precedence(term: &Term) -> u64 } } -fn formula_precedence(formula: &Formula) -> u64 +pub fn formula_precedence(formula: &Formula) -> u64 { match formula { Formula::Predicate(_) | Formula::Boolean(_) | Formula::Less(_, _) | Formula::LessOrEqual(_, _) | Formula::Greater(_, _) | Formula::GreaterOrEqual(_, _) | Formula::Equal(_, _) | Formula::NotEqual(_, _) => 0, - Formula::Not(_) => 1, - Formula::And(_) => 2, - Formula::Or(_) => 3, - Formula::Implies(_, _) => 4, - Formula::Biconditional(_, _) => 5, - Formula::Exists(_) | Formula::ForAll(_) => 6, + Formula::Exists(_) | Formula::ForAll(_) => 1, + Formula::Not(_) => 2, + Formula::And(_) => 3, + Formula::Or(_) => 4, + Formula::Implies(_, _) => 5, + Formula::Biconditional(_, _) => 6, } } @@ -440,7 +440,7 @@ fn is_lowercase_alphanumeric(c: char) -> bool fn symbolic_identifier(i: &str) -> IResult<&str, String> { - map + let (i, symbolic_identifier) = map ( pair ( @@ -448,7 +448,9 @@ fn symbolic_identifier(i: &str) -> IResult<&str, String> take_while(char::is_alphanumeric) ), |(s0, s1)| format!("{}{}", s0, s1) - )(i) + )(i)?; + + Ok((i, symbolic_identifier)) } fn symbolic(i: &str) -> IResult<&str, Term> @@ -489,7 +491,7 @@ fn program_variable_identifier(i: &str) -> IResult<&str, String> preceded ( tag("X"), - take_while1(char::is_alphanumeric) + take_while(char::is_alphanumeric) ), multispace0 ), @@ -507,7 +509,7 @@ fn integer_variable_identifier(i: &str) -> IResult<&str, String> preceded ( tag("N"), - take_while1(char::is_alphanumeric) + take_while(char::is_alphanumeric) ), multispace0 ), @@ -597,9 +599,14 @@ fn predicate_n_ary(i: &str) -> IResult<&str, Formula> delimited(multispace0, symbolic_identifier, multispace0), delimited ( - tag("("), - separated_list(tag(","), term), - tag(")") + multispace0, + delimited + ( + tag("("), + separated_list(tag(","), term), + tag(")") + ), + multispace0 ) ), |(name, arguments)| Formula::Predicate( @@ -643,10 +650,96 @@ fn boolean(i: &str) -> IResult<&str, Formula> )(i) } +fn less(i: &str) -> IResult<&str, Formula> +{ + map + ( + pair + ( + term, + preceded(tag("<"), term) + ), + |(left, right)| Formula::Less(left, right) + )(i) +} +fn less_or_equal(i: &str) -> IResult<&str, Formula> +{ + map + ( + pair + ( + term, + preceded(tag("<="), term) + ), + |(left, right)| Formula::LessOrEqual(left, right) + )(i) +} +fn greater(i: &str) -> IResult<&str, Formula> +{ + map + ( + pair + ( + term, + preceded(tag(">"), term) + ), + |(left, right)| Formula::Greater(left, right) + )(i) +} +fn greater_or_equal(i: &str) -> IResult<&str, Formula> +{ + map + ( + pair + ( + term, + preceded(tag(">="), term) + ), + |(left, right)| Formula::GreaterOrEqual(left, right) + )(i) +} +fn equal(i: &str) -> IResult<&str, Formula> +{ + map + ( + pair + ( + term, + preceded(tag("="), term) + ), + |(left, right)| Formula::Equal(left, right) + )(i) +} + +fn not_equal(i: &str) -> IResult<&str, Formula> +{ + map + ( + pair + ( + term, + preceded(tag("!="), term) + ), + |(left, right)| Formula::NotEqual(left, right) + )(i) +} + +fn comparison(i: &str) -> IResult<&str, Formula> +{ + alt + (( + less, + less_or_equal, + greater, + greater_or_equal, + equal, + not_equal + ))(i) +} fn term_parenthesized(i: &str) -> IResult<&str, Term> { @@ -751,11 +844,197 @@ fn term_precedence_3(i: &str) -> IResult<&str, Term> Ok((i, fold_terms(initial, remainder))) } -fn term(i: &str) -> IResult<&str, Term> +pub fn term(i: &str) -> IResult<&str, Term> { term_precedence_3(i) } +fn formula_parenthesized(i: &str) -> IResult<&str, Formula> +{ + delimited + ( + multispace0, + delimited + ( + tag("("), + formula, + tag(")") + ), + multispace0 + )(i) +} + +fn formula_precedence_0(i: &str) -> IResult<&str, Formula> +{ + alt + (( + predicate, + boolean, + comparison, + formula_parenthesized + ))(i) +} + +fn exists(i: &str) -> IResult<&str, Formula> +{ + map + ( + delimited + ( + multispace0, + preceded + ( + tag("exists "), + pair + ( + separated_list + ( + tag(","), + variable_declaration + ), + formula_precedence_1 + ) + ), + multispace0 + ), + |(parameters, argument)| Formula::Exists( + Exists + { + parameters: parameters, + argument: Box::new(argument), + }) + )(i) +} + +fn for_all(i: &str) -> IResult<&str, Formula> +{ + map + ( + delimited + ( + multispace0, + preceded + ( + tag("forall "), + pair + ( + separated_list + ( + tag(","), + variable_declaration + ), + formula_precedence_1 + ) + ), + multispace0 + ), + |(parameters, argument)| Formula::ForAll( + ForAll + { + parameters: parameters, + argument: Box::new(argument), + }) + )(i) +} + +fn formula_precedence_1(i: &str) -> IResult<&str, Formula> +{ + alt + (( + exists, + for_all, + formula_precedence_0 + ))(i) +} + +fn formula_precedence_2(i: &str) -> IResult<&str, Formula> +{ + alt + (( + map + ( + delimited + ( + multispace0, + preceded(tag("not "), formula_precedence_1), + multispace0 + ), + |argument| Formula::Not(Box::new(argument)) + ), + formula_precedence_1 + ))(i) +} + +fn formula_precedence_3(i: &str) -> IResult<&str, Formula> +{ + alt + (( + map_res + ( + separated_list(tag("and"), map(formula_precedence_2, |argument| Box::new(argument))), + |arguments| + match arguments.len() + { + // TODO: improve error handling + 0 | 1 => Err(nom::Err::Error("")), + _ => Ok(Formula::And(arguments)), + } + ), + formula_precedence_2 + ))(i) +} + +fn formula_precedence_4(i: &str) -> IResult<&str, Formula> +{ + alt + (( + map_res + ( + separated_list(tag("or"), map(formula_precedence_3, |argument| Box::new(argument))), + |arguments| + match arguments.len() + { + // TODO: improve error handling + 0 | 1 => Err(nom::Err::Error("")), + _ => Ok(Formula::Or(arguments)), + } + ), + formula_precedence_3 + ))(i) +} + +fn formula_precedence_5(i: &str) -> IResult<&str, Formula> +{ + let (i, left) = formula_precedence_4(i)?; + + match preceded(tag("->"), formula_precedence_4)(i) + { + Ok((i, right)) => Ok((i, Formula::Implies(Box::new(left), Box::new(right)))), + Err(_) => Ok((i, left)), + } +} + +fn formula_precedence_6(i: &str) -> IResult<&str, Formula> +{ + let (i, left) = formula_precedence_5(i)?; + + match preceded(tag("<->"), formula_precedence_5)(i) + { + Ok((i, right)) => Ok((i, Formula::Biconditional(Box::new(left), Box::new(right)))), + Err(_) => Ok((i, left)), + } +} + +pub fn formula(i: &str) -> IResult<&str, Formula> +{ + formula_precedence_6(i) +} + +pub fn formulas(i: &str) -> IResult<&str, Vec> +{ + many0(formula)(i) +} + #[cfg(test)] mod tests { @@ -768,8 +1047,8 @@ mod tests #[test] fn parse_variable_declaration() { - assert_eq!(crate::variable_declaration("X5"), Ok(("", crate::VariableDeclaration{domain: crate::Domain::Program, name: "5".to_string()}))); - assert_eq!(crate::variable_declaration("NX3"), Ok(("", crate::VariableDeclaration{domain: crate::Domain::Integer, name: "X3".to_string()}))); + assert_eq!(crate::variable_declaration(" X5 "), Ok(("", crate::VariableDeclaration{domain: crate::Domain::Program, name: "5".to_string()}))); + assert_eq!(crate::variable_declaration(" NX3 "), Ok(("", crate::VariableDeclaration{domain: crate::Domain::Integer, name: "X3".to_string()}))); } #[test] @@ -870,9 +1149,9 @@ mod tests #[test] fn parse_predicate() { - assert_eq!(crate::predicate("p"), Ok(("", crate::Formula::Predicate(crate::Predicate{declaration: crate::PredicateDeclaration{name: "p".to_string(), arity: 0}, arguments: vec![]})))); + assert_eq!(crate::predicate(" p "), Ok(("", crate::Formula::Predicate(crate::Predicate{declaration: crate::PredicateDeclaration{name: "p".to_string(), arity: 0}, arguments: vec![]})))); - assert_eq!(crate::predicate_n_ary("p(5, 6, 7)"), Ok(("", + assert_eq!(crate::predicate_n_ary(" p(5, 6, 7) "), Ok(("", crate::Formula::Predicate ( crate::Predicate @@ -889,11 +1168,11 @@ mod tests crate::Term::Integer(5), crate::Term::Integer(6), crate::Term::Integer(7), - ] + ], } )))); - assert_eq!(crate::predicate("p(1, 3+4*5+6, \"test\")"), Ok(("", + assert_eq!(crate::predicate(" p(1, 3+4*5+6, \"test\") "), Ok(("", crate::Formula::Predicate ( crate::Predicate @@ -922,7 +1201,281 @@ mod tests Box::new(crate::Term::Integer(6)), ), crate::Term::String("test".to_string()), + ], + } + )))); + } + + #[test] + fn parse_comparison() + { + assert_eq!(crate::comparison("5 + 9 < #sup"), Ok(("", + crate::Formula::Less + ( + crate::Term::Add + ( + Box::new(crate::Term::Integer(5)), + Box::new(crate::Term::Integer(9)), + ), + crate::Term::Supremum, + )))); + + assert_eq!(crate::comparison("#inf != 6 * 9"), Ok(("", + crate::Formula::NotEqual + ( + crate::Term::Infimum, + crate::Term::Multiply + ( + Box::new(crate::Term::Integer(6)), + Box::new(crate::Term::Integer(9)), + ), + )))); + } + + #[test] + fn formula() + { + assert_eq!(crate::formula("p(1, a) or q(2)"), Ok(("", + crate::Formula::Or + ( + vec! + [ + Box::new(crate::Formula::Predicate + ( + crate::Predicate + { + declaration: + crate::PredicateDeclaration + { + name: "p".to_string(), + arity: 2, + }, + arguments: + vec! + [ + crate::Term::Integer(1), + crate::Term::Symbolic("a".to_string()), + ], + } + )), + Box::new(crate::Formula::Predicate + ( + crate::Predicate + { + declaration: + crate::PredicateDeclaration + { + name: "q".to_string(), + arity: 1, + }, + arguments: + vec! + [ + crate::Term::Integer(2), + ], + } + )), + ] + )))); + + assert_eq!(crate::formula("#inf < 5 and p(1, a) or q(2)"), Ok(("", + crate::Formula::Or + ( + vec! + [ + Box::new(crate::Formula::And + ( + vec! + [ + Box::new(crate::Formula::Less + ( + crate::Term::Infimum, + crate::Term::Integer(5), + )), + Box::new(crate::Formula::Predicate + ( + crate::Predicate + { + declaration: + crate::PredicateDeclaration + { + name: "p".to_string(), + arity: 2, + }, + arguments: + vec! + [ + crate::Term::Integer(1), + crate::Term::Symbolic("a".to_string()), + ], + } + )), ] + )), + Box::new(crate::Formula::Predicate + ( + crate::Predicate + { + declaration: + crate::PredicateDeclaration + { + name: "q".to_string(), + arity: 1, + }, + arguments: + vec! + [ + crate::Term::Integer(2), + ], + } + )), + ] + )))); + + assert_eq!(crate::formula("#inf < 5 and p(1, a) or q(2) -> #false"), Ok(("", + crate::Formula::Implies + ( + Box::new(crate::Formula::Or + ( + vec! + [ + Box::new(crate::Formula::And + ( + vec! + [ + Box::new(crate::Formula::Less + ( + crate::Term::Infimum, + crate::Term::Integer(5), + )), + Box::new(crate::Formula::Predicate + ( + crate::Predicate + { + declaration: + crate::PredicateDeclaration + { + name: "p".to_string(), + arity: 2, + }, + arguments: + vec! + [ + crate::Term::Integer(1), + crate::Term::Symbolic("a".to_string()), + ], + } + )), + ] + )), + Box::new(crate::Formula::Predicate + ( + crate::Predicate + { + declaration: + crate::PredicateDeclaration + { + name: "q".to_string(), + arity: 1, + }, + arguments: + vec! + [ + crate::Term::Integer(2), + ], + } + )), + ] + )), + Box::new(crate::Formula::Boolean(false)), + )))); + + assert_eq!(crate::formula(" not #true"), Ok(("", + crate::Formula::Not(Box::new(crate::Formula::Boolean(true)))))); + + assert_eq!(crate::formula("exists X forall N1 p(1, 2) and #false"), Ok(("", + crate::Formula::And + ( + vec! + [ + Box::new(crate::Formula::Exists + ( + crate::Exists + { + parameters: vec![crate::VariableDeclaration{name: "".to_string(), domain: crate::Domain::Program}], + argument: + Box::new(crate::Formula::ForAll + ( + crate::ForAll + { + parameters: vec![crate::VariableDeclaration{name: "1".to_string(), domain: crate::Domain::Integer}], + argument: + Box::new(crate::Formula::Predicate + ( + crate::Predicate + { + declaration: + crate::PredicateDeclaration + { + name: "p".to_string(), + arity: 2, + }, + arguments: + vec! + [ + crate::Term::Integer(1), + crate::Term::Integer(2), + ], + } + )), + } + )), + } + )), + Box::new(crate::Formula::Boolean(false)), + ] + )))); + + assert_eq!(crate::formula("exists X forall N1 (p(1, 2) and #false)"), Ok(("", + crate::Formula::Exists + ( + crate::Exists + { + parameters: vec![crate::VariableDeclaration{name: "".to_string(), domain: crate::Domain::Program}], + argument: + Box::new(crate::Formula::ForAll + ( + crate::ForAll + { + parameters: vec![crate::VariableDeclaration{name: "1".to_string(), domain: crate::Domain::Integer}], + argument: + Box::new(crate::Formula::And + ( + vec! + [ + Box::new(crate::Formula::Predicate + ( + crate::Predicate + { + declaration: + crate::PredicateDeclaration + { + name: "p".to_string(), + arity: 2, + }, + arguments: + vec! + [ + crate::Term::Integer(1), + crate::Term::Integer(2), + ], + } + )), + Box::new(crate::Formula::Boolean(false)), + ] + )), + } + )), } )))); }