From 1c00e5be1691da1e88844eb5ab66fdfa09583d9a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Sat, 14 Mar 2020 02:11:33 +0100 Subject: [PATCH] Continue parsing formulas --- src/ast.rs | 46 +- src/format.rs | 28 +- src/parse.rs | 992 ------------------------------------------ src/parse/formulas.rs | 280 ++++++++---- src/parse/helpers.rs | 6 + src/parse/terms.rs | 41 +- 6 files changed, 256 insertions(+), 1137 deletions(-) diff --git a/src/ast.rs b/src/ast.rs index aab5c08..9f43335 100644 --- a/src/ast.rs +++ b/src/ast.rs @@ -29,6 +29,15 @@ pub enum UnaryOperator Negative, } +// ImplicationDirection + +#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)] +pub enum ImplicationDirection +{ + LeftToRight, + RightToLeft, +} + // Primitives #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)] @@ -291,38 +300,22 @@ impl ForAll } } -#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)] -pub struct IfAndOnlyIf -{ - pub left: Box, - pub right: Box, -} - -impl IfAndOnlyIf -{ - pub fn new(left: Box, right: Box) -> Self - { - Self - { - left, - right, - } - } -} - #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)] pub struct Implies { + pub direction: ImplicationDirection, pub antecedent: Box, pub implication: Box, } impl Implies { - pub fn new(antecedent: Box, implication: Box) -> Self + pub fn new(direction: ImplicationDirection, antecedent: Box, implication: Box) + -> Self { Self { + direction, antecedent, implication, } @@ -480,7 +473,7 @@ pub enum Formula Compare(Compare), Exists(Exists), ForAll(ForAll), - IfAndOnlyIf(IfAndOnlyIf), + IfAndOnlyIf(Formulas), Implies(Implies), Not(Box), Or(Formulas), @@ -542,14 +535,17 @@ impl Formula Self::compare(ComparisonOperator::GreaterOrEqual, left, right) } - pub fn if_and_only_if(left: Box, right: Box) -> Self + pub fn if_and_only_if(arguments: Formulas) -> Self { - Self::IfAndOnlyIf(IfAndOnlyIf::new(left, right)) + assert!(!arguments.is_empty()); + + Self::IfAndOnlyIf(arguments) } - pub fn implies(antecedent: Box, consequent: Box) -> Self + pub fn implies(direction: ImplicationDirection, antecedent: Box, + consequent: Box) -> Self { - Self::Implies(Implies::new(antecedent, consequent)) + Self::Implies(Implies::new(direction, antecedent, consequent)) } pub fn less(left: Box, right: Box) -> Self diff --git a/src/format.rs b/src/format.rs index 8c20b42..c6b8896 100644 --- a/src/format.rs +++ b/src/format.rs @@ -389,12 +389,28 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula> separator = " or " } }, - crate::Formula::Implies(crate::Implies{antecedent, implication}) - => write!(format, "{:?} -> {:?}", display_formula(antecedent, precedence), - display_formula(implication, precedence))?, - crate::Formula::IfAndOnlyIf(crate::IfAndOnlyIf{left, right}) - => write!(format, "{:?} <-> {:?}", display_formula(left, precedence), - display_formula(right, precedence))?, + crate::Formula::Implies(crate::Implies{direction, antecedent, implication}) => + { + let operator_symbol = match direction + { + crate::ImplicationDirection::LeftToRight => "->", + crate::ImplicationDirection::RightToLeft => "<-", + }; + + write!(format, "{:?} {} {:?}", display_formula(antecedent, precedence), + operator_symbol, display_formula(implication, precedence))?; + }, + crate::Formula::IfAndOnlyIf(arguments) => + { + let mut separator = ""; + + for argument in arguments + { + write!(format, "{}{:?}", separator, display_formula(argument, precedence))?; + + separator = " <-> "; + } + }, crate::Formula::Compare( crate::Compare{operator: crate::ComparisonOperator::Less, left, right}) => write!(format, "{:?} < {:?}", display_term(left, None), diff --git a/src/parse.rs b/src/parse.rs index c1b8333..1e79a84 100644 --- a/src/parse.rs +++ b/src/parse.rs @@ -28,995 +28,3 @@ impl Declarations } } } - -/* -use nom:: -{ - IResult, - bytes::complete::{take_while, take_while_m_n, is_not}, - character::complete::{digit1, multispace0}, - sequence::{preceded, delimited, pair}, - combinator::{map, map_res}, - multi::{many0, separated_list}, - branch::alt, - bytes::complete::tag, -}; - -struct Declarations -{ - //function_declarations:, - //predicate_declarations:, - //variable_declaration_stack: VariableDeclarationStack, -} - -enum TermOperator -{ - Add, - Subtract, - Multiply, -} - -fn variable_declaration<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::VariableDeclaration> -{ - map - ( - |i| variable_identifier(i, declarations), - |s| crate::VariableDeclaration{name: s}, - )(i) -}*/ - -/* -fn program_variable<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term> -{ - map - ( - |i| program_variable_identifier(i, declarations), - |s| - { - let declaration = declarations.variable_declaration_stack.get(s.as_ref()); - - crate::Term::Variable(crate::VariableDeclaration{name: s, domain: crate::Domain::Program}) - }, - )(i) -} - -fn integer_variable<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term> -{ - map - ( - |i| integer_variable_identifier, - |s| crate::Term::Variable(crate::VariableDeclaration{name: s, domain: crate::Domain::Integer}), - )(i) -} - -fn variable<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term> -{ - alt - (( - |i| program_variable(i, declarations), - |i| integer_variable(i, declarations), - ))(i) -} - -fn predicate_0_ary<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> -{ - map - ( - delimited(multispace0, symbolic_identifier, multispace0), - |name| crate::Formula::Predicate( - crate::Predicate - { - declaration: - crate::PredicateDeclaration - { - name: name, - arity: 0, - }, - arguments: vec![], - }) - )(i) -} - -fn predicate_n_ary<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> -{ - map - ( - pair - ( - delimited(multispace0, symbolic_identifier, multispace0), - delimited - ( - multispace0, - delimited - ( - tag("("), - separated_list(tag(","), term), - tag(")") - ), - multispace0 - ) - ), - |(name, arguments)| crate::Formula::Predicate( - crate::Predicate - { - declaration: - crate::PredicateDeclaration - { - name: name, - arity: arguments.len(), - }, - arguments: arguments, - }) - )(i) -} - -fn predicate<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> -{ - alt - (( - predicate_n_ary, - predicate_0_ary - ))(i) -} - -fn boolean<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> -{ - map - ( - delimited - ( - multispace0, - alt - (( - map(tag("#true"), |_| true), - map(tag("#false"), |_| false) - )), - multispace0 - ), - |value| crate::Formula::Boolean(value) - )(i) -} - -fn less<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> -{ - map - ( - pair - ( - term, - preceded(tag("<"), term) - ), - |(left, right)| crate::Formula::Less(left, right) - )(i) -} - -fn less_or_equal<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> -{ - map - ( - pair - ( - term, - preceded(tag("<="), term) - ), - |(left, right)| crate::Formula::LessOrEqual(left, right) - )(i) -} - -fn greater<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> -{ - map - ( - pair - ( - term, - preceded(tag(">"), term) - ), - |(left, right)| crate::Formula::Greater(left, right) - )(i) -} - -fn greater_or_equal<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> -{ - map - ( - pair - ( - term, - preceded(tag(">="), term) - ), - |(left, right)| crate::Formula::GreaterOrEqual(left, right) - )(i) -} - -fn equal<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> -{ - map - ( - pair - ( - term, - preceded(tag("="), term) - ), - |(left, right)| crate::Formula::Equal(left, right) - )(i) -} - -fn not_equal<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> -{ - map - ( - pair - ( - term, - preceded(tag("!="), term) - ), - |(left, right)| crate::Formula::NotEqual(left, right) - )(i) -} - -fn comparison<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> -{ - alt - (( - less, - less_or_equal, - greater, - greater_or_equal, - equal, - not_equal - ))(i) -} -*/ - -/*fn term_parenthesized<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term> -{ - delimited - ( - multispace0, - delimited - ( - tag("("), - term, - tag(")") - ), - multispace0 - )(i) -} - -fn fold_terms(initial: crate::Term, remainder: Vec<(TermOperator, crate::Term)>) -> crate::Term -{ - remainder.into_iter().fold(initial, - |accumulator, pair| - { - let (term_operator, term) = pair; - - match term_operator - { - TermOperator::Add => crate::Term::Add(Box::new(accumulator), Box::new(term)), - TermOperator::Subtract => crate::Term::Subtract(Box::new(accumulator), Box::new(term)), - TermOperator::Multiply => crate::Term::Multiply(Box::new(accumulator), Box::new(term)), - } - }) -} - -fn term_precedence_0<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term> -{ - alt - (( - infimum, - supremum, - integer, - symbolic, - string, - variable, - term_parenthesized - ))(i) -} - -fn term_precedence_1<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term> -{ - alt - (( - map - ( - delimited - ( - multispace0, - preceded(tag("-"), term_precedence_0), - multispace0 - ), - |term| crate::Term::Negative(Box::new(term)) - ), - term_precedence_0 - ))(i) -} - -fn term_precedence_2<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term> -{ - let (i, initial) = term_precedence_1(i)?; - let (i, remainder) = - many0 - ( - |i| - { - let (i, term) = preceded(tag("*"), term_precedence_1)(i)?; - Ok((i, (TermOperator::Multiply, term))) - } - )(i)?; - - Ok((i, fold_terms(initial, remainder))) -} - -fn term_precedence_3<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term> -{ - let (i, initial) = term_precedence_2(i)?; - let (i, remainder) = - many0 - ( - alt - (( - |i| - { - let (i, term) = preceded(tag("+"), term_precedence_2)(i)?; - Ok((i, (TermOperator::Add, term))) - }, - |i| - { - let (i, term) = preceded(tag("-"), term_precedence_2)(i)?; - Ok((i, (TermOperator::Subtract, term))) - } - )) - )(i)?; - - Ok((i, fold_terms(initial, remainder))) -} - -pub fn term<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term> -{ - term_precedence_3(i) -} -*/ - -/* -fn formula_parenthesized<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> -{ - delimited - ( - multispace0, - delimited - ( - tag("("), - formula, - tag(")") - ), - multispace0 - )(i) -} - -fn formula_precedence_0<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> -{ - alt - (( - comparison, - predicate, - boolean, - formula_parenthesized - ))(i) -} - -fn exists<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> -{ - map - ( - delimited - ( - multispace0, - preceded - ( - tag("exists "), - pair - ( - separated_list - ( - tag(","), - variable_declaration - ), - formula_precedence_1 - ) - ), - multispace0 - ), - |(parameters, argument)| crate::Formula::Exists( - crate::Exists - { - parameters: parameters, - argument: Box::new(argument), - }) - )(i) -} - -fn for_all<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> -{ - map - ( - delimited - ( - multispace0, - preceded - ( - tag("forall "), - pair - ( - separated_list - ( - tag(","), - variable_declaration - ), - formula_precedence_1 - ) - ), - multispace0 - ), - |(parameters, argument)| crate::Formula::ForAll( - crate::ForAll - { - parameters: parameters, - argument: Box::new(argument), - }) - )(i) -} - -fn formula_precedence_1<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> -{ - alt - (( - exists, - for_all, - formula_precedence_0 - ))(i) -} - -fn formula_precedence_2<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> -{ - alt - (( - map - ( - delimited - ( - multispace0, - preceded(tag("not "), formula_precedence_1), - multispace0 - ), - |argument| crate::Formula::Not(Box::new(argument)) - ), - formula_precedence_1 - ))(i) -} - -fn formula_precedence_3<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::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(crate::Formula::And(arguments)), - } - ), - formula_precedence_2 - ))(i) -} - -fn formula_precedence_4<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::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(crate::Formula::Or(arguments)), - } - ), - formula_precedence_3 - ))(i) -} - -fn formula_precedence_5<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> -{ - let (i, left) = formula_precedence_4(i)?; - - match preceded(tag("->"), formula_precedence_4)(i) - { - Ok((i, right)) => Ok((i, crate::Formula::Implies(Box::new(left), Box::new(right)))), - Err(_) => Ok((i, left)), - } -} - -fn formula_precedence_6<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> -{ - let (i, left) = formula_precedence_5(i)?; - - match preceded(tag("<->"), formula_precedence_5)(i) - { - Ok((i, right)) => Ok((i, crate::Formula::Biconditional(Box::new(left), Box::new(right)))), - Err(_) => Ok((i, left)), - } -} - -pub fn formula<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> -{ - formula_precedence_6(i) -} - -pub fn formulas<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, Vec> -{ - many0(formula)(i) -} -*/ - -/* -#[cfg(test)] -mod tests -{ - #[test] - fn parse_integer() - { - assert_eq!(crate::term("12345"), Ok(("", crate::Term::Integer(12345)))); - } - - #[test] - fn parse_variable_declaration() - { - assert_eq!(crate::term(" X5 "), Ok(("", crate::Term::Variable(crate::VariableDeclaration{domain: crate::Domain::Program, name: "5".to_string()})))); - assert_eq!(crate::term(" NX3 "), Ok(("", crate::Term::Variable(crate::VariableDeclaration{domain: crate::Domain::Integer, name: "X3".to_string()})))); - } - - #[test] - fn parse_variable() - { - assert_eq!(crate::term("X5"), Ok(("", crate::Term::Variable(crate::VariableDeclaration{domain: crate::Domain::Program, name: "5".to_string()})))); - assert_eq!(crate::term("NX3"), Ok(("", crate::Term::Variable(crate::VariableDeclaration{domain: crate::Domain::Integer, name: "X3".to_string()})))); - } - - #[test] - fn parse_string() - { - assert_eq!(crate::term(" \"foobar\" "), Ok(("", crate::Term::String("foobar".to_string())))); - } - - #[test] - fn parse_boolean() - { - assert_eq!(crate::formula(" #true "), Ok(("", crate::Formula::Boolean(true)))); - assert_eq!(crate::formula(" #false "), Ok(("", crate::Formula::Boolean(false)))); - } - - #[test] - fn parse_term() - { - assert_eq!(crate::term(" 5 + 3"), Ok(("", - crate::Term::Add - ( - Box::new(crate::Term::Integer(5)), - Box::new(crate::Term::Integer(3)), - )))); - - assert_eq!(crate::term(" -5"), Ok(("", - crate::Term::Negative - ( - Box::new(crate::Term::Integer(5)) - ) - ))); - - assert_eq!(crate::term(" 5+3 * -(9+ 1) + 2 "), Ok(("", - crate::Term::Add - ( - Box::new(crate::Term::Add - ( - Box::new(crate::Term::Integer(5)), - Box::new(crate::Term::Multiply - ( - Box::new(crate::Term::Integer(3)), - Box::new(crate::Term::Negative - ( - Box::new(crate::Term::Add - ( - Box::new(crate::Term::Integer(9)), - Box::new(crate::Term::Integer(1)), - )) - )), - )), - )), - Box::new(crate::Term::Integer(2)), - )))); - - assert_eq!(crate::term(" 5 + a "), Ok(("", - crate::Term::Add - ( - Box::new(crate::Term::Integer(5)), - Box::new(crate::Term::Symbolic("a".to_string())), - )))); - - assert_eq!(crate::term(" 5 + #sup "), Ok(("", - crate::Term::Add - ( - Box::new(crate::Term::Integer(5)), - Box::new(crate::Term::Supremum), - )))); - - assert_eq!(crate::term(" 5 + #inf "), Ok(("", - crate::Term::Add - ( - Box::new(crate::Term::Integer(5)), - Box::new(crate::Term::Infimum), - )))); - - assert_eq!(crate::term(" 5 + \" text \" "), Ok(("", - crate::Term::Add - ( - Box::new(crate::Term::Integer(5)), - Box::new(crate::Term::String(" text ".to_string())), - )))); - - assert_eq!(crate::term(" 5 + X1 "), Ok(("", - crate::Term::Add - ( - Box::new(crate::Term::Integer(5)), - Box::new(crate::Term::Variable(crate::VariableDeclaration{domain: crate::Domain::Program, name: "1".to_string()})), - )))); - } - - #[test] - fn parse_predicate() - { - assert_eq!(crate::formula(" p "), Ok(("", crate::Formula::Predicate(crate::Predicate{declaration: crate::PredicateDeclaration{name: "p".to_string(), arity: 0}, arguments: vec![]})))); - - assert_eq!(crate::formula(" p(5, 6, 7) "), Ok(("", - crate::Formula::Predicate - ( - crate::Predicate - { - declaration: - crate::PredicateDeclaration - { - name: "p".to_string(), - arity: 3, - }, - arguments: - vec! - [ - crate::Term::Integer(5), - crate::Term::Integer(6), - crate::Term::Integer(7), - ], - } - )))); - - assert_eq!(crate::formula(" p(1, 3+4*5+6, \"test\") "), Ok(("", - crate::Formula::Predicate - ( - crate::Predicate - { - declaration: - crate::PredicateDeclaration - { - name: "p".to_string(), - arity: 3, - }, - arguments: - vec! - [ - crate::Term::Integer(1), - crate::Term::Add - ( - Box::new(crate::Term::Add - ( - Box::new(crate::Term::Integer(3)), - Box::new(crate::Term::Multiply - ( - Box::new(crate::Term::Integer(4)), - Box::new(crate::Term::Integer(5)), - )), - )), - Box::new(crate::Term::Integer(6)), - ), - crate::Term::String("test".to_string()), - ], - } - )))); - } - - #[test] - fn parse_comparison() - { - assert_eq!(crate::formula("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::formula("#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)), - ), - )))); - - assert_eq!(crate::formula("n = 5"), Ok(("", - crate::Formula::Equal - ( - crate::Term::Symbolic("n".to_string()), - crate::Term::Integer(5), - )))); - } - - #[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)), - ] - )), - } - )), - } - )))); - } -} -*/ diff --git a/src/parse/formulas.rs b/src/parse/formulas.rs index bf1ba7a..650361e 100644 --- a/src/parse/formulas.rs +++ b/src/parse/formulas.rs @@ -47,7 +47,46 @@ pub fn boolean(i: &str) -> IResult<&str, crate::Formula> ))(i) } -/*fn formula_parenthesized<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula> +pub fn predicate<'i>(i: &'i str, d: &Declarations) -> IResult<&'i str, crate::Predicate> +{ + map + ( + |i| crate::parse::terms::function_or_predicate(i, d), + |(name, arguments)| + { + let arguments = match arguments + { + Some(arguments) => arguments, + None => vec![], + }; + + let mut predicate_declarations = d.predicate_declarations.borrow_mut(); + + let declaration = match predicate_declarations.iter() + .find(|x| x.name == name && x.arity == arguments.len()) + { + Some(declaration) => std::rc::Rc::clone(&declaration), + None => + { + let declaration = crate::PredicateDeclaration + { + name: name.to_string(), + arity: arguments.len(), + }; + let declaration = std::rc::Rc::new(declaration); + + predicate_declarations.insert(std::rc::Rc::clone(&declaration)); + + declaration + }, + }; + + crate::Predicate::new(declaration, arguments) + }, + )(i) +} + +fn formula_parenthesized<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula> { delimited ( @@ -65,39 +104,99 @@ pub fn boolean(i: &str) -> IResult<&str, crate::Formula> )(i) } -fn term_precedence_0<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Term> +fn formula_precedence_0<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula> { alt (( boolean, - special_integer, - integer, map ( - |i| function(i, d), - crate::Term::Function, + |i| predicate(i, d), + crate::Formula::Predicate, ), - string, - map - ( - |i| variable(i, d), - crate::Term::Variable, - ), - |i| absolute_value(i, d), - |i| term_parenthesized(i, d), + // TODO: comparisons + // TODO: quantified expressions + // TODO: negation + |i| formula_parenthesized(i, d), ))(i) } -fn term_precedence_1<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Term> +fn formula_precedence_3<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula> { alt (( - |i| negative(i, d), - |i| term_precedence_0(i, d), + map_res + ( + 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)) + } + } + ), + // TODO: fix + |i| formula_precedence_0(i, d), ))(i) } -fn term_precedence_2<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Term> +fn formula_precedence_4<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula> +{ + alt + (( + 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(crate::Formula::or(arguments.into_iter().map(Box::new).collect())) + } + else + { + Err(nom::error::make_error(i, nom::error::ErrorKind::Many1)) + } + } + ), + |i| formula_precedence_3(i, d), + ))(i) +} + +fn implication_left_to_right<'a>(i: &'a str, d: &Declarations) + -> IResult<&'a str, crate::Formula> { alt (( @@ -109,26 +208,28 @@ fn term_precedence_2<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate ( terminated ( - |i| term_precedence_1(i, d), + |i| formula_precedence_4(i, d), delimited ( multispace0, - tag("**"), + tag("->"), multispace0, ), ) ), - |i| term_precedence_1(i, d), + |i| formula_precedence_4(i, d), ), |(arguments, last_argument)| arguments.into_iter().rev().fold(last_argument, |accumulator, argument| - crate::Term::exponentiate(Box::new(argument), Box::new(accumulator))), + crate::Formula::implies(crate::ImplicationDirection::LeftToRight, + Box::new(accumulator), Box::new(argument))) ), - |i| term_precedence_1(i, d), + |i| formula_precedence_4(i, d), ))(i) } -fn term_precedence_3<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Term> +fn implication_right_to_left<'a>(i: &'a str, d: &Declarations) + -> IResult<&'a str, crate::Formula> { alt (( @@ -136,92 +237,82 @@ fn term_precedence_3<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate ( pair ( - |i| term_precedence_2(i, d), + |i| formula_precedence_4(i, d), many1 ( - pair + preceded ( delimited ( multispace0, - alt - (( - tag("*"), - tag("/"), - tag("%"), - )), + tag("<-"), multispace0, ), - |i| term_precedence_2(i, d), + |i| formula_precedence_4(i, d), ) ), ), |(first_argument, arguments)| arguments.into_iter().fold(first_argument, - |accumulator, (operator, argument)| - match operator - { - "*" => crate::Term::multiply(Box::new(accumulator), Box::new(argument)), - "/" => crate::Term::divide(Box::new(accumulator), Box::new(argument)), - "%" => crate::Term::modulo(Box::new(accumulator), Box::new(argument)), - // TODO: handle appropriately - _ => panic!("test"), - }) + |accumulator, argument| + crate::Formula::implies(crate::ImplicationDirection::RightToLeft, + Box::new(accumulator), Box::new(argument))) ), - |i| term_precedence_2(i, d), + |i| formula_precedence_4(i, d), ))(i) } -fn term_precedence_4<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Term> +fn formula_precedence_5<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula> { alt (( - map + |i| implication_right_to_left(i, d), + |i| implication_left_to_right(i, d), + ))(i) +} + +fn formula_precedence_6<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula> +{ + alt + (( + map_res ( - pair + separated_list ( - |i| term_precedence_3(i, d), - many1 + delimited ( - pair - ( - delimited - ( - multispace0, - alt - (( - tag("+"), - tag("-"), - )), - multispace0, - ), - |i| term_precedence_3(i, d), - ) + multispace0, + tag("<->"), + multispace0, ), + |i| formula_precedence_5(i, d), ), - |(first_argument, arguments)| arguments.into_iter().fold(first_argument, - |accumulator, (operator, argument)| - match operator + |arguments| -> Result<_, (_, _)> + { + if arguments.len() >= 2 { - "+" => crate::Term::add(Box::new(accumulator), Box::new(argument)), - "-" => crate::Term::subtract(Box::new(accumulator), Box::new(argument)), - // TODO: handle appropriately - _ => panic!("test"), - }) + 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| term_precedence_3(i, d), + |i| formula_precedence_5(i, d), ))(i) } pub fn formula<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula> { - formula_precedence_4(i, d) -}*/ + formula_precedence_6(i, d) +} #[cfg(test)] mod tests { use crate::parse::formulas::*; - use crate::{Formula, VariableDeclaration, VariableDeclarationStack}; + use crate::{Formula, Term, VariableDeclaration, VariableDeclarationStack}; /*fn formula(i: &str) -> Formula { @@ -257,4 +348,45 @@ mod tests assert!(boolean("-").is_err()); assert!(boolean(" ").is_err()); } + + #[test] + fn parse_predicate() + { + assert_eq!(predicate("s", &Declarations::new()) + .map(|(i, x)| (i, x.declaration.name.clone())), + Ok(("", "s".to_string()))); + assert_eq!(predicate("s", &Declarations::new()) + .map(|(i, x)| (i, x.declaration.arity)), + Ok(("", 0))); + assert_eq!(predicate("s ( )", &Declarations::new()) + .map(|(i, x)| (i, x.declaration.name.clone())), + Ok(("", "s".to_string()))); + assert_eq!(predicate("s ( )", &Declarations::new()) + .map(|(i, x)| (i, x.declaration.arity)), + Ok(("", 0))); + assert_eq!(predicate("s ( 1 , 2 , 3 )", &Declarations::new()) + .map(|(i, x)| (i, x.declaration.name.clone())), + Ok(("", "s".to_string()))); + assert_eq!(predicate("s ( 1 , 2 , 3 )", &Declarations::new()) + .map(|(i, x)| (i, x.declaration.arity)), + Ok(("", 3))); + assert_eq!(predicate("s ( 1 , 2 , 3 )", &Declarations::new()) + .map(|(i, mut x)| (i, x.arguments.remove(0))), + Ok(("", Box::new(Term::integer(1))))); + assert_eq!(predicate("s ( 1 , 2 , 3 )", &Declarations::new()) + .map(|(i, mut x)| (i, x.arguments.remove(2))), + Ok(("", Box::new(Term::integer(3))))); + assert_eq!(predicate("s ( ), rest", &Declarations::new()) + .map(|(i, x)| (i, x.declaration.name.clone())), + Ok((", rest", "s".to_string()))); + assert_eq!(predicate("s ( ), rest", &Declarations::new()) + .map(|(i, x)| (i, x.declaration.arity)), + Ok((", rest", 0))); + assert_eq!(predicate("s ( 1 , 2 , 3 ), rest", &Declarations::new()) + .map(|(i, x)| (i, x.declaration.name.clone())), + Ok((", rest", "s".to_string()))); + assert_eq!(predicate("s ( 1 , 2 , 3 ), rest", &Declarations::new()) + .map(|(i, x)| (i, x.declaration.arity)), + Ok((", rest", 3))); + } } diff --git a/src/parse/helpers.rs b/src/parse/helpers.rs index c622b86..26047f4 100644 --- a/src/parse/helpers.rs +++ b/src/parse/helpers.rs @@ -17,6 +17,9 @@ fn is_character_word_boundary(c: char) -> bool { '(' | ')' + | '>' + | '<' + | '=' | ',' | '+' | '-' @@ -73,6 +76,9 @@ mod tests assert_eq!(word_boundary("/rest"), Ok(("/rest", ()))); assert_eq!(word_boundary("%rest"), Ok(("%rest", ()))); assert_eq!(word_boundary("|rest"), Ok(("|rest", ()))); + assert_eq!(word_boundary("rest"), Ok((">rest", ()))); + assert_eq!(word_boundary("=rest"), Ok(("=rest", ()))); assert!(word_boundary("0").is_err()); assert!(word_boundary("rest").is_err()); } diff --git a/src/parse/terms.rs b/src/parse/terms.rs index a4ab1f3..4a1d18a 100644 --- a/src/parse/terms.rs +++ b/src/parse/terms.rs @@ -195,7 +195,7 @@ pub fn string(i: &str) -> IResult<&str, crate::Term> )(i) } -fn function_or_predicate<'i>(i: &'i str, d: &Declarations) +pub(crate) fn function_or_predicate<'i>(i: &'i str, d: &Declarations) -> IResult<&'i str, (&'i str, Option>>)> { pair @@ -274,45 +274,6 @@ pub fn function<'i>(i: &'i str, d: &Declarations) -> IResult<&'i str, crate::Fun )(i) } -pub fn predicate<'i>(i: &'i str, d: &Declarations) -> IResult<&'i str, crate::Predicate> -{ - map - ( - |i| function_or_predicate(i, d), - |(name, arguments)| - { - let arguments = match arguments - { - Some(arguments) => arguments, - None => vec![], - }; - - let mut predicate_declarations = d.predicate_declarations.borrow_mut(); - - let declaration = match predicate_declarations.iter() - .find(|x| x.name == name && x.arity == arguments.len()) - { - Some(declaration) => std::rc::Rc::clone(&declaration), - None => - { - let declaration = crate::PredicateDeclaration - { - name: name.to_string(), - arity: arguments.len(), - }; - let declaration = std::rc::Rc::new(declaration); - - predicate_declarations.insert(std::rc::Rc::clone(&declaration)); - - declaration - }, - }; - - crate::Predicate::new(declaration, arguments) - }, - )(i) -} - pub fn variable_declaration(i: &str) -> IResult<&str, crate::VariableDeclaration> { map