use nom::branch::alt;
use nom::character::complete::multispace1;
use nom::combinator::map;
use nom::sequence::{preceded, tuple};
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", tuple((parse_gd, preceded(multispace1, parse_gd)))),
GoalDefinition::new_imply_tuple,
);
let exists = map(
prefix_expr(
"exists",
tuple((
parens(typed_list(parse_variable)),
preceded(multispace1, parse_gd),
)),
),
GoalDefinition::new_exists_tuple,
);
let forall = map(
prefix_expr(
"forall",
tuple((
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))(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, BinaryComp, BinaryOp, FComp, FExp, GoalDefinition, Parser, Term, TypedList,
Variable,
};
#[test]
fn test_parse() {
assert!(
GoalDefinition::parse("(= x y)").is_value(GoalDefinition::AtomicFormula(
AtomicFormula::new_equality(Term::Name("x".into()), Term::Name("y".into()))
))
);
assert!(
GoalDefinition::parse("(not (= x y))").is_value(GoalDefinition::new_not(
GoalDefinition::new_atomic_formula(AtomicFormula::new_equality(
Term::Name("x".into()),
Term::Name("y".into())
))
))
);
assert!(
GoalDefinition::parse("(and (not (= x y)) (= x z))").is_value(GoalDefinition::new_and(
[
GoalDefinition::new_not(GoalDefinition::new_atomic_formula(
AtomicFormula::new_equality(Term::Name("x".into()), Term::Name("y".into()))
)),
GoalDefinition::AtomicFormula(AtomicFormula::new_equality(
Term::Name("x".into()),
Term::Name("z".into())
))
]
))
);
assert!(
GoalDefinition::parse("(or (not (= x y)) (= x z))").is_value(GoalDefinition::new_or([
GoalDefinition::new_not(GoalDefinition::new_atomic_formula(
AtomicFormula::new_equality(Term::Name("x".into()), Term::Name("y".into()))
)),
GoalDefinition::AtomicFormula(AtomicFormula::new_equality(
Term::Name("x".into()),
Term::Name("z".into())
))
]))
);
assert!(
GoalDefinition::parse("(imply (not (= x y)) (= x z))").is_value(
GoalDefinition::new_imply(
GoalDefinition::new_not(GoalDefinition::new_atomic_formula(
AtomicFormula::new_equality(Term::Name("x".into()), Term::Name("y".into()))
)),
GoalDefinition::AtomicFormula(AtomicFormula::new_equality(
Term::Name("x".into()),
Term::Name("z".into())
))
)
)
);
assert!(
GoalDefinition::parse("(exists (?x ?y) (not (= ?x ?y)))").is_value(
GoalDefinition::new_exists(
TypedList::from_iter([
Variable::from_str("x").into(),
Variable::from_str("y").into()
]),
GoalDefinition::new_not(GoalDefinition::new_atomic_formula(
AtomicFormula::new_equality(
Term::Variable("x".into()),
Term::Variable("y".into())
)
))
)
)
);
assert!(
GoalDefinition::parse("(forall (?x ?y) (not (= ?x ?y)))").is_value(
GoalDefinition::new_forall(
TypedList::from_iter([
Variable::from_str("x").into(),
Variable::from_str("y").into()
]),
GoalDefinition::new_not(GoalDefinition::new_atomic_formula(
AtomicFormula::new_equality(
Term::Variable("x".into()),
Term::Variable("y".into())
)
))
)
)
);
assert!(
GoalDefinition::parse("(= (+ 1.23 2.34) (+ 1.23 2.34))").is_value(
GoalDefinition::new_f_comp(FComp::new(
BinaryComp::Equal,
FExp::new_binary_op(
BinaryOp::Addition,
FExp::new_number(1.23),
FExp::new_number(2.34),
),
FExp::new_binary_op(
BinaryOp::Addition,
FExp::new_number(1.23),
FExp::new_number(2.34),
)
))
)
);
}
}