diff --git a/include/kllvm/ast/attribute_set.h b/include/kllvm/ast/attribute_set.h index fedcc0589..d8a1f9da9 100644 --- a/include/kllvm/ast/attribute_set.h +++ b/include/kllvm/ast/attribute_set.h @@ -58,7 +58,6 @@ class attribute_set { macro_rec, nat, non_executable, - overload, priorities, priority, right, @@ -66,6 +65,7 @@ class attribute_set { sort_injection, source, subsort, + symbol_overload, terminals, total, unit, diff --git a/lib/ast/attribute_set.cpp b/lib/ast/attribute_set.cpp index cbff96131..893e890d8 100644 --- a/lib/ast/attribute_set.cpp +++ b/lib/ast/attribute_set.cpp @@ -35,7 +35,6 @@ std::unordered_map 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 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 index e3a25cdf5..5858dfb04 100644 --- a/lib/ast/definition.cpp +++ b/lib/ast/definition.cpp @@ -1,5 +1,6 @@ #include +#include #include #include @@ -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( 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 index d3aa8e1bf..5a4271b1a 100644 --- 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 index 0725a672e..52cb41bb1 100644 --- 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 index bb2ca989d..ecc756712 100644 --- 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])] diff --git a/test/defn/test10.kore b/test/defn/test10.kore index 4bdea0d8d..a25c925ef 100644 --- a/test/defn/test10.kore +++ b/test/defn/test10.kore @@ -371,12 +371,12 @@ module TEST 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{SortOperand{}} (\exists{SortOperand{}} (Val:SortInt{}, inj{SortInt{}, SortOperand{}} (Val:SortInt{})), \bottom{SortOperand{}}()) [constructor{}()] // no junk axiom{} \or{SortNEInts{}} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'NEInts'Unds'Int'Unds'NEInts'QuotRBraUnds'NEInts{}(), \or{SortNEInts{}} (\exists{SortNEInts{}} (X0:SortInt{}, \exists{SortNEInts{}} (X1:SortNEInts{}, Lbl'UndsCommUndsUnds'TEST'Unds'NEInts'Unds'Int'Unds'NEInts{}(X0:SortInt{}, X1:SortNEInts{}))), \bottom{SortNEInts{}}())) [constructor{}()] // no junk - axiom{R} \equals{SortOperands{}, R} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'Operands'Unds'Operand'Unds'Operands'QuotRBraUnds'Operands{}(), inj{SortNEInts{}, SortOperands{}} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'NEInts'Unds'Int'Unds'NEInts'QuotRBraUnds'NEInts{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'Operands'Unds'Operand'Unds'Operands'QuotRBraUnds'Operands{}(), Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'NEInts'Unds'Int'Unds'NEInts'QuotRBraUnds'NEInts{}())] // overloaded production - axiom{R} \equals{SortInts{}, R} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'Ints'Unds'Int'Unds'Ints'QuotRBraUnds'Ints{}(), inj{SortNEInts{}, SortInts{}} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'NEInts'Unds'Int'Unds'NEInts'QuotRBraUnds'NEInts{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'Ints'Unds'Int'Unds'Ints'QuotRBraUnds'Ints{}(), Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'NEInts'Unds'Int'Unds'NEInts'QuotRBraUnds'NEInts{}())] // overloaded production - axiom{R} \equals{SortOperands{}, R} (Lbl'UndsCommUndsUnds'TEST'Unds'Operands'Unds'Operand'Unds'Operands{}(inj{SortInt{}, SortOperand{}} (K0:SortInt{}),inj{SortInts{}, SortOperands{}} (K1:SortInts{})), inj{SortInts{}, SortOperands{}} (Lbl'UndsCommUndsUnds'TEST'Unds'Ints'Unds'Int'Unds'Ints{}(K0:SortInt{},K1:SortInts{}))) [overload{}(Lbl'UndsCommUndsUnds'TEST'Unds'Operands'Unds'Operand'Unds'Operands{}(), Lbl'UndsCommUndsUnds'TEST'Unds'Ints'Unds'Int'Unds'Ints{}())] // overloaded production - axiom{R} \equals{SortOperands{}, R} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'Operands'Unds'Operand'Unds'Operands'QuotRBraUnds'Operands{}(), inj{SortInts{}, SortOperands{}} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'Ints'Unds'Int'Unds'Ints'QuotRBraUnds'Ints{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'Operands'Unds'Operand'Unds'Operands'QuotRBraUnds'Operands{}(), Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'Ints'Unds'Int'Unds'Ints'QuotRBraUnds'Ints{}())] // overloaded production - axiom{R} \equals{SortInts{}, R} (Lbl'UndsCommUndsUnds'TEST'Unds'Ints'Unds'Int'Unds'Ints{}(K0:SortInt{},inj{SortNEInts{}, SortInts{}} (K1:SortNEInts{})), inj{SortNEInts{}, SortInts{}} (Lbl'UndsCommUndsUnds'TEST'Unds'NEInts'Unds'Int'Unds'NEInts{}(K0:SortInt{},K1:SortNEInts{}))) [overload{}(Lbl'UndsCommUndsUnds'TEST'Unds'Ints'Unds'Int'Unds'Ints{}(), Lbl'UndsCommUndsUnds'TEST'Unds'NEInts'Unds'Int'Unds'NEInts{}())] // overloaded production - axiom{R} \equals{SortOperands{}, R} (Lbl'UndsCommUndsUnds'TEST'Unds'Operands'Unds'Operand'Unds'Operands{}(inj{SortInt{}, SortOperand{}} (K0:SortInt{}),inj{SortNEInts{}, SortOperands{}} (K1:SortNEInts{})), inj{SortNEInts{}, SortOperands{}} (Lbl'UndsCommUndsUnds'TEST'Unds'NEInts'Unds'Int'Unds'NEInts{}(K0:SortInt{},K1:SortNEInts{}))) [overload{}(Lbl'UndsCommUndsUnds'TEST'Unds'Operands'Unds'Operand'Unds'Operands{}(), Lbl'UndsCommUndsUnds'TEST'Unds'NEInts'Unds'Int'Unds'NEInts{}())] // overloaded production + axiom{R} \equals{SortOperands{}, R} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'Operands'Unds'Operand'Unds'Operands'QuotRBraUnds'Operands{}(), inj{SortNEInts{}, SortOperands{}} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'NEInts'Unds'Int'Unds'NEInts'QuotRBraUnds'NEInts{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'Operands'Unds'Operand'Unds'Operands'QuotRBraUnds'Operands{}(), Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'NEInts'Unds'Int'Unds'NEInts'QuotRBraUnds'NEInts{}())] // overloaded production + axiom{R} \equals{SortInts{}, R} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'Ints'Unds'Int'Unds'Ints'QuotRBraUnds'Ints{}(), inj{SortNEInts{}, SortInts{}} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'NEInts'Unds'Int'Unds'NEInts'QuotRBraUnds'NEInts{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'Ints'Unds'Int'Unds'Ints'QuotRBraUnds'Ints{}(), Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'NEInts'Unds'Int'Unds'NEInts'QuotRBraUnds'NEInts{}())] // overloaded production + axiom{R} \equals{SortOperands{}, R} (Lbl'UndsCommUndsUnds'TEST'Unds'Operands'Unds'Operand'Unds'Operands{}(inj{SortInt{}, SortOperand{}} (K0:SortInt{}),inj{SortInts{}, SortOperands{}} (K1:SortInts{})), inj{SortInts{}, SortOperands{}} (Lbl'UndsCommUndsUnds'TEST'Unds'Ints'Unds'Int'Unds'Ints{}(K0:SortInt{},K1:SortInts{}))) [symbol-overload{}(Lbl'UndsCommUndsUnds'TEST'Unds'Operands'Unds'Operand'Unds'Operands{}(), Lbl'UndsCommUndsUnds'TEST'Unds'Ints'Unds'Int'Unds'Ints{}())] // overloaded production + axiom{R} \equals{SortOperands{}, R} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'Operands'Unds'Operand'Unds'Operands'QuotRBraUnds'Operands{}(), inj{SortInts{}, SortOperands{}} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'Ints'Unds'Int'Unds'Ints'QuotRBraUnds'Ints{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'Operands'Unds'Operand'Unds'Operands'QuotRBraUnds'Operands{}(), Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'Ints'Unds'Int'Unds'Ints'QuotRBraUnds'Ints{}())] // overloaded production + axiom{R} \equals{SortInts{}, R} (Lbl'UndsCommUndsUnds'TEST'Unds'Ints'Unds'Int'Unds'Ints{}(K0:SortInt{},inj{SortNEInts{}, SortInts{}} (K1:SortNEInts{})), inj{SortNEInts{}, SortInts{}} (Lbl'UndsCommUndsUnds'TEST'Unds'NEInts'Unds'Int'Unds'NEInts{}(K0:SortInt{},K1:SortNEInts{}))) [symbol-overload{}(Lbl'UndsCommUndsUnds'TEST'Unds'Ints'Unds'Int'Unds'Ints{}(), Lbl'UndsCommUndsUnds'TEST'Unds'NEInts'Unds'Int'Unds'NEInts{}())] // overloaded production + axiom{R} \equals{SortOperands{}, R} (Lbl'UndsCommUndsUnds'TEST'Unds'Operands'Unds'Operand'Unds'Operands{}(inj{SortInt{}, SortOperand{}} (K0:SortInt{}),inj{SortNEInts{}, SortOperands{}} (K1:SortNEInts{})), inj{SortNEInts{}, SortOperands{}} (Lbl'UndsCommUndsUnds'TEST'Unds'NEInts'Unds'Int'Unds'NEInts{}(K0:SortInt{},K1:SortNEInts{}))) [symbol-overload{}(Lbl'UndsCommUndsUnds'TEST'Unds'Operands'Unds'Operand'Unds'Operands{}(), Lbl'UndsCommUndsUnds'TEST'Unds'NEInts'Unds'Int'Unds'NEInts{}())] // 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])] diff --git a/test/defn/test33.kore b/test/defn/test33.kore index 0e0c7de11..b24a65660 100644 --- a/test/defn/test33.kore +++ b/test/defn/test33.kore @@ -6888,8 +6888,8 @@ module KOOL-UNTYPED axiom{} \or{SortGeneratedTopCellFragment{}} (\exists{SortGeneratedTopCellFragment{}} (X0:SortTCellOpt{}, \exists{SortGeneratedTopCellFragment{}} (X1:SortGeneratedCounterCellOpt{}, Lbl'-LT-'generatedTop'-GT-'-fragment{}(X0:SortTCellOpt{}, X1:SortGeneratedCounterCellOpt{}))), \bottom{SortGeneratedTopCellFragment{}}()) [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{} \or{SortCrntClassCell{}} (\exists{SortCrntClassCell{}} (X0:SortId{}, Lbl'-LT-'crntClass'-GT-'{}(X0:SortId{})), \bottom{SortCrntClassCell{}}()) [constructor{}()] // no junk - axiom{R} \equals{SortExps{}, R} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'KOOL-UNTYPED-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps'QuotRBraUnds'Exps{}(), inj{SortVals{}, SortExps{}} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'KOOL-UNTYPED-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsCommUndsUnds'KOOL-UNTYPED-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps'QuotRBraUnds'Exps{}(), Lbl'Stop'List'LBraQuotUndsCommUndsUnds'KOOL-UNTYPED-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}())] // overloaded production - axiom{R} \equals{SortExps{}, R} (Lbl'UndsCommUndsUnds'KOOL-UNTYPED-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(inj{SortVal{}, SortExp{}} (K0:SortVal{}),inj{SortVals{}, SortExps{}} (K1:SortVals{})), inj{SortVals{}, SortExps{}} (Lbl'UndsCommUndsUnds'KOOL-UNTYPED-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals{}(K0:SortVal{},K1:SortVals{}))) [overload{}(Lbl'UndsCommUndsUnds'KOOL-UNTYPED-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(), Lbl'UndsCommUndsUnds'KOOL-UNTYPED-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals{}())] // overloaded production + axiom{R} \equals{SortExps{}, R} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'KOOL-UNTYPED-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps'QuotRBraUnds'Exps{}(), inj{SortVals{}, SortExps{}} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'KOOL-UNTYPED-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsCommUndsUnds'KOOL-UNTYPED-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps'QuotRBraUnds'Exps{}(), Lbl'Stop'List'LBraQuotUndsCommUndsUnds'KOOL-UNTYPED-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}())] // overloaded production + axiom{R} \equals{SortExps{}, R} (Lbl'UndsCommUndsUnds'KOOL-UNTYPED-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(inj{SortVal{}, SortExp{}} (K0:SortVal{}),inj{SortVals{}, SortExps{}} (K1:SortVals{})), inj{SortVals{}, SortExps{}} (Lbl'UndsCommUndsUnds'KOOL-UNTYPED-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals{}(K0:SortVal{},K1:SortVals{}))) [symbol-overload{}(Lbl'UndsCommUndsUnds'KOOL-UNTYPED-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(), Lbl'UndsCommUndsUnds'KOOL-UNTYPED-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals{}())] // 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])] diff --git a/test/defn/test9.kore b/test/defn/test9.kore index 2df21473f..17a1e50d0 100644 --- a/test/defn/test9.kore +++ b/test/defn/test9.kore @@ -370,12 +370,12 @@ module TEST 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{SortOperand{}} (\exists{SortOperand{}} (Val:SortInt{}, inj{SortInt{}, SortOperand{}} (Val:SortInt{})), \bottom{SortOperand{}}()) [constructor{}()] // no junk axiom{} \or{SortNEInts{}} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'NEInts'Unds'Int'Unds'NEInts'QuotRBraUnds'NEInts{}(), \or{SortNEInts{}} (\exists{SortNEInts{}} (X0:SortInt{}, \exists{SortNEInts{}} (X1:SortNEInts{}, Lbl'UndsCommUndsUnds'TEST'Unds'NEInts'Unds'Int'Unds'NEInts{}(X0:SortInt{}, X1:SortNEInts{}))), \bottom{SortNEInts{}}())) [constructor{}()] // no junk - axiom{R} \equals{SortOperands{}, R} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'Operands'Unds'Operand'Unds'Operands'QuotRBraUnds'Operands{}(), inj{SortNEInts{}, SortOperands{}} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'NEInts'Unds'Int'Unds'NEInts'QuotRBraUnds'NEInts{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'Operands'Unds'Operand'Unds'Operands'QuotRBraUnds'Operands{}(), Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'NEInts'Unds'Int'Unds'NEInts'QuotRBraUnds'NEInts{}())] // overloaded production - axiom{R} \equals{SortInts{}, R} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'Ints'Unds'Int'Unds'Ints'QuotRBraUnds'Ints{}(), inj{SortNEInts{}, SortInts{}} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'NEInts'Unds'Int'Unds'NEInts'QuotRBraUnds'NEInts{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'Ints'Unds'Int'Unds'Ints'QuotRBraUnds'Ints{}(), Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'NEInts'Unds'Int'Unds'NEInts'QuotRBraUnds'NEInts{}())] // overloaded production - axiom{R} \equals{SortOperands{}, R} (Lbl'UndsCommUndsUnds'TEST'Unds'Operands'Unds'Operand'Unds'Operands{}(inj{SortInt{}, SortOperand{}} (K0:SortInt{}),inj{SortInts{}, SortOperands{}} (K1:SortInts{})), inj{SortInts{}, SortOperands{}} (Lbl'UndsCommUndsUnds'TEST'Unds'Ints'Unds'Int'Unds'Ints{}(K0:SortInt{},K1:SortInts{}))) [overload{}(Lbl'UndsCommUndsUnds'TEST'Unds'Operands'Unds'Operand'Unds'Operands{}(), Lbl'UndsCommUndsUnds'TEST'Unds'Ints'Unds'Int'Unds'Ints{}())] // overloaded production - axiom{R} \equals{SortOperands{}, R} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'Operands'Unds'Operand'Unds'Operands'QuotRBraUnds'Operands{}(), inj{SortInts{}, SortOperands{}} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'Ints'Unds'Int'Unds'Ints'QuotRBraUnds'Ints{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'Operands'Unds'Operand'Unds'Operands'QuotRBraUnds'Operands{}(), Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'Ints'Unds'Int'Unds'Ints'QuotRBraUnds'Ints{}())] // overloaded production - axiom{R} \equals{SortInts{}, R} (Lbl'UndsCommUndsUnds'TEST'Unds'Ints'Unds'Int'Unds'Ints{}(K0:SortInt{},inj{SortNEInts{}, SortInts{}} (K1:SortNEInts{})), inj{SortNEInts{}, SortInts{}} (Lbl'UndsCommUndsUnds'TEST'Unds'NEInts'Unds'Int'Unds'NEInts{}(K0:SortInt{},K1:SortNEInts{}))) [overload{}(Lbl'UndsCommUndsUnds'TEST'Unds'Ints'Unds'Int'Unds'Ints{}(), Lbl'UndsCommUndsUnds'TEST'Unds'NEInts'Unds'Int'Unds'NEInts{}())] // overloaded production - axiom{R} \equals{SortOperands{}, R} (Lbl'UndsCommUndsUnds'TEST'Unds'Operands'Unds'Operand'Unds'Operands{}(inj{SortInt{}, SortOperand{}} (K0:SortInt{}),inj{SortNEInts{}, SortOperands{}} (K1:SortNEInts{})), inj{SortNEInts{}, SortOperands{}} (Lbl'UndsCommUndsUnds'TEST'Unds'NEInts'Unds'Int'Unds'NEInts{}(K0:SortInt{},K1:SortNEInts{}))) [overload{}(Lbl'UndsCommUndsUnds'TEST'Unds'Operands'Unds'Operand'Unds'Operands{}(), Lbl'UndsCommUndsUnds'TEST'Unds'NEInts'Unds'Int'Unds'NEInts{}())] // overloaded production + axiom{R} \equals{SortOperands{}, R} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'Operands'Unds'Operand'Unds'Operands'QuotRBraUnds'Operands{}(), inj{SortNEInts{}, SortOperands{}} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'NEInts'Unds'Int'Unds'NEInts'QuotRBraUnds'NEInts{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'Operands'Unds'Operand'Unds'Operands'QuotRBraUnds'Operands{}(), Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'NEInts'Unds'Int'Unds'NEInts'QuotRBraUnds'NEInts{}())] // overloaded production + axiom{R} \equals{SortInts{}, R} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'Ints'Unds'Int'Unds'Ints'QuotRBraUnds'Ints{}(), inj{SortNEInts{}, SortInts{}} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'NEInts'Unds'Int'Unds'NEInts'QuotRBraUnds'NEInts{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'Ints'Unds'Int'Unds'Ints'QuotRBraUnds'Ints{}(), Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'NEInts'Unds'Int'Unds'NEInts'QuotRBraUnds'NEInts{}())] // overloaded production + axiom{R} \equals{SortOperands{}, R} (Lbl'UndsCommUndsUnds'TEST'Unds'Operands'Unds'Operand'Unds'Operands{}(inj{SortInt{}, SortOperand{}} (K0:SortInt{}),inj{SortInts{}, SortOperands{}} (K1:SortInts{})), inj{SortInts{}, SortOperands{}} (Lbl'UndsCommUndsUnds'TEST'Unds'Ints'Unds'Int'Unds'Ints{}(K0:SortInt{},K1:SortInts{}))) [symbol-overload{}(Lbl'UndsCommUndsUnds'TEST'Unds'Operands'Unds'Operand'Unds'Operands{}(), Lbl'UndsCommUndsUnds'TEST'Unds'Ints'Unds'Int'Unds'Ints{}())] // overloaded production + axiom{R} \equals{SortOperands{}, R} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'Operands'Unds'Operand'Unds'Operands'QuotRBraUnds'Operands{}(), inj{SortInts{}, SortOperands{}} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'Ints'Unds'Int'Unds'Ints'QuotRBraUnds'Ints{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'Operands'Unds'Operand'Unds'Operands'QuotRBraUnds'Operands{}(), Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST'Unds'Ints'Unds'Int'Unds'Ints'QuotRBraUnds'Ints{}())] // overloaded production + axiom{R} \equals{SortInts{}, R} (Lbl'UndsCommUndsUnds'TEST'Unds'Ints'Unds'Int'Unds'Ints{}(K0:SortInt{},inj{SortNEInts{}, SortInts{}} (K1:SortNEInts{})), inj{SortNEInts{}, SortInts{}} (Lbl'UndsCommUndsUnds'TEST'Unds'NEInts'Unds'Int'Unds'NEInts{}(K0:SortInt{},K1:SortNEInts{}))) [symbol-overload{}(Lbl'UndsCommUndsUnds'TEST'Unds'Ints'Unds'Int'Unds'Ints{}(), Lbl'UndsCommUndsUnds'TEST'Unds'NEInts'Unds'Int'Unds'NEInts{}())] // overloaded production + axiom{R} \equals{SortOperands{}, R} (Lbl'UndsCommUndsUnds'TEST'Unds'Operands'Unds'Operand'Unds'Operands{}(inj{SortInt{}, SortOperand{}} (K0:SortInt{}),inj{SortNEInts{}, SortOperands{}} (K1:SortNEInts{})), inj{SortNEInts{}, SortOperands{}} (Lbl'UndsCommUndsUnds'TEST'Unds'NEInts'Unds'Int'Unds'NEInts{}(K0:SortInt{},K1:SortNEInts{}))) [symbol-overload{}(Lbl'UndsCommUndsUnds'TEST'Unds'Operands'Unds'Operand'Unds'Operands{}(), Lbl'UndsCommUndsUnds'TEST'Unds'NEInts'Unds'Int'Unds'NEInts{}())] // 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])] diff --git a/test/defn/wasm.kore b/test/defn/wasm.kore index a189d5977..c850ec758 100644 --- a/test/defn/wasm.kore +++ b/test/defn/wasm.kore @@ -5215,18 +5215,18 @@ module WASM-TEST axiom{} \or{SortCvti64Op{}} (LblaConvert'Unds'i64'Unds's{}(), \or{SortCvti64Op{}} (LblaConvert'Unds'i64'Unds'u{}(), \or{SortCvti64Op{}} (LblaWrap'Unds'i64{}(), \bottom{SortCvti64Op{}}()))) [constructor{}()] // no junk axiom{} \or{SortMmaxCell{}} (\exists{SortMmaxCell{}} (X0:SortOptionalInt{}, Lbl'-LT-'mmax'-GT-'{}(X0:SortOptionalInt{})), \bottom{SortMmaxCell{}}()) [constructor{}()] // no junk axiom{} \or{SortTextFormatGlobalType{}} (\exists{SortTextFormatGlobalType{}} (X0:SortValType{}, Lbl'LPar'mut'UndsRParUnds'WASM-TEXT-COMMON-SYNTAX'Unds'TextFormatGlobalType'Unds'ValType{}(X0:SortValType{})), \or{SortTextFormatGlobalType{}} (\exists{SortTextFormatGlobalType{}} (Val:SortValType{}, inj{SortValType{}, SortTextFormatGlobalType{}} (Val:SortValType{})), \or{SortTextFormatGlobalType{}} (\exists{SortTextFormatGlobalType{}} (Val:SortFValType{}, inj{SortFValType{}, SortTextFormatGlobalType{}} (Val:SortFValType{})), \or{SortTextFormatGlobalType{}} (\exists{SortTextFormatGlobalType{}} (Val:SortIValType{}, inj{SortIValType{}, SortTextFormatGlobalType{}} (Val:SortIValType{})), \bottom{SortTextFormatGlobalType{}}())))) [constructor{}()] // no junk - axiom{R} \equals{SortStmts{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(inj{SortInstr{}, SortStmt{}} (K0:SortInstr{}),inj{SortInstrs{}, SortStmts{}} (K1:SortInstrs{})), inj{SortInstrs{}, SortStmts{}} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}(K0:SortInstr{},K1:SortInstrs{}))) [overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(), Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}())] // overloaded production - axiom{R} \equals{SortStmts{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), inj{SortDefns{}, SortStmts{}} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}())] // overloaded production - axiom{R} \equals{SortDefns{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}(), inj{SortEmptyStmts{}, SortDefns{}} (Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}(), Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())] // overloaded production - axiom{R} \equals{SortInstrs{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}(), inj{SortEmptyStmts{}, SortInstrs{}} (Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}(), Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())] // overloaded production - axiom{R} \equals{SortStmts{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), inj{SortEmptyStmts{}, SortStmts{}} (Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())] // overloaded production - axiom{R} \equals{SortVal{}, R} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(inj{SortFValType{}, SortValType{}} (K0:SortFValType{}),inj{SortFloat{}, SortNumber{}} (K1:SortFloat{})), inj{SortFVal{}, SortVal{}} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'FVal'Unds'FValType'Unds'Float{}(K0:SortFValType{},K1:SortFloat{}))) [overload{}(Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(), Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'FVal'Unds'FValType'Unds'Float{}())] // overloaded production - axiom{R} \equals{SortStmts{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), inj{SortInstrs{}, SortStmts{}} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}())] // overloaded production - axiom{R} \equals{SortInstrs{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}(inj{SortEmptyStmt{}, SortInstr{}} (K0:SortEmptyStmt{}),inj{SortEmptyStmts{}, SortInstrs{}} (K1:SortEmptyStmts{})), inj{SortEmptyStmts{}, SortInstrs{}} (LbllistStmt{}(K0:SortEmptyStmt{},K1:SortEmptyStmts{}))) [overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}(), LbllistStmt{}())] // overloaded production - axiom{R} \equals{SortDefns{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}(inj{SortEmptyStmt{}, SortDefn{}} (K0:SortEmptyStmt{}),inj{SortEmptyStmts{}, SortDefns{}} (K1:SortEmptyStmts{})), inj{SortEmptyStmts{}, SortDefns{}} (LbllistStmt{}(K0:SortEmptyStmt{},K1:SortEmptyStmts{}))) [overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}(), LbllistStmt{}())] // overloaded production - axiom{R} \equals{SortStmts{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(inj{SortEmptyStmt{}, SortStmt{}} (K0:SortEmptyStmt{}),inj{SortEmptyStmts{}, SortStmts{}} (K1:SortEmptyStmts{})), inj{SortEmptyStmts{}, SortStmts{}} (LbllistStmt{}(K0:SortEmptyStmt{},K1:SortEmptyStmts{}))) [overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(), LbllistStmt{}())] // overloaded production - axiom{R} \equals{SortVal{}, R} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(inj{SortIValType{}, SortValType{}} (K0:SortIValType{}),inj{SortInt{}, SortNumber{}} (K1:SortInt{})), inj{SortIVal{}, SortVal{}} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'IVal'Unds'IValType'Unds'Int{}(K0:SortIValType{},K1:SortInt{}))) [overload{}(Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(), Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'IVal'Unds'IValType'Unds'Int{}())] // overloaded production - axiom{R} \equals{SortStmts{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(inj{SortDefn{}, SortStmt{}} (K0:SortDefn{}),inj{SortDefns{}, SortStmts{}} (K1:SortDefns{})), inj{SortDefns{}, SortStmts{}} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}(K0:SortDefn{},K1:SortDefns{}))) [overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(), Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}())] // overloaded production + axiom{R} \equals{SortStmts{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(inj{SortInstr{}, SortStmt{}} (K0:SortInstr{}),inj{SortInstrs{}, SortStmts{}} (K1:SortInstrs{})), inj{SortInstrs{}, SortStmts{}} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}(K0:SortInstr{},K1:SortInstrs{}))) [symbol-overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(), Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}())] // overloaded production + axiom{R} \equals{SortStmts{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), inj{SortDefns{}, SortStmts{}} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}())] // overloaded production + axiom{R} \equals{SortDefns{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}(), inj{SortEmptyStmts{}, SortDefns{}} (Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}(), Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())] // overloaded production + axiom{R} \equals{SortInstrs{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}(), inj{SortEmptyStmts{}, SortInstrs{}} (Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}(), Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())] // overloaded production + axiom{R} \equals{SortStmts{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), inj{SortEmptyStmts{}, SortStmts{}} (Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())] // overloaded production + axiom{R} \equals{SortVal{}, R} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(inj{SortFValType{}, SortValType{}} (K0:SortFValType{}),inj{SortFloat{}, SortNumber{}} (K1:SortFloat{})), inj{SortFVal{}, SortVal{}} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'FVal'Unds'FValType'Unds'Float{}(K0:SortFValType{},K1:SortFloat{}))) [symbol-overload{}(Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(), Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'FVal'Unds'FValType'Unds'Float{}())] // overloaded production + axiom{R} \equals{SortStmts{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), inj{SortInstrs{}, SortStmts{}} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}())] // overloaded production + axiom{R} \equals{SortInstrs{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}(inj{SortEmptyStmt{}, SortInstr{}} (K0:SortEmptyStmt{}),inj{SortEmptyStmts{}, SortInstrs{}} (K1:SortEmptyStmts{})), inj{SortEmptyStmts{}, SortInstrs{}} (LbllistStmt{}(K0:SortEmptyStmt{},K1:SortEmptyStmts{}))) [symbol-overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}(), LbllistStmt{}())] // overloaded production + axiom{R} \equals{SortDefns{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}(inj{SortEmptyStmt{}, SortDefn{}} (K0:SortEmptyStmt{}),inj{SortEmptyStmts{}, SortDefns{}} (K1:SortEmptyStmts{})), inj{SortEmptyStmts{}, SortDefns{}} (LbllistStmt{}(K0:SortEmptyStmt{},K1:SortEmptyStmts{}))) [symbol-overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}(), LbllistStmt{}())] // overloaded production + axiom{R} \equals{SortStmts{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(inj{SortEmptyStmt{}, SortStmt{}} (K0:SortEmptyStmt{}),inj{SortEmptyStmts{}, SortStmts{}} (K1:SortEmptyStmts{})), inj{SortEmptyStmts{}, SortStmts{}} (LbllistStmt{}(K0:SortEmptyStmt{},K1:SortEmptyStmts{}))) [symbol-overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(), LbllistStmt{}())] // overloaded production + axiom{R} \equals{SortVal{}, R} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(inj{SortIValType{}, SortValType{}} (K0:SortIValType{}),inj{SortInt{}, SortNumber{}} (K1:SortInt{})), inj{SortIVal{}, SortVal{}} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'IVal'Unds'IValType'Unds'Int{}(K0:SortIValType{},K1:SortInt{}))) [symbol-overload{}(Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(), Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'IVal'Unds'IValType'Unds'Int{}())] // overloaded production + axiom{R} \equals{SortStmts{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(inj{SortDefn{}, SortStmt{}} (K0:SortDefn{}),inj{SortDefns{}, SortStmts{}} (K1:SortDefns{})), inj{SortDefns{}, SortStmts{}} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}(K0:SortDefn{},K1:SortDefns{}))) [symbol-overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(), Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}())] // overloaded production // rules // rule `#ContextLookup(_,_)_WASM-DATA_Int_Map_Index`(IDS,inj{Identifier,Index}(ID))=>`project:Int`(`Map:lookup`(IDS,inj{Identifier,KItem}(ID))) requires `_in_keys(_)_MAP_Bool_KItem_Map`(inj{Identifier,KItem}(ID),IDS) ensures #token("true","Bool") [UNIQUE_ID(fe974a5febf8c8a9cbe3fda608f423fbb6279d1ec26d7059387d402414901ea7), org.kframework.attributes.Location(Location(1601,8,1602,31)), org.kframework.attributes.Source(Source(/home/dwightguth/llvm-backend/test/defn/k-files/wasm.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [klabel(#ruleRequires), symbol])] diff --git a/test/unparse/sort/syntaxDefinition.kore b/test/unparse/sort/syntaxDefinition.kore index 22de46d79..dc5203389 100644 --- a/test/unparse/sort/syntaxDefinition.kore +++ b/test/unparse/sort/syntaxDefinition.kore @@ -592,6 +592,6 @@ module IMP axiom{R} \exists{R} (Val:SortPrintable{}, \equals{SortPrintable{}, R} (Val:SortPrintable{}, inj{SortString{}, SortPrintable{}} (From:SortString{}))) [subsort{SortString{}, SortPrintable{}}()] // subsort axiom{R} \exists{R} (Val:SortThreadCellMap{}, \equals{SortThreadCellMap{}, R} (Val:SortThreadCellMap{}, inj{SortThreadCell{}, SortThreadCellMap{}} (From:SortThreadCell{}))) [subsort{SortThreadCell{}, SortThreadCellMap{}}()] // subsort axiom{R} \exists{R} (Val:SortInputCellOpt{}, \equals{SortInputCellOpt{}, R} (Val:SortInputCellOpt{}, inj{SortInputCell{}, SortInputCellOpt{}} (From:SortInputCell{}))) [subsort{SortInputCell{}, SortInputCellOpt{}}()] // subsort - axiom{R} \equals{SortAExps{}, R} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'AExps'Unds'AExp'Unds'AExps'QuotRBraUnds'AExps{}(), inj{SortIds{}, SortAExps{}} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'Ids'Unds'Id'Unds'Ids'QuotRBraUnds'Ids{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'AExps'Unds'AExp'Unds'AExps'QuotRBraUnds'AExps{}(), Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'Ids'Unds'Id'Unds'Ids'QuotRBraUnds'Ids{}())] // overloaded production - axiom{R} \equals{SortAExps{}, R} (Lbl'UndsCommUndsUnds'IMP-SYNTAX'Unds'AExps'Unds'AExp'Unds'AExps{}(inj{SortId{}, SortAExp{}} (K0:SortId{}),inj{SortIds{}, SortAExps{}} (K1:SortIds{})), inj{SortIds{}, SortAExps{}} (Lbl'UndsCommUndsUnds'IMP-SYNTAX'Unds'Ids'Unds'Id'Unds'Ids{}(K0:SortId{},K1:SortIds{}))) [overload{}(Lbl'UndsCommUndsUnds'IMP-SYNTAX'Unds'AExps'Unds'AExp'Unds'AExps{}(), Lbl'UndsCommUndsUnds'IMP-SYNTAX'Unds'Ids'Unds'Id'Unds'Ids{}())] // overloaded production + axiom{R} \equals{SortAExps{}, R} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'AExps'Unds'AExp'Unds'AExps'QuotRBraUnds'AExps{}(), inj{SortIds{}, SortAExps{}} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'Ids'Unds'Id'Unds'Ids'QuotRBraUnds'Ids{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'AExps'Unds'AExp'Unds'AExps'QuotRBraUnds'AExps{}(), Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'Ids'Unds'Id'Unds'Ids'QuotRBraUnds'Ids{}())] // overloaded production + axiom{R} \equals{SortAExps{}, R} (Lbl'UndsCommUndsUnds'IMP-SYNTAX'Unds'AExps'Unds'AExp'Unds'AExps{}(inj{SortId{}, SortAExp{}} (K0:SortId{}),inj{SortIds{}, SortAExps{}} (K1:SortIds{})), inj{SortIds{}, SortAExps{}} (Lbl'UndsCommUndsUnds'IMP-SYNTAX'Unds'Ids'Unds'Id'Unds'Ids{}(K0:SortId{},K1:SortIds{}))) [symbol-overload{}(Lbl'UndsCommUndsUnds'IMP-SYNTAX'Unds'AExps'Unds'AExp'Unds'AExps{}(), Lbl'UndsCommUndsUnds'IMP-SYNTAX'Unds'Ids'Unds'Id'Unds'Ids{}())] // overloaded production endmodule []