Use new symbol-overload(_, _) attribute (#984)

Following runtimeverification/k#3989, the KORE attribute that encodes "this axiom declares an overload equality over two symbols `X` and `Y`" is being gradually renamed from `overload(_,_)` to `symbol-overload(_,_)`. This PR moves the LLVM backend over to accepting the new attribute rather than the old one; doing so is a simple renaming process on the attribute following #983. The checked-in KORE test files are updated by a simple renaming of the attribute.[^1] ~~Blocked on: #983~~ [^1]: See #987; it's a pain to regenerate all the KORE at the moment so I've edited the files manually using `sed` rather than the actual K frontend. This is fine for this case in the frontend, but in the future if we make more complex changes to the structure of compiled KORE definitions we should implement a more robust way of rebuilding the test suite to pin against a particular frontend version.
runtimeverification · Feb 16, 2024 · 95ab61e · 95ab61e
1 parent c4675e2
commit 95ab61e
Show file tree

Hide file tree

Showing 11 changed files with 40 additions and 38 deletions.
diff --git a/include/kllvm/ast/attribute_set.h b/include/kllvm/ast/attribute_set.h
@@ -58,14 +58,14 @@ class attribute_set {
     macro_rec,
     nat,
     non_executable,
-    overload,
     priorities,
     priority,
     right,
     simplification,
     sort_injection,
     source,
     subsort,
+    symbol_overload,
     terminals,
     total,
     unit,

diff --git a/lib/ast/attribute_set.cpp b/lib/ast/attribute_set.cpp
@@ -35,7 +35,6 @@ std::unordered_map<attribute_set::key, std::string> const &attribute_table() {
       {attribute_set::key::macro_rec, "macro-rec"},
       {attribute_set::key::nat, "nat"},
       {attribute_set::key::non_executable, "non-executable"},
-      {attribute_set::key::overload, "overload"},
       {attribute_set::key::priorities, "priorities"},
       {attribute_set::key::priority, "priority"},
       {attribute_set::key::right, "right"},
@@ -44,6 +43,7 @@ std::unordered_map<attribute_set::key, std::string> const &attribute_table() {
       {attribute_set::key::source,
        "org'Stop'kframework'Stop'attributes'Stop'Source"},
       {attribute_set::key::subsort, "subsort"},
+      {attribute_set::key::symbol_overload, "symbol-overload"},
       {attribute_set::key::terminals, "terminals"},
       {attribute_set::key::total, "total"},
       {attribute_set::key::unit, "unit"},

diff --git a/lib/ast/definition.cpp b/lib/ast/definition.cpp
@@ -1,5 +1,6 @@
 #include <kllvm/ast/AST.h>
 
+#include <iostream>
 #include <string>
 #include <unordered_set>
 
@@ -97,8 +98,9 @@ SymbolMap KOREDefinition::getOverloads() const {
   auto overloads = SymbolMap{};
 
   for (auto *axiom : axioms) {
-    if (axiom->attributes().contains(attribute_set::key::overload)) {
-      auto const &att = axiom->attributes().get(attribute_set::key::overload);
+    if (axiom->attributes().contains(attribute_set::key::symbol_overload)) {
+      auto const &att
+          = axiom->attributes().get(attribute_set::key::symbol_overload);
       auto *innerSymbol = std::dynamic_pointer_cast<KORECompositePattern>(
                               att->getArguments()[1])
                               ->getConstructor();

diff --git a/matching/src/main/scala/org/kframework/backend/llvm/matching/Parser.scala b/matching/src/main/scala/org/kframework/backend/llvm/matching/Parser.scala
@@ -422,8 +422,8 @@ object Parser {
       Seq()
     }
     axioms
-      .filter(hasAtt(_, "overload"))
-      .map(getAtt(_, "overload") match {
+      .filter(hasAtt(_, "symbol-overload"))
+      .map(getAtt(_, "symbol-overload") match {
         case Some(Application(_, args)) =>
           assert(args.size == 2)
           (args.head, args(1)) match {

diff --git a/test/defn/kool-static.kore b/test/defn/kool-static.kore
@@ -6570,8 +6570,8 @@ module KOOL-TYPED-STATIC
   axiom{} \or{SortGeneratedTopCellFragment{}} (\exists{SortGeneratedTopCellFragment{}} (X0:SortTCellOpt{}, \exists{SortGeneratedTopCellFragment{}} (X1:SortOutputCellOpt{}, Lbl'-LT-'generatedTop'-GT-'-fragment{}(X0:SortTCellOpt{}, X1:SortOutputCellOpt{}))), \bottom{SortGeneratedTopCellFragment{}}()) [constructor{}()] // no junk
   axiom{} \or{SortReturnTypeCell{}} (Lbl'Stop'ReturnTypeCell{}(), \or{SortReturnTypeCell{}} (\exists{SortReturnTypeCell{}} (X0:SortType{}, Lbl'-LT-'returnType'-GT-'{}(X0:SortType{})), \bottom{SortReturnTypeCell{}}())) [constructor{}()] // no junk
   axiom{} \or{SortIOError{}} (Lbl'Hash'E2BIG{}(), \or{SortIOError{}} (Lbl'Hash'EACCES{}(), \or{SortIOError{}} (Lbl'Hash'EADDRINUSE{}(), \or{SortIOError{}} (Lbl'Hash'EADDRNOTAVAIL{}(), \or{SortIOError{}} (Lbl'Hash'EAFNOSUPPORT{}(), \or{SortIOError{}} (Lbl'Hash'EAGAIN{}(), \or{SortIOError{}} (Lbl'Hash'EALREADY{}(), \or{SortIOError{}} (Lbl'Hash'EBADF{}(), \or{SortIOError{}} (Lbl'Hash'EBUSY{}(), \or{SortIOError{}} (Lbl'Hash'ECHILD{}(), \or{SortIOError{}} (Lbl'Hash'ECONNABORTED{}(), \or{SortIOError{}} (Lbl'Hash'ECONNREFUSED{}(), \or{SortIOError{}} (Lbl'Hash'ECONNRESET{}(), \or{SortIOError{}} (Lbl'Hash'EDEADLK{}(), \or{SortIOError{}} (Lbl'Hash'EDESTADDRREQ{}(), \or{SortIOError{}} (Lbl'Hash'EDOM{}(), \or{SortIOError{}} (Lbl'Hash'EEXIST{}(), \or{SortIOError{}} (Lbl'Hash'EFAULT{}(), \or{SortIOError{}} (Lbl'Hash'EFBIG{}(), \or{SortIOError{}} (Lbl'Hash'EHOSTDOWN{}(), \or{SortIOError{}} (Lbl'Hash'EHOSTUNREACH{}(), \or{SortIOError{}} (Lbl'Hash'EINPROGRESS{}(), \or{SortIOError{}} (Lbl'Hash'EINTR{}(), \or{SortIOError{}} (Lbl'Hash'EINVAL{}(), \or{SortIOError{}} (Lbl'Hash'EIO{}(), \or{SortIOError{}} (Lbl'Hash'EISCONN{}(), \or{SortIOError{}} (Lbl'Hash'EISDIR{}(), \or{SortIOError{}} (Lbl'Hash'ELOOP{}(), \or{SortIOError{}} (Lbl'Hash'EMFILE{}(), \or{SortIOError{}} (Lbl'Hash'EMLINK{}(), \or{SortIOError{}} (Lbl'Hash'EMSGSIZE{}(), \or{SortIOError{}} (Lbl'Hash'ENAMETOOLONG{}(), \or{SortIOError{}} (Lbl'Hash'ENETDOWN{}(), \or{SortIOError{}} (Lbl'Hash'ENETRESET{}(), \or{SortIOError{}} (Lbl'Hash'ENETUNREACH{}(), \or{SortIOError{}} (Lbl'Hash'ENFILE{}(), \or{SortIOError{}} (Lbl'Hash'ENOBUFS{}(), \or{SortIOError{}} (Lbl'Hash'ENODEV{}(), \or{SortIOError{}} (Lbl'Hash'ENOENT{}(), \or{SortIOError{}} (Lbl'Hash'ENOEXEC{}(), \or{SortIOError{}} (Lbl'Hash'ENOLCK{}(), \or{SortIOError{}} (Lbl'Hash'ENOMEM{}(), \or{SortIOError{}} (Lbl'Hash'ENOPROTOOPT{}(), \or{SortIOError{}} (Lbl'Hash'ENOSPC{}(), \or{SortIOError{}} (Lbl'Hash'ENOSYS{}(), \or{SortIOError{}} (Lbl'Hash'ENOTCONN{}(), \or{SortIOError{}} (Lbl'Hash'ENOTDIR{}(), \or{SortIOError{}} (Lbl'Hash'ENOTEMPTY{}(), \or{SortIOError{}} (Lbl'Hash'ENOTSOCK{}(), \or{SortIOError{}} (Lbl'Hash'ENOTTY{}(), \or{SortIOError{}} (Lbl'Hash'ENXIO{}(), \or{SortIOError{}} (Lbl'Hash'EOF{}(), \or{SortIOError{}} (Lbl'Hash'EOPNOTSUPP{}(), \or{SortIOError{}} (Lbl'Hash'EOVERFLOW{}(), \or{SortIOError{}} (Lbl'Hash'EPERM{}(), \or{SortIOError{}} (Lbl'Hash'EPFNOSUPPORT{}(), \or{SortIOError{}} (Lbl'Hash'EPIPE{}(), \or{SortIOError{}} (Lbl'Hash'EPROTONOSUPPORT{}(), \or{SortIOError{}} (Lbl'Hash'EPROTOTYPE{}(), \or{SortIOError{}} (Lbl'Hash'ERANGE{}(), \or{SortIOError{}} (Lbl'Hash'EROFS{}(), \or{SortIOError{}} (Lbl'Hash'ESHUTDOWN{}(), \or{SortIOError{}} (Lbl'Hash'ESOCKTNOSUPPORT{}(), \or{SortIOError{}} (Lbl'Hash'ESPIPE{}(), \or{SortIOError{}} (Lbl'Hash'ESRCH{}(), \or{SortIOError{}} (Lbl'Hash'ETIMEDOUT{}(), \or{SortIOError{}} (Lbl'Hash'ETOOMANYREFS{}(), \or{SortIOError{}} (Lbl'Hash'EWOULDBLOCK{}(), \or{SortIOError{}} (Lbl'Hash'EXDEV{}(), \or{SortIOError{}} (\exists{SortIOError{}} (X0:SortString{}, Lbl'Hash'noParse{}(X0:SortString{})), \or{SortIOError{}} (\exists{SortIOError{}} (X0:SortInt{}, Lbl'Hash'unknownIOError{}(X0:SortInt{})), \bottom{SortIOError{}}()))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) [constructor{}()] // no junk
-  axiom{R} \equals{SortExps{}, R} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'KOOL-TYPED-STATIC-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps'QuotRBraUnds'Exps{}(), inj{SortTypes{}, SortExps{}} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'KOOL-TYPED-STATIC-SYNTAX'Unds'Types'Unds'Type'Unds'Types'QuotRBraUnds'Types{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsCommUndsUnds'KOOL-TYPED-STATIC-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps'QuotRBraUnds'Exps{}(), Lbl'Stop'List'LBraQuotUndsCommUndsUnds'KOOL-TYPED-STATIC-SYNTAX'Unds'Types'Unds'Type'Unds'Types'QuotRBraUnds'Types{}())] // overloaded production
-  axiom{R} \equals{SortExps{}, R} (Lbl'UndsCommUndsUnds'KOOL-TYPED-STATIC-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(inj{SortType{}, SortExp{}} (K0:SortType{}),inj{SortTypes{}, SortExps{}} (K1:SortTypes{})), inj{SortTypes{}, SortExps{}} (Lbl'UndsCommUndsUnds'KOOL-TYPED-STATIC-SYNTAX'Unds'Types'Unds'Type'Unds'Types{}(K0:SortType{},K1:SortTypes{}))) [overload{}(Lbl'UndsCommUndsUnds'KOOL-TYPED-STATIC-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(), Lbl'UndsCommUndsUnds'KOOL-TYPED-STATIC-SYNTAX'Unds'Types'Unds'Type'Unds'Types{}())] // overloaded production
+  axiom{R} \equals{SortExps{}, R} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'KOOL-TYPED-STATIC-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps'QuotRBraUnds'Exps{}(), inj{SortTypes{}, SortExps{}} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'KOOL-TYPED-STATIC-SYNTAX'Unds'Types'Unds'Type'Unds'Types'QuotRBraUnds'Types{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsCommUndsUnds'KOOL-TYPED-STATIC-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps'QuotRBraUnds'Exps{}(), Lbl'Stop'List'LBraQuotUndsCommUndsUnds'KOOL-TYPED-STATIC-SYNTAX'Unds'Types'Unds'Type'Unds'Types'QuotRBraUnds'Types{}())] // overloaded production
+  axiom{R} \equals{SortExps{}, R} (Lbl'UndsCommUndsUnds'KOOL-TYPED-STATIC-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(inj{SortType{}, SortExp{}} (K0:SortType{}),inj{SortTypes{}, SortExps{}} (K1:SortTypes{})), inj{SortTypes{}, SortExps{}} (Lbl'UndsCommUndsUnds'KOOL-TYPED-STATIC-SYNTAX'Unds'Types'Unds'Type'Unds'Types{}(K0:SortType{},K1:SortTypes{}))) [symbol-overload{}(Lbl'UndsCommUndsUnds'KOOL-TYPED-STATIC-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(), Lbl'UndsCommUndsUnds'KOOL-TYPED-STATIC-SYNTAX'Unds'Types'Unds'Type'Unds'Types{}())] // overloaded production
 
 // rules
 // rule `#if_#then_#else_#fi_K-EQUAL-SYNTAX_Sort_Bool_Sort_Sort`{K}(C,B1,_Gen0)=>B1 requires C ensures #token("true","Bool") [UNIQUE_ID(2b32069ac3f589174502fa507ebc88fab7c902854c0a9baa8ab09beb551232e2), org.kframework.attributes.Location(Location(2222,8,2222,59)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework-5.0.0/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [klabel(#ruleRequires), symbol])]

diff --git a/test/defn/sk.kore b/test/defn/sk.kore
@@ -3170,8 +3170,8 @@ module LAMBDA
   axiom{} \or{SortGeneratedTopCellFragment{}} (\exists{SortGeneratedTopCellFragment{}} (X0:SortKCellOpt{}, \exists{SortGeneratedTopCellFragment{}} (X1:SortGeneratedCounterCellOpt{}, Lbl'-LT-'generatedTop'-GT-'-fragment{}(X0:SortKCellOpt{}, X1:SortGeneratedCounterCellOpt{}))), \bottom{SortGeneratedTopCellFragment{}}()) [constructor{}()] // no junk
   axiom{} \or{SortBuiltVal{}} (\exists{SortBuiltVal{}} (Val:SortBuiltTernOp{}, inj{SortBuiltTernOp{}, SortBuiltVal{}} (Val:SortBuiltTernOp{})), \or{SortBuiltVal{}} (\exists{SortBuiltVal{}} (Val:SortId{}, inj{SortId{}, SortBuiltVal{}} (Val:SortId{})), \or{SortBuiltVal{}} (\exists{SortBuiltVal{}} (Val:SortBool{}, inj{SortBool{}, SortBuiltVal{}} (Val:SortBool{})), \or{SortBuiltVal{}} (\exists{SortBuiltVal{}} (Val:SortInt{}, inj{SortInt{}, SortBuiltVal{}} (Val:SortInt{})), \or{SortBuiltVal{}} (\exists{SortBuiltVal{}} (Val:SortBuiltBinOp{}, inj{SortBuiltBinOp{}, SortBuiltVal{}} (Val:SortBuiltBinOp{})), \bottom{SortBuiltVal{}}()))))) [constructor{}()] // no junk
   axiom{} \or{SortIOError{}} (Lbl'Hash'E2BIG{}(), \or{SortIOError{}} (Lbl'Hash'EACCES{}(), \or{SortIOError{}} (Lbl'Hash'EADDRINUSE{}(), \or{SortIOError{}} (Lbl'Hash'EADDRNOTAVAIL{}(), \or{SortIOError{}} (Lbl'Hash'EAFNOSUPPORT{}(), \or{SortIOError{}} (Lbl'Hash'EAGAIN{}(), \or{SortIOError{}} (Lbl'Hash'EALREADY{}(), \or{SortIOError{}} (Lbl'Hash'EBADF{}(), \or{SortIOError{}} (Lbl'Hash'EBUSY{}(), \or{SortIOError{}} (Lbl'Hash'ECHILD{}(), \or{SortIOError{}} (Lbl'Hash'ECONNABORTED{}(), \or{SortIOError{}} (Lbl'Hash'ECONNREFUSED{}(), \or{SortIOError{}} (Lbl'Hash'ECONNRESET{}(), \or{SortIOError{}} (Lbl'Hash'EDEADLK{}(), \or{SortIOError{}} (Lbl'Hash'EDESTADDRREQ{}(), \or{SortIOError{}} (Lbl'Hash'EDOM{}(), \or{SortIOError{}} (Lbl'Hash'EEXIST{}(), \or{SortIOError{}} (Lbl'Hash'EFAULT{}(), \or{SortIOError{}} (Lbl'Hash'EFBIG{}(), \or{SortIOError{}} (Lbl'Hash'EHOSTDOWN{}(), \or{SortIOError{}} (Lbl'Hash'EHOSTUNREACH{}(), \or{SortIOError{}} (Lbl'Hash'EINPROGRESS{}(), \or{SortIOError{}} (Lbl'Hash'EINTR{}(), \or{SortIOError{}} (Lbl'Hash'EINVAL{}(), \or{SortIOError{}} (Lbl'Hash'EIO{}(), \or{SortIOError{}} (Lbl'Hash'EISCONN{}(), \or{SortIOError{}} (Lbl'Hash'EISDIR{}(), \or{SortIOError{}} (Lbl'Hash'ELOOP{}(), \or{SortIOError{}} (Lbl'Hash'EMFILE{}(), \or{SortIOError{}} (Lbl'Hash'EMLINK{}(), \or{SortIOError{}} (Lbl'Hash'EMSGSIZE{}(), \or{SortIOError{}} (Lbl'Hash'ENAMETOOLONG{}(), \or{SortIOError{}} (Lbl'Hash'ENETDOWN{}(), \or{SortIOError{}} (Lbl'Hash'ENETRESET{}(), \or{SortIOError{}} (Lbl'Hash'ENETUNREACH{}(), \or{SortIOError{}} (Lbl'Hash'ENFILE{}(), \or{SortIOError{}} (Lbl'Hash'ENOBUFS{}(), \or{SortIOError{}} (Lbl'Hash'ENODEV{}(), \or{SortIOError{}} (Lbl'Hash'ENOENT{}(), \or{SortIOError{}} (Lbl'Hash'ENOEXEC{}(), \or{SortIOError{}} (Lbl'Hash'ENOLCK{}(), \or{SortIOError{}} (Lbl'Hash'ENOMEM{}(), \or{SortIOError{}} (Lbl'Hash'ENOPROTOOPT{}(), \or{SortIOError{}} (Lbl'Hash'ENOSPC{}(), \or{SortIOError{}} (Lbl'Hash'ENOSYS{}(), \or{SortIOError{}} (Lbl'Hash'ENOTCONN{}(), \or{SortIOError{}} (Lbl'Hash'ENOTDIR{}(), \or{SortIOError{}} (Lbl'Hash'ENOTEMPTY{}(), \or{SortIOError{}} (Lbl'Hash'ENOTSOCK{}(), \or{SortIOError{}} (Lbl'Hash'ENOTTY{}(), \or{SortIOError{}} (Lbl'Hash'ENXIO{}(), \or{SortIOError{}} (Lbl'Hash'EOF{}(), \or{SortIOError{}} (Lbl'Hash'EOPNOTSUPP{}(), \or{SortIOError{}} (Lbl'Hash'EOVERFLOW{}(), \or{SortIOError{}} (Lbl'Hash'EPERM{}(), \or{SortIOError{}} (Lbl'Hash'EPFNOSUPPORT{}(), \or{SortIOError{}} (Lbl'Hash'EPIPE{}(), \or{SortIOError{}} (Lbl'Hash'EPROTONOSUPPORT{}(), \or{SortIOError{}} (Lbl'Hash'EPROTOTYPE{}(), \or{SortIOError{}} (Lbl'Hash'ERANGE{}(), \or{SortIOError{}} (Lbl'Hash'EROFS{}(), \or{SortIOError{}} (Lbl'Hash'ESHUTDOWN{}(), \or{SortIOError{}} (Lbl'Hash'ESOCKTNOSUPPORT{}(), \or{SortIOError{}} (Lbl'Hash'ESPIPE{}(), \or{SortIOError{}} (Lbl'Hash'ESRCH{}(), \or{SortIOError{}} (Lbl'Hash'ETIMEDOUT{}(), \or{SortIOError{}} (Lbl'Hash'ETOOMANYREFS{}(), \or{SortIOError{}} (Lbl'Hash'EWOULDBLOCK{}(), \or{SortIOError{}} (Lbl'Hash'EXDEV{}(), \or{SortIOError{}} (\exists{SortIOError{}} (X0:SortInt{}, Lbl'Hash'unknownIOError{}(X0:SortInt{})), \bottom{SortIOError{}}())))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) [constructor{}()] // no junk
-  axiom{R} \equals{SortExp{}, R} (Lbl'UndsUndsUnds'LAMBDA-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(inj{SortBuiltBinOp{}, SortExp{}} (K0:SortBuiltBinOp{}),inj{SortVal{}, SortExp{}} (K1:SortVal{})), inj{SortVal{}, SortExp{}} (Lbl'UndsUndsUnds'LAMBDA'Unds'Val'Unds'BuiltBinOp'Unds'Val{}(K0:SortBuiltBinOp{},K1:SortVal{}))) [overload{}(Lbl'UndsUndsUnds'LAMBDA-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(), Lbl'UndsUndsUnds'LAMBDA'Unds'Val'Unds'BuiltBinOp'Unds'Val{}())] // overloaded production
-  axiom{R} \equals{SortExp{}, R} (Lbl'UndsUndsUnds'LAMBDA-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(inj{SortBuiltTernOp{}, SortExp{}} (K0:SortBuiltTernOp{}),inj{SortVal{}, SortExp{}} (K1:SortVal{})), inj{SortBuiltBinOp{}, SortExp{}} (Lbl'UndsUndsUnds'LAMBDA'Unds'BuiltBinOp'Unds'BuiltTernOp'Unds'Val{}(K0:SortBuiltTernOp{},K1:SortVal{}))) [overload{}(Lbl'UndsUndsUnds'LAMBDA-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(), Lbl'UndsUndsUnds'LAMBDA'Unds'BuiltBinOp'Unds'BuiltTernOp'Unds'Val{}())] // overloaded production
+  axiom{R} \equals{SortExp{}, R} (Lbl'UndsUndsUnds'LAMBDA-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(inj{SortBuiltBinOp{}, SortExp{}} (K0:SortBuiltBinOp{}),inj{SortVal{}, SortExp{}} (K1:SortVal{})), inj{SortVal{}, SortExp{}} (Lbl'UndsUndsUnds'LAMBDA'Unds'Val'Unds'BuiltBinOp'Unds'Val{}(K0:SortBuiltBinOp{},K1:SortVal{}))) [symbol-overload{}(Lbl'UndsUndsUnds'LAMBDA-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(), Lbl'UndsUndsUnds'LAMBDA'Unds'Val'Unds'BuiltBinOp'Unds'Val{}())] // overloaded production
+  axiom{R} \equals{SortExp{}, R} (Lbl'UndsUndsUnds'LAMBDA-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(inj{SortBuiltTernOp{}, SortExp{}} (K0:SortBuiltTernOp{}),inj{SortVal{}, SortExp{}} (K1:SortVal{})), inj{SortBuiltBinOp{}, SortExp{}} (Lbl'UndsUndsUnds'LAMBDA'Unds'BuiltBinOp'Unds'BuiltTernOp'Unds'Val{}(K0:SortBuiltTernOp{},K1:SortVal{}))) [symbol-overload{}(Lbl'UndsUndsUnds'LAMBDA-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(), Lbl'UndsUndsUnds'LAMBDA'Unds'BuiltBinOp'Unds'BuiltTernOp'Unds'Val{}())] // overloaded production
 
 // rules
 // rule `#if_#then_#else_#fi_K-EQUAL-SYNTAX_Sort_Bool_Sort_Sort`{K}(C,B1,_Gen0)=>B1 requires C ensures #token("true","Bool") [UNIQUE_ID(2b32069ac3f589174502fa507ebc88fab7c902854c0a9baa8ab09beb551232e2), org.kframework.attributes.Location(Location(2073,8,2073,59)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework-5.0.0/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [klabel(#ruleRequires), symbol])]