2020-02-25 15:36:34 +01:00
|
|
|
|
use nom::
|
|
|
|
|
{
|
|
|
|
|
IResult,
|
|
|
|
|
branch::alt,
|
|
|
|
|
bytes::complete::tag,
|
|
|
|
|
character::complete::multispace0,
|
2020-04-20 02:40:13 +02:00
|
|
|
|
combinator::{cut, map, map_res, peek},
|
2020-04-17 18:22:50 +02:00
|
|
|
|
multi::{many1, separated_list1},
|
2020-02-25 15:36:34 +01:00
|
|
|
|
sequence::{delimited, pair, preceded, terminated, tuple},
|
|
|
|
|
};
|
|
|
|
|
|
2020-04-17 04:06:22 +02:00
|
|
|
|
use super::{boolean, word_boundary};
|
2020-02-25 15:36:34 +01:00
|
|
|
|
|
2020-04-17 04:06:22 +02:00
|
|
|
|
pub fn predicate<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
|
2020-04-17 02:53:23 +02:00
|
|
|
|
-> IResult<&'i str, crate::Predicate>
|
2020-04-17 04:06:22 +02:00
|
|
|
|
where
|
|
|
|
|
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
|
2020-02-25 15:36:34 +01:00
|
|
|
|
{
|
|
|
|
|
map
|
|
|
|
|
(
|
2020-04-17 02:53:23 +02:00
|
|
|
|
|i| crate::parse::terms::function_or_predicate(i, d, v),
|
2020-02-25 15:36:34 +01:00
|
|
|
|
|(name, arguments)|
|
|
|
|
|
{
|
|
|
|
|
let arguments = match arguments
|
|
|
|
|
{
|
|
|
|
|
Some(arguments) => arguments,
|
|
|
|
|
None => vec![],
|
|
|
|
|
};
|
|
|
|
|
|
2020-04-17 04:06:22 +02:00
|
|
|
|
let declaration = d.find_or_create_predicate_declaration(name, arguments.len());
|
2020-02-25 15:36:34 +01:00
|
|
|
|
|
|
|
|
|
crate::Predicate::new(declaration, arguments)
|
|
|
|
|
},
|
|
|
|
|
)(i)
|
|
|
|
|
}
|
|
|
|
|
|
2020-04-17 04:06:22 +02:00
|
|
|
|
fn not<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
|
2020-04-17 02:53:23 +02:00
|
|
|
|
-> IResult<&'i str, crate::Formula>
|
2020-04-17 04:06:22 +02:00
|
|
|
|
where
|
|
|
|
|
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
|
2020-02-25 15:36:34 +01:00
|
|
|
|
{
|
|
|
|
|
map
|
|
|
|
|
(
|
|
|
|
|
preceded
|
|
|
|
|
(
|
|
|
|
|
terminated
|
|
|
|
|
(
|
|
|
|
|
tag("not"),
|
|
|
|
|
multispace0,
|
|
|
|
|
),
|
2020-04-17 02:53:23 +02:00
|
|
|
|
|i| formula_precedence_2(i, d, v),
|
2020-02-25 15:36:34 +01:00
|
|
|
|
),
|
|
|
|
|
|x| crate::Formula::not(Box::new(x)),
|
|
|
|
|
)(i)
|
|
|
|
|
}
|
|
|
|
|
|
2020-04-17 04:06:22 +02:00
|
|
|
|
fn and<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
|
2020-04-17 02:53:23 +02:00
|
|
|
|
-> IResult<&'i str, crate::Formulas>
|
2020-04-17 04:06:22 +02:00
|
|
|
|
where
|
|
|
|
|
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
|
2020-02-25 15:36:34 +01:00
|
|
|
|
{
|
|
|
|
|
map_res
|
|
|
|
|
(
|
2020-04-17 18:22:50 +02:00
|
|
|
|
separated_list1
|
2020-02-25 15:36:34 +01:00
|
|
|
|
(
|
|
|
|
|
delimited
|
|
|
|
|
(
|
|
|
|
|
multispace0,
|
|
|
|
|
terminated
|
|
|
|
|
(
|
|
|
|
|
tag("and"),
|
|
|
|
|
word_boundary,
|
|
|
|
|
),
|
|
|
|
|
multispace0,
|
|
|
|
|
),
|
2020-04-17 02:53:23 +02:00
|
|
|
|
|i| formula_precedence_2(i, d, v),
|
2020-02-25 15:36:34 +01:00
|
|
|
|
),
|
|
|
|
|
|arguments| -> Result<_, (_, _)>
|
|
|
|
|
{
|
|
|
|
|
if arguments.len() >= 2
|
|
|
|
|
{
|
|
|
|
|
Ok(arguments.into_iter().collect())
|
|
|
|
|
}
|
|
|
|
|
else
|
|
|
|
|
{
|
2020-04-17 18:22:50 +02:00
|
|
|
|
// TODO: return more appropriate error type
|
2020-02-25 15:36:34 +01:00
|
|
|
|
Err(nom::error::make_error(i, nom::error::ErrorKind::Many1))
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
)(i)
|
|
|
|
|
}
|
|
|
|
|
|
2020-04-17 04:06:22 +02:00
|
|
|
|
fn or<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
|
2020-04-17 02:53:23 +02:00
|
|
|
|
-> IResult<&'i str, crate::Formulas>
|
2020-04-17 04:06:22 +02:00
|
|
|
|
where
|
|
|
|
|
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
|
2020-02-25 15:36:34 +01:00
|
|
|
|
{
|
|
|
|
|
map_res
|
|
|
|
|
(
|
2020-04-17 18:22:50 +02:00
|
|
|
|
separated_list1
|
2020-02-25 15:36:34 +01:00
|
|
|
|
(
|
|
|
|
|
delimited
|
|
|
|
|
(
|
|
|
|
|
multispace0,
|
|
|
|
|
terminated
|
|
|
|
|
(
|
|
|
|
|
tag("or"),
|
|
|
|
|
word_boundary,
|
|
|
|
|
),
|
|
|
|
|
multispace0,
|
|
|
|
|
),
|
2020-04-17 02:53:23 +02:00
|
|
|
|
|i| formula_precedence_3(i, d, v),
|
2020-02-25 15:36:34 +01:00
|
|
|
|
),
|
|
|
|
|
|arguments| -> Result<_, (_, _)>
|
|
|
|
|
{
|
|
|
|
|
if arguments.len() >= 2
|
|
|
|
|
{
|
|
|
|
|
Ok(arguments.into_iter().collect())
|
|
|
|
|
}
|
|
|
|
|
else
|
|
|
|
|
{
|
2020-04-17 18:22:50 +02:00
|
|
|
|
// TODO: return more appropriate error type
|
2020-02-25 15:36:34 +01:00
|
|
|
|
Err(nom::error::make_error(i, nom::error::ErrorKind::Many1))
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
)(i)
|
|
|
|
|
}
|
|
|
|
|
|
2020-04-17 04:06:22 +02:00
|
|
|
|
fn implies_left_to_right<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
|
2020-04-17 02:53:23 +02:00
|
|
|
|
-> IResult<&'i str, crate::Formula>
|
2020-04-17 04:06:22 +02:00
|
|
|
|
where
|
|
|
|
|
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
|
2020-02-25 15:36:34 +01:00
|
|
|
|
{
|
|
|
|
|
map
|
|
|
|
|
(
|
|
|
|
|
pair
|
|
|
|
|
(
|
|
|
|
|
many1
|
|
|
|
|
(
|
|
|
|
|
terminated
|
|
|
|
|
(
|
2020-04-17 02:53:23 +02:00
|
|
|
|
|i| formula_precedence_4(i, d, v),
|
2020-02-25 15:36:34 +01:00
|
|
|
|
delimited
|
|
|
|
|
(
|
|
|
|
|
multispace0,
|
|
|
|
|
tag("->"),
|
|
|
|
|
multispace0,
|
|
|
|
|
),
|
|
|
|
|
)
|
|
|
|
|
),
|
2020-04-17 02:53:23 +02:00
|
|
|
|
|i| formula_precedence_4(i, d, v),
|
2020-02-25 15:36:34 +01:00
|
|
|
|
),
|
|
|
|
|
|(arguments, last_argument)| arguments.into_iter().rev().fold(last_argument,
|
|
|
|
|
|accumulator, argument|
|
|
|
|
|
crate::Formula::implies(crate::ImplicationDirection::LeftToRight,
|
|
|
|
|
Box::new(argument), Box::new(accumulator)))
|
|
|
|
|
)(i)
|
|
|
|
|
}
|
|
|
|
|
|
2020-04-17 04:06:22 +02:00
|
|
|
|
fn implies_right_to_left<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
|
2020-04-17 02:53:23 +02:00
|
|
|
|
-> IResult<&'i str, crate::Formula>
|
2020-04-17 04:06:22 +02:00
|
|
|
|
where
|
|
|
|
|
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
|
2020-02-25 15:36:34 +01:00
|
|
|
|
{
|
|
|
|
|
map
|
|
|
|
|
(
|
|
|
|
|
pair
|
|
|
|
|
(
|
2020-04-17 02:53:23 +02:00
|
|
|
|
|i| formula_precedence_4(i, d, v),
|
2020-02-25 15:36:34 +01:00
|
|
|
|
many1
|
|
|
|
|
(
|
|
|
|
|
preceded
|
|
|
|
|
(
|
|
|
|
|
delimited
|
|
|
|
|
(
|
|
|
|
|
multispace0,
|
|
|
|
|
tag("<-"),
|
|
|
|
|
multispace0,
|
|
|
|
|
),
|
2020-04-17 02:53:23 +02:00
|
|
|
|
|i| formula_precedence_4(i, d, v),
|
2020-02-25 15:36:34 +01:00
|
|
|
|
)
|
|
|
|
|
),
|
|
|
|
|
),
|
|
|
|
|
|(first_argument, arguments)| arguments.into_iter().fold(first_argument,
|
|
|
|
|
|accumulator, argument|
|
|
|
|
|
crate::Formula::implies(crate::ImplicationDirection::RightToLeft,
|
|
|
|
|
Box::new(argument), Box::new(accumulator)))
|
|
|
|
|
)(i)
|
|
|
|
|
}
|
|
|
|
|
|
2020-04-17 04:06:22 +02:00
|
|
|
|
fn if_and_only_if<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
|
2020-04-17 02:53:23 +02:00
|
|
|
|
-> IResult<&'i str, crate::Formulas>
|
2020-04-17 04:06:22 +02:00
|
|
|
|
where
|
|
|
|
|
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
|
2020-02-25 15:36:34 +01:00
|
|
|
|
{
|
|
|
|
|
map_res
|
|
|
|
|
(
|
2020-04-17 18:22:50 +02:00
|
|
|
|
separated_list1
|
2020-02-25 15:36:34 +01:00
|
|
|
|
(
|
|
|
|
|
delimited
|
|
|
|
|
(
|
|
|
|
|
multispace0,
|
|
|
|
|
tag("<->"),
|
|
|
|
|
multispace0,
|
|
|
|
|
),
|
2020-04-17 02:53:23 +02:00
|
|
|
|
|i| formula_precedence_5(i, d, v),
|
2020-02-25 15:36:34 +01:00
|
|
|
|
),
|
|
|
|
|
|arguments| -> Result<_, (_, _)>
|
|
|
|
|
{
|
|
|
|
|
if arguments.len() >= 2
|
|
|
|
|
{
|
|
|
|
|
Ok(arguments.into_iter().collect())
|
|
|
|
|
}
|
|
|
|
|
else
|
|
|
|
|
{
|
2020-04-17 18:22:50 +02:00
|
|
|
|
// TODO: return more appropriate error type
|
2020-02-25 15:36:34 +01:00
|
|
|
|
Err(nom::error::make_error(i, nom::error::ErrorKind::Many1))
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
)(i)
|
|
|
|
|
}
|
|
|
|
|
|
2020-04-17 04:06:22 +02:00
|
|
|
|
fn quantified_formula<'i, 'b, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer,
|
|
|
|
|
keyword: &'b str)
|
2020-04-17 02:53:23 +02:00
|
|
|
|
-> IResult<&'i str, crate::QuantifiedFormula>
|
2020-04-17 04:06:22 +02:00
|
|
|
|
where
|
|
|
|
|
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
|
2020-02-25 15:36:34 +01:00
|
|
|
|
{
|
|
|
|
|
preceded
|
|
|
|
|
(
|
|
|
|
|
terminated
|
|
|
|
|
(
|
|
|
|
|
tag(keyword),
|
|
|
|
|
word_boundary,
|
|
|
|
|
),
|
|
|
|
|
cut
|
|
|
|
|
(
|
|
|
|
|
|i|
|
|
|
|
|
{
|
|
|
|
|
let (i, variable_declarations) =
|
|
|
|
|
map
|
|
|
|
|
(
|
|
|
|
|
delimited
|
|
|
|
|
(
|
|
|
|
|
multispace0,
|
2020-04-17 18:22:50 +02:00
|
|
|
|
separated_list1
|
2020-02-25 15:36:34 +01:00
|
|
|
|
(
|
|
|
|
|
delimited
|
|
|
|
|
(
|
|
|
|
|
multispace0,
|
|
|
|
|
tag(","),
|
|
|
|
|
multispace0,
|
|
|
|
|
),
|
|
|
|
|
map
|
|
|
|
|
(
|
|
|
|
|
crate::parse::terms::variable_declaration,
|
|
|
|
|
std::rc::Rc::new,
|
|
|
|
|
),
|
|
|
|
|
),
|
|
|
|
|
multispace0,
|
|
|
|
|
),
|
|
|
|
|
std::rc::Rc::new,
|
|
|
|
|
)(i)?;
|
|
|
|
|
|
2020-04-17 18:22:50 +02:00
|
|
|
|
let bound_variable_declarations = crate::VariableDeclarationStackLayer::bound(v,
|
2020-04-17 03:30:32 +02:00
|
|
|
|
std::rc::Rc::clone(&variable_declarations));
|
2020-02-25 15:36:34 +01:00
|
|
|
|
|
2020-04-20 02:57:32 +02:00
|
|
|
|
let (i, argument) = formula_precedence_2(i, d, &bound_variable_declarations)?;
|
2020-02-25 15:36:34 +01:00
|
|
|
|
|
|
|
|
|
Ok((i, crate::QuantifiedFormula::new(variable_declarations, Box::new(argument))))
|
|
|
|
|
}
|
|
|
|
|
),
|
|
|
|
|
)(i)
|
|
|
|
|
}
|
|
|
|
|
|
2020-04-17 04:06:22 +02:00
|
|
|
|
fn compare<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
|
2020-04-17 02:53:23 +02:00
|
|
|
|
-> IResult<&'i str, crate::Compare>
|
2020-04-17 04:06:22 +02:00
|
|
|
|
where
|
|
|
|
|
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
|
2020-02-25 15:36:34 +01:00
|
|
|
|
{
|
|
|
|
|
map
|
|
|
|
|
(
|
|
|
|
|
tuple
|
|
|
|
|
((
|
2020-04-17 02:53:23 +02:00
|
|
|
|
|i| crate::parse::term(i, d, v),
|
2020-02-25 15:36:34 +01:00
|
|
|
|
delimited
|
|
|
|
|
(
|
|
|
|
|
multispace0,
|
2020-04-20 02:40:13 +02:00
|
|
|
|
terminated
|
|
|
|
|
(
|
|
|
|
|
alt
|
|
|
|
|
((
|
|
|
|
|
map
|
|
|
|
|
(
|
|
|
|
|
tag("<="),
|
|
|
|
|
|_| crate::ComparisonOperator::LessOrEqual,
|
|
|
|
|
),
|
|
|
|
|
map
|
|
|
|
|
(
|
|
|
|
|
tag(">="),
|
|
|
|
|
|_| crate::ComparisonOperator::GreaterOrEqual,
|
|
|
|
|
),
|
|
|
|
|
map
|
|
|
|
|
(
|
|
|
|
|
tag("<"),
|
|
|
|
|
|_| crate::ComparisonOperator::Less,
|
|
|
|
|
),
|
|
|
|
|
map
|
|
|
|
|
(
|
|
|
|
|
tag(">"),
|
|
|
|
|
|_| crate::ComparisonOperator::Greater,
|
|
|
|
|
),
|
|
|
|
|
map
|
|
|
|
|
(
|
|
|
|
|
tag("!="),
|
|
|
|
|
|_| crate::ComparisonOperator::NotEqual,
|
|
|
|
|
),
|
|
|
|
|
map
|
|
|
|
|
(
|
|
|
|
|
tag("="),
|
|
|
|
|
|_| crate::ComparisonOperator::Equal,
|
|
|
|
|
),
|
|
|
|
|
)),
|
|
|
|
|
peek(nom::combinator::not(tag("-"))),
|
|
|
|
|
),
|
2020-02-25 15:36:34 +01:00
|
|
|
|
multispace0,
|
|
|
|
|
),
|
2020-04-17 02:53:23 +02:00
|
|
|
|
|i| crate::parse::term(i, d, v),
|
2020-02-25 15:36:34 +01:00
|
|
|
|
)),
|
|
|
|
|
|(left, operator, right)|
|
|
|
|
|
{
|
|
|
|
|
crate::Compare::new(operator, Box::new(left), Box::new(right))
|
|
|
|
|
}
|
|
|
|
|
)(i)
|
|
|
|
|
}
|
|
|
|
|
|
2020-04-17 04:06:22 +02:00
|
|
|
|
fn exists<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
|
2020-04-17 02:53:23 +02:00
|
|
|
|
-> IResult<&'i str, crate::QuantifiedFormula>
|
2020-04-17 04:06:22 +02:00
|
|
|
|
where
|
|
|
|
|
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
|
2020-02-25 15:36:34 +01:00
|
|
|
|
{
|
2020-04-17 02:53:23 +02:00
|
|
|
|
quantified_formula(i, d, v, "exists")
|
2020-02-25 15:36:34 +01:00
|
|
|
|
}
|
|
|
|
|
|
2020-04-17 04:06:22 +02:00
|
|
|
|
fn for_all<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
|
2020-04-17 02:53:23 +02:00
|
|
|
|
-> IResult<&'i str, crate::QuantifiedFormula>
|
2020-04-17 04:06:22 +02:00
|
|
|
|
where
|
|
|
|
|
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
|
2020-02-25 15:36:34 +01:00
|
|
|
|
{
|
2020-04-17 02:53:23 +02:00
|
|
|
|
quantified_formula(i, d, v, "forall")
|
2020-02-25 15:36:34 +01:00
|
|
|
|
}
|
|
|
|
|
|
2020-04-17 04:06:22 +02:00
|
|
|
|
fn formula_parenthesized<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
|
2020-04-17 02:53:23 +02:00
|
|
|
|
-> IResult<&'i str, crate::Formula>
|
2020-04-17 04:06:22 +02:00
|
|
|
|
where
|
|
|
|
|
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
|
2020-02-25 15:36:34 +01:00
|
|
|
|
{
|
|
|
|
|
delimited
|
|
|
|
|
(
|
|
|
|
|
terminated
|
|
|
|
|
(
|
|
|
|
|
tag("("),
|
|
|
|
|
multispace0,
|
|
|
|
|
),
|
2020-04-17 02:53:23 +02:00
|
|
|
|
|i| formula(i, d, v),
|
2020-02-25 15:36:34 +01:00
|
|
|
|
preceded
|
|
|
|
|
(
|
|
|
|
|
multispace0,
|
|
|
|
|
tag(")"),
|
|
|
|
|
),
|
|
|
|
|
)(i)
|
|
|
|
|
}
|
|
|
|
|
|
2020-04-17 04:06:22 +02:00
|
|
|
|
fn formula_precedence_0<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
|
2020-04-17 02:53:23 +02:00
|
|
|
|
-> IResult<&'i str, crate::Formula>
|
2020-04-17 04:06:22 +02:00
|
|
|
|
where
|
|
|
|
|
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
|
2020-02-25 15:36:34 +01:00
|
|
|
|
{
|
|
|
|
|
alt
|
|
|
|
|
((
|
|
|
|
|
map
|
|
|
|
|
(
|
|
|
|
|
boolean,
|
|
|
|
|
crate::Formula::Boolean,
|
|
|
|
|
),
|
|
|
|
|
map
|
|
|
|
|
(
|
2020-04-20 02:40:13 +02:00
|
|
|
|
|i| compare(i, d, v),
|
|
|
|
|
crate::Formula::Compare,
|
2020-02-25 15:36:34 +01:00
|
|
|
|
),
|
|
|
|
|
map
|
|
|
|
|
(
|
2020-04-20 02:40:13 +02:00
|
|
|
|
|i| predicate(i, d, v),
|
|
|
|
|
crate::Formula::Predicate,
|
2020-02-25 15:36:34 +01:00
|
|
|
|
),
|
2020-04-17 02:53:23 +02:00
|
|
|
|
|i| formula_parenthesized(i, d, v),
|
2020-02-25 15:36:34 +01:00
|
|
|
|
))(i)
|
|
|
|
|
}
|
|
|
|
|
|
2020-04-17 04:06:22 +02:00
|
|
|
|
fn formula_precedence_1<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
|
2020-04-17 02:53:23 +02:00
|
|
|
|
-> IResult<&'i str, crate::Formula>
|
2020-04-17 04:06:22 +02:00
|
|
|
|
where
|
|
|
|
|
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
|
2020-02-25 15:36:34 +01:00
|
|
|
|
{
|
|
|
|
|
alt
|
|
|
|
|
((
|
|
|
|
|
map
|
|
|
|
|
(
|
2020-04-17 02:53:23 +02:00
|
|
|
|
|i| exists(i, d, v),
|
2020-02-25 15:36:34 +01:00
|
|
|
|
crate::Formula::Exists,
|
|
|
|
|
),
|
|
|
|
|
map
|
|
|
|
|
(
|
2020-04-17 02:53:23 +02:00
|
|
|
|
|i| for_all(i, d, v),
|
2020-02-25 15:36:34 +01:00
|
|
|
|
crate::Formula::ForAll,
|
|
|
|
|
),
|
2020-04-17 02:53:23 +02:00
|
|
|
|
|i| formula_precedence_0(i, d, v),
|
2020-02-25 15:36:34 +01:00
|
|
|
|
))(i)
|
|
|
|
|
}
|
|
|
|
|
|
2020-04-17 04:06:22 +02:00
|
|
|
|
fn formula_precedence_2<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
|
2020-04-17 02:53:23 +02:00
|
|
|
|
-> IResult<&'i str, crate::Formula>
|
2020-04-17 04:06:22 +02:00
|
|
|
|
where
|
|
|
|
|
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
|
2020-02-25 15:36:34 +01:00
|
|
|
|
{
|
|
|
|
|
alt
|
|
|
|
|
((
|
2020-04-17 02:53:23 +02:00
|
|
|
|
|i| not(i, d, v),
|
|
|
|
|
|i| formula_precedence_1(i, d, v),
|
2020-02-25 15:36:34 +01:00
|
|
|
|
))(i)
|
|
|
|
|
}
|
|
|
|
|
|
2020-04-17 04:06:22 +02:00
|
|
|
|
fn formula_precedence_3<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
|
2020-04-17 02:53:23 +02:00
|
|
|
|
-> IResult<&'i str, crate::Formula>
|
2020-04-17 04:06:22 +02:00
|
|
|
|
where
|
|
|
|
|
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
|
2020-02-25 15:36:34 +01:00
|
|
|
|
{
|
|
|
|
|
alt
|
|
|
|
|
((
|
|
|
|
|
map
|
|
|
|
|
(
|
2020-04-17 02:53:23 +02:00
|
|
|
|
|i| and(i, d, v),
|
2020-02-25 15:36:34 +01:00
|
|
|
|
crate::Formula::And,
|
|
|
|
|
),
|
2020-04-17 02:53:23 +02:00
|
|
|
|
|i| formula_precedence_2(i, d, v),
|
2020-02-25 15:36:34 +01:00
|
|
|
|
))(i)
|
|
|
|
|
}
|
|
|
|
|
|
2020-04-17 04:06:22 +02:00
|
|
|
|
fn formula_precedence_4<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
|
2020-04-17 02:53:23 +02:00
|
|
|
|
-> IResult<&'i str, crate::Formula>
|
2020-04-17 04:06:22 +02:00
|
|
|
|
where
|
|
|
|
|
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
|
2020-02-25 15:36:34 +01:00
|
|
|
|
{
|
|
|
|
|
alt
|
|
|
|
|
((
|
|
|
|
|
map
|
|
|
|
|
(
|
2020-04-17 02:53:23 +02:00
|
|
|
|
|i| or(i, d, v),
|
2020-02-25 15:36:34 +01:00
|
|
|
|
crate::Formula::Or,
|
|
|
|
|
),
|
2020-04-17 02:53:23 +02:00
|
|
|
|
|i| formula_precedence_3(i, d, v),
|
2020-02-25 15:36:34 +01:00
|
|
|
|
))(i)
|
|
|
|
|
}
|
|
|
|
|
|
2020-04-17 04:06:22 +02:00
|
|
|
|
fn formula_precedence_5<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
|
2020-04-17 02:53:23 +02:00
|
|
|
|
-> IResult<&'i str, crate::Formula>
|
2020-04-17 04:06:22 +02:00
|
|
|
|
where
|
|
|
|
|
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
|
2020-02-25 15:36:34 +01:00
|
|
|
|
{
|
|
|
|
|
alt
|
|
|
|
|
((
|
2020-04-17 02:53:23 +02:00
|
|
|
|
|i| implies_left_to_right(i, d, v),
|
|
|
|
|
|i| implies_right_to_left(i, d, v),
|
|
|
|
|
|i| formula_precedence_4(i, d, v),
|
2020-02-25 15:36:34 +01:00
|
|
|
|
))(i)
|
|
|
|
|
}
|
|
|
|
|
|
2020-04-17 04:06:22 +02:00
|
|
|
|
fn formula_precedence_6<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
|
2020-04-17 02:53:23 +02:00
|
|
|
|
-> IResult<&'i str, crate::Formula>
|
2020-04-17 04:06:22 +02:00
|
|
|
|
where
|
|
|
|
|
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
|
2020-02-25 15:36:34 +01:00
|
|
|
|
{
|
|
|
|
|
alt
|
|
|
|
|
((
|
|
|
|
|
map
|
|
|
|
|
(
|
2020-04-17 02:53:23 +02:00
|
|
|
|
|i| if_and_only_if(i, d, v),
|
2020-02-25 15:36:34 +01:00
|
|
|
|
crate::Formula::IfAndOnlyIf,
|
|
|
|
|
),
|
2020-04-17 02:53:23 +02:00
|
|
|
|
|i| formula_precedence_5(i, d, v),
|
2020-02-25 15:36:34 +01:00
|
|
|
|
))(i)
|
|
|
|
|
}
|
|
|
|
|
|
2020-04-17 04:06:22 +02:00
|
|
|
|
pub fn formula<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
|
2020-04-17 02:53:23 +02:00
|
|
|
|
-> IResult<&'i str, crate::Formula>
|
2020-04-17 04:06:22 +02:00
|
|
|
|
where
|
|
|
|
|
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
|
2020-02-25 15:36:34 +01:00
|
|
|
|
{
|
2020-04-17 02:53:23 +02:00
|
|
|
|
formula_precedence_6(i, d, v)
|
2020-02-25 15:36:34 +01:00
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[cfg(test)]
|
|
|
|
|
mod tests
|
|
|
|
|
{
|
2020-04-17 02:53:23 +02:00
|
|
|
|
use crate::{Formula, ImplicationDirection, Term, VariableDeclarationStackLayer};
|
2020-04-17 04:06:22 +02:00
|
|
|
|
use crate::parse::formulas as original;
|
|
|
|
|
use crate::utils::*;
|
2020-02-25 15:36:34 +01:00
|
|
|
|
|
|
|
|
|
fn formula(i: &str) -> Formula
|
|
|
|
|
{
|
2020-04-17 02:53:23 +02:00
|
|
|
|
original::formula(i, &Declarations::new(), &VariableDeclarationStackLayer::free())
|
|
|
|
|
.unwrap().1
|
2020-02-25 15:36:34 +01:00
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
fn formula_remainder(i: &str) -> &str
|
|
|
|
|
{
|
2020-04-17 02:53:23 +02:00
|
|
|
|
original::formula(i, &Declarations::new(), &VariableDeclarationStackLayer::free())
|
|
|
|
|
.unwrap().0
|
2020-02-25 15:36:34 +01:00
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
fn format_formula(i: &str) -> String
|
|
|
|
|
{
|
|
|
|
|
format!("{}", formula(i))
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[test]
|
|
|
|
|
fn parse_boolean()
|
|
|
|
|
{
|
|
|
|
|
assert_eq!(formula("true"), Formula::true_());
|
|
|
|
|
assert_eq!(formula("false"), Formula::false_());
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[test]
|
|
|
|
|
fn parse_precedence()
|
|
|
|
|
{
|
|
|
|
|
assert_eq!(format_formula("a -> b -> c <-> d -> e -> f"), "a -> b -> c <-> d -> e -> f");
|
|
|
|
|
assert_eq!(format_formula("(a -> b -> c) <-> (d -> e -> f)"), "a -> b -> c <-> d -> e -> f");
|
|
|
|
|
assert_eq!(format_formula("a <- b <- c <-> d <- e <- f"), "a <- b <- c <-> d <- e <- f");
|
|
|
|
|
assert_eq!(format_formula("(a <- b <- c) <-> (d <- e <- f)"), "a <- b <- c <-> d <- e <- f");
|
|
|
|
|
}
|
|
|
|
|
|
2020-04-20 02:40:13 +02:00
|
|
|
|
#[test]
|
|
|
|
|
fn parse_compare()
|
|
|
|
|
{
|
2020-04-20 02:51:46 +02:00
|
|
|
|
assert_eq!(format_formula("X>=0."), "X >= 0");
|
|
|
|
|
assert_eq!(format_formula("N>=0."), "N >= 0");
|
|
|
|
|
assert_eq!(format_formula("n<0."), "n < 0");
|
|
|
|
|
assert_eq!(format_formula("n>=0."), "n >= 0");
|
|
|
|
|
assert_eq!(format_formula("p(0)>=q."), "p(0) >= q");
|
2020-04-20 02:40:13 +02:00
|
|
|
|
}
|
|
|
|
|
|
2020-02-25 15:36:34 +01:00
|
|
|
|
#[test]
|
|
|
|
|
fn parse_exists()
|
|
|
|
|
{
|
|
|
|
|
let formula_as_exists = |i| match formula(i)
|
|
|
|
|
{
|
|
|
|
|
Formula::Exists(exists) => exists,
|
|
|
|
|
_ => panic!("expected existentially quantified formula"),
|
|
|
|
|
};
|
|
|
|
|
|
|
|
|
|
let as_predicate = |x| match x
|
|
|
|
|
{
|
|
|
|
|
Formula::Predicate(arguments) => arguments,
|
|
|
|
|
_ => panic!("expected predicate"),
|
|
|
|
|
};
|
|
|
|
|
|
|
|
|
|
assert_eq!(format_formula("exists X , Y , Z ( p )"), "exists X, Y, Z p");
|
|
|
|
|
assert_eq!(formula_as_exists("exists X , Y , Z ( p )").parameters.len(), 3);
|
|
|
|
|
assert_eq!(as_predicate(*formula_as_exists("exists X , Y , Z ( p )").argument)
|
|
|
|
|
.declaration.name, "p");
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[test]
|
|
|
|
|
fn parse_and()
|
|
|
|
|
{
|
|
|
|
|
let formula_as_and = |i| match formula(i)
|
|
|
|
|
{
|
|
|
|
|
Formula::And(arguments) => arguments,
|
|
|
|
|
_ => panic!("expected conjunction"),
|
|
|
|
|
};
|
|
|
|
|
|
|
|
|
|
let as_predicate = |x| match x
|
|
|
|
|
{
|
|
|
|
|
Formula::Predicate(arguments) => arguments,
|
|
|
|
|
_ => panic!("expected predicate"),
|
|
|
|
|
};
|
|
|
|
|
|
|
|
|
|
assert_eq!(format_formula("(true and false)"), "true and false");
|
|
|
|
|
assert_eq!(formula_as_and("(true and false)").len(), 2);
|
|
|
|
|
assert_eq!(formula_as_and("(true and false)").remove(0), Formula::true_());
|
|
|
|
|
assert_eq!(formula_as_and("(true and false)").remove(1), Formula::false_());
|
|
|
|
|
// The order of elements is retained
|
|
|
|
|
assert_ne!(formula("(true and false)"), formula("false and true"));
|
|
|
|
|
assert_eq!(format_formula("(p and q and r and s)"), "p and q and r and s");
|
|
|
|
|
assert_eq!(
|
|
|
|
|
as_predicate(formula_as_and("(p and q and r and s)").remove(0)).declaration.name, "p");
|
|
|
|
|
assert_eq!(
|
|
|
|
|
as_predicate(formula_as_and("(p and q and r and s)").remove(3)).declaration.name, "s");
|
|
|
|
|
|
2020-04-17 02:53:23 +02:00
|
|
|
|
let formula = |i| original::formula(i, &Declarations::new(),
|
|
|
|
|
&VariableDeclarationStackLayer::free());
|
2020-02-25 15:36:34 +01:00
|
|
|
|
|
|
|
|
|
// Malformed formulas shouldn’t be accepted
|
|
|
|
|
assert!(formula("and").is_err());
|
|
|
|
|
assert!(formula("and p").is_err());
|
|
|
|
|
assert_eq!(formula_remainder("p and"), " and");
|
|
|
|
|
assert_eq!(formula_remainder("p andq"), " andq");
|
|
|
|
|
assert_eq!(formula_remainder("p and q and"), " and");
|
|
|
|
|
assert_eq!(formula_remainder("p and q andq"), " andq");
|
|
|
|
|
assert!(formula("(p and) q").is_err());
|
|
|
|
|
assert_eq!(formula_remainder("p (and q)"), " (and q)");
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[test]
|
|
|
|
|
fn parse_or()
|
|
|
|
|
{
|
|
|
|
|
let formula_as_or = |i| match formula(i)
|
|
|
|
|
{
|
|
|
|
|
Formula::Or(arguments) => arguments,
|
|
|
|
|
_ => panic!("expected disjunction"),
|
|
|
|
|
};
|
|
|
|
|
|
|
|
|
|
let as_predicate = |x| match x
|
|
|
|
|
{
|
|
|
|
|
Formula::Predicate(arguments) => arguments,
|
|
|
|
|
_ => panic!("expected predicate"),
|
|
|
|
|
};
|
|
|
|
|
|
|
|
|
|
assert_eq!(format_formula("(true or false)"), "true or false");
|
|
|
|
|
assert_eq!(formula_as_or("(true or false)").len(), 2);
|
|
|
|
|
assert_eq!(formula_as_or("(true or false)").remove(0), Formula::true_());
|
|
|
|
|
assert_eq!(formula_as_or("(true or false)").remove(1), Formula::false_());
|
|
|
|
|
// The order of elements is retained
|
|
|
|
|
assert_ne!(formula("(true or false)"), formula("false or true)"));
|
|
|
|
|
assert_eq!(format_formula("(p or q or r or s)"), "p or q or r or s");
|
|
|
|
|
assert_eq!(
|
|
|
|
|
as_predicate(formula_as_or("(p or q or r or s)").remove(0)).declaration.name, "p");
|
|
|
|
|
assert_eq!(
|
|
|
|
|
as_predicate(formula_as_or("(p or q or r or s)").remove(3)).declaration.name, "s");
|
|
|
|
|
|
2020-04-17 02:53:23 +02:00
|
|
|
|
let formula = |i| original::formula(i, &Declarations::new(),
|
|
|
|
|
&VariableDeclarationStackLayer::free());
|
2020-02-25 15:36:34 +01:00
|
|
|
|
|
|
|
|
|
// Malformed formulas shouldn’t be accepted
|
|
|
|
|
assert!(formula("or").is_err());
|
|
|
|
|
assert!(formula("or p").is_err());
|
|
|
|
|
assert_eq!(formula_remainder("p or"), " or");
|
|
|
|
|
assert_eq!(formula_remainder("p orq"), " orq");
|
|
|
|
|
assert_eq!(formula_remainder("p or q or"), " or");
|
|
|
|
|
assert_eq!(formula_remainder("p or q orq"), " orq");
|
|
|
|
|
assert!(formula("(p or) q").is_err());
|
|
|
|
|
assert_eq!(formula_remainder("p (or q)"), " (or q)");
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[test]
|
|
|
|
|
fn parse_implies()
|
|
|
|
|
{
|
|
|
|
|
let formula_as_implies = |i| match formula(i)
|
|
|
|
|
{
|
|
|
|
|
Formula::Implies(implies) => implies,
|
|
|
|
|
_ => panic!("expected implication"),
|
|
|
|
|
};
|
|
|
|
|
|
|
|
|
|
let as_predicate = |x| match x
|
|
|
|
|
{
|
|
|
|
|
Formula::Predicate(arguments) => arguments,
|
|
|
|
|
_ => panic!("expected predicate"),
|
|
|
|
|
};
|
|
|
|
|
|
|
|
|
|
assert_eq!(as_predicate(*formula_as_implies("a -> b").antecedent).declaration.name, "a");
|
|
|
|
|
assert_eq!(as_predicate(*formula_as_implies("a -> b").implication).declaration.name, "b");
|
2020-04-17 02:53:23 +02:00
|
|
|
|
assert_eq!(formula_as_implies("a -> b").direction, ImplicationDirection::LeftToRight);
|
2020-02-25 15:36:34 +01:00
|
|
|
|
|
|
|
|
|
assert_eq!(as_predicate(*formula_as_implies("a <- b").antecedent).declaration.name, "b");
|
|
|
|
|
assert_eq!(as_predicate(*formula_as_implies("a <- b").implication).declaration.name, "a");
|
2020-04-17 02:53:23 +02:00
|
|
|
|
assert_eq!(formula_as_implies("a <- b").direction, ImplicationDirection::RightToLeft);
|
2020-02-25 15:36:34 +01:00
|
|
|
|
|
|
|
|
|
assert_eq!(format_formula("(a -> b -> c)"), "a -> b -> c");
|
|
|
|
|
assert_eq!(format_formula("(a -> (b -> c))"), "a -> b -> c");
|
|
|
|
|
assert_eq!(format_formula("((a -> b) -> c)"), "(a -> b) -> c");
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[test]
|
|
|
|
|
fn parse_predicate()
|
|
|
|
|
{
|
2020-04-17 02:53:23 +02:00
|
|
|
|
let predicate = |i| original::predicate(i, &Declarations::new(),
|
|
|
|
|
&VariableDeclarationStackLayer::free()).unwrap().1;
|
|
|
|
|
let predicate_remainder = |i| original::predicate(i, &Declarations::new(),
|
|
|
|
|
&VariableDeclarationStackLayer::free()).unwrap().0;
|
2020-02-25 15:36:34 +01:00
|
|
|
|
|
|
|
|
|
assert_eq!(predicate("s").declaration.name, "s");
|
|
|
|
|
assert_eq!(predicate("s").declaration.arity, 0);
|
|
|
|
|
assert_eq!(predicate_remainder("s"), "");
|
|
|
|
|
assert_eq!(predicate("s ( )").declaration.name, "s");
|
|
|
|
|
assert_eq!(predicate("s ( )").declaration.arity, 0);
|
|
|
|
|
assert_eq!(predicate_remainder("s ( )"), "");
|
|
|
|
|
assert_eq!(predicate("s ( 1 , 2 , 3 )").declaration.name, "s");
|
|
|
|
|
assert_eq!(predicate("s ( 1 , 2 , 3 )").declaration.arity, 3);
|
|
|
|
|
assert_eq!(predicate("s ( 1 , 2 , 3 )").arguments.remove(0), Term::integer(1));
|
|
|
|
|
assert_eq!(predicate("s ( 1 , 2 , 3 )").arguments.remove(1), Term::integer(2));
|
|
|
|
|
assert_eq!(predicate("s ( 1 , 2 , 3 )").arguments.remove(2), Term::integer(3));
|
|
|
|
|
assert_eq!(predicate_remainder("s ( 1 , 2 , 3 )"), "");
|
|
|
|
|
assert_eq!(predicate_remainder("s ( 1 , 2 , 3 )"), "");
|
|
|
|
|
assert_eq!(predicate("s ( ), rest").declaration.name, "s");
|
|
|
|
|
assert_eq!(predicate("s ( ), rest").declaration.arity, 0);
|
|
|
|
|
assert_eq!(predicate_remainder("s ( ), rest"), ", rest");
|
|
|
|
|
assert_eq!(predicate("s ( 1 , 2 , 3 ), rest").declaration.name, "s");
|
|
|
|
|
assert_eq!(predicate("s ( 1 , 2 , 3 ), rest").declaration.arity, 3);
|
|
|
|
|
assert_eq!(predicate_remainder("s ( 1 , 2 , 3 ), rest"), ", rest");
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[test]
|
|
|
|
|
fn parse_exists_primitive()
|
|
|
|
|
{
|
2020-04-17 02:53:23 +02:00
|
|
|
|
let exists = |i| original::exists(i, &Declarations::new(),
|
|
|
|
|
&VariableDeclarationStackLayer::free());
|
|
|
|
|
|
|
|
|
|
assert_eq!(exists("exists X (p(X, Y, X, Y)), rest")
|
2020-02-25 15:36:34 +01:00
|
|
|
|
.map(|(i, x)| (i, x.parameters.len())),
|
|
|
|
|
Ok((", rest", 1)));
|
2020-04-17 02:53:23 +02:00
|
|
|
|
assert_eq!(exists("exists X p(X, Y, X, Y), rest")
|
2020-02-25 15:36:34 +01:00
|
|
|
|
.map(|(i, x)| (i, x.parameters.len())),
|
|
|
|
|
Ok((", rest", 1)));
|
2020-04-17 02:53:23 +02:00
|
|
|
|
assert!(exists("exists (p(X, Y, X, Y)), rest").is_err());
|
|
|
|
|
assert!(exists("exists X, rest").is_err());
|
|
|
|
|
assert!(exists("exists X (), rest").is_err());
|
|
|
|
|
assert!(exists("exists X (, true), rest").is_err());
|
|
|
|
|
assert!(exists("exists X (true, ), rest").is_err());
|
|
|
|
|
assert!(exists("exists X (true false), rest").is_err());
|
|
|
|
|
assert!(exists("exists X (true), rest").is_ok());
|
|
|
|
|
assert!(exists("exists X p(X), rest").is_ok());
|
2020-02-25 15:36:34 +01:00
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[test]
|
|
|
|
|
fn parse_formula()
|
|
|
|
|
{
|
|
|
|
|
// TODO: refactor
|
|
|
|
|
formula("exists X, Y (p(X, Y, X, Y) and X < Y and q(X) <-> r(X)), rest");
|
|
|
|
|
}
|
|
|
|
|
}
|