Exposing symbol entry point to kore_pareser

bindings/python/ast.cpp

@@ -373,9 +373,12 @@ void bind_parser(py::module_ &mod) {
           "pattern",
           [](kore_parser &parser) { return std::shared_ptr(parser.pattern()); })
       .def("sort", [](kore_parser &parser) { return parser.sort(); })
-      .def("definition", [](kore_parser &parser) {
-        return std::shared_ptr(parser.definition());
-      });
+      .def(
+          "definition",
+          [](kore_parser &parser) {
+            return std::shared_ptr(parser.definition());
+          })
+      .def("symbol", &kore_parser::symbol);
 }
 
 void bind_proof_trace(py::module_ &m) {

include/kllvm/parser/KOREParser.h

@@ -23,6 +23,7 @@ class kore_parser {
   ptr<kore_definition> definition();
   sptr<kore_pattern> pattern();
   sptr<kore_sort> sort();
+  ptr<kore_symbol> symbol();
   std::vector<ptr<kore_declaration>> declarations();
 
   std::pair<std::string, std::vector<sptr<kore_sort>>> symbol_sort_list();

lib/parser/KOREParser.cpp

@@ -1,5 +1,5 @@
-#include "kllvm/parser/KOREParser.h"
 #include "kllvm/ast/AST.h"
+#include "kllvm/parser/KOREParser.h"
 #include "kllvm/parser/KOREScanner.h"
 #include "kllvm/util/temporary_file.h"
 
@@ -90,6 +90,7 @@ ptr<kore_definition> kore_parser::definition() {
 }
 
 sptr<kore_pattern> kore_parser::pattern() {
+  std::cerr << "Parsing pattern\n";
   auto result = pattern_internal();
   consume(token::TokenEof);
   return result;
@@ -312,6 +313,7 @@ sptr<kore_sort> kore_parser::sort() {
 }
 
 sptr<kore_pattern> kore_parser::pattern_internal() {
+  std::cerr << "Parsing pattern internal\n";
   token current = peek();
   switch (current) {
   case token::Id: {
@@ -321,7 +323,9 @@ sptr<kore_pattern> kore_parser::pattern_internal() {
     case token::Colon:
       consume(token::Colon);
       return kore_variable_pattern::create(name, sort());
-    case token::LeftBrace: return application_pattern(name);
+    case token::LeftBrace:
+      std::cerr << "Passing through LeftBrace\n";
+      return application_pattern(name);
     default: error(loc_, "Expected: [:, {] Actual: " + str(current));
     }
   }
@@ -402,6 +406,16 @@ sptr<kore_pattern> kore_parser::application_pattern(std::string const &name) {
   return result;
 }
 
+ptr<kore_symbol> kore_parser::symbol() {
+  std::string symbol = consume(token::Id);
+  consume(token::LeftBrace);
+  auto pat = kore_composite_pattern::create(symbol);
+  sorts(pat->get_constructor());
+  pat->get_constructor()->init_pattern_arguments();
+  consume(token::RightBrace);
+  return std::make_unique<kore_symbol>(*pat->get_constructor());
+}
+
 ptr<kore_composite_pattern>
 kore_parser::application_pattern_internal(std::string const &name) {
   consume(token::LeftBrace);

test/python/test_symbols.py

@@ -28,6 +28,17 @@ def test_equal(self):
         b1 = kllvm.ast.Symbol("B")
         self.assertNotEqual(a1, b1)
 
+    def test_parse_symbol_name(self):
+        sym_base = kllvm.ast.Symbol("Lbl'Plus")
+        self.assertEqual(str(sym_base), "Lbl'Plus{}")
+
+        parser = kllvm.parser.Parser.from_string(str(sym_base))
+        sym_parsed = parser.symbol()
+        self.assertEqual(sym_base, sym_parsed)
+
+        self.assertEqual(sym_parsed.name, "Lbl'Plus")
+        self.assertTrue(sym_parsed.is_concrete)
+        self.assertFalse(sym_parsed.is_builtin)
 
 class TestVariables(unittest.TestCase):