Promote Sort to a Node and use its new parser to solve a bug

potassco · Aug 22, 2024 · 9d308ec · 9d308ec
1 parent c830877
commit 9d308ec
Show file tree

Hide file tree

Showing 4 changed files with 55 additions and 22 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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 {