Add support for rawTerm to Python bindings (#908)

~~Blocked on
#907

This PR follows up #907 by having the Python bindings strip patterns of
the form `rawTerm{}(inj{...}(...)})` when deserializing from binary
KORE; this will allow Pyk and subsequently the proof checker's parser to
soundly load function arguments from proof traces and pass them to the
function evaluator in #905.

---------

Co-authored-by: Tamás Tóth <[email protected]>

Author: Baltoli

bindings/python/ast.cpp

@@ -294,10 +294,13 @@ void bind_ast(py::module_ &m) {
                 py::kw_only(), py::arg("emit_size") = false)
             .def_static(
                 "deserialize",
-                [](py::bytes const &bytes) {
+                [](py::bytes const &bytes, bool strip_raw_term) {
                   auto str = std::string(bytes);
-                  return deserialize_pattern(str.begin(), str.end());
-                })
+                  return deserialize_pattern(
+                      str.begin(), str.end(), strip_raw_term);
+                },
+                py::arg("bytes"), py::kw_only(),
+                py::arg("strip_raw_term") = true)
             .def_static("read_from", &read_pattern_from_file);
 
   py::class_<KORECompositePattern, std::shared_ptr<KORECompositePattern>>(

bindings/python/package/kllvm/__init__.py

@@ -32,6 +32,11 @@ def to_pattern(self):
         def serialize(self, emit_size=False):
             return self._block.serialize(emit_size=emit_size)
 
+        # Used to implement backend integration tests; should not be bound
+        # onwards to Pyk without rethinking the underlying API.
+        def _serialize_raw(self, filename, sort):
+            self._block._serialize_raw(filename, sort)
+
         @staticmethod
         def deserialize(bs):
             return mod.InternalTerm.deserialize(bs)

bindings/python/runtime.cpp

@@ -80,10 +80,17 @@ void bind_runtime(py::module_ &m) {
             return py::bytes(std::string(data, data + size));
           },
           py::kw_only(), py::arg("emit_size") = false)
-      .def("deserialize", [](py::bytes const &bytes) {
-        auto str = std::string(bytes);
-        return deserializeConfiguration(str.data(), str.size());
-      });
+      .def(
+          "deserialize",
+          [](py::bytes const &bytes) {
+            auto str = std::string(bytes);
+            return deserializeConfiguration(str.data(), str.size());
+          })
+      .def(
+          "_serialize_raw", [](block *term, std::string const &filename,
+                               std::string const &sort) {
+            serializeRawTermToFile(filename.c_str(), term, sort.c_str());
+          });
 }
 
 PYBIND11_MODULE(_kllvm_runtime, m) {

include/kllvm/binary/deserializer.h

@@ -254,7 +254,8 @@ sptr<KOREPattern> read(It &ptr, It end, binary_version version) {
 std::string file_contents(std::string const &fn, int max_bytes = -1);
 
 template <typename It>
-sptr<KOREPattern> deserialize_pattern(It begin, It end) {
+sptr<KOREPattern>
+deserialize_pattern(It begin, It end, bool strip_raw_term = true) {
   // Try to parse the file even if the magic header isn't correct; by the time
   // we're here we already know that we're trying to parse a binary KORE file.
   // The header itself gets used by the application when detecting binary vs.
@@ -270,7 +271,31 @@ sptr<KOREPattern> deserialize_pattern(It begin, It end) {
     end = std::next(begin, total_size);
   }
 
-  return detail::read(begin, end, version);
+  auto pattern = detail::read(begin, end, version);
+
+  // When strip_raw_term is set, we're looking for special patterns that have
+  // the form:
+  //
+  //   rawTerm{}(inj{S, SortKItem{}}(X))
+  //
+  // and extracting the inner term X.
+  if (strip_raw_term) {
+    if (auto composite
+        = std::dynamic_pointer_cast<KORECompositePattern>(pattern)) {
+      if (composite->getConstructor()->getName() == "rawTerm"
+          && composite->getArguments().size() == 1) {
+        if (auto inj = std::dynamic_pointer_cast<KORECompositePattern>(
+                composite->getArguments()[0])) {
+          if (inj->getConstructor()->getName() == "inj"
+              && inj->getArguments().size() == 1) {
+            return inj->getArguments()[0];
+          }
+        }
+      }
+    }
+  }
+
+  return pattern;
 }
 
 bool has_binary_kore_header(std::string const &filename);