From 169a35603851b0cc1534814023c5d02d5dcca84e Mon Sep 17 00:00:00 2001
From: Roberto Rosmaninho <robertogomes@dcc.ufmg.br>
Date: Fri, 26 Apr 2024 12:19:29 -0300
Subject: [PATCH] Addressing comments

---
 include/kllvm/ast/AST.h    | 15 ++++++++++++---
 lib/ast/definition.cpp     | 11 ++++++-----
 lib/codegen/CreateTerm.cpp |  2 +-
 3 files changed, 19 insertions(+), 9 deletions(-)

diff --git a/include/kllvm/ast/AST.h b/include/kllvm/ast/AST.h
index ca1658bf8..e545184d8 100644
--- a/include/kllvm/ast/AST.h
+++ b/include/kllvm/ast/AST.h
@@ -914,8 +914,8 @@ class kore_definition {
 
   kore_symbol *inj_symbol_{};
 
-  SubsortMap *subsorts_ = nullptr;
-  SubsortMap *subsorts_inverted_ = nullptr;
+  std::optional<SubsortMap> subsorts_;
+  std::optional<SubsortMap> subsorts_inverted_;
 
   /*
    * Insert symbols into this definition that have knowable labels, but cannot
@@ -967,7 +967,16 @@ class kore_definition {
    *   S |-> {T . S is a subsort of T}
    */
   [[nodiscard]] SubsortMap get_subsorts();
-  [[nodiscard]] SubsortMap get_inverted_subsorts();
+
+  /*
+   * Build this definition's inverted subsort relation from axioms that have the
+   * `subsort` attribute.
+   *
+   * The returned map is as follows:
+   *
+   * S |-> {T . S is a direct supersort of T}
+   */
+  [[nodiscard]] SubsortMap get_supersort();
 
   /*
    * Build this definition's overload relation from axioms that have the
diff --git a/lib/ast/definition.cpp b/lib/ast/definition.cpp
index a905b1399..79c32f8f9 100644
--- a/lib/ast/definition.cpp
+++ b/lib/ast/definition.cpp
@@ -106,7 +106,7 @@ void kore_definition::insert_reserved_symbols() {
 
 SubsortMap kore_definition::get_subsorts() {
 
-  if (subsorts_ != nullptr) {
+  if (subsorts_.has_value()) {
     return *subsorts_;
   }
 
@@ -123,13 +123,14 @@ SubsortMap kore_definition::get_subsorts() {
     }
   }
 
-  subsorts_ = new SubsortMap(transitive_closure(subsorts));
+  subsorts_
+      = std::optional<SubsortMap>(SubsortMap(transitive_closure(subsorts)));
   return *subsorts_;
 }
 
-SubsortMap kore_definition::get_inverted_subsorts() {
+SubsortMap kore_definition::get_supersort() {
 
-  if (subsorts_inverted_ != nullptr) {
+  if (subsorts_inverted_.has_value()) {
     return *subsorts_inverted_;
   }
 
@@ -141,7 +142,7 @@ SubsortMap kore_definition::get_inverted_subsorts() {
     }
   }
 
-  subsorts_inverted_ = new SubsortMap(inverted_subsorts);
+  subsorts_inverted_ = std::optional<SubsortMap>(SubsortMap(inverted_subsorts));
   return inverted_subsorts;
 }
 
diff --git a/lib/codegen/CreateTerm.cpp b/lib/codegen/CreateTerm.cpp
index f315dece1..4c2ce8461 100644
--- a/lib/codegen/CreateTerm.cpp
+++ b/lib/codegen/CreateTerm.cpp
@@ -956,7 +956,7 @@ std::pair<llvm::Value *, bool> create_term::create_allocation(
         = dynamic_cast<kore_composite_sort *>(symbol->get_arguments()[0].get());
         symbol_decl->attributes().contains(attribute_set::key::SortInjection)
         && (sort->get_category(definition_).cat == sort_category::Symbol)
-        && definition_->get_inverted_subsorts()[sort].empty()) {
+        && definition_->get_supersort()[sort].empty()) {
       std::pair<llvm::Value *, bool> val = create_allocation(
           constructor->get_arguments()[0].get(), location_stack);
       if (val.second) {