use crate::parsers::{
parens, parse_con_gd, parse_pref_name, parse_variable, prefix_expr, space_separated_list0,
typed_list, ParseResult, Span,
};
use crate::PrefConGDs;
use nom::branch::alt;
use nom::character::complete::multispace1;
use nom::combinator::map;
use nom::sequence::{preceded, tuple};
pub fn parse_pref_con_gd<'a, T: Into<Span<'a>>>(input: T) -> ParseResult<'a, PrefConGDs> {
let and = map(
prefix_expr("and", space_separated_list0(parse_pref_con_gd)),
|x| PrefConGDs::from_iter(x.into_iter().flatten()),
);
let forall = map(
prefix_expr(
"forall",
tuple((
parens(typed_list(parse_variable)),
preceded(multispace1, parse_pref_con_gd),
)),
),
|(vars, gd)| PrefConGDs::new_forall(vars, gd),
);
let named_preference = map(
prefix_expr(
"preference",
tuple((parse_pref_name, preceded(multispace1, parse_con_gd))),
),
|(name, gd)| PrefConGDs::new_preference(Some(name), gd),
);
let unnamed_preference = map(prefix_expr("preference", parse_con_gd), |gd| {
PrefConGDs::new_preference(None, gd)
});
let goal = map(parse_con_gd, PrefConGDs::new_goal);
alt((and, forall, named_preference, unnamed_preference, goal))(input.into())
}
impl crate::parsers::Parser for PrefConGDs {
type Item = PrefConGDs;
fn parse<'a, S: Into<Span<'a>>>(input: S) -> ParseResult<'a, Self::Item> {
parse_pref_con_gd(input)
}
}
#[cfg(test)]
mod tests {
use crate::parsers::preamble::*;
use crate::{
AtomicFormula, Con2GD, ConGD, GoalDefinition, PrefConGD, PrefConGDs, Term, ToTyped, Type,
TypedList, Variable,
};
#[test]
fn test_parse() {
let gd_a = GoalDefinition::new_atomic_formula(AtomicFormula::new_equality(
Term::Name("x".into()),
Term::Name("y".into()),
));
let gd_b = GoalDefinition::new_not(GoalDefinition::new_atomic_formula(
AtomicFormula::new_equality(Term::Name("x".into()), Term::Name("z".into())),
));
assert!(PrefConGDs::parse("(and)").is_value(PrefConGDs::default()));
assert!(
PrefConGDs::parse("(and (at end (= x y)) (at end (not (= x z))))").is_value(
PrefConGDs::from_iter([
PrefConGD::new_goal(ConGD::new_at_end(gd_a.clone())),
PrefConGD::new_goal(ConGD::new_at_end(gd_b.clone())),
])
)
);
assert!(
PrefConGDs::parse("(forall (?x ?z) (sometime (= ?x ?z)))").is_value(
PrefConGDs::new_forall(
TypedList::from_iter([
Variable::from("x").to_typed(Type::OBJECT),
Variable::from("z").to_typed(Type::OBJECT),
]),
PrefConGDs::new_goal(ConGD::new_sometime(Con2GD::Goal(
GoalDefinition::new_atomic_formula(AtomicFormula::new_equality(
Term::Variable("x".into()),
Term::Variable("z".into())
))
)))
)
)
);
assert!(PrefConGDs::parse("(at end (= x y))")
.is_value(PrefConGDs::new_goal(ConGD::AtEnd(gd_a.clone()))));
assert!(PrefConGDs::parse("(preference (at end (= x y)))")
.is_value(PrefConGDs::new_preference(None, ConGD::AtEnd(gd_a.clone()))));
assert!(
PrefConGDs::parse("(preference name (at end (= x y)))").is_value(
PrefConGDs::new_preference(Some("name".into()), ConGD::AtEnd(gd_a.clone()))
)
);
}
}