Squashed commit of the following:

commit 4a0c5474a12689d194a34b07039ffef09028c912
Author: Bruce Collie <[email protected]>
Date:   Thu Nov 30 13:37:47 2023 +0000

    Add stubbed strip-raw-term interface

commit 66b6b8f
Author: Bruce Collie <[email protected]>
Date:   Thu Nov 30 11:24:58 2023 +0000

    Update test/python/test_raw_term.py

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

commit 23e9e5e
Author: Bruce Collie <[email protected]>
Date:   Tue Nov 28 14:50:57 2023 +0000

    Implement and test bindings strip

bindings/c/lib.cpp

@@ -273,7 +273,7 @@ void kore_simplify_binary(
     size_t *size_out) {
   auto sort_str = kore_sort_dump(sort);
 
-  auto block = deserializeConfiguration(data_in, size_in);
+  auto block = deserializeConfiguration(data_in, size_in, true);
   serializeConfiguration(block, sort_str, data_out, size_out, true);
 
   free(sort_str);

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

@@ -83,10 +83,19 @@ 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_static(
+          "deserialize",
+          [](py::bytes const &bytes, bool strip_raw_term) {
+            auto str = std::string(bytes);
+            return deserializeConfiguration(
+                str.data(), str.size(), strip_raw_term);
+          },
+          py::arg("bytes"), py::kw_only(), py::arg("strip_raw_term") = true)
+      .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);

include/runtime/header.h

@@ -289,7 +289,7 @@ void *constructCompositePattern(uint32_t tag, std::vector<void *> &arguments);
 extern "C" {
 
 block *parseConfiguration(const char *filename);
-block *deserializeConfiguration(char *, size_t);
+block *deserializeConfiguration(char *, size_t, bool);
 
 void printConfiguration(const char *filename, block *subject);
 void printStatistics(const char *filename, uint64_t steps);

runtime/util/ConfigurationParser.cpp

@@ -246,7 +246,7 @@ deserializeInitialConfiguration(It ptr, It end, binary_version version) {
 block *parseConfiguration(const char *filename) {
   if (has_binary_kore_header(filename)) {
     auto data = file_contents(filename);
-    return deserializeConfiguration(data.data(), data.size());
+    return deserializeConfiguration(data.data(), data.size(), true);
   } else {
     auto InitialConfiguration = parser::KOREParser(filename).pattern();
     // InitialConfiguration->print(std::cout);
@@ -258,7 +258,7 @@ block *parseConfiguration(const char *filename) {
   }
 }
 
-block *deserializeConfiguration(char *data, size_t size) {
+block *deserializeConfiguration(char *data, size_t size, bool strip_raw_term) {
   auto ptr = data;
   auto end = data + size;