Skip to content

Commit bba8f4a

Browse files
tothtamas28rv-auditor
authored andcommitted
Add test case for strip_raw_term in Pattern.deserialize (runtimeverification/pyk#748)
~Blocked on runtimeverification/llvm-backend#908 --------- Co-authored-by: devops <[email protected]>
1 parent 2e16212 commit bba8f4a

File tree

3 files changed

+35
-2
lines changed

3 files changed

+35
-2
lines changed

pyk/package/version

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
0.1.531
1+
0.1.532

pyk/pyproject.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
44

55
[tool.poetry]
66
name = "pyk"
7-
version = "0.1.531"
7+
version = "0.1.532"
88
description = ""
99
authors = [
1010
"Runtime Verification, Inc. <[email protected]>",

pyk/src/tests/integration/kllvm/test_serialize.py

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,22 @@
1+
from __future__ import annotations
2+
3+
from typing import TYPE_CHECKING
4+
15
import pytest
26

37
import pyk.kllvm.load # noqa: F401
8+
from pyk.kllvm import parser
49
from pyk.kllvm.ast import Pattern
510
from pyk.kllvm.convert import pattern_to_llvm
611
from pyk.kore.parser import KoreParser
12+
from pyk.testing import RuntimeTest
13+
14+
from ..utils import K_FILES
15+
16+
if TYPE_CHECKING:
17+
from pathlib import Path
18+
19+
from pyk.kllvm.runtime import Runtime
720

821
TEST_DATA = (
922
'"foo"',
@@ -30,3 +43,23 @@ def test_serialize(kore_text: str) -> None:
3043
# Then
3144
assert actual is not None
3245
assert str(actual) == str(pattern)
46+
47+
48+
class TestSerializeRaw(RuntimeTest):
49+
KOMPILE_MAIN_FILE = K_FILES / 'imp.k'
50+
51+
def test_serialize_raw(self, runtime: Runtime, tmp_path: Path) -> None:
52+
# Given
53+
kore_text = r"""Lbl'UndsPlus'Int'Unds'{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("2"))"""
54+
pattern = parser.parse_pattern(kore_text)
55+
term = runtime.term(pattern)
56+
kore_file = tmp_path / 'kore'
57+
58+
# When
59+
term._block._serialize_raw(str(kore_file), 'SortInt{}')
60+
pattern = Pattern.deserialize(kore_file.read_bytes())
61+
pattern_with_raw = Pattern.deserialize(kore_file.read_bytes(), strip_raw_term=False)
62+
63+
# Then
64+
assert str(pattern) == r'\dv{SortInt{}}("3")'
65+
assert str(pattern_with_raw) == r'rawTerm{}(inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("3")))'

0 commit comments

Comments
 (0)