fix: reflect review comments in PR

Author: coeff-aij

src/annot.rs

@@ -420,7 +420,7 @@ where
         Ok(AnnotPath { segments })
     }
 
-    fn parse_datatype_ctor_args(&mut self) -> Result<Vec<chc::Term<T::Output>>> {
+    fn parse_arg_terms(&mut self) -> Result<Vec<chc::Term<T::Output>>> {
         if self.look_ahead_token(0).is_none() {
             return Ok(Vec::new());
         }
@@ -477,7 +477,9 @@ where
                             chc::Term::FormulaExistentialVar(sort.clone(), ident.name.to_string());
                         FormulaOrTerm::Term(var, sort.clone())
                     }
-                    _ => {                        
+                    _ => {
+                        // If the single-segment identifier is followed by parethesized arguments,
+                        // parse them as user-defined predicate calls.
                         let next_tt = self.look_ahead_token_tree(0);
 
                         if let Some(TokenTree::Delimited(_, _, Delimiter::Parenthesis, args)) = next_tt {
@@ -492,7 +494,7 @@ where
                                 cursor: args.trees(),
                                 formula_existentials: self.formula_existentials.clone(),
                             };
-                            let args = parser.parse_datatype_ctor_args()?;
+                            let args = parser.parse_arg_terms()?;
 
                             let atom = chc::Atom::new(pred, args);
                             let formula = chc::Formula::Atom(atom);
@@ -517,7 +519,7 @@ where
                     cursor: s.trees(),
                     formula_existentials: self.formula_existentials.clone(),
                 };
-                let args = parser.parse_datatype_ctor_args()?;
+                let args = parser.parse_arg_terms()?;
                 parser.end_of_input()?;
                 let (term, sort) = path.to_datatype_ctor(args);
                 FormulaOrTerm::Term(term, sort)

src/chc.rs

@@ -902,7 +902,6 @@ impl MatcherPred {
     }
 }
 
-// TODO: This struct is almost copy of `DatatypeSymbol`. Two traits maight be unified with aliases.
 #[derive(Debug, Clone, PartialEq, Eq, Hash)]
 pub struct UserDefinedPredSymbol {
     inner: String,
@@ -1035,7 +1034,7 @@ impl Pred {
             Pred::Known(p) => p.name().into(),
             Pred::Var(p) => p.to_string().into(),
             Pred::Matcher(p) => p.name().into(),
-            Pred::UserDefined(p) => p.inner.clone().into(),
+            Pred::UserDefined(p) => p.to_string().into(),
         }
     }