pyk.ktool.krun module

class KRun(definition_dir: Path, use_directory: Path | None = None, command: str = 'krun', bug_report: BugReport | None = None, extra_unparsing_modules: Iterable[KFlatModule] = (), patch_symbol_table: Callable[[SymbolTable], None] | None = None)

Bases: KPrint

command: str

krun(input_file: Path) → tuple[int, KInner]

run(pgm: Pattern, *, cmap: Mapping[str, str] | None = None, pmap: Mapping[str, str] | None = None, term: bool = False, depth: int | None = None, expand_macros: bool = True, search_final: bool = False, no_pattern: bool = False, output: KRunOutput | None = KRunOutput.PRETTY, check: bool = False, pipe_stderr: bool = True, bug_report: BugReport | None = None, debugger: bool = False) → None

run_pattern(pattern: Pattern, *, depth: int | None = None, expand_macros: bool = False, search_final: bool = False, no_pattern: bool = False, pipe_stderr: bool = True, check: bool = False, bug_report: BugReport | None = None, debugger: bool = False) → Pattern

run_process(pgm: Pattern, *, cmap: Mapping[str, str] | None = None, pmap: Mapping[str, str] | None = None, term: bool = False, depth: int | None = None, expand_macros: bool = True, search_final: bool = False, no_pattern: bool = False, output: KRunOutput | None = KRunOutput.PRETTY, pipe_stderr: bool = True, bug_report: BugReport | None = None, debugger: bool = False) → CompletedProcess

class KRunOutput(value)

Bases: Enum

An enumeration.

BINARY = 'binary'

JSON = 'json'

KAST = 'kast'

KORE = 'kore'

LATEX = 'latex'

NONE = 'none'

PRETTY = 'pretty'

PROGRAM = 'program'

llvm_interpret(definition_dir: str | Path, pattern: Pattern, *, depth: int | None = None) → Pattern

Execute the interpreter binary generated by the LLVM Backend.

Parameters:

• definition_dir – Path to the kompiled definition directory

• pattern – KORE pattern to start rewriting from

• depth – Maximal number of rewrite steps to take

Returns:

A pattern resulting from the rewrites

Raises:

RuntimeError – If the interpreter fails