fix: wrong implementation of parser for predicate call arguments

Author: coeff-aij

src/annot.rs

@@ -477,14 +477,23 @@ where
                             chc::Term::FormulaExistentialVar(sort.clone(), ident.name.to_string());
                         FormulaOrTerm::Term(var, sort.clone())
                     }
-                    _ => {
-                        if let Some(TokenTree::Delimited(_, _, Delimiter::Parenthesis, _args)) = self.look_ahead_token_tree(1) {
+                    _ => {                        
+                        let next_tt = self.look_ahead_token_tree(0);
+
+                        if let Some(TokenTree::Delimited(_, _, Delimiter::Parenthesis, args)) = next_tt {
+                            let args = args.clone();
                             self.consume();
+
                             let pred_symbol = chc::UserDefinedPredSymbol::new(ident.name.to_string());
                             let pred = chc::Pred::UserDefined(pred_symbol);
 
-                            let args = self.parse_datatype_ctor_args()?;
-                            
+                            let mut parser = Parser {
+                                resolver: self.boxed_resolver(),
+                                cursor: args.trees(),
+                                formula_existentials: self.formula_existentials.clone(),
+                            };
+                            let args = parser.parse_datatype_ctor_args()?;
+
                             let atom = chc::Atom::new(pred, args);
                             let formula = chc::Formula::Atom(atom);
                             return Ok(FormulaOrTerm::Formula(formula));