Emit per-node diagnostics, graph-level checks, and structural theorems.
(ir: WorkflowIR, prefix: str)
| 1100 | |
| 1101 | |
| 1102 | def _gen_structural(ir: WorkflowIR, prefix: str) -> list[str]: |
| 1103 | """Emit per-node diagnostics, graph-level checks, and structural theorems.""" |
| 1104 | lines: list[str] = [] |
| 1105 | thm = ir.name.replace("-", "_") |
| 1106 | ns = ", ".join(f"{prefix}_node{n.id}" for n in ir.nodes) |
| 1107 | pl = ", ".join(p.to_lean_typed() for p in ir.parameters) |
| 1108 | |
| 1109 | # STEP 2: Per-node diagnostics |
| 1110 | lines.append("/-") |
| 1111 | lines.append("=" * 72) |
| 1112 | lines.append("STEP 2: PER-NODE STRUCTURAL DIAGNOSTICS") |
| 1113 | lines.append("=" * 72) |
| 1114 | lines.append("-/") |
| 1115 | lines.append("") |
| 1116 | lines.append("#eval do") |
| 1117 | lines.append(f" let g := {prefix}Graph") |
| 1118 | lines.append(' for node in g.nodes do') |
| 1119 | lines.append(' let name := node.name.getD "(unnamed)"') |
| 1120 | lines.append(' IO.println s!"\\n--- Node {node.id}: \\"{name}\\" [{repr node.stepType}] ---"') |
| 1121 | lines.append(' IO.println s!" writesConsistent: {node.writesConsistent}"') |
| 1122 | lines.append(' IO.println s!" reachableFromEntry: {g.reachable g.entry node.id}"') |
| 1123 | lines.append(' for rv in node.reads do') |
| 1124 | lines.append(' let fromParam := g.parameters.any (fun p =>') |
| 1125 | lines.append(' p.name == rv.name && p.type.compatible rv.type)') |
| 1126 | lines.append(' let fromPred := g.nodes.any (fun o =>') |
| 1127 | lines.append(' o.id != node.id && g.reachable o.id node.id &&') |
| 1128 | lines.append(' (!g.isParallelScopedNode o.id || g.isParallelScopedNode node.id) &&') |
| 1129 | lines.append(' o.writes.any (fun w => w.name == rv.name && w.type.compatible rv.type))') |
| 1130 | lines.append(' let status := if fromParam || fromPred then "✓" else "✗ UNRESOLVED"') |
| 1131 | lines.append(' IO.println s!" read \\"{rv.name}\\" ({repr rv.type}): {status}"') |
| 1132 | lines.append(' for wv in node.writes do') |
| 1133 | lines.append(' IO.println s!" write \\"{wv.name}\\" ({repr wv.type})"') |
| 1134 | lines.append("") |
| 1135 | |
| 1136 | # STEP 3: Graph-level checks |
| 1137 | lines.append("/-") |
| 1138 | lines.append("=" * 72) |
| 1139 | lines.append("STEP 3: GRAPH-LEVEL STRUCTURAL CHECKS") |
| 1140 | lines.append("=" * 72) |
| 1141 | lines.append("-/") |
| 1142 | lines.append("") |
| 1143 | for prop in ("allWritesConsistent", "allReadResolvable", "edgesValid", |
| 1144 | "entryNodeValid", "exitNodesValid", "allExitsReachable", "noOrphanNodes"): |
| 1145 | lines.append(f"#eval {prefix}Graph.{prop}") |
| 1146 | lines.append(f"#eval {prefix}Graph.returnType") |
| 1147 | lines.append("") |
| 1148 | |
| 1149 | # STEP 4-5: Theorems |
| 1150 | lines.append("/-") |
| 1151 | lines.append("=" * 72) |
| 1152 | lines.append("STEP 4-5: THEOREMS") |
| 1153 | lines.append("=" * 72) |
| 1154 | lines.append("-/") |
| 1155 | lines.append("") |
| 1156 | for s, p in (("writesConsistent", "allWritesConsistent"), |
| 1157 | ("readsResolvable", "allReadResolvable"), |
| 1158 | ("edgesValid", "edgesValid"), |
| 1159 | ("entryValid", "entryNodeValid"), |
no test coverage detected