diff --git a/pyk/deps/k_release b/pyk/deps/k_release index 4b7d460fe81..4ae4ba479bd 100644 --- 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 index c3ea77661e6..5950bc01383 100644 --- 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 index 5941951189a..c7b4503cd44 100644 --- 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 index 6555210cffe..e0923fee8d6 100644 --- 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. ", diff --git a/pyk/src/pyk/__init__.py b/pyk/src/pyk/__init__.py index 069f701c6cb..13370a50bd9 100644 --- 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 index 05f7c318330..7ab5b769f3c 100644 --- 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 index 7bdd018673f..558996ba6fd 100644 --- 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 index 47ad96e287b..97992a3971d 100644 --- 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 index 7417fc7fe6f..0205a5d16d6 100644 --- 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,9 +448,7 @@ 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( @@ -466,7 +456,7 @@ [ 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,7 +626,7 @@ ( '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'), @@ -644,7 +634,7 @@ ( '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'),