Fix attribute parsing (#4530)

Fixes `OuterParser` for attributes of the form `foo()`.
runtimeverification · Jul 18, 2024 · 788d1f3 · 788d1f3
1 parent 2c95ae9
commit 788d1f3
Show file tree

Hide file tree

Showing 2 changed files with 27 additions and 4 deletions.
diff --git a/pyk/src/pyk/kast/outer_parser.py b/pyk/src/pyk/kast/outer_parser.py
@@ -379,10 +379,13 @@ def _maybe_att(self) -> Att:
             value: str
             if self._la.type == TokenType.LPAREN:
                 self._consume()
-                if self._la.type is TokenType.ATTR_CONTENT:
-                    value = self._consume()
-                else:
-                    value = _dequote_string(self._match(TokenType.STRING))
+                match self._la.type:
+                    case TokenType.ATTR_CONTENT:
+                        value = self._consume()
+                    case TokenType.STRING:
+                        value = _dequote_string(self._consume())
+                    case _:
+                        value = ''
                 self._match(TokenType.RPAREN)
             else:
                 value = ''

diff --git a/pyk/src/tests/unit/kast/test_outer_parser.py b/pyk/src/tests/unit/kast/test_outer_parser.py
@@ -113,6 +113,26 @@
         'syntax Foo ::= "foo"',
         SyntaxDefn(SortDecl('Foo'), (PriorityBlock((Production((Terminal('foo'),)),)),)),
     ),
+    (
+        'syntax Foo ::= "foo" [symbol]',
+        SyntaxDefn(SortDecl('Foo'), (PriorityBlock((Production((Terminal('foo'),), att=Att((('symbol', ''),))),)),)),
+    ),
+    (
+        'syntax Foo ::= "foo" [symbol()]',
+        SyntaxDefn(SortDecl('Foo'), (PriorityBlock((Production((Terminal('foo'),), att=Att((('symbol', ''),))),)),)),
+    ),
+    (
+        'syntax Foo ::= "foo" [symbol("")]',
+        SyntaxDefn(SortDecl('Foo'), (PriorityBlock((Production((Terminal('foo'),), att=Att((('symbol', ''),))),)),)),
+    ),
+    (
+        'syntax Foo ::= "foo" [symbol(foo)]',
+        SyntaxDefn(SortDecl('Foo'), (PriorityBlock((Production((Terminal('foo'),), att=Att((('symbol', 'foo'),))),)),)),
+    ),
+    (
+        'syntax Foo ::= "foo" [symbol("foo")]',
+        SyntaxDefn(SortDecl('Foo'), (PriorityBlock((Production((Terminal('foo'),), att=Att((('symbol', 'foo'),))),)),)),
+    ),
     (
         'syntax Foo ::= Bar',
         SyntaxDefn(SortDecl('Foo'), (PriorityBlock((Production((NonTerminal(Sort('Bar')),)),)),)),