use nom::branch::alt;
use nom::character::complete::multispace1;
use nom::combinator::map;
use nom::sequence::preceded;
use nom::Parser;
use crate::parsers::{
atomic_formula, literal, parse_f_comp, parse_term, parse_variable, ParseResult, Span,
};
use crate::parsers::{parens, prefix_expr, space_separated_list0, typed_list};
use crate::types::GoalDefinition;
pub fn parse_gd<'a, T: Into<Span<'a>>>(input: T) -> ParseResult<'a, GoalDefinition> {
let af = map(
atomic_formula(parse_term),
GoalDefinition::new_atomic_formula,
);
let literal = map(literal(parse_term), GoalDefinition::new_literal);
let and = map(
prefix_expr("and", space_separated_list0(parse_gd)),
GoalDefinition::new_and,
);
let or = map(
prefix_expr("or", space_separated_list0(parse_gd)),
GoalDefinition::new_or,
);
let not = map(prefix_expr("not", parse_gd), GoalDefinition::new_not);
let imply = map(
prefix_expr("imply", (parse_gd, preceded(multispace1, parse_gd))),
GoalDefinition::new_imply_tuple,
);
let exists = map(
prefix_expr(
"exists",
(
parens(typed_list(parse_variable)),
preceded(multispace1, parse_gd),
),
),
GoalDefinition::new_exists_tuple,
);
let forall = map(
prefix_expr(
"forall",
(
parens(typed_list(parse_variable)),
preceded(multispace1, parse_gd),
),
),
GoalDefinition::new_forall_tuple,
);
let f_comp = map(parse_f_comp, GoalDefinition::new_f_comp);
alt((and, or, not, imply, exists, forall, af, literal, f_comp)).parse(input.into())
}
impl crate::parsers::Parser for GoalDefinition {
type Item = GoalDefinition;
fn parse<'a, S: Into<Span<'a>>>(input: S) -> ParseResult<'a, Self::Item> {
parse_gd(input)
}
}
#[cfg(test)]
mod tests {
use crate::parsers::UnwrapValue;
use crate::{
AtomicFormula, BinaryComparison, BinaryOp, FluentComparison, FluentExpression,
GoalDefinition, Parser, Term, TypedList, Variable,
};
#[test]
fn test_parse() {
assert!(
GoalDefinition::parse("(= x y)").is_value(GoalDefinition::AtomicFormula(
AtomicFormula::equality(Term::Name("x".into()), Term::Name("y".into()))
))
);
assert!(
GoalDefinition::parse("(not (= x y))").is_value(GoalDefinition::not(
GoalDefinition::atomic_formula(AtomicFormula::equality(
Term::Name("x".into()),
Term::Name("y".into())
))
))
);
assert!(
GoalDefinition::parse("(and (not (= x y)) (= x z))").is_value(GoalDefinition::and([
GoalDefinition::not(GoalDefinition::atomic_formula(AtomicFormula::equality(
Term::Name("x".into()),
Term::Name("y".into())
))),
GoalDefinition::AtomicFormula(AtomicFormula::equality(
Term::Name("x".into()),
Term::Name("z".into())
))
]))
);
assert!(
GoalDefinition::parse("(or (not (= x y)) (= x z))").is_value(GoalDefinition::or([
GoalDefinition::not(GoalDefinition::atomic_formula(AtomicFormula::equality(
Term::Name("x".into()),
Term::Name("y".into())
))),
GoalDefinition::AtomicFormula(AtomicFormula::equality(
Term::Name("x".into()),
Term::Name("z".into())
))
]))
);
assert!(
GoalDefinition::parse("(imply (not (= x y)) (= x z))").is_value(GoalDefinition::imply(
GoalDefinition::not(GoalDefinition::atomic_formula(AtomicFormula::equality(
Term::Name("x".into()),
Term::Name("y".into())
))),
GoalDefinition::AtomicFormula(AtomicFormula::equality(
Term::Name("x".into()),
Term::Name("z".into())
))
))
);
assert!(
GoalDefinition::parse("(exists (?x ?y) (not (= ?x ?y)))").is_value(
GoalDefinition::exists(
TypedList::from_iter([
Variable::new_string("x").into(),
Variable::new_string("y").into()
]),
GoalDefinition::not(GoalDefinition::atomic_formula(AtomicFormula::equality(
Term::Variable("x".into()),
Term::Variable("y".into())
)))
)
)
);
assert!(
GoalDefinition::parse("(forall (?x ?y) (not (= ?x ?y)))").is_value(
GoalDefinition::forall(
TypedList::from_iter([
Variable::new_string("x").into(),
Variable::new_string("y").into()
]),
GoalDefinition::not(GoalDefinition::atomic_formula(AtomicFormula::equality(
Term::Variable("x".into()),
Term::Variable("y".into())
)))
)
)
);
assert!(
GoalDefinition::parse("(= (+ 1.23 2.34) (+ 1.23 2.34))").is_value(
GoalDefinition::fluent_comparison(FluentComparison::new(
BinaryComparison::Equal,
FluentExpression::binary_op(
BinaryOp::Addition,
FluentExpression::number(1.23),
FluentExpression::number(2.34),
),
FluentExpression::binary_op(
BinaryOp::Addition,
FluentExpression::number(1.23),
FluentExpression::number(2.34),
)
))
)
);
}
}