Translate proof to natural language. Args: proof_step: pr.Dependency with .name and .args refs: dict(hash: int) to keep track of derived predicates last_step: boolean to keep track whether this is the last step. Returns: a string of (pseudo) natural language of the proof step f
(
proof_step: pr.Dependency, refs: dict[tuple[str, ...], int], last_step: bool
)
| 95 | |
| 96 | |
| 97 | def proof_step_string( |
| 98 | proof_step: pr.Dependency, refs: dict[tuple[str, ...], int], last_step: bool |
| 99 | ) -> str: |
| 100 | """Translate proof to natural language. |
| 101 | |
| 102 | Args: |
| 103 | proof_step: pr.Dependency with .name and .args |
| 104 | refs: dict(hash: int) to keep track of derived predicates |
| 105 | last_step: boolean to keep track whether this is the last step. |
| 106 | |
| 107 | Returns: |
| 108 | a string of (pseudo) natural language of the proof step for human reader. |
| 109 | """ |
| 110 | premises, [conclusion] = proof_step |
| 111 | |
| 112 | premises_nl = ' & '.join( |
| 113 | [ |
| 114 | natural_language_statement(p) + ' [{:02}]'.format(refs[p.hashed()]) |
| 115 | for p in premises |
| 116 | ] |
| 117 | ) |
| 118 | |
| 119 | if not premises: |
| 120 | premises_nl = 'similarly' |
| 121 | |
| 122 | refs[conclusion.hashed()] = len(refs) |
| 123 | |
| 124 | conclusion_nl = natural_language_statement(conclusion) |
| 125 | if not last_step: |
| 126 | conclusion_nl += ' [{:02}]'.format(refs[conclusion.hashed()]) |
| 127 | |
| 128 | return f'{premises_nl} \u21d2 {conclusion_nl}' |
| 129 | |
| 130 | |
| 131 | def write_solution(g: gh.Graph, p: pr.Problem, out_file: str) -> None: |
no test coverage detected