Source code for pyk.kllvm.runtime

 1from __future__ import annotations
 2
 3from typing import TYPE_CHECKING
 4
 5if TYPE_CHECKING:
 6    from types import ModuleType
 7    from typing import Any
 8
 9    from .ast import Pattern, Sort
10
11


[docs]
12class Runtime:
13    _module: ModuleType
14
15    def __init__(self, module: ModuleType):
16        module.init_static_objects()
17        self._module = module
18


[docs]
19    def term(self, pattern: Pattern) -> Term:
20        return Term(self._module.InternalTerm(pattern))


21


[docs]
22    def deserialize(self, bs: bytes) -> Term | None:
23        block = self._module.InternalTerm.deserialize(bs)
24        if block is None:
25            return None
26        return Term(block)


27


[docs]
28    def step(self, pattern: Pattern, depth: int | None = 1) -> Pattern:
29        term = self.term(pattern)
30        term.step(depth=depth)
31        return term.pattern


32


[docs]
33    def run(self, pattern: Pattern) -> Pattern:
34        return self.step(pattern, depth=None)


35


[docs]
36    def simplify(self, pattern: Pattern, sort: Sort) -> Pattern:
37        res = self._module.simplify_pattern(pattern, sort)
38        self._module.free_all_gc_memory()
39        return res


40


[docs]
41    def simplify_bool(self, pattern: Pattern) -> bool:
42        res = self._module.simplify_bool_pattern(pattern)
43        self._module.free_all_gc_memory()
44        return res




45
46


[docs]
47class Term:
48    _block: Any  # module.InternalTerm
49
50    def __init__(self, block: Any):
51        self._block = block
52
53    @property
54    def pattern(self) -> Pattern:
55        return self._block.to_pattern()
56


[docs]
57    def serialize(self) -> bytes:
58        return self._block.serialize()


59


[docs]
60    def step(self, depth: int | None = 1) -> None:
61        self._block = self._block.step(depth if depth is not None else -1)


62


[docs]
63    def run(self) -> None:
64        self.step(depth=None)


65
66    def __str__(self) -> str:
67        return str(self._block)