Match all instances of a single theorem (rule).
(
g: gh.Graph,
cache: Callable[str, list[tuple[gm.Point, ...]]],
theorem: pr.Theorem
)
| 947 | |
| 948 | |
| 949 | def match_one_theorem( |
| 950 | g: gh.Graph, |
| 951 | cache: Callable[str, list[tuple[gm.Point, ...]]], |
| 952 | theorem: pr.Theorem |
| 953 | ) -> Generator[dict[str, gm.Point], None, None]: |
| 954 | """Match all instances of a single theorem (rule).""" |
| 955 | if cache is None: |
| 956 | cache = cache_match(g) |
| 957 | |
| 958 | if theorem.name in SKIP_THEOREMS: |
| 959 | return [] |
| 960 | |
| 961 | if theorem.name.split('_')[-1] in SKIP_THEOREMS: |
| 962 | return [] |
| 963 | |
| 964 | if theorem.name in BUILT_IN_FNS: |
| 965 | mps = BUILT_IN_FNS[theorem.name](g, cache, theorem) |
| 966 | else: |
| 967 | mps = match_generic(g, cache, theorem) |
| 968 | |
| 969 | mappings = [] |
| 970 | for mp in mps: |
| 971 | mappings.append(mp) |
| 972 | if len(mappings) > MAX_BRANCH: # cap branching at this number. |
| 973 | break |
| 974 | |
| 975 | return mappings |
| 976 | |
| 977 | |
| 978 | def match_all_theorems( |
no test coverage detected