Skip to content

Commit

Permalink
Make anchor arg parsing robust to recent changes
Browse files Browse the repository at this point in the history
  • Loading branch information
bpandreotti committed May 14, 2024
1 parent 4487229 commit 3e1525a
Showing 1 changed file with 15 additions and 2 deletions.
17 changes: 15 additions & 2 deletions carcara/src/parser/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -984,8 +984,21 @@ impl<'a, R: BufRead> Parser<'a, R> {
self.expect_token(Token::OpenParen)?;
Ok(if self.current_token == Token::Keyword("=".into()) {
self.next_token()?;
let (var, sort) = self.parse_sorted_var()?;
let value = self.parse_term_expecting_sort(sort.as_sort().unwrap())?;

// To make Carcara more robust to recent changes in the Alethe format, we support
// parsing the two versions of assign-style anchor arguments:
// - the old version, without the sort hint: `(:= <symbol> <term>)`
// - and the new version, with the sort hint: `(:= (<symbol> <sort>) <term>)`
let (var, value, sort) = if matches!(self.current_token, Token::Symbol(_)) {
let var = self.expect_symbol()?;
let value = self.parse_term()?;
let sort = self.pool.sort(&value);
(var, value, sort)
} else {
let (var, sort) = self.parse_sorted_var()?;
let value = self.parse_term_expecting_sort(sort.as_sort().unwrap())?;
(var, value, sort)
};
self.insert_sorted_var((var.clone(), sort.clone()));
self.expect_token(Token::CloseParen)?;
AnchorArg::Assign((var, sort), value)
Expand Down

0 comments on commit 3e1525a

Please sign in to comment.