Source code for pyk.kore.manip

 1from __future__ import annotations
 2
 3from typing import TYPE_CHECKING
 4
 5from .syntax import And, Assoc, EVar, MLQuant, Top
 6
 7if TYPE_CHECKING:
 8    from collections.abc import Collection
 9
10    from .syntax import Pattern
11
12


[docs]
13def conjuncts(pattern: Pattern) -> tuple[Pattern, ...]:
14    if isinstance(pattern, Top):
15        return ()
16    if isinstance(pattern, And):
17        return tuple(conjunct for op in pattern.ops for conjunct in conjuncts(op))
18    return (pattern,)


19
20


[docs]
21def free_occs(pattern: Pattern, *, bound_vars: Collection[str] = ()) -> dict[str, list[EVar]]:
22    occurrences: dict[str, list[EVar]] = {}
23
24    def collect(pattern: Pattern, bound_vars: set[str]) -> None:
25        if type(pattern) is EVar and pattern.name not in bound_vars:
26            if pattern.name in occurrences:
27                occurrences[pattern.name].append(pattern)
28            else:
29                occurrences[pattern.name] = [pattern]
30
31        elif isinstance(pattern, Assoc):
32            collect(pattern.app, bound_vars)
33
34        elif isinstance(pattern, MLQuant):
35            new_bound_vars = {pattern.var.name}.union(bound_vars)
36            collect(pattern.pattern, new_bound_vars)
37
38        else:
39            for sub_pattern in pattern.patterns:
40                collect(sub_pattern, bound_vars)
41
42    collect(pattern, set(bound_vars))
43    return occurrences