Finish implementing formula parsing
This commit is contained in:
parent
1c00e5be16
commit
a1bbae9201
GPG Key ID:
05F3611E97A70ABF
|
|
@ -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
|
||||
{
|
||||
|
|
|
|||
|
|
@ -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<Box<crate::Formula>>>
|
||||
{
|
||||
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<Box<crate::Formula>>>
|
||||
{
|
||||
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<Box<crate::Formula>>>
|
||||
{
|
||||
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<crate::VariableDeclarations>, Box<crate::Formula>) -> 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::<crate::Exists, _>(i, d, "exists", crate::Exists::new)
|
||||
}
|
||||
|
||||
fn for_all<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::ForAll>
|
||||
{
|
||||
quantified_expression::<crate::ForAll, _>(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());
|
||||
}
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in New Issue