From a1bbae920118ed690044cddd107d8d71afbb994d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Fri, 27 Mar 2020 02:46:33 +0100 Subject: [PATCH] Finish implementing formula parsing --- src/parse.rs | 2 +- src/parse/formulas.rs | 512 +++++++++++++++++++++++++++++------------- 2 files changed, 359 insertions(+), 155 deletions(-) diff --git a/src/parse.rs b/src/parse.rs index 1e79a84..9026b2e 100644 --- a/src/parse.rs +++ b/src/parse.rs @@ -6,7 +6,7 @@ mod terms; pub(crate) use helpers::word_boundary; pub use names::{function_or_predicate_name, variable_name}; pub use terms::term; -//pub use formulas::formula; +pub use formulas::formula; pub struct Declarations { diff --git a/src/parse/formulas.rs b/src/parse/formulas.rs index 650361e..eb8f9f2 100644 --- a/src/parse/formulas.rs +++ b/src/parse/formulas.rs @@ -2,14 +2,14 @@ use nom:: { IResult, branch::alt, - bytes::complete::{escaped_transform, tag}, - character::complete::{digit1, multispace0, none_of}, - combinator::{map, map_res, opt, recognize}, + bytes::complete::tag, + character::complete::multispace0, + combinator::{cut, map, map_res}, multi::{many1, separated_list}, - sequence::{delimited, pair, preceded, terminated}, + sequence::{delimited, pair, preceded, terminated, tuple}, }; -use super::{Declarations, function_or_predicate_name, word_boundary, variable_name}; +use super::{Declarations, word_boundary}; // TODO: avoid code duplication fn true_(i: &str) -> IResult<&str, crate::Formula> @@ -86,6 +86,292 @@ pub fn predicate<'i>(i: &'i str, d: &Declarations) -> IResult<&'i str, crate::Pr )(i) } +fn not<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula> +{ + preceded + ( + terminated + ( + tag("not"), + multispace0, + ), + |i| formula_precedence_2(i, d), + )(i) +} + +fn and<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, Vec>> +{ + map_res + ( + separated_list + ( + delimited + ( + multispace0, + terminated + ( + tag("and"), + word_boundary, + ), + multispace0, + ), + |i| formula_precedence_2(i, d), + ), + |arguments| -> Result<_, (_, _)> + { + if arguments.len() >= 2 + { + Ok(arguments.into_iter().map(Box::new).collect()) + } + else + { + Err(nom::error::make_error(i, nom::error::ErrorKind::Many1)) + } + } + )(i) +} + +fn or<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, Vec>> +{ + map_res + ( + separated_list + ( + delimited + ( + multispace0, + terminated + ( + tag("or"), + word_boundary, + ), + multispace0, + ), + |i| formula_precedence_3(i, d), + ), + |arguments| -> Result<_, (_, _)> + { + if arguments.len() >= 2 + { + Ok(arguments.into_iter().map(Box::new).collect()) + } + else + { + Err(nom::error::make_error(i, nom::error::ErrorKind::Many1)) + } + } + )(i) +} + +fn implication_left_to_right<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula> +{ + map + ( + pair + ( + many1 + ( + terminated + ( + |i| formula_precedence_4(i, d), + delimited + ( + multispace0, + tag("->"), + multispace0, + ), + ) + ), + |i| formula_precedence_4(i, d), + ), + |(arguments, last_argument)| arguments.into_iter().rev().fold(last_argument, + |accumulator, argument| + crate::Formula::implies(crate::ImplicationDirection::LeftToRight, + Box::new(accumulator), Box::new(argument))) + )(i) +} + +fn implication_right_to_left<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula> +{ + map + ( + pair + ( + |i| formula_precedence_4(i, d), + many1 + ( + preceded + ( + delimited + ( + multispace0, + tag("<-"), + multispace0, + ), + |i| formula_precedence_4(i, d), + ) + ), + ), + |(first_argument, arguments)| arguments.into_iter().fold(first_argument, + |accumulator, argument| + crate::Formula::implies(crate::ImplicationDirection::RightToLeft, + Box::new(accumulator), Box::new(argument))) + )(i) +} + +fn if_and_only_if<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, Vec>> +{ + map_res + ( + separated_list + ( + delimited + ( + multispace0, + tag("<->"), + multispace0, + ), + |i| formula_precedence_5(i, d), + ), + |arguments| -> Result<_, (_, _)> + { + if arguments.len() >= 2 + { + Ok(arguments.into_iter().map(Box::new).collect()) + } + else + { + Err(nom::error::make_error(i, nom::error::ErrorKind::Many1)) + } + } + )(i) +} + +fn quantified_expression<'a, 'b, T, N>(i: &'a str, d: &Declarations, keyword: &'b str, + new_functor: N) + -> IResult<&'a str, T> +where + N: Fn(std::rc::Rc, Box) -> T +{ + preceded + ( + terminated + ( + tag(keyword), + word_boundary, + ), + cut + ( + |i| -> IResult<&'a str, T> + { + let (i, variable_declarations) = + map + ( + delimited + ( + multispace0, + separated_list + ( + delimited + ( + multispace0, + tag(","), + multispace0, + ), + map + ( + crate::parse::terms::variable_declaration, + std::rc::Rc::new, + ), + ), + multispace0, + ), + std::rc::Rc::new, + )(i)?; + + if variable_declarations.is_empty() + { + return Err(nom::Err::Failure((i, nom::error::ErrorKind::Many1))); + } + + d.variable_declaration_stack.borrow_mut().push(std::rc::Rc::clone(&variable_declarations)); + + let (i, argument) = formula_parenthesized(i, d)?; + + // TODO: report logic errors more appropriately + d.variable_declaration_stack.borrow_mut().pop() + .map_err(|_| nom::Err::Failure((i, nom::error::ErrorKind::Verify)))?; + + Ok((i, new_functor(variable_declarations, Box::new(argument)))) + } + ), + )(i) +} + +fn compare<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Compare> +{ + map + ( + tuple + (( + |i| crate::parse::term(i, d), + delimited + ( + multispace0, + alt + (( + map + ( + tag(">"), + |_| crate::ComparisonOperator::Greater, + ), + map + ( + tag("<"), + |_| crate::ComparisonOperator::Less, + ), + map + ( + tag("<="), + |_| crate::ComparisonOperator::LessOrEqual, + ), + map + ( + tag(">="), + |_| crate::ComparisonOperator::GreaterOrEqual, + ), + map + ( + tag("!="), + |_| crate::ComparisonOperator::NotEqual, + ), + map + ( + tag("="), + |_| crate::ComparisonOperator::Equal, + ), + )), + multispace0, + ), + |i| crate::parse::term(i, d), + )), + |(left, operator, right)| + { + crate::Compare::new(operator, Box::new(left), Box::new(right)) + } + )(i) +} + +fn exists<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Exists> +{ + quantified_expression::(i, d, "exists", crate::Exists::new) +} + +fn for_all<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::ForAll> +{ + quantified_expression::(i, d, "forall", crate::ForAll::new) +} + fn formula_parenthesized<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula> { delimited @@ -114,48 +400,52 @@ fn formula_precedence_0<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, cr |i| predicate(i, d), crate::Formula::Predicate, ), - // TODO: comparisons - // TODO: quantified expressions - // TODO: negation + map + ( + |i| compare(i, d), + crate::Formula::Compare, + ), |i| formula_parenthesized(i, d), ))(i) } +fn formula_precedence_1<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula> +{ + alt + (( + map + ( + |i| exists(i, d), + crate::Formula::Exists, + ), + map + ( + |i| for_all(i, d), + crate::Formula::ForAll, + ), + |i| formula_precedence_0(i, d), + ))(i) +} + +fn formula_precedence_2<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula> +{ + alt + (( + |i| not(i, d), + |i| formula_precedence_1(i, d), + ))(i) +} + fn formula_precedence_3<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula> { alt (( - map_res + map ( - separated_list - ( - delimited - ( - multispace0, - terminated - ( - tag("and"), - word_boundary, - ), - multispace0, - ), - // TODO: fix - |i| formula_precedence_0(i, d), - ), - |arguments| -> Result<_, (_, _)> - { - if arguments.len() >= 2 - { - Ok(crate::Formula::and(arguments.into_iter().map(Box::new).collect())) - } - else - { - Err(nom::error::make_error(i, nom::error::ErrorKind::Many1)) - } - } + |i| and(i, d), + crate::Formula::And, ), - // TODO: fix - |i| formula_precedence_0(i, d), + |i| formula_precedence_2(i, d), ))(i) } @@ -163,110 +453,22 @@ fn formula_precedence_4<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, cr { alt (( - map_res + map ( - separated_list - ( - delimited - ( - multispace0, - terminated - ( - tag("or"), - word_boundary, - ), - multispace0, - ), - |i| formula_precedence_3(i, d), - ), - |arguments| -> Result<_, (_, _)> - { - if arguments.len() >= 2 - { - Ok(crate::Formula::or(arguments.into_iter().map(Box::new).collect())) - } - else - { - Err(nom::error::make_error(i, nom::error::ErrorKind::Many1)) - } - } + |i| or(i, d), + crate::Formula::Or, ), |i| formula_precedence_3(i, d), ))(i) } -fn implication_left_to_right<'a>(i: &'a str, d: &Declarations) - -> IResult<&'a str, crate::Formula> -{ - alt - (( - map - ( - pair - ( - many1 - ( - terminated - ( - |i| formula_precedence_4(i, d), - delimited - ( - multispace0, - tag("->"), - multispace0, - ), - ) - ), - |i| formula_precedence_4(i, d), - ), - |(arguments, last_argument)| arguments.into_iter().rev().fold(last_argument, - |accumulator, argument| - crate::Formula::implies(crate::ImplicationDirection::LeftToRight, - Box::new(accumulator), Box::new(argument))) - ), - |i| formula_precedence_4(i, d), - ))(i) -} - -fn implication_right_to_left<'a>(i: &'a str, d: &Declarations) - -> IResult<&'a str, crate::Formula> -{ - alt - (( - map - ( - pair - ( - |i| formula_precedence_4(i, d), - many1 - ( - preceded - ( - delimited - ( - multispace0, - tag("<-"), - multispace0, - ), - |i| formula_precedence_4(i, d), - ) - ), - ), - |(first_argument, arguments)| arguments.into_iter().fold(first_argument, - |accumulator, argument| - crate::Formula::implies(crate::ImplicationDirection::RightToLeft, - Box::new(accumulator), Box::new(argument))) - ), - |i| formula_precedence_4(i, d), - ))(i) -} - fn formula_precedence_5<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula> { alt (( - |i| implication_right_to_left(i, d), |i| implication_left_to_right(i, d), + |i| implication_right_to_left(i, d), + |i| formula_precedence_4(i, d), ))(i) } @@ -274,30 +476,10 @@ fn formula_precedence_6<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, cr { alt (( - map_res + map ( - separated_list - ( - delimited - ( - multispace0, - tag("<->"), - multispace0, - ), - |i| formula_precedence_5(i, d), - ), - |arguments| -> Result<_, (_, _)> - { - if arguments.len() >= 2 - { - Ok(crate::Formula::if_and_only_if( - arguments.into_iter().map(Box::new).collect())) - } - else - { - Err(nom::error::make_error(i, nom::error::ErrorKind::Many1)) - } - } + |i| if_and_only_if(i, d), + crate::Formula::IfAndOnlyIf, ), |i| formula_precedence_5(i, d), ))(i) @@ -312,7 +494,7 @@ pub fn formula<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Form mod tests { use crate::parse::formulas::*; - use crate::{Formula, Term, VariableDeclaration, VariableDeclarationStack}; + use crate::{Formula, Term}; /*fn formula(i: &str) -> Formula { @@ -389,4 +571,26 @@ mod tests .map(|(i, x)| (i, x.declaration.arity)), Ok((", rest", 3))); } + + #[test] + fn parse_exists() + { + assert_eq!(exists("exists X (p(X, Y, X, Y)), rest", &Declarations::new()) + .map(|(i, x)| (i, x.parameters.len())), + Ok((", rest", 1))); + assert!(exists("exists (p(X, Y, X, Y)), rest", &Declarations::new()).is_err()); + assert!(exists("exists X, rest", &Declarations::new()).is_err()); + assert!(exists("exists X (), rest", &Declarations::new()).is_err()); + assert!(exists("exists X (, true), rest", &Declarations::new()).is_err()); + assert!(exists("exists X (true, ), rest", &Declarations::new()).is_err()); + assert!(exists("exists X (true false), rest", &Declarations::new()).is_err()); + assert!(exists("exists X (true), rest", &Declarations::new()).is_ok()); + assert!(exists("exists X p(X), rest", &Declarations::new()).is_err()); + } + + #[test] + fn parse_formula() + { + assert!(formula("exists X, Y (p(X, Y, X, Y) and X < Y and q(X) <-> r(X)), rest", &Declarations::new()).is_ok()); + } }