From b76287a07b747c427ce622f2ddddf3959c5616f1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Fri, 1 Nov 2019 22:00:17 +0100 Subject: [PATCH] Restructure crate for a nicer interface --- examples/test.rs | 2 + src/ast.rs | 76 +++ src/format.rs | 306 ++++++++++ src/lib.rs | 1485 +--------------------------------------------- src/parse.rs | 1097 ++++++++++++++++++++++++++++++++++ 5 files changed, 1486 insertions(+), 1480 deletions(-) create mode 100644 src/ast.rs create mode 100644 src/format.rs create mode 100644 src/parse.rs diff --git a/examples/test.rs b/examples/test.rs index 297265d..7497522 100644 --- a/examples/test.rs +++ b/examples/test.rs @@ -1,3 +1,5 @@ +use foliage::format; + fn main() -> Result<(), Box> { let formulas = "forall XV1 (p(XV1) <-> (exists XU1 (exists X1, X2 (X1 = XU1 and exists N1, N2, N3 (N1 = 0 and N2 = n and N1 <= N3 and N3 <= N2 and X2 = N3) and X1 = X2) and exists X3, X4 (exists N4, N5 (X3 = (N4 * N5) and N4 = XU1 and N5 = XU1) and X4 = n and X3 <= X4) and XV1 = XU1))) diff --git a/src/ast.rs b/src/ast.rs new file mode 100644 index 0000000..ef19a04 --- /dev/null +++ b/src/ast.rs @@ -0,0 +1,76 @@ +#[derive(PartialEq)] +pub struct PredicateDeclaration +{ + pub name: String, + pub arity: usize, +} + +#[derive(PartialEq)] +pub struct Predicate +{ + pub declaration: PredicateDeclaration, + pub arguments: Vec, +} + +#[derive(PartialEq)] +pub struct Exists +{ + pub parameters: Vec, + pub argument: Box, +} + +#[derive(PartialEq)] +pub struct ForAll +{ + pub parameters: Vec, + pub argument: Box, +} + +#[derive(PartialEq)] +pub enum Formula +{ + Exists(Exists), + ForAll(ForAll), + Not(Box), + And(Vec>), + Or(Vec>), + Implies(Box, Box), + Biconditional(Box, Box), + Less(Term, Term), + LessOrEqual(Term, Term), + Greater(Term, Term), + GreaterOrEqual(Term, Term), + Equal(Term, Term), + NotEqual(Term, Term), + Boolean(bool), + Predicate(Predicate), +} + +#[derive(PartialEq)] +pub enum Domain +{ + Program, + Integer, +} + +#[derive(PartialEq)] +pub struct VariableDeclaration +{ + pub name: String, + pub domain: Domain, +} + +#[derive(PartialEq)] +pub enum Term +{ + Infimum, + Supremum, + Integer(i64), + Symbolic(String), + String(String), + Variable(VariableDeclaration), + Add(Box, Box), + Subtract(Box, Box), + Multiply(Box, Box), + Negative(Box), +} diff --git a/src/format.rs b/src/format.rs new file mode 100644 index 0000000..bf6170b --- /dev/null +++ b/src/format.rs @@ -0,0 +1,306 @@ +fn term_precedence(term: &crate::Term) -> u64 +{ + match term + { + crate::Term::Infimum | crate::Term::Supremum | crate::Term::Integer(_) | crate::Term::Symbolic(_) | crate::Term::String(_) | crate::Term::Variable(_) => 0, + crate::Term::Negative(_) => 1, + crate::Term::Multiply(_, _) => 2, + crate::Term::Add(_, _) | crate::Term::Subtract(_, _) => 3, + } +} + +fn formula_precedence(formula: &crate::Formula) -> u64 +{ + match formula + { + crate::Formula::Predicate(_) | crate::Formula::Boolean(_) | crate::Formula::Less(_, _) | crate::Formula::LessOrEqual(_, _) | crate::Formula::Greater(_, _) | crate::Formula::GreaterOrEqual(_, _) | crate::Formula::Equal(_, _) | crate::Formula::NotEqual(_, _) => 0, + crate::Formula::Exists(_) | crate::Formula::ForAll(_) => 1, + crate::Formula::Not(_) => 2, + crate::Formula::And(_) => 3, + crate::Formula::Or(_) => 4, + crate::Formula::Implies(_, _) => 5, + crate::Formula::Biconditional(_, _) => 6, + } +} + +impl std::fmt::Debug for crate::VariableDeclaration +{ + fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result + { + match &self.domain + { + crate::Domain::Program => write!(format, "X")?, + crate::Domain::Integer => write!(format, "N")?, + }; + + write!(format, "{}", &self.name) + } +} + +impl std::fmt::Display for crate::VariableDeclaration +{ + fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result + { + match &self.domain + { + crate::Domain::Program => write!(format, "X")?, + crate::Domain::Integer => write!(format, "N")?, + }; + + write!(format, "{}", &self.name) + } +} + +impl std::fmt::Debug for crate::Term +{ + fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result + { + match *self + { + crate::Term::Infimum => write!(format, "#inf"), + crate::Term::Supremum => write!(format, "#sup"), + crate::Term::Integer(value) => write!(format, "{}", value), + crate::Term::Symbolic(ref value) => write!(format, "{}", value), + crate::Term::String(ref value) => write!(format, "\"{}\"", value), + crate::Term::Variable(ref declaration) => write!(format, "{:?}", declaration), + crate::Term::Add(ref left, ref right) => write!(format, "({:?} + {:?})", left, right), + crate::Term::Subtract(ref left, ref right) => write!(format, "({:?} - {:?})", left, right), + crate::Term::Multiply(ref left, ref right) => write!(format, "({:?} * {:?})", left, right), + crate::Term::Negative(ref argument) => write!(format, "-({:?})", argument), + } + } +} + +impl std::fmt::Display for crate::Term +{ + fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result + { + match *self + { + crate::Term::Infimum => write!(format, "#inf"), + crate::Term::Supremum => write!(format, "#sup"), + crate::Term::Integer(value) => write!(format, "{}", value), + crate::Term::Symbolic(ref value) => write!(format, "{}", value), + crate::Term::String(ref value) => write!(format, "\"{}\"", value), + crate::Term::Variable(ref declaration) => write!(format, "{}", declaration), + crate::Term::Add(ref left, ref right) => write!(format, "({} + {})", left, right), + crate::Term::Subtract(ref left, ref right) => write!(format, "({} - {})", left, right), + crate::Term::Multiply(ref left, ref right) => write!(format, "({} * {})", left, right), + crate::Term::Negative(ref argument) => write!(format, "-({})", argument), + } + } +} + +impl std::fmt::Debug for crate::Formula +{ + fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result + { + match *self + { + crate::Formula::Exists(ref exists) => + { + write!(format, "exists")?; + + let mut separator = " "; + + for parameter in &exists.parameters + { + write!(format, "{}{:?}", separator, parameter)?; + + separator = ", " + } + + write!(format, " ({:?})", exists.argument) + }, + crate::Formula::ForAll(ref for_all) => + { + write!(format, "forall")?; + + let mut separator = " "; + + for parameter in &for_all.parameters + { + write!(format, "{}{:?}", separator, parameter)?; + + separator = ", " + } + + write!(format, " ({:?})", for_all.argument) + }, + crate::Formula::Not(ref argument) => write!(format, "not {:?}", argument), + crate::Formula::And(ref arguments) => + { + write!(format, "(")?; + + let mut separator = ""; + + for argument in arguments + { + write!(format, "{}{:?}", separator, argument)?; + + separator = " and " + } + + write!(format, ")") + }, + crate::Formula::Or(ref arguments) => + { + write!(format, "(")?; + + let mut separator = ""; + + for argument in arguments + { + write!(format, "{}{:?}", separator, argument)?; + + separator = " or " + } + + write!(format, ")") + }, + crate::Formula::Implies(ref left, ref right) => write!(format, "({:?} -> {:?})", left, right), + crate::Formula::Biconditional(ref left, ref right) => write!(format, "({:?} <-> {:?})", left, right), + crate::Formula::Less(ref left, ref right) => write!(format, "({:?} < {:?})", left, right), + crate::Formula::LessOrEqual(ref left, ref right) => write!(format, "({:?} <= {:?})", left, right), + crate::Formula::Greater(ref left, ref right) => write!(format, "({:?} > {:?})", left, right), + crate::Formula::GreaterOrEqual(ref left, ref right) => write!(format, "({:?} >= {:?})", left, right), + crate::Formula::Equal(ref left, ref right) => write!(format, "({:?} = {:?})", left, right), + crate::Formula::NotEqual(ref left, ref right) => write!(format, "({:?} != {:?})", left, right), + crate::Formula::Boolean(value) => + match value + { + true => write!(format, "#true"), + false => write!(format, "#false"), + }, + crate::Formula::Predicate(ref predicate) => + { + write!(format, "{}", predicate.declaration.name)?; + + if !predicate.arguments.is_empty() + { + write!(format, "(")?; + + let mut separator = ""; + + for argument in &predicate.arguments + { + write!(format, "{}{:?}", separator, argument)?; + + separator = ", " + } + + write!(format, ")")?; + } + + Ok(()) + }, + } + } +} + +impl std::fmt::Display for crate::Formula +{ + fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result + { + match *self + { + crate::Formula::Exists(ref exists) => + { + write!(format, "exists")?; + + let mut separator = " "; + + for parameter in &exists.parameters + { + write!(format, "{}{}", separator, parameter)?; + + separator = ", " + } + + write!(format, " ({})", exists.argument) + }, + crate::Formula::ForAll(ref for_all) => + { + write!(format, "forall")?; + + let mut separator = " "; + + for parameter in &for_all.parameters + { + write!(format, "{}{}", separator, parameter)?; + + separator = ", " + } + + write!(format, " ({})", for_all.argument) + }, + crate::Formula::Not(ref argument) => write!(format, "not {}", argument), + crate::Formula::And(ref arguments) => + { + write!(format, "(")?; + + let mut separator = ""; + + for argument in arguments + { + write!(format, "{}{}", separator, argument)?; + + separator = " and " + } + + write!(format, ")") + }, + crate::Formula::Or(ref arguments) => + { + write!(format, "(")?; + + let mut separator = ""; + + for argument in arguments + { + write!(format, "{}{}", separator, argument)?; + + separator = " or " + } + + write!(format, ")") + }, + crate::Formula::Implies(ref left, ref right) => write!(format, "({} -> {})", left, right), + crate::Formula::Biconditional(ref left, ref right) => write!(format, "({} <-> {})", left, right), + crate::Formula::Less(ref left, ref right) => write!(format, "({} < {})", left, right), + crate::Formula::LessOrEqual(ref left, ref right) => write!(format, "({} <= {})", left, right), + crate::Formula::Greater(ref left, ref right) => write!(format, "({} > {})", left, right), + crate::Formula::GreaterOrEqual(ref left, ref right) => write!(format, "({} >= {})", left, right), + crate::Formula::Equal(ref left, ref right) => write!(format, "({} = {})", left, right), + crate::Formula::NotEqual(ref left, ref right) => write!(format, "({} != {})", left, right), + crate::Formula::Boolean(value) => + match value + { + true => write!(format, "#true"), + false => write!(format, "#false"), + }, + crate::Formula::Predicate(ref predicate) => + { + write!(format, "{}", predicate.declaration.name)?; + + if !predicate.arguments.is_empty() + { + write!(format, "(")?; + + let mut separator = ""; + + for argument in &predicate.arguments + { + write!(format, "{}{}", separator, argument)?; + + separator = ", " + } + + write!(format, ")")?; + } + + Ok(()) + }, + } + } +} diff --git a/src/lib.rs b/src/lib.rs index caf7e0d..be744e7 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,1481 +1,6 @@ -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, -}; +mod ast; +pub mod format; +mod parse; -#[derive(PartialEq)] -pub struct PredicateDeclaration -{ - name: String, - arity: usize, -} - -#[derive(PartialEq)] -pub struct Predicate -{ - declaration: PredicateDeclaration, - arguments: Vec, -} - -#[derive(PartialEq)] -pub struct Exists -{ - parameters: Vec, - argument: Box, -} - -#[derive(PartialEq)] -pub struct ForAll -{ - parameters: Vec, - argument: Box, -} - -#[derive(PartialEq)] -pub enum Formula -{ - Exists(Exists), - ForAll(ForAll), - Not(Box), - And(Vec>), - Or(Vec>), - Implies(Box, Box), - Biconditional(Box, Box), - Less(Term, Term), - LessOrEqual(Term, Term), - Greater(Term, Term), - GreaterOrEqual(Term, Term), - Equal(Term, Term), - NotEqual(Term, Term), - Boolean(bool), - Predicate(Predicate), -} - -#[derive(PartialEq)] -pub enum Domain -{ - Program, - Integer, -} - -#[derive(PartialEq)] -pub struct VariableDeclaration -{ - name: String, - domain: Domain, -} - -#[derive(PartialEq)] -pub enum Term -{ - Infimum, - Supremum, - Integer(i64), - Symbolic(String), - String(String), - Variable(VariableDeclaration), - Add(Box, Box), - Subtract(Box, Box), - Multiply(Box, Box), - Negative(Box), -} - -pub enum TermOperator -{ - Add, - Subtract, - Multiply, -} - -impl std::fmt::Debug for VariableDeclaration -{ - fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result - { - match &self.domain - { - Domain::Program => write!(format, "X")?, - Domain::Integer => write!(format, "N")?, - }; - - write!(format, "{}", &self.name) - } -} - -impl std::fmt::Display for VariableDeclaration -{ - fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result - { - match &self.domain - { - Domain::Program => write!(format, "X")?, - Domain::Integer => write!(format, "N")?, - }; - - write!(format, "{}", &self.name) - } -} - -pub fn term_precedence(term: &Term) -> u64 -{ - match term - { - Term::Infimum | Term::Supremum | Term::Integer(_) | Term::Symbolic(_) | Term::String(_) | Term::Variable(_) => 0, - Term::Negative(_) => 1, - Term::Multiply(_, _) => 2, - Term::Add(_, _) | Term::Subtract(_, _) => 3, - } -} - -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::Exists(_) | Formula::ForAll(_) => 1, - Formula::Not(_) => 2, - Formula::And(_) => 3, - Formula::Or(_) => 4, - Formula::Implies(_, _) => 5, - Formula::Biconditional(_, _) => 6, - } -} - -impl std::fmt::Debug for Term -{ - fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result - { - match *self - { - Term::Infimum => write!(format, "#inf"), - Term::Supremum => write!(format, "#sup"), - Term::Integer(value) => write!(format, "{}", value), - Term::Symbolic(ref value) => write!(format, "{}", value), - Term::String(ref value) => write!(format, "\"{}\"", value), - Term::Variable(ref declaration) => write!(format, "{:?}", declaration), - Term::Add(ref left, ref right) => write!(format, "({:?} + {:?})", left, right), - Term::Subtract(ref left, ref right) => write!(format, "({:?} - {:?})", left, right), - Term::Multiply(ref left, ref right) => write!(format, "({:?} * {:?})", left, right), - Term::Negative(ref argument) => write!(format, "-({:?})", argument), - } - } -} - -impl std::fmt::Display for Term -{ - fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result - { - match *self - { - Term::Infimum => write!(format, "#inf"), - Term::Supremum => write!(format, "#sup"), - Term::Integer(value) => write!(format, "{}", value), - Term::Symbolic(ref value) => write!(format, "{}", value), - Term::String(ref value) => write!(format, "\"{}\"", value), - Term::Variable(ref declaration) => write!(format, "{}", declaration), - Term::Add(ref left, ref right) => write!(format, "({} + {})", left, right), - Term::Subtract(ref left, ref right) => write!(format, "({} - {})", left, right), - Term::Multiply(ref left, ref right) => write!(format, "({} * {})", left, right), - Term::Negative(ref argument) => write!(format, "-({})", argument), - } - } -} - -impl std::fmt::Debug for Formula -{ - fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result - { - match *self - { - Formula::Exists(ref exists) => - { - write!(format, "exists")?; - - let mut separator = " "; - - for parameter in &exists.parameters - { - write!(format, "{}{:?}", separator, parameter)?; - - separator = ", " - } - - write!(format, " ({:?})", exists.argument) - }, - Formula::ForAll(ref for_all) => - { - write!(format, "forall")?; - - let mut separator = " "; - - for parameter in &for_all.parameters - { - write!(format, "{}{:?}", separator, parameter)?; - - separator = ", " - } - - write!(format, " ({:?})", for_all.argument) - }, - Formula::Not(ref argument) => write!(format, "not {:?}", argument), - Formula::And(ref arguments) => - { - write!(format, "(")?; - - let mut separator = ""; - - for argument in arguments - { - write!(format, "{}{:?}", separator, argument)?; - - separator = " and " - } - - write!(format, ")") - }, - Formula::Or(ref arguments) => - { - write!(format, "(")?; - - let mut separator = ""; - - for argument in arguments - { - write!(format, "{}{:?}", separator, argument)?; - - separator = " or " - } - - write!(format, ")") - }, - Formula::Implies(ref left, ref right) => write!(format, "({:?} -> {:?})", left, right), - Formula::Biconditional(ref left, ref right) => write!(format, "({:?} <-> {:?})", left, right), - Formula::Less(ref left, ref right) => write!(format, "({:?} < {:?})", left, right), - Formula::LessOrEqual(ref left, ref right) => write!(format, "({:?} <= {:?})", left, right), - Formula::Greater(ref left, ref right) => write!(format, "({:?} > {:?})", left, right), - Formula::GreaterOrEqual(ref left, ref right) => write!(format, "({:?} >= {:?})", left, right), - Formula::Equal(ref left, ref right) => write!(format, "({:?} = {:?})", left, right), - Formula::NotEqual(ref left, ref right) => write!(format, "({:?} != {:?})", left, right), - Formula::Boolean(value) => - match value - { - true => write!(format, "#true"), - false => write!(format, "#false"), - }, - Formula::Predicate(ref predicate) => - { - write!(format, "{}", predicate.declaration.name)?; - - if !predicate.arguments.is_empty() - { - write!(format, "(")?; - - let mut separator = ""; - - for argument in &predicate.arguments - { - write!(format, "{}{:?}", separator, argument)?; - - separator = ", " - } - - write!(format, ")")?; - } - - Ok(()) - }, - } - } -} - -impl std::fmt::Display for Formula -{ - fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result - { - match *self - { - Formula::Exists(ref exists) => - { - write!(format, "exists")?; - - let mut separator = " "; - - for parameter in &exists.parameters - { - write!(format, "{}{}", separator, parameter)?; - - separator = ", " - } - - write!(format, " ({})", exists.argument) - }, - Formula::ForAll(ref for_all) => - { - write!(format, "forall")?; - - let mut separator = " "; - - for parameter in &for_all.parameters - { - write!(format, "{}{}", separator, parameter)?; - - separator = ", " - } - - write!(format, " ({})", for_all.argument) - }, - Formula::Not(ref argument) => write!(format, "not {}", argument), - Formula::And(ref arguments) => - { - write!(format, "(")?; - - let mut separator = ""; - - for argument in arguments - { - write!(format, "{}{}", separator, argument)?; - - separator = " and " - } - - write!(format, ")") - }, - Formula::Or(ref arguments) => - { - write!(format, "(")?; - - let mut separator = ""; - - for argument in arguments - { - write!(format, "{}{}", separator, argument)?; - - separator = " or " - } - - write!(format, ")") - }, - Formula::Implies(ref left, ref right) => write!(format, "({} -> {})", left, right), - Formula::Biconditional(ref left, ref right) => write!(format, "({} <-> {})", left, right), - Formula::Less(ref left, ref right) => write!(format, "({} < {})", left, right), - Formula::LessOrEqual(ref left, ref right) => write!(format, "({} <= {})", left, right), - Formula::Greater(ref left, ref right) => write!(format, "({} > {})", left, right), - Formula::GreaterOrEqual(ref left, ref right) => write!(format, "({} >= {})", left, right), - Formula::Equal(ref left, ref right) => write!(format, "({} = {})", left, right), - Formula::NotEqual(ref left, ref right) => write!(format, "({} != {})", left, right), - Formula::Boolean(value) => - match value - { - true => write!(format, "#true"), - false => write!(format, "#false"), - }, - Formula::Predicate(ref predicate) => - { - write!(format, "{}", predicate.declaration.name)?; - - if !predicate.arguments.is_empty() - { - write!(format, "(")?; - - let mut separator = ""; - - for argument in &predicate.arguments - { - write!(format, "{}{}", separator, argument)?; - - separator = ", " - } - - write!(format, ")")?; - } - - Ok(()) - }, - } - } -} - -fn infimum(i: &str) -> IResult<&str, Term> -{ - map - ( - delimited(multispace0, tag("#inf"), multispace0), - |_| Term::Infimum - )(i) -} - -fn supremum(i: &str) -> IResult<&str, Term> -{ - map - ( - delimited(multispace0, tag("#sup"), multispace0), - |_| Term::Supremum - )(i) -} - -fn integer(i: &str) -> IResult<&str, Term> -{ - map - ( - map_res - ( - delimited(multispace0, digit1, multispace0), - std::str::FromStr::from_str - ), - Term::Integer - )(i) -} - -fn is_lowercase_alphanumeric(c: char) -> bool -{ - c.is_alphanumeric() && c.is_lowercase() -} - -fn symbolic_identifier(i: &str) -> IResult<&str, String> -{ - let (i, symbolic_identifier) = map - ( - pair - ( - take_while_m_n(1, 1, is_lowercase_alphanumeric), - take_while(char::is_alphanumeric) - ), - |(s0, s1)| format!("{}{}", s0, s1) - )(i)?; - - Ok((i, symbolic_identifier)) -} - -fn symbolic(i: &str) -> IResult<&str, Term> -{ - map - ( - delimited(multispace0, symbolic_identifier, multispace0), - Term::Symbolic - )(i) -} - -fn string(i: &str) -> IResult<&str, Term> -{ - map - ( - delimited - ( - multispace0, - delimited - ( - tag("\""), - is_not("\""), - tag("\""), - ), - multispace0 - ), - |s: &str| Term::String(s.to_string()) - )(i) -} - -fn program_variable_identifier(i: &str) -> IResult<&str, String> -{ - map - ( - delimited - ( - multispace0, - preceded - ( - tag("X"), - take_while(char::is_alphanumeric) - ), - multispace0 - ), - |s: &str| s.to_string() - )(i) -} - -fn integer_variable_identifier(i: &str) -> IResult<&str, String> -{ - map - ( - delimited - ( - multispace0, - preceded - ( - tag("N"), - take_while(char::is_alphanumeric) - ), - multispace0 - ), - |s: &str| s.to_string() - )(i) -} - -fn program_variable_declaration(i: &str) -> IResult<&str, VariableDeclaration> -{ - map - ( - program_variable_identifier, - |s| VariableDeclaration{name: s, domain: Domain::Program} - )(i) -} - -fn integer_variable_declaration(i: &str) -> IResult<&str, VariableDeclaration> -{ - map - ( - integer_variable_identifier, - |s| VariableDeclaration{name: s, domain: Domain::Integer} - )(i) -} - -fn variable_declaration(i: &str) -> IResult<&str, VariableDeclaration> -{ - alt - (( - program_variable_declaration, - integer_variable_declaration - ))(i) -} - -fn program_variable(i: &str) -> IResult<&str, Term> -{ - map - ( - program_variable_identifier, - |s| Term::Variable(VariableDeclaration{name: s, domain: Domain::Program}) - )(i) -} - -fn integer_variable(i: &str) -> IResult<&str, Term> -{ - map - ( - integer_variable_identifier, - |s| Term::Variable(VariableDeclaration{name: s, domain: Domain::Integer}) - )(i) -} - -fn variable(i: &str) -> IResult<&str, Term> -{ - alt - (( - program_variable, - integer_variable - ))(i) -} - -fn predicate_0_ary(i: &str) -> IResult<&str, Formula> -{ - map - ( - delimited(multispace0, symbolic_identifier, multispace0), - |name| Formula::Predicate( - Predicate - { - declaration: - PredicateDeclaration - { - name: name, - arity: 0, - }, - arguments: vec![], - }) - )(i) -} - -fn predicate_n_ary(i: &str) -> IResult<&str, Formula> -{ - map - ( - pair - ( - delimited(multispace0, symbolic_identifier, multispace0), - delimited - ( - multispace0, - delimited - ( - tag("("), - separated_list(tag(","), term), - tag(")") - ), - multispace0 - ) - ), - |(name, arguments)| Formula::Predicate( - Predicate - { - declaration: - PredicateDeclaration - { - name: name, - arity: arguments.len(), - }, - arguments: arguments, - }) - )(i) -} - -fn predicate(i: &str) -> IResult<&str, Formula> -{ - alt - (( - predicate_n_ary, - predicate_0_ary - ))(i) -} - -fn boolean(i: &str) -> IResult<&str, Formula> -{ - map - ( - delimited - ( - multispace0, - alt - (( - map(tag("#true"), |_| true), - map(tag("#false"), |_| false) - )), - multispace0 - ), - |value| Formula::Boolean(value) - )(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> -{ - delimited - ( - multispace0, - delimited - ( - tag("("), - term, - tag(")") - ), - multispace0 - )(i) -} - -fn fold_terms(initial: Term, remainder: Vec<(TermOperator, Term)>) -> Term -{ - remainder.into_iter().fold(initial, - |accumulator, pair| - { - let (term_operator, term) = pair; - - match term_operator - { - TermOperator::Add => Term::Add(Box::new(accumulator), Box::new(term)), - TermOperator::Subtract => Term::Subtract(Box::new(accumulator), Box::new(term)), - TermOperator::Multiply => Term::Multiply(Box::new(accumulator), Box::new(term)), - } - }) -} - -fn term_precedence_0(i: &str) -> IResult<&str, Term> -{ - alt - (( - infimum, - supremum, - integer, - symbolic, - string, - variable, - term_parenthesized - ))(i) -} - -fn term_precedence_1(i: &str) -> IResult<&str, Term> -{ - alt - (( - map - ( - delimited - ( - multispace0, - preceded(tag("-"), term_precedence_0), - multispace0 - ), - |term| Term::Negative(Box::new(term)) - ), - term_precedence_0 - ))(i) -} - -fn term_precedence_2(i: &str) -> IResult<&str, 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(i: &str) -> IResult<&str, 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(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 -{ - #[test] - fn parse_integer() - { - assert_eq!(crate::integer("12345"), Ok(("", crate::Term::Integer(12345)))); - } - - #[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()}))); - } - - #[test] - fn parse_variable() - { - assert_eq!(crate::variable("X5"), Ok(("", crate::Term::Variable(crate::VariableDeclaration{domain: crate::Domain::Program, name: "5".to_string()})))); - assert_eq!(crate::variable("NX3"), Ok(("", crate::Term::Variable(crate::VariableDeclaration{domain: crate::Domain::Integer, name: "X3".to_string()})))); - } - - #[test] - fn parse_string() - { - assert_eq!(crate::string(" \"foobar\" "), Ok(("", crate::Term::String("foobar".to_string())))); - } - - #[test] - fn parse_boolean() - { - assert_eq!(crate::boolean(" #true "), Ok(("", crate::Formula::Boolean(true)))); - assert_eq!(crate::boolean(" #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::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(("", - 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::predicate(" 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::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)), - ] - )), - } - )), - } - )))); - } -} +pub use ast::{Domain, Exists, Formula, ForAll, Predicate, PredicateDeclaration, VariableDeclaration, Term}; +pub use parse::{formula, formulas, term}; diff --git a/src/parse.rs b/src/parse.rs new file mode 100644 index 0000000..20e5499 --- /dev/null +++ b/src/parse.rs @@ -0,0 +1,1097 @@ +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, +}; + +enum TermOperator +{ + Add, + Subtract, + Multiply, +} + +fn infimum(i: &str) -> IResult<&str, crate::Term> +{ + map + ( + delimited(multispace0, tag("#inf"), multispace0), + |_| crate::Term::Infimum + )(i) +} + +fn supremum(i: &str) -> IResult<&str, crate::Term> +{ + map + ( + delimited(multispace0, tag("#sup"), multispace0), + |_| crate::Term::Supremum + )(i) +} + +fn integer(i: &str) -> IResult<&str, crate::Term> +{ + map + ( + map_res + ( + delimited(multispace0, digit1, multispace0), + std::str::FromStr::from_str + ), + crate::Term::Integer + )(i) +} + +fn is_lowercase_alphanumeric(c: char) -> bool +{ + c.is_alphanumeric() && c.is_lowercase() +} + +fn symbolic_identifier(i: &str) -> IResult<&str, String> +{ + let (i, symbolic_identifier) = map + ( + pair + ( + take_while_m_n(1, 1, is_lowercase_alphanumeric), + take_while(char::is_alphanumeric) + ), + |(s0, s1)| format!("{}{}", s0, s1) + )(i)?; + + Ok((i, symbolic_identifier)) +} + +fn symbolic(i: &str) -> IResult<&str, crate::Term> +{ + map + ( + delimited(multispace0, symbolic_identifier, multispace0), + crate::Term::Symbolic + )(i) +} + +fn string(i: &str) -> IResult<&str, crate::Term> +{ + map + ( + delimited + ( + multispace0, + delimited + ( + tag("\""), + is_not("\""), + tag("\""), + ), + multispace0 + ), + |s: &str| crate::Term::String(s.to_string()) + )(i) +} + +fn program_variable_identifier(i: &str) -> IResult<&str, String> +{ + map + ( + delimited + ( + multispace0, + preceded + ( + tag("X"), + take_while(char::is_alphanumeric) + ), + multispace0 + ), + |s: &str| s.to_string() + )(i) +} + +fn integer_variable_identifier(i: &str) -> IResult<&str, String> +{ + map + ( + delimited + ( + multispace0, + preceded + ( + tag("N"), + take_while(char::is_alphanumeric) + ), + multispace0 + ), + |s: &str| s.to_string() + )(i) +} + +fn program_variable_declaration(i: &str) -> IResult<&str, crate::VariableDeclaration> +{ + map + ( + program_variable_identifier, + |s| crate::VariableDeclaration{name: s, domain: crate::Domain::Program} + )(i) +} + +fn integer_variable_declaration(i: &str) -> IResult<&str, crate::VariableDeclaration> +{ + map + ( + integer_variable_identifier, + |s| crate::VariableDeclaration{name: s, domain: crate::Domain::Integer} + )(i) +} + +fn variable_declaration(i: &str) -> IResult<&str, crate::VariableDeclaration> +{ + alt + (( + program_variable_declaration, + integer_variable_declaration + ))(i) +} + +fn program_variable(i: &str) -> IResult<&str, crate::Term> +{ + map + ( + program_variable_identifier, + |s| crate::Term::Variable(crate::VariableDeclaration{name: s, domain: crate::Domain::Program}) + )(i) +} + +fn integer_variable(i: &str) -> IResult<&str, crate::Term> +{ + map + ( + integer_variable_identifier, + |s| crate::Term::Variable(crate::VariableDeclaration{name: s, domain: crate::Domain::Integer}) + )(i) +} + +fn variable(i: &str) -> IResult<&str, crate::Term> +{ + alt + (( + program_variable, + integer_variable + ))(i) +} + +fn predicate_0_ary(i: &str) -> IResult<&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(i: &str) -> IResult<&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(i: &str) -> IResult<&str, crate::Formula> +{ + alt + (( + predicate_n_ary, + predicate_0_ary + ))(i) +} + +fn boolean(i: &str) -> IResult<&str, crate::Formula> +{ + map + ( + delimited + ( + multispace0, + alt + (( + map(tag("#true"), |_| true), + map(tag("#false"), |_| false) + )), + multispace0 + ), + |value| crate::Formula::Boolean(value) + )(i) +} + +fn less(i: &str) -> IResult<&str, crate::Formula> +{ + map + ( + pair + ( + term, + preceded(tag("<"), term) + ), + |(left, right)| crate::Formula::Less(left, right) + )(i) +} + +fn less_or_equal(i: &str) -> IResult<&str, crate::Formula> +{ + map + ( + pair + ( + term, + preceded(tag("<="), term) + ), + |(left, right)| crate::Formula::LessOrEqual(left, right) + )(i) +} + +fn greater(i: &str) -> IResult<&str, crate::Formula> +{ + map + ( + pair + ( + term, + preceded(tag(">"), term) + ), + |(left, right)| crate::Formula::Greater(left, right) + )(i) +} + +fn greater_or_equal(i: &str) -> IResult<&str, crate::Formula> +{ + map + ( + pair + ( + term, + preceded(tag(">="), term) + ), + |(left, right)| crate::Formula::GreaterOrEqual(left, right) + )(i) +} + +fn equal(i: &str) -> IResult<&str, crate::Formula> +{ + map + ( + pair + ( + term, + preceded(tag("="), term) + ), + |(left, right)| crate::Formula::Equal(left, right) + )(i) +} + +fn not_equal(i: &str) -> IResult<&str, crate::Formula> +{ + map + ( + pair + ( + term, + preceded(tag("!="), term) + ), + |(left, right)| crate::Formula::NotEqual(left, right) + )(i) +} + +fn comparison(i: &str) -> IResult<&str, crate::Formula> +{ + alt + (( + less, + less_or_equal, + greater, + greater_or_equal, + equal, + not_equal + ))(i) +} + +fn term_parenthesized(i: &str) -> IResult<&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(i: &str) -> IResult<&str, crate::Term> +{ + alt + (( + infimum, + supremum, + integer, + symbolic, + string, + variable, + term_parenthesized + ))(i) +} + +fn term_precedence_1(i: &str) -> IResult<&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(i: &str) -> IResult<&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(i: &str) -> IResult<&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(i: &str) -> IResult<&str, crate::Term> +{ + term_precedence_3(i) +} + +fn formula_parenthesized(i: &str) -> IResult<&str, crate::Formula> +{ + delimited + ( + multispace0, + delimited + ( + tag("("), + formula, + tag(")") + ), + multispace0 + )(i) +} + +fn formula_precedence_0(i: &str) -> IResult<&str, crate::Formula> +{ + alt + (( + predicate, + boolean, + comparison, + formula_parenthesized + ))(i) +} + +fn exists(i: &str) -> IResult<&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(i: &str) -> IResult<&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(i: &str) -> IResult<&str, crate::Formula> +{ + alt + (( + exists, + for_all, + formula_precedence_0 + ))(i) +} + +fn formula_precedence_2(i: &str) -> IResult<&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(i: &str) -> IResult<&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(i: &str) -> IResult<&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(i: &str) -> IResult<&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(i: &str) -> IResult<&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(i: &str) -> IResult<&str, crate::Formula> +{ + formula_precedence_6(i) +} + +pub fn formulas(i: &str) -> IResult<&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)), + ), + )))); + } + + #[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)), + ] + )), + } + )), + } + )))); + } +}