Update dependency: deps/k_release (runtimeverification/pyk#979)

Related: * runtimeverification/llvm-backend#1000 * #4064 --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Tamás Tóth <tothtamas28@users.noreply.github.com>
runtimeverification · Apr 9, 2024 · 6f620be · 6f620be
1 parent cb742a5
commit 6f620be
Show file tree

Hide file tree

Showing 9 changed files with 21 additions and 33 deletions.
diff --git a/pyk/deps/k_release b/pyk/deps/k_release
@@ -1 +1 @@
-6.3.32
+6.3.37
diff --git a/pyk/docs/conf.py b/pyk/docs/conf.py
@@ -9,8 +9,8 @@
 project = 'pyk'
 author = 'Runtime Verification, Inc'
 copyright = '2024, Runtime Verification, Inc'
-version = '0.1.706'
-release = '0.1.706'
+version = '0.1.707'
+release = '0.1.707'
 
 # -- General configuration ---------------------------------------------------
 # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration

diff --git a/pyk/package/version b/pyk/package/version
@@ -1 +1 @@
-0.1.706
+0.1.707
diff --git a/pyk/pyproject.toml b/pyk/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.706"
+version = "0.1.707"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

diff --git a/pyk/src/pyk/__init__.py b/pyk/src/pyk/__init__.py
@@ -6,4 +6,4 @@
     from typing import Final
 
 
-K_VERSION: Final = '6.3.32'
+K_VERSION: Final = '6.3.37'
diff --git a/pyk/src/pyk/kllvm/ast.py b/pyk/src/pyk/kllvm/ast.py
@@ -16,7 +16,7 @@
     Symbol,
     SymbolAliasDeclaration,
     SymbolDeclaration,
-    ValueType,
     Variable,
     VariablePattern,
+    value_type,
 )
diff --git a/pyk/src/pyk/kllvm/convert.py b/pyk/src/pyk/kllvm/convert.py
@@ -121,7 +121,7 @@ def sort_to_llvm(sort: Sort) -> kllvm.Sort:
         case SortVar(name):
             return kllvm.SortVariable(name)
         case SortApp(name, sorts):
-            res = kllvm.CompositeSort(sort.name, kllvm.ValueType(kllvm.SortCategory(0)))
+            res = kllvm.CompositeSort(sort.name, kllvm.value_type(kllvm.SortCategory(0)))
             for subsort in sorts:
                 res.add_argument(sort_to_llvm(subsort))
             return res

diff --git a/pyk/src/pyk/kore/prelude.py b/pyk/src/pyk/kore/prelude.py
@@ -148,9 +148,7 @@ def le_int(left: Pattern, right: Pattern) -> Pattern:
 LBL_GENERATED_TOP: Final = SymbolId("Lbl'-LT-'generatedTop'-GT-'")
 LBL_GENERATED_COUNTER: Final = SymbolId("Lbl'-LT-'generatedCounter'-GT-'")
 LBL_K: Final = SymbolId("Lbl'-LT-'k'-GT-'")
-LBL_ITE: Final = SymbolId(
-    "Lbl'Hash'if'UndsHash'then'UndsHash'else'UndsHash'fi'Unds'K-EQUAL-SYNTAX'Unds'Sort'Unds'Bool'Unds'Sort'Unds'Sort"
-)
+LBL_ITE: Final = SymbolId('Lblite')
 INJ: Final = SymbolId('inj')
 KSEQ: Final = SymbolId('kseq')
 

diff --git a/pyk/src/tests/integration/konvert/test_simple_proofs.py b/pyk/src/tests/integration/konvert/test_simple_proofs.py
@@ -216,13 +216,9 @@
     (
         'if-then-else',
         KSort('K'),
-        r"""
-        Lbl'Hash'if'UndsHash'then'UndsHash'else'UndsHash'fi'Unds'K-EQUAL-SYNTAX'Unds'Sort'Unds'Bool'Unds'Sort'Unds'Sort{SortK{}}(
-            VarC : SortBool{}, VarB1 : SortK{}, VarB2 : SortK {}
-        )
-        """,
+        r'Lblite{SortK{}}(VarC : SortBool{}, VarB1 : SortK{}, VarB2 : SortK {})',
         KApply(
-            KLabel('#if_#then_#else_#fi_K-EQUAL-SYNTAX_Sort_Bool_Sort_Sort', [KSort('K')]),
+            KLabel('ite', [KSort('K')]),
             [
                 KVariable('C', sort=KSort('Bool')),
                 KVariable('B1', sort=KSort('K')),
@@ -436,13 +432,9 @@
     (
         'if-then-else-no-sort-param-k',
         KSort('K'),
-        r"""
-        Lbl'Hash'if'UndsHash'then'UndsHash'else'UndsHash'fi'Unds'K-EQUAL-SYNTAX'Unds'Sort'Unds'Bool'Unds'Sort'Unds'Sort{SortK{}}(
-            VarC : SortBool{}, VarB1 : SortK{}, VarB2 : SortK {}
-        )
-        """,
+        r'Lblite{SortK{}}(VarC : SortBool{}, VarB1 : SortK{}, VarB2 : SortK {})',
         KApply(
-            KLabel('#if_#then_#else_#fi_K-EQUAL-SYNTAX_Sort_Bool_Sort_Sort', []),
+            KLabel('ite', []),
             [
                 KVariable('C', sort=KSort('Bool')),
                 KVariable('B1', sort=KSort('K')),
@@ -456,17 +448,15 @@
         r"""
         Lbl'UndsPlus'Int'Unds'{}(
             VarA : SortInt{},
-            Lbl'Hash'if'UndsHash'then'UndsHash'else'UndsHash'fi'Unds'K-EQUAL-SYNTAX'Unds'Sort'Unds'Bool'Unds'Sort'Unds'Sort{SortInt{}}(
-                VarC : SortBool{}, VarI1 : SortInt{}, VarI2 : SortInt {}
-            )
+            Lblite{SortInt{}}(VarC : SortBool{}, VarI1 : SortInt{}, VarI2 : SortInt {})
         )
         """,
         KApply(
             '_+Int_',
             [
                 KVariable('A', sort=KSort('Int')),
                 KApply(
-                    KLabel('#if_#then_#else_#fi_K-EQUAL-SYNTAX_Sort_Bool_Sort_Sort', []),
+                    KLabel('ite', []),
                     [
                         KVariable('C', sort=KSort('Bool')),
                         KVariable('I1', sort=KSort('Int')),
@@ -480,20 +470,20 @@
         'if-then-else-no-sort-param-nested',
         KSort('Int'),
         r"""
-        Lbl'Hash'if'UndsHash'then'UndsHash'else'UndsHash'fi'Unds'K-EQUAL-SYNTAX'Unds'Sort'Unds'Bool'Unds'Sort'Unds'Sort{SortInt{}}(
+        Lblite{SortInt{}}(
             VarC1 : SortBool{},
-            Lbl'Hash'if'UndsHash'then'UndsHash'else'UndsHash'fi'Unds'K-EQUAL-SYNTAX'Unds'Sort'Unds'Bool'Unds'Sort'Unds'Sort{SortInt{}}(
+            Lblite{SortInt{}}(
                 VarC2 : SortBool{}, VarI1 : SortInt{} , VarI2 : SortInt{}
             ),
             VarI3 : SortInt{}
         )
         """,
         KApply(
-            KLabel('#if_#then_#else_#fi_K-EQUAL-SYNTAX_Sort_Bool_Sort_Sort', []),
+            KLabel('ite', []),
             [
                 KVariable('C1', sort=KSort('Bool')),
                 KApply(
-                    KLabel('#if_#then_#else_#fi_K-EQUAL-SYNTAX_Sort_Bool_Sort_Sort', []),
+                    KLabel('ite', []),
                     [
                         KVariable('C2', sort=KSort('Bool')),
                         KVariable('I1', sort=KSort('Int')),
@@ -636,15 +626,15 @@
     (
         'sort-parametric-int',
         KApply(
-            KLabel('#if_#then_#else_#fi_K-EQUAL-SYNTAX_Sort_Bool_Sort_Sort', [KSort('Int')]),
+            KLabel('ite', [KSort('Int')]),
             [KToken('true', 'Bool'), intToken(1), intToken(2)],
         ),
         KSort('Int'),
     ),
     (
         'sort-parametric-bool',
         KApply(
-            KLabel('#if_#then_#else_#fi_K-EQUAL-SYNTAX_Sort_Bool_Sort_Sort', [KSort('Bool')]),
+            KLabel('ite', [KSort('Bool')]),
             [KToken('true', 'Bool'), KToken('true', 'Bool'), KToken('false', 'Bool')],
         ),
         KSort('Bool'),
Original file line number	Diff line number	Diff line change
Expand Up		@@ -6,4 +6,4 @@
		from typing import Final


		K_VERSION: Final = '6.3.32'
		K_VERSION: Final = '6.3.37'