Remove rawTerm from hints output (#1027)

Closes Pi-Squared-Inc/pi2#1300: 

`rawTerm` is a useful wrapper on a KItem injection. However, The Math
Proof Generation Team from $Piˆ2$ doesn't use it in their parser, so
they need to unwrap the injection and drop the `rawTerm` string every
time. To avoid this unnecessary overhead, we introduce in this PR a
modification to `proof_event::emit_serialize_term` and
`serialize_term_to_file` to allow us to construct the injection without
using the `rawTerm` wrapper.

The idea of including this modification into `serialize_term_to_file`
was to avoid a third function (`serialize_k_term_inj_to_file`) that has
the exact same structure as `serialize_term_to_file` and
`serialize_raw_term_to_file` with a single different line.

include/runtime/header.h

@@ -336,7 +336,8 @@ void serialize_configuration_to_file(
 void write_uint64_to_file(FILE *file, uint64_t i);
 void write_bool_to_file(FILE *file, bool b);
 void serialize_term_to_file(
-    FILE *file, block *subject, char const *sort, bool use_intern);
+    FILE *file, void *subject, char const *sort, bool use_intern,
+    bool k_item_inj = false);
 void serialize_raw_term_to_file(
     FILE *file, void *subject, char const *sort, bool use_intern);
 void print_variable_to_file(FILE *file, char const *varname);

lib/codegen/ProofEvent.cpp

@@ -38,34 +38,25 @@ llvm::CallInst *proof_event::emit_serialize_term(
   auto *i8_ptr_ty = llvm::Type::getInt8PtrTy(ctx_);
   auto *i1_ty = llvm::Type::getInt1Ty(ctx_);
 
-  if (cat.cat == sort_category::Symbol || cat.cat == sort_category::Variable) {
-    auto *block_ty = getvalue_type({sort_category::Symbol, 0}, module_);
-
-    auto *func_ty = llvm::FunctionType::get(
-        void_ty, {i8_ptr_ty, block_ty, i8_ptr_ty, i1_ty}, false);
-
-    auto *serialize
-        = get_or_insert_function(module_, "serialize_term_to_file", func_ty);
-
-    return b.CreateCall(
-        serialize,
-        {output_file, term, sort_name_ptr, llvm::ConstantInt::getFalse(ctx_)});
-  }
-  if (term->getType()->isIntegerTy()) {
-    term = b.CreateIntToPtr(term, i8_ptr_ty);
-  } else {
-    term = b.CreatePointerCast(term, i8_ptr_ty);
+  auto is_sym_or_var
+      = cat.cat == sort_category::Symbol || cat.cat == sort_category::Variable;
+  auto *construct_k_term_inj = llvm::ConstantInt::getBool(ctx_, !is_sym_or_var);
+
+  if (!is_sym_or_var) {
+    term = term->getType()->isIntegerTy()
+               ? b.CreateIntToPtr(term, i8_ptr_ty)
+               : b.CreatePointerCast(term, i8_ptr_ty);
   }
 
   auto *func_ty = llvm::FunctionType::get(
-      void_ty, {i8_ptr_ty, i8_ptr_ty, i8_ptr_ty, i1_ty}, false);
+      void_ty, {i8_ptr_ty, i8_ptr_ty, i8_ptr_ty, i1_ty, i1_ty}, false);
 
   auto *serialize
-      = get_or_insert_function(module_, "serialize_raw_term_to_file", func_ty);
+      = get_or_insert_function(module_, "serialize_term_to_file", func_ty);
 
   return b.CreateCall(
-      serialize,
-      {output_file, term, sort_name_ptr, llvm::ConstantInt::getFalse(ctx_)});
+      serialize, {output_file, term, sort_name_ptr,
+                  llvm::ConstantInt::getFalse(ctx_), construct_k_term_inj});
 }
 
 llvm::CallInst *proof_event::emit_serialize_configuration(

runtime/util/ConfigurationSerializer.cpp

@@ -449,10 +449,15 @@ void write_bool_to_file(FILE *file, bool b) {
 }
 
 void serialize_term_to_file(
-    FILE *file, block *subject, char const *sort, bool use_intern) {
+    FILE *file, void *subject, char const *sort, bool use_intern,
+    bool k_item_inj) {
+  block *term = k_item_inj ? construct_k_item_inj(subject, sort, true)
+                           : (block *)subject;
+  sort = k_item_inj ? "SortKItem{}" : sort;
+
   char *data = nullptr;
   size_t size = 0;
-  serialize_configuration(subject, sort, &data, &size, true, use_intern);
+  serialize_configuration(term, sort, &data, &size, true, use_intern);
 
   fwrite(data, 1, size, file);