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 CompositePattern, 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
[docs]
46 def evaluate(self, pattern: CompositePattern) -> Pattern:
47 res = self._module.evaluate_function(pattern)
48 self._module.free_all_gc_memory()
49 return res
50
51
[docs]
52class Term:
53 _block: Any # module.InternalTerm
54
55 def __init__(self, block: Any):
56 self._block = block
57
58 @property
59 def pattern(self) -> Pattern:
60 return self._block.to_pattern()
61
[docs]
62 def serialize(self) -> bytes:
63 return self._block.serialize()
64
[docs]
65 def step(self, depth: int | None = 1) -> None:
66 self._block = self._block.step(depth if depth is not None else -1)
67
[docs]
68 def run(self) -> None:
69 self.step(depth=None)
70
71 def __str__(self) -> str:
72 return str(self._block)