Add option to parse arguments to hole rule

This reverts the default behaviour that was changed in
16adacd. Now, the flag
`--parse-hole-args` can be used to get the new behaviour.

Author: bpandreotti

carcara/src/elaborator/hole.rs

@@ -149,6 +149,7 @@ fn parse_and_check_solver_proof(
         expand_lets: true,
         allow_int_real_subtyping: true,
         strict: false,
+        parse_hole_args: false,
     };
 
     let (problem, proof) = parser::parse_instance_with_pool(problem, proof, config, pool)?;

carcara/src/elaborator/lia_generic.rs

@@ -136,6 +136,7 @@ fn parse_and_check_solver_proof(
         expand_lets: true,
         allow_int_real_subtyping: true,
         strict: false,
+        parse_hole_args: false,
     };
     let (problem, proof) = parser::parse_instance_with_pool(problem, proof, config, pool)?;
 

carcara/src/parser/mod.rs

@@ -45,6 +45,10 @@ pub struct Config {
     /// - Unary `and`, `or` and `xor` terms are not allowed
     /// - Anchor arguments using the old syntax (i.e., `(:= <symbol> <term>)`) are not allowed
     pub strict: bool,
+
+    /// If `true`, the parser will parse arguments to the `hole` rule, expecting them to be valid
+    /// terms.
+    pub parse_hole_args: bool,
 }
 
 impl Config {
@@ -910,7 +914,16 @@ impl<'a, R: BufRead> Parser<'a, R> {
         let args = if self.current_token == Token::Keyword("args".into()) {
             self.next_token()?;
             self.expect_token(Token::OpenParen)?;
-            self.parse_sequence(Self::parse_term, true)?
+
+            // If the rule is `hole` and `--parse-hole-args` is not enabled, we want to allow any
+            // invalid arguments, so we read the rest of the `:args` attribute without trying to
+            // parse anything
+            if rule == "hole" && !self.config.parse_hole_args {
+                self.ignore_until_close_parens()?;
+                Vec::new()
+            } else {
+                self.parse_sequence(Self::parse_term, true)?
+            }
         } else {
             Vec::new()
         };

carcara/src/parser/tests.rs

@@ -13,6 +13,7 @@ const TEST_CONFIG: Config = Config {
     expand_lets: false,
     allow_int_real_subtyping: false,
     strict: false,
+    parse_hole_args: false,
 };
 
 pub fn parse_terms<const N: usize>(

cli/src/main.rs

@@ -129,6 +129,11 @@ struct ParsingOptions {
     /// When this flag is enabled: unary `and`, `or` and `xor` terms are not allowed;
     #[clap(short, long = "strict-parsing")]
     strict: bool,
+
+    /// If `true`, Carcara will parse arguments to the `hole` rule, expecting them to be valid
+    /// terms. In the future, this will be the default behaviour.
+    #[clap(long)]
+    parse_hole_args: bool,
 }
 
 impl From<ParsingOptions> for parser::Config {
@@ -138,6 +143,7 @@ impl From<ParsingOptions> for parser::Config {
             expand_lets: val.expand_let_bindings,
             allow_int_real_subtyping: val.allow_int_real_subtyping,
             strict: val.strict,
+            parse_hole_args: val.parse_hole_args,
         }
     }
 }