From 063b1f023f49c3e11db000fd274ba2bd391a4473 Mon Sep 17 00:00:00 2001 From: Bruce Collie Date: Mon, 4 Dec 2023 16:11:15 +0000 Subject: [PATCH] Implement sorted term -> pattern --- bindings/core/src/core.cpp | 3 ++- include/runtime/header.h | 2 ++ runtime/util/ConfigurationSerializer.cpp | 14 +++++++++++--- 3 files changed, 15 insertions(+), 4 deletions(-) diff --git a/bindings/core/src/core.cpp b/bindings/core/src/core.cpp index 03479067c..7f797f091 100644 --- a/bindings/core/src/core.cpp +++ b/bindings/core/src/core.cpp @@ -78,9 +78,10 @@ std::shared_ptr evaluate_function( } auto tag = getTagForSymbolName(label.c_str()); + auto return_sort = getReturnSortForTag(tag); auto result = evaluateFunctionSymbol(tag, term_args.data()); - return term_to_pattern(static_cast(result)); + return sortedTermToKorePattern(static_cast(result), return_sort); } bool is_sort_kitem(std::shared_ptr const &sort) { diff --git a/include/runtime/header.h b/include/runtime/header.h index 55c1313fb..44550c4b0 100644 --- a/include/runtime/header.h +++ b/include/runtime/header.h @@ -310,6 +310,8 @@ void printConfigurationInternal( // you can use the C bindings, which wrap the return value of this method in // a POD struct. std::shared_ptr termToKorePattern(block *); +std::shared_ptr +sortedTermToKorePattern(block *, const char *); // This function injects its argument into KItem before printing, using the sort // argument as the source sort. Doing so allows the term to be pretty-printed diff --git a/runtime/util/ConfigurationSerializer.cpp b/runtime/util/ConfigurationSerializer.cpp index 232ad2ff0..fbe8d40cf 100644 --- a/runtime/util/ConfigurationSerializer.cpp +++ b/runtime/util/ConfigurationSerializer.cpp @@ -452,10 +452,18 @@ void serializeRawTermToFile( fclose(file); } -std::shared_ptr termToKorePattern(block *subject) { +std::shared_ptr +sortedTermToKorePattern(block *subject, const char *sort) { + auto is_kitem = (std::string(sort) == "SortKItem{}"); + block *term = is_kitem ? subject : constructRawTerm(subject, sort); + char *data_out; size_t size_out; - serializeConfiguration(subject, "SortKItem{}", &data_out, &size_out, true); - return deserialize_pattern(data_out, data_out + size_out); + serializeConfiguration(term, "SortKItem{}", &data_out, &size_out, true); + return deserialize_pattern(data_out, data_out + size_out, true); +} + +std::shared_ptr termToKorePattern(block *subject) { + return sortedTermToKorePattern(subject, "SortKItem{}"); }