Add module pyk.kllvm (#52)

~Blocked on:
runtimeverification/llvm-backend#600

Based on:
*
https://github.com/runtimeverification/llvm-backend/blob/2ec0f1988efda8d53152dec25dca0c11909ba5bf/bindings/python/package/kllvm/__init__.py
*
https://github.com/runtimeverification/llvm-backend/blob/4e51aea6e7813f206cf8fceb1ed471339eb1b684/bin/k-repl

Co-authored-by: Bruce Collie <[email protected]>
Co-authored-by: devops <[email protected]>

Author: 3 people

deps/K_VERSION

@@ -1 +1 @@
-5.5.4
+5.5.32

k-files/ctor.k

@@ -0,0 +1,3 @@
+module CTOR
+    syntax Foo ::= one() | two() | three()
+endmodule

k-files/steps.k

@@ -0,0 +1,9 @@
+module STEPS-SYNTAX
+endmodule
+
+module STEPS
+  imports INT
+  syntax Foo ::= foo(Int) | bar()
+  rule foo(I) => foo(I -Int 1) requires I >Int 0
+  rule foo(_) => bar() [owise]
+endmodule

package/version

@@ -1 +1 @@
-0.1.66
+0.1.67

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.66"
+version = "0.1.67"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

src/integration_tests/kllvm/__init__.py

@@ -0,0 +1,42 @@
+from pathlib import Path
+
+from pyk.kllvm.parser import Parser, read_pattern
+
+
+def test_read_pattern(tmp_path: Path) -> None:
+    # Given
+    kore_text = 'A{}(B{}(),C{}())'
+    kore_file = tmp_path / 'test.kore'
+    kore_file.write_text(kore_text)
+
+    # When
+    actual = read_pattern(kore_file)
+
+    # Then
+    assert str(actual) == kore_text
+
+
+def test_parser_from_file(tmp_path: Path) -> None:
+    # Given
+    kore_text = 'A{}(B{}(),C{}())'
+    kore_file = tmp_path / 'test.kore'
+    kore_file.write_text(kore_text)
+    parser = Parser(str(kore_file))
+
+    # When
+    actual = parser.pattern()
+
+    # Then
+    assert str(actual) == kore_text
+
+
+def test_parser_from_string() -> None:
+    # Given
+    kore_text = 'A{}(X : S,Y : Z,Int{}())'
+    parser = Parser.from_string(kore_text)
+
+    # When
+    actual = parser.pattern()
+
+    # Then
+    assert str(actual) == kore_text

src/integration_tests/kllvm/test_parser.py

@@ -0,0 +1,56 @@
+from tempfile import NamedTemporaryFile
+from unittest import TestCase
+
+from pyk.kllvm.ast import CompositePattern, CompositeSort, Pattern, StringPattern, VariablePattern
+
+
+class PatternTest(TestCase):
+    def test_file_load(self) -> None:
+        # Given
+        test_data = (
+            'A{}(B{}(),C{}())',
+            '"string pattern"',
+            'XYZ : ABC',
+        )
+
+        for text in test_data:
+            with self.subTest(text):
+                with NamedTemporaryFile(mode='w') as f:
+                    f.write(text)
+                    f.flush()
+
+                    # When
+                    actual = Pattern(f.name)
+
+                # Then
+                self.assertEqual(str(actual), text)
+
+    def test_composite(self) -> None:
+        # Given
+        pattern = CompositePattern('F')
+        pattern.add_argument(CompositePattern('A'))
+        pattern.add_argument(VariablePattern('X', CompositeSort('S')))
+
+        # When
+        actual = pattern.substitute({'X': CompositePattern('B')})
+
+        # Then
+        self.assertEqual(str(actual), 'F{}(A{}(),B{}())')
+
+    def test_string(self) -> None:
+        # Given
+        pattern = StringPattern('abc')
+
+        # Then
+        self.assertEqual(str(pattern), '"abc"')
+        self.assertEqual(pattern.contents, 'abc')
+
+    def test_variable(self) -> None:
+        # Given
+        pattern = VariablePattern('X', CompositeSort('S'))
+
+        # When
+        actual = pattern.substitute({'X': CompositePattern('A')})
+
+        # Then
+        self.assertEqual(str(actual), 'A{}()')

src/integration_tests/kllvm/test_patterns.py

@@ -0,0 +1,122 @@
+from unittest import TestCase
+
+from pyk.kllvm.ast import CompositeSort, SortVariable
+
+
+class SortTest(TestCase):
+    def test_is_concrete(self) -> None:
+        # Given
+        test_data = (
+            (CompositeSort('A'), True),
+            (SortVariable('B'), False),
+        )
+
+        for i, (sort, expected) in enumerate(test_data):
+            with self.subTest(i=i):
+                # When
+                actual = sort.is_concrete
+
+                # Then
+                self.assertEqual(actual, expected)
+
+    def test_name(self) -> None:
+        # Given
+        names = ('A', 'SortInt', '')
+
+        for name in names:
+            with self.subTest(name):
+                # When
+                sort = CompositeSort(name)
+
+                # Then
+                self.assertEqual(sort.name, name)
+
+    def test_str(self) -> None:
+        # Given
+        test_data = (
+            (CompositeSort('A'), 'A{}'),
+            (SortVariable('B'), 'B'),
+        )
+
+        for i, (sort, expected) in enumerate(test_data):
+            with self.subTest(i=i):
+                # When
+                actual = str(sort)
+
+                # Then
+                self.assertEqual(actual, expected)
+
+    def test_add_argument(self) -> None:
+        # Given
+        f = CompositeSort('F')
+        a = CompositeSort('A')
+        b = SortVariable('B')
+
+        # When
+        f.add_argument(a)
+        f.add_argument(b)
+
+        # Then
+        self.assertEqual(str(f), 'F{A{},B}')
+
+    def test_substitution_1(self) -> None:
+        # Given
+        x = SortVariable('X')
+        a = CompositeSort('A')
+        expected = a
+
+        # When
+        actual = a.substitute({x: a})
+
+        # Then
+        self.assertEqual(actual, expected)
+
+    def test_substitution_2(self) -> None:
+        x = SortVariable('X')
+        y = SortVariable('Y')
+        a = CompositeSort('A')
+        b = CompositeSort('B')
+        c = CompositeSort('C')
+
+        original = CompositeSort('F')
+        g1 = CompositeSort('G')
+        g1.add_argument(x)
+        g1.add_argument(x)
+        g1.add_argument(b)
+        g1.add_argument(y)
+        original.add_argument(g1)
+
+        self.assertEqual(str(original), 'F{G{X,X,B{},Y}}')
+        self.assertFalse(original.is_concrete)
+
+        expected = CompositeSort('F')
+        g2 = CompositeSort('G')
+        g2.add_argument(a)
+        g2.add_argument(a)
+        g2.add_argument(b)
+        g2.add_argument(c)
+        expected.add_argument(g2)
+
+        self.assertEqual(str(expected), 'F{G{A{},A{},B{},C{}}}')
+        self.assertTrue(expected.is_concrete)
+
+        # When
+        actual = original.substitute({x: a, y: c})
+
+        # Then
+        self.assertEqual(actual, expected)
+
+    def test_equality(self) -> None:
+        # Given
+        a1 = CompositeSort('A')
+        a2 = CompositeSort('A')
+        b1 = SortVariable('B')
+        b2 = SortVariable('B')
+
+        # Then
+        self.assertIsNot(a1, a2)
+        self.assertEqual(a1, a2)
+        self.assertIsNot(b1, b2)
+        self.assertEqual(b1, b2)
+        self.assertNotEqual(a1, b1)
+        self.assertNotEqual(a2, b2)

src/integration_tests/kllvm/test_sorts.py

@@ -0,0 +1,67 @@
+from pyk.kllvm.ast import Pattern
+from pyk.kllvm.parser import Parser
+
+from .utils import RuntimeTest
+
+
+class StepTest(RuntimeTest):
+    KOMPILE_MAIN_FILE = 'k-files/steps.k'
+
+    def test_steps_1(self) -> None:
+        term = self.runtime.Term(start_pattern())
+        term.step(0)
+        self.assertEqual(str(term), foo_output(0))
+        term.step()
+        term.step()
+        self.assertEqual(str(term), foo_output(2))
+        term.step(200)
+        self.assertEqual(str(term), bar_output())
+
+    def test_steps_2(self) -> None:
+        term = self.runtime.Term(start_pattern())
+        self.assertEqual(str(term), foo_output(0))
+        term.step(50)
+        self.assertEqual(str(term), foo_output(50))
+        term.step(-1)
+        self.assertEqual(str(term), bar_output())
+
+    def test_steps_3(self) -> None:
+        term = self.runtime.Term(start_pattern())
+        term.run()
+        self.assertEqual(str(term), bar_output())
+
+
+def start_pattern() -> Pattern:
+    """
+    <k> foo(100) </k>
+    """
+    text = r"""
+        LblinitGeneratedTopCell{}(
+            Lbl'Unds'Map'Unds'{}(
+                Lbl'Stop'Map{}(),
+                Lbl'UndsPipe'-'-GT-Unds'{}(
+                    inj{SortKConfigVar{}, SortKItem{}}(\dv{SortKConfigVar{}}("$PGM")),
+                    inj{SortFoo{}, SortKItem{}}(
+                        inj{SortFoo{}, SortKItem{}}(
+                            Lblfoo'LParUndsRParUnds'STEPS'Unds'Foo'Unds'Int{}(\dv{SortInt{}}("100"))
+                        )
+                    )
+                )
+            )
+        )
+    """
+    return Parser.from_string(text).pattern()
+
+
+def foo_output(n: int) -> str:
+    """
+    <k> foo(100 - n) </k>
+    """
+    return fr"""Lbl'-LT-'generatedTop'-GT-'{{}}(Lbl'-LT-'k'-GT-'{{}}(kseq{{}}(inj{{SortFoo{{}}, SortKItem{{}}}}(Lblfoo'LParUndsRParUnds'STEPS'Unds'Foo'Unds'Int{{}}(\dv{{SortInt{{}}}}("{100-n}"))),dotk{{}}())),Lbl'-LT-'generatedCounter'-GT-'{{}}(\dv{{SortInt{{}}}}("0")))"""
+
+
+def bar_output() -> str:
+    """
+    <k> bar() </k>
+    """
+    return r"""Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortFoo{}, SortKItem{}}(Lblbar'LParRParUnds'STEPS'Unds'Foo{}()),dotk{}())),Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0")))"""

src/integration_tests/kllvm/test_step.py

@@ -0,0 +1,42 @@
+from unittest import TestCase
+
+from pyk.kllvm.ast import CompositeSort, Symbol, Variable
+
+
+class SymbolTest(TestCase):
+    def test_str(self) -> None:
+        # Given
+        s1 = Symbol("Lbl'Plus")
+        s2 = Symbol("Lbl'Plus")
+        s2.add_formal_argument(CompositeSort('A'))
+
+        test_data = (
+            (s1, "Lbl'Plus{}"),
+            (s2, "Lbl'Plus{A{}}"),
+        )
+
+        for i, (symbol, expected) in enumerate(test_data):
+            with self.subTest(i=i):
+                # When
+                actual = str(symbol)
+
+                # Then
+                self.assertEqual(actual, expected)
+
+    def test_equal(self) -> None:
+        a1 = Symbol('A')
+        a2 = Symbol('A')
+        b1 = Symbol('B')
+        self.assertIsNot(a1, a2)
+        self.assertEqual(a1, a2)
+        self.assertNotEqual(a1, b1)
+
+
+class VariableTest(TestCase):
+    def test_variable(self) -> None:
+        # When
+        a = Variable('A')
+
+        # Then
+        self.assertEqual(a.name, 'A')
+        self.assertEqual(str(a), 'A')

src/integration_tests/kllvm/test_symbols.py

@@ -0,0 +1,26 @@
+from pyk.kllvm.ast import CompositePattern
+from pyk.kllvm.runtime import compile_runtime, import_runtime
+
+from .utils import RuntimeTest
+
+
+class TermTest(RuntimeTest):
+    KOMPILE_MAIN_FILE = 'k-files/ctor.k'
+    KOMPILE_SYNTAX_MODULE = 'CTOR'
+
+    def setUp(self) -> None:
+        super().setUp()
+        compile_runtime(self.kompiled_dir)
+        self.runtime = import_runtime(self.kompiled_dir)
+
+    def test_construct(self) -> None:
+        test_data = ('one', 'two', 'three')
+        for ctor in test_data:
+            with self.subTest(ctor):
+                # Given
+                label = f"Lbl{ctor}'LParRParUnds'CTOR'Unds'Foo"
+                pattern = CompositePattern(label)
+                term = self.runtime.Term(pattern)
+
+                # Then
+                self.assertEqual(str(pattern), str(term))