diff --git a/src/formatting/asp/default.rs b/src/formatting/asp/default.rs index b5bb0208..01e22753 100644 --- a/src/formatting/asp/default.rs +++ b/src/formatting/asp/default.rs @@ -4,7 +4,8 @@ use { syntax_tree::{ asp::{ Atom, AtomicFormula, BinaryOperator, Body, Comparison, Head, Literal, - PrecomputedTerm, Program, Relation, Rule, Sign, Term, UnaryOperator, Variable, + PrecomputedTerm, Predicate, Program, Relation, Rule, Sign, Term, UnaryOperator, + Variable, }, Node, }, @@ -106,9 +107,17 @@ impl Display for Format<'_, Term> { } } +impl Display for Format<'_, Predicate> { + fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result { + let symbol = &self.0.symbol; + let arity = &self.0.arity; + write!(f, "{symbol}/{arity}") + } +} + impl Display for Format<'_, Atom> { fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result { - let predicate = &self.0.predicate; + let predicate = &self.0.predicate_symbol; let terms = &self.0.terms; write!(f, "{predicate}")?; @@ -342,7 +351,7 @@ mod tests { fn format_atom() { assert_eq!( Format(&Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![], }) .to_string(), @@ -351,7 +360,7 @@ mod tests { assert_eq!( Format(&Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![Term::PrecomputedTerm(PrecomputedTerm::Numeral(1))], }) .to_string(), @@ -360,7 +369,7 @@ mod tests { assert_eq!( Format(&Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![ Term::PrecomputedTerm(PrecomputedTerm::Numeral(1)), Term::PrecomputedTerm(PrecomputedTerm::Numeral(2)) @@ -384,7 +393,7 @@ mod tests { Format(&Literal { sign: Sign::Negation, atom: Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![] } }) @@ -422,7 +431,7 @@ mod tests { Format(&AtomicFormula::Literal(Literal { sign: Sign::DoubleNegation, atom: Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![] } })) @@ -445,7 +454,7 @@ mod tests { fn format_head() { assert_eq!( Format(&Head::Basic(Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![] })) .to_string(), @@ -454,7 +463,7 @@ mod tests { assert_eq!( Format(&Head::Choice(Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![] })) .to_string(), @@ -474,7 +483,7 @@ mod tests { AtomicFormula::Literal(Literal { sign: Sign::NoSign, atom: Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![Term::Variable(Variable("X".into()))] } }), @@ -502,21 +511,21 @@ mod tests { rules: vec![ Rule { head: Head::Basic(Atom { - predicate: "a".into(), + predicate_symbol: "a".into(), terms: vec![] }), body: Body { formulas: vec![] } }, Rule { head: Head::Basic(Atom { - predicate: "b".into(), + predicate_symbol: "b".into(), terms: vec![] }), body: Body { formulas: vec![AtomicFormula::Literal(Literal { sign: Sign::Negation, atom: Atom { - predicate: "a".into(), + predicate_symbol: "a".into(), terms: vec![] } })] diff --git a/src/formatting/fol/default.rs b/src/formatting/fol/default.rs index a97b8f02..473e37aa 100644 --- a/src/formatting/fol/default.rs +++ b/src/formatting/fol/default.rs @@ -4,8 +4,8 @@ use { syntax_tree::{ fol::{ Atom, AtomicFormula, BasicIntegerTerm, BinaryConnective, BinaryOperator, - Comparison, Formula, GeneralTerm, Guard, IntegerTerm, Quantification, Quantifier, - Relation, Sort, Theory, UnaryConnective, UnaryOperator, Variable, + Comparison, Formula, GeneralTerm, Guard, IntegerTerm, Predicate, Quantification, + Quantifier, Relation, Sort, Theory, UnaryConnective, UnaryOperator, Variable, }, Node, }, @@ -101,9 +101,17 @@ impl Display for Format<'_, GeneralTerm> { } } +impl Display for Format<'_, Predicate> { + fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result { + let symbol = &self.0.symbol; + let arity = &self.0.arity; + write!(f, "{symbol}/{arity}") + } +} + impl Display for Format<'_, Atom> { fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result { - let predicate = &self.0.predicate; + let predicate = &self.0.predicate_symbol; let terms = &self.0.terms; write!(f, "{predicate}")?; @@ -445,7 +453,7 @@ mod tests { fn format_atomic_formula() { assert_eq!( Format(&AtomicFormula::Atom(Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![ GeneralTerm::Symbol("a".into()), GeneralTerm::IntegerTerm(IntegerTerm::BasicIntegerTerm( @@ -476,7 +484,7 @@ mod tests { fn format_formula() { assert_eq!( Format(&Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![] }))) .to_string(), @@ -487,7 +495,7 @@ mod tests { Format(&Formula::UnaryFormula { connective: UnaryConnective::Negation, formula: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![] })) .into() @@ -506,7 +514,7 @@ mod tests { }] }, formula: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![GeneralTerm::GeneralVariable("X".into())] })) .into() @@ -521,19 +529,19 @@ mod tests { lhs: Formula::BinaryFormula { connective: BinaryConnective::ReverseImplication, lhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![] })) .into(), rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "q".into(), + predicate_symbol: "q".into(), terms: vec![] })) .into() } .into(), rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "r".into(), + predicate_symbol: "r".into(), terms: vec![] })) .into(), @@ -546,19 +554,19 @@ mod tests { Format(&Formula::BinaryFormula { connective: BinaryConnective::ReverseImplication, lhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![] })) .into(), rhs: Formula::BinaryFormula { connective: BinaryConnective::ReverseImplication, lhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "q".into(), + predicate_symbol: "q".into(), terms: vec![] })) .into(), rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "r".into(), + predicate_symbol: "r".into(), terms: vec![] })) .into() @@ -575,19 +583,19 @@ mod tests { lhs: Formula::BinaryFormula { connective: BinaryConnective::Implication, lhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![] })) .into(), rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "q".into(), + predicate_symbol: "q".into(), terms: vec![] })) .into() } .into(), rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "r".into(), + predicate_symbol: "r".into(), terms: vec![] })) .into(), @@ -600,19 +608,19 @@ mod tests { Format(&Formula::BinaryFormula { connective: BinaryConnective::Implication, lhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![] })) .into(), rhs: Formula::BinaryFormula { connective: BinaryConnective::Implication, lhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "q".into(), + predicate_symbol: "q".into(), terms: vec![] })) .into(), rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "r".into(), + predicate_symbol: "r".into(), terms: vec![] })) .into() @@ -629,19 +637,19 @@ mod tests { lhs: Formula::BinaryFormula { connective: BinaryConnective::Implication, lhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![] })) .into(), rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "q".into(), + predicate_symbol: "q".into(), terms: vec![] })) .into() } .into(), rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "r".into(), + predicate_symbol: "r".into(), terms: vec![] })) .into(), @@ -654,19 +662,19 @@ mod tests { Format(&Formula::BinaryFormula { connective: BinaryConnective::Implication, lhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![] })) .into(), rhs: Formula::BinaryFormula { connective: BinaryConnective::ReverseImplication, lhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "q".into(), + predicate_symbol: "q".into(), terms: vec![] })) .into(), rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "r".into(), + predicate_symbol: "r".into(), terms: vec![] })) .into() @@ -683,19 +691,19 @@ mod tests { lhs: Formula::BinaryFormula { connective: BinaryConnective::ReverseImplication, lhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![] })) .into(), rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "q".into(), + predicate_symbol: "q".into(), terms: vec![] })) .into() } .into(), rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "r".into(), + predicate_symbol: "r".into(), terms: vec![] })) .into(), @@ -708,19 +716,19 @@ mod tests { Format(&Formula::BinaryFormula { connective: BinaryConnective::ReverseImplication, lhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![] })) .into(), rhs: Formula::BinaryFormula { connective: BinaryConnective::Implication, lhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "q".into(), + predicate_symbol: "q".into(), terms: vec![] })) .into(), rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "r".into(), + predicate_symbol: "r".into(), terms: vec![] })) .into() diff --git a/src/formatting/fol/tptp.rs b/src/formatting/fol/tptp.rs index d22427f6..ba3e5b63 100644 --- a/src/formatting/fol/tptp.rs +++ b/src/formatting/fol/tptp.rs @@ -84,7 +84,7 @@ impl Display for Format<'_, GeneralTerm> { impl Display for Format<'_, Atom> { fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result { - let predicate = &self.0.predicate; + let predicate = &self.0.predicate_symbol; let terms = &self.0.terms; write!(f, "{predicate}")?; @@ -373,7 +373,7 @@ mod tests { fn format_atom() { assert_eq!( Format(&Atom { - predicate: "prime".into(), + predicate_symbol: "prime".into(), terms: vec![ GeneralTerm::IntegerTerm(IntegerTerm::BinaryOperation { op: BinaryOperator::Add, @@ -530,7 +530,7 @@ mod tests { fn format_formula() { assert_eq!( Format(&Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![] }))) .to_string(), @@ -542,19 +542,19 @@ mod tests { lhs: Formula::BinaryFormula { connective: BinaryConnective::Implication, lhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![] })) .into(), rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "q".into(), + predicate_symbol: "q".into(), terms: vec![] })) .into() } .into(), rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "r".into(), + predicate_symbol: "r".into(), terms: vec![] })) .into(), @@ -580,12 +580,12 @@ mod tests { formula: Formula::BinaryFormula { connective: BinaryConnective::Conjunction, lhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![], })) .into(), rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "q".into(), + predicate_symbol: "q".into(), terms: vec![], })) .into(), diff --git a/src/parsing/asp/grammar.pest b/src/parsing/asp/grammar.pest index b347088c..834946d0 100644 --- a/src/parsing/asp/grammar.pest +++ b/src/parsing/asp/grammar.pest @@ -22,6 +22,9 @@ binary_operator = _{ add | subtract | multiply | divide | modulo | interval } term = { unary_operator* ~ primary_term ~ (binary_operator ~ unary_operator* ~ primary_term)* } primary_term = _{ precomputed_term | variable | "(" ~ term ~ ")"} +predicate = { symbol ~ "/" ~ arity } + arity = @{ ("0") | (ASCII_NONZERO_DIGIT ~ ASCII_DIGIT*) } + atom = { symbol ~ term_tuple? } term_tuple = _{ "(" ~ (term ~ ("," ~ term)*)? ~ ")" } diff --git a/src/parsing/asp/pest.rs b/src/parsing/asp/pest.rs index 85614444..67048986 100644 --- a/src/parsing/asp/pest.rs +++ b/src/parsing/asp/pest.rs @@ -2,7 +2,7 @@ use crate::{ parsing::PestParser, syntax_tree::asp::{ Atom, AtomicFormula, BinaryOperator, Body, Comparison, Head, Literal, PrecomputedTerm, - Program, Relation, Rule, Sign, Term, UnaryOperator, Variable, + Predicate, Program, Relation, Rule, Sign, Term, UnaryOperator, Variable, }, }; @@ -137,6 +137,36 @@ impl PestParser for TermParser { } } +pub struct PredicateParser; + +impl PestParser for PredicateParser { + type Node = Predicate; + + type InternalParser = internal::Parser; + type Rule = internal::Rule; + const RULE: Self::Rule = internal::Rule::predicate; + + fn translate_pair(pair: pest::iterators::Pair<'_, Self::Rule>) -> Self::Node { + if pair.as_rule() != internal::Rule::predicate { + Self::report_unexpected_pair(pair) + } + + let mut pairs = pair.into_inner(); + let symbol = pairs + .next() + .unwrap_or_else(|| Self::report_missing_pair()) + .as_str() + .into(); + let arity_string: &str = pairs + .next() + .unwrap_or_else(|| Self::report_missing_pair()) + .as_str(); + let arity: usize = arity_string.parse().unwrap(); + + Predicate { symbol, arity } + } +} + pub struct AtomParser; impl PestParser for AtomParser { @@ -160,7 +190,10 @@ impl PestParser for AtomParser { .into(); let terms: Vec<_> = pairs.map(TermParser::translate_pair).collect(); - Atom { predicate, terms } + Atom { + predicate_symbol: predicate, + terms, + } } } @@ -414,14 +447,16 @@ mod tests { use { super::{ AtomParser, AtomicFormulaParser, BinaryOperatorParser, BodyParser, ComparisonParser, - HeadParser, LiteralParser, PrecomputedTermParser, ProgramParser, RelationParser, - RuleParser, SignParser, TermParser, UnaryOperatorParser, VariableParser, + HeadParser, LiteralParser, PrecomputedTermParser, PredicateParser, ProgramParser, + RelationParser, RuleParser, SignParser, TermParser, UnaryOperatorParser, + VariableParser, }, crate::{ parsing::TestedParser, syntax_tree::asp::{ Atom, AtomicFormula, BinaryOperator, Body, Comparison, Head, Literal, - PrecomputedTerm, Program, Relation, Rule, Sign, Term, UnaryOperator, Variable, + PrecomputedTerm, Predicate, Program, Relation, Rule, Sign, Term, UnaryOperator, + Variable, }, }, }; @@ -735,6 +770,19 @@ mod tests { ]); } + #[test] + fn parse_predicate() { + PredicateParser + .should_parse_into([( + "p/1", + Predicate { + symbol: "p".into(), + arity: 1, + }, + )]) + .should_reject(["p", "1/1", "p/00", "p/01", "_/1", "p/p", "_p/1"]); + } + #[test] fn parse_atom() { AtomParser @@ -742,28 +790,28 @@ mod tests { ( "p", Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![], }, ), ( "p()", Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![], }, ), ( "p(1)", Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![Term::PrecomputedTerm(PrecomputedTerm::Numeral(1))], }, ), ( "p(1, 2)", Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![ Term::PrecomputedTerm(PrecomputedTerm::Numeral(1)), Term::PrecomputedTerm(PrecomputedTerm::Numeral(2)), @@ -793,7 +841,7 @@ mod tests { Literal { sign: Sign::NoSign, atom: Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![], }, }, @@ -803,7 +851,7 @@ mod tests { Literal { sign: Sign::Negation, atom: Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![], }, }, @@ -813,7 +861,7 @@ mod tests { Literal { sign: Sign::DoubleNegation, atom: Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![], }, }, @@ -823,7 +871,7 @@ mod tests { Literal { sign: Sign::NoSign, atom: Atom { - predicate: "notp".into(), + predicate_symbol: "notp".into(), terms: vec![], }, }, @@ -873,7 +921,7 @@ mod tests { AtomicFormula::Literal(Literal { sign: Sign::Negation, atom: Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![], }, }), @@ -887,14 +935,14 @@ mod tests { ( "p", Head::Basic(Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![], }), ), ( "{p}", Head::Choice(Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![], }), ), @@ -912,7 +960,7 @@ mod tests { formulas: vec![AtomicFormula::Literal(Literal { sign: Sign::NoSign, atom: Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![], }, })], @@ -925,7 +973,7 @@ mod tests { AtomicFormula::Literal(Literal { sign: Sign::NoSign, atom: Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![], }, }), @@ -955,14 +1003,14 @@ mod tests { "a :- b.", Rule { head: Head::Basic(Atom { - predicate: "a".into(), + predicate_symbol: "a".into(), terms: vec![], }), body: Body { formulas: vec![AtomicFormula::Literal(Literal { sign: Sign::NoSign, atom: Atom { - predicate: "b".into(), + predicate_symbol: "b".into(), terms: vec![], }, })], @@ -973,7 +1021,7 @@ mod tests { "a :-.", Rule { head: Head::Basic(Atom { - predicate: "a".into(), + predicate_symbol: "a".into(), terms: vec![], }), body: Body { formulas: vec![] }, @@ -983,7 +1031,7 @@ mod tests { "a.", Rule { head: Head::Basic(Atom { - predicate: "a".into(), + predicate_symbol: "a".into(), terms: vec![], }), body: Body { formulas: vec![] }, @@ -1003,21 +1051,21 @@ mod tests { rules: vec![ Rule { head: Head::Basic(Atom { - predicate: "a".into(), + predicate_symbol: "a".into(), terms: vec![], }), body: Body { formulas: vec![] }, }, Rule { head: Head::Basic(Atom { - predicate: "b".into(), + predicate_symbol: "b".into(), terms: vec![], }), body: Body { formulas: vec![AtomicFormula::Literal(Literal { sign: Sign::NoSign, atom: Atom { - predicate: "a".into(), + predicate_symbol: "a".into(), terms: vec![], }, })], @@ -1031,7 +1079,7 @@ mod tests { Program { rules: vec![Rule { head: Head::Basic(Atom { - predicate: "a".into(), + predicate_symbol: "a".into(), terms: vec![], }), body: Body { formulas: vec![] }, diff --git a/src/parsing/fol/grammar.pest b/src/parsing/fol/grammar.pest index 09416c29..f839cedd 100644 --- a/src/parsing/fol/grammar.pest +++ b/src/parsing/fol/grammar.pest @@ -54,8 +54,11 @@ general_term = { integer_term | symbolic_constant | general_variable } variable = { integer_variable | general_variable } -atom = { predicate_symbol ~ term_tuple? } +predicate = { predicate_symbol ~ "/" ~ arity } predicate_symbol = _{ symbolic_constant } + arity = @{ ("0") | (ASCII_NONZERO_DIGIT ~ ASCII_DIGIT*) } + +atom = { predicate_symbol ~ term_tuple? } term_tuple = _{ "(" ~ (general_term ~ ("," ~ general_term)*)? ~ ")" } relation = { greater_equal | less_equal | greater | less | not_equal | equal } diff --git a/src/parsing/fol/pest.rs b/src/parsing/fol/pest.rs index 232e219a..abaca386 100644 --- a/src/parsing/fol/pest.rs +++ b/src/parsing/fol/pest.rs @@ -2,8 +2,8 @@ use crate::{ parsing::PestParser, syntax_tree::fol::{ Atom, AtomicFormula, BasicIntegerTerm, BinaryConnective, BinaryOperator, Comparison, - Formula, GeneralTerm, Guard, IntegerTerm, Quantification, Quantifier, Relation, Sort, - Theory, UnaryConnective, UnaryOperator, Variable, + Formula, GeneralTerm, Guard, IntegerTerm, Predicate, Quantification, Quantifier, Relation, + Sort, Theory, UnaryConnective, UnaryOperator, Variable, }, }; @@ -160,6 +160,36 @@ impl PestParser for GeneralTermParser { } } +pub struct PredicateParser; + +impl PestParser for PredicateParser { + type Node = Predicate; + + type InternalParser = internal::Parser; + type Rule = internal::Rule; + const RULE: Self::Rule = internal::Rule::predicate; + + fn translate_pair(pair: pest::iterators::Pair<'_, Self::Rule>) -> Self::Node { + if pair.as_rule() != internal::Rule::predicate { + Self::report_unexpected_pair(pair) + } + + let mut pairs = pair.into_inner(); + let symbol = pairs + .next() + .unwrap_or_else(|| Self::report_missing_pair()) + .as_str() + .into(); + let arity_string: &str = pairs + .next() + .unwrap_or_else(|| Self::report_missing_pair()) + .as_str(); + let arity: usize = arity_string.parse().unwrap(); + + Predicate { symbol, arity } + } +} + pub struct AtomParser; impl PestParser for AtomParser { @@ -176,14 +206,17 @@ impl PestParser for AtomParser { let mut pairs = pair.into_inner(); - let predicate = pairs + let predicate_symbol = pairs .next() .unwrap_or_else(|| Self::report_missing_pair()) .as_str() .into(); let terms: Vec<_> = pairs.map(GeneralTermParser::translate_pair).collect(); - Atom { predicate, terms } + Atom { + predicate_symbol, + terms, + } } } @@ -480,15 +513,16 @@ mod tests { super::{ AtomParser, AtomicFormulaParser, BasicIntegerTermParser, BinaryConnectiveParser, BinaryOperatorParser, ComparisonParser, FormulaParser, GeneralTermParser, GuardParser, - IntegerTermParser, QuantificationParser, QuantifierParser, RelationParser, - TheoryParser, UnaryConnectiveParser, UnaryOperatorParser, VariableParser, + IntegerTermParser, PredicateParser, QuantificationParser, QuantifierParser, + RelationParser, TheoryParser, UnaryConnectiveParser, UnaryOperatorParser, + VariableParser, }, crate::{ parsing::TestedParser, syntax_tree::fol::{ Atom, AtomicFormula, BasicIntegerTerm, BinaryConnective, BinaryOperator, - Comparison, Formula, GeneralTerm, Guard, IntegerTerm, Quantification, Quantifier, - Relation, Sort, Theory, UnaryConnective, UnaryOperator, Variable, + Comparison, Formula, GeneralTerm, Guard, IntegerTerm, Predicate, Quantification, + Quantifier, Relation, Sort, Theory, UnaryConnective, UnaryOperator, Variable, }, }, }; @@ -746,6 +780,28 @@ mod tests { ]); } + #[test] + fn parse_predicate() { + PredicateParser + .should_parse_into([ + ( + "p/1", + Predicate { + symbol: "p".into(), + arity: 1, + }, + ), + ( + "_p/1", + Predicate { + symbol: "_p".into(), + arity: 1, + }, + ), + ]) + .should_reject(["p", "1/1", "p/00", "p/01", "_/1", "p/p"]); + } + #[test] fn parse_atom() { AtomParser @@ -753,7 +809,7 @@ mod tests { ( "p", Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![], }, ), @@ -761,21 +817,21 @@ mod tests { // Parsing "g" caused issues ealier because "g" is also a sort declaration. "g", Atom { - predicate: "g".into(), + predicate_symbol: "g".into(), terms: vec![], }, ), ( "p()", Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![], }, ), ( "p(1)", Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![GeneralTerm::IntegerTerm(IntegerTerm::BasicIntegerTerm( BasicIntegerTerm::Numeral(1), ))], @@ -784,7 +840,7 @@ mod tests { ( "p(1, 2)", Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![ GeneralTerm::IntegerTerm(IntegerTerm::BasicIntegerTerm( BasicIntegerTerm::Numeral(1), @@ -798,7 +854,7 @@ mod tests { ( "p(X, a)", Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![ GeneralTerm::GeneralVariable("X".into()), GeneralTerm::Symbol("a".into()), @@ -926,7 +982,7 @@ mod tests { ( "p(N$i, 3*2)", AtomicFormula::Atom(Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![ GeneralTerm::IntegerTerm(IntegerTerm::BasicIntegerTerm( BasicIntegerTerm::IntegerVariable("N".into()), @@ -1066,7 +1122,7 @@ mod tests { Formula::UnaryFormula { connective: UnaryConnective::Negation, formula: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![], })) .into(), @@ -1085,14 +1141,14 @@ mod tests { }], }, formula: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![GeneralTerm::GeneralVariable("A".into())], })) .into(), } .into(), rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "q".into(), + predicate_symbol: "q".into(), terms: vec![], })) .into(), @@ -1111,7 +1167,7 @@ mod tests { }], }, formula: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![GeneralTerm::GeneralVariable("A".into())], })) .into(), @@ -1133,7 +1189,7 @@ mod tests { }], }, formula: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![GeneralTerm::GeneralVariable("A".into())], })) .into(), @@ -1173,7 +1229,7 @@ mod tests { formula: Formula::UnaryFormula { connective: UnaryConnective::Negation, formula: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "ra".to_string(), + predicate_symbol: "ra".to_string(), terms: vec![ GeneralTerm::GeneralVariable("V1".into()), GeneralTerm::GeneralVariable("V2".into()), @@ -1185,7 +1241,7 @@ mod tests { } .into(), rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "ra".to_string(), + predicate_symbol: "ra".to_string(), terms: vec![ GeneralTerm::GeneralVariable("V1".into()), GeneralTerm::GeneralVariable("V2".into()), @@ -1215,7 +1271,7 @@ mod tests { formula: Formula::BinaryFormula { connective: BinaryConnective::Equivalence, lhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "p".into(), + predicate_symbol: "p".into(), terms: vec![ GeneralTerm::GeneralVariable("G".into()), GeneralTerm::IntegerTerm(IntegerTerm::BinaryOperation { @@ -1235,19 +1291,19 @@ mod tests { rhs: Formula::BinaryFormula { connective: BinaryConnective::Disjunction, lhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "q".into(), + predicate_symbol: "q".into(), terms: vec![], })) .into(), rhs: Formula::BinaryFormula { connective: BinaryConnective::Conjunction, lhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "r".into(), + predicate_symbol: "r".into(), terms: vec![], })) .into(), rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "t".into(), + predicate_symbol: "t".into(), terms: vec![], })) .into(), @@ -1270,7 +1326,7 @@ mod tests { "a.\n", Theory { formulas: vec![Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate: "a".into(), + predicate_symbol: "a".into(), terms: vec![], }))], }, diff --git a/src/syntax_tree/asp.rs b/src/syntax_tree/asp.rs index 882857c3..c8f9782e 100644 --- a/src/syntax_tree/asp.rs +++ b/src/syntax_tree/asp.rs @@ -3,8 +3,9 @@ use { formatting::asp::default::Format, parsing::asp::pest::{ AtomParser, AtomicFormulaParser, BinaryOperatorParser, BodyParser, ComparisonParser, - HeadParser, LiteralParser, PrecomputedTermParser, ProgramParser, RelationParser, - RuleParser, SignParser, TermParser, UnaryOperatorParser, VariableParser, + HeadParser, LiteralParser, PrecomputedTermParser, PredicateParser, ProgramParser, + RelationParser, RuleParser, SignParser, TermParser, UnaryOperatorParser, + VariableParser, }, syntax_tree::{impl_node, Node}, }, @@ -77,15 +78,30 @@ impl Term { } } +#[derive(Clone, Debug, Eq, PartialEq, Hash)] +pub struct Predicate { + pub symbol: String, + pub arity: usize, +} + +impl_node!(Predicate, Format, PredicateParser); + #[derive(Clone, Debug, Eq, PartialEq, Hash)] pub struct Atom { - pub predicate: String, + pub predicate_symbol: String, pub terms: Vec, } impl_node!(Atom, Format, AtomParser); impl Atom { + pub fn predicate(&self) -> Predicate { + Predicate { + symbol: self.predicate_symbol.clone(), + arity: self.terms.len(), + } + } + pub fn variables(&self) -> HashSet { let mut vars = HashSet::new(); for term in self.terms.iter() { @@ -113,6 +129,10 @@ pub struct Literal { impl_node!(Literal, Format, LiteralParser); impl Literal { + pub fn predicate(&self) -> Predicate { + self.atom.predicate() + } + pub fn variables(&self) -> HashSet { self.atom.variables() } @@ -162,6 +182,13 @@ impl AtomicFormula { AtomicFormula::Comparison(c) => c.variables(), } } + + pub fn predicates(&self) -> HashSet { + match &self { + AtomicFormula::Literal(l) => HashSet::from([l.predicate()]), + AtomicFormula::Comparison(_) => HashSet::new(), + } + } } #[derive(Clone, Debug, Eq, PartialEq, Hash)] @@ -174,10 +201,12 @@ pub enum Head { impl_node!(Head, Format, HeadParser); impl Head { + // TODO: Revisit these helper function; make sure they are symmetric with all the others. + pub fn predicate(&self) -> Option<&str> { match self { - Head::Basic(a) => Some(&a.predicate), - Head::Choice(a) => Some(&a.predicate), + Head::Basic(a) => Some(&a.predicate_symbol), + Head::Choice(a) => Some(&a.predicate_symbol), Head::Falsity => None, } } diff --git a/src/syntax_tree/fol.rs b/src/syntax_tree/fol.rs index dc805d41..a1a4f53b 100644 --- a/src/syntax_tree/fol.rs +++ b/src/syntax_tree/fol.rs @@ -4,8 +4,9 @@ use { parsing::fol::pest::{ AtomParser, AtomicFormulaParser, BasicIntegerTermParser, BinaryConnectiveParser, BinaryOperatorParser, ComparisonParser, FormulaParser, GeneralTermParser, GuardParser, - IntegerTermParser, QuantificationParser, QuantifierParser, RelationParser, - TheoryParser, UnaryConnectiveParser, UnaryOperatorParser, VariableParser, + IntegerTermParser, PredicateParser, QuantificationParser, QuantifierParser, + RelationParser, TheoryParser, UnaryConnectiveParser, UnaryOperatorParser, + VariableParser, }, syntax_tree::{impl_node, Node}, }, @@ -102,12 +103,29 @@ impl GeneralTerm { } } +#[derive(Clone, Debug, Eq, PartialEq, Hash)] +pub struct Predicate { + pub symbol: String, + pub arity: usize, +} + +impl_node!(Predicate, Format, PredicateParser); + #[derive(Clone, Debug, Eq, PartialEq, Hash)] pub struct Atom { - pub predicate: String, + pub predicate_symbol: String, pub terms: Vec, } +impl Atom { + pub fn predicate(&self) -> Predicate { + Predicate { + symbol: self.predicate_symbol.clone(), + arity: self.terms.len(), + } + } +} + impl_node!(Atom, Format, AtomParser); #[derive(Clone, Debug, Eq, PartialEq, Hash)] @@ -174,6 +192,15 @@ impl AtomicFormula { } } } + + pub fn predicates(&self) -> HashSet { + match &self { + AtomicFormula::Falsity | AtomicFormula::Truth | AtomicFormula::Comparison(_) => { + HashSet::new() + } + AtomicFormula::Atom(a) => HashSet::from([a.predicate()]), + } + } } #[derive(Clone, Debug, Eq, PartialEq, Hash)] @@ -259,6 +286,19 @@ impl Formula { Formula::QuantifiedFormula { formula, .. } => formula.variables(), } } + + pub fn predicates(&self) -> HashSet { + match &self { + Formula::AtomicFormula(f) => f.predicates(), + Formula::UnaryFormula { formula, .. } => formula.predicates(), + Formula::BinaryFormula { lhs, rhs, .. } => { + let mut vars = lhs.predicates(); + vars.extend(rhs.predicates()); + vars + } + Formula::QuantifiedFormula { formula, .. } => formula.predicates(), + } + } } #[derive(Clone, Debug, Eq, PartialEq, Hash)]