From bf99da6ed483849285b52fb3470607f7d2c1611a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?=
 <tothtamas28@users.noreply.github.com>
Date: Fri, 15 Dec 2023 10:27:57 +0000
Subject: [PATCH] Expose function evaluation from KLLVM bindings

---
 src/pyk/kllvm/runtime.py                     |  5 +-
 src/tests/integration/kllvm/test_evaluate.py | 49 ++++++++++++++++++++
 2 files changed, 53 insertions(+), 1 deletion(-)
 create mode 100644 src/tests/integration/kllvm/test_evaluate.py

diff --git a/src/pyk/kllvm/runtime.py b/src/pyk/kllvm/runtime.py
index e22a24750c..e6b3acbe72 100644
--- a/src/pyk/kllvm/runtime.py
+++ b/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:
@@ -38,6 +38,9 @@ def simplify(self, pattern: Pattern, sort: Sort) -> Pattern:
     def simplify_bool(self, pattern: Pattern) -> bool:
         return self._module.simplify_bool_pattern(pattern)
 
+    def evaluate(self, pattern: CompositePattern) -> Pattern:
+        return self._module.evaluate_function(pattern)
+
 
 class Term:
     _block: Any  # module.InternalTerm
diff --git a/src/tests/integration/kllvm/test_evaluate.py b/src/tests/integration/kllvm/test_evaluate.py
new file mode 100644
index 0000000000..caa059d3d1
--- /dev/null
+++ b/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