diff --git a/src/formatting/fol/default.rs b/src/formatting/fol/default.rs index 8df1e3e3..aa38d8e6 100644 --- a/src/formatting/fol/default.rs +++ b/src/formatting/fol/default.rs @@ -195,14 +195,7 @@ impl Display for Format<'_, Quantifier> { impl Display for Format<'_, FunctionConstant> { fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result { - let name = &self.0.name; - let sort = &self.0.sort; - - match sort { - Sort::General => write!(f, "{name}$g"), - Sort::Integer => write!(f, "{name}$i"), - Sort::Symbol => write!(f, "{name}$s"), - } + write!(f, "{}${}", self.0.name, Format(&self.0.sort)) } } @@ -219,6 +212,16 @@ impl Display for Format<'_, Variable> { } } +impl Display for Format<'_, Sort> { + fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result { + match self.0 { + Sort::General => write!(f, "g"), + Sort::Integer => write!(f, "i"), + Sort::Symbol => write!(f, "s"), + } + } +} + impl Display for Format<'_, Quantification> { fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result { let quantifier = &self.0.quantifier; diff --git a/src/parsing/fol/grammar.pest b/src/parsing/fol/grammar.pest index 4cff4511..d21b04b8 100644 --- a/src/parsing/fol/grammar.pest +++ b/src/parsing/fol/grammar.pest @@ -7,6 +7,7 @@ keyword = _{ primitive | binary_connective | unary_connective | quantifier } supremum = { "#sup" } sort = { general_sort | integer_sort | symbolic_sort } +sort_eoi = _{ sort ~ EOI } general_sort = @{ "g" ~ "eneral"? } integer_sort = @{ "i" ~ "nteger"? } symbolic_sort = @{ "s" ~ "ymbol"? } diff --git a/src/parsing/fol/pest.rs b/src/parsing/fol/pest.rs index 3f486b05..a3ea43b5 100644 --- a/src/parsing/fol/pest.rs +++ b/src/parsing/fol/pest.rs @@ -493,6 +493,26 @@ impl PestParser for QuantificationParser { } } +pub struct SortParser; + +impl PestParser for SortParser { + type Node = Sort; + + type InternalParser = internal::Parser; + type Rule = internal::Rule; + const RULE: internal::Rule = internal::Rule::sort_eoi; + + fn translate_pair(pair: pest::iterators::Pair<'_, Self::Rule>) -> Self::Node { + match pair.as_rule() { + internal::Rule::sort => Self::translate_pairs(pair.into_inner()), + internal::Rule::general_sort => Sort::General, + internal::Rule::symbolic_sort => Sort::Symbol, + internal::Rule::integer_sort => Sort::Integer, + _ => Self::report_unexpected_pair(pair), + } + } +} + pub struct UnaryConnectiveParser; impl PestParser for UnaryConnectiveParser { @@ -729,15 +749,10 @@ impl PestParser for PlaceholderDeclarationParser { .as_str() .into(); - let sort = match pairs.next() { - Some(pair) => match pair.as_rule() { - internal::Rule::general_sort => Sort::General, - internal::Rule::symbolic_sort => Sort::Symbol, - internal::Rule::integer_sort => Sort::Integer, - _ => Self::report_unexpected_pair(pair), - }, - None => Sort::General, - }; + let sort = pairs + .next() + .map(SortParser::translate_pair) + .unwrap_or_else(|| Sort::General); if let Some(pair) = pairs.next() { Self::report_unexpected_pair(pair) @@ -805,7 +820,7 @@ mod tests { AnnotatedFormulaParser, AtomParser, AtomicFormulaParser, BinaryConnectiveParser, BinaryOperatorParser, ComparisonParser, FormulaParser, GeneralTermParser, GuardParser, IntegerTermParser, PredicateParser, QuantificationParser, QuantifierParser, - RelationParser, SpecificationParser, SymbolicTermParser, TheoryParser, + RelationParser, SortParser, SpecificationParser, SymbolicTermParser, TheoryParser, UnaryConnectiveParser, UnaryOperatorParser, UserGuideParser, VariableParser, }, crate::{ @@ -1229,6 +1244,20 @@ mod tests { .should_reject(["p and b"]); } + #[test] + fn parse_sort() { + SortParser + .should_parse_into([ + ("i", Sort::Integer), + ("integer", Sort::Integer), + ("s", Sort::Symbol), + ("symbol", Sort::Symbol), + ("g", Sort::General), + ("general", Sort::General), + ]) + .should_reject(["int", "sym", "gen"]); + } + #[test] fn parse_unary_connective() { UnaryConnectiveParser diff --git a/src/syntax_tree/fol.rs b/src/syntax_tree/fol.rs index 7d83d3ec..cf657960 100644 --- a/src/syntax_tree/fol.rs +++ b/src/syntax_tree/fol.rs @@ -6,9 +6,9 @@ use { BinaryOperatorParser, ComparisonParser, DirectionParser, FormulaParser, FunctionConstantParser, GeneralTermParser, GuardParser, IntegerTermParser, PlaceholderDeclarationParser, PredicateParser, QuantificationParser, QuantifierParser, - RelationParser, RoleParser, SpecificationParser, SymbolicTermParser, TheoryParser, - UnaryConnectiveParser, UnaryOperatorParser, UserGuideEntryParser, UserGuideParser, - VariableParser, + RelationParser, RoleParser, SortParser, SpecificationParser, SymbolicTermParser, + TheoryParser, UnaryConnectiveParser, UnaryOperatorParser, UserGuideEntryParser, + UserGuideParser, VariableParser, }, syntax_tree::{impl_node, Node}, verifying::problem, @@ -502,7 +502,7 @@ pub enum Sort { Symbol, } -// TODO: Should Sort be a Node? +impl_node!(Sort, Format, SortParser); #[derive(Clone, Debug, Eq, PartialEq, Hash, Ord, PartialOrd)] pub struct FunctionConstant {