Extract proof steps from the built DAG.
(
g: gh.Graph, goal: pr.Clause, merge_trivials: bool = False
)
| 132 | |
| 133 | |
| 134 | def get_proof_steps( |
| 135 | g: gh.Graph, goal: pr.Clause, merge_trivials: bool = False |
| 136 | ) -> tuple[ |
| 137 | list[pr.Dependency], |
| 138 | list[pr.Dependency], |
| 139 | list[tuple[list[pr.Dependency], list[pr.Dependency]]], |
| 140 | dict[tuple[str, ...], int], |
| 141 | ]: |
| 142 | """Extract proof steps from the built DAG.""" |
| 143 | goal_args = g.names2nodes(goal.args) |
| 144 | query = Dependency(goal.name, goal_args, None, None) |
| 145 | |
| 146 | setup, aux, log, setup_points = trace_back.get_logs( |
| 147 | query, g, merge_trivials=merge_trivials |
| 148 | ) |
| 149 | |
| 150 | refs = {} |
| 151 | setup = trace_back.point_log(setup, refs, set()) |
| 152 | aux = trace_back.point_log(aux, refs, setup_points) |
| 153 | |
| 154 | setup = [(prems, [tuple(p)]) for p, prems in setup] |
| 155 | aux = [(prems, [tuple(p)]) for p, prems in aux] |
| 156 | |
| 157 | return setup, aux, log, refs |
nothing calls this directly
no test coverage detected