1from __future__ import annotations
2
3import json
4import logging
5from contextlib import contextmanager
6from enum import Enum
7from functools import cached_property
8from pathlib import Path
9from tempfile import NamedTemporaryFile
10from typing import TYPE_CHECKING
11
12from ..cli.utils import check_dir_path, check_file_path
13from ..kast import KAst, kast_term
14from ..kast.inner import KInner
15from ..kast.outer import read_kast_definition
16from ..kast.pretty import PrettyPrinter
17from ..konvert import kast_to_kore, kore_to_kast
18from ..kore.parser import KoreParser
19from ..kore.syntax import App, SortApp
20from ..kore.tools import PrintOutput, kore_print
21from ..utils import run_process_2
22from .kompile import DefinitionInfo
23
24if TYPE_CHECKING:
25 from collections.abc import Callable, Iterable, Iterator
26 from subprocess import CompletedProcess
27 from tempfile import _TemporaryFileWrapper
28 from typing import Final
29
30 from ..kast.inner import KSort, KToken
31 from ..kast.outer import KDefinition, KFlatModule
32 from ..kast.pretty import SymbolTable
33 from ..kore.syntax import Pattern
34 from ..utils import BugReport
35
36_LOGGER: Final = logging.getLogger(__name__)
37
38
46
47
[docs]
48class KAstOutput(Enum):
49 PRETTY = 'pretty'
50 PROGRAM = 'program'
51 KAST = 'kast'
52 BINARY = 'binary'
53 JSON = 'json'
54 LATEX = 'latex'
55 KORE = 'kore'
56 NONE = 'none'
57
58
59def _kast(
60 file: str | Path | None = None,
61 *,
62 command: str | None = None,
63 definition_dir: str | Path | None = None,
64 input: str | KAstInput | None = None,
65 output: str | KAstOutput | None = None,
66 expression: str | None = None,
67 module: str | None = None,
68 sort: str | None = None,
69 temp_dir: str | Path | None = None,
70 gen_glr_parser: bool = False,
71 # ---
72 check: bool = True,
73) -> CompletedProcess:
74 if file is not None:
75 file = Path(file)
76
77 if file and not gen_glr_parser:
78 check_file_path(file)
79
80 if not file and gen_glr_parser:
81 raise ValueError('No output file specified for --gen-glr-parser')
82
83 if definition_dir is not None:
84 definition_dir = Path(definition_dir)
85 check_dir_path(definition_dir)
86
87 if temp_dir is not None:
88 temp_dir = Path(temp_dir)
89
90 if input is not None:
91 input = KAstInput(input)
92
93 if output is not None:
94 output = KAstOutput(output)
95
96 args = _build_arg_list(
97 file=file,
98 command=command,
99 definition_dir=definition_dir,
100 input=input,
101 output=output,
102 expression=expression,
103 module=module,
104 sort=sort,
105 temp_dir=temp_dir,
106 gen_glr_parser=gen_glr_parser,
107 )
108
109 return run_process_2(args, logger=_LOGGER, check=check)
110
111
[docs]
112def gen_glr_parser(
113 parser_file: str | Path,
114 *,
115 command: str | None = None,
116 definition_dir: str | Path | None = None,
117 module: str | None = None,
118 sort: str | None = None,
119 temp_dir: str | Path | None = None,
120) -> Path:
121 parser_file = Path(parser_file)
122 _kast(
123 file=parser_file,
124 command=command,
125 definition_dir=definition_dir,
126 module=module,
127 sort=sort,
128 temp_dir=temp_dir,
129 gen_glr_parser=True,
130 check=True,
131 )
132 assert parser_file.is_file()
133 return parser_file
134
135
136def _build_arg_list(
137 *,
138 file: Path | None,
139 command: str | None,
140 definition_dir: Path | None,
141 input: KAstInput | None,
142 output: KAstOutput | None,
143 expression: str | None,
144 module: str | None,
145 sort: str | None,
146 temp_dir: Path | None,
147 gen_glr_parser: bool,
148) -> list[str]:
149 args = [command if command is not None else 'kast']
150 if file:
151 args += [str(file)]
152 if definition_dir:
153 args += ['--definition', str(definition_dir)]
154 if input:
155 args += ['--input', input.value]
156 if output:
157 args += ['--output', output.value]
158 if expression:
159 args += ['--expression', expression]
160 if module:
161 args += ['--module', module]
162 if sort:
163 args += ['--sort', sort]
164 if temp_dir:
165 args += ['--temp-dir', str(temp_dir)]
166 if gen_glr_parser:
167 args += ['--gen-glr-parser']
168 return args
169
170
[docs]
171class KPrint:
172 definition_dir: Path
173 use_directory: Path | None
174 main_module: str
175 backend: str
176 _extra_unparsing_modules: Iterable[KFlatModule]
177 _patch_symbol_table: Callable[[SymbolTable], None] | None
178
179 _bug_report: BugReport | None
180
181 def __init__(
182 self,
183 definition_dir: Path,
184 use_directory: Path | None = None,
185 bug_report: BugReport | None = None,
186 extra_unparsing_modules: Iterable[KFlatModule] = (),
187 patch_symbol_table: Callable[[SymbolTable], None] | None = None,
188 ) -> None:
189 self.definition_dir = definition_dir
190
191 if use_directory:
192 check_dir_path(use_directory)
193
194 self.use_directory = use_directory
195 self._definition = None
196 self._symbol_table = None
197
198 info = DefinitionInfo(self.definition_dir)
199 self.main_module = info.main_module_name
200 self.backend = info.backend.value
201
202 self._extra_unparsing_modules = extra_unparsing_modules
203 self._patch_symbol_table = patch_symbol_table
204 self._bug_report = bug_report
205
206 @contextmanager
207 def _temp_file(self, prefix: str | None = None, suffix: str | None = None) -> Iterator[_TemporaryFileWrapper]:
208 with NamedTemporaryFile(
209 'w',
210 dir=self.use_directory,
211 delete=not self.use_directory,
212 prefix=prefix,
213 suffix=suffix,
214 ) as ntf:
215 _LOGGER.info(f'Created temporary file: {ntf.name}')
216 yield ntf
217
218 @cached_property
219 def definition(self) -> KDefinition:
220 return read_kast_definition(self.definition_dir / 'compiled.json')
221
222 @property
223 def definition_hash(self) -> str:
224 return self.definition.hash
225
[docs]
226 def parse_token(self, ktoken: KToken, *, as_rule: bool = False) -> KInner:
227 input = KAstInput('rule' if as_rule else 'program')
228 proc_res = self._expression_kast(
229 ktoken.token,
230 input=input,
231 output=KAstOutput.JSON,
232 sort=ktoken.sort.name,
233 )
234 return KInner.from_dict(kast_term(json.loads(proc_res.stdout)))
235
[docs]
236 def kore_to_pretty(self, pattern: Pattern) -> str:
237 proc_res = self._expression_kast(
238 pattern.text,
239 input=KAstInput.KORE,
240 output=KAstOutput.PRETTY,
241 )
242 return proc_res.stdout
243
[docs]
244 def kore_to_kast(self, kore: Pattern) -> KInner:
245 try:
246 _LOGGER.info('Invoking kore_to_kast')
247 return kore_to_kast(self.definition, kore)
248 except ValueError as err:
249 _LOGGER.warning(err)
250
251 _LOGGER.warning(f'Falling back to using `kore-print` for Kore -> Kast: {kore.text}')
252 return KInner.from_dict(
253 kast_term(json.loads(kore_print(kore, definition_dir=self.definition_dir, output=PrintOutput.JSON)))
254 )
255
[docs]
256 def kast_to_kore(self, kast: KInner, sort: KSort | None = None, *, force_kast: bool = False) -> Pattern:
257 if not force_kast:
258 try:
259 _LOGGER.info('Invoking kast_to_kore')
260 return kast_to_kore(self.definition, kast, sort)
261 except ValueError as ve:
262 _LOGGER.warning(ve)
263
264 _LOGGER.warning(f'Falling back to using `kast` for KAst -> Kore: {kast}')
265 kast_json = {'format': 'KAST', 'version': KAst.version(), 'term': kast.to_dict()}
266 proc_res = self._expression_kast(
267 json.dumps(kast_json),
268 input=KAstInput.JSON,
269 output=KAstOutput.KORE,
270 sort=sort.name if sort is not None else None,
271 )
272 return KoreParser(proc_res.stdout).pattern()
273
274 def _add_sort_injection(self, pat: Pattern, isort: KSort, osort: KSort) -> Pattern:
275 if isort == osort:
276 return pat
277 if isort not in self.definition.subsorts(osort):
278 raise ValueError(
279 f'Could not find injection from subsort to supersort {isort} -> {osort} for pattern: {pat}'
280 )
281 return App('inj', [SortApp('Sort' + isort.name), SortApp('Sort' + osort.name)], [pat])
282
[docs]
283 def pretty_print(
284 self, kast: KAst, *, in_module: str | None = None, unalias: bool = True, sort_collections: bool = False
285 ) -> str:
286 defn = self.definition.let(main_module_name=in_module)
287
288 return PrettyPrinter(
289 defn,
290 extra_unparsing_modules=self._extra_unparsing_modules,
291 patch_symbol_table=self._patch_symbol_table,
292 unalias=unalias,
293 sort_collections=sort_collections,
294 ).print(kast)
295
296 def _expression_kast(
297 self,
298 expression: str,
299 *,
300 command: str | None = None,
301 input: str | KAstInput | None = None,
302 output: str | KAstOutput | None = None,
303 module: str | None = None,
304 sort: str | None = None,
305 # ---
306 check: bool = True,
307 ) -> CompletedProcess:
308 if len(expression) < 128 * 1024:
309 return _kast(
310 expression=expression,
311 command=command,
312 definition_dir=self.definition_dir,
313 input=input,
314 output=output,
315 module=module,
316 sort=sort,
317 temp_dir=self.use_directory,
318 check=check,
319 )
320
321 with self._temp_file() as ntf:
322 ntf.write(expression)
323 ntf.flush()
324
325 return _kast(
326 ntf.name,
327 command=command,
328 definition_dir=self.definition_dir,
329 input=input,
330 output=output,
331 module=module,
332 sort=sort,
333 temp_dir=self.use_directory,
334 check=check,
335 )