diff --git a/pyk/src/pyk/kllvm/runtime.py b/pyk/src/pyk/kllvm/runtime.py index 3f73aa02aca..d041f0bd73e 100644 --- a/pyk/src/pyk/kllvm/runtime.py +++ b/pyk/src/pyk/kllvm/runtime.py @@ -6,7 +6,7 @@ from types import ModuleType from typing import Any - from .ast import Pattern, Sort + from .ast import CompositePattern, Pattern, Sort class Runtime: @@ -43,6 +43,11 @@ def simplify_bool(self, pattern: Pattern) -> bool: self._module.free_all_gc_memory() return res + def evaluate(self, pattern: CompositePattern) -> Pattern: + res = self._module.evaluate_function(pattern) + self._module.free_all_gc_memory() + return res + class Term: _block: Any # module.InternalTerm diff --git a/pyk/src/tests/integration/kllvm/test_evaluate.py b/pyk/src/tests/integration/kllvm/test_evaluate.py new file mode 100644 index 00000000000..caa059d3d10 --- /dev/null +++ b/pyk/src/tests/integration/kllvm/test_evaluate.py @@ -0,0 +1,49 @@ +from __future__ import annotations + +from typing import TYPE_CHECKING + +import pytest + +import pyk.kllvm.load # noqa: F401 +from pyk.kllvm import parser +from pyk.testing import RuntimeTest + +from ..utils import K_FILES + +if TYPE_CHECKING: + from pyk.kllvm.runtime import Runtime + + +EVALUATE_TEST_DATA = ( + ('1 + 2', r"""Lbl'UndsPlus'Int'Unds'{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("2"))""", r'\dv{SortInt{}}("3")'), + ('1 * 2', r"""Lbl'UndsStar'Int'Unds'{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("2"))""", r'\dv{SortInt{}}("2")'), + ( + '1 + (2 * 3)', + r""" + Lbl'UndsPlus'Int'Unds'{}( + \dv{SortInt{}}("1"), + Lbl'UndsStar'Int'Unds'{}(\dv{SortInt{}}("2"), \dv{SortInt{}}("3")) + ) + """, + r'\dv{SortInt{}}("7")', + ), +) + + +class TestEvaluate(RuntimeTest): + KOMPILE_MAIN_FILE = K_FILES / 'imp.k' + + @pytest.mark.parametrize( + 'test_id,pattern_text,expected', + EVALUATE_TEST_DATA, + ids=[test_id for test_id, *_ in EVALUATE_TEST_DATA], + ) + def test_simplify(self, runtime: Runtime, test_id: str, pattern_text: str, expected: str) -> None: + # Given + pattern = parser.parse_pattern(pattern_text) + + # When + actual = runtime.evaluate(pattern) + + # Then + assert str(actual) == expected